| Rank | Theorem | Name |
| 4 | | | Thm*  A:ioa{i:l}(), I:Fmla, rho:Decl, te:(Label  Label ), a:dec().  ioa_mentions_trace(A)   trace_consistent_pred(rho;A.da;te;I) a  A.da trace_consistent_pred(rho;A.da;te;smts_eff_pred(action_effect(a.lbl;A.eff;A.frame);I)) | [trace_consistent_action_effect] |
| cites |
| 3 | | | Thm* r:rel(), as:(Label Term) List, daa:Collection(dec()), rho:Decl, te:(LabelLabel). trace_consistent_rel(rho;daa;te;r) subst_mentions_trace(as) trace_consistent_rel(rho;daa;te;rel_subst(as;r)) | [trace_consistent_rel_subst] |
| 0 | | | 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] |