Nuprl - Proof: hanoi seq core

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
If you take an interior subsequence of a proper stacking sequence and remove the disks above a certain size, you'll be left with a proper stacking sequence.

At: hanoi seq core

n':

, n:{n'...}, a,z:

, s:({a...z}

{1...n}

Peg).

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

(

a',z':{a...z}.

((

x:{a'...z'}, i:{n'+1...n}. s(a',i) = s(x,i))

(

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

By:

Auto

Generated subgoal:

1 1. n' :
2. n : {n'...}
3. a :
4. z :
5. s : {a...z}{1...n}Peg
6. s is a Hanoi(n disk) seq on a..z
7. a' : {a...z}
8. z' : {a...z}
9. x:{a'...z'}, i:{n'+1...n}. s(a',i) = s(x,i)
s is a Hanoi(n' disk) seq on a'..z'
5 steps

About:

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

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