Nuprl - Proof: divides of absvals 1 1

(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 0

a else -a fi | if 0

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:

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

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