A:ioa{i:l}(), rho:Decl, te:(Label
Label
). 
ioa_mentions_trace(A) 
trace_consistent_pred(rho;A.da;te;A.init)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). ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;A.init) | [trace_consistent_init] | ||
| 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] |