law wput.m

lawful-words@0.1.0.0 · proof_u32.bend:73

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N
import lawful-words@0.1.0.0/proof_word.bend as W

73law wput.m:
74  for +c: Bool
75  for +w: Word(32n)
76  for +m: Nat
77  for +hm: {Nat.pow(2n, 32n) == m : Nat}
78  {Nat.add(Word.to_nat(32n, Word.shl.put(32n, c, w)), Nat.mul(N.bn(W.stop(32n, c, w)), m))
79    == Nat.add(N.bn(c), Nat.double(Word.to_nat(32n, w))) : Nat}