Nuprl - Proof: mklist select 2 1 2

(12steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc

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

1. T : Type
2. n :

3. 0<n
4.

f:(

(n-1)

T), i:

(n-1). mklist(n-1;f)[i] = f(i)
5. f :

n

T
6.

i:

(n-1). mklist(n-1;f)[i] = f(i)
7.

n = 0

i:

n.

((

i,l. l @ [(f(i))])(n-1,primrec(n-1;nil;

i,l. l @ [(f(i))])))[i] = f(i)

T

By:	Reduce 0 THEN Fold `mklist` 0

Generated subgoal:

1 8. i : n
(mklist(n-1;f) @ [(f(n-1))])[i] = f(i)
6 steps

About:

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

(12steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc