a,z:
, n:
, s:({a...z}
{1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
h:({n+1...n'}Peg).
Thm* (s is a Hanoi(n disk) seq on a..z
Thm* (
Thm* ((s(?) {to n}
h {to n'}) is a Hanoi(n' disk) seq on a..z)a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
h:({n+1...n'}Peg), i:{1...n'}.
Thm* (n<i
(x:{a...z}. (s(?) {to n} h {to n'})(x,i) = h(i)))a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
h:({n+1...n'}Peg), i:{1...n'}.
Thm* (i
n (x:{a...z}. (s(?) {to n} h {to n'})(x,i) = s(x,i)))