M:(I
sm{i:l}()), j:I, x:
i:IM(i).action. x 
M(j).actionM:(Ism{i:l}()), j:I, x:i:IM(i).state. x M(j).statei: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))
is mentioned by
|
Thm* M:(Ism{i:l}()), j:I, x:i:IM(i).action. x M(j).action | [small_action] |
|
Thm* M:(Ism{i:l}()), j:I, x:i:IM(i).state. x M(j).state | [small_state] |
Try larger context: GenAutomata