mb
state
machine
Sections
GenAutomata
Doc
Def
t.ds == 1of(2of(t))
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.state == {M.ds}
[sm_state]
Try larger context:
GenAutomata
mb
state
machine
Sections
GenAutomata
Doc