Basic theorems about major-stack-p, generated by deflist.
Theorem:
(defthm major-stack-p-of-cons (implies (major-stack-p x) (iff (major-stack-p (cons a x)) (major-frame-p a))) :rule-classes ((:rewrite)))
Theorem:
(defthm major-stack-p-of-singleton (iff (major-stack-p (cons a nil)) (major-frame-p a)) :rule-classes ((:rewrite)))
Theorem:
(defthm major-stack-p-of-cdr-when-major-stack-p (implies (and (major-stack-p (double-rewrite x)) (consp (cdr x))) (major-stack-p (cdr x))) :rule-classes ((:rewrite)))
Theorem:
(defthm major-stack-p-when-not-consp (implies (not (consp x)) (not (major-stack-p x))) :rule-classes ((:rewrite)))
Theorem:
(defthm major-stack-p-implies-consp (implies (major-stack-p x) (consp x)) :rule-classes ((:forward-chaining :trigger-terms ((acl2::element-list-nonempty-p x)))))
Theorem:
(defthm major-frame-p-of-car-when-major-stack-p (implies (major-stack-p x) (major-frame-p (car x))) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-when-major-stack-p (implies (major-stack-p x) (true-listp x)) :rule-classes :compound-recognizer)
Theorem:
(defthm major-stack-p-of-append (implies (and (major-stack-p a) (major-stack-p b)) (major-stack-p (append a b))) :rule-classes ((:rewrite)))