At: pump thm cor 1 1 1 2 1 1 1 1 2 1 1 1 1 1 1 1 1 1 1 1 1 1
1. n: 
2. Alph: Type
3. S: ActionSet(Alph)
4. s: S.car
5. f: S.car
6. #(S.car)=n
7. 
l:Alph*. (S:l
s) = f
8. k: 
9. 0 < k
10. l: Alph*
11. ||l|| < k
12. (S:ls) = f
13. 
||l||
n
14. a: Alph*
15. b: Alph*
16. c: Alph*
17. 0 < ||b||
18. l = ((a @ b) @ c)
19. (S:a @ cs) = (S:ls)
20. ||l|| = ||(a @ b) @ c|| 
||a||+||c|| < k-1
By: RWH
(LemmaC
Thm* 
as,bs:T*. ||as @ bs|| = ||as||+||bs||)
20
Generated subgoals:None
About:
