(12steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
invariant
1
2
1
1
1
1
1
1.
a:
2.
a
0
3.
n:
4.
b:
5.
0+1
b
6.
((a+(b-1)
n) rem n) = (a rem n)
7.
n
(0+1)
n
b
8.
n
(0+1)
n
b
a+b
n
n
By:
FwdThru
Thm*
i1,i2,j1,j2:
. i1
j1
i2
j2
i1+i2
j1+j2 [2;7]
Generated subgoal:
1
9.
0+n
(0+1)
a+n
b
a+b
n
n
About:
(12steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
(0+1)
a+nb
a+bn
n
0
bn) rem n) = (a rem n)(0+1)nb(0+1)nb a+bnn
i1,i2,j1,j2:. i1j1 
i2j2 i1+i2j1+j2
[2;7](0+1)a+nb a+bnn
