Nuprl - Proof: paren order1 3 2 1 1

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

1. T: Type
2. s: (T+T) List
3. t: T
4. i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2)
5. paren(T;s)
6. i: T
7. s1: (T+T) List
8. s2: (T+T) List
9. ([inl(t)] @ s @ [inr(t)]) = (s1 @ [inl(i)] @ s2)
10. e: (T+T) List
11. s1 = ([inl(t)] @ e)
12. (s @ [inr(t)]) = (e @ [inl(i)] @ s2)
13. e1: (T+T) List
14. s = (e @ e1)
15. ([inl(i)] @ s2) = (e1 @ [inr(t)])
16. e2: (T+T) List
17. [inl(i)] = (e1 @ e2)
18. [inr(t)] = (e2 @ s2)

(inr(i) s2)

By: SingletonAppendD -2 THEN SingletonAppendD -3

Generated subgoals:

1 19. e1 = nil
20. e2 = [inl(i)]
21. e2 = nil
22. s2 = [inr(t)]
(inr(i) s2) 1 step

2 19. e1 = nil
20. e2 = [inl(i)]
21. s2 = nil
22. e2 = [inr(t)]
(inr(i) s2) 2 steps

3 19. e2 = nil
20. e1 = [inl(i)]
21. e2 = nil
22. s2 = [inr(t)]
(inr(i) s2) 4 steps

4 19. e2 = nil
20. e1 = [inl(i)]
21. s2 = nil
22. e2 = [inr(t)]
(inr(i) s2) 1 step

About:

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

1	19. `e1 = nil` 20. `e2 = [inl(i)]` 21. `e2 = nil` 22. `s2 = [inr(t)]` `(inr(i) s2)`	1 step

2	19. `e1 = nil` 20. `e2 = [inl(i)]` 21. `s2 = nil` 22. `e2 = [inr(t)]` `(inr(i) s2)`	2 steps

3	19. `e2 = nil` 20. `e1 = [inl(i)]` 21. `e2 = nil` 22. `s2 = [inr(t)]` `(inr(i) s2)`	4 steps

4	19. `e2 = nil` 20. `e1 = [inl(i)]` 21. `s2 = nil` 22. `e2 = [inr(t)]` `(inr(i) s2)`	1 step