PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
3
1
2
1
1
1
2
1
1
1
1
1
1
1.
n:
2.
m:
3.
b:
4.
0
b
5.
(b
m)
m+(b rem m) < n
m
6.
b = (b
m)
m+(b rem m)
7.
0
(b rem m)
8.
(b rem m) < m
(b
m) < n
By:
Inst Thm*
i,j:
. i
j
-i
-j [b rem m;0]
Generated subgoal:
1
9.
(b rem m)
0
-(b rem m)
-0
(b
m) < n
About:
0 
-(b rem m)
-0
(b 
m) < n
b m)
m+(b rem m) < nm m)m+(b rem m)(b rem m) (b m) < n
i,j:. ij -i-j [b rem m;0]0 -(b rem m)-0 (b m) < n
