Nuprl - Proof: negnegelim imp notfin imp unb inf 1 2 2 1 2 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: negnegelim imp notfin imp unb inf 1 2 2 1 2 1 1

1.

P:Prop.

P

P
2. A : Type
3.

(

n:

. A ~

n)
4. k :

5. 0<k
6. f :

(k-1)

A
7. Inj(

(k-1); A; f)
8. a : A
9.

i:

(k-1). f(i)

a
10. (

j.if j=

k-1

a else f(j) fi)

k

A
11. a1 :

k
12. a2 :

k
13. if a1=

k-1

a else f(a1) fi = if a2=

k-1

a else f(a2) fi

a1 = a2

By:	SplitITE Hyp:-1 THEN SplitITE Hyp:-2

Generated subgoals:

1 13. a = f(a2)
14. a1 = k-1
15. a2  k-1
  a1 = a2
1 step

2 13. f(a1) = a
14. a1  k-1
15. a2 = k-1
  a1 = a2
1 step

3 13. f(a1) = f(a2)
14. a1  k-1
15. a2  k-1
  a1 = a2
1 step

About:

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

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