		Search-engine friendly clone of the ACL2 documentation.

Bed-from-aig

Match-aig-xor-1

Signature
(match-aig-xor-1 x) → (mv okp arg1 arg2)
Arguments: x — AIG to pattern match.
Returns: okp — Whether x matches (xor arg1 arg2).; arg1 — On success, arg1 from the match.; arg2 — On success, arg2 from the match.

Definitions and Theorems

Function: match-aig-xor-1

(defun match-aig-xor-1 (x)
  (declare (xargs :guard t))
  (let ((__function__ 'match-aig-xor-1))
    (declare (ignorable __function__))
    (b* (((mv okp left right) (match-aig-or x))
         ((unless okp) (mv nil nil nil))
         ((mv okp a b) (match-aig-andc1 left))
         ((when okp)
          (b* (((mv okp c d) (match-aig-andc1 right))
               ((when (and okp (hons-equal a d)
                           (hons-equal b c)))
                (mv t a b))
               ((mv okp c d) (match-aig-andc2 right))
               ((when (and okp (hons-equal a c)
                           (hons-equal b d)))
                (mv t a b)))
            (mv nil nil nil)))
         ((mv okp a b) (match-aig-andc2 left))
         ((unless okp) (mv nil nil nil))
         ((mv okp c d) (match-aig-andc1 right))
         ((when (and okp (hons-equal a c)
                     (hons-equal b d)))
          (mv t a b))
         ((mv okp c d) (match-aig-andc2 right))
         ((when (and okp (hons-equal a d)
                     (hons-equal b c)))
          (mv t a b)))
      (mv nil nil nil))))

Theorem: match-aig-xor-1-correct

(defthm match-aig-xor-1-correct
  (b* (((mv okp arg1 arg2)
        (match-aig-xor-1 x)))
    (implies okp
             (equal (aig-eval x env)
                    (xor (aig-eval arg1 env)
                         (aig-eval arg2 env))))))

Theorem: acl2-count-of-match-aig-xor-1-weak-1

(defthm acl2-count-of-match-aig-xor-1-weak-1
  (b* (((mv & arg1 &) (match-aig-xor-1 x)))
    (<= (acl2-count arg1) (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-match-aig-xor-1-weak-2

(defthm acl2-count-of-match-aig-xor-1-weak-2
  (b* (((mv & & arg2) (match-aig-xor-1 x)))
    (<= (acl2-count arg2) (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-match-aig-xor-1-strong-1

(defthm acl2-count-of-match-aig-xor-1-strong-1
  (b* (((mv okp arg1 &) (match-aig-xor-1 x)))
    (implies okp
             (< (acl2-count arg1) (acl2-count x))))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-match-aig-xor-1-strong-2

(defthm acl2-count-of-match-aig-xor-1-strong-2
  (b* (((mv okp & arg2) (match-aig-xor-1 x)))
    (implies okp
             (< (acl2-count arg2) (acl2-count x))))
  :rule-classes ((:rewrite) (:linear)))