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