• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
      • Aig-constructors
      • Aig-vars
      • Aig-sat
      • Bddify
      • Aig-substitution
        • Aig-partial-eval
        • Aig-restrict
          • Aig-restrict-thms
        • Aig-compose
        • 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-restrict

Aig-restrict-thms

Basic theorems about aig-restrict.

Definitions and Theorems

Theorem: aig-equiv-implies-aig-equiv-aig-restrict-1

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

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

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

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

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

Theorem: aig-restrict-aig-restrict

(defthm aig-restrict-aig-restrict
  (aig-equiv (aig-restrict (aig-restrict x al1) al2)
             (aig-restrict x
                           (append (aig-restrict-alist al1 al2)
                                   al2))))