PrintForm Definitions exponent Sections AutomataTheory Doc

At: en surj 2 1 3 1 1

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

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

By:
RecUnfold `en` 0
THEN
Reduce 0


Generated subgoal:

16. ||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


About:
andequalintconsremainderless_than
natural_numberlistsubtractdivideaddmultiply