(svtv-simplify-outs/states outs nextstates simplify) → (mv simp-outs simp-states)
Function:
(defun svtv-simplify-outs/states (outs nextstates simplify) (declare (xargs :guard (and (svex-alist-p outs) (svex-alist-p nextstates)))) (let ((__function__ 'svtv-simplify-outs/states)) (declare (ignorable __function__)) (b* ((outs (svex-alist-fix outs)) (nextstates (svex-alist-fix nextstates)) ((unless simplify) (mv outs nextstates)) (alist (append outs nextstates)) (simp-alist (svex-alist-normalize-concats (svex-alist-rewrite-fixpoint alist :verbosep t) :verbosep t)) (outs-len (len outs)) (simp-outs (take outs-len simp-alist)) (simp-states (nthcdr outs-len simp-alist))) (mv simp-outs simp-states))))
Theorem:
(defthm svex-alist-p-of-svtv-simplify-outs/states.simp-outs (b* (((mv ?simp-outs ?simp-states) (svtv-simplify-outs/states outs nextstates simplify))) (svex-alist-p simp-outs)) :rule-classes :rewrite)
Theorem:
(defthm svex-alist-p-of-svtv-simplify-outs/states.simp-states (b* (((mv ?simp-outs ?simp-states) (svtv-simplify-outs/states outs nextstates simplify))) (svex-alist-p simp-states)) :rule-classes :rewrite)
Theorem:
(defthm svtv-simplify-outs/states-of-svex-alist-fix-outs (equal (svtv-simplify-outs/states (svex-alist-fix outs) nextstates simplify) (svtv-simplify-outs/states outs nextstates simplify)))
Theorem:
(defthm svtv-simplify-outs/states-svex-alist-equiv-congruence-on-outs (implies (svex-alist-equiv outs outs-equiv) (equal (svtv-simplify-outs/states outs nextstates simplify) (svtv-simplify-outs/states outs-equiv nextstates simplify))) :rule-classes :congruence)
Theorem:
(defthm svtv-simplify-outs/states-of-svex-alist-fix-nextstates (equal (svtv-simplify-outs/states outs (svex-alist-fix nextstates) simplify) (svtv-simplify-outs/states outs nextstates simplify)))
Theorem:
(defthm svtv-simplify-outs/states-svex-alist-equiv-congruence-on-nextstates (implies (svex-alist-equiv nextstates nextstates-equiv) (equal (svtv-simplify-outs/states outs nextstates simplify) (svtv-simplify-outs/states outs nextstates-equiv simplify))) :rule-classes :congruence)