PrintForm Definitions exponent Sections AutomataTheory Doc

At: en surj 2 1 3

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

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

By: Analyze 5

Generated subgoal:

15. l: n*
6. ||l|| = m-1 & en(l) = (k n)
l:n*. ||l|| = m & en(l) = k


About:
existslistnatural_numberandequal
intless_thansubtractdivide