law allz_orm

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:17

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

17law allz_orm:
18  for +n: Nat
19  for +x: Word(n)
20  for +y: Word(n)
21  for +z: Word(n)
22  {Z.allz(n, Word.and(n, Word.or(n, x, y), z)) == Bool.and(Z.allz(n, Word.and(n, x, z)), Z.allz(n, Word.and(n, y, z))) : Bool}