PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
3
1
1
1
1
1
1
1
1
1
1
1
1
2
1.
n:
2.
m:
3.
a3:
4.
0
a3 < n
5.
a4:
6.
0
a4 < m
7.
a5:
8.
0
a5 < n
9.
a6:
10.
0
a6 < m
11.
a3
m+a4 = a5
m+a6
(n
m)
a4 = a6
m
By:
Inst
Thm*
a:
, b:
. |a| < |b|
(a rem b) = a [a4;m]
Generated subgoals:
1
4.
0
a3
5.
a3 < n
6.
a4:
7.
0
a4
8.
a4 < m
9.
a5:
10.
0
a5
11.
a5 < n
12.
a6:
13.
0
a6
14.
a6 < m
15.
a3
m+a4 = a5
m+a6
(n
m)
|a4| < |m|
2
12.
(a4 rem m) = a4
a4 = a6
m
About: