PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
enum
surj
1
1
3
1
1
1
1
1
1.
q:
2.
a:
3.
n:
4.
(q
n
)
a <
(q
n+1
)
5.
l:
q*
6.
||l|| = n
7.
en(l) = a-
(q
n
)
8.
||l|| = n
(q
||l||
)+en(l) = a
By:
RWH (HypC 8) 0
Generated subgoals:
None
About:
(q
n
) 
a < (qn+1)q*(qn)
(q||l||)+en(l) = a
