Term) List
Label
i:
||r.args||. trace_consistent(rho;daa;te;r.args[i])
subst_mentions_trace(as)
||map(
t.term_subst(as;t);r.args)||
g:Label.
term_mentions_guard(g;r.args[i])
((
[[ < d 
daa | te(g,d.lbl) > ]] rho) List) 
(rho(lbl_pr( < Trace, g > )))
t.term_subst(as;t);r.args)|| = ||r.args|| 
term_mentions_guard(g;r.args[i])
as:(LabelTerm) List, g:Label, t:Term. subst_mentions_trace(as) term_mentions_guard(g;term_subst(as;t)) term_mentions_guard(g;t)
None
About:
| | | | | | | |
 |  |  |  |  |