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

At: rel mng tappend 1 1
1. d: Decl
2. tr: trace_env(d)
3. a: (d)
4. name: relname()
5. r1: Term List
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) ~ ...)
By:
RepeatFor 7 ((ParallelOp -1) THEN (Thin -3))
THEN
Analyze 0
THEN
Analyze 0
Generated subgoal:

18. rho: Top
9. ds: Top
10. da: Top
11. de: Top
12. e: Top
13. s: Top
14. v@0: Top
15. 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))
16. x: Top
17. 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:
listconsassertapplysqequaltopimpliesall

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