Nuprl - Proof: paren order1 2 1

(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. e: (T+T) List
13. s1 = (s1@0 @ e) & ([inl(i)] @ s2@0) = (e @ s2)

(inr(i) s2@0)

By: Analyze -1 THEN FwdThru Thm* equal_appends [-1] THEN Analyze -1 THEN Analyze -1

Generated subgoals:

1 13. s1 = (s1@0 @ e)
14. ([inl(i)] @ s2@0) = (e @ s2)
15. e1: (T+T) List
16. [inl(i)] = (e @ e1) & s2 = (e1 @ s2@0)
(inr(i) s2@0) 7 steps

2 13. s1 = (s1@0 @ e)
14. ([inl(i)] @ s2@0) = (e @ s2)
15. e1: (T+T) List
16. e = ([inl(i)] @ e1) & s2@0 = (e1 @ s2)
(inr(i) s2@0) 4 steps

About:

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

1	13. `s1 = (s1@0 @ e)` 14. `([inl(i)] @ s2@0) = (e @ s2)` 15. `e1:` `(T+T) List` 16. `[inl(i)] = (e @ e1) & s2 = (e1 @ s2@0)` `(inr(i) s2@0)`	7 steps

2	13. `s1 = (s1@0 @ e)` 14. `([inl(i)] @ s2@0) = (e @ s2)` 15. `e1:` `(T+T) List` 16. `e = ([inl(i)] @ e1) & s2@0 = (e1 @ s2)` `(inr(i) s2@0)`	4 steps