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

At: rel mng 2 addprime 1 1
1. name: relname()
2. r1: Term List
3. rho: Top
4. ds: Top
5. da: Top
6. de: Top
7. e: Top
8. s: Top
9. s': Top
10. a: Top
11. tr: Top
12. u: Term
13. v: Term List
14. z:Top. list_accum(x,t.x([[t]] 1of(e) s s' a tr);z;map(t. (t)';v)) ~ list_accum(x,t.x([[t]] 1of(e) s' a tr);z;v)
15. z: Top

list_accum(x,t.x([[t]] 1of(e) s s' a tr);z([[(u)']] 1of(e) s s' a tr);map(t. (t)';v)) ~ list_accum(x,t.x([[t]] 1of(e) s' a tr);z([[u]] 1of(e) s' a tr);v)
By: Subst ([[(u)']] 1of(e) s s' a tr ~ [[u]] 1of(e) s' a tr) 0
Generated subgoals:

1 [[(u)']] 1of(e) s s' a tr ~ [[u]] 1of(e) s' a tr
2 list_accum(x,t.x([[t]] 1of(e) s s' a tr);z([[u]] 1of(e) s' a tr);map(t. (t)';v)) ~ list_accum(x,t.x([[t]] 1of(e) s' a tr);z([[u]] 1of(e) s' a tr);v)

About:
listlambdaapplysqequaltopall

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