Word.or_zero: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend as Word
Lines 130-136 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend&start_line=130&end_line=136

import Base

# zero(x | y) == zero(x) && zero(y)
law or_zero:
  for +n: Nat
  for +x: Word(n)
  for +y: Word(n)
  {Cmp.is_eq(Word.cmp(n, Word.or(n, x, y), Word.zero(n))) ==
    Bool.and(Cmp.is_eq(Word.cmp(n, x, Word.zero(n))), Cmp.is_eq(Word.cmp(n, y, Word.zero(n)))) : Bool}

Uses (15):
  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.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  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
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  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.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend&name=bits_or
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend&name=fin_eq