At:
trace consistent rel subst
2
1
1.
r: rel()
2.
as: (Label
Term) List
3.
daa: Collection(dec())
4.
rho: Decl
5.
te: Label
Label
6.
i:
||r.args||. trace_consistent(rho;daa;te;r.args[i])
7.
subst_mentions_trace(as)
8.
i: ||map(
t.term_subst(as;t);r.args)||
9.
g:Label.
term_mentions_guard(g;r.args[i])
((
[[ < d 
daa | te(g,d.lbl) > ]] rho) List) 
(rho(lbl_pr( < Trace, g > )))
10.
||map(t.term_subst(as;t);r.args)|| = ||r.args|| 
11.
g: Label
12.
term_mentions_guard(g;map(t.term_subst(as;t);r.args)[i])
13.
x,y:Term. x = y (x ~ y)
map(t.term_subst(as;t);r.args)[i] = term_subst(as;r.args[i])
By:
RWO "map_select" 0
THEN
Reduce 0
Generated subgoals:
None
About:
