mb automata 3 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* ds,da:Collection(dec()), st:Collection(SimpleType), de:sig(), rho:Decl , e1:{1of([[de]] rho)}, s1,s2:{[[ds]] rho}, a:[[st]] rho, tr:trace_env([[da]] rho), u:Term , t:SimpleType. trace_consistent(rho;da;tr.proj;u) (x:Label. (x term_vars(u)) s1.x = s2.x) t term_types(ds;st;de;u) [[u]] e1 s1 a tr = [[u]] e1 s2 a tr [[t]] rho[term_mng_equal]
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_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_subst(as;t))[term_subst_tc]

In prior sections: mb automata 2

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc