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

(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 2

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 :

(k+1)
14. y :

(k+1)
15. x

y
16. (e o f)(x) = (e o f)(y)
17.

x<y

x,y:

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

By:	Witness: y \| x

Generated subgoals:

None

About:

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

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