s1,a,s2. 
l:Label. kind(a) = f(l) & M.trans(s1, < l,value(a) > ,s2))
i:I
M(i)
== mk_sm(M(i).da for i 
I,
M(i).ds for i I,
s.
i:I. M(i).init(s),
s1,a,s2. i:I. M(i).trans(s1,a,s2))
M.da)is mentioned by
|
Def (f o M)
== mk_sm(M.da o f, M.ds, M.init, s1,a,s2. l:Label. kind(a) = f(l) & M.trans(s1, < l,value(a) > ,s2)) | [sm_a_rename] |
|
Def i:I
M(i)
== mk_sm(M(i).da for i I,
M(i).ds for i I,
s.i:I. M(i).init(s),
s1,a,s2. i:I. M(i).trans(s1,a,s2)) | [sm_all] |
|
Def M.action == (M.da) | [sm_action] |
Try larger context: GenAutomata