law lower_bound_above

bend-osdev-algo@0.1.0.0 · LAWS.bend:238

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S

238law lower_bound_above:
239  for xs: List<&2, U32>
240  for key: U32
241  for i: Nat
242  for x: U32
243  for s: {S.bsearch.sorted(xs) == True{} : Bool}
244  for e: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
245  for l: {Nat.is_le(S.bsearch.lower_bound(xs, key), i) == True{} : Bool}
246  {U32.is_lt(x, key) == False{} : Bool}