Nuprl - Proof: hanoi sol2 via permshift

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

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/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

, p,q:Peg.

(

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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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

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