law to_nat_xor_split

lawful-words@0.1.0.0 · LAWS.bend:276

import Base

276law to_nat_xor_split:
277  for a: U32
278  for b: U32
279  for k: Nat
280  for ha: {Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) == 0n : Nat}
281  for hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, k)) == True{} : Bool}
282  {U32.to_nat(U32.xor(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}