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

At: paren induction
T:Type, P:(((T+T) List)Prop). P(nil) (s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)) (s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])) (s:(T+T) List. paren(T;s) P(s))
By:
Unfold `guard` 0
THEN
MoveToConcl -1
THEN
LengthInd -1
THEN
RecUnfold `paren` -1
THEN
SplitOrHyps
THEN
ExRepD
Generated subgoals:

11. T: Type
2. P: ((T+T) List)Prop
3. P(nil)
4. s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)
5. s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])
6. n:
7. s: (T+T) List
8. s1:(T+T) List. ||s1|| < ||s|| paren(T;s1) P(s1)
9. s = nil
P(s)		1 step
 
21. T: Type
2. P: ((T+T) List)Prop
3. P(nil)
4. s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)
5. s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])
6. n:
7. s: (T+T) List
8. s1:(T+T) List. ||s1|| < ||s|| paren(T;s1) P(s1)
9. t: T
10. s': (T+T) List
11. s = ([inl(t)] @ s' @ [inr(t)])
12. paren(T;s')
P(s)		2 steps
 
31. T: Type
2. P: ((T+T) List)Prop
3. P(nil)
4. s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)
5. s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])
6. n:
7. s: (T+T) List
8. s1:(T+T) List. ||s1|| < ||s|| paren(T;s1) P(s1)
9. s': (T+T) List
10. s'': (T+T) List
11. ||s'|| < ||s||
12. ||s''|| < ||s||
13. s = (s' @ s'')
14. paren(T;s')
15. paren(T;s'')
P(s)		1 step

About:
listconsnilunioninlinrfunctionuniversepropimpliesall

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