		Search-engine friendly clone of the ACL2 documentation.

Irv-ballot-p

Non-empty-true-list-listp

Similar to true-list-listp, except that if x is non-empty, each element of x must be non-nil.

Signature
(non-empty-true-list-listp x) → *

Definitions and Theorems

Function: non-empty-true-list-listp

(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: non-empty-true-list-listp-implies-true-listp

(defthm non-empty-true-list-listp-implies-true-listp
  (implies (non-empty-true-list-listp xs)
           (true-listp xs))
  :rule-classes :forward-chaining)

Theorem: non-empty-true-list-listp-implies-true-list-listp

(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: non-empty-true-list-listp-bigger-implies-smaller

(defthm non-empty-true-list-listp-bigger-implies-smaller
  (implies (non-empty-true-list-listp xs)
           (non-empty-true-list-listp (cdr xs))))