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

At: paren interval 3 1
1. T: Type
2. s: (T+T) List
3. t: T
4. no_repeats(T+T;s) (s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))
5. paren(T;s)
6. l_disjoint(T+T;[inl(t)];s @ [inr(t)])
7. no_repeats(T+T;[inl(t)])
8. l_disjoint(T+T;s;[inr(t)])
9. no_repeats(T+T;s)
10. no_repeats(T+T;[inr(t)])
11. s1: (T+T) List
12. s2: (T+T) List
13. s3: (T+T) List
14. x: T
15. ([inl(t)] @ s @ [inr(t)]) = (s1 @ [inl(x)] @ s2 @ [inr(x)] @ s3)
paren(T;s2)
By:
Analyze -5
THEN
All Reduce
THEN
SplitCons -1
THEN
Try ((Reduce 0) THEN (Reduce 0) THEN (Unfold `label` 0))
Generated subgoals:

14. no_repeats(T+T;s) (s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x) / (s2 @ [inr(x) / s3])]) paren(T;s2))
5. paren(T;s)
6. l_disjoint(T+T;[inl(t)];s @ [inr(t)])
7. no_repeats(T+T;[inl(t)])
8. l_disjoint(T+T;s;[inr(t)])
9. no_repeats(T+T;s)
10. no_repeats(T+T;[inr(t)])
11. s2: (T+T) List
12. s3: (T+T) List
13. x: T
14. inl(t) = inl(x) T+T
15. (s @ [inr(t)]) = (s2 @ [inr(x) / s3])
paren(T;s2)		9 steps
 
24. no_repeats(T+T;s) (s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x) / (s2 @ [inr(x) / s3])]) paren(T;s2))
5. paren(T;s)
6. l_disjoint(T+T;[inl(t)];s @ [inr(t)])
7. no_repeats(T+T;[inl(t)])
8. l_disjoint(T+T;s;[inr(t)])
9. no_repeats(T+T;s)
10. no_repeats(T+T;[inr(t)])
11. u: T+T
12. v: (T+T) List
13. s2: (T+T) List
14. s3: (T+T) List
15. x: T
16. inl(t) = u
17. (s @ [inr(t)]) = (v @ [inl(x) / (s2 @ [inr(x) / s3])])
paren(T;s2)		16 steps

About:
listconsnilunioninlinruniverseequalimpliesall

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