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))
14. (
x,i. permute(p to otherPeg(p; q) ; otherPeg(p; q) to q)(s1(x,i)))
14. is a Hanoi(n-1 disk) seq on 1..m
15. (
x,i. permute(p to otherPeg(p; q) ; otherPeg(p; q) to q)(s1(x-m,i)))
15. is a Hanoi(n-1 disk) seq on 1+m..m+m
16. i : {1...n-1}
s1(m,i) p
