Nuprl - Proof: paren order1 2

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

1. T: Type

s1,s2:(T+T) List. (i:T, s1@0,s2:(T+T) List. s1 = (s1@0 @ [inl(i)] @ s2) (inr(i) s2)) (i:T, s1,s2@0:(T+T) List. s2 = (s1 @ [inl(i)] @ s2@0) (inr(i) s2@0)) paren(T;s1) paren(T;s2) (i:T, s1@0,s2@0:(T+T) List. (s1 @ s2) = (s1@0 @ [inl(i)] @ s2@0) (inr(i) s2@0))

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

Generated subgoals:

1 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) 12 steps

2 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@0 = (s1 @ e) & s2 = (e @ [inl(i)] @ s2@0)
(inr(i) s2@0) 1 step

About:

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

1	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)`	12 steps

2	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@0 = (s1 @ e) & s2 = (e @ [inl(i)] @ s2@0)` `(inr(i) s2@0)`	1 step