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