def iroot_big

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:1193

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/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
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/math/typed/u32.bend as U32P
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/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as RT
import bend-collections-laws-math@1.0.0.0/src/math/pow2.bend as P2
import bend-collections-laws-math@1.0.0.0/proofs/math/pow2/pow2.bend as PP

1193def iroot_big(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +kp: Nat) -> {v(G.iroot_k(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp)) == M.iroot_k(v(n), 2n+kp) : Nat}:
1194  +bg = G.bit_length(~U32, ~I.u32_op, ~I.u32_is, n)
1195  +bl = M.bit_length(v(n))
1196  +ebl = bit_length_k(K, hK, n)
1197  +hn = U32P.val_lt(1n, {==}, K, hK, n)
1198  +hbl = L.subst(Nat, z => {Nat.is_le(bl, z) == True{} : Bool}, K, 32n, hK, NF.bl_le_n(K, v(n), hn))
1199  +E2 = {1n+Nat.div(bl, 2n+kp) : Nat}
1200  +E = {1n+Nat.div(bg, 2n+kp) : Nat}
1201  +eE = Equal.cong(Nat, Nat, t => 1n+Nat.div(t, 2n+kp), bg, bl, ebl)
1202  +hE2 = NF.e_lt(kp, bl, hbl)
1203  +hE = L.subst(Nat, z => {Nat.is_lt(z, 32n) == True{} : Bool}, E2, E, Equal.sym(Nat, E, E2, eE), hE2)
1204  +hi = I.u32_op(NM.Pow2{E})
1205  +W = C.pow2(E2)
1206  ehi0 = LW.ops_pow2(E, hE)
1207  +ehi = Equal.trans(Nat, v(hi), C.pow2(E), W, ehi0, Equal.cong(Nat, Nat, t => C.pow2(t), E, E2, eE))
1208  +zero = I.u32_op(NM.ZeroOp{})
1209  +m = G.imid(~U32, ~I.u32_op, zero, hi)
1210  +hm = imid_v(K, hK, zero, hi, 0n, W, zero_v(), ehi)
1211  +hmore = ltv(I.u32_op(NM.One{}), hi, 1n, W, one_v(), ehi)
1212  +hhit = Equal.trans(Bool, G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp, m), Nat.is_le(Nat.pow(v(m), 2n+kp), v(n)), Nat.is_le(Nat.pow(Nat.div(W, 2n), 2n+kp), v(n)), rl_v(K, hK, n, 2n+kp, m), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, 2n+kp), v(n)), v(m), Nat.div(W, 2n), hm))
1213  +R = M.iroot_k(v(n), 2n+kp)
1214  +hb = Equal.trans(Bool, Nat.is_le(Nat.pow(P2.pow2t(E2), 2n+kp), v(n)), M.root_le(v(n), 2n+kp, P2.pow2t(E2)), False{}, Equal.sym(Bool, M.root_le(v(n), 2n+kp, P2.pow2t(E2)), Nat.is_le(Nat.pow(P2.pow2t(E2), 2n+kp), v(n)), RT.root_le_ok(v(n), 2n+kp, P2.pow2t(E2))), RT.hi_bound(v(n), 1n+kp))
1215  +hb2 = L.subst(Nat, z => {Nat.is_le(Nat.pow(z, 2n+kp), v(n)) == False{} : Bool}, P2.pow2t(E2), W, PP.same(E2), hb)
1216  +hR1 = RT.iroot_le(v(n), 1n+kp)
1217  +hr = NF.root_above(R, W, 2n+kp, v(n), hb2, hR1)
1218  +hf = N.le_trans(1n+E2, 32n, 140n, N.lt_succ_le_succ(E2, 32n, hE2), {==})
1219  srch(140n, n, 2n+kp, zero, hi, m, I.u32_is(NM.Lt{I.u32_op(NM.One{}), hi}), G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp, m), E2, 0n, W, R, K, hK, zero_v(), ehi, hm, hR1, RT.lt_succ_iroot(v(n), 1n+kp), N.zero_le(R), hr, hmore, hhit, N.le_refl(W), hf)