Nuprl - Proof: finite choice 1 2 2 1 1 2

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

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))
9. y : A
10. Q(k-1;y)
11. f :

k

A
12. f(k-1) = y
13.

x:

(k-1). f(x) = g(x)
14. x :

k

Q(x;f(x))

By:	Decide: x = k-1 k

Generated subgoals:

1 15. x = k-1  k
  Q(x;f(x))
1 step

2 15. x = k-1  k
  Q(x;f(x))
3 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