n:
, p,q:Peg.
Thm* p
q
Thm*
Thm* (
a:
.
Thm* (HanoiSTD(n disks; from: p; to: q; indexing from: a)
Thm* (
z:{a...}
({a...z}
{1...n}Peg))x,y:Peg. x y x otherPeg(x; y)x,y:Peg. x y otherPeg(x; y) y| Rank | Theorem | Name |
| 2 | n:, p,q:Peg.
Thm* p q
Thm*
Thm* ( a:.
Thm* (HanoiSTD(n disks; from: p; to: q; indexing from: a) Thm* ( z:{a...}({a...z}{1...n}Peg)) | [hanoi_sol2_ala_generalPROG_wf] |
| cites the following: | ||
| 1 | x,y:Peg. x y x otherPeg(x; y) | [hanoi_otherpeg_diff3] |
| 1 | x,y:Peg. x y otherPeg(x; y) y | [hanoi_otherpeg_diff2] |