def low_l

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/step.bend:26

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/lib/u32alg.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

26def low_l(+k: Nat, +a: Nat, +b: Nat) -> {C.low(k, Nat.add(C.low(k, a), b)) == C.low(k, Nat.add(a, b)) : Nat}:
27  +la = C.low(k, a)
28  +h = C.high(k, a)
29  +e1 = Equal.trans(Nat, Nat.add(a, b), Nat.add(Nat.add(la, C.shift(k, h)), b), Nat.add(Nat.add(la, b), C.shift(k, h)),
30    Equal.cong(Nat, Nat, z => Nat.add(z, b), a, Nat.add(la, C.shift(k, h)), WW.low_high(k, a)),
31    A.add_rot(la, C.shift(k, h), b))
32  Equal.sym(Nat, C.low(k, Nat.add(a, b)), C.low(k, Nat.add(la, b)),
33    Equal.trans(Nat, C.low(k, Nat.add(a, b)), C.low(k, Nat.add(Nat.add(la, b), C.shift(k, h))), C.low(k, Nat.add(la, b)),
34      Equal.cong(Nat, Nat, z => C.low(k, z), Nat.add(a, b), Nat.add(Nat.add(la, b), C.shift(k, h)), e1),
35      WW.low_add_shift(k, Nat.add(la, b), h)))