|
|
|---|
|
|
|
|---|
Declarative definition of decoding as inverse of encoding.
We provide a declarative (non-executable) definition of decoding as the inverse of encoding. We use the inversion theorems proved in decoding-of-encoding and encoding-of-decoding to show that this is equivalent to the executable definition.