HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
3Thm*  n:, f,g:({1...n}Peg).
Thm*  f(n) = g(n)
Thm*  
Thm*  (a:, z:{a...}.
Thm*  ((s:({a...z}{1...n-1}Peg). 
Thm*  ((s is a Hanoi(n-1 disk) seq on a..z
Thm*  ((& s(a) = f  {1...n-1}Peg
Thm*  ((& s(z) = g  {1...n-1}Peg)
Thm*  (
Thm*  ((s:({a...z}{1...n}Peg). 
Thm*  ((s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g))		[hanoi_general_exists_lemma1]
cites the following:
2Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm*  nn'
Thm*  
Thm*  (h:({n+1...n'}Peg). 
Thm*  (s is a Hanoi(n disk) seq on a..z
Thm*  (
Thm*  ((s(?) {to n}  h {to n'}) is a Hanoi(n' disk) seq on a..z)		[hanoi_seq_deepen_seq]
1Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm*  nn'
Thm*  
Thm*  (h:({n+1...n'}Peg), i:{1...n'}.
Thm*  (in  (x:{a...z}. (s(?) {to n}  h {to n'})(x,i) = s(x,i)))		[hanoi_seq_deepen_loweq]
1Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm*  nn'
Thm*  
Thm*  (h:({n+1...n'}Peg), i:{1...n'}.
Thm*  (n<i  (x:{a...z}. (s(?) {to n}  h {to n'})(x,i) = h(i)))		[hanoi_seq_deepen_higheq]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
HanoiTowers Sections NuprlLIB Doc