is mentioned by

Thm* A:ioa{i:l}(), rho:Decl, te:(LabelLabel), k:Label. ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;action_pre(k;A.pre))	[trace_consistent_action_pre]
Def ioa_trans(A;a;I) == vc_qimp(mk_qimp(a, I action_pre(a;A.pre), smts_eff_pred(action_effect(a;A.eff;A.frame);I)))	[ioa_trans]

Try larger context: GenAutomata