def AP.lt_bv
bend-osdev-array@0.1.0.1 · PROOF.bend:903
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
903def AP.lt_bv(+b: Bool, +x: Nat, +s: Nat, h: {Nat.is_lt(x, s) == True{} : Bool}) -> {Nat.is_lt(AP.bv(b, x), AP.bv(False{}, s)) == True{} : Bool}:
904 %Equal.sym(Cmp, Nat.cmp(AP.bv(b, x), AP.bv(False{}, s)), Word.cmp.fin(b, False{}, Nat.cmp(x, s)), AP.nc(x, s, b, False{})) : {Cmp.is_lt(_) == True{} : Bool}
905 %Equal.sym(Bool, Cmp.is_lt(Word.cmp.fin(b, False{}, Nat.cmp(x, s))), Cmp.is_lt(Nat.cmp(x, s)), AP.fin_lt_xf(b, Nat.cmp(x, s))) : {_ == True{} : Bool}
906 h