is mentioned by

Thm* t:ioa{i:l}(). t.pre Collection(pre())	[ioa_pre_wf]
Thm* t:pre(). t.rel rel()	[pre_rel_wf]
Thm* t:pre(). t.kind Label	[pre_kind_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]

Try larger context: GenAutomata