F64sqf.sqg: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqf.bend as F64sqf Lines 42-60 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqf.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqf.bend&start_line=42&end_line=60 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/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/lemmas/proofs/nat_algebra.bend as NA 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/f64sqv.bend as QV import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend as QR import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqs.bend as QS import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqx.bend as QX # the generic even-exponent root def sqg(+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}, +MX: Nat, +sa: Nat, +ci: Nat, +cs: Nat, +hnh: {SW.value(nh) == C.shift(8n, C.shift(Nat.add(sa, ci), MX)) : Nat}, +Ep: Nat, +p: Nat, +hp: {Nat.add(Nat.add(p, p), 1075n) == Nat.add(Ep, 4096n) : Nat}, +hpe: {Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n) == p : Nat}, +EN: Nat, +hE: {Nat.add(Ep, ci) == EN : Nat}, +XX: Nat, +hEN: {Nat.add(EN, sa) == Nat.add(XX, 2171n) : Nat}, +Mq: Nat, +hMq: {C.shift(200n, Mq) == C.shift(Nat.add(200n, cs), MX) : Nat}, +Xq: Nat, +q: Nat, +hq: {Nat.add(Nat.add(q, q), cs) == XX : Nat}, +hqd: {Nat.div(Xq, 2n) == q : Nat}, +j: Nat, +hj: {Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))) == Nat.add(200n, cs) : Nat}) -> {F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), nh) == SF.sqrt_even(Mq, Xq) : F.F64}: +hpv = Equal.cong(Nat, Nat, z => Nat.add(z, 1048n), Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), p, hpe) +pge = N.not_lt_le(p, 1132n, p_ge(p, Ep, hp, Nat.is_lt(p, 1132n), {==})) +hle = Equal.trans(Bool, Nat.is_le(Nat.add(1132n, 1048n), Nat.add(p, 1048n)), Nat.is_le(1132n, p), True{}, FR.le_cancel_r(1132n, p, 1048n), pge) +hxs = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(p, 1048n), 2180n), 2180n), Nat.add(2180n, Nat.sub(Nat.add(p, 1048n), 2180n)), Nat.add(p, 1048n), NA.add_comm(Nat.sub(Nat.add(p, 1048n), 2180n), 2180n), N.sub_add(Nat.add(p, 1048n), 2180n, hle)) +hx = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(p, 1048n), 2180n), 2180n), Nat.add(p, 1048n), Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), hxs, Equal.sym(Nat, Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), Nat.add(p, 1048n), hpv)) +r1 = QR.sqr_root_v(one, h1, nh, h62, h60, Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), Nat.sub(Nat.add(p, 1048n), 2180n), hx) +hEs = Equal.trans(Nat, Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), Nat.sub(Nat.add(q, 1500n), 101n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, 1500n), 101n), Nat.div(Xq, 2n), q, hqd), FR.sub_add_a(q, 1500n, 101n, {==})) +g = QX.sqexp(q, p, j, Nat.sub(Nat.add(p, 1048n), 2180n), XX, EN, Ep, sa, ci, cs, hq, hp, hE, hEN, hj, hxs) +hEx = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), 1n+j), Nat.add(Nat.add(q, 1399n), 1n+j), Nat.sub(Nat.add(p, 1048n), 2180n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n+j), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), Nat.add(q, 1399n), hEs), g) +r2 = QS.sq_spec(one, h1, C.shift(64n, SW.value(nh)), j, QV.s62(one, h1, nh, h62, h60), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), Nat.sub(Nat.add(p, 1048n), 2180n), hEx) +e1 = Equal.cong(Nat, Nat, z => C.shift(j, C.shift(j, C.shift(64n, z))), SW.value(nh), C.shift(8n, C.shift(Nat.add(sa, ci), MX)), hnh) +e2 = shift_nest(j, Nat.add(sa, ci), MX) +e3 = Equal.cong(Nat, Nat, z => C.shift(z, MX), Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), Nat.add(200n, cs), hj) +eN = Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(Nat.add(sa, ci), MX))))), C.shift(Nat.add(200n, cs), MX), e1, Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(Nat.add(sa, ci), MX))))), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), MX), C.shift(Nat.add(200n, cs), MX), e2, e3)) +eNs = Equal.trans(Nat, C.shift(200n, Mq), C.shift(Nat.add(200n, cs), MX), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), hMq, Equal.sym(Nat, C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), C.shift(Nat.add(200n, cs), MX), eN)) +r3 = Equal.cong(Nat, F.F64, z => SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(z)), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(z), 2n), z)))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), C.shift(200n, Mq), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), eNs) Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), 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)))))), Nat.sub(Nat.add(p, 1048n), 2180n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(200n, Mq))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(200n, Mq)), 2n), C.shift(200n, Mq))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), r1, Equal.trans(F.F64, 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)))))), Nat.sub(Nat.add(p, 1048n), 2180n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh))))), 2n), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(200n, Mq))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(200n, Mq)), 2n), C.shift(200n, Mq))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), Equal.sym(F.F64, SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh))))), 2n), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), 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)))))), Nat.sub(Nat.add(p, 1048n), 2180n)), r2), Equal.sym(F.F64, SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(200n, Mq))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(200n, Mq)), 2n), C.shift(200n, Mq))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh))))), 2n), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), r3))) Uses (37): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=not_lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=le_cancel_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=sub_add_a https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqf.bend&name=p_ge https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqf.bend&name=shift_nest https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend&name=sqr_root_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqs.bend&name=sq_spec https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend&name=s62 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqx.bend&name=sqexp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=b2n https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=round https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=sqrt_even https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=jam https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=off https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=sq_root https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=isqrt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64