def ident

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqr.bend:61

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend as SK

61# N + q^2 == S0^2 + u 2^32
62def ident(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}) -> {Nat.add(C.shift(32n, C.shift(32n, n)), Nat.mul(Q, Q)) == Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)) : Nat}:
63  +e0 = Equal.cong(Nat, Nat, z => Nat.mul(z, z), Nat.add(Q, C.shift(32n, s)), Nat.add(C.shift(32n, s), Q), NA.add_comm(Q, C.shift(32n, s)))
64  +e1 = SK.sqa(C.shift(32n, s), Q)
65  +e2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), z), Nat.mul(Q, Q)), Nat.add(Nat.mul(C.shift(32n, s), Q), Nat.mul(C.shift(32n, s), Q)), C.shift(32n, Nat.mul(Q, D)), SK.uw2(s, Q, D, hD))
66  +eS = Equal.trans(Nat, Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(C.shift(32n, s), Q), Nat.add(C.shift(32n, s), Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), e0, Equal.trans(Nat, Nat.mul(Nat.add(C.shift(32n, s), Q), Nat.add(C.shift(32n, s), Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(Nat.mul(C.shift(32n, s), Q), Nat.mul(C.shift(32n, s), Q))), Nat.mul(Q, Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), e1, e2))
67  +f1 = Equal.sym(Nat, Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, rr))), C.shift(32n, C.shift(32n, n)), SK.usq(s, rr, n, hn))
68  +f2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, z)), C.shift(32n, rr), Nat.add(Nat.mul(Q, D), U), Equal.sym(Nat, Nat.add(Nat.mul(Q, D), U), C.shift(32n, rr), hc))
69  +f3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), z), C.shift(32n, Nat.add(Nat.mul(Q, D), U)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U)), WW.shift_add(32n, Nat.mul(Q, D), U))
70  +eN = Equal.trans(Nat, C.shift(32n, C.shift(32n, n)), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, rr))), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), f1, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, rr))), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.add(Nat.mul(Q, D), U))), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), f2, f3))
71  +g1 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(Q, Q)), C.shift(32n, C.shift(32n, n)), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), eN)
72  +g2 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, U)), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), eS)
73  Equal.trans(Nat, Nat.add(C.shift(32n, C.shift(32n, n)), Nat.mul(Q, Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), g1, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), Nat.mul(Q, Q)), Nat.add(Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), C.shift(32n, U)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), C.shift(32n, U)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), Nat.mul(Q, Q)), rearr(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U), Nat.mul(Q, Q))), Equal.sym(Nat, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), C.shift(32n, U)), g2)))