def b1_T

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

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

153# D <= c: the root is S1, exact iff D == c
154def b1_T(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hpos: {Nat.is_lt(0n, Dx) == True{} : Bool}, +hs: {Nat.is_le(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == True{} : Bool}) -> {M.isqrt(C.shift(64n, n)) == 1n+S2 : Nat}:
155  +e1 = b_s1(n, S2, Dx, hnd)
156  +a1 = N.le_add_left(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n), hs)
157  +a2 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) == True{} : Bool}, Nat.add(C.shift(64n, n), Dx), Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Equal.sym(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(C.shift(64n, n), Dx), e1), a1)
158  +a3 = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n)), NA.add_comm(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) == True{} : Bool}, 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.mul(1n+S2, 1n+S2)), NA.add_comm(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), a2))
159  +hle = Equal.trans(Bool, Nat.is_le(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)), Nat.is_le(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n))), Nat.is_le(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)), NR.le_add_cancel(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2), C.shift(64n, n))), a3)
160  +hlt = L.subst(Nat, z => {Nat.is_lt(C.shift(64n, n), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Dx), Nat.mul(2n+S2, 2n+S2), hnd, DM.lt_add_pos(C.shift(64n, n), Dx, hpos))
161  AQ.isqrt_char(C.shift(64n, n), 1n+S2, hle, hlt)