Nuprl - Proof: no finite model 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. 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. A ~

n
8.

k:

.

f:(

k

A).

i,j:

k. i<j

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

(n+1)

A
10.

i,j:

(n+1). i<j

R(f(i);f(j))

x:A. R(x;x)

By:	New:e Analyze7 THEN Analyze8

Generated subgoal:

1 7. e : An
8. g : nA
9. InvFuns(A;n;e;g)
10. k:. f:(kA). 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))
  x:A. R(x;x)
12 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