r:rel(), te:(Label
Label
), rho,ds,da,de,e,s,a:Top.
[[r]] rho ds da de e s a mk_trace_env(nil, te) ~ [[r]] rho ds da de e s a niltrace()is mentioned by
|
Thm* r:rel(), te:(LabelLabel), rho,ds,da,de,e,s,a:Top.
[[r]] rho ds da de e s a mk_trace_env(nil, te) ~ [[r]] rho ds da de e s a niltrace() | [rel_mng_nil] |
In prior sections: mb automata 1
Try larger context: GenAutomata