law wshl.m

lawful-words@0.1.0.0 · proof_u32.bend:63

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

63law wshl.m:
64  for +w: Word(32n)
65  for +m: Nat
66  for +hm: {Nat.pow(2n, 32n) == m : Nat}
67  {Nat.add(Word.to_nat(32n, Word.shl(32n, w)), Nat.mul(N.bn(W.shtop(32n, w)), m)) == Nat.double(Word.to_nat(32n, w)) : Nat}