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

• Faig-fix

Faig-fix-thms

Basic theorems about faig-fix.

Definitions and Theorems

Theorem: faig-eval-faig-fix

(defthm faig-eval-faig-fix
  (equal (faig-eval (faig-fix x) env)
         (faig-eval x env)))

Theorem: faig-restrict-faig-fix

(defthm faig-restrict-faig-fix
  (equal (faig-restrict (faig-fix x) al)
         (faig-restrict x al)))

Theorem: faig-partial-eval-faig-fix

(defthm faig-partial-eval-faig-fix
  (equal (faig-partial-eval (faig-fix x) al)
         (faig-partial-eval x al)))