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