Nuprl - Proof: paren interval 3 1 1 2

(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. s2: (T+T) List
12. s3: (T+T) List
13. x: T
14. inl(t) = inl(x) T+T
15. (s @ [inr(t)]) = (s2 @ [inr(x) / s3])
16. e: (T+T) List
17. s2 = (s @ e)
18. [inr(t)] = (e @ [inr(x) / s3])

paren(T;s2)

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

Generated subgoals:

1 16. s2 = (s @ nil)
17. inr(t) = inr(x) T+T
18. nil = s3
paren(T;s2) 1 step

2 16. u: T+T
17. v: (T+T) List
18. s2 = (s @ [u / v])
19. inr(t) = u
20. nil = (v @ [inr(x) / s3])
paren(T;s2) 1 step

About:

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

1	16. `s2 = (s @ nil)` 17. `inr(t) = inr(x) T+T` 18. `nil = s3` `paren(T;s2)`	1 step

2	16. `u:` `T+T` 17. `v:` `(T+T) List` 18. `s2 = (s @ [u / v])` 19. `inr(t) = u` 20. `nil = (v @ [inr(x) / s3])` `paren(T;s2)`	1 step