(2steps)
PrintForm
Definitions
mb
state
machine
Sections
GenAutomata
Doc
At:
small
action
1
1.
I:
Type
2.
M:
I
sm{i:l}()
3.
j:
I
4.
x:
(
(M(i)).da for i
I)
x
(
(M(j)).da)
By:
RSallHD -1
Generated subgoals:
None
About:
(2steps)
PrintForm
Definitions
mb
state
machine
Sections
GenAutomata
Doc
sm{i:l}()
(M(i)).da for i 
I)
x ((M(j)).da)
