M:sm{i:l}(), f:(Label
Label), s:(f o M).state. s 
M.state
s1,a,s2. 
l:Label. kind(a) = f(l) & M.trans(s1, < l,value(a) > ,s2))
is mentioned by
|
Thm* M:sm{i:l}(), f:(LabelLabel), s:(f o M).state. s M.state | [sm_a_rename_state] |
Try larger context: GenAutomata