|
|
|---|
|
|
|
|---|
Encoding applied to the executable decoding.
We show that the executable decoding is right inverse of encoding (i.e. that encoding is left inverse of the executable 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 decodex), 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.