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
Q) (
P Q)| Theorem | Name |
| 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] |
| cites the following: | |
| Q) (P Q) | [not_functionality_wrt_iff] |