law byte_xor

lawful-words@0.1.0.0 · LAWS.bend:403

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

403law byte_xor:
404  for a: U32
405  for b: U32
406  for j: Nat
407  {D.byte(U32.xor(a, b), j) == U32.xor(D.byte(a, j), D.byte(b, j)) : U32}