law xor_zero

lawful-words@0.1.0.0 · proof_word.bend:1087

import Base

1087law xor_zero:
1088  for +n: Nat
1089  for +a: Word(n)
1090  for +b: Word(n)
1091  for +h: {Word.to_nat(n, b) == 0n : Nat}
1092  {Word.to_nat(n, Word.xor(n, a, b)) == Word.to_nat(n, a) : Nat}