law concat_pad

stelliferous@0.0.2.0 · proofs/u32_successor.bend:95

import Base
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
import stelliferous@0.0.2.0/proofs/word_width.bend as WordWidth

95law concat_pad:
96  for +width: Nat
97  for +word: Word(width)
98  {WordWidth.transport(Nat.add(width,1n),1n+width,WordEncoding.concat(width,1n,word,Word.zero(1n)),
99      Addition.successor_width(width)) == Word.shr.pad(width,word) : Word(1n+width)}