IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi sol2 via permshift213 1. n : 2. 0<n 3. p,q:Peg.
3. pq 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. pq 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))
z:{1...}, m:{1...z-1}, s1:({1...m}{1...n}Peg),
s2:({m+1...z}{1...n}Peg).
(s1 @(m) s2) is a Hanoi(n disk) seq on 1..z & s1(1) = (i.p) {1...n}Peg
& s2(z) = (i.q)
By:
(qp Peg By SimilarTo: p = q Peg ; Id)
THEN
FwdThru:
Thm*n:, a,z:, s:({a...z}{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z Thm* Thm* (f:(PegPeg).
Thm* (Inj(Peg; Peg; f) (x,i. f(s(x,i))) is a Hanoi(n disk) seq on a..z)
on [ Hyp:11 ]
Using:[permute(p to otherPeg(p; q) ; otherPeg(p; q) to q)]