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* 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* x:Label, u:Term. (x term_primed_vars(u)) (x term_vars(u))	[term_primed_vars_term_vars]
Thm* t:qimp{i:l}(). t.lbl Label	[qimp_lbl_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.kind Label	[eff_kind_wf]
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]
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.var Label	[frame_var_wf]
Thm* t:smt(). t.lbl Label	[smt_lbl_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]
Def covers_rel(A;r) == x:Label. rel_mentions(r;x) covers_var(A;x)	[covers_rel]
Def closed_term(t) == term_free_vars(t) = nil	[closed_term]
Def eff() == LabelLabelSimpleTypesmt()	[eff]
Def qimp{i:l}() == LabelFmlaFmla	[qimp]
Def col_map_subst(x.f(x);c) == < f(x) | x c >	[col_map_subst]
Def rel_mentions(r;x) == i:. i < ||r.args|| & (x term_vars(r.args[i]))	[rel_mentions]
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 frame() == LabelSimpleType(Label List)	[frame]
Def relname() == SimpleType+Label	[relname]
Def smt() == LabelTermSimpleType	[smt]
Def dec() == LabelSimpleType	[dec]
Def sig() == (LabelSimpleType)(Label(SimpleType List))	[sig]
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: mb label mb declaration mb events mb automata 1 mb record

Try larger context: GenAutomata