		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svdecomp-symenv->term

Signature
(svdecomp-symenv->term x) → xx
Arguments: x — Guard (svdecomp-symenv-p x).
Returns: xx — Type (pseudo-termp xx), given the guard.

Definitions and Theorems

Function: svdecomp-symenv->term

(defun svdecomp-symenv->term (x)
 (declare (xargs :guard (svdecomp-symenv-p x)))
 (let ((__function__ 'svdecomp-symenv->term))
  (declare (ignorable __function__))
  (if (atom x)
      ''nil
    (if
      (mbt (and (consp (car x)) (svar-p (caar x))))
      (cons 'cons
            (cons (cons 'cons
                        (cons (cons 'quote
                                    (cons (svar-fix (caar x)) 'nil))
                              (cons (cdar x) 'nil)))
                  (cons (svdecomp-symenv->term (cdr x))
                        'nil)))
      (svdecomp-symenv->term (cdr x))))))

Theorem: pseudo-termp-of-svdecomp-symenv->term

(defthm pseudo-termp-of-svdecomp-symenv->term
  (implies (and (svdecomp-symenv-p x))
           (b* ((xx (svdecomp-symenv->term x)))
             (pseudo-termp xx)))
  :rule-classes :rewrite)

Theorem: svdecomp-ev-of-svdecomp-symenv->term

(defthm svdecomp-ev-of-svdecomp-symenv->term
  (equal (svdecomp-ev (svdecomp-symenv->term x)
                      a)
         (svdecomp-ev-symenv x a)))

Theorem: svdecomp-symenv->term-of-svar-alist-fix-x

(defthm svdecomp-symenv->term-of-svar-alist-fix-x
  (equal (svdecomp-symenv->term (svar-alist-fix x))
         (svdecomp-symenv->term x)))

Theorem: svdecomp-symenv->term-svar-alist-equiv-congruence-on-x

(defthm svdecomp-symenv->term-svar-alist-equiv-congruence-on-x
  (implies (svar-alist-equiv x x-equiv)
           (equal (svdecomp-symenv->term x)
                  (svdecomp-symenv->term x-equiv)))
  :rule-classes :congruence)