Nuprl - Proof: division4 sfa 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: division4 sfa 1

1. k :

2. r1 :

k
3. r2 :

k
4. q1 :

5. q2 :

6. q1

k+r1 = q2

k-r2

q1 = q2 & r1 = 0 & r2 = 0

q2 = q1+1 & r2 = k-r1

By:	Decide: r2 = 0 THENL [Select: 1;Select: 2]

Generated subgoals:

1 7. r2 = 0
q1 = q2 & r1 = 0 & r2 = 0
1 step

2 7. r2 = 0
q2 = q1+1 & r2 = k-r1
1 step

About:

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

1	7. r2 = 0 q1 = q2 & r1 = 0 & r2 = 0	1 step
2	7. r2 = 0 q2 = q1+1 & r2 = k-r1	1 step