is mentioned by

Thm* t1,t2:Term. closed_term(t1 t2) closed_term(t1) & closed_term(t2)	[closed_tapp]
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* 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. termlist_eq(a;b) a = b	[assert_termlist_eq]
Thm* ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds	[member_dec_lookup]
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]

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

Try larger context: GenAutomata