mb automata 4 Sections GenAutomata Doc

TheoremName
Thm* A:(Iioa{i:l}()), rho:Decl, de:sig(), e:{[[de]] rho}, s:([[ioa_all(I; i.A(i)).da]] rho), i:I. s [[A(i)]] rho de e.action[ioa_all_mng_action]
cites
Thm* ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x). (d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x)[decls_mng_member]

mb automata 4 Sections GenAutomata Doc