Nuprl - Proof: hanoi seq deepen seq 1 1 1

(8steps total) PfGloss PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi seq deepen seq 1 1 1

1. a :

2. z :

3. n :

4. s : {a...z}

{1...n}

Peg
5. n' :

6. n

n'
7. h : {n+1...n'}

Peg
8. x : {a...z}
9. x' : {a...z}
10. x+1 = x'
11. k : {1...n}
12.

i:{1...n}. s(x,i) = s(x',i)

k
13. i : {1...n'}

(s(?) {to n}

h {to n'})(x,i) = (s(?) {to n}

h {to n'})(x',i)

By:	Decide: in

Generated subgoals:

1 14. in
(s(?) {to n} h {to n'})(x,i) = (s(?) {to n} h {to n'})(x',i) i k
2 steps

2 14. in
(s(?) {to n} h {to n'})(x,i) = (s(?) {to n} h {to n'})(x',i) i k
1 step

About:

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

(8steps total) PfGloss PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc

1	14. in (s(?) {to n} h {to n'})(x,i) = (s(?) {to n} h {to n'})(x',i) i k	2 steps
2	14. in (s(?) {to n} h {to n'})(x,i) = (s(?) {to n} h {to n'})(x',i) i k	1 step