(19steps total) Remark 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 generalPROGworks 2

1. n : 
2. 0<n
3. p,q:Peg.
3. p  q
3. 
3. (a:
3. (HanoiSTD(n-1 disks; from: p; to: q; indexing from: a)/z,s.
3. (s is a Hanoi(n-1 disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. a : 
  HanoiSTD(n disks; from: p; to: q; indexing from: a)/z,s.
  s is a Hanoi(n disk) seq on a..z
  s(a) = (i.p {1...n}Peg
  s(z) = (i.q {1...n}Peg


By: p = otherPeg(pq) | otherPeg(pq) = q  Asserted


Generated subgoals:

1   p = otherPeg(pq)
1 step
2 8. p = otherPeg(pq)
  otherPeg(pq) = q

1 step
3 8. p = otherPeg(pq)
9. otherPeg(pq) = q
  HanoiSTD(n disks; from: p; to: q; indexing from: a)/z,s.
  s is a Hanoi(n disk) seq on a..z
  s(a) = (i.p {1...n}Peg
  s(z) = (i.q {1...n}Peg

11 steps

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

(19steps total) Remark PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc