PrintForm Definitions mb state machine Sections GenAutomata Doc

At: sm da wf


t:sm{i:l}(). t.da Decl

By: YRecModulePiTac 4 `sm` [`sm_da`;`sm_ds`;`sm_init`;`sm_trans`]

Generated subgoals:

None


About:
memberall

PrintForm Definitions mb state machine Sections GenAutomata Doc