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

At: closed rel mng sq 1 1 2
1. 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))
By: RepeatFor 2 (Analyze 0)
Generated subgoal:

110. X: Top
11. (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