law or_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/subtle/word.bend:130

import Base

130# zero(x | y) == zero(x) && zero(y)
131law or_zero:
132  for +n: Nat
133  for +x: Word(n)
134  for +y: Word(n)
135  {Cmp.is_eq(Word.cmp(n, Word.or(n, x, y), Word.zero(n))) ==
136    Bool.and(Cmp.is_eq(Word.cmp(n, x, Word.zero(n))), Cmp.is_eq(Word.cmp(n, y, Word.zero(n)))) : Bool}