PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
pump
thm
cor
1
2
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*
8.
(S:l
s) = f
l@0:Alph*. ||l@0|| < ||l||+1 & (S:l@0
s) = f
By:
Witness l
Generated subgoal:
1
||l|| < ||l||+1 & (S:l
s) = f
About:
||l|| < ||l||+1 & (S:l
s) = f
s) = f 
l@0:Alph*. ||l@0|| < ||l||+1 & (S:l@0s) = f ||l|| < ||l||+1 & (S:ls) = f
