Nuprl - Proof: nsub bool 1

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

InvFuns(

;

b.if b

1 else 0 fi;

i.if i=0

false

; true

fi)

By:	Analyze THEN Reduce Concl

Generated subgoals:

1 1. x :
if if x 1 else 0 fi=0 false ; true fi = x
1 step

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

About:

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

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