• 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-equiv
      • Faig-eval
      • Faig-restrict
      • Faig-fix
      • Faig-partial-eval
      • Faig-compose
      • Faig-compose-alist
        • Faig-compose-alist-thms
      • Patbind-faig
      • Faig-constants
    • Bed
    • 4v
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Faig-compose-alist

Faig-compose-alist-thms

Basic theorems about faig-compose-alist.

Definitions and Theorems

Theorem: faig-eval-alist-of-faig-compose-alist

(defthm faig-eval-alist-of-faig-compose-alist
  (equal (faig-eval-alist (faig-compose-alist x al1)
                          al2)
         (faig-eval-alist x (aig-eval-alist al1 al2))))

Theorem: lookup-in-faig-compose-alist

(defthm lookup-in-faig-compose-alist
  (equal (hons-assoc-equal k (faig-compose-alist x env))
         (and (hons-assoc-equal k x)
              (cons k
                    (faig-compose (cdr (hons-assoc-equal k x))
                                  env)))))

Theorem: faig-alist-equiv-implies-faig-alist-equiv-faig-compose-alist-1

(defthm
     faig-alist-equiv-implies-faig-alist-equiv-faig-compose-alist-1
  (implies (faig-alist-equiv x x-equiv)
           (faig-alist-equiv (faig-compose-alist x al)
                             (faig-compose-alist x-equiv al)))
  :rule-classes (:congruence))

Theorem: aig-alist-equiv-implies-faig-alist-equiv-faig-compose-alist-2

(defthm
      aig-alist-equiv-implies-faig-alist-equiv-faig-compose-alist-2
  (implies (aig-alist-equiv al al-equiv)
           (faig-alist-equiv (faig-compose-alist x al)
                             (faig-compose-alist x al-equiv)))
  :rule-classes (:congruence))

Theorem: alist-equiv-implies-equal-faig-compose-alist-2

(defthm alist-equiv-implies-equal-faig-compose-alist-2
  (implies (alist-equiv env env-equiv)
           (equal (faig-compose-alist x env)
                  (faig-compose-alist x env-equiv)))
  :rule-classes (:congruence))