is mentioned by

Def term_subst2(as;t) == iterate(statevar v- > v statevar v'- > apply_alist(as;v;v') funsymbol f- > f freevar f- > f trace(P)- > trace(P) x(y)- > x y over t)	[term_subst2]
Def action_effect(a;es;fs) == < e.smt | e < e es | e.kind = a > > + < mk_smt(f.var, f.var, f.typ) | f < f fs | a f.acts > >	[action_effect]
Def term_subst(as;t) == iterate(statevar v- > apply_alist(as;v;v) statevar v'- > apply_alist(as;v;v') funsymbol f- > f freevar f- > f trace(P)- > trace(P) x(y)- > x y over t)	[term_subst]
Def unprime(t) == term_iterate(x.x;x.x;op.op;f.f;P.trace(P);a,b. a b;t)	[unprime]

Try larger context: GenAutomata