mb automata 2 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 by

Thm* x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)[term_subst2_addprime]
Def rel_subst(as;r) == mk_rel(r.name, map(t.term_subst(as;t);r.args))[rel_subst]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc