def jfg

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:98
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as F64sqc
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
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/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend as SQ2
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT

98# the exponent step of sqn_c for any parity: 2a + p + s = 2b + q + 2171 with
99# s <= 53, p <= 1, K <= 1022 and 2K + p = 2043 + u gives
100# 2 ((a - b) - K) + 72 + s + u = 200 + q
101def jfg(+a: Nat, +b: Nat, +sa: Nat, +p: Nat, +q: Nat, +K: Nat, +u: Nat, +hEN2: {Nat.add(Nat.add(Nat.add(a, a), p), sa) == Nat.add(Nat.add(Nat.add(b, b), q), 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hp: {Nat.is_le(p, 1n) == True{} : Bool}, +hK: {Nat.is_le(K, 1022n) == True{} : Bool}, +hKu: {Nat.add(Nat.add(K, K), p) == Nat.add(2043n, u) : Nat}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), K), Nat.sub(Nat.sub(a, b), K)), Nat.add(72n, Nat.add(sa, u))) == Nat.add(200n, q) : Nat}:
102  +aa = Nat.add(a, a)
103  +bb = Nat.add(b, b)
104  +c54 = Nat.add(1n, 53n)
105  +l0 = Equal.trans(Bool, Nat.is_le(Nat.add(bb, 2171n), Nat.add(Nat.add(bb, q), 2171n)), Nat.is_le(bb, Nat.add(bb, q)), True{}, FR.le_cancel_r(bb, Nat.add(bb, q), 2171n), N.le_add_right(bb, q))
106  +l1 = L.subst(Nat, z => {Nat.is_le(Nat.add(bb, 2171n), z) == True{} : Bool}, Nat.add(Nat.add(bb, q), 2171n), Nat.add(Nat.add(aa, p), sa), Equal.sym(Nat, Nat.add(Nat.add(aa, p), sa), Nat.add(Nat.add(bb, q), 2171n), hEN2), l0)
107  +l2 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(aa, c54)) == True{} : Bool}, Nat.add(aa, Nat.add(p, sa)), Nat.add(Nat.add(aa, p), sa), Equal.sym(Nat, Nat.add(Nat.add(aa, p), sa), Nat.add(aa, Nat.add(p, sa)), NA.add_assoc(aa, p, sa)), N.le_add_left(Nat.add(p, sa), c54, aa, SQ2.le_add2(p, 1n, sa, 53n, hp, hsa)))
108  +l3 = N.le_trans(Nat.add(bb, 2171n), Nat.add(Nat.add(aa, p), sa), Nat.add(aa, c54), l1, l2)
109  +e4 = Equal.trans(Nat, Nat.add(Nat.add(bb, 2117n), c54), Nat.add(bb, Nat.add(2117n, c54)), Nat.add(bb, 2171n), NA.add_assoc(bb, 2117n, c54), Equal.cong(Nat, Nat, z => Nat.add(bb, z), Nat.add(2117n, c54), 2171n, {==}))
110  +l4 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(aa, c54)) == True{} : Bool}, Nat.add(bb, 2171n), Nat.add(Nat.add(bb, 2117n), c54), Equal.sym(Nat, Nat.add(Nat.add(bb, 2117n), c54), Nat.add(bb, 2171n), e4), l3)
111  +l5 = Equal.trans(Bool, Nat.is_le(Nat.add(bb, 2117n), aa), Nat.is_le(Nat.add(Nat.add(bb, 2117n), c54), Nat.add(aa, c54)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(Nat.add(bb, 2117n), c54), Nat.add(aa, c54)), Nat.is_le(Nat.add(bb, 2117n), aa), FR.le_cancel_r(Nat.add(bb, 2117n), aa, c54)), l4)
112  +k3 = N.le_add_left(Nat.add(K, K), Nat.add(1022n, 1022n), bb, SQ2.le_add2(K, 1022n, K, 1022n, hK, hK))
113  +k5 = N.le_trans(Nat.add(bb, Nat.add(K, K)), Nat.add(bb, Nat.add(1022n, 1022n)), Nat.add(bb, 2117n), k3, N.le_add_left(Nat.add(1022n, 1022n), 2117n, bb, {==}))
114  +k6 = N.le_trans(Nat.add(bb, Nat.add(K, K)), Nat.add(bb, 2117n), aa, k5, l5)
115  +eBK = Equal.trans(Nat, Nat.add(Nat.add(b, K), Nat.add(b, K)), Nat.add(b, Nat.add(K, Nat.add(b, K))), Nat.add(bb, Nat.add(K, K)), NA.add_assoc(b, K, Nat.add(b, K)), Equal.trans(Nat, Nat.add(b, Nat.add(K, Nat.add(b, K))), Nat.add(b, Nat.add(b, Nat.add(K, K))), Nat.add(bb, Nat.add(K, K)), Equal.cong(Nat, Nat, z => Nat.add(b, z), Nat.add(K, Nat.add(b, K)), Nat.add(b, Nat.add(K, K)), NA.add_swap(K, b, K)), Equal.sym(Nat, Nat.add(bb, Nat.add(K, K)), Nat.add(b, Nat.add(b, Nat.add(K, K))), NA.add_assoc(b, b, Nat.add(K, K)))))
116  +k7 = L.subst(Nat, z => {Nat.is_le(z, aa) == True{} : Bool}, Nat.add(bb, Nat.add(K, K)), Nat.add(Nat.add(b, K), Nat.add(b, K)), Equal.sym(Nat, Nat.add(Nat.add(b, K), Nat.add(b, K)), Nat.add(bb, Nat.add(K, K)), eBK), k6)
117  +hbK = halve(Nat.add(b, K), a, k7)
118  +hb = N.le_trans(b, Nat.add(b, K), a, N.le_add_right(b, K), hbK)
119  +hK2 = RT.le_sub(K, b, a, L.subst(Nat, z => {Nat.is_le(z, a) == True{} : Bool}, Nat.add(b, K), Nat.add(K, b), NA.add_comm(b, K), hbK))
120  +D = Nat.sub(Nat.sub(a, b), K)
121  +DD = Nat.add(D, D)
122  +ea = Equal.trans(Nat, a, Nat.add(b, Nat.sub(a, b)), Nat.add(b, Nat.add(K, D)), Equal.sym(Nat, Nat.add(b, Nat.sub(a, b)), a, N.sub_add(a, b, hb)), Equal.cong(Nat, Nat, z => Nat.add(b, z), Nat.sub(a, b), Nat.add(K, D), Equal.sym(Nat, Nat.add(K, D), Nat.sub(a, b), N.sub_add(Nat.sub(a, b), K, hK2))))
123  +h2 = L.subst(Nat, z => {Nat.add(Nat.add(Nat.add(z, z), p), sa) == Nat.add(Nat.add(bb, q), 2171n) : Nat}, a, Nat.add(b, Nat.add(K, D)), ea, hEN2)
124  +h3 = Equal.trans(Nat, Nat.add(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa))), Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), sa), Nat.add(bb, Nat.add(q, 2171n)), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), sa), Nat.add(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa))), jperm(b, K, D, p, sa)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), sa), Nat.add(Nat.add(bb, q), 2171n), Nat.add(bb, Nat.add(q, 2171n)), h2, NA.add_assoc(bb, q, 2171n)))
125  +h4 = NR.add_cancel(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa)), Nat.add(q, 2171n), h3)
126  +h5 = L.subst(Nat, z => {Nat.add(z, Nat.add(DD, sa)) == Nat.add(q, 2171n) : Nat}, Nat.add(Nat.add(K, K), p), Nat.add(2043n, u), hKu, h4)
127  +W = Nat.add(u, Nat.add(DD, sa))
128  +m1 = Equal.trans(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(2043n, W), Nat.add(1971n, Nat.add(72n, W)), NA.add_assoc(2043n, u, Nat.add(DD, sa)), {==})
129  +m2 = Equal.trans(Nat, W, Nat.add(DD, Nat.add(u, sa)), Nat.add(DD, Nat.add(sa, u)), NA.add_swap(u, DD, sa), Equal.cong(Nat, Nat, z => Nat.add(DD, z), Nat.add(u, sa), Nat.add(sa, u), NA.add_comm(u, sa)))
130  +m3 = Equal.trans(Nat, Nat.add(72n, W), Nat.add(72n, Nat.add(DD, Nat.add(sa, u))), Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), Equal.cong(Nat, Nat, z => Nat.add(72n, z), W, Nat.add(DD, Nat.add(sa, u)), m2), NA.add_swap(72n, DD, Nat.add(sa, u)))
131  +m4 = Equal.trans(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(1971n, Nat.add(72n, W)), Nat.add(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u)))), m1, Equal.cong(Nat, Nat, z => Nat.add(1971n, z), Nat.add(72n, W), Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), m3))
132  +r1 = Equal.trans(Nat, Nat.add(q, 2171n), Nat.add(2171n, q), Nat.add(1971n, Nat.add(200n, q)), NA.add_comm(q, 2171n), {==})
133  +fin = Equal.trans(Nat, Nat.add(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u)))), Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(1971n, Nat.add(200n, q)), Equal.sym(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u)))), m4), Equal.trans(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(q, 2171n), Nat.add(1971n, Nat.add(200n, q)), h5, r1))
134  NR.add_cancel(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), Nat.add(200n, q), fin)
def jfg

Uses (22)

Used by (4)
