def ba.lb_le

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

import Base
import bend-osdev-array@0.1.0.0/array.bend as AR
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

1372# the lower bound is at most n
1373def ba.lb_le(-d: Nat, +l: List<&2, U32>, +n: U32, +key: U32, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}) -> {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(n)) == True{} : Bool}:
1374  Q.bq.le_rw(Q.bq.lb(l, n, key), List.length(&2, U32, Q.bq.pre(l, n)), Q.bq.lb(l, n, key), U32.to_nat(n), {==}, Q.bq.len_take(l, U32.to_nat(n), Q.bq.le_rw(U32.to_nat(n), AR.Arrays.slots(d), U32.to_nat(n), List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hn)), Laws.lower_bound_le_length(Q.bq.pre(l, n), key))