def low_add_shift

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

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

400def low_add_shift(+k: Nat, +x: Nat, +y: Nat) -> {C.low(k, Nat.add(x, C.shift(k, y))) == C.low(k, x) : Nat}:
401  +l = C.low(k, x)
402  +h = C.high(k, x)
403  +e = Equal.trans(Nat, Nat.add(x, C.shift(k, y)), Nat.add(Nat.add(l, C.shift(k, h)), C.shift(k, y)), Nat.add(l, C.shift(k, Nat.add(h, y))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(k, y)), 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, y)), Nat.add(l, Nat.add(C.shift(k, h), C.shift(k, y))), Nat.add(l, C.shift(k, Nat.add(h, y))), NA.add_assoc(l, C.shift(k, h), C.shift(k, y)), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(C.shift(k, h), C.shift(k, y)), C.shift(k, Nat.add(h, y)), Equal.sym(Nat, C.shift(k, Nat.add(h, y)), Nat.add(C.shift(k, h), C.shift(k, y)), shift_add(k, h, y)))))
404  Equal.trans(Nat, C.low(k, Nat.add(x, C.shift(k, y))), C.low(k, Nat.add(l, C.shift(k, Nat.add(h, y)))), l, Equal.cong(Nat, Nat, t => C.low(k, t), Nat.add(x, C.shift(k, y)), Nat.add(l, C.shift(k, Nat.add(h, y))), e), low_u(k, l, Nat.add(h, y), low_fits(k, x)))