PrintForm Definitions exponent Sections AutomataTheory Doc

At: enum surj 1 1

1. q:
2. a:
3. n:
4. (qn) a < (qn+1)

l:q*. enum(l) = a

By: Inst Thm* n:, m:, k:(nm). l:n*. ||l|| = m & en(l) = k [q;n;a-(qn)]

Generated subgoals:

14. (qn)a
5. a < (qn+1)
0a-(qn)
24. (qn)a
5. a < (qn+1)
a-(qn) < (qn)
35. l:q*. ||l|| = n & en(l) = a-(qn)
l:q*. enum(l) = a


About:
existslistnatural_numberequalint
allandsubtractaddless_than