• 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-restrict-alist
          • Aig-restrict-alist-thms
        • 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
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Aig-restrict-alist

Aig-restrict-alist-thms

Basic theorems about aig-restrict-alist.

Definitions and Theorems

Theorem: lookup-in-aig-restrict-alist

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

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

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

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

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

Theorem: aig-eval-alist-of-aig-restrict-alist

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

Theorem: aig-restrict-alist-aig-restrict-alist

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