Def ts_case(x)var(a)= > v(a)var'(b)= > p(b)opr(f)= > op(f)fvar(x)= > f(x)trace(P)= > t(P)end_ts_case == Case(x) Case ts_var(a) = > v(a) Case ts_pvar(b) = > p(b) Case ts_op(f) = > op(f) Case ts_fvar(x) = > f(x) Case ts_trace(P) = > t(P) Default = > 
is mentioned
In prior sections:
mb automata 1
