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

• Aig-compose

Aig-compose-thms

Basic theorems about aig-compose.

Definitions and Theorems

Theorem: aig-eval-of-aig-compose

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

Theorem: aig-equiv-implies-aig-equiv-aig-compose-1

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

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

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

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

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