• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
      • Bed-op-p
      • Bed-from-aig
        • Match-aig-var-ite
        • Match-aig-var-ite-aux
        • Match-aig-xor-1
        • Match-aig-iff-2
        • Match-aig-xor-2
        • Match-aig-iff-1
        • Bed-from-aig-aux
        • Match-aig-nor
        • Match-aig-andc2
        • Match-aig-andc1
        • Match-aig-xor
        • Match-aig-or
        • Match-aig-iff
        • Match-aig-and
        • Match-aig-not
      • Bed-mk1
      • Bed-eval
      • Up
      • Aig-translation
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bed-from-aig

Match-aig-not

Signature

(match-aig-not x) → (mv okp arg)

Arguments

x — AIG to pattern match.

Returns

okp — Whether x matches (not arg).

arg — On success, the arg from the match.

Definitions and Theorems

Function: match-aig-not$inline

(defun match-aig-not$inline (x)
  (declare (xargs :guard t))
  (let ((__function__ 'match-aig-not))
    (declare (ignorable __function__))
    (if (and (not (aig-atom-p x)) (not (cdr x)))
        (mv t (car x))
      (mv nil nil))))

Theorem: match-aig-not-correct

(defthm match-aig-not-correct
  (b* (((mv okp arg) (match-aig-not x)))
    (implies okp
             (equal (aig-eval x env)
                    (not (aig-eval arg env))))))

Theorem: acl2-count-of-match-aig-not-weak

(defthm acl2-count-of-match-aig-not-weak
  (b* (((mv ?okp arg) (match-aig-not x)))
    (<= (acl2-count arg) (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-match-aig-not-strong

(defthm acl2-count-of-match-aig-not-strong
  (b* (((mv okp arg) (match-aig-not x)))
    (implies okp
             (< (acl2-count arg) (acl2-count x))))
  :rule-classes ((:rewrite) (:linear)))