• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
      • Faig-constructors
      • Faig-onoff-equiv
      • Faig-purebool-p
      • Faig-alist-equiv
        • Faig-alist-equiv-thms
      • Faig-equiv
      • Faig-eval
      • Faig-restrict
      • Faig-fix
      • Faig-partial-eval
      • Faig-compose
      • Faig-compose-alist
      • Patbind-faig
      • Faig-constants
    • Bed
    • 4v
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Faig

Faig-alist-equiv

We say the FAIG Alists X and Y are equivalent when they bind the same keys to equivalent FAIGs, in the sense of faig-equiv.

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

Function: faig-alist-equiv

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

Definitions and Theorems

Theorem: faig-alist-equiv-necc

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

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

(defthm faig-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))
                           (faig-equiv (cdr (hons-assoc-equal k x))
                                       (cdr (hons-assoc-equal k y)))
                         'nil)))
                (faig-alist-equiv-witness x y)
                y x))
          (faig-alist-equiv x y))
 :rule-classes nil)

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

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

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

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

Subtopics

Faig-alist-equiv-thms

Basic theorems about faig-alist-equiv.