|
|
|---|
|
|
|
|---|
Encoding applied to decoding.
We show that encoding is left inverse of decoding over valid encodings, i.e. over encodings of valid instructions: if decoding yields an instruction (which we know to be valid as proved in decode), then applying the encoding to the instruction yields the original encoding. As a consequence, decoding is injective over valid encodings: if two different encodings were decoded in the same way, the encoder would have to restore both from the same instruction, which is impossible since encoding is a function.