Nuprl - Proof: paren interval 2 1 1 2 1 2

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

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. 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) s2)

By: BackThru Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s')) THEN SubstFor s2 0

Generated subgoal:

1 (inr(x) e1 @ s2@0 @ [inr(x)] @ s3) 1 step

About:

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