2. p : Peg
3. q : Peg
4. p
q
5. a :
6. z : {a...}
7.
f:({a...z}
Peg).
7. f(a) = p & f(z) = q
7.
7. (
x:{a...z-1}, y:{x+1...z}.
7. ((
u:{a...x}. f(u) = p) & f(x+1) p & f(y-1) q & (u:{y...z}. f(u) = q))
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. x : {a...z-1}
13. y : {x+1...z}
14.
u:{a...x}. s(u,n) = p
15. s(x+1,n)
p
16. s(y-1,n)
q
17.
u:{y...z}. s(u,n) = q
18. s(x,n)
s(x+1,n)
19. s(y-1,n)
s(y,n)
20.
k:{1...n}. Moving disk k of n takes s(x) to s(x+1)
21.
k:{1...n}. Moving disk k of n takes s(y-1) to s(y)
22. Moving disk n of n takes s(x) to s(x+1)
23. Moving disk n of n takes s(y-1) to s(y)
p',q':Peg.
(u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q)
& s(x) = (i.p') 
{1...n-1}Peg & s(y) = (i.q') {1...n-1}Peg
& p p'
& q q'
