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(), de:sig(), ds1,ds2:Collection(dec()) , da1,da2:Collection(SimpleType). ds1 ds2 da1 da2 tc(r;ds1;da1;de) tc(r;ds2;da2;de)	[tc_monotone]
Thm* r:rel(), as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) (x:Label. (x rel_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) tc(rel_subst(as;r);ds;da;de)	[rel_subst_tc]
Thm* r:rel(), as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) (x:Label. (x rel_primed_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) tc(rel_subst2(as;r);ds;da;de)	[rel_subst2_tc]
Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc(rel_unprime(r);ds;da;de)	[tc_unprime]
Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc((r)';ds;da;de)	[tc_addprime]
Thm* r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_rel(r) tc(r;ds;da1;de) tc(r;ds;da2;de)	[tc_closed_rel]
Thm* r:rel(), ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType) , de:sig(). ds1 = ds2 da1 = da2 (tc(r;ds1;da1;de) tc(r;ds2;da2;de))	[tc_functionality]
Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) Prop	[tc_wf]
Thm* r:rel(), I:Fmla, A:ioa{i:l}(), a:Label. covers_pred(A;I) r I (r':rel(). r' col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))	[covers_pred_lemma2]
Thm* c:(LabelCollection(Term)), r,r':rel(). r' col_subst2(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst2(as;r))	[member_col_subst2]
Thm* r:rel(), rho,ds,da1,da2,de,s,s',e,a1,a2,tr:Top. closed_rel(r) (rel_mng_2(r; rho; ds; da1; de; e; s; s'; a1; tr) ~ rel_mng_2 (r; rho; ds; da2; de; e; s; s'; a2; tr))	[closed_rel_mng2]
Thm* r:rel(), rho,ds,da,de,e,s,s',a,tr:Top. rel_mng_2(rel_unprime(r); rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s a tr	[rel_mng_2_unprime]
Thm* r:rel(), rho,ds,da,de,e,s,s',a,tr:Top. rel_mng_2((r)'; rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s' a tr	[rel_mng_2_addprime]
Thm* c:(LabelCollection(Term)), r:rel(). col_subst(c;r) Collection(rel())	[col_subst_wf_2]
Thm* c:(LabelCollection(Term)), r,r':rel(). r' col_subst(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst(as;r))	[member_col_subst]
Thm* A:ioa{i:l}(), I:Fmla, r:rel(). r I covers_pred(A;I) covers_rel(A;r)	[covers_pred_rel_member]
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(), rho,ds,da1,da2,de,s,e,a1,a2,tr:Top. closed_rel(r) ([[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr)	[closed_rel_mng_sq]
Thm* r:rel(). rel_mentions_trace(r) (i:. i < ||r.args|| & mentions_trace(r.args[i]))	[rel_mentions_trace_iff]
Thm* r:rel(), x:Label. (x rel_primed_vars(r)) (x rel_vars(r))	[rel_primed_vars_rel_vars]
Thm* r:rel(), i:. closed_rel(r) i < ||r.args|| closed_term(r.args[i])	[closed_rel_args]
Thm* r:rel(). rel_primed_vars((r)') = rel_vars(r)	[rel_vars_addprime]
Thm* x:Label, r:rel(). (x rel_primed_vars(r)) (i:. i < ||r.args|| & (x term_primed_vars(r.args[i])))	[member_rel_primed_vars]
Thm* r:rel(), e,a,s,ds,da,de,rho,tr:Top. [[r]] rho ds da de e s a tr ~ [[rel_unprime(r)]] rho ds da de e s a tr	[rel_mng_unprime]
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]
Thm* r:rel(), as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) rel_unprime(rel_subst(as;r)) = rel_unprime(r)	[trivial_rel_subst]
Thm* t:ioa{i:l}(). t.init Collection(rel())	[ioa_init_wf]
Thm* t:pre(). t.rel rel()	[pre_rel_wf]
Thm* a,b:rel(). rel_eq(a;b) a = b	[assert_rel_eq]
Def wp2(A;a;Q) == (rQ.col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))	[wp2]
Def pred_mng_2(p; rho; ds; da; de; e; s; s'; a; tr) == r:rel(). r p rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr)	[pred_mng_2]
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 closed_pred(p) == r:rel(). r p closed_rel(r)	[closed_pred]
Def [[p]] rho ds da de e s a tr == r:rel(). r p [[r]] rho ds da de e s a tr	[pred_mng]
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 (P)' == (rP. < (r)' > )	[pred_addprime]
Def pred_unprime(P) == < rel_unprime(r) | r P >	[pred_unprime]
Def ioa{i:l}() == Collection(dec())Collection(dec())Collection(rel())Collection(pre())Collection(eff()) Collection(frame())	[ioa]
Def pre() == LabelLabelrel()	[pre]

In prior sections: mb automata 2

Try larger context: GenAutomata