PROOF.ba.fd: def of bend-osdev-algo@0.1.0.0 Import: import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF Lines 1395-1419 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=1395&end_line=1419 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-array@0.1.0.0/LAWS.bend as AL import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as Q import bend-osdev-algo@0.1.0.0/LAWS.bend as Laws def ba.fd(c: Bool, +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}, +r: U32, +ec: {U32.is_lt(r, n) == c : Bool}, +er: {U32.to_nat(r) == Q.bq.lb(l, n, key) : Nat}) -> {Laws.algo_index_nat(Pair.snd(Array, Maybe<&2, U32>, S.bsearch.array.found(c, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, AR.Arrays.index(d, r), 0)), r, key))) == S.bsearch.find(Q.bq.pre(l, n), key) : Maybe<&2, Nat>}: match c: case True{}: +lb = Q.bq.lb(l, n, key) +nn = U32.to_nat(n) +pre = Q.bq.pre(l, n) +hnl = Q.bq.le_rw(nn, AR.Arrays.slots(d), nn, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hn) +hc = Equal.trans(Bool, Nat.is_lt(lb, nn), Nat.is_lt(U32.to_nat(r), nn), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, nn), lb, U32.to_nat(r), Equal.sym(Nat, U32.to_nat(r), lb, er)), u32.mv_lt(r, n, True{}, ec)) +hls = Q.bq.lt_le_trans(lb, nn, AR.Arrays.slots(d), hc, hn) +ei = Equal.trans(Nat, AR.Arrays.index(d, r), U32.to_nat(r), lb, AL.index_of_u32(d, r, Q.bq.lt_rw(lb, AR.Arrays.slots(d), U32.to_nat(r), AR.Arrays.slots(d), Equal.sym(Nat, U32.to_nat(r), lb, er), {==}, hls)), er) +hll = Q.bq.lt_rw(lb, AR.Arrays.slots(d), lb, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hls) +eg = Equal.trans(Maybe<&2, U32>, List.get(&2, U32, pre, lb), List.get(&2, U32, l, lb), Some{AR.Arrays.nth(U32, l, lb, 0)}, Q.bq.get_take(l, nn, lb, hc), Q.bq.get_nth(l, lb, hll)) %Equal.sym(Nat, AR.Arrays.index(d, r), lb, ei) : {Laws.algo_index_nat(Pair.snd(Array, Maybe<&2, U32>, S.bsearch.array.found(True{}, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, _, 0)), r, key))) == S.bsearch.find(pre, key) : Maybe<&2, Nat>} %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, pre, lb), Some{AR.Arrays.nth(U32, l, lb, 0)}, eg) : {Laws.algo_index_nat(Pair.snd(Array, Maybe<&2, U32>, S.bsearch.array.found(True{}, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, lb, 0)), r, key))) == S.bsearch.find.check(lb, _, key) : Maybe<&2, Nat>} ba.hit(U32.is_eq(AR.Arrays.nth(U32, l, lb, 0), key), r, lb, er) case False{}: +lb = Q.bq.lb(l, n, key) +nn = U32.to_nat(n) +pre = Q.bq.pre(l, n) +hnl = Q.bq.le_rw(nn, AR.Arrays.slots(d), nn, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hn) +hc = Equal.trans(Bool, Nat.is_lt(lb, nn), Nat.is_lt(U32.to_nat(r), nn), False{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, nn), lb, U32.to_nat(r), Equal.sym(Nat, U32.to_nat(r), lb, er)), u32.mv_lt(r, n, False{}, ec)) +eln = Q.bq.le_antisym(lb, nn, ba.lb_le(d, l, n, key, hl, hn), Q.bq.not_lt(lb, nn, hc)) +eg = Equal.trans(Maybe<&2, U32>, List.get(&2, U32, pre, lb), List.get(&2, U32, pre, List.length(&2, U32, pre)), None{}, Equal.cong(Nat, Maybe<&2, U32>, z => List.get(&2, U32, pre, z), lb, List.length(&2, U32, pre), Equal.trans(Nat, lb, nn, List.length(&2, U32, pre), eln, Equal.sym(Nat, List.length(&2, U32, pre), nn, Q.bq.len_take(l, nn, hnl)))), Q.bq.get_len(pre)) %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, pre, lb), None{}, eg) : {Laws.algo_index_nat(Pair.snd(Array, Maybe<&2, U32>, S.bsearch.array.found(False{}, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, AR.Arrays.index(d, r), 0)), r, key))) == S.bsearch.find.check(lb, _, key) : Maybe<&2, Nat>} {==} Uses (41): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array 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.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe 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=Pair.snd 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.is_eq 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.to_nat https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=algo_index_nat https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=ba.hit https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=ba.lb_le 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.array.found https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bsearch.bend&name=bsearch.find https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bsearch.bend&name=bsearch.find.check https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.get_len https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.get_nth https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.get_take 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_antisym 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.len_take 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.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-array@0.1.0.1/LAWS.bend&name=index_of_u32 https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.index https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.nth https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.of_list https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.slots