PrintForm Definitions action sets Sections AutomataTheory Doc

At: pump thm cor 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:

(l:Alph*. ||l|| < k & (S:ls) = f) (l:Alph*. ||l||n & (S:ls) = f)
By: NatInd 8
Generated subgoals:

1 (l:Alph*. ||l|| < 0 & (S:ls) = f) (l:Alph*. ||l||n & (S:ls) = f)
28. k:
9. 0 < k
10. (l:Alph*. ||l|| < k-1 & (S:ls) = f) (l:Alph*. ||l||n & (S:ls) = f)
(l:Alph*. ||l|| < k & (S:ls) = f) (l:Alph*. ||l||n & (S:ls) = f)

About:
impliesexistslistandless_thanequaluniversenatural_number