is mentioned by

Thm* r:rel(), as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) rel_subst2(as;(r)') = rel_subst(as;r)	[rel_subst2_addprime]
Thm* t:Term, e,s,s',a1,a2,tr:Top. closed_term(t) ([[t]] e s s' a1 tr ~ [[t]] e s s' a2 tr)	[closed_term_mng2]
Thm* t:Term, e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)	[closed_term_mng]
Thm* x:Label, u:Term. (x term_primed_vars(u)) (x term_vars(u))	[term_primed_vars_term_vars]
Thm* t1,t2:Term. closed_term(t1 t2) closed_term(t1) & closed_term(t2)	[closed_tapp]
Thm* t:Term. term_primed_vars((t)') ~ term_vars(t)	[term_vars_addprime]
Thm* t:rel(). t.args Term List	[rel_args_wf]
Thm* u:Term, d:Decl, tr:trace_env(d), a:(d), e,s,v:Top. affects_trace(tr.proj;kind(a);u) ([[u]] e s v tappend(tr;a) ~ [[u]] e s v tr)	[term_mng_tappend]
Thm* a,b:Term List. a = b ||a|| = ||b|| (i:. i < ||a|| & a[i] = b[i])	[unequal_termlists]
Thm* u:Term, e,s,a,tr,tr':Top. mentions_trace(u) ([[u]] e s a tr' ~ [[u]] e s a tr)	[term_mng_static]
Thm* g:Label, t:Term. term_mentions_guard(g;t) mentions_trace(t)	[mentions_guard_mentions_trace]
Thm* a,b:Term List. termlist_eq(a;b) a = b	[assert_termlist_eq]
Thm* a,b:Term List. termlist_eq(a;b)	[termlist_eq_wf]
Thm* x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)	[term_subst2_addprime]
Thm* t:Term. term_free_vars((t)') ~ term_free_vars(t)	[term_free_vars_addprime]
Thm* t:Term, e,s,s',a,tr:Top. [[(t)']] e s s' a tr ~ [[t]] e s' a tr	[term_mng2_addprime]
Thm* t:Term, e,s,s',a,tr:Top. [[unprime(t)]] e s s' a tr ~ [[t]] e s a tr	[term_mng2_unprime]
Thm* t:Term, e,a,s,tr:Top. [[t]] e s a tr ~ [[unprime(t)]] e s a tr	[term_mng_unprime]
Thm* t:smt(). t.term Term	[smt_term_wf]
Thm* a,b:Term. term_eq(a;b) a = b	[assert_term_eq]
Thm* a,b:Term. term_eq(a;b)	[term_eq_wf]
Def rel() == relname()(Term List)	[rel]
Def smt_terms(c) == < s.term | s c >	[smt_terms]
Def col_map_subst(x.f(x);c) == < f(x) | x c >	[col_map_subst]
Def smt() == LabelTermSimpleType	[smt]

In prior sections: mb automata 1

Try larger context: GenAutomata