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* sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho	[sts_mng_functionality]
Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType. s sts v [[s]] rho	[sts_mng_subtype]
Thm* r:rel(), de:sig(), i:. tc1(r;de) i < ||r.args|| rel_arg_typ(r.name;i;de) SimpleType	[rel_arg_typ_wf]
Thm* a1,a2,b1,b2:Collection(SimpleType). a1 = a2 b1 = b2 st_app(a1;b1) = st_app(a2;b2)	[st_app_functionality]
Thm* a1,a2,b1,b2:Collection(SimpleType). a1 a2 b1 b2 st_app(a1;b1) st_app(a2;b2)	[st_app_monotone]
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* 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* x:Label, a1,a2:Collection(dec()). a1 a2 dec_lookup(a1;x) dec_lookup(a2;x)	[dec_lookup_monotone]
Thm* ds1,ds2:Collection(dec()), x:Label. ds1 = ds2 dec_lookup(ds1;x) = dec_lookup(ds2;x)	[dec_lookup_functionality]
Def covers_rel(A;r) == x:Label. rel_mentions(r;x) covers_var(A;x)	[covers_rel]
Def single_valued_decls(c) == x:Label, t1,t2:SimpleType. mk_dec(x, t1) c mk_dec(x, t2) c t1 = t2	[single_valued_decls]
Def covers_var(A;x) == fr:frame(). fr < fr A.frame | fr.var = x > & (a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > ))	[covers_var]

In prior sections: core fun 1 well fnd int 1 bool 1 sqequal 1 int 2 list 1 prog 1 rel 1 mb basic mb nat union num thy 1 mb list 1 mb label mb collection mb tree mb list 2 mb automata 1

Try larger context: GenAutomata