d:Decl, tr:trace_env(d), a:(d), r:rel(), rho,ds,da,de,e,s,v:Top. affects_trace_rel(tr.proj;kind(a);r) ([[r]] rho ds da de e s v tappend(tr;a) ~ [[r]] rho ds da de e s v tr)

RepeatFor 4 (Analyze 0)
THEN
Analyze -1
THEN
Unfold `rel_mng` 0
THEN
Reduce 0
THEN
Assert (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;r1)))

1

1. d: Decl 2. tr: trace_env(d) 3. a: (d) 4. name: relname() 5. r1: Term List 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))

2

1. d: Decl 2. tr: trace_env(d) 3. a: (d) 4. name: relname() 5. r1: Term List 6. 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)) rho,ds,da,de,e,s,v:Top. affects_trace_rel(tr.proj;kind(a); < name,r1 > ) (list_accum(x,t.x ([[t]] 1of(e) s v tappend(tr;a));[[name]] rho 2of(e) ;r1) ~ ...)

About: