Nuprl - Pf closed_rel_mng

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

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. closed_rel(r)

[[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr

By: MoveToConcl -1 THEN Unfolds [`closed_rel`;`rel_mng`] 0 THEN Unfold `rel_free_vars` 0 THEN GenConcl (r.args = l) THEN GenConcl ([[r.name]] rho 2of(e) = X)

Generated subgoal:

1 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))

About:

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