W64isq.up64p: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend as W64isq Lines 108-125 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend&start_line=108&end_line=125 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 def 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}: match fu ub: case 0n _: 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)) case 1n+g False{}: (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)) case 1n+ +g True{}: +q1 = U32.add(q, 1) +ha = W64S.and_l(U32.is_lt(q, m), Bool.not(X.sq_over(n, q1)), hub) +hb = W64S.and_r(U32.is_lt(q, m), Bool.not(X.sq_over(n, q1)), hub) +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) +e1 = succ_m(one, h1, q, m, pm, lt) +nov = not_t(X.sq_over(n, q1), hb) +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)) +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)) +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) +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) up64p(g, one, h1, n, q1, m, pm, up64_okg(n, q1, m), hf1, hle1, hs1, hX, {==}) Uses (34): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le_succ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_zero_absurd https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=not_lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&name=is_lt_nat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=mask https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend&name=not_t https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend&name=ovs https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend&name=sq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend&name=succ_m https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend&name=up64_okg https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend&name=up64g https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend&name=ustop https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64isq.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=and_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=and_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=sub_succ_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=sq_over