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

At: closed rel mng2 1 1
1. r: rel()
2. rho: Top
3. ds: Top
4. da1: Top
5. da2: Top
6. de: Top
7. s: Top
8. s': Top
9. e: Top
10. a1: Top
11. a2: Top
12. tr: Top
13. l: Term List
14. r.args = l
15. X: Top
16. [[r.name]] rho 2of(e) = X

reduce(t,vs. term_free_vars(t) @ vs;nil;l) = nil (list_accum(x,t.x([[t]] 1of(e) s s' a1 tr);X;l) ~ list_accum(x,t.x([[t]] 1of(e) s s' a2 tr);X;l))
By:
AllHyps Thin
THEN
MoveToConcl -1
THEN
ListInd -1
THEN
Reduce 0
Generated subgoals:

11. s: Top
2. s': Top
3. e: Top
4. a1: Top
5. a2: Top
6. tr: Top
7. l: Term List
X:Top. nil = nil Label List (X ~ X)
21. s: Top
2. s': Top
3. e: Top
4. a1: Top
5. a2: Top
6. tr: Top
7. l: Term List
8. u: Term
9. v: Term List
10. X:Top. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil (list_accum(x,t.x([[t]] 1of(e) s s' a1 tr);X;v) ~ list_accum(x,t.x([[t]] 1of(e) s s' a2 tr);X;v))
X:Top. (term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil ...

About:
listnillambdaapplyequalsqequaltopimpliesall

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