mb automata 4 Sections GenAutomata Doc

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)

is mentioned

In prior sections: mb automata 2 mb automata 3

Try larger context: GenAutomata

mb automata 4 Sections GenAutomata Doc