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