Nuprl - Proof: hanoi seq core 1

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

1. n' :

2. n : {n'...}
3. a :

4. z :

5. s : {a...z}

{1...n}

Peg
6. s is a Hanoi(n disk) seq on a..z
7. a' : {a...z}
8. z' : {a...z}
9.

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

s is a Hanoi(n' disk) seq on a'..z'

By:	SimilarTo: Hyp:6

Generated subgoal:

1 10. x : {a'...z'}
11. x' : {a'...z'}
12. x+1 = x'
13. k : {1...n}
14. Moving disk k of n takes s(x) to s(x')
k {1...n'}
4 steps

About:

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