mb
state
machine
Sections
GenAutomata
Doc
Theorem
Name
Thm*
M:sm{i:l}(), a:M.action. kind(a)
Label & kind(a)
Pattern
[kind_wf2]
cites
Thm*
d:Decl, a:(
d). kind(a)
Label
[kind_wf]
mb
state
machine
Sections
GenAutomata
Doc
M:sm{i:l}(), a:M.action. kind(a) 
Label & kind(a) Patternd:Decl, a:(
d). kind(a) LabelM:sm{i:l}(), a:M.action. kind(a) Label & kind(a) Patternd:Decl, a:(d). kind(a) Label