PrintForm Definitions exponent Sections AutomataTheory Doc

At: en surj


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

By:
Analyze 0
THEN
Analyze 0
THEN
NatInd 2


Generated subgoals:

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


About:
allnatural_numberexistslistandequalint