mb automata 2 Sections GenAutomata Doc

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

is mentioned by

Thm* x:Label, u:Term. (x term_primed_vars(u)) (x term_vars(u))[term_primed_vars_term_vars]
Thm* t:Term. term_primed_vars((t)') ~ term_vars(t)[term_vars_addprime]
Thm* x:Label, r:rel(). (x rel_vars(r)) (i:. i < ||r.args|| & (x term_vars(r.args[i])))[member_rel_vars]
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_mentions(r;x) == i:. i < ||r.args|| & (x term_vars(r.args[i]))[rel_mentions]
Def rel_vars(r) == reduce(t,vs. term_vars(t) @ vs;nil;r.args)[rel_vars]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc