Nuprl - Proof: hanoi sol2 ala generalPROGcomp 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi sol2 ala generalPROGcomp 1 2

1. n :

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

q
5. a :

6. n

0
7. m : {a...}
8. s1 : {a...m}

{1...n-1}

Peg
9. HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a) = <m,s1>

otherPeg(p; q)

By:	BackThru: Thm* x,y:Peg. x y otherPeg(x; y) y

Generated subgoals:

None

About:

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