(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
addition
1
1
1
1
1
1
1.
i:
2.
j:
3.
n:
4.
0
(i rem n) & (i rem n) < n
5.
0
(j rem n) & (j rem n) < n
0
(i rem n)+(j rem n)
By:
Analyze 5
THEN
Analyze 4
Generated subgoal:
1
4.
0
(i rem n)
5.
(i rem n) < n
6.
0
(j rem n)
7.
(j rem n) < n
0
(i rem n)+(j rem n)
About:
(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc