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* r:rel(), rho,ds,da,de,e,s,a,tr,tr':Top. rel_mentions_trace(r) ([[r]] rho ds da de e s a tr' ~ [[r]] rho ds da de e s a tr)	[rel_mng_static]
Thm* r:rel(). rel_mentions_trace(r) (i:. i < ||r.args|| & mentions_trace(r.args[i]))	[rel_mentions_trace_iff]
Def ioa_mentions_trace(A) == (e:eff(). e A.eff & mentions_trace(e.smt.term)) (p:pre(). p A.pre & rel_mentions_trace(p.rel)) (r:rel(). r A.init & rel_mentions_trace(r))	[ioa_mentions_trace]

Try larger context: GenAutomata