Nuprl - Proof: nsub delete 1

(7steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

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

1. k :

2. j :

k
3. m :

4. m = k-1

{i:

k|

i = j } ~

m

By:	Witness: i.if i<j i else i-1 fi with type {i:k\| i = j }m THEN Witness: i.if i<j i else i+1 fi with type m{i:k\| i = j }

Generated subgoals:

1   (i.if i<j i else i-1 fi)  {i:k| i = j }m
2 steps

2 5. (i.if i<j i else i-1 fi)  {i:k| i = j }m
  (i.if i<j i else i+1 fi)  m{i:k| i = j }
2 steps

3 5. (i.if i<j i else i-1 fi)  {i:k| i = j }m
6. (i.if i<j i else i+1 fi)  m{i:k| i = j }
  InvFuns({i:k| i = j };m
  InvFuns;i.if i<j i else i-1 fi;i.if i<j i else i+1 fi)
1 step

About:

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

(7steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc