mb automata 1 Sections GenAutomata Doc

Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive)

is mentioned by

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)[term_vars]
Def tappend(tr;a) == mk_trace_env(tr.trace @ [a], tr.proj)[tappend]

In prior sections: list 1 mb list 1 mb events mb list 2

Try larger context: GenAutomata

mb automata 1 Sections GenAutomata Doc