Prove that an SVTV cycle FSM an unrolling of the phase FSM that it's based on
The
(b* (((fsm phase-fsm) (phase-fsm)) ((mv values nextstate) (svtv-cycle-compile (svex-identity-subst (svex-alist-keys phase-fsm.nextstate)) (cycle-phases) phase-fsm nil))) (fsm-eval-equiv (cycle-fsm) (make-fsm :values values :nextstate nextstate)))
The options for
(def-cycle-thm svtv-name ;; used for default names ;; optional, in case cycle was introduced previously :cycle-name cycle-name :phase-name phase-name :define-cycle t :define-phase t :stobj-name svtv-data)