def ba.run

bend-osdev-algo@0.1.0.0 · PROOF.bend:1354

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

1354# f halvings from lo <= LB <= hi <= n with hi - lo < 2^f end at LB
1355def ba.run(f: 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, +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(f)) == True{} : Bool}) -> {U32.to_nat(Q.bq.run(f, d, l, lo, hi, key)) == Q.bq.lb(l, n, key) : Nat}:
1356  match f:
1357    case 0n:
1358      +l0 = U32.to_nat(lo)
1359      +h0 = U32.to_nat(hi)
1360      +lb = Q.bq.lb(l, n, key)
1361      Q.bq.le_antisym(l0, lb, i1, Q.bq.le_trans(lb, h0, l0, i2, Q.bq.sub0_le(h0, l0, Q.bq.lt_one(Q.bq.s(lo, hi), hz))))
1362    case 1n+ +g:
1363      ba.adv(U32.is_lt(lo, hi), g, d, l, hl, key, n, hN, hs, lo, hi, {==}, i1, i2, i3, hz, lo2 => hi2 => j1 => j2 => j3 => jz => ba.run(g, d, l, hl, key, n, hN, hs, lo2, hi2, j1, j2, j3, jz))