Step.high_word: 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 179-189 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=179&end_line=189

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

# the new high word is Z mod 2^64 (t, vH, u: the sums of the implementation)
def high_word(+k: Nat, +vh: Nat, +p2: Nat, +p1: Nat, +p3: Nat, +vih: Nat, +c: Nat, +t: Nat, +vH: Nat, +u: Nat, +vH2: Nat, +hT: {C.low(k, t) == C.low(k, Nat.add(p2, p1)) : Nat}, +hH: {C.low(k, vH) == C.low(k, Nat.add(vh, t)) : Nat}, +hU: {C.low(k, u) == C.low(k, Nat.add(vH, vih)) : Nat}, +hV: {vH2 == C.low(k, Nat.add(u, c)) : Nat}) -> {C.low(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(p2, p1)), vih), c), C.shift(k, p3))) == vH2 : Nat}:
  +S = Nat.add(p2, p1)
  +V = Nat.add(vh, S)
  +W1 = Nat.add(V, vih)
  +eH = Equal.trans(Nat, C.low(k, vH), C.low(k, Nat.add(vh, t)), C.low(k, V), hH, low_add(k, vh, vh, t, S, {==}, hT))
  +eU = Equal.trans(Nat, C.low(k, u), C.low(k, Nat.add(vH, vih)), C.low(k, W1), hU, low_add(k, vH, V, vih, vih, eH, {==}))
  +eZ = Equal.trans(Nat, C.low(k, Nat.add(Nat.add(W1, c), C.shift(k, p3))), C.low(k, Nat.add(W1, c)), C.low(k, Nat.add(u, c)),
    WW.low_add_shift(k, Nat.add(W1, c), p3),
    Equal.sym(Nat, C.low(k, Nat.add(u, c)), C.low(k, Nat.add(W1, c)), low_add(k, u, W1, c, c, eU, {==})))
  Equal.trans(Nat, C.low(k, Nat.add(Nat.add(W1, c), C.shift(k, p3))), C.low(k, Nat.add(u, c)), vH2, eZ, Equal.sym(Nat, vH2, C.low(k, Nat.add(u, c)), hV))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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/random/pcg/step.bend&name=low_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_add_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift