law wput

lawful-words@0.1.0.0 · proof_word.bend:546

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

546law wput:
547  for +n: Nat
548  for +c: Bool
549  for +w: Word(n)
550  {Nat.add(Word.to_nat(n, Word.shl.put(n, c, w)), Nat.mul(N.bn(stop(n, c, w)), Nat.pow(2n, n)))
551    == Nat.add(N.bn(c), Nat.double(Word.to_nat(n, w))) : Nat}