def half_limbs

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

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/lemmas/proofs/nat_algebra.bend as NA

368# half(x + shift(1 + p, y)) == half(x) + bit(y) shift(p, one) + shift(1 + p, half(y))
369def half_limbs(+p: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat) -> {C.half(Nat.add(x, C.shift(1n+p, y))) == Nat.add(Nat.add(C.half(x), Nat.mul(C.bit(y), C.shift(p, one))), C.shift(1n+p, C.half(y))) : Nat}:
370  +hx = C.half(x)
371  +b = C.bit(y)
372  +hy = C.half(y)
373  +e1 = half_dbl(x, C.shift(p, y))
374  +e2 = Equal.trans(Nat, C.shift(p, y), C.shift(p, Nat.add(b, Nat.double(hy))), Nat.add(C.shift(p, b), C.shift(p, Nat.double(hy))), Equal.cong(Nat, Nat, t => C.shift(p, t), y, Nat.add(b, Nat.double(hy)), hb(y)), shift_add(p, b, Nat.double(hy)))
375  +e3 = Equal.trans(Nat, Nat.add(C.shift(p, b), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, 1n)), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(p, Nat.double(hy))), C.shift(p, b), Nat.mul(b, C.shift(p, 1n)), shift_mul(p, b)), Equal.trans(Nat, Nat.add(Nat.mul(b, C.shift(p, 1n)), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, one)), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))), Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(b, C.shift(p, t)), C.shift(p, Nat.double(hy))), 1n, one, Equal.sym(Nat, one, 1n, h1)), Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(b, C.shift(p, one)), t), C.shift(p, Nat.double(hy)), Nat.double(C.shift(p, hy)), shift_dbl(p, hy))))
376  +e4 = Equal.cong(Nat, Nat, t => Nat.add(hx, t), C.shift(p, y), Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))), Equal.trans(Nat, C.shift(p, y), Nat.add(C.shift(p, b), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))), e2, e3))
377  Equal.trans(Nat, C.half(Nat.add(x, Nat.double(C.shift(p, y)))), Nat.add(hx, C.shift(p, y)), Nat.add(Nat.add(hx, Nat.mul(b, C.shift(p, one))), Nat.double(C.shift(p, hy))), e1, Equal.trans(Nat, Nat.add(hx, C.shift(p, y)), Nat.add(hx, Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy)))), Nat.add(Nat.add(hx, Nat.mul(b, C.shift(p, one))), Nat.double(C.shift(p, hy))), e4, Equal.sym(Nat, Nat.add(Nat.add(hx, Nat.mul(b, C.shift(p, one))), Nat.double(C.shift(p, hy))), Nat.add(hx, Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy)))), NA.add_assoc(hx, Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))))))