def b2_T

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

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/src/math/natural.bend as M
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/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend as DM
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as AQ

174# c < D: the root is S2 (it is at least S0 - 2), exact iff D - c == c - 2
175def b2_T(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hb: {Nat.is_lt(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == True{} : Bool}, +hge: {Nat.is_le(2n+S2, Nat.add(M.isqrt(C.shift(64n, n)), 2n)) == True{} : Bool}) -> {M.isqrt(C.shift(64n, n)) == S2 : Nat}:
176  +eD = N.sub_add(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), N.lt_le(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx, hb))
177  +e1 = L.subst(Nat, z => {Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == Nat.add(C.shift(64n, n), z) : Nat}, Dx, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Dx, eD), b_s1(n, S2, Dx, hnd))
178  +e2 = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), NA.add_comm(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Equal.trans(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(C.shift(64n, n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), e1, NA.add_swap(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))))
179  +e3 = NR.add_cancel(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), e2)
180  +hp = Equal.trans(Bool, Nat.is_lt(0n, Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Nat.is_lt(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), Nat.is_lt(0n, Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), WW.lt_cancel_l(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n, Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), z) == True{} : Bool}, Dx, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Dx, eD), L.subst(Nat, z => {Nat.is_lt(z, Dx) == True{} : Bool}, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), N.add_zero(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), hb)))
181  +hlt = L.subst(Nat, z => {Nat.is_lt(C.shift(64n, n), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Nat.mul(1n+S2, 1n+S2), Equal.sym(Nat, Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), e3), DM.lt_add_pos(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), hp))
182  +hup = N.lt_succ_le(M.isqrt(C.shift(64n, n)), S2, AQ.isqrt_lt(C.shift(64n, n), 1n+S2, hlt))
183  +hdn = L.subst(Nat, z => {Nat.is_le(2n+S2, z) == True{} : Bool}, Nat.add(M.isqrt(C.shift(64n, n)), 2n), 2n+M.isqrt(C.shift(64n, n)), NA.add_comm(M.isqrt(C.shift(64n, n)), 2n), hge)
184  N.le_antisym(M.isqrt(C.shift(64n, n)), S2, hup, hdn)