| Rank | Theorem | Name |
| 5 | | | Thm*  A:ioa{i:l}(), I:Fmla, rho:Decl, te:(Label  Label ).  ioa_mentions_trace(A)   trace_consistent_pred(rho;A.da;te;I) (v VCs(A;I).trace_consistent_vc(rho;A.da;te;v)) | [trace_consistent_ioa_inv_vc] |
| cites |
| 4 | | | Thm* A:ioa{i:l}(), I:Fmla, rho:Decl, te:(LabelLabel), 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] |
| 2 | | | Thm* A:ioa{i:l}(), rho:Decl, te:(LabelLabel). ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;A.init) | [trace_consistent_init] |
| 2 | | | 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] |
| 0 | | | 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] |