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