Function:
(defun svstack-filter-global-lhs-vars (x stack) (declare (xargs :guard (and (lhs-p x) (svstack-p stack)))) (declare (xargs :guard (consp stack))) (let ((__function__ 'svstack-filter-global-lhs-vars)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((lhrange x1) (lhrange-fix (car x))) ((when (lhatom-case x1.atom :z)) (svstack-filter-global-lhs-vars (cdr x) stack)) ((lhatom-var x1.atom)) ((unless (svstack-globalp x1.atom.name stack)) (svstack-filter-global-lhs-vars (cdr x) stack))) (cons x1 (svstack-filter-global-lhs-vars (cdr x) stack)))))
Theorem:
(defthm lhs-p-of-svstack-filter-global-lhs-vars (b* ((filtered-lhs (svstack-filter-global-lhs-vars x stack))) (lhs-p filtered-lhs)) :rule-classes :rewrite)
Theorem:
(defthm svstack-filter-global-lhs-vars-of-lhs-fix-x (equal (svstack-filter-global-lhs-vars (lhs-fix x) stack) (svstack-filter-global-lhs-vars x stack)))
Theorem:
(defthm svstack-filter-global-lhs-vars-lhs-equiv-congruence-on-x (implies (lhs-equiv x x-equiv) (equal (svstack-filter-global-lhs-vars x stack) (svstack-filter-global-lhs-vars x-equiv stack))) :rule-classes :congruence)
Theorem:
(defthm svstack-filter-global-lhs-vars-of-svstack-fix-stack (equal (svstack-filter-global-lhs-vars x (svstack-fix stack)) (svstack-filter-global-lhs-vars x stack)))
Theorem:
(defthm svstack-filter-global-lhs-vars-svstack-equiv-congruence-on-stack (implies (svstack-equiv stack stack-equiv) (equal (svstack-filter-global-lhs-vars x stack) (svstack-filter-global-lhs-vars x stack-equiv))) :rule-classes :congruence)