PrintForm Definitions exponent Sections AutomataTheory Doc

At: en surj 2 1 3 1 1 1

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

(k rem n)+en(l)n = k

By: RWH (HypC 7) 0

Generated subgoal:

1 (k rem n)+(k n)n = k


About:
equalintaddremaindermultiply
less_thannatural_numberlistsubtractdivide