• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
          • 4v-and-faig-operations-commute
          • 4v-sexpr-to-faig-plain
          • 4v-sexpr-to-faig-opt
          • Sfaig
          • 4v->faig-const
          • 4v-sexpr-to-faig-list
          • Faig-const-fix
          • Faig-const->4v
          • 4v-sexpr-to-faig-alist
          • Faig-const-<=
          • Faig-const-p
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-sexpr-to-faig

4v-and-faig-operations-commute

Lemmas showing that equivalence of 4v-operations to faig-constructors.

Definitions and Theorems

Function: apply-to-args

(defun apply-to-args (fn args)
  (declare (xargs :guard t))
  (if (atom args)
      nil
    (cons (list fn (car args))
          (apply-to-args fn (cdr args)))))

Theorem: 4v->faig-const-of-4v-fix

(defthm 4v->faig-const-of-4v-fix
  (equal (4v->faig-const (4v-fix a))
         (faig-const-fix (4v->faig-const a))))

Theorem: 4v->faig-const-of-4v-unfloat

(defthm 4v->faig-const-of-4v-unfloat
  (equal (4v->faig-const (4v-unfloat a))
         (f-aig-unfloat (4v->faig-const a))))

Theorem: 4v->faig-const-of-4v-not

(defthm 4v->faig-const-of-4v-not
  (equal (4v->faig-const (4v-not a))
         (f-aig-not (4v->faig-const a))))

Theorem: 4v->faig-const-of-4v-xdet

(defthm 4v->faig-const-of-4v-xdet
  (equal (4v->faig-const (4v-xdet a))
         (f-aig-xdet (4v->faig-const a))))

Theorem: 4v->faig-const-of-4v-and

(defthm 4v->faig-const-of-4v-and
  (equal (4v->faig-const (4v-and a b))
         (f-aig-and (4v->faig-const a)
                    (4v->faig-const b))))

Theorem: 4v->faig-const-of-4v-or

(defthm 4v->faig-const-of-4v-or
  (equal (4v->faig-const (4v-or a b))
         (f-aig-or (4v->faig-const a)
                   (4v->faig-const b))))

Theorem: 4v->faig-const-of-4v-xor

(defthm 4v->faig-const-of-4v-xor
  (equal (4v->faig-const (4v-xor a b))
         (f-aig-xor (4v->faig-const a)
                    (4v->faig-const b))))

Theorem: 4v->faig-const-of-4v-iff

(defthm 4v->faig-const-of-4v-iff
  (equal (4v->faig-const (4v-iff a b))
         (f-aig-iff (4v->faig-const a)
                    (4v->faig-const b))))

Theorem: 4v->faig-const-of-4v-ite

(defthm 4v->faig-const-of-4v-ite
  (equal (4v->faig-const (4v-ite a b c))
         (f-aig-ite (4v->faig-const a)
                    (4v->faig-const b)
                    (4v->faig-const c))))

Theorem: 4v->faig-const-of-4v-ite*

(defthm 4v->faig-const-of-4v-ite*
  (equal (4v->faig-const (4v-ite* a b c))
         (f-aig-ite* (4v->faig-const a)
                     (4v->faig-const b)
                     (4v->faig-const c))))

Theorem: 4v->faig-const-of-4v-zif

(defthm 4v->faig-const-of-4v-zif
  (equal (4v->faig-const (4v-zif a b c))
         (f-aig-zif (4v->faig-const a)
                    (4v->faig-const b)
                    (4v->faig-const c))))

Theorem: 4v->faig-const-of-4v-tristate

(defthm 4v->faig-const-of-4v-tristate
  (equal (4v->faig-const (4v-tristate c a))
         (t-aig-tristate (4v->faig-const c)
                         (4v->faig-const a))))

Theorem: 4v->faig-const-of-4v-pullup

(defthm 4v->faig-const-of-4v-pullup
  (equal (4v->faig-const (4v-pullup a))
         (f-aig-pullup (4v->faig-const a))))

Theorem: 4v->faig-const-of-4v-res

(defthm 4v->faig-const-of-4v-res
  (equal (4v->faig-const (4v-res a b))
         (f-aig-res (4v->faig-const a)
                    (4v->faig-const b))))