Nuprl - Proof: hanoi general exists lemma2PROGworks 1 1

(26steps total) Remark 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 lemma2PROGworks 1 1

1. n :

2. a :

3. z : {a...}
4. m : {a...z-1}
5. f : {1...n}

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

Peg
7. f(n)

g(n)
8. s1 : {a...m}

{1...n-1}

Peg
9. s2 : {m+1...z}

{1...n-1}

Peg
10. s1 is a Hanoi(n-1 disk) seq on a..m
11. s1(a) = f
12. s2 is a Hanoi(n-1 disk) seq on m+1..z
13. s2(z) = g
14. s1(m) = s2(m+1)
15.

i:{1...n-1}. s1(m,i)

f(n) & s2(m+1,i)

g(n)

((s1(?) {to n-1}

f {to n}) @(m) (s2(?) {to n-1}

g {to n}))

is a Hanoi(n disk) seq on a..z

By:

BackThru:
Thm*

n:

, a,z:

, m:{a...z-1}, s1:({a...m}

{1...n}

Peg),
Thm*

s2:({m+1...z}

{1...n}

Peg).
Thm* (

k:{1...n}. Moving disk k of n takes s1(m) to s2(m+1))
Thm*

Thm* s1 is a Hanoi(n disk) seq on a..m
Thm*

Thm* s2 is a Hanoi(n disk) seq on m+1..z
Thm*

Thm* (s1 @(m) s2) is a Hanoi(n disk) seq on a..z

Generated subgoals:

1   k:{1...n}.
  Moving disk k of n
  takes (s1(?) {to n-1}  f {to n})(m) to (s2(?) {to n-1}  g {to n})(m+1)
13 steps

2   (s1(?) {to n-1}  f {to n}) is a Hanoi(n disk) seq on a..m
1 step

3   (s2(?) {to n-1}  g {to n}) is a Hanoi(n disk) seq on m+1..z
1 step

About:

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

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