PrintForm Definitions action sets Sections AutomataTheory Doc

At: pump thm cor 1 1 1 2 1 1 1 1 2 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:ls) = f
8. k:
9. 0 < k
10. (l:Alph*. ||l|| < k-1 & (S:ls) = f) (l:Alph*. ||l||n & (S:ls) = f)
11. l: Alph*
12. ||l|| < k
13. (S:ls) = f
14. ||l||n
15. a: Alph*
16. b: Alph*
17. c: Alph*
18. 0 < ||b|| & l = ((a @ b) @ c)
19. (S:a @ cs) = (S:ls)

l:Alph*. ||l||n & (S:ls) = f
By: Analyze 10
Generated subgoals:

110. l: Alph*
11. ||l|| < k
12. (S:ls) = f
13. ||l||n
14. a: Alph*
15. b: Alph*
16. c: Alph*
17. 0 < ||b|| & l = ((a @ b) @ c)
18. (S:a @ cs) = (S:ls)
l:Alph*. ||l|| < k-1 & (S:ls) = f
210. l: Alph*
11. ||l|| < k
12. (S:ls) = f
13. ||l||n
14. a: Alph*
15. b: Alph*
16. c: Alph*
17. 0 < ||b|| & l = ((a @ b) @ c)
18. (S:a @ cs) = (S:ls)
19. l:Alph*. ||l||n & (S:ls) = f
l:Alph*. ||l||n & (S:ls) = f

About:
existslistandequaluniverse
intless_thannatural_numberimpliessubtract