Nuprl - Proof: hanoi sol2 via general 1

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

1. n :

2. p : Peg
3. q : Peg
4. p

q
5. a :

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

{1...n}

Peg).

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

i.p) & s(z) = (

i.q)

By:	{Note that p q is irrelevant } BackThru: Thm* n:, f,g:({1...n}Peg), a:. Thm* z:{a...}, s:({a...z}{1...n}Peg). Thm* s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g

Generated subgoals:

None

About:

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