Our proof has reduced to showing (*1) thru (*4).

(*1) s(x) = (i.otherPeg(s(x,n); s(x+1,n)))  {1...n-1}Peg follows from (I) and the lemma

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

(*2) s(y) = (i.otherPeg(s(y-1,n); s(y,n)))  {1...n-1}Peg follows from (J), from the lemma just cited, and from a couple of symmetry lemmas

Thm*  x,y:Peg. x  y  otherPeg(x; y) = otherPeg(y; x)

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

(*3) p  otherPeg(s(x,n); s(x+1,n)) follows from the fact that, by (E), p = s(x,n), and the lemma

Thm*  x,y:Peg. x  y  x  otherPeg(x; y)

(*4) q  otherPeg(s(y-1,n); s(y,n)) follows from the fact that, by (H), q = s(y,n), and the same lemma.

QED

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