mb automata 3 Sections GenAutomata Doc

Def term_primed_vars(t) == iterate(statevar v- > nil statevar v'- > [v] funsymbol f- > nil freevar f- > nil trace(P)- > nil x(y)- > x @ y over t)

is mentioned by

Thm* x:Label, r:rel(). (x rel_primed_vars(r)) (i:. i < ||r.args|| & (x term_primed_vars(r.args[i])))[member_rel_primed_vars]
Thm* t:Term, s:SimpleType, as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(SimpleType), de:sig(). s term_types(ds;da;de;t) (x:Label. (x term_primed_vars(t)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) s term_types(ds;da;de;term_subst2(as;t))[term_subst2_tc]
Def rel_primed_vars(r) == reduce(t,vs. term_primed_vars(t) @ vs;nil;r.args)[rel_primed_vars]

In prior sections: mb automata 2

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc