(10steps 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 generalPROG wf 1 1 1 2 1 2
1. n : 
2. n1:. 
2. n1<n
2. 
2. (p,q:Peg.
2. (p  q
2. (
2. ((a:. 
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. a : 
7. n  0
8. HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)
8.  z:{a...}({a...z}{1...n-1}Peg)
9. m : {a...}
10. s1 : {a...m}{1...n-1}Peg
11. <m,s1> = HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)
12. HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)
12.  z:{m+1...}({m+1...z}{1...n-1}Peg)
  (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>)
   z:{a...}({a...z}{1...n}Peg)
By: Let
(whatnot = HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1))
THEN
New:[z | s2] Analyze-2
THEN
Reduce Concl

Generated subgoal:

1 13. z : {m+1...}
14. s2 : {m+1...z}{1...n-1}Peg
15. <z,s2>
15. =
15. HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)
  <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2>
   z:{a...}({a...z}{1...n}Peg)
Auto

About:
pairspreadproductintnatural_numberaddsubtract
less_thanlambdafunctionequalmemberimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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