|
|
|---|
|
|
|
|---|
Special recognizer for conses, except that to save space we require that (nil . nil) be represented just as nil.
Function:
(defun prod-consp (x) (declare (xargs :guard t)) (if (consp x) (and (or (car x) (cdr x)) t) (not x)))
Theorem:
(defthm booleanp-of-prod-consp (booleanp (prod-consp x)) :rule-classes :type-prescription)
Theorem:
(defthm prod-consp-compound-recognizer (implies (prod-consp x) (or (consp x) (not x))) :rule-classes :compound-recognizer)