PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
enum
surj
1
1
3
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
)
l:
q*. enum(l) = a
By:
Witness l
Generated subgoal:
1
enum(l) = a
About:
(q
n
) 
a < (qn+1)q*(qn)
l:q*. enum(l) = a enum(l) = a
