Nuprl - Proof: hanoi sol2 ala generalPROG wf 1 1 1 1

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

1. n :

n1:

.
2. n1<n
2.

2. (

p,q:Peg.
2. (p

q
2. (

2. ((

.
2. ((HanoiSTD(n1 disks; from: p; to: q; indexing from: a)
2. ((

z:{a...}

({a...z}

{1...n1}

Peg)))
3. p : Peg
4. q : Peg
5. p

q
6.

7. n

otherPeg(p; q)

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

Generated subgoals:

None

About:

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