PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
pump
thm
cor
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.
l:Alph*. ||l|| < 0 & (S:l
s) = f
l:Alph*. ||l||
n & (S:l
s) = f
By:
Analyze 8
Generated subgoals:
None
About:
l:Alph*. (S:l
s) = fl:Alph*. ||l|| < 0 & (S:ls) = f
l:Alph*. ||l||
n & (S:ls) = f
