~/jendhub

def ud.hb

bend-osdev-u32@0.1.0.0 · PROOF.bend:1808

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as Laws

1808def ud.hb(+bw: Word(32n), h: {U32.is_zero(U32{bw}) == False{} : Bool}) -> {Nat.is_lt(0n, Word.to_nat(32n, bw)) == True{} : Bool}:
1809  ud.nz(Word.to_nat(32n, bw), Equal.trans(Bool, Nat.is_eq(Word.to_nat(32n, bw), 0n), U32.is_zero(U32{bw}), False{}, Equal.sym(Bool, U32.is_zero(U32{bw}), Nat.is_eq(Word.to_nat(32n, bw), 0n), Laws.u32_eq_value(U32{bw}, 0)), h))

Uses (11)

Used by (1)