Nuprl - Proof: hanoi sol2 ala general

(19steps 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 Towers of Hanoi Problem is soluble.

At: hanoi sol2 ala general

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))

By:	NatInd Concl

Generated subgoals:

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

2 1. n :
2. 0<n
3. p,q:Peg.
3. p  q
3.
3. (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) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. 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)
14 steps

About:

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

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