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]

In prior sections: mb automata 1 mb automata 2

Try larger context: GenAutomata