law allz_or

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:47

import Base
import lawful-words@0.1.0.0/proof_zb.bend as Z

47law allz_or:
48  for +n: Nat
49  for +x: Word(n)
50  for +y: Word(n)
51  {Z.allz(n, Word.or(n, x, y)) == Bool.and(Z.allz(n, x), Z.allz(n, y)) : Bool}