• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
      • Aig-constructors
      • Aig-vars
        • Aig-vars-thms
        • Aig-vars-1pass
        • Aig-vars-fast
      • Aig-sat
      • Bddify
      • Aig-substitution
      • 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-vars

Aig-vars-thms

Theorems about aig-vars from centaur/aig/aig-vars.

Definitions and Theorems

Theorem: aig-vars-cons

(defthm aig-vars-cons
  (implies (or x (not y))
           (equal (aig-vars (cons x y))
                  (set::union (aig-vars x)
                              (aig-vars y)))))

Theorem: member-aig-vars-alist-vals

(defthm member-aig-vars-alist-vals
 (implies (not (set::in v (aiglist-vars (alist-vals al))))
          (not (set::in v
                        (aig-vars (cdr (hons-assoc-equal x al)))))))

Theorem: aig-vars-aig-not

(defthm aig-vars-aig-not
  (equal (aig-vars (aig-not x))
         (aig-vars x)))

Theorem: member-aig-vars-aig-and

(defthm member-aig-vars-aig-and
  (implies (and (not (set::in v (aig-vars x)))
                (not (set::in v (aig-vars y))))
           (not (set::in v (aig-vars (aig-and x y))))))

Theorem: member-aig-vars-aig-and-dumb

(defthm member-aig-vars-aig-and-dumb
  (implies (and (not (set::in v (aig-vars x)))
                (not (set::in v (aig-vars y))))
           (not (set::in v (aig-vars (aig-and-dumb x y))))))

Theorem: member-aig-vars-aig-restrict

(defthm member-aig-vars-aig-restrict
  (implies (and (not (and (set::in v (aig-vars x))
                          (not (member-equal v (alist-keys al)))))
                (not (set::in v (aiglist-vars (alist-vals al)))))
           (not (set::in v (aig-vars (aig-restrict x al))))))

Theorem: member-aig-vars-aig-partial-eval

(defthm member-aig-vars-aig-partial-eval
  (implies (not (and (set::in v (aig-vars x))
                     (not (member-equal v (alist-keys al)))))
           (not (set::in v (aig-vars (aig-partial-eval x al))))))