is mentioned by

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* 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:relname(). eq_relname(a;b) a = b	[assert_eq_relname]
Thm* s1,s2,s:SimpleType. s st_app1(s1;s2) st_eq(s1;s2s)	[member_st_app1]
Thm* a,b:Term. term_eq(a;b) a = b	[assert_term_eq]
Def smts_eff(ss;x) == smt_terms( < s ss | s.lbl = x > )	[smts_eff]
Def action_effect(a;es;fs) == < e.smt | e < e es | e.kind = a > > + < mk_smt(f.var, f.var, f.typ) | f < f fs | a f.acts > >	[action_effect]
Def dec_lookup(ds;x) == < d.typ | d < d ds | d.lbl = x > >	[dec_lookup]
Def action_pre(a;ps) == < p.rel | p < p ps | p.kind = a > >	[action_pre]
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: bool 1 list 1 mb basic mb nat union mb list 1 mb label mb tree mb list 2 mb automata 1 rel 1

Try larger context: GenAutomata