(19steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat to nat pair surj 1 1 1 2 1 1

1. k : 
2. k1:k1<k  (x,y:x+y = k1  (a:. nat_to_nat_pair(a) = <x,y>))
3. x : 
4. x1:x1<x  (y:x1+y = k  (a:. nat_to_nat_pair(a) = <x1,y>))
5. y : 
6. x+y = k
7. x = 0
8. y = 0
9. n : 
10. nat_to_nat_pair(n) = <y-1,0>
  nat_to_nat_pair(n+1) = <x,y>


By: Compute nat_to_nat_pair(n+1) THEN SplitITE Concl THEN Subst: n+1-1 = n  


Generated subgoal:

1 11. n+1  0
  next_nat_pair(nat_to_nat_pair(n)) = <x,y>

2 steps

About:
pairproductintnatural_numberaddsubtractless_thanapply
equalimpliesallexistsmarkup_tag
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(19steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc