		Search-engine friendly clone of the ACL2 documentation.

Aig-and

Aig-and-main

And-Node, Main Optimizations, Non-Recursive.

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

Definitions and Theorems

Function: aig-and-main

(defun aig-and-main (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-and-main))
    (declare (ignorable __function__))
    (b* (((mv hit ans) (aig-and-pass1 x y))
         ((when hit) (mv :subterm ans ans))
         ((mv status arg1 arg2)
          (aig-and-pass2 x y))
         ((unless (eq status :fail))
          (mv status arg1 arg2))
         ((mv status arg1 arg2)
          (aig-and-pass3 x y))
         ((unless (eq status :fail))
          (mv status arg1 arg2))
         ((mv status arg1 arg2)
          (aig-and-pass4 x y))
         ((unless (eq status :fail))
          (mv status arg1 arg2))
         ((mv status arg1 arg2)
          (aig-and-pass5 x y))
         ((unless (eq status :fail))
          (mv status arg1 arg2)))
      (aig-and-pass6 x y))))

Theorem: aig-and-main-correct

(defthm aig-and-main-correct
  (b* (((mv ?status ?arg1 ?arg2)
        (aig-and-main 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-main-reduces-count

(defthm aig-and-main-reduces-count
  (b* (((mv ?status ?arg1 ?arg2)
        (aig-and-main 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-main-subterm-convention

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

Theorem: aig-and-main-on-failure

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

Theorem: aig-and-main-of-constants

(defthm aig-and-main-of-constants
  (and (equal (aig-and-main x nil)
              (mv :subterm nil nil))
       (equal (aig-and-main nil y)
              (mv :subterm nil nil))
       (equal (aig-and-main x t)
              (mv :subterm x x))
       (equal (aig-and-main t x)
              (mv :subterm x x))))

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

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