Nuprl - Proof: hanoi general exists 2

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi general exists 2

1. n :

2. 0<n
3.

f,g:({1...n-1}

Peg), 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) = f & s(z) = g
4. f : {1...n}

Peg
5. g : {1...n}

Peg
6. a :

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

{1...n}

Peg).

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

By:	Decide: f(n) = g(n) Peg

Generated subgoals:

1 7. f(n) = g(n)
  z:{a...}, s:({a...z}{1...n}Peg).
  s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g
2 steps

2 7. f(n) = g(n)
  z:{a...}, s:({a...z}{1...n}Peg).
  s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g
11 steps

About:

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

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

1	7. f(n) = g(n) z:{a...}, s:({a...z}{1...n}Peg). s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g	2 steps
2	7. f(n) = g(n) z:{a...}, s:({a...z}{1...n}Peg). s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g	11 steps