PROOF.ba.adv: def of bend-osdev-algo@0.1.0.0 Import: import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF Lines 1326-1352 of bend-osdev-algo@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&start_line=1326&end_line=1352 import Base import bend-osdev-algo@0.1.0.0/bsearch.bend as S import bend-osdev-array@0.1.0.0/array.bend as AR import bend-osdev-algo@0.1.0.0/proof_u32.bend as U import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as Q # one halving of [lo, hi): active when lo < hi (c) def ba.adv(c: Bool, +g: Nat, +d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +key: U32, +n: U32, +hN: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +hs: {S.bsearch.sorted(Q.bq.pre(l, n)) == True{} : Bool}, +lo: U32, +hi: U32, +ec: {U32.is_lt(lo, hi) == c : Bool}, +i1: {Nat.is_le(U32.to_nat(lo), Q.bq.lb(l, n, key)) == True{} : Bool}, +i2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi)) == True{} : Bool}, +i3: {Nat.is_le(U32.to_nat(hi), U32.to_nat(n)) == True{} : Bool}, +hz: {Nat.is_lt(Q.bq.s(lo, hi), U.uq.pw(1n+g)) == True{} : Bool}, ih: @lo2: U32 -> @hi2: U32 -> @j1: {Nat.is_le(U32.to_nat(lo2), Q.bq.lb(l, n, key)) == True{} : Bool} -> @j2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi2)) == True{} : Bool} -> @j3: {Nat.is_le(U32.to_nat(hi2), U32.to_nat(n)) == True{} : Bool} -> @jz: {Nat.is_lt(Q.bq.s(lo2, hi2), U.uq.pw(g)) == True{} : Bool} -> {U32.to_nat(Q.bq.run(g, d, l, lo2, hi2, key)) == Q.bq.lb(l, n, key) : Nat}) -> {U32.to_nat(Q.bq.run(g, d, l, Q.bq.nlo.a(c, U32.is_lt(Q.bq.x(d, l, lo, hi), key), lo, Q.bq.mid(lo, hi)), Q.bq.nhi.a(c, U32.is_lt(Q.bq.x(d, l, lo, hi), key), hi, Q.bq.mid(lo, hi)), key)) == Q.bq.lb(l, n, key) : Nat}: match c: case False{}: +h0 = U32.to_nat(hi) +l0 = U32.to_nat(lo) +e0 = Q.bq.sub_le0(h0, l0, Q.bq.not_lt(l0, h0, u32.mv_lt(lo, hi, False{}, ec))) ih(lo, hi, i1, i2, i3, Q.bq.lt_rw(0n, U.uq.pw(g), Q.bq.s(lo, hi), U.uq.pw(g), Equal.sym(Nat, Q.bq.s(lo, hi), 0n, e0), {==}, Q.bq.pw_pos(g))) case True{}: +h0 = U32.to_nat(hi) +l0 = U32.to_nat(lo) +s = Q.bq.s(lo, hi) +m = Q.bq.m(lo, hi) +mid = Q.bq.mid(lo, hi) +lb = Q.bq.lb(l, n, key) +sh = U32.to_nat(U32.shr(U32.sub(hi, lo))) +hlt = u32.mv_lt(lo, hi, True{}, ec) +hle = Q.bq.lt_le(l0, h0, hlt) +eD = U.uq.u32_sub(hi, lo, hle) +eE = Equal.trans(Nat, sh, U.uq.half(U32.to_nat(U32.sub(hi, lo))), U.uq.half(s), U.uq.u32_shr(U32.sub(hi, lo)), Equal.cong(Nat, Nat, z => U.uq.half(z), U32.to_nat(U32.sub(hi, lo)), s, eD)) +ehs = Q.bq.add_sub(l0, h0, hle) +hmh = Q.bq.lt_rw(Nat.add(l0, U.uq.half(s)), Nat.add(l0, s), m, h0, {==}, ehs, Equal.trans(Bool, Nat.is_lt(Nat.add(l0, U.uq.half(s)), Nat.add(l0, s)), Nat.is_lt(U.uq.half(s), s), True{}, Q.bq.lt_cancel(l0, U.uq.half(s), s), Q.bq.half_lt(s, Q.bq.sub_pos(l0, h0, hlt)))) +hadd = Q.bq.le_rw(m, h0, Nat.add(l0, sh), h0, Equal.cong(Nat, Nat, z => Nat.add(l0, z), U.uq.half(s), sh, Equal.sym(Nat, sh, U.uq.half(s), eE)), {==}, Q.bq.lt_le(m, h0, hmh)) +eM = Equal.trans(Nat, U32.to_nat(mid), Nat.add(l0, sh), m, U.uq.u32_add(lo, U32.shr(U32.sub(hi, lo)), hi, hadd), Equal.cong(Nat, Nat, z => Nat.add(l0, z), sh, U.uq.half(s), eE)) +hmN = Q.bq.lt_le_trans(m, h0, U32.to_nat(n), hmh, i3) %Equal.sym(Bool, U32.is_lt(Q.bq.x(d, l, lo, hi), key), Nat.is_lt(m, lb), ba.key_cmp(d, l, hl, key, n, hN, hs, mid, m, eM, hmN)) : {U32.to_nat(Q.bq.run(g, d, l, Q.bq.lo_b(_, lo, mid), Q.bq.hi_b(_, hi, mid), key)) == lb : Nat} ba.adv2(Nat.is_lt(m, lb), g, d, l, key, n, lo, hi, {==}, i1, i2, i3, hz, eM, ehs, hmh, ih) Uses (47): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length 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.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=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=ba.adv2 https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=ba.key_cmp https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=u32.mv_lt https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bsearch.bend&name=bsearch.sorted https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.add_sub https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.half_lt https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.hi_b https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.lb https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.le_rw https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.lo_b https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.lt_cancel https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.lt_le https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.lt_le_trans https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.lt_rw https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.m https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.mid https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.nhi.a https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.nlo.a https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.not_lt https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.pre https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.pw_pos https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.run https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.s https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.sub_le0 https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.sub_pos https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.x https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.half https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.pw https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.u32_add https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.u32_shr https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.u32_sub https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.slots