Nuprl - Proof: paren interval 3

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

1. T: Type

s:(T+T) List, t:T. (no_repeats(T+T;s) (s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))) paren(T;s) no_repeats(T+T;[inl(t)] @ s @ [inr(t)]) (s1,s2,s3:(T+T) List, x:T. ([inl(t)] @ s @ [inr(t)]) = (s1 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))

By: Auto THEN RWO Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2) 6 THEN RWO Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2) 8

Generated subgoal:

1 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) 26 steps

About:

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