• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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.