law zb_zero

lawful-words@0.1.0.0 · proof_zb.bend:1132

import Base
import lawful-words@0.1.0.0/defs.bend as D

1132law zb_zero:
1133  for +v: U32
1134  {U32.is_zero(D.zb(v)) == (U32.is_ne(D.byte(v, 0n), 0) && (U32.is_ne(D.byte(v, 1n), 0) && (U32.is_ne(D.byte(v, 2n), 0) && U32.is_ne(D.byte(v, 3n), 0)))) : Bool}