(svtv-compile-phases-lazy phase nphases outs updates data state-machine) → (mv outalist final-state)
Function:
(defun svtv-compile-phases-lazy (phase nphases outs updates data state-machine) (declare (xargs :guard (and (natp phase) (posp nphases) (svtv-lines-p outs) (svex-alist-p updates) (svtv-composedata-p data)))) (declare (xargs :guard (<= phase nphases))) (let ((__function__ 'svtv-compile-phases-lazy)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (pos-fix nphases) (nfix phase))) :exec (eql nphases phase))) (mv nil (and state-machine (svex-alist-compose-svtv-phases (nth phase (svtv-composedata->nextstates data)) (1- (lposfix nphases)) data)))) (phase-outalist (svex-alist-compose (svtv-outputs->outalist outs phase) updates)) (composed-outalist (svex-alist-compose-svtv-phases phase-outalist phase data)) ((mv rest-outs final-state) (svtv-compile-phases-lazy (1+ (lnfix phase)) nphases outs updates data state-machine))) (mv (append composed-outalist rest-outs) final-state))))
Theorem:
(defthm svex-alist-p-of-svtv-compile-phases-lazy.outalist (b* (((mv ?outalist ?final-state) (svtv-compile-phases-lazy phase nphases outs updates data state-machine))) (svex-alist-p outalist)) :rule-classes :rewrite)
Theorem:
(defthm svex-alist-p-of-svtv-compile-phases-lazy.final-state (b* (((mv ?outalist ?final-state) (svtv-compile-phases-lazy phase nphases outs updates data state-machine))) (svex-alist-p final-state)) :rule-classes :rewrite)
Theorem:
(defthm svtv-compile-phases-lazy-of-nfix-phase (equal (svtv-compile-phases-lazy (nfix phase) nphases outs updates data state-machine) (svtv-compile-phases-lazy phase nphases outs updates data state-machine)))
Theorem:
(defthm svtv-compile-phases-lazy-nat-equiv-congruence-on-phase (implies (nat-equiv phase phase-equiv) (equal (svtv-compile-phases-lazy phase nphases outs updates data state-machine) (svtv-compile-phases-lazy phase-equiv nphases outs updates data state-machine))) :rule-classes :congruence)
Theorem:
(defthm svtv-compile-phases-lazy-of-pos-fix-nphases (equal (svtv-compile-phases-lazy phase (pos-fix nphases) outs updates data state-machine) (svtv-compile-phases-lazy phase nphases outs updates data state-machine)))
Theorem:
(defthm svtv-compile-phases-lazy-pos-equiv-congruence-on-nphases (implies (pos-equiv nphases nphases-equiv) (equal (svtv-compile-phases-lazy phase nphases outs updates data state-machine) (svtv-compile-phases-lazy phase nphases-equiv outs updates data state-machine))) :rule-classes :congruence)
Theorem:
(defthm svtv-compile-phases-lazy-of-svtv-lines-fix-outs (equal (svtv-compile-phases-lazy phase nphases (svtv-lines-fix outs) updates data state-machine) (svtv-compile-phases-lazy phase nphases outs updates data state-machine)))
Theorem:
(defthm svtv-compile-phases-lazy-svtv-lines-equiv-congruence-on-outs (implies (svtv-lines-equiv outs outs-equiv) (equal (svtv-compile-phases-lazy phase nphases outs updates data state-machine) (svtv-compile-phases-lazy phase nphases outs-equiv updates data state-machine))) :rule-classes :congruence)
Theorem:
(defthm svtv-compile-phases-lazy-of-svex-alist-fix-updates (equal (svtv-compile-phases-lazy phase nphases outs (svex-alist-fix updates) data state-machine) (svtv-compile-phases-lazy phase nphases outs updates data state-machine)))
Theorem:
(defthm svtv-compile-phases-lazy-svex-alist-equiv-congruence-on-updates (implies (svex-alist-equiv updates updates-equiv) (equal (svtv-compile-phases-lazy phase nphases outs updates data state-machine) (svtv-compile-phases-lazy phase nphases outs updates-equiv data state-machine))) :rule-classes :congruence)
Theorem:
(defthm svtv-compile-phases-lazy-of-svtv-composedata-fix-data (equal (svtv-compile-phases-lazy phase nphases outs updates (svtv-composedata-fix data) state-machine) (svtv-compile-phases-lazy phase nphases outs updates data state-machine)))
Theorem:
(defthm svtv-compile-phases-lazy-svtv-composedata-equiv-congruence-on-data (implies (svtv-composedata-equiv data data-equiv) (equal (svtv-compile-phases-lazy phase nphases outs updates data state-machine) (svtv-compile-phases-lazy phase nphases outs updates data-equiv state-machine))) :rule-classes :congruence)