PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
enum
surj
1
1
3
1
1
1.
q:
2.
a:
3.
n:
4.
(q
n
)
a <
(q
n+1
)
5.
l:
q*
6.
||l|| = n & en(l) = a-
(q
n
)
enum(l) = a
By:
Unfold `enum` 0
Generated subgoal:
1
(q
||l||
)+en(l) = a
About:
(q
||l||
)+en(l) = a
(qn) 
a < (qn+1)q*(qn) enum(l) = a (q||l||)+en(l) = a
