is mentioned by

Thm* A:ioa{i:l}(), as:(LabelTerm) List, k:Label. ioa_mentions_trace(A) (i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))) subst_mentions_trace(as)	[effect_subst_mentions_trace]
Thm* r:rel(), I:Fmla, A:ioa{i:l}(), a:Label. covers_pred(A;I) r I (r':rel(). r' col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))	[covers_pred_lemma2]
Def wp2_rel(A;a;r) == col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r)	[wp2_rel]
Def wp2(A;a;Q) == (rQ.col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))	[wp2]
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]

In prior sections: mb automata 1 mb automata 2

Try larger context: GenAutomata