def x2_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64div.bend:93

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as PD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as WM

93def x2_eq(+one: Nat, +h1: {one == 1n : Nat}, +h: Nat, +g1: Nat, +g2: Nat) -> {Nat.add(Nat.mul(Nat.add(Nat.mul(h, 65536n), g1), 65536n), g2) == Nat.add(Nat.add(WD.sc(16n, g1), g2), WD.sc(32n, h)) : Nat}:
94  +h16 = WD.sc(16n, h)
95  +a1 = Nat.add(Nat.mul(h, 65536n), g1)
96  +e1 = WM.cong_l(Nat.mul(h, 65536n), h16, g1, PD.mul_pow(one, h1, 16n, h, 65536n, k65536(one, h1)))
97  +e2 = Equal.trans(Nat, Nat.mul(a1, 65536n), Nat.mul(Nat.add(h16, g1), 65536n), WD.sc(16n, Nat.add(h16, g1)), Equal.cong(Nat, Nat, t => Nat.mul(t, 65536n), a1, Nat.add(h16, g1), e1), PD.mul_pow(one, h1, 16n, Nat.add(h16, g1), 65536n, k65536(one, h1)))
98  +e3 = Equal.trans(Nat, WD.sc(16n, Nat.add(h16, g1)), Nat.add(WD.sc(16n, h16), WD.sc(16n, g1)), Nat.add(WD.sc(32n, h), WD.sc(16n, g1)), WM.sc_add2(16n, h16, g1), WM.cong_l(WD.sc(16n, h16), WD.sc(32n, h), WD.sc(16n, g1), WM.sc_sc(16n, 16n, h)))
99  +pp = WD.sc(32n, h)
100  +aa = WD.sc(16n, g1)
101  +e4 = WM.cong_l(Nat.mul(a1, 65536n), Nat.add(pp, aa), g2, Equal.trans(Nat, Nat.mul(a1, 65536n), WD.sc(16n, Nat.add(h16, g1)), Nat.add(pp, aa), e2, e3))
102  Equal.trans(Nat, Nat.add(Nat.mul(a1, 65536n), g2), Nat.add(Nat.add(pp, aa), g2), Nat.add(Nat.add(aa, g2), pp), e4, Equal.trans(Nat, Nat.add(Nat.add(pp, aa), g2), Nat.add(pp, Nat.add(aa, g2)), Nat.add(Nat.add(aa, g2), pp), NA.add_assoc(pp, aa, g2), NA.add_comm(pp, Nat.add(aa, g2))))