|
|
|---|
|
|
|
|---|
Correctness of the executable decoding.
We use the inversion theorems proved in decoding-left-inverse and decoding-right-inverse to show that the declarative definition of the decoder is equivalent to the executable definition of the decoder.
See encoding-decoding-illustration for an illustration of encoding and decoding.