Nuprl - Proof: fin plus nat ooc nat 1 2

(8steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fin plus nat ooc nat 1 2

1. k :

InvFuns(

;

InvFuns;

d.InjCase(d; i. i; n. k+n);

j.if j<

inl(j) else inr(j-k) fi)

By:	Analyze THEN Reduce Concl

Generated subgoals:

1 2. x : k+
  if InjCase(x; i. i; n. k+n)<k inl(InjCase(x; i. i; n. k+n))
  else inr(InjCase(x; i. i; n. k+n)-k) fi
  =
  x
   k+
3 steps

2 2. y :
  InjCase(if y<k inl(y) else inr(y-k) fi; i. i; n. k+n) = y
1 step

About:

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

(8steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

1	2. x : k+ if InjCase(x; i. i; n. k+n)<k inl(InjCase(x; i. i; n. k+n)) else inr(InjCase(x; i. i; n. k+n)-k) fi = x k+	3 steps
2	2. y : InjCase(if y<k inl(y) else inr(y-k) fi; i. i; n. k+n) = y	1 step