PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
enum
surj
1
1.
q:
2.
a:
l:
q*. enum(l) = a
By:
Inst
Thm*
q:
, a:
.
n:
.
(q
n
)
a <
(q
n+1
) [q;a]
THEN
Analyze 3
Generated subgoal:
1
3.
n:
4.
(q
n
)
a <
(q
n+1
)
l:
q*. enum(l) = a
About:
(q
n
) 
a < (qn+1)
l:q*. enum(l) = a
l:q*. enum(l) = a
q:, a:. n:. (qn) a < (qn+1)
[q;a]
(qn) a < (qn+1) l:q*. enum(l) = a
