Nuprl - Pf closed_rel

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

1. 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))
11. X: Top
12. (term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil

list_accum(x,t.x ([[t]] 1of(e) s s' a1 tr);X ([[u]] 1of(e) s s' a1 tr);v) ~ list_accum(x,t.x (...);...;v)

By: InstHyp [X([[u]] 1of(e) s s' a1 tr)] -3 THEN Try Trivial

Generated subgoals:

1 reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil

2 13. list_accum(x,t.x ([[t]] 1of(e) s s' a1 tr);X ([[u]] 1of(e) s s' a1 tr);v) ~ list_accum(x,t.x (...);...;v)
list_accum(x,t.x ([[t]] 1of(e) s s' a1 tr);X ([[u]] 1of(e) s s' a1 tr);v) ~ list_accum(x,t.x (...);...;v)

About:

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

1	`reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil`
2	13. `list_accum(x,t.x ([[t]] 1of(e) s s' a1 tr);X ([[u]] 1of(e) s s' a1 tr);v) ~ list_accum(x,t.x (...);...;v)` `list_accum(x,t.x ([[t]] 1of(e) s s' a1 tr);X ([[u]] 1of(e) s s' a1 tr);v) ~ list_accum(x,t.x (...);...;v)`