Nuprl - Proof: paren interval 3 1 2 1

(60steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

1. T: Type
2. s: (T+T) List
3. t: T
4. no_repeats(T+T;s) (s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x) / (s2 @ [inr(x) / s3])]) paren(T;s2))
5. paren(T;s)
6. l_disjoint(T+T;[inl(t)];s @ [inr(t)])
7. no_repeats(T+T;[inl(t)])
8. l_disjoint(T+T;s;[inr(t)])
9. no_repeats(T+T;s)
10. no_repeats(T+T;[inr(t)])
11. u: T+T
12. v: (T+T) List
13. s2: (T+T) List
14. s3: (T+T) List
15. x: T
16. inl(t) = u
17. (s @ [inr(t)]) = (v @ [inl(x) / (s2 @ [inr(x) / s3])])
18. e: (T+T) List
19. s = (v @ e)
20. [inl(x) / (s2 @ [inr(x) / s3])] = (e @ [inr(t)])

paren(T;s2)

By: Analyze -3 THEN All Reduce THEN SplitCons -1

Generated subgoals:

1 18. s = (v @ nil)
19. inl(x) = inr(t) T+T
20. (s2 @ [inr(x) / s3]) = nil
paren(T;s2) 1 step

2 18. u1: T+T
19. v1: (T+T) List
20. s = (v @ [u1 / v1])
21. inl(x) = u1
22. (s2 @ [inr(x) / s3]) = (v1 @ [inr(t)])
paren(T;s2) 12 steps

About:

(60steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

1	18. `s = (v @ nil)` 19. `inl(x) = inr(t) T+T` 20. `(s2 @ [inr(x) / s3]) = nil` `paren(T;s2)`	1 step

2	18. `u1:` `T+T` 19. `v1:` `(T+T) List` 20. `s = (v @ [u1 / v1])` 21. `inl(x) = u1` 22. `(s2 @ [inr(x) / s3]) = (v1 @ [inr(t)])` `paren(T;s2)`	12 steps