~/jendhub

def uq.hb

bend-osdev-algo@0.1.0.0 · proof_u32.bend:294

import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
import Base

294def uq.hb(+y: Nat, +x: Nat, h: {Nat.is_le(uq.bv(True{}, y), uq.bv(False{}, x)) == True{} : Bool}) -> {Nat.is_le(1n+y, x) == True{} : Bool}:
295  %Equal.sym(Bool, Nat.is_le(1n+y, x), Nat.is_lt(y, x), uq.le_succ(y, x)) : {_ == True{} : Bool}
296  %uq.fin_le_tf(Nat.cmp(y, x)) : {_ == True{} : Bool}
297  uq.le_bits(y, x, True{}, False{}, h)

Uses (10)

Used by (1)