is mentioned by

Def affects_trace(e;k;t) == iterate(statevar x- > false statevar x'- > false funsymbol x- > false freevar x- > false trace(P)- > e(P,k) x(y)- > x y over t)	[affects_trace]
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]
Def eq_relname(a;b) == Case(a) Case eq(x) = > Case(b) Case eq(x') = > st_eq(x;x') Case x' = > false Default = > false Case x = > Case(b) Case eq(x') = > false Case x' = > x = x' Default = > false Default = > false	[eq_relname]
Def term_eq(a;b) == Case(a) Case x;y = > Case(b) Case x';y' = > term_eq(x;x')term_eq(y;y') Case tree_leaf(x) = > false Default = > True Case tree_leaf(x) = > Case(b) Case x';y' = > false Case tree_leaf(x') = > (x=x') Default = > True Default = > True (recursive)	[term_eq]
Def term_mentions_guard(g;t) == term_iterate(x.false;x.false;x.false;x.false;x.x = g;x,y. x y;t)	[term_mentions_guard]

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

Try larger context: GenAutomata