(7steps) PrintForm Definitions int 2 Sections StandardLIB Doc

At: absval eq 1 1

1. x:
2. y:

if 0x x else -x fi = if 0y y else -y fi x = y

By:
BoolCasesOnCExp (0x)
THEN
BoolCasesOnCExp (0y)
THEN
AbReduce 0


Generated subgoals:

13. 0x
4. 0y
x = y x = y
23. 0x
4. y < 0
x = -y x = y
33. x < 0
4. 0y
-x = y x = y
43. x < 0
4. y < 0
-x = -y x = y


About:
ifthenelseintnatural_numberminusequal

(7steps) PrintForm Definitions int 2 Sections StandardLIB Doc