is mentioned by

Def rel_free_vars(r) == reduce(t,vs. term_free_vars(t) @ vs;nil;r.args)	[rel_free_vars]
Def term_primed_vars(t) == iterate(statevar v- > nil statevar v'- > [v] funsymbol f- > nil freevar f- > nil trace(P)- > nil x(y)- > x @ y over t)	[term_primed_vars]
Def rel_vars(r) == reduce(t,vs. term_vars(t) @ vs;nil;r.args)	[rel_vars]
Def term_free_vars(t) == term_iterate(f.nil;f.nil;f.nil;v.[v];P.nil;x,y. x @ y;t)	[term_free_vars]

In prior sections: list 1 mb list 1 mb events mb list 2 mb automata 1

Try larger context: GenAutomata