• 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-alist->faig-const-alist
            • 4v-list->faig-const-list
          • 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
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-sexpr-to-faig

4v->faig-const

Convert a 4vp into a faig-const-p.

Signature

(4v->faig-const x) → *

Definitions and Theorems

Function: 4v->faig-const

(defun 4v->faig-const (x)
  (declare (xargs :guard t))
  (let ((__function__ '4v->faig-const))
    (declare (ignorable __function__))
    (cond ((eq x (4vt)) (faig-t))
          ((eq x (4vf)) (faig-f))
          ((eq x (4vz)) (faig-z))
          (t (faig-x)))))

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

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

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

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

Theorem: faig-const-<=-4v->faig-const

(defthm faig-const-<=-4v->faig-const
  (equal (faig-const-<= (4v->faig-const a) b)
         (4v-<= a (faig-const->4v b))))

Theorem: 4v-<=-faig-const->4v

(defthm 4v-<=-faig-const->4v
  (equal (4v-<= (faig-const->4v a) b)
         (faig-const-<= a (4v->faig-const b))))

Theorem: 4v-equiv-implies-equal-4v->faig-const-1

(defthm 4v-equiv-implies-equal-4v->faig-const-1
  (implies (4v-equiv x x-equiv)
           (equal (4v->faig-const x)
                  (4v->faig-const x-equiv)))
  :rule-classes (:congruence))

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

(defthm faig-const-p-of-4v->faig-const
  (faig-const-p (4v->faig-const x)))

Subtopics

4v-alist->faig-const-alist

4v-list->faig-const-list