is mentioned by

Thm* p,q:Fmla, rho:Decl, da:Collection(dec()), R:(LabelLabel). trace_consistent_pred(rho;da;R;p q) trace_consistent_pred(rho;da;R;p) & trace_consistent_pred(rho;da;R;q)	[trace_consistent_pred_and]
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