|
|
|---|
|
|
|
|---|
Support lemma for generated fixing theorem.
In the events generated by deflist-of-len, proving that the fixer returns a value that satisifes the recognizer involves showing that take returns a list of length equal to the first argument of take. This is not readily provable from the built-in definition of take, but it is proved in ACL2::std/lists/take. To avoid implicitly including that file when including this file for deflist-of-len, we locally include that file and provide the theorem here, so that it can be used in the generated theorem.
Theorem:
(defthm deflist-of-len-support-lemma (equal (len (take n x)) (nfix n)))