|
|
|---|
|
|
|
|---|
Support lemma for generated fixing theorem.
In the events generated by defbyte, proving that the fixer returns a value that satisfies the recognizer boils down to proving that 0 satisfies the recognizer. This is easy when the size of the bytes is known: the proof is done via the executable counterparts of the functions. When the size of the bytes is a nullary function call, we need a bit of arithmetic reasoning, based on the fact that the size must be provably positive.
The following general lemma is referenced in the hints generated by defbyte.
Theorem:
(defthm defbyte-fix-support-lemma (implies (posp z) (and (<= (- (expt 2 (1- z))) 0) (< 0 (expt 2 (1- z))) (< 0 (expt 2 z)))) :rule-classes nil)