def s_bl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqs.bend:68

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
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/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/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as AQ

68def s_bl(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +j: Nat, +h62: {Nat.is_le(C.shift(62n, one), M.isqrt(n)) == True{} : Bool}) -> {Nat.is_le(Nat.add(1n+j, 55n), M.bit_length(Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))) == True{} : Bool}:
69  +l1 = N.le_trans(C.shift(1n+j, M.isqrt(n)), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), N.double_le(C.shift(j, M.isqrt(n)), M.isqrt(C.shift(j, C.shift(j, n))), AQ.sc_lo(n, j)), L.subst(Nat, z => {Nat.is_le(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), z) == True{} : Bool}, Nat.add(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), NA.add_comm(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), N.le_add_right(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))))
70  +l2 = L.subst(Nat, z => {Nat.is_le(C.shift(1n+j, M.isqrt(n)), z) == True{} : Bool}, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Equal.sym(Nat, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), mform(n, j)), l1)
71  +f62 = Equal.trans(Bool, C.fits(62n, M.isqrt(n)), Nat.is_lt(M.isqrt(n), C.shift(62n, one)), False{}, Equal.sym(Bool, Nat.is_lt(M.isqrt(n), C.shift(62n, one)), C.fits(62n, M.isqrt(n)), FR.lt_fit(62n, one, h1, M.isqrt(n))), N.le_not_lt(M.isqrt(n), C.shift(62n, one), h62))
72  +f54 = FL.nfit_mono(54n, 62n, M.isqrt(n), {==}, f62)
73  +fS = Equal.trans(Bool, C.fits(Nat.add(1n+j, 54n), C.shift(1n+j, M.isqrt(n))), C.fits(54n, M.isqrt(n)), False{}, RT.fits_sh(1n+j, 54n, M.isqrt(n)), f54)
74  +fM = FR.nfit(Nat.add(1n+j, 54n), C.shift(1n+j, M.isqrt(n)), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), l2, fS)
75  +b1 = FL.nfit_bl(Nat.add(1n+j, 54n), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), fM)
76  L.subst(Nat, z => {Nat.is_le(1n+z, M.bit_length(Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))) == True{} : Bool}, 1n+Nat.add(j, 54n), Nat.add(j, 55n), Equal.sym(Nat, Nat.add(j, 55n), 1n+Nat.add(j, 54n), N.add_succ(j, 54n)), b1)