is mentioned by

Thm* r:rel(). rel_mentions_trace(r) (i:. i < ||r.args|| & mentions_trace(r.args[i]))	[rel_mentions_trace_iff]
Thm* r:rel(), i:. closed_rel(r) i < ||r.args|| closed_term(r.args[i])	[closed_rel_args]
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]
Def trace_consistent_rel(rho;da;R;r) == i:||r.args||. trace_consistent(rho;da;R;r.args[i])	[trace_consistent_rel]
Def tc(r;ds;da;de) == Case(r.name) Case eq(Q) = > ||r.args|| = 2 & Q term_types(ds;da;de;r.args[0]) & Q term_types(ds;da;de;r.args[1]) Case R = > ||de.rel(R)|| = ||r.args|| & (i:. i < ||r.args|| (de.rel(R))[i] term_types(ds;da;de;r.args[i])) Default = > False	[tc]
Def rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr) == list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[r.name]] rho 2of(e) ;r.args)	[rel_mng_2]
Def affects_trace_rel(e;k;r) == reduce(x,y. affects_trace(e;k;x) y;false;r.args)	[affects_trace_rel]
Def rel_mentions_trace(r) == reduce(x,y. mentions_trace(x) y;false;r.args)	[rel_mentions_trace]
Def rel_primed_vars(r) == reduce(t,vs. term_primed_vars(t) @ vs;nil;r.args)	[rel_primed_vars]
Def [[r]] rho ds da de e s a tr == list_accum(x,t.x([[t]] 1of(e) s a tr);[[r.name]] rho 2of(e) ;r.args)	[rel_mng]
Def rel_eq(a;b) == eq_relname(a.name;b.name)termlist_eq(a.args;b.args)	[rel_eq]

In prior sections: mb automata 2 mb automata 1

Try larger context: GenAutomata