law wsub_val.m

lawful-words@0.1.0.0 · proof_u32.bend:99

import Base

99law wsub_val.m:
100  for +x: Word(32n)
101  for +y: Word(32n)
102  for +m: Nat
103  for +hm: {Nat.pow(2n, 32n) == m : Nat}
104  {Nat.sub(Nat.add(Word.to_nat(32n, x), m), Word.to_nat(32n, y))
105    == 1n+Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, Word.not(32n, y))) : Nat}