Nuprl - Proof: nsub bool 1 2

(6steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

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

1. y :

if if y=0

false

; true

1 else 0 fi = y

By:	Decide: y = 0 2 \| y = 1 2

Generated subgoals:

1 2. y = 0  2
3. y = 1  2
  if if y=0 false ; true fi 1 else 0 fi = y  2
1 step

2 2. y = 0  2
3. y = 1  2
  if if y=0 false ; true fi 1 else 0 fi = y  2
1 step

About:

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

(6steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

1	2. y = 0 2 3. y = 1 2 if if y=0 false ; true fi 1 else 0 fi = y 2	1 step
2	2. y = 0 2 3. y = 1 2 if if y=0 false ; true fi 1 else 0 fi = y 2	1 step