is mentioned by

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* 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(), 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* v:Top, rho:Decl, x:Label. v [[ < > ]] rho(x)	[empty_decls_mng]
Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t)	[term_types_unprime]
Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)	[term_types_addprime]

In prior sections: mb events mb automata 1 mb automata 2 mb basic mb declaration

Try larger context: GenAutomata