law byte_and

lawful-words@0.1.0.0 · LAWS.bend:390

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

390# Bitwise operations work byte by byte.
391law byte_and:
392  for a: U32
393  for b: U32
394  for j: Nat
395  {D.byte(U32.and(a, b), j) == U32.and(D.byte(a, j), D.byte(b, j)) : U32}