Nuprl - Proof: hanoi subseq 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi subseq 1

1. n :

2. a :

3. z :

4. s : {a...z}

{1...n}

Peg
5. s is a Hanoi(n disk) seq on a..z
6. a' : {a...z}
7. z' : {a...z}

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

By:	SimilarTo: Hyp:-3

Generated subgoals:

None

About:

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