def low_high

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:91

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

91def low_high(+k: Nat, +n: Nat) -> {n == Nat.add(C.low(k, n), C.shift(k, C.high(k, n))) : Nat}:
92  match k:
93    case 0n:
94      {==}
95    case 1n+ +p:
96      +h = C.half(n)
97      +l = C.low(p, h)
98      +s = C.shift(p, C.high(p, h))
99      +e1 = Equal.trans(Nat, n, Nat.add(C.bit(n), Nat.double(h)), Nat.add(C.bit(n), Nat.double(Nat.add(l, s))), hb(n), Equal.cong(Nat, Nat, t => Nat.add(C.bit(n), Nat.double(t)), h, Nat.add(l, s), low_high(p, h)))
100      +e2 = Equal.trans(Nat, Nat.add(C.bit(n), Nat.double(Nat.add(l, s))), Nat.add(C.bit(n), Nat.add(Nat.double(l), Nat.double(s))), Nat.add(Nat.add(C.bit(n), Nat.double(l)), Nat.double(s)), Equal.cong(Nat, Nat, t => Nat.add(C.bit(n), t), Nat.double(Nat.add(l, s)), Nat.add(Nat.double(l), Nat.double(s)), NA.double_add(l, s)), Equal.sym(Nat, Nat.add(Nat.add(C.bit(n), Nat.double(l)), Nat.double(s)), Nat.add(C.bit(n), Nat.add(Nat.double(l), Nat.double(s))), NA.add_assoc(C.bit(n), Nat.double(l), Nat.double(s))))
101      Equal.trans(Nat, n, Nat.add(C.bit(n), Nat.double(Nat.add(l, s))), Nat.add(Nat.add(C.bit(n), Nat.double(l)), Nat.double(s)), e1, e2)