(7steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
At:
absval
eq
1
1
1.
x:
2.
y:
if 0
x
x else -x fi = if 0
y
y else -y fi
x =
y
By:
BoolCasesOnCExp (0
x)
THEN
BoolCasesOnCExp (0
y)
THEN
AbReduce 0
Generated subgoals:
1
3.
0
x
4.
0
y
x = y
x =
y
2
3.
0
x
4.
y < 0
x = -y
x =
y
3
3.
x < 0
4.
0
y
-x = y
x =
y
4
3.
x < 0
4.
y < 0
-x = -y
x =
y
About:
(7steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc