Nuprl - Proof: hpre def 1

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

1. m :

if m=

0 then 0 else m-1 fi

if m =

0 then 0 else @

. (m =

(n+1)) fi

By:	BifCase THEN Simp THEN StrongAuto

Generated subgoals:

1 2. m = 0
0 = if m = 0 then 0 else @n:. (m = (n+1)) fi
1 step

2 2. m = 0
m-1 = if m = 0 then 0 else @n:. (m = (n+1)) fi
5 steps

About:

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

1	2. m = 0 0 = if m = 0 then 0 else @n:. (m = (n+1)) fi	1 step
2	2. m = 0 m-1 = if m = 0 then 0 else @n:. (m = (n+1)) fi	5 steps