mb automata 2 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, 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]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc