(11steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: rel mng tappend 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) ~ ...)
By:
Repeat ((ParallelOp -1) THEN (Thin -3))
THEN
SimpleInstHyp [[name]] rho 2of(e) -1
THEN
NthHyp -1
Generated subgoals:

None

About:
pairlistassertapplysqequaltopimpliesall

(11steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc