A:ioa{i:l}(), rho:Decl, te:(Label
Label
), k:Label. 
ioa_mentions_trace(A) 
trace_consistent_pred(rho;A.da;te;action_pre(k;A.pre))rho:Decl, r:rel(), da:Collection(dec()), R:(LabelLabel). rel_mentions_trace(r) trace_consistent_rel(rho;da;R;r)| Rank | Theorem | Name | ||
| 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] | ||
| cites | ||||
| 1 | Thm* rho:Decl, r:rel(), da:Collection(dec()), R:(LabelLabel). rel_mentions_trace(r) trace_consistent_rel(rho;da;R;r) | [no_mention_implies_consistent_rel] |