mb automata 3 Sections GenAutomata Doc

Def < f(x) | x c > (y) == x:T. x c & y = f(x) T'

is mentioned by

Def col_subst2(c;r) == col_map_subst(as.rel_subst2(as;r); < zip(rel_primed_vars(r);s) | s col_list_prod(map(c;rel_primed_vars(r))) > )[col_subst2]
Def col_subst(c;r) == col_map_subst(as.rel_subst(as;r); < zip(rel_vars(r);s) | s col_list_prod(map(c;rel_vars(r))) > )[col_subst]
Def pred_unprime(P) == < rel_unprime(r) | r P > [pred_unprime]

In prior sections: mb collection mb automata 2

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc