Nuprl - Proof: finite choice 1 2 2 1

(15steps total) Remark PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite choice 1 2 2 1

1. A : Type
2. k :

3.

k1:

.
3. k1<k
3.

3. (

Q:(

k1

A

Prop).
3. ((

x:

k1.

y:A. Q(x;y))

(

f:(

k1

A).

x:

k1. Q(x;f(x))))
4. Q :

k

A

Prop
5.

x:

k.

y:A. Q(x;y)
6.

k = 0
7. g :

(k-1)

A
8.

x:

(k-1). Q(x;g(x))

f:(

k

A).

x:

k. Q(x;f(x))

By:	(SimilarTo: f:(kA). f(k-1) = y & (x:(k-1). f(x) = g(x)) ; Witness5: k-1) THEN Analyze-1

Generated subgoal:

1 9. y : A
10. Q(k-1;y)
f:(kA). x:k. Q(x;f(x))
8 steps

About:

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

(15steps total) Remark PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc