At:
rem add22
1.
x:
2.
y:
3.
n:
4.
x = (x n)n+(x rem n)
5.
|x rem n| < |n|
6.
(x rem n) < 0 x < 0
7.
(x rem n) > 0 x > 0
8.
y = (y n)n+(y rem n)
9.
|y rem n| < |n|
10.
(y rem n) < 0 y < 0
11.
(y rem n) > 0 y > 0
12.
(x rem n)+(y rem n) = (((x rem n)+(y rem n)) n)n+(((x rem n)+(y rem n)) rem n)
13.
|((x rem n)+(y rem n)) rem n| < |n|
14.
(((x rem n)+(y rem n)) rem n) < 0 (x rem n)+(y rem n) < 0
15.
(((x rem n)+(y rem n)) rem n) > 0 (x rem n)+(y rem n) > 0
16.
x+y = 0
|(((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi| < |n|
By:
MoveToConcl -4
THEN
Unfold `absval` 0
THEN
RepeatFor 2 SplitOnConclITE
THEN
AutoBoolCase (x+y < 0)
THEN
AutoBoolCase (0 < x+y)
THEN
AutoBoolCase ((((x rem n)+(y rem n)) rem n) < 0)
THEN
AutoBoolCase (0 < (((x rem n)+(y rem n)) rem n))
THEN
SplitOnConclITE
Generated subgoals:
n)
n+(x rem n)
x < 0
x+y = 0
|(((x rem n)+(y rem n)) rem n)+if (x+y < 
0)
-|n| ;((((x rem n)+(y rem n)) rem n) <