PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
mn
23
lem
0
1
2
1
1
2
1
2
1
1
1.
P:
Prop
2.
n:
3.
m:
4.
P(m)
5.
m < n
6.
i:
7.
0 < i
8.
i < m-n+2
9.
l:
(m-(i-1)+1)
10.
P(l)
11.
l < m-i+1
12.
i:
l. P(i)
l:
(m-i+1). P(l)
By:
Analyze 12
Generated subgoal:
1
12.
i1:
l
13.
P(i1)
l:
(m-i+1). P(l)
About:
l
l:(m-i+1). P(l)
Prop
m < n
(m-(i-1)+1)l < m-i+1i:l. P(i) l:(m-i+1). P(l)l l:(m-i+1). P(l)
