law mask_step

lawful-words@0.1.0.0 · proof_word.bend:992

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

992law mask_step:
993  for +p: Nat
994  for +x: Bool
995  for +t: Word(p)
996  for +j: Nat
997  for +r: Nat
998  for +ih: {r == Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)) : Nat}
999  {Nat.add(N.bn(x), Nat.double(r)) == Nat.mod(Word.to_nat(1n+p, WCon{x, t}), Nat.pow(2n, 1n+j)) : Nat}