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* v:vc{i:l}(). vc_concl(v) Fmla	[vc_concl_wf]
Thm* v:vc{i:l}(). vc_hyp(v) Fmla	[vc_hyp_wf]
Thm* r:rel(). rel_free_vars((r)') = rel_free_vars(r)	[rel_free_vars_addprime]
Thm* p:Fmla, x:Label. pred_mentions(p;x) Prop	[pred_mentions_wf]
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* rho:Decl, d:dec(). [[d]] rho Decl	[dec_mng_wf]
Thm* t:qimp{i:l}(). t.concl Fmla	[qimp_concl_wf]
Thm* t:qimp{i:l}(). t.hyp Fmla	[qimp_hyp_wf]
Thm* t:qimp{i:l}(). t.lbl Label	[qimp_lbl_wf]
Thm* t:imp{i:l}(). t.concl Fmla	[imp_concl_wf]
Thm* t:imp{i:l}(). t.hyp Fmla	[imp_hyp_wf]
Thm* l:SimpleType List, rho:Decl{i}. [[l]] rho{i} Type{i'}	[st_list_mng_wf]
Thm* r:rel(), x:Label. rel_mentions(r;x) (x rel_vars(r))	[rel_mentions_iff]
Thm* x:Label, r:rel(). (x rel_vars(r)) (i:. i < ||r.args|| & (x term_vars(r.args[i])))	[member_rel_vars]
Thm* t:eff(). t.smt smt()	[eff_smt_wf]
Thm* t:eff(). t.typ SimpleType	[eff_typ_wf]
Thm* t:eff(). t.kind Label	[eff_kind_wf]
Thm* sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho	[sts_mng_functionality]
Thm* t:SimpleType, rho:Decl, v:[[t]] rho. v [[ < t > ]] rho	[sts_mng_singleton]
Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType. s sts v [[s]] rho	[sts_mng_subtype]
Thm* v:Top, rho:Decl. v [[ < > ]] rho	[empty_sts_mng]
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* t:rel(). t.args Term List	[rel_args_wf]
Thm* t:rel(). t.name relname()	[rel_name_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* c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1)	[member_st_app]
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* 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]
Thm* ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds	[member_dec_lookup]
Thm* t:frame(). t.acts Label List	[frame_acts_wf]
Thm* t:frame(). t.typ SimpleType	[frame_typ_wf]
Thm* t:frame(). t.var Label	[frame_var_wf]
Thm* a,b:relname(). eq_relname(a;b) a = b	[assert_eq_relname]
Thm* a,b:relname(). eq_relname(a;b)	[eq_relname_wf]
Thm* t:smt(). t.typ SimpleType	[smt_typ_wf]
Thm* t:smt(). t.term Term	[smt_term_wf]
Thm* t:smt(). t.lbl Label	[smt_lbl_wf]
Thm* t:dec(). t.typ SimpleType	[dec_typ_wf]
Thm* t:dec(). t.lbl Label	[dec_lbl_wf]
Thm* t:sig(). t.rel Label(SimpleType List)	[sig_rel_wf]
Thm* t:sig(). t.fun LabelSimpleType	[sig_fun_wf]
Thm* s1,s2,s:SimpleType. s st_app1(s1;s2) st_eq(s1;s2s)	[member_st_app1]
Thm* s1,s2:SimpleType. st_app1(s1;s2) Collection(SimpleType)	[st_app1_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 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 declaration mb record mb events mb collection mb tree mb list 2 mb automata 1

Try larger context: GenAutomata