Similar to true-list-listp, except that if
(non-empty-true-list-listp x) → *
Function:
(defun non-empty-true-list-listp (x) (declare (xargs :guard t)) (let ((__function__ 'non-empty-true-list-listp)) (declare (ignorable __function__)) (cond ((atom x) (eq x nil)) (t (and (true-listp (car x)) (car x) (non-empty-true-list-listp (cdr x)))))))
Theorem:
(defthm non-empty-true-list-listp-implies-true-listp (implies (non-empty-true-list-listp xs) (true-listp xs)) :rule-classes :forward-chaining)
Theorem:
(defthm non-empty-true-list-listp-implies-true-list-listp (implies (non-empty-true-list-listp x) (true-list-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm non-empty-true-list-listp-bigger-implies-smaller (implies (non-empty-true-list-listp xs) (non-empty-true-list-listp (cdr xs))))