law bit_xor

lawful-words@0.1.0.0 · proof_u32.bend:1293

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

1293law bit_xor:
1294  for +a: U32
1295  for +b: U32
1296  for +k: Nat
1297  {D.bit(U32.xor(a, b), k) == Bool.xor(D.bit(a, k), D.bit(b, k)) : Bool}