rho:Decl, r:rel(), da:Collection(dec())
, R:(Label
Label
). 
rel_mentions_trace(r) 
trace_consistent_rel(rho;da;R;r)i:
||r.args||. trace_consistent(rho;da;R;r.args[i])
is mentioned by
|
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] |
Try larger context: GenAutomata