Nuprl - Pf closed rel mng 2 1 2 2 2 1 1 1

(24steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1. r: rel()
2. rho: Decl
3. ds: Collection(dec())
4. daa: Collection(dec())
5. da1: Collection(SimpleType)
6. da2: Collection(SimpleType)
7. de: sig()
8. s: {[[ds]] rho}
9. e: {[[de]] rho}
10. a1: Top
11. a2: Top
12. tr: trace_env([[daa]] rho)
13. trace_consistent_rel(rho;daa;tr.proj;r)
14. tc(r;ds;da1;de)
15. tc(r;ds; < > ;de) & a1 [[ < > ]] rho & a2 [[ < > ]] rho
16. aa: Term List
17. u: Term
18. v: Term List
19. xx:Top. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil (list_accum(x,t.x([[t]] 1of(e) s a2 tr);xx;v) ~ list_accum(x,t.x([[t]] 1of(e) s a1 tr);xx;v))

xx: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 a2 tr);xx([[u]] 1of(e) s a2 tr);v) ~ list_accum(x,t.x([[t]] 1of(e) s a1 tr);xx([[u]] 1of(e) s a1 tr);v))

By: Analyze 0 THEN Analyze 0 THEN Subst ((xx([[u]] 1of(e) s a2 tr)) ~ (xx([[u]] 1of(e) s a1 tr))) 0

Generated subgoals:

1 20. xx: Top
21. (term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil
(xx([[u]] 1of(e) s a2 tr)) ~ (xx([[u]] 1of(e) s a1 tr))

2 20. xx: Top
21. (term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil
list_accum(x,t.x([[t]] 1of(e) s a2 tr);xx([[u]] 1of(e) s a1 tr);v) ~ list_accum(x,t.x([[t]] 1of(e) s a1 tr);xx([[u]] 1of(e) s a1 tr);v)

About:

(24steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1	20. `xx:` `Top` 21. `(term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil` `(xx([[u]] 1of(e) s a2 tr)) ~ (xx([[u]] 1of(e) s a1 tr))`
2	20. `xx:` `Top` 21. `(term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil` `list_accum(x,t.x([[t]] 1of(e) s a2 tr);xx([[u]] 1of(e) s a1 tr);v) ~ list_accum(x,t.x([[t]] 1of(e) s a1 tr);xx([[u]] 1of(e) s a1 tr);v)`