def up64p

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64isq.bend:108

import Base
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/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
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/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S

108def up64p(+fu: Nat, +one: Nat, +h1: {one == 1n : Nat}, +n: WU.U64, +q: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 32n)} : U32}, +ub: Bool, +hf: {Nat.is_lt(Nat.sub(v(m), v(q)), fu) == True{} : Bool}, +hle: {Nat.is_le(v(q), v(m)) == True{} : Bool}, +hs: {Nat.is_le(sq(v(q)), SW.value(n)) == True{} : Bool}, +hX: {Nat.is_lt(SW.value(n), sq(1n+v(m))) == True{} : Bool}, +hub: {up64_okg(n, q, m) == ub : Bool}) -> {Nat.is_le(sq(v(up64g(fu, n, q, ub, m))), SW.value(n)) == True{} : Bool} & {Nat.is_lt(SW.value(n), sq(1n+v(up64g(fu, n, q, ub, m)))) == True{} : Bool}:
109  match fu ub:
110    case 0n _:
111      Empty.absurd({Nat.is_le(sq(v(up64g(0n, n, q, ub, m))), SW.value(n)) == True{} : Bool} & {Nat.is_lt(SW.value(n), sq(1n+v(up64g(0n, n, q, ub, m)))) == True{} : Bool}, N.lt_zero_absurd(Nat.sub(v(m), v(q)), hf))
112    case 1n+g False{}:
113      (hs, ustop(one, h1, n, q, m, pm, hle, hX, U32.is_lt(q, m), {==}, Bool.not(X.sq_over(n, U32.add(q, 1))), {==}, hub))
114    case 1n+ +g True{}:
115      +q1 = U32.add(q, 1)
116      +ha = W64S.and_l(U32.is_lt(q, m), Bool.not(X.sq_over(n, q1)), hub)
117      +hb = W64S.and_r(U32.is_lt(q, m), Bool.not(X.sq_over(n, q1)), hub)
118      +lt = Equal.trans(Bool, Nat.is_lt(v(q), v(m)), U32.is_lt(q, m), True{}, Equal.sym(Bool, U32.is_lt(q, m), Nat.is_lt(v(q), v(m)), U.is_lt_nat(q, m)), ha)
119      +e1 = succ_m(one, h1, q, m, pm, lt)
120      +nov = not_t(X.sq_over(n, q1), hb)
121      +hs1 = N.not_lt_le(SW.value(n), sq(v(q1)), Equal.trans(Bool, Nat.is_lt(SW.value(n), sq(v(q1))), X.sq_over(n, q1), False{}, Equal.sym(Bool, X.sq_over(n, q1), Nat.is_lt(SW.value(n), sq(v(q1))), ovs(n, q1)), nov))
122      +hle1 = L.subst(Nat, z => {Nat.is_le(z, v(m)) == True{} : Bool}, 1n+v(q), v(q1), Equal.sym(Nat, v(q1), 1n+v(q), e1), N.lt_succ_le_succ(v(q), v(m), lt))
123      +hf0 = L.subst(Nat, z => {Nat.is_lt(z, 1n+g) == True{} : Bool}, Nat.sub(v(m), v(q)), 1n+Nat.sub(v(m), 1n+v(q)), W64S.sub_succ_r(v(q), v(m), lt), hf)
124      +hf1 = L.subst(Nat, z => {Nat.is_lt(Nat.sub(v(m), z), g) == True{} : Bool}, 1n+v(q), v(q1), Equal.sym(Nat, v(q1), 1n+v(q), e1), hf0)
125      up64p(g, one, h1, n, q1, m, pm, up64_okg(n, q1, m), hf1, hle1, hs1, hX, {==})