def cl_f_o

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqr.bend:352
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend as F64sqr
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/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
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/word.bend as WD
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/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend as SK
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend as QV

352# q = 2^32 (r = 2 s): taken as 2^32 - 1 with u = 2 s
353# over an open all-ones word o: v(4294967295) would be expanded in unary
354def cl_f_o(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hz: {U32.is_zero(X.hi(qq)) == False{} : Bool}, +o: U32, +po: {o == U32{WD.mask(32n, 32n)} : U32}) -> {F.sq_qu(e, X.lo(X.isqrt(nh)), o, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:
355  +e1 = Equal.trans(Nat, 1n+v(o), WD.sc(32n, one), C.shift(32n, one), W64S.mask_v(32n, {==}, one, h1, o, po), Equal.sym(Nat, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one)))
356  +hQ = L.subst(Nat, z => {Nat.is_lt(v(o), z) == True{} : Bool}, 1n+v(o), C.shift(32n, one), e1, N.lt_succ(v(o)))
357  +eU = QV.dw_v(one, h1, nh, h62, h60)
358  +hhi = WA.pos_ne(v(X.hi(qq)), Equal.trans(Bool, Nat.is_eq(v(X.hi(qq)), 0n), U32.is_zero(X.hi(qq)), False{}, Equal.sym(Bool, U32.is_zero(X.hi(qq)), Nat.is_eq(v(X.hi(qq)), 0n), LW.zero_nat(X.hi(qq))), hz))
359  +g1 = N.le_trans(C.shift(32n, one), C.shift(32n, v(X.hi(qq))), SW.value(qq), WW.shift_mono(32n, one, v(X.hi(qq)), L.subst(Nat, z => {Nat.is_le(z, v(X.hi(qq))) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), hhi)), L.subst(Nat, z => {Nat.is_le(C.shift(32n, v(X.hi(qq))), z) == True{} : Bool}, Nat.add(C.shift(32n, v(X.hi(qq))), v(X.lo(qq))), SW.value(qq), Equal.trans(Nat, Nat.add(C.shift(32n, v(X.hi(qq))), v(X.lo(qq))), Nat.add(v(X.lo(qq)), C.shift(32n, v(X.hi(qq)))), SW.value(qq), NA.add_comm(C.shift(32n, v(X.hi(qq))), v(X.lo(qq))), Equal.sym(Nat, SW.value(qq), Nat.add(v(X.lo(qq)), C.shift(32n, v(X.hi(qq)))), WA.val_eta(qq))), N.le_add_right(C.shift(32n, v(X.hi(qq))), v(X.lo(qq)))))
360  +hqD = L.subst(Nat, z => {Nat.is_le(Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}, Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(qq), Equal.sym(Nat, SW.value(qq), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), hq), QV.dq_le(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.d_pos(one, h1, nh, h62, h60)))
361  +g2 = SK.qb(one, h1, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(qq), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), hqD, QV.r_le(one, h1, nh, h62, h60), QV.d_pos(one, h1, nh, h62, h60))
362  +eq1 = N.le_antisym(SW.value(qq), C.shift(32n, one), g2, g1)
363  +g3 = L.subst(Nat, z => {Nat.is_le(Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}, SW.value(qq), C.shift(32n, one), eq1, hqD)
364  +eP = Equal.trans(Nat, Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), C.shift(32n, one)), C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), NA.mul_comm(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.sym(Nat, C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), C.shift(32n, one)), WW.shift_mul_one(32n, one, h1, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))))
365  +g4 = L.subst(Nat, z => {Nat.is_le(z, C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}, Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), eP, g3)
366  +g5 = N.le_antisym(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.r_le(one, h1, nh, h62, h60), shl_le_inv(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), g4))
367  +hc0 = Equal.trans(Nat, Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), NA.add_comm(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.trans(Nat, Nat.add(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), 1n+v(o), C.shift(32n, one), e1), Equal.trans(Nat, Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), eP, Equal.cong(Nat, Nat, z => C.shift(32n, z), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.sym(Nat, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), g5)))))
368  +hc = Equal.trans(Nat, Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), z), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), eU), hc0)
369  +hU = L.subst(Nat, z => {Nat.is_le(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Equal.sym(Nat, v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), eU), N.le_refl(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))
370  qu_v(one, h1, nh, h62, h60, e, x, hx, o, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))), hc, hU, hQ)
Uses (54)

Used by (1)

bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr:cl_f