|
|
|---|
|
|
|
|---|
Rewrite: (RESET-ARRAY1 name l) = (LIST (HEADER name l)).
This definition of RESET-ARRAY1 is logically equivalent to the actual definition. The actual definition, which includes a COMPRESS1 call, has the run-time side-effect of re-installing the new array. The COMPRESS1 is logically redundant, however.
This lemma is exported DISABLED, however this is the preferred definition to use to reason about RESET-ARRAY1.
Theorem:
(defthm reset-array1* (implies (array1p name l) (equal (reset-array1 name l) (list (header name l)))))