def sc_x_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:124

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

124def sc_x_c(+n: Nat, +j: Nat, +c: Bool, +hc: {Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n) == c : Bool}) -> {Bool.or(Bool.not(Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))) == Bool.not(c) : Bool}:
125  match c:
126    case True{}:
127      +e0 = N.eq_from_is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n, hc)
128      +eN = Equal.trans(Nat, Nat.mul(C.shift(j, M.isqrt(n)), C.shift(j, M.isqrt(n))), C.shift(j, C.shift(j, Nat.mul(M.isqrt(n), M.isqrt(n)))), C.shift(j, C.shift(j, n)), sh_sq(j, M.isqrt(n)), Equal.cong(Nat, Nat, z => C.shift(j, C.shift(j, z)), Nat.mul(M.isqrt(n), M.isqrt(n)), n, e0))
129      +h1 = L.subst(Nat, z => {Nat.is_le(Nat.mul(C.shift(j, M.isqrt(n)), C.shift(j, M.isqrt(n))), z) == True{} : Bool}, Nat.mul(C.shift(j, M.isqrt(n)), C.shift(j, M.isqrt(n))), C.shift(j, C.shift(j, n)), eN, N.le_refl(Nat.mul(C.shift(j, M.isqrt(n)), C.shift(j, M.isqrt(n)))))
130      +h2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.mul(1n+C.shift(j, M.isqrt(n)), 1n+C.shift(j, M.isqrt(n)))) == True{} : Bool}, Nat.mul(C.shift(j, M.isqrt(n)), C.shift(j, M.isqrt(n))), C.shift(j, C.shift(j, n)), eN, sqlt(C.shift(j, M.isqrt(n))))
131      +et = isqrt_char(C.shift(j, C.shift(j, n)), C.shift(j, M.isqrt(n)), h1, h2)
132      +er = sub_z(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)), et)
133      +eT = Equal.trans(Nat, Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), Nat.mul(C.shift(j, M.isqrt(n)), C.shift(j, M.isqrt(n))), C.shift(j, C.shift(j, n)), Equal.trans(Nat, Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), Nat.mul(C.shift(j, M.isqrt(n)), M.isqrt(C.shift(j, C.shift(j, n)))), Nat.mul(C.shift(j, M.isqrt(n)), C.shift(j, M.isqrt(n))), Equal.cong(Nat, Nat, z => Nat.mul(z, M.isqrt(C.shift(j, C.shift(j, n)))), M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)), et), Equal.cong(Nat, Nat, z => Nat.mul(C.shift(j, M.isqrt(n)), z), M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)), et)), eN)
134      +b1 = Equal.cong(Nat, Bool, z => Bool.or(Bool.not(Nat.is_eq(z, 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))), Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n, er)
135      +b2 = Equal.cong(Nat, Bool, z => Bool.or(False{}, Bool.not(Nat.is_eq(z, C.shift(j, C.shift(j, n))))), Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n)), eT)
136      Equal.trans(Bool, Bool.or(Bool.not(Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))), Bool.or(False{}, Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))), False{}, b1, Equal.trans(Bool, Bool.or(False{}, Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))), Bool.or(False{}, Bool.not(Nat.is_eq(C.shift(j, C.shift(j, n)), C.shift(j, C.shift(j, n))))), False{}, b2, Equal.cong(Bool, Bool, t => Bool.or(False{}, Bool.not(t)), Nat.is_eq(C.shift(j, C.shift(j, n)), C.shift(j, C.shift(j, n))), True{}, N.is_eq_refl(C.shift(j, C.shift(j, n))))))
137    case False{}:
138      sc_x_f(n, j, hc, Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n), {==})