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

At: paren interval 2 1 2
1. T: Type
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)
17. e1: (T+T) List
18. e = ([inl(x)] @ e1)
19. (s2@0 @ [inr(x)] @ s3) = (e1 @ s2)
paren(T;s2@0)
By:
EqualAppendsD -1
THEN
Analyze -1
Generated subgoals:

120. e2: (T+T) List
21. s2@0 = (e1 @ e2)
22. s2 = (e2 @ [inr(x)] @ s3)
paren(T;s2@0)		7 steps
 
220. e2: (T+T) List
21. e1 = (s2@0 @ e2)
22. ([inr(x)] @ s3) = (e2 @ s2)
paren(T;s2@0)		12 steps

About:
listconsnilunioninlinruniverseequalimpliesandall

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