PrintForm Definitions exponent Sections AutomataTheory Doc

At: en surj 2 1 3 1

1. n:
2. m:
3. 0 < m
4. k: (nm)
5. l: n*
6. ||l|| = m-1 & en(l) = (k n)

l:n*. ||l|| = m & en(l) = k

By:
Inst Thm* a:, n:. 0(a rem n) & (a rem n) < n [k;n]
THEN
Witness (k rem n).l


Generated subgoal:

17. 0(k rem n) & (k rem n) < n
||(k rem n).l|| = m & en((k rem n).l) = k


About:
existslistnatural_numberandequalint
consremainderless_thansubtractdivide