Nuprl - Proof: hanoi seq shift 1

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

1. n :

2. a :

3. z :

4. d :

5. s : {a...z}

{1...n}

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

(

x.s(x-d)) is a Hanoi(n disk) seq on a+d..z+d

By:	UnivCD THEN Reduce Concl

Generated subgoal:

1 7. x : {a+d...z+d}
8. x' : {a+d...z+d}
9. x+1 = x'
k:{1...n}. Moving disk k of n takes s(x-d) to s(x'-d)
4 steps

About:

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