~/jendhub

def un.u32_low_self

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

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

2240def un.u32_low_self(+a: U32) -> {U32.to_nat(a) == U.U32Nat.low(32n, U32.to_nat(a)) : Nat}:
2241  match a:
2242    case U32{+w}:
2243      Equal.sym(Nat, U.U32Nat.low(32n, Word.to_nat(32n, w)), Word.to_nat(32n, w), Laws.low_small(32n, Word.to_nat(32n, w), Laws.word_value_lt(32n, w)))

Uses (8)

Used by (1)