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

At: rel mng unprime 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

list_accum(x,t.x ([[t]] 1of(e) s a tr);[[name]] rho 2of(e) ;r1) ~ list_accum(x,t....;...;map(t. unprime(t);r1))
By: (GenConcl ([[name]] rho 2of(e) = F)) THENA (Auto THEN (Try (Unfold `top` 0)))
Generated subgoal:

111. F: Top
12. [[name]] rho 2of(e) = F
list_accum(x,t.x([[t]] 1of(e) s a tr);F;r1) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);F;map(t. unprime(t);r1))

About:
listlambdaapplyequalsqequaltop

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