From (A) we infer that there are x  {a...z-1}, y  {x+1...z}, such that

(E) u:{a...x}. s(u,n) = p

(F) s(x+1,n)  p

(G) s(y-1,n)  q

(H) u:{y...z}. s(u,n) = q

this inference being justified by (C) and (D), using s(u,n) for f(u). This x and y will serve as the x and y of our goal (*). Now we apply assumption (B) twice to get

k:{1...n}. Moving disk k of n takes s(x) to s(x+1)

k:{1...n}. Moving disk k of n takes s(y-1) to s(y)

and applying to each of these the lemma

Thm*  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

we infer

(I) Moving disk n of n takes s(x) to s(x+1)

(s(x,n)  s(x+1,n) because of (E) and (F))

(J) Moving disk n of n takes s(y-1) to s(y)

(s(y-1,n)  s(y,n) because of (G) and (H))

At last we provide the witnesses for p', q'  Peg for our goal (*), namely

otherPeg(s(x,n); s(x+1,n)) and otherPeg(s(y-1,n); s(y,n))

leaving us with 4 subgoals, since the first two conjuncts of (*) are just (E) and (H) themselves:

(*1) s(x) = (i.otherPeg(s(x,n); s(x+1,n)))  {1...n-1}Peg

(*2) s(y) = (i.otherPeg(s(y-1,n); s(y,n)))  {1...n-1}Peg

(*3) p  otherPeg(s(x,n); s(x+1,n))

(*4) q  otherPeg(s(y-1,n); s(y,n))

Continued at hanoi sol2 analemma gloss cont2

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html