• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
      • Aig-constructors
      • Aig-vars
      • Aig-sat
      • Bddify
      • Aig-substitution
      • Aig-other
      • Aig-semantics
        • Aig-eval
        • Aig-alist-equiv
        • Aig-env-equiv
        • Aig-equiv
        • Aig-eval-alist
        • Aig-eval-list
        • Aig-eval-alists
      • Aig-and-count
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Aig-semantics

Aig-alist-equiv

We say the AIG Alists X and Y are equivalent when they bind the same keys to equivalent AIGs, in the sense of aig-equiv.

This is a universal equivalence, introduced using def-universal-equiv.

Function: aig-alist-equiv

(defun
     aig-alist-equiv (x y)
     (declare (xargs :non-executable t))
     (declare (xargs :guard t))
     (prog2$ (throw-nonexec-error 'aig-alist-equiv
                                  (list x y))
             (let ((k (aig-alist-equiv-witness x y)))
                  (and (iff (hons-assoc-equal k x)
                            (hons-assoc-equal k y))
                       (aig-equiv (cdr (hons-assoc-equal k x))
                                  (cdr (hons-assoc-equal k y)))))))

Definitions and Theorems

Theorem: aig-alist-equiv-necc

(defthm
     aig-alist-equiv-necc
     (implies (not (and (iff (hons-assoc-equal k x)
                             (hons-assoc-equal k y))
                        (aig-equiv (cdr (hons-assoc-equal k x))
                                   (cdr (hons-assoc-equal k y)))))
              (not (aig-alist-equiv x y))))

Theorem: aig-alist-equiv-witnessing-witness-rule-correct

(defthm
 aig-alist-equiv-witnessing-witness-rule-correct
 (implies
     (not ((lambda (k y x)
                   (not (if (iff (hons-assoc-equal k x)
                                 (hons-assoc-equal k y))
                            (aig-equiv (cdr (hons-assoc-equal k x))
                                       (cdr (hons-assoc-equal k y)))
                            'nil)))
           (aig-alist-equiv-witness x y)
           y x))
     (aig-alist-equiv x y))
 :rule-classes nil)

Theorem: aig-alist-equiv-instancing-instance-rule-correct

(defthm aig-alist-equiv-instancing-instance-rule-correct
        (implies (not (if (iff (hons-assoc-equal k x)
                               (hons-assoc-equal k y))
                          (aig-equiv (cdr (hons-assoc-equal k x))
                                     (cdr (hons-assoc-equal k y)))
                          'nil))
                 (not (aig-alist-equiv x y)))
        :rule-classes nil)

Theorem: aig-alist-equiv-is-an-equivalence

(defthm aig-alist-equiv-is-an-equivalence
        (and (booleanp (aig-alist-equiv x y))
             (aig-alist-equiv x x)
             (implies (aig-alist-equiv x y)
                      (aig-alist-equiv y x))
             (implies (and (aig-alist-equiv x y)
                           (aig-alist-equiv y z))
                      (aig-alist-equiv x z)))
        :rule-classes (:equivalence))

Theorem: alist-equiv-refines-aig-alist-equiv

(defthm alist-equiv-refines-aig-alist-equiv
        (implies (alist-equiv x y)
                 (aig-alist-equiv x y))
        :rule-classes (:refinement))