| Some definitions of interest. |
|
hanoi_step_at | Def Moving disk k of n takes f to g
Def == ( i:{1...n}. f(i) = g(i) Peg  i k)
Def == & ( i:{1...k-1}. f(i) f(k) Peg & g(i) g(k) Peg) |
| | Thm* n: , f,g:({1...n} Peg), k:{1...n}.
Thm* Moving disk k of n takes f to g Prop |
|
hanoi_PEG | Def Peg == {1...3} |
| | Thm* Peg Type |
|
hanoi_seq_deepen | Def (s(?) {to n} h {to n'})(x) == s(x) {to n} h {to n'} |
| | Thm* a,z: , n: , s:({a...z} {1...n} Peg), n': .
Thm* n n'
Thm* 
Thm* ( h:({n+1...n'} Peg). (s(?) {to n} h {to n'}) {a...z} {1...n'} Peg) |
|
iff | Def P  Q == (P  Q) & (P  Q) |
| | Thm* A,B:Prop. (A  B) Prop |
|
int_iseg | Def {i...j} == {k: | i k & k j } |
| | Thm* i,j: . {i...j} Type |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
nequal | Def a b T == a = b T |
| | Thm* A:Type, x,y:A. (x y) Prop |