law to_nat_not

lawful-words@0.1.0.0 · LAWS.bend:262

import Base

262law to_nat_not:
263  for a: U32
264  {U32.to_nat(U32.not(a)) == Nat.sub(Nat.sub(Nat.pow(2n, 32n), 1n), U32.to_nat(a)) : Nat}