Nuprl - Proof: hanoi sol2 ala generalPROGcomp

(4steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc

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

n:

, p,q:Peg.

p

q

(

a:

.

(HanoiSTD(n disks; from: p; to: q; indexing from: a)

(=

((HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1.

((HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)/z,s2.

((<z,HanoiHelper(n; s1;

i.p; s2;

i.q)/r1,r2. r1 @(m) r2>))

By:

Auto

Generated subgoal:

1 1. n :
2. p : Peg
3. q : Peg
4. p  q
5. a :
  HanoiSTD(n disks; from: p; to: q; indexing from: a)
  =
  (HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1.
  (HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)/z,s2.
  (<z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2>)
3 steps

About:

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

(4steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc