law xor_split

lawful-words@0.1.0.0 · proof_word.bend:1203

import Base

1203# Xor likewise.
1204law xor_split:
1205  for +n: Nat
1206  for +a: Word(n)
1207  for +b: Word(n)
1208  for +k: Nat
1209  for +ha: {Nat.mod(Word.to_nat(n, a), Nat.pow(2n, k)) == 0n : Nat}
1210  for +hb: {Nat.is_lt(Word.to_nat(n, b), Nat.pow(2n, k)) == True{} : Bool}
1211  {Word.to_nat(n, Word.xor(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}