law wbit_and

lawful-words@0.1.0.0 · proof_word.bend:835

import Base

835law wbit_and:
836  for +n: Nat
837  for +a: Word(n)
838  for +b: Word(n)
839  for +k: Nat
840  {wbit(n, Word.and(n, a, b), k) == Bool.and(wbit(n, a, k), wbit(n, b, k)) : Bool}