(5steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: rel mng nil 1 1
1. name: relname()
2. r1: Term List
3. u: Term
4. v: Term List
5. te:(LabelLabel), rho,ds,da,de,e,s,a,x:Top. list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));x;v) ~ list_accum(x,t.x([[t]] 1of(e) s a niltrace());x;v)

te:(LabelLabel), rho,ds,da,de,e,s,a,x:Top. list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));x ([[u]] 1of(e) s a mk_trace_env(nil, te));v) ~ list_accum(x,t....;x (...);v)
By:
RepeatFor 8 ((ParallelOp -1) THEN (Thin -3))
THEN
Analyze 0
Generated subgoal:

15. te: LabelLabel
6. rho: Top
7. ds: Top
8. da: Top
9. de: Top
10. e: Top
11. s: Top
12. a: Top
13. x:Top. list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));x;v) ~ list_accum(x,t.x([[t]] 1of(e) s a niltrace());x;v)
14. x: Top
list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));x ([[u]] 1of(e) s a mk_trace_env(nil, te));v) ~ list_accum(x,t....;x (...);v)

About:
listnilboolapplyfunctionsqequaltopall

(5steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc