Nuprl - Proof: no finite model 1 1 1 1 1 1 a

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: no finite model 1 1 1 1 1 1 a

1. A : Type
2. R : A

A

Prop
3.

A
4. Trans x,y:A. R(x;y)
5.

x:A.

y:A. R(x;y)
6. k :

7. e : A

k
8. g :

k

A
9. InvFuns(A;

k;e;g)
10.

k:

.

f:(

k

A).

i,j:

k. i<j

R(f(i);f(j))
11. f :

(k+1)

A
12.

i,j:

(k+1). i<j

R(f(i);f(j))
13.

x,y:

(k+1). x

y & (e o f)(x) = (e o f)(y)

x,y:

(k+1). x<y & (e o f)(x) = (e o f)(y)

By:	ExistHD Hyp:13

Generated subgoal:

1 13. x : (k+1)
14. y : (k+1)
15. x y
16. (e o f)(x) = (e o f)(y)
x,y:(k+1). x<y & (e o f)(x) = (e o f)(y)
3 steps

About:

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

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