def high_add_shift

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

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

432def high_add_shift(+k: Nat, +x: Nat, +z: Nat) -> {C.high(k, Nat.add(x, C.shift(k, z))) == Nat.add(C.high(k, x), z) : Nat}:
433  +l = C.low(k, x)
434  +h = C.high(k, x)
435  +e = Equal.trans(Nat, Nat.add(x, C.shift(k, z)), Nat.add(Nat.add(l, C.shift(k, h)), C.shift(k, z)), Nat.add(l, C.shift(k, Nat.add(h, z))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(k, z)), x, Nat.add(l, C.shift(k, h)), low_high(k, x)), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(k, h)), C.shift(k, z)), Nat.add(l, Nat.add(C.shift(k, h), C.shift(k, z))), Nat.add(l, C.shift(k, Nat.add(h, z))), NA.add_assoc(l, C.shift(k, h), C.shift(k, z)), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(C.shift(k, h), C.shift(k, z)), C.shift(k, Nat.add(h, z)), Equal.sym(Nat, C.shift(k, Nat.add(h, z)), Nat.add(C.shift(k, h), C.shift(k, z)), shift_add(k, h, z)))))
436  Equal.trans(Nat, C.high(k, Nat.add(x, C.shift(k, z))), C.high(k, Nat.add(l, C.shift(k, Nat.add(h, z)))), Nat.add(h, z), Equal.cong(Nat, Nat, t => C.high(k, t), Nat.add(x, C.shift(k, z)), Nat.add(l, C.shift(k, Nat.add(h, z))), e), high_u(k, l, Nat.add(h, z), low_fits(k, x)))