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}, y:{x+1...z}.
12. (
u:{a...x}. s(u,n) = p)
12. & s(x+1,n)
p
12. & s(y-1,n)
q
12. & (
u:{y...z}. s(u,n) = q)
x:{a...z-1}, y:{x+1...z}, 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'
