Nuprl - Proof: select listify id 1 1

(12steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc

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

1. T : Type
2. n :

3. f :

n

T

j:{...n}. 0

j

(

i:{j..n

}. (f{j..n

})[(i-j)] = f(i))

By:	(BackThru (Thm* i:, E:({...i}Prop). (Thm* E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))) THEN UnivCD

Generated subgoals:

1 4. 0n
5. i : {n..n}
  (f{n..n})[(i-n)] = f(i)
1 step

2 4. j : {...n-1}
5. 0j+1  (i:{(j+1)..n}. (f{(j+1)..n})[(i-(j+1))] = f(i))
6. 0j
7. i : {j..n}
  (f{j..n})[(i-j)] = f(i)
7 steps

About:

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

(12steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc