def mid_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:148

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

148# 2^16 Mlo + (2^32 Mhi + 2^48 K) == 2^16 LH + 2^16 HL, from M == Mlo + 2^16 Mhi and M + 2^32 K == LH + HL
149def mid_eq(+m: Nat, +k: Nat, +mlo: Nat, +mhi: Nat, +lh: Nat, +hl: Nat, +e3: {Nat.add(m, WD.sc(32n, k)) == Nat.add(lh, hl) : Nat}, +e5: {m == Nat.add(mlo, WD.sc(16n, mhi)) : Nat}) -> {Nat.add(WD.sc(16n, mlo), Nat.add(WD.sc(32n, mhi), WD.sc(48n, k))) == Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)) : Nat}:
150  +a = WD.sc(16n, mlo)
151  +b = WD.sc(32n, mhi)
152  +c = WD.sc(48n, k)
153  +x1 = Nat.add(Nat.add(a, b), c)
154  +x2 = Nat.add(WD.sc(16n, m), c)
155  +x3 = Nat.add(WD.sc(16n, m), WD.sc(16n, WD.sc(32n, k)))
156  +x4 = WD.sc(16n, Nat.add(m, WD.sc(32n, k)))
157  +x5 = WD.sc(16n, Nat.add(lh, hl))
158  +eab = Equal.trans(Nat, Nat.add(a, b), Nat.add(a, WD.sc(16n, WD.sc(16n, mhi))), WD.sc(16n, m), cong_r(a, b, WD.sc(16n, WD.sc(16n, mhi)), Equal.sym(Nat, WD.sc(16n, WD.sc(16n, mhi)), b, sc_sc(16n, 16n, mhi))), Equal.trans(Nat, Nat.add(a, WD.sc(16n, WD.sc(16n, mhi))), WD.sc(16n, Nat.add(mlo, WD.sc(16n, mhi))), WD.sc(16n, m), A.sc_add(16n, mlo, WD.sc(16n, mhi)), cong_sc(16n, Nat.add(mlo, WD.sc(16n, mhi)), m, Equal.sym(Nat, m, Nat.add(mlo, WD.sc(16n, mhi)), e5))))
159  Equal.trans(Nat, Nat.add(a, Nat.add(b, c)), x1, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), Equal.sym(Nat, x1, Nat.add(a, Nat.add(b, c)), NA.add_assoc(a, b, c)),
160    Equal.trans(Nat, x1, x2, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), cong_l(Nat.add(a, b), WD.sc(16n, m), c, eab),
161      Equal.trans(Nat, x2, x3, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), cong_r(WD.sc(16n, m), c, WD.sc(16n, WD.sc(32n, k)), Equal.sym(Nat, WD.sc(16n, WD.sc(32n, k)), c, sc_sc(16n, 32n, k))),
162        Equal.trans(Nat, x3, x4, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), A.sc_add(16n, m, WD.sc(32n, k)),
163          Equal.trans(Nat, x4, x5, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), cong_sc(16n, Nat.add(m, WD.sc(32n, k)), Nat.add(lh, hl), e3), sc_add2(16n, lh, hl))))))