		Search-engine friendly clone of the ACL2 documentation.

Aig-and

Aig-and-pass6a

Level 3 Substitution Rules, Single Direction.

Signature
(aig-and-pass6a x y) → (mv status arg1 arg2)

Definitions and Theorems

Function: aig-and-pass6a

(defun aig-and-pass6a (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-and-pass6a))
    (declare (ignorable __function__))
    (b* (((unless (and (not (aig-atom-p x))
                       (eq (cdr x) nil)
                       (not (aig-atom-p (car x)))
                       (not (eq (cdar x) nil))))
          (mv :fail x y))
         (a (caar x))
         (b (cdar x))
         ((when (hons-equal a y))
          (mv :reduced a (aig-not b)))
         ((when (hons-equal b y))
          (mv :reduced b (aig-not a)))
         ((unless (and (not (aig-atom-p y))
                       (not (eq (cdr y) nil))))
          (mv :fail x y))
         (c (car y))
         (d (cdr y))
         ((when (or (hons-equal b c) (hons-equal b d)))
          (mv :reduced (aig-not a) y))
         ((when (or (hons-equal a c) (hons-equal a d)))
          (mv :reduced (aig-not b) y)))
      (mv :fail x y))))

Theorem: aig-and-pass6a-correct

(defthm aig-and-pass6a-correct
  (b* (((mv ?status ?arg1 ?arg2)
        (aig-and-pass6a x y)))
    (equal (and (aig-eval arg1 env)
                (aig-eval arg2 env))
           (and (aig-eval x env)
                (aig-eval y env))))
  :rule-classes nil)

Theorem: aig-and-pass6a-reduces-count

(defthm aig-and-pass6a-reduces-count
  (b* (((mv ?status ?arg1 ?arg2)
        (aig-and-pass6a x y)))
    (implies (eq status :reduced)
             (< (+ (aig-and-count arg1)
                   (aig-and-count arg2))
                (+ (aig-and-count x)
                   (aig-and-count y)))))
  :rule-classes nil)

Theorem: aig-and-pass6a-subterm-convention

(defthm aig-and-pass6a-subterm-convention
  (b* (((mv ?status ?arg1 ?arg2)
        (aig-and-pass6a x y)))
    (implies (equal status :subterm)
             (equal arg2 arg1))))

Theorem: aig-and-pass6a-arg2-on-failure

(defthm aig-and-pass6a-arg2-on-failure
  (b* (((mv ?status ?arg1 ?arg2)
        (aig-and-pass6a x y)))
    (implies (and (equal status :fail) y)
             (iff arg2 t))))

Theorem: aig-and-pass6a-when-fail

(defthm aig-and-pass6a-when-fail
  (b* (((mv ?status ?arg1 ?arg2)
        (aig-and-pass6a x y)))
    (implies (and (not (equal status :subterm))
                  (not (equal status :reduced)))
             (and (equal status :fail)
                  (equal arg1 x)
                  (equal arg2 y)))))