law u32_xor_and

bend-osdev-u32@0.1.0.0 · LAWS.bend:604

import Base

604law u32_xor_and:
605  for +a: U32
606  for +b: U32
607  {Nat.add(U32.to_nat(U32.xor(a, b)), Nat.double(U32.to_nat(U32.and(a, b)))) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}