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

At: rel mng nil 1 1 1
1. name: relname()
2. r1: Term List
3. u: Term
4. v: Term List
5. 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)
By:
Subst ([[u]] 1of(e) s a mk_trace_env(nil, te) ~ [[u]] 1of(e) s a niltrace()) 0
THEN
Easy
Generated subgoals:

None

About:
listnilboolapplyfunctionsqequaltopall

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