U64int.srch: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend as U64int Lines 1151-1192 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&start_line=1151&end_line=1192 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/generic.bend as G import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I 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/natural/arith.bend as NR 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/math/typed/natfuel.bend as NF import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR2 import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as RT def srch(+f: Nat, +n: WU.U64, +k: Nat, +lo: WU.U64, +hi: WU.U64, +m: WU.U64, +more: Bool, +hit: Bool, +j: Nat, +nlo: Nat, +w: Nat, +R: Nat, +K: Nat, +hK: {K == 64n : Nat}, +hlo: {v(lo) == nlo : Nat}, +hhi: {v(hi) == Nat.add(nlo, w) : Nat}, +hm: {v(m) == Nat.add(nlo, Nat.div(w, 2n)) : Nat}, +hR1: {Nat.is_le(Nat.pow(R, k), v(n)) == True{} : Bool}, +hR2: {Nat.is_lt(v(n), Nat.pow(1n+R, k)) == True{} : Bool}, +hl: {Nat.is_le(nlo, R) == True{} : Bool}, +hr: {Nat.is_lt(R, Nat.add(nlo, w)) == True{} : Bool}, +hmore: {more == Nat.is_lt(1n, w) : Bool}, +hhit: {hit == Nat.is_le(Nat.pow(Nat.add(nlo, Nat.div(w, 2n)), k), v(n)) : Bool}, +hw: {Nat.is_le(w, C.pow2(j)) == True{} : Bool}, +hf: {Nat.is_le(1n+j, f) == True{} : Bool}) -> {v(G.search_go(~WU.U64, ~I.u64_op, ~I.u64_is, f, n, k, lo, hi, m, more, hit)) == R : Nat}: match f more hit j: case 0n _ _ _: Empty.absurd({v(G.search_go(~WU.U64, ~I.u64_op, ~I.u64_is, 0n, n, k, lo, hi, m, more, hit)) == R : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf))) case 1n+g False{} _ _: +hw1 = N.not_lt_le(1n, w, Equal.sym(Bool, False{}, Nat.is_lt(1n, w), hmore)) +h1 = L.subst(Nat, z => {Nat.is_le(Nat.add(nlo, w), z) == True{} : Bool}, Nat.add(nlo, 1n), 1n+nlo, plus1(nlo), N.le_add_left(w, 1n, nlo, hw1)) +hrl = N.lt_succ_le(R, nlo, N.lt_le_trans(R, Nat.add(nlo, w), 1n+nlo, hr, h1)) Equal.trans(Nat, v(lo), nlo, R, hlo, N.le_antisym(nlo, R, hl, hrl)) case 1n+g True{} _ 0n: Empty.absurd({v(G.search_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, n, k, lo, hi, m, True{}, hit)) == R : Nat}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(1n, w), False{}, hmore, N.le_not_lt(1n, w, hw)))) case 1n+ +g True{} True{} 1n+ +jp: +q = Nat.div(w, 2n) +X = Nat.add(nlo, q) +w2 = Nat.sub(w, q) +hqw = Equal.trans(Nat, Nat.add(q, w2), w, w, N.sub_add(w, q, AR2.div_le(w, 2n)), {==}) +ehi = Equal.trans(Nat, Nat.add(X, w2), Nat.add(nlo, Nat.add(q, w2)), Nat.add(nlo, w), N.add_assoc(nlo, q, w2), Equal.cong(Nat, Nat, t => Nat.add(nlo, t), Nat.add(q, w2), w, hqw)) +hhi2 = Equal.trans(Nat, v(hi), Nat.add(nlo, w), Nat.add(X, w2), hhi, Equal.sym(Nat, Nat.add(X, w2), Nat.add(nlo, w), ehi)) +hw0 = N.lt_trans(0n, 1n, w, {==}, Equal.sym(Bool, True{}, Nat.is_lt(1n, w), hmore)) +hdw = L.subst(Nat, z => {Nat.is_lt(w, z) == True{} : Bool}, Nat.add(w, w), Nat.double(w), Equal.sym(Nat, Nat.double(w), Nat.add(w, w), NA.double_self(w)), lt_add_r(w, w, hw0)) +hpos = RT.sub_pos(q, w, NF.half_below(w, w, hdw)) +m2 = G.imid(~WU.U64, ~I.u64_op, m, hi) +hm2 = imid_v(K, hK, m, hi, X, w2, hm, hhi2) +hmore2 = more_v(K, hK, m, hi, X, w2, hm, hhi2, hpos) +hhit2 = Equal.trans(Bool, G.root_le(~WU.U64, ~I.u64_op, ~I.u64_is, n, k, m2), Nat.is_le(Nat.pow(v(m2), k), v(n)), Nat.is_le(Nat.pow(Nat.add(X, Nat.div(w2, 2n)), k), v(n)), rl_v(K, hK, n, k, m2), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, k), v(n)), v(m2), Nat.add(X, Nat.div(w2, 2n)), hm2)) +hl2 = NF.root_below(R, X, k, v(n), Equal.sym(Bool, True{}, Nat.is_le(Nat.pow(X, k), v(n)), hhit), hR2) +hr2 = L.subst(Nat, z => {Nat.is_lt(R, z) == True{} : Bool}, Nat.add(nlo, w), Nat.add(X, w2), Equal.sym(Nat, Nat.add(X, w2), Nat.add(nlo, w), ehi), hr) +hw3 = NF.w_hi(w, C.pow2(jp), hw) srch(g, n, k, m, hi, m2, I.u64_is(NM.Lt{G.inc(~WU.U64, ~I.u64_op, m), hi}), G.root_le(~WU.U64, ~I.u64_op, ~I.u64_is, n, k, m2), jp, X, w2, R, K, hK, hm, hhi2, hm2, hR1, hR2, hl2, hr2, Equal.sym(Bool, Nat.is_lt(1n, w2), I.u64_is(NM.Lt{G.inc(~WU.U64, ~I.u64_op, m), hi}), Equal.sym(Bool, I.u64_is(NM.Lt{G.inc(~WU.U64, ~I.u64_op, m), hi}), Nat.is_lt(1n, w2), hmore2)), hhit2, hw3, hf) case 1n+ +g True{} False{} 1n+ +jp: +q = Nat.div(w, 2n) +X = Nat.add(nlo, q) +h2w = N.lt_succ_le_succ(1n, w, Equal.sym(Bool, True{}, Nat.is_lt(1n, w), hmore)) +hq1 = Equal.trans(Bool, Nat.is_le(1n, q), Nat.is_le(Nat.mul(1n, 2n), w), True{}, NR.le_div(1n, 1n, w), h2w) +hpos = pos_of(q, hq1) +m2 = G.imid(~WU.U64, ~I.u64_op, lo, m) +hm2 = imid_v(K, hK, lo, m, nlo, q, hlo, hm) +hmore2 = more_v(K, hK, lo, m, nlo, q, hlo, hm, hpos) +hhit2 = Equal.trans(Bool, G.root_le(~WU.U64, ~I.u64_op, ~I.u64_is, n, k, m2), Nat.is_le(Nat.pow(v(m2), k), v(n)), Nat.is_le(Nat.pow(Nat.add(nlo, Nat.div(q, 2n)), k), v(n)), rl_v(K, hK, n, k, m2), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, k), v(n)), v(m2), Nat.add(nlo, Nat.div(q, 2n)), hm2)) +hr2 = NF.root_above(R, X, k, v(n), Equal.sym(Bool, False{}, Nat.is_le(Nat.pow(X, k), v(n)), hhit), hR1) +hw3 = NF.w_lo(w, C.pow2(jp), hw) srch(g, n, k, lo, m, m2, I.u64_is(NM.Lt{G.inc(~WU.U64, ~I.u64_op, lo), m}), G.root_le(~WU.U64, ~I.u64_op, ~I.u64_is, n, k, m2), jp, nlo, q, R, K, hK, hlo, hm, hm2, hR1, hR2, hl, hr2, Equal.sym(Bool, Nat.is_lt(1n, q), I.u64_is(NM.Lt{G.inc(~WU.U64, ~I.u64_op, lo), m}), Equal.sym(Bool, I.u64_is(NM.Lt{G.inc(~WU.U64, ~I.u64_op, lo), m}), Nat.is_lt(1n, q), hmore2)), hhit2, hw3, hf) Uses (51): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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.cong 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.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double 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.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=div_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_self 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=add_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_antisym https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_not_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le 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_trans 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/nat.bend&name=sub_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=le_div https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend&name=sub_pos https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=half_below https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=root_above https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=root_below https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=w_hi https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=w_lo https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=imid_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=lt_add_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=more_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=plus1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=pos_of https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=rl_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=true_ne_false https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=pow2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=imid https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=inc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=root_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=search_go https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/instances.bend&name=u64_is https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/instances.bend&name=u64_op https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Test https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64