Nuprl - Proof: hanoi seq join seq

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Joining two Hanoi sequences produces a Hanoi sequence if a single move takes the end of the first to the start of the second.

At: hanoi seq join seq

, a,z:

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

{1...n}

Peg),

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

{1...n}

Peg).

(

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

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

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

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

By:

Auto

Generated subgoal:

1 1. n :
2. a :
3. z :
4. m : {a...z-1}
5. s1 : {a...m}{1...n}Peg
6. s2 : {m+1...z}{1...n}Peg
7. k:{1...n}. Moving disk k of n takes s1(m) to s2(m+1)
8. s1 is a Hanoi(n disk) seq on a..m
9. s2 is a Hanoi(n disk) seq on m+1..z
(s1 @(m) s2) is a Hanoi(n disk) seq on a..z
8 steps

About:

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

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