Nuprl - Proof: int ooc nat 1 1 a 2

(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 2

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

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