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