is mentioned by

Thm* Q:Fmla. closed_pred((Q)') closed_pred(Q)	[closed_pred_addprime]
Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc(rel_unprime(r);ds;da;de)	[tc_unprime]
Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc((r)';ds;da;de)	[tc_addprime]
Thm* r:rel(), ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType) , de:sig(). ds1 = ds2 da1 = da2 (tc(r;ds1;da1;de) tc(r;ds2;da2;de))	[tc_functionality]
Thm* c:(LabelCollection(Term)), r,r':rel(). r' col_subst2(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst2(as;r))	[member_col_subst2]
Thm* Q:Fmla, A:ioa{i:l}(). covers_pred(A;(Q)') covers_pred(A;Q)	[covers_pred_addprime]
Thm* c:(LabelCollection(Term)), r,r':rel(). r' col_subst(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst(as;r))	[member_col_subst]
Thm* r:rel(). rel_mentions_trace(r) (i:. i < ||r.args|| & mentions_trace(r.args[i]))	[rel_mentions_trace_iff]
Thm* x:Label, r:rel(). (x rel_primed_vars(r)) (i:. i < ||r.args|| & (x term_primed_vars(r.args[i])))	[member_rel_primed_vars]
Thm* as:(LabelTerm) List. subst_mentions_trace(as) (i:||as||. mentions_trace(2of(as[i])))	[assert_subst_mentions_trace]
Thm* a,b:rel(). rel_eq(a;b) a = b	[assert_rel_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 mb automata 2 mb state machine

Try larger context: GenAutomata