def ba.key_cmp

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

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

1278def ba.key_cmp(+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}, +mid: U32, +m: Nat, +eM: {U32.to_nat(mid) == m : Nat}, +hmN: {Nat.is_lt(m, U32.to_nat(n)) == True{} : Bool}) -> {U32.is_lt(AR.Arrays.nth(U32, l, AR.Arrays.index(d, mid), 0), key) == Nat.is_lt(m, Q.bq.lb(l, n, key)) : Bool}:
1279  +hmS = Q.bq.lt_le_trans(m, U32.to_nat(n), AR.Arrays.slots(d), hmN, hN)
1280  +eI = Equal.trans(Nat, AR.Arrays.index(d, mid), U32.to_nat(mid), m, AL.index_of_u32(d, mid, Q.bq.lt_rw(m, AR.Arrays.slots(d), U32.to_nat(mid), AR.Arrays.slots(d), Equal.sym(Nat, U32.to_nat(mid), m, eM), {==}, hmS)), eM)
1281  +hml = Q.bq.lt_rw(m, AR.Arrays.slots(d), m, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hmS)
1282  +eg = Equal.trans(Maybe<&2, U32>, List.get(&2, U32, Q.bq.pre(l, n), m), List.get(&2, U32, l, m), Some{AR.Arrays.nth(U32, l, m, 0)}, Q.bq.get_take(l, U32.to_nat(n), m, hmN), Q.bq.get_nth(l, m, hml))
1283  %Equal.sym(Nat, AR.Arrays.index(d, mid), m, eI) : {U32.is_lt(AR.Arrays.nth(U32, l, _, 0), key) == Nat.is_lt(m, Q.bq.lb(l, n, key)) : Bool}
1284  ba.kc(Nat.is_lt(m, Q.bq.lb(l, n, key)), l, key, n, hs, m, eg, {==})