PrintForm Definitions action sets Sections AutomataTheory Doc

At: pump thm cor 1 2 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*
8. (S:ls) = f
9. (l@0:Alph*. ||l@0|| < ||l||+1 & (S:l@0s) = f) (l:Alph*. ||l||n & (S:ls) = f)

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

1 l@0:Alph*. ||l@0|| < ||l||+1 & (S:l@0s) = f
29. l:Alph*. ||l||n & (S:ls) = f
l:Alph*. ||l||n & (S:ls) = f

About:
existslistandequaluniverse
impliesless_thanaddnatural_number