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

At: closed rel mng sq 1 1
1. r: rel()
2. rho: Top
3. ds: Top
4. da1: Top
5. da2: Top
6. de: Top
7. s: Top
8. e: Top
9. a1: Top
10. a2: Top
11. tr: Top
12. l: Term List
13. r.args = l
14. X: Top
15. [[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 a1 tr);X;l) ~ list_accum(x,t.x([[t]] 1of(e) s a2 tr);X;l))
By:
AllHyps Thin
THEN
MoveToConcl -1
THEN
ListInd -1
THEN
Reduce 0
Generated subgoals:

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

About:
listnillambdaapplyequalsqequaltopimpliesall

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