Nuprl - Proof: hanoi seq shift 1 1

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

1. n :

2. a :

3. z :

4. d :

5. s : {a...z}

{1...n}

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

k:{1...n}. Moving disk k of n takes s(x-d) to s(x'-d)

By:	BackThru: Hyp:6

Generated subgoals:

1   x-d  {a...z}
Auto

2   x'-d  {a...z}
Auto

3   x-d+1 = x'-d
Auto

About:

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