| Rank | Theorem | Name |
| 4 | | | Thm*  A:ioa{i:l}(), rho:Decl, r:rel(), R:(Label  Label ), k:Label.  ioa_mentions_trace(A)   trace_consistent_rel(rho;A.da;R;r) trace_consistent_pred(rho;A.da;R;wp_rel(A;k;r)) | [trace_consistent_wp_rel] |
| 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] |