(12steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
invariant
1
2
1
1
1
1
1.
a:
2.
n:
3.
b:
4.
0+1
b
5.
((a+(b-1)
n) rem n) = (a rem n)
6.
n
(0+1)
n
b
7.
n
(0+1)
n
b
a+b
n
n
By:
Analyze 1
Generated subgoal:
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
About:
(12steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc