Generic typed list recognizer function.
Function:
(defun element-list-nonempty-p (x) (and (consp x) (element-p (car x)) (let ((x (cdr x))) (if (consp x) (element-list-nonempty-p x) (element-list-final-cdr-p x)))))
Theorem:
(defthm element-list-nonempty-p-of-cons (implies (element-list-nonempty-p x) (iff (element-list-nonempty-p (cons a x)) (element-p a))) :rule-classes :rewrite)
Theorem:
(defthm element-list-nonempty-p-of-singleton-true-list (iff (element-list-nonempty-p (cons a nil)) (element-p a)) :rule-classes :rewrite)
Theorem:
(defthm element-list-nonempty-p-of-singleton-non-true-list (implies (and (not (consp x)) (element-list-final-cdr-p t)) (iff (element-list-nonempty-p (cons a x)) (element-p a))) :rule-classes :rewrite)
Theorem:
(defthm element-list-nonempty-p-of-cdr-when-element-list-nonempty-p (implies (and (element-list-nonempty-p (double-rewrite x)) (consp (cdr x))) (element-list-nonempty-p (cdr x))) :rule-classes :rewrite)
Theorem:
(defthm element-list-nonempty-p-when-not-consp (implies (not (consp x)) (not (element-list-nonempty-p x))) :rule-classes :rewrite)
Theorem:
(defthm element-list-nonempty-p-implies-consp (implies (element-list-nonempty-p x) (consp x)) :rule-classes :forward-chaining)
Theorem:
(defthm element-p-of-car-when-element-list-nonempty-p (implies (element-list-nonempty-p x) (element-p (car x))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-when-element-list-nonempty-p-rewrite (implies (and (element-list-nonempty-p x) (not (element-list-final-cdr-p t))) (true-listp x)) :rule-classes nil)
Theorem:
(defthm true-listp-when-element-list-nonempty-p-compound-recognizer (implies (and (element-list-nonempty-p x) (not (element-list-final-cdr-p t))) (true-listp x)) :rule-classes nil)
Theorem:
(defthm element-list-nonempty-p-of-append (implies (and (element-list-nonempty-p a) (element-list-nonempty-p b)) (element-list-nonempty-p (append a b))) :rule-classes :rewrite)