(svdecomp-symenv->term x) → xx
Function:
(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:
(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:
(defthm svdecomp-ev-of-svdecomp-symenv->term (equal (svdecomp-ev (svdecomp-symenv->term x) a) (svdecomp-ev-symenv x a)))
Theorem:
(defthm svdecomp-symenv->term-of-svar-alist-fix-x (equal (svdecomp-symenv->term (svar-alist-fix x)) (svdecomp-symenv->term x)))
Theorem:
(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)