law byte_and

lawful-words@0.1.0.0 · proof_bytes.bend:587

import Base
import lawful-words@0.1.0.0/defs.bend as D

587law byte_and:
588  for +a: U32
589  for +b: U32
590  for +j: Nat
591  {D.byte(U32.and(a, b), j) == U32.and(D.byte(a, j), D.byte(b, j)) : U32}