Nuprl - Proof: paren order1 2 1 1 2

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

1. T: Type
2. s1: (T+T) List
3. s2: (T+T) List
4. i:T, s1@0,s2:(T+T) List. s1 = (s1@0 @ [inl(i) / s2]) (inr(i) s2)
5. i:T, s1,s2@0:(T+T) List. s2 = (s1 @ [inl(i) / s2@0]) (inr(i) s2@0)
6. paren(T;s1)
7. paren(T;s2)
8. i: T
9. s1@0: (T+T) List
10. s2@0: (T+T) List
11. (s1 @ s2) = (s1@0 @ [inl(i) / s2@0])
12. u: T+T
13. v: (T+T) List
14. s1 = (s1@0 @ [u / v])
15. [inl(i) / s2@0] = [u / (v @ s2)]
16. e1: (T+T) List
17. [inl(i)] = [u / (v @ e1)] & s2 = (e1 @ s2@0)

(inr(i) s2@0)

By: Auto THEN SplitCons -2

Generated subgoal:

1 17. s2 = (e1 @ s2@0)
18. inl(i) = u
19. nil = (v @ e1)
(inr(i) s2@0) 3 steps

About:

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