Nuprl - Proof: int ooc nat 1 1 a 3

(27steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: int ooc nat 1 1 a 3

1. (

i.if 0

i

i

2 else (-i)

2-1 fi)

2. i :

3.

0

i

if 0

i

i

2 else (-i)

2-1 fi = (-i)

2-1

By:	SplitOnConclITE

Generated subgoals:

None

About:

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

(27steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc