law moddbl_w

lawful-words@0.1.0.0 · proof_word.bend:964

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

964law moddbl_w:
965  for +p: Nat
966  for +x: Bool
967  for +t: Word(p)
968  for +j: Nat
969  {Nat.mod(Word.to_nat(1n+p, WCon{x, t}), Nat.pow(2n, 1n+j)) == Nat.add(N.bn(x), Nat.double(Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)))) : Nat}