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

At: paren interval 2 1 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. [inl(x)] = (e @ e1)
19. s2 = (e1 @ s2@0 @ [inr(x)] @ s3)
20. e1 = nil
21. e = [inl(x)]
paren(T;s2@0)
By:
Auto
THEN
AllHyps (h.(Unfold `l_disjoint` h) THEN (InstHyp [inl(x)] h) THEN (Analyze -1))
Generated subgoal:

18. x:T+T. ((x s1) & (x s2))
9. no_repeats(T+T;s1)
10. no_repeats(T+T;s2)
11. s1@0: (T+T) List
12. s2@0: (T+T) List
13. s3: (T+T) List
14. x: T
15. (s1 @ s2) = (s1@0 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3)
16. e: (T+T) List
17. s1 = (s1@0 @ e)
18. ([inl(x)] @ s2@0 @ [inr(x)] @ s3) = (e @ s2)
19. e1: (T+T) List
20. [inl(x)] = (e @ e1)
21. s2 = (e1 @ s2@0 @ [inr(x)] @ s3)
22. e1 = nil
23. e = [inl(x)]
(inl(x) s1) & (inl(x) s2)		5 steps

About:
listconsnilunioninlinruniverseequalimpliesandall

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