1. n : 
2. 0<n
3. p,q:Peg.
3. p  q
3. 
3. (z:{1...}, s:({1...z}{1...n-1}Peg).
3. (s is a Hanoi(n-1 disk) seq on 1..z & s(1) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. p  otherPeg(p; q)
8. otherPeg(p; q)  q
9. m : {1...}
10. s1 : {1...m}{1...n-1}Peg
11. s1 is a Hanoi(n-1 disk) seq on 1..m
12. s1(1) = (i.p)
13. s1(m) = (i.otherPeg(p; q))
  Inj(Peg; Peg; permute(p to otherPeg(p; q) ; otherPeg(p; q) to q))

By:	BackThru:  Thm*  p,r,q,s:Peg. p  q  r  s  Inj(Peg; Peg; permute(p to r ; q to s))

None

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