2. 0<n
3.
p,q:Peg.
3. p
q
3.
3. (
a:.
3. (
z:{a...}, s:({a...z}
{1...n-1}Peg).
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 :
8.
p = otherPeg(p; q)
9.
otherPeg(p; q) = q
10. m : {a...}
11. s1 : {a...m}
{1...n-1}Peg
12. s1 is a Hanoi(n-1 disk) seq on a..m
13. s1(a) = (
i.p)
14. s1(m) = (
i.otherPeg(p; q))
15. z : {m+1...}
16. s2 : {m+1...z}
{1...n-1}Peg
17. s2 is a Hanoi(n-1 disk) seq on m+1..z
18. s2(m+1) = (
i.otherPeg(p; q))
19. s2(z) = (
i.q)
(i.p)(n) (i.q)(n) 
Peg
