(16steps total) PfGloss PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
From a sequence of moves for one fewer disks we can derive one having the largest disk on the same peg at the beginning and the end.

At: hanoi general exists lemma1

  n:, f,g:({1...n}Peg).
  f(n) = g(n)
  
  (a:, z:{a...}.
  ((s:({a...z}{1...n-1}Peg). 
  ((s is a Hanoi(n-1 disk) seq on a..z
  ((& s(a) = f  {1...n-1}Peg
  ((& s(z) = g  {1...n-1}Peg)
  (
  ((s:({a...z}{1...n}Peg). 
  ((s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g))
By: Auto

Generated subgoal:

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

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

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