ProofZb.zb_zero: law of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_zb.bend as ProofZb
Lines 1132-1134 of lawful-words@0.1.0.0/proof_zb.bend: https://jend.leeeet.dev/read.txt?path=lawful-words@0.1.0.0/proof_zb.bend&start_line=1132&end_line=1134

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

law zb_zero:
  for +v: U32
  {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}

Uses (27):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_ne
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=zb
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=and_true_r_id
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=allz
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=allz_cmp
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=app8
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=h8
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=one8
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=zb_byte
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=zb_ne0
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=zb_ne1
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=zb_ne2
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=zb_ne3
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=zf