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

(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

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. n :

7. e : A

n
8. g :

n

A
9. InvFuns(A;

n;e;g)
10.

k:

.

f:(

k

A).

i,j:

k. i<j

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

(n+1)

A
12.

i,j:

(n+1). i<j

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

x,y:

(n+1). x

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

x:A. R(x;x)

By:	x,y:(n+1). x<y & (e o f)(x) = (e o f)(y) By SideProof THEN ExistHD Hyp:-1

Generated subgoal:

1 14. x : (n+1)
15. y : (n+1)
16. x<y
17. (e o f)(x) = (e o f)(y)
x:A. R(x;x)
6 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