Nuprl - Proof: hanoi seq shift

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

, a,z,d:

, s:({a...z}

{1...n}

Peg).

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:

Auto

Generated subgoal:

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
5 steps

About:

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