Nuprl - Proof: mklist select 2 1

(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

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)

i:

n. mklist(n;f)[i] = f(i)

By:	Unfold `mklist` 0 THEN RecUnfold `primrec` 0 THEN SplitOnConclITE

Generated subgoals:

1 7. n = 0
  i:n. nil[i] = f(i)  T
Auto

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