Nuprl - Proof: hanoi sol2 via permshift

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
There is a Hanoi sequence taking all the disks from any peg to any other.

At: hanoi sol2 via permshift

n:

, p,q:Peg.

p

q

(

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

{1...n}

Peg).

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

i.p) & s(z) = (

i.q))

By:	NatInd Concl

Generated subgoals:

1 1. p : Peg
2. q : Peg
3. p  q
  z:{1...}, s:({1...z}{1...0}Peg).
  s is a Hanoi(0 disk) seq on 1..z & s(1) = (i.p) & s(z) = (i.q)
4 steps

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

About:

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

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