def s_high

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

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/src/math/natural.bend as M
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/f64sqa.bend as AQ

44def s_high(+n: Nat, +j: Nat) -> {C.high(1n+j, 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))))))) == M.isqrt(n) : Nat}:
45  +e1 = Equal.cong(Nat, Nat, z => C.high(1n+j, z), 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))
46  +e2 = Equal.cong(Nat, Nat, z => C.high(j, z), C.half(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)))))), M.isqrt(C.shift(j, C.shift(j, n))), Equal.trans(Nat, C.half(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(C.half(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)))))), M.isqrt(C.shift(j, C.shift(j, n)))), M.isqrt(C.shift(j, C.shift(j, n))), WW.half_dbl(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))))), M.isqrt(C.shift(j, C.shift(j, n)))), Equal.cong(Nat, Nat, z => Nat.add(z, M.isqrt(C.shift(j, C.shift(j, n)))), C.half(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)))))), 0n, hb2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))))
47  Equal.trans(Nat, C.high(1n+j, 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))))))), C.high(j, C.half(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))))))), M.isqrt(n), Equal.trans(Nat, C.high(1n+j, 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))))))), C.high(1n+j, 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)))))), C.high(j, C.half(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))))))), e1, {==}), Equal.trans(Nat, C.high(j, C.half(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))))))), C.high(j, M.isqrt(C.shift(j, C.shift(j, n)))), M.isqrt(n), e2, AQ.sc_high(n, j)))