PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
surj
n:
, m:
, k:
(n
m).
l:
n*. ||l|| = m & en(l) = k
By:
Analyze 0
THEN
Analyze 0
THEN
NatInd 2
Generated subgoals:
1
1.
n:
k:
(n
0).
l:
n*. ||l|| = 0 & en(l) = k
2
1.
n:
2.
m:
3.
0 < m
4.
k:
(n
m-1).
l:
n*. ||l|| = m-1 & en(l) = k
k:
(n
m).
l:
n*. ||l|| = m & en(l) = k
About: