is mentioned by

Def mentions_trace(t) == iterate(statevar x- > false statevar x'- > false funsymbol x- > false freevar x- > false trace(P)- > true x(y)- > x y over t)	[mentions_trace]
Def termlist_eq(a;b) == Case of a; nil Case of b; nil true ; x.xs false ; x.xs Case of b; nil false ; x'.xs' term_eq(x;x')termlist_eq(xs;xs') (recursive)	[termlist_eq]

In prior sections: bool 1 sqequal 1 prog 1 mb basic mb list 2 list 1 union mb tree mb automata 1

Try larger context: GenAutomata