(12steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
invariant
1
2
1
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
9.
0+n
(0+1)
a+n
b
a+b
n
n
By:
Auto
Generated subgoals:
None
About:
(12steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
0
b
n) rem n) = (a rem n)(0+1)nb(0+1)nb(0+1)a+nb
a+bnn
