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

At: paren interval 2 1 1
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. [inl(x)] = (e @ e1)
19. s2 = (e1 @ s2@0 @ [inr(x)] @ s3)
paren(T;s2@0)
By: SingletonAppendD -2
Generated subgoals:

120. e = nil
21. e1 = [inl(x)]
paren(T;s2@0)		1 step
 
220. e1 = nil
21. e = [inl(x)]
paren(T;s2@0)		6 steps

About:
listconsnilunioninlinruniverseequalimpliesandall

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