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* A:ioa{i:l}(), as:(LabelTerm) List, k:Label. ioa_mentions_trace(A) (i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))) subst_mentions_trace(as)	[effect_subst_mentions_trace]
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* d:Decl, tr:trace_env(d), a:(d), r:rel(), rho,ds,da,de,e,s,v:Top. affects_trace_rel(tr.proj;kind(a);r) ([[r]] rho ds da de e s v tappend(tr;a) ~ [[r]] rho ds da de e s v tr)	[rel_mng_tappend]
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]
Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label. tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List	[tproj_w_f]
Thm* as:(LabelTerm) List, g:Label, t:Term. subst_mentions_trace(as) term_mentions_guard(g;term_subst2(as;t)) term_mentions_guard(g;t)	[term_subst2_mentions_guard]
Thm* as:(LabelTerm) List, g:Label, t:Term. subst_mentions_trace(as) term_mentions_guard(g;term_subst(as;t)) term_mentions_guard(g;t)	[term_subst_mentions_guard]
Thm* as:(LabelTerm) List. subst_mentions_trace(as) (i:||as||. mentions_trace(2of(as[i])))	[assert_subst_mentions_trace]
Thm* a,b:rel(). rel_eq(a;b) a = b	[assert_rel_eq]
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]
Def guarded_trace(da;e;I) == r:rel(). r I (k:Label. affects_trace_rel(e;k;r) (t:dec(). t da & t.lbl = k))	[guarded_trace]
Def trace_consistent(rho;da;R;t) == g:Label. term_mentions_guard(g;t) subtype_rel(({a:([[da]] rho)| (R(g,kind(a))) } List); (rho(lbl_pr( < Trace, g > ))))	[trace_consistent]

In prior sections: bool 1 list 1 mb basic mb nat union mb list 1 mb label mb tree mb list 2 mb automata 1 mb automata 2 rel 1

Try larger context: GenAutomata