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