		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-to-faig

Faig-const->4v

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

Definitions and Theorems

Function: faig-const->4v

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

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

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

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

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

Subtopics

Faig-const-alist->4v-alist
Faig-const-list->4v-list