Nuprl - Proof: hanoi sol2 lb

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The length of any Hanoi sequence solving The Towers of Hanoi Problem is at least 2 raised to the number of disks.

At: hanoi sol2 lb

n:

, p,q:Peg.

p

q

(

a:

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

{1...n}

Peg).

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

i.p) & s(z) = (

i.q)

(

((2^n)

z-a+1)

By:	CompNatInd Concl

Generated subgoal:

1 1. n :
2. n1:.
2. n1<n
2.
2. (p,q:Peg.
2. (p  q
2. (
2. ((a:, z:{a...}, s:({a...z}{1...n1}Peg).
2. ((s is a Hanoi(n1 disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q)
2. ((
2. (((2^n1)z-a+1))
3. p : Peg
4. q : Peg
5. p  q
6. a :
7. z : {a...}
8. s : {a...z}{1...n}Peg
9. s is a Hanoi(n disk) seq on a..z
10. s(a) = (i.p)
11. s(z) = (i.q)
  (2^n)z-a+1
14 steps

About:

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

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