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

At: rel mng static 1 1
1. name: relname()
2. r1: Term List
3. u: Term
4. v: Term List
5. rho,ds,da,de,e,s,a,tr,tr',x:Top. rel_mentions_trace(mk_rel(name, v)) (list_accum(x,t.x([[t]] 1of(e) s a tr');x;v) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);x;v))

rho,ds,da,de,e,s,a,tr,tr',x:Top. rel_mentions_trace(mk_rel(name, [u / v])) (list_accum(x,t.x ([[t]] 1of(e) s a tr');x ([[u]] 1of(e) s a tr');v) ~ list_accum(x,t....;x (...);v))
By:
RepeatFor 9 ((ParallelOp -1) THEN (Thin -3))
THEN
Analyze 0
THEN
Analyze 0
Generated subgoal:

15. rho: Top
6. ds: Top
7. da: Top
8. de: Top
9. e: Top
10. s: Top
11. a: Top
12. tr: Top
13. tr': Top
14. x:Top. rel_mentions_trace(mk_rel(name, v)) (list_accum(x,t.x([[t]] 1of(e) s a tr');x;v) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);x;v))
15. x: Top
16. rel_mentions_trace(mk_rel(name, [u / v]))
list_accum(x,t.x ([[t]] 1of(e) s a tr');x ([[u]] 1of(e) s a tr');v) ~ list_accum(x,t....;x (...);v)

About:
listconsassertapplysqequaltopimpliesall

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