PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
surj
2
1
3
1
1.
n:
2.
m:
3.
0 < m
4.
k:
(n
m)
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:
1
7.
0
(k rem n) & (k rem n) < n
||(k rem n).l|| = m & en((k rem n).l) = k
About: