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)i:{1...n}. f(i) = g(i) Peg i k)
i:{1...k-1}. f(i) f(k) Peg & g(i) g(k) Peg)is mentioned by
n: , a,z: , m:{a...z-1}, s1:({a...m}  {1...n}Peg),
Thm*  s2:({m+1...z}{1...n}Peg).
Thm* (  k:{1...n}. Moving disk k of n takes s1(m) to s2(m+1))
Thm* 
Thm* s1 is a Hanoi(n disk) seq on a..m Thm*
Thm* s2 is a Hanoi(n disk) seq on m+1..z Thm*
Thm* (s1 @(m) s2) is a Hanoi(n disk) seq on a..z | [hanoi_seq_join_seq] |
| n:, f,g:({1...n}Peg), k:{1...n}.
Thm* Moving disk k of n takes f to g f(k) g(k) | [hanoi_step_at_diff] |
| n:, f,g:({1...n}Peg), k:{1...n}.
Thm* Moving disk k of n takes f to g Moving disk k of n takes g to f | [hanoi_step_at_sym] |
| n:, f,g:({1...n}Peg), j:{1...n}.
Thm* ( k:{1...n}. Moving disk k of n takes f to g)
Thm*
Thm* f(j) g(j) Moving disk j of n takes f to g | [hanoi_step_at_change] |
| n:, f,g:({1...n}Peg), i,k:{1...n}.
Thm* Moving disk k of n takes f to g f(i) g(i) i = k | [hanoi_step_at_unique] |
| n:, f,g:({1...n}Peg), k:{1...n}.
Thm* Moving disk k of n takes f to g Thm*
Thm* f = (  i.otherPeg(f(k); g(k))) {1...k-1}Peg | [hanoi_step_at_otherpeg] |
| n:, f,g:({1...n}Peg), k:{1...n}.
Thm* Moving disk k of n takes f to g f(k) g(k) | [hanoi_step_at_change2] |
| n:, f,g:({1...n}Peg), k,i:{1...n}.
Thm* Moving disk k of n takes f to g i k f(i) = g(i) | [hanoi_step_at_same] |
Def == x,x':{a...z}.
Def == x+1 = x' (k:{1...n}. Moving disk k of n takes s(x) to s(x')) | [hanoi_seq] |
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html