Step.shx: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend as Step
Lines 132-146 of bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend&start_line=132&end_line=146

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

# 2^64 ((((h + (p2 + p1)) + i) + c) + 2^64 p3), distributed
def shx(+k: Nat, +h: Nat, +p2: Nat, +p1: Nat, +i: Nat, +c: Nat, +p3: Nat) -> {C.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(h, Nat.add(p2, p1)), i), c), C.shift(k, p3))) == Nat.add(Nat.add(Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), C.shift(k, c)), C.shift(k, C.shift(k, p3))) : Nat}:
  +w1 = Nat.add(Nat.add(h, Nat.add(p2, p1)), i)
  +ew1 = Equal.trans(Nat, C.shift(k, w1), Nat.add(C.shift(k, Nat.add(h, Nat.add(p2, p1))), C.shift(k, i)), Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)),
    WW.shift_add(k, Nat.add(h, Nat.add(p2, p1)), i),
    Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(k, i)), C.shift(k, Nat.add(h, Nat.add(p2, p1))), Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))),
      Equal.trans(Nat, C.shift(k, Nat.add(h, Nat.add(p2, p1))), Nat.add(C.shift(k, h), C.shift(k, Nat.add(p2, p1))), Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))),
        WW.shift_add(k, h, Nat.add(p2, p1)),
        Equal.cong(Nat, Nat, z => Nat.add(C.shift(k, h), z), C.shift(k, Nat.add(p2, p1)), Nat.add(C.shift(k, p2), C.shift(k, p1)), WW.shift_add(k, p2, p1)))))
  Equal.trans(Nat, C.shift(k, Nat.add(Nat.add(w1, c), C.shift(k, p3))), Nat.add(C.shift(k, Nat.add(w1, c)), C.shift(k, C.shift(k, p3))), Nat.add(Nat.add(Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), C.shift(k, c)), C.shift(k, C.shift(k, p3))),
    WW.shift_add(k, Nat.add(w1, c), C.shift(k, p3)),
    Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(k, C.shift(k, p3))), C.shift(k, Nat.add(w1, c)), Nat.add(Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), C.shift(k, c)),
      Equal.trans(Nat, C.shift(k, Nat.add(w1, c)), Nat.add(C.shift(k, w1), C.shift(k, c)), Nat.add(Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), C.shift(k, c)),
        WW.shift_add(k, w1, c),
        Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(k, c)), C.shift(k, w1), Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), ew1))))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift