(26steps total) Remark PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi general exists lemma2PROGworks

  n:a:z:{a...}, m:{a...z-1}, f,g:({1...n}Peg).
  f(n g(n)
  
  (s1:({a...m}{1...n-1}Peg), s2:({m+1...z}{1...n-1}Peg).
  (s1 is a Hanoi(n-1 disk) seq on a..m
  (s1(a) = f  {1...n-1}Peg
  (s2 is a Hanoi(n-1 disk) seq on m+1..z
  (s2(z) = g  {1...n-1}Peg
  (s1(m) = s2(m+1)
  (& (i:{1...n-1}. s1(m,i f(n) & s2(m+1,i g(n))
  (
  ((HanoiHelper(ns1fs2g)/r1,r2.
  (((r1 @(mr2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g))


By: Auto


Generated subgoal:

1 1. n : 
2. a : 
3. z : {a...}
4. m : {a...z-1}
5. f : {1...n}Peg
6. g : {1...n}Peg
7. f(n g(n)
8. s1 : {a...m}{1...n-1}Peg
9. s2 : {m+1...z}{1...n-1}Peg
10. s1 is a Hanoi(n-1 disk) seq on a..m
11. s1(a) = f  {1...n-1}Peg
12. s2 is a Hanoi(n-1 disk) seq on m+1..z
13. s2(z) = g  {1...n-1}Peg
14. s1(m) = s2(m+1)
15. i:{1...n-1}. s1(m,i f(n) & s2(m+1,i g(n)
  HanoiHelper(ns1fs2g)/r1,r2.
  (r1 @(mr2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g

25 steps

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

(26steps total) Remark PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc