law wshl

lawful-words@0.1.0.0 · proof_word.bend:594

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

594law wshl:
595  for +n: Nat
596  for +w: Word(n)
597  {Nat.add(Word.to_nat(n, Word.shl(n, w)), Nat.mul(N.bn(shtop(n, w)), Nat.pow(2n, n))) == Nat.double(Word.to_nat(n, w)) : Nat}