Theorem:
(defthm ev-process-hint-constraint-0 (implies (and (consp acl2::x) (syntaxp (not (equal acl2::a ''nil))) (not (equal (car acl2::x) 'quote))) (equal (ev-process-hint acl2::x acl2::a) (ev-process-hint (cons (car acl2::x) (kwote-lst (ev-lst-process-hint (cdr acl2::x) acl2::a))) nil))))
Theorem:
(defthm ev-process-hint-constraint-1 (implies (symbolp acl2::x) (equal (ev-process-hint acl2::x acl2::a) (and acl2::x (cdr (assoc-equal acl2::x acl2::a))))))
Theorem:
(defthm ev-process-hint-constraint-2 (implies (and (consp acl2::x) (equal (car acl2::x) 'quote)) (equal (ev-process-hint acl2::x acl2::a) (cadr acl2::x))))
Theorem:
(defthm ev-process-hint-constraint-3 (implies (and (consp acl2::x) (consp (car acl2::x))) (equal (ev-process-hint acl2::x acl2::a) (ev-process-hint (caddr (car acl2::x)) (pairlis$ (cadr (car acl2::x)) (ev-lst-process-hint (cdr acl2::x) acl2::a))))))
Theorem:
(defthm ev-process-hint-constraint-4 (implies (not (consp acl2::x-lst)) (equal (ev-lst-process-hint acl2::x-lst acl2::a) nil)))
Theorem:
(defthm ev-process-hint-constraint-5 (implies (consp acl2::x-lst) (equal (ev-lst-process-hint acl2::x-lst acl2::a) (cons (ev-process-hint (car acl2::x-lst) acl2::a) (ev-lst-process-hint (cdr acl2::x-lst) acl2::a)))))
Theorem:
(defthm ev-process-hint-constraint-6 (implies (and (not (consp acl2::x)) (not (symbolp acl2::x))) (equal (ev-process-hint acl2::x acl2::a) nil)))
Theorem:
(defthm ev-process-hint-constraint-7 (implies (and (consp acl2::x) (not (consp (car acl2::x))) (not (symbolp (car acl2::x)))) (equal (ev-process-hint acl2::x acl2::a) nil)))
Theorem:
(defthm ev-process-hint-constraint-8 (implies (and (consp acl2::x) (equal (car acl2::x) 'not)) (equal (ev-process-hint acl2::x acl2::a) (not (ev-process-hint (cadr acl2::x) acl2::a)))))
Theorem:
(defthm ev-process-hint-constraint-9 (implies (and (consp acl2::x) (equal (car acl2::x) 'if)) (equal (ev-process-hint acl2::x acl2::a) (if (ev-process-hint (cadr acl2::x) acl2::a) (ev-process-hint (caddr acl2::x) acl2::a) (ev-process-hint (cadddr acl2::x) acl2::a)))))
Theorem:
(defthm ev-process-hint-constraint-10 (implies (and (consp acl2::x) (equal (car acl2::x) 'hint-please)) (equal (ev-process-hint acl2::x acl2::a) (hint-please (ev-process-hint (cadr acl2::x) acl2::a)))))
Theorem:
(defthm ev-process-hint-disjoin-cons (iff (ev-process-hint (disjoin (cons acl2::x acl2::y)) acl2::a) (or (ev-process-hint acl2::x acl2::a) (ev-process-hint (disjoin acl2::y) acl2::a))))
Theorem:
(defthm ev-process-hint-disjoin-when-consp (implies (consp acl2::x) (iff (ev-process-hint (disjoin acl2::x) acl2::a) (or (ev-process-hint (car acl2::x) acl2::a) (ev-process-hint (disjoin (cdr acl2::x)) acl2::a)))))
Theorem:
(defthm ev-process-hint-disjoin-atom (implies (not (consp acl2::x)) (equal (ev-process-hint (disjoin acl2::x) acl2::a) nil)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm ev-process-hint-disjoin-append (iff (ev-process-hint (disjoin (append acl2::x acl2::y)) acl2::a) (or (ev-process-hint (disjoin acl2::x) acl2::a) (ev-process-hint (disjoin acl2::y) acl2::a))))
Theorem:
(defthm ev-process-hint-conjoin-cons (iff (ev-process-hint (conjoin (cons acl2::x acl2::y)) acl2::a) (and (ev-process-hint acl2::x acl2::a) (ev-process-hint (conjoin acl2::y) acl2::a))))
Theorem:
(defthm ev-process-hint-conjoin-when-consp (implies (consp acl2::x) (iff (ev-process-hint (conjoin acl2::x) acl2::a) (and (ev-process-hint (car acl2::x) acl2::a) (ev-process-hint (conjoin (cdr acl2::x)) acl2::a)))))
Theorem:
(defthm ev-process-hint-conjoin-atom (implies (not (consp acl2::x)) (equal (ev-process-hint (conjoin acl2::x) acl2::a) t)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm ev-process-hint-conjoin-append (iff (ev-process-hint (conjoin (append acl2::x acl2::y)) acl2::a) (and (ev-process-hint (conjoin acl2::x) acl2::a) (ev-process-hint (conjoin acl2::y) acl2::a))))
Theorem:
(defthm ev-process-hint-conjoin-clauses-cons (iff (ev-process-hint (conjoin-clauses (cons acl2::x acl2::y)) acl2::a) (and (ev-process-hint (disjoin acl2::x) acl2::a) (ev-process-hint (conjoin-clauses acl2::y) acl2::a))))
Theorem:
(defthm ev-process-hint-conjoin-clauses-when-consp (implies (consp acl2::x) (iff (ev-process-hint (conjoin-clauses acl2::x) acl2::a) (and (ev-process-hint (disjoin (car acl2::x)) acl2::a) (ev-process-hint (conjoin-clauses (cdr acl2::x)) acl2::a)))))
Theorem:
(defthm ev-process-hint-conjoin-clauses-atom (implies (not (consp acl2::x)) (equal (ev-process-hint (conjoin-clauses acl2::x) acl2::a) t)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm ev-process-hint-conjoin-clauses-append (iff (ev-process-hint (conjoin-clauses (append acl2::x acl2::y)) acl2::a) (and (ev-process-hint (conjoin-clauses acl2::x) acl2::a) (ev-process-hint (conjoin-clauses acl2::y) acl2::a))))
Theorem:
(defthm correctness-of-process-hint (implies (and (pseudo-term-listp cl) (alistp b) (ev-process-hint (conjoin-clauses (process-hint cl hint)) b)) (ev-process-hint (disjoin cl) b)) :rule-classes :clause-processor)