Def ==
x,x':{a...z}.
Def == x+1 = x'
(
k:{1...n}. Moving disk k of n takes s(x) to s(x'))n:
, a,z:
, s:({a...z}
{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z
Prop Type| i
k & kj }i,j:. {i...j} Type == {i:| 0i } Type| Some definitions of interest. | |
| hanoi_seq | Def == x,x':{a...z}.
Def == x+1 = x' (k:{1...n}. Moving disk k of n takes s(x) to s(x')) |
| n:, a,z:, s:({a...z}{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z Prop | |
| hanoi_PEG | |
| Type | |
| int_iseg | | ik & kj } |
| i,j:. {i...j} Type | |
| nat | == {i:| 0i } |
| Type |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |