2.
n1:.
2. n1<n
2.
2. (
p,q:Peg.
2. (p
q
2. (
2. ((
a:
, z:{a...}, s:({a...z}
{1...n1}Peg).
2. ((s is a Hanoi(n1 disk) seq on a..z & s(a) = (
i.p) & s(z) = (i.q)
2. ((
2. (((2^n1)
z-a+1))
3. p : Peg
4. q : Peg
5. p
q
6. a :
7. z : {a...}
8. s : {a...z}
{1...n}Peg
9. s is a Hanoi(n disk) seq on a..z
10. s(a) = (
i.p)
11. s(z) = (
i.q)
12. n
0
13. x : {a...z-1}
14. y : {x+1...z}
15. p' : Peg
16. q' : Peg
17.
u:{a...x}. s(u,n) = p
18.
u:{y...z}. s(u,n) = q
19. s(x) = (
i.p')
20. s(y) = (
i.q')
21. p
p'
22. q
q'
s(a) = (i.p) 
{1...n-1}Peg
