Decode-is-decodex
Equivalence of declarative and executable decoding.
If the encoding enc is valid,
it is equal to (encode (encoding-valid-witness enc feat) feat)
by the definition of encoding-validp.
If we substitute that into (decodex enc feat)
and use decodex-of-encode,
that simplifies to (encoding-valid-witness enc feat),
which is the same as (decode enc feat)
by definition of the latter.
If instead the encoding enc is invalid,
by definition (decode enc feat) is nil.
If (decodex enc feat) were not nil,
it would be a witness for encoding-validp,
using encode-of-decodex to show that
the encoding of the witness is enc,
but we had assumed that the encoding was not valid.
Thus also (decodex enc feat) must be nil,
the same as (decode enc feat).
Definitions and Theorems
Theorem: decode-is-decodex
(defthm decode-is-decodex
(equal (decode enc feat)
(decodex enc feat)))
