law wpad

lawful-words@0.1.0.0 · proof_word.bend:633

import Base

633law wpad:
634  for +p: Nat
635  for +t: Word(p)
636  {Word.to_nat(1n+p, Word.shr.pad(p, t)) == Word.to_nat(p, t) : Nat}