n:
, p,q:Peg.
Thm* p
q
Thm*
Thm* (
a:
.
Thm* (1of(HanoiSTD(n disks; from: p; to: q; indexing from: a)) = a+(2^n)-1)
x,y:Peg. x y otherPeg(x; y) yx,y:Peg. x y x otherPeg(x; y)| Rank | Theorem | Name |
| 2 | n:, p,q:Peg.
Thm* p q
Thm*
Thm* ( a:.
Thm* (1of(HanoiSTD(n disks; from: p; to: q; indexing from: a)) = a+(2^n)-1) | [hanoi_general_exists_lemma2PROG_endpoint] |
| cites the following: | ||
| 1 | x,y:Peg. x y otherPeg(x; y) y | [hanoi_otherpeg_diff2] |
| 1 | x,y:Peg. x y x otherPeg(x; y) | [hanoi_otherpeg_diff3] |