law word_xor_and

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

import Base

549law word_xor_and:
550  for +n: Nat
551  for +a: Word(n)
552  for +b: Word(n)
553  {Nat.add(Word.to_nat(n, Word.xor(n, a, b)), Nat.double(Word.to_nat(n, Word.and(n, a, b)))) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}