Nuprl - Proof: hanoi seq shallower

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

n':

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

, z:{a...}, s:({a...z}

{1...n}

Peg).

s is a Hanoi(n disk) seq on 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 THEN BackThru: Thm* n':, n:{n'...}, a,z:, s:({a...z}{1...n}Peg). Thm* s is a Hanoi(n disk) seq on a..z Thm* Thm* (a',z':{a...z}. Thm* ((x:{a'...z'}, i:{n'+1...n}. s(a',i) = s(x,i)) Thm* ( Thm* (s is a Hanoi(n' disk) seq on a'..z')

Generated subgoals:

None

About:

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