~/jendhub

def AP.hc

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

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

238def AP.hc(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(False{}, y), AP.bv(True{}, x)) == True{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
239  %AP.fin_le_ft(Nat.cmp(y, x)) : {_ == True{} : Bool}
240  AP.le_bits(y, x, False{}, True{}, h)

Uses (7)

Used by (1)