(19steps total) PfGloss PfGloss PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi sol2 ala general 2 1
1. n : 
2. 0<n
3. p,q:Peg.
3. p  q
3. 
3. (a:. 
3. (z:{a...}, s:({a...z}{1...n-1}Peg).
3. (s is a Hanoi(n-1 disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. a : 
  z:{a...}, m:{a...z-1}, s1:({a...m}{1...n}Peg),
  s2:({m+1...z}{1...n}Peg).
  (s1 @(m) s2) is a Hanoi(n disk) seq on a..z & s1(a) = (i.p) & s2(z) = (i.q)
By: p = otherPeg(p; q) | otherPeg(p; q) = q  Asserted
THEN
(Inst: 3 Using:[p | otherPeg(p; q) | a]
(THEN
(Inst: 3 Using:[otherPeg(p; q) | q | m+1]
(THEN
(Witness: z | m)

Generated subgoals:

1   p = otherPeg(p; q)
1 step
2 8. p = otherPeg(p; q)
  otherPeg(p; q) = q
1 step
3 8. p = otherPeg(p; q)
9. otherPeg(p; q) = q
10. m : {a...}
11. s1 : {a...m}{1...n-1}Peg
12. s1 is a Hanoi(n-1 disk) seq on a..m
13. s1(a) = (i.p)
14. s1(m) = (i.otherPeg(p; q))
15. z : {m+1...}
16. s2 : {m+1...z}{1...n-1}Peg
17. s2 is a Hanoi(n-1 disk) seq on m+1..z
18. s2(m+1) = (i.otherPeg(p; q))
19. s2(z) = (i.q)
  s1:({a...m}{1...n}Peg), s2:({m+1...z}{1...n}Peg).
  (s1 @(m) s2) is a Hanoi(n disk) seq on a..z
  & s1(a) = (i.p)  {1...n}Peg
  & s2(z) = (i.q)  {1...n}Peg
6 steps

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

(19steps total) PfGloss PfGloss PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc