At: hanoi sol2 analemma

  n:, p,q:Peg.
  p  q
  
  (a:, z:{a...}, s:({a...z}{1...n}Peg).
  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q)
  (
  ((x:{a...z-1}, y:{x+1...z}, p',q':Peg.
  (((u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q)
  ((& s(x) = (i.p')  {1...n-1}Peg & s(y) = (i.q')  {1...n-1}Peg
  ((& p  p'
  ((& q  q'))

By:	Analyze THEN SimilarTo Thm*  p,q:Peg. Thm*  p  q Thm*   Thm*  (a:, z:{a...}, f:({a...z}Peg). Thm*  (f(a) = p & f(z) = q Thm*  ( Thm*  ((x:{a...z-1}, y:{x+1...z}. Thm*  (((u:{a...x}. f(u) = p) Thm*  ((& f(x+1)  p Thm*  ((& f(y-1)  q Thm*  ((& (u:{y...z}. f(u) = q)))

1

1. n :  2. p : Peg 3. q : Peg 4. p  q 5. a :  6. z : {a...} 7. f:({a...z}Peg).  7. f(a) = p & f(z) = q 7.  7. (x:{a...z-1}, y:{x+1...z}. 7. ((u:{a...x}. f(u) = p) & f(x+1)  p & f(y-1)  q & (u:{y...z}. f(u) = q)) 8. s : {a...z}{1...n}Peg 9. s is a Hanoi(n disk) seq on a..z 10. s(a) = (i.p) 11. s(z) = (i.q)   x:{a...z-1}, y:{x+1...z}, p',q':Peg.   (u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q)   & s(x) = (i.p')  {1...n-1}Peg & s(y) = (i.q')  {1...n-1}Peg   & p  p'   & q  q'

23 steps

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