n:
, f,g:({1...n}
Peg), j:{1...n}.
Thm* (
k:{1...n}. Moving disk k of n takes f to g)
Thm*
Thm* f(j)
g(j) Moving disk j of n takes f to gn:, f,g:({1...n}Peg), i,k:{1...n}.
Thm* Moving disk k of n takes f to g
f(i) g(i) i = k| Rank | Theorem | Name |
| 2 | n:, f,g:({1...n}Peg), j:{1...n}.
Thm* ( k:{1...n}. Moving disk k of n takes f to g)
Thm*
Thm* f(j) g(j) Moving disk j of n takes f to g | [hanoi_step_at_change] |
| cites the following: | ||
| 1 | n:, f,g:({1...n}Peg), i,k:{1...n}.
Thm* Moving disk k of n takes f to g f(i) g(i) i = k | [hanoi_step_at_unique] |