r:rel(), as:(Label
Term) List, daa:Collection(dec()), rho:Decl, te:(Label
Label
). trace_consistent_rel(rho;daa;te;r) 
subst_mentions_trace(as) trace_consistent_rel(rho;daa;te;rel_subst(as;r))
t.term_subst(as;t);r.args))
is mentioned by
| Thm* r:rel(), as:(LabelTerm) 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] |
In prior sections: mb automata 2 mb automata 3
Try larger context:
GenAutomata