is mentioned by

Thm* t:ioa{i:l}(). t.eff Collection(eff())	[ioa_eff_wf]
Def ioa_mentions_trace(A) == (e:eff(). e A.eff & mentions_trace(e.smt.term)) (p:pre(). p A.pre & rel_mentions_trace(p.rel)) (r:rel(). r A.init & rel_mentions_trace(r))	[ioa_mentions_trace]
Def ioa{i:l}() == Collection(dec())Collection(dec())Collection(rel())Collection(pre())Collection(eff()) Collection(frame())	[ioa]

In prior sections: mb automata 2

Try larger context: GenAutomata