PrintForm Definitions exponent Sections AutomataTheory Doc

At: en surj 2 1

1. n:
2. m:
3. 0 < m
4. k:(nm-1). l:n*. ||l|| = m-1 & en(l) = k
5. k: (nm)

l:n*. ||l|| = m & en(l) = k

By: Witness4 k n

Generated subgoals:

14. k: (nm)
0(k n)
24. k: (nm)
(k n) < (nm-1)
34. k: (nm)
5. l:n*. ||l|| = m-1 & en(l) = (k n)
l:n*. ||l|| = m & en(l) = k


About:
existslistnatural_numberandequal
intdivideless_thanallsubtract