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

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

F:Top. list_accum(x,t.x ([[t]] 1of(e) s a tr);F ([[u]] 1of(e) s a tr);v) ~ list_accum(x,t....;F (...);map(t. unprime(t);v))
By: Analyze 0
Generated subgoal:

114. F: Top
list_accum(x,t.x ([[t]] 1of(e) s a tr);F ([[u]] 1of(e) s a tr);v) ~ list_accum(x,t....;F (...);map(t. unprime(t);v))

About:
listlambdaapplysqequaltopall

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