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]
Thm* rho:Decl, t:Term, da:Collection(dec()), R:(LabelLabel). trace_consistent(rho;da;R;t) Prop	[trace_consistent_wf]
Thm* rho:Decl, t:Term, da:Collection(dec()) , R:(LabelLabel). mentions_trace(t) trace_consistent(rho;da;R;t)	[no_mention_implies_consistent_term]
Thm* r:rel(), te:(LabelLabel), rho,ds,da,de,e,s,a:Top. [[r]] rho ds da de e s a mk_trace_env(nil, te) ~ [[r]] rho ds da de e s a niltrace()	[rel_mng_nil]

In prior sections: bool 1 sqequal 1 list 1 rel 1 mb basic mb nat mb list 1 mb events mb tree mb list 2 mb automata 1 mb automata 2 prog 1

Try larger context: GenAutomata