Function:
(defun lhatom->svex-zero (x) (declare (xargs :guard (lhatom-p x))) (let ((__function__ 'lhatom->svex-zero)) (declare (ignorable __function__)) (lhatom-case x :z (svex-quote 0) :var (svex-rsh x.rsh (svex-var x.name)))))
Theorem:
(defthm svex-p-of-lhatom->svex-zero (b* ((xx (lhatom->svex-zero x))) (svex-p xx)) :rule-classes :rewrite)
Theorem:
(defthm lhatom->svex-zero-of-lhatom-fix-x (equal (lhatom->svex-zero (lhatom-fix x)) (lhatom->svex-zero x)))
Theorem:
(defthm lhatom->svex-zero-lhatom-equiv-congruence-on-x (implies (lhatom-equiv x x-equiv) (equal (lhatom->svex-zero x) (lhatom->svex-zero x-equiv))) :rule-classes :congruence)
Theorem:
(defthm lhatom->svex-zero-correct (equal (svex-eval (lhatom->svex-zero x) env) (lhatom-eval-zero x env)))