def AP.lt_bv_inv

bend-osdev-array@0.1.0.1 · PROOF.bend:899

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

899def AP.lt_bv_inv(+b: Bool, +x: Nat, +s: Nat, h: {Nat.is_lt(AP.bv(b, x), AP.bv(False{}, s)) == True{} : Bool}) -> {Nat.is_lt(x, s) == True{} : Bool}:
900  %AP.fin_lt_xf(b, Nat.cmp(x, s)) : {_ == True{} : Bool}
901  AP.lt_bits(x, s, b, False{}, h)

Uses (7)

Used by (3)