law wnot.m

lawful-words@0.1.0.0 · proof_u32.bend:53

import Base

53law wnot.m:
54  for +w: Word(32n)
55  for +m: Nat
56  for +hm: {Nat.pow(2n, 32n) == m : Nat}
57  {1n+Nat.add(Word.to_nat(32n, Word.not(32n, w)), Word.to_nat(32n, w)) == m : Nat}