		Search-engine friendly clone of the ACL2 documentation.

Def-cycle-thm

Prove that an SVTV cycle FSM an unrolling of the phase FSM that it's based on

The def-cycle-thm event uses this invariant of the svtv-data stobj to prove that the cycle FSM is equivalent to the unrolling according to the cycle phases of the phase FSM. This event requires that the svtv-data stobj was not disrupted in such a way as to make its cycle FSM invalid since creating the cycle using defcycle or defsvtv$. It proves a theorem of the following form:

(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 are as follows:

(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)