(d)

rho,ds,da,de,e,s,v,x:Top. affects_trace_rel(tr.proj;kind(a); < name,r1 > ) (list_accum(x,t.x ([[t]] 1of(e) s v tappend(tr;a));x;r1) ~ list_accum(x,t.x ([[t]] 1of(e) s v tr);x;r1))

1

6. u: Term 7. v: Term List 8. rho,ds,da,de,e,s,v@0,x:Top. affects_trace_rel(tr.proj;kind(a);mk_rel(name, v)) (list_accum(x,t.x ([[t]] 1of(e) s v@0 tappend(tr;a));x;v) ~ list_accum(x,t....;x;v)) rho,ds,da,de,e,s,v@0,x:Top. affects_trace_rel(tr.proj;kind(a);mk_rel(name, [u / v])) (list_accum(x,t.x ([[t]] 1of(e) s v@0 tappend(tr;a));x ([[u]] 1of(e) s v@0 tappend(tr;a));v) ~ ...)

About: