Nuprl - Proof: dep finite choice 1 2

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

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

1. k :

2.

k1:

.
2. k1<k
2.

2. (

B:(

k1

Type), Q:(x:

k1

B(x)

Prop).
2. ((

x:

k1.

y:B(x). Q(x;y))

(

f:(x:

k1

B(x)).

x:

k1. Q(x;f(x))))
3. B :

k

Type
4. Q : x:

k

B(x)

Prop
5.

x:

k.

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

k = 0

f:(x:

k

B(x)).

x:

k. Q(x;f(x))

By:	FwdThru: Hyp:2 on [ x:(k-1). y:B(x). Q(x;y) ]

Generated subgoals:

1 7. x : (k-1)
y:B(x). Q(x;y)
1 step

2 7. f:(x:(k-1)B(x)). x:(k-1). Q(x;f(x))
f:(x:kB(x)). x:k. Q(x;f(x))
20 steps

About:

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

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