Nuprl - Proof: hanoi general exists lemma2

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A lemma about composing stacking situations into a Hanoi seqence, given one already has appropriate Hanoi sequences for one fewer disks.

At: hanoi general exists lemma2

, a:

, z:{a...}, m:{a...z-1}, f,g:({1...n}

Peg).

f(n)

g(n)

(

s1:({a...m}

{1...n-1}

Peg), s2:({m+1...z}

{1...n-1}

Peg).

(s1 is a Hanoi(n-1 disk) seq on a..m

(& s1(a) = f

{1...n-1}

Peg

(& s2 is a Hanoi(n-1 disk) seq on m+1..z

(& s2(z) = g

{1...n-1}

Peg

(& s1(m) = s2(m+1)

(& (

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

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

g(n)))

(

r1:({a...m}

{1...n}

Peg), r2:({m+1...z}

{1...n}

Peg).

((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g)

By:	Auto THEN New:s1 Analyze-1 THEN New:s2 Analyze-1

Generated subgoal:

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  {1...n-1}Peg
12. s2 is a Hanoi(n-1 disk) seq on m+1..z
13. s2(z) = g  {1...n-1}Peg
14. s1(m) = s2(m+1)
15. i:{1...n-1}. s1(m,i)  f(n) & s2(m+1,i)  g(n)
  r1:({a...m}{1...n}Peg), r2:({m+1...z}{1...n}Peg).
  (r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g
25 steps

About:

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

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