~/jendhub

def inc_zero32

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64.bend:232

import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as U64
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

232def inc_zero32(+x: Word(32n)) -> {U32.is_zero(U32{Word.inc(32n, x)}) == WD.ones(32n, x) : Bool}:
233  WD.inc_zero(32n, x)

Uses (7)

Used by (1)