Nuprl - mb_automata_1 Citations of term

Def [[t]] e s a tr == iterate(statevar x- > s.x statevar x'- > s.x funsymbol f- > e.f freevar x- > a trace(P)- > tr.P x(y)- > x(y) over t)

is mentioned by

Thm* u:Term, te:(LabelLabel), e,s,a:Top. [[u]] e s a mk_trace_env(nil, te) ~ [[u]] e s a niltrace() [term_mng_nil]

Try larger context: GenAutomata