Nuprl - Proof: paren interval 2

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

1. T: Type

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

By: Auto THEN RWO Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2) 8 THEN EqualAppendsD -1 THEN Analyze -1

Generated subgoals:

1 2. s1: (T+T) List
3. s2: (T+T) List
4. no_repeats(T+T;s1) (s1@0,s2,s3:(T+T) List, x:T. s1 = (s1@0 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))
5. no_repeats(T+T;s2) (s1,s2@0,s3:(T+T) List, x:T. s2 = (s1 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3) paren(T;s2@0))
6. paren(T;s1)
7. paren(T;s2)
8. l_disjoint(T+T;s1;s2) & no_repeats(T+T;s1) & no_repeats(T+T;s2)
9. s1@0: (T+T) List
10. s2@0: (T+T) List
11. s3: (T+T) List
12. x: T
13. (s1 @ s2) = (s1@0 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3)
14. e: (T+T) List
15. s1 = (s1@0 @ e)
16. ([inl(x)] @ s2@0 @ [inr(x)] @ s3) = (e @ s2)
paren(T;s2@0) 29 steps

2 2. s1: (T+T) List
3. s2: (T+T) List
4. no_repeats(T+T;s1) (s1@0,s2,s3:(T+T) List, x:T. s1 = (s1@0 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))
5. no_repeats(T+T;s2) (s1,s2@0,s3:(T+T) List, x:T. s2 = (s1 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3) paren(T;s2@0))
6. paren(T;s1)
7. paren(T;s2)
8. l_disjoint(T+T;s1;s2) & no_repeats(T+T;s1) & no_repeats(T+T;s2)
9. s1@0: (T+T) List
10. s2@0: (T+T) List
11. s3: (T+T) List
12. x: T
13. (s1 @ s2) = (s1@0 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3)
14. e: (T+T) List
15. s1@0 = (s1 @ e)
16. s2 = (e @ [inl(x)] @ s2@0 @ [inr(x)] @ s3)
paren(T;s2@0) 1 step

About:

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

1	2. `s1:` `(T+T) List` 3. `s2:` `(T+T) List` 4. `no_repeats(T+T;s1) (s1@0,s2,s3:(T+T) List, x:T. s1 = (s1@0 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))` 5. `no_repeats(T+T;s2) (s1,s2@0,s3:(T+T) List, x:T. s2 = (s1 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3) paren(T;s2@0))` 6. `paren(T;s1)` 7. `paren(T;s2)` 8. `l_disjoint(T+T;s1;s2) & no_repeats(T+T;s1) & no_repeats(T+T;s2)` 9. `s1@0:` `(T+T) List` 10. `s2@0:` `(T+T) List` 11. `s3:` `(T+T) List` 12. `x:` `T` 13. `(s1 @ s2) = (s1@0 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3)` 14. `e:` `(T+T) List` 15. `s1 = (s1@0 @ e)` 16. `([inl(x)] @ s2@0 @ [inr(x)] @ s3) = (e @ s2)` `paren(T;s2@0)`	29 steps

2	2. `s1:` `(T+T) List` 3. `s2:` `(T+T) List` 4. `no_repeats(T+T;s1) (s1@0,s2,s3:(T+T) List, x:T. s1 = (s1@0 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))` 5. `no_repeats(T+T;s2) (s1,s2@0,s3:(T+T) List, x:T. s2 = (s1 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3) paren(T;s2@0))` 6. `paren(T;s1)` 7. `paren(T;s2)` 8. `l_disjoint(T+T;s1;s2) & no_repeats(T+T;s1) & no_repeats(T+T;s2)` 9. `s1@0:` `(T+T) List` 10. `s2@0:` `(T+T) List` 11. `s3:` `(T+T) List` 12. `x:` `T` 13. `(s1 @ s2) = (s1@0 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3)` 14. `e:` `(T+T) List` 15. `s1@0 = (s1 @ e)` 16. `s2 = (e @ [inl(x)] @ s2@0 @ [inr(x)] @ s3)` `paren(T;s2@0)`	1 step