Decodei-is-decode
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 (decode enc feat)
and use decode-of-encode,
that simplifies to (encoding-valid-witness enc feat),
which is the same as (decodei enc feat)
by definition of the latter.
If instead the encoding enc is invalid,
by definition (decodei enc feat) is nil.
If (decode enc feat) were not nil,
it would be a witness for encoding-validp,
using encode-of-decode to show that
the encoding of the witness is enc,
but we had assumed that the encoding was not valid.
Thus also (decode enc feat) must be nil,
the same as (decodei enc feat).
Definitions and Theorems
Theorem: decodei-is-decode
(defthm decodei-is-decode
(equal (decodei enc feat)
(decode enc feat)))
