| Some definitions of interest. |
|
hanoi_seq | Def s is a Hanoi(n disk) seq on a..z
Def == x,x':{a...z}.
Def == x+1 = x'  ( k:{1...n}. Moving disk k of n takes s(x) to s(x')) |
| | Thm* n: , a,z: , s:({a...z} {1...n} Peg).
Thm* s is a Hanoi(n disk) seq on a..z Prop |
|
hanoi_PEG | Def Peg == {1...3} |
| | Thm* Peg Type |
|
hanoi_general_exists_lemma2PROG | Def HanoiHelper(n; s1; f; s2; g)
Def == <s1(?) {to n-1} f {to n},s2(?) {to n-1} g {to n}> |
| | Thm* n: , a: , z:{a...}, m:{a...z-1}, f,g:({1...n} Peg),
Thm* s1:({a...m} {1...n-1} Peg), s2:({m+1...z} {1...n-1} Peg).
Thm* HanoiHelper(n; s1; f; s2; g)
Thm* ({a...m} {1...n} Peg) ({m+1...z} {1...n} Peg) |
|
hanoi_seq_join | Def (s1 @(m) s2)(x) == if x m s1(x) else s2(x) fi |
| | Thm* n: , m,a,z: , s1:({a...m} {1...n} Peg), s2:({m+1...z} {1...n} Peg).
Thm* (s1 @(m) s2) {a...z} {1...n} Peg |
|
int_iseg | Def {i...j} == {k: | i k & k j } |
| | Thm* i,j: . {i...j} Type |
|
int_upper | Def {i...} == {j: | i j } |
| | Thm* n: . {n...} Type |
|
nat_plus | Def  == {i: | 0<i } |
| | Thm*  Type |
|
nequal | Def a b T == a = b T |
| | Thm* A:Type, x,y:A. (x y) Prop |