PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
enum
surj
1
1
1.
q:
2.
a:
3.
n:
4.
(q
n
)
a <
(q
n+1
)
l:
q*. enum(l) = a
By:
Inst
Thm*
n:
, m:
, k:
(n
m).
l:
n*. ||l|| = m & en(l) = k [q;n;a-
(q
n
)]
Generated subgoals:
1
4.
(q
n
)
a
5.
a <
(q
n+1
)
0
a-
(q
n
)
2
4.
(q
n
)
a
5.
a <
(q
n+1
)
a-
(q
n
) < (q
n)
3
5.
l:
q*. ||l|| = n & en(l) = a-
(q
n
)
l:
q*. enum(l) = a
About: