mb
state
machine
Sections
GenAutomata
Doc
Def
mk_sm(da, ds, init, trans) == < da,ds,init,trans >
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]
Try larger context:
GenAutomata
mb
state
machine
Sections
GenAutomata
Doc