is mentioned by

Thm* A:ioa{i:l}(), a:Label, Q:Fmla. wp2(A;a;Q) Fmla	[wp2_wf]
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]
Thm* Q:Fmla, A:ioa{i:l}(). covers_pred(A;(Q)') covers_pred(A;Q)	[covers_pred_addprime]
Thm* A:ioa{i:l}(), I:Fmla, r:rel(). r I covers_pred(A;I) covers_rel(A;r)	[covers_pred_rel_member]
Thm* t:ioa{i:l}(). t.frame Collection(frame())	[ioa_frame_wf]
Thm* t:ioa{i:l}(). t.eff Collection(eff())	[ioa_eff_wf]
Thm* t:ioa{i:l}(). t.pre Collection(pre())	[ioa_pre_wf]
Thm* t:ioa{i:l}(). t.init Collection(rel())	[ioa_init_wf]
Thm* t:ioa{i:l}(). t.da Collection(dec())	[ioa_da_wf]
Thm* t:ioa{i:l}(). t.ds Collection(dec())	[ioa_ds_wf]
Thm* A:ioa{i:l}(). A ioa{i':l}	[ioa_univ_lemma]

Try larger context: GenAutomata