Nuprl - Proof: hanoi general exists

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
This generalizes of The Towers of Hanoi Problem by not constraining the start and end positions of the disks.

There is a Hanoi sequence of moves for any possible starting and ending situations.

At: hanoi general exists

, f,g:({1...n}

Peg), a:

z:{a...}, s:({a...z}

{1...n}

Peg).

s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g

By:	NatInd Concl

Generated subgoals:

1 1. f : {1...0}Peg
2. g : {1...0}Peg
3. a :
  z:{a...}, s:({a...z}{1...0}Peg).
  s is a Hanoi(0 disk) seq on a..z & s(a) = f & s(z) = g
3 steps

2 1. n :
2. 0<n
3. f,g:({1...n-1}Peg), a:.
3. z:{a...}, s:({a...z}{1...n-1}Peg).
3. s is a Hanoi(n-1 disk) seq on a..z & s(a) = f & s(z) = g
4. f : {1...n}Peg
5. g : {1...n}Peg
6. a :
  z:{a...}, s:({a...z}{1...n}Peg).
  s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g
14 steps

About:

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

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

1	1. f : {1...0}Peg 2. g : {1...0}Peg 3. a : z:{a...}, s:({a...z}{1...0}Peg). s is a Hanoi(0 disk) seq on a..z & s(a) = f & s(z) = g	3 steps
2	1. n : 2. 0<n 3. f,g:({1...n-1}Peg), a:. 3. z:{a...}, s:({a...z}{1...n-1}Peg). 3. s is a Hanoi(n-1 disk) seq on a..z & s(a) = f & s(z) = g 4. f : {1...n}Peg 5. g : {1...n}Peg 6. a : z:{a...}, s:({a...z}{1...n}Peg). s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g	14 steps