(7steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: divides of absvals 1 1

1. a : 
2. b : 
  if 0a a else -a fi | if 0b b else -b fi  a | b


By: (BoolCasesOnCExp (0a)) THEN (BoolCasesOnCExp (0b)) THEN (AbReduce 0)


Generated subgoals:

1 3. 0a
4. 0b
  a | b  a | b

Auto
2 3. 0a
4. b<0
  a | -b  a | b

1 step
3 3. a<0
4. 0b
  -a | b  a | b

1 step
4 3. a<0
4. b<0
  -a | -b  a | b

1 step

About:
ifthenelseintnatural_numberminus
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(7steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc