(15steps 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 lb 1 1 1 1

1. n : 
2. n1:
2. n1<n
2. 
2. (p,q:Peg.
2. (p  q
2. (
2. ((a:z:{a...}, s:({a...z}{1...n1}Peg).
2. ((s is a Hanoi(n1 disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q)
2. ((
2. (((2^n1)z-a+1))
3. p : Peg
4. q : Peg
5. p  q
6. a : 
7. z : {a...}
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)
12. n  0
13. x : {a...z-1}
14. y : {x+1...z}
15. p' : Peg
16. q' : Peg
17. u:{a...x}. s(u,n) = p
18. u:{y...z}. s(u,n) = q
19. s(x) = (i.p')
20. s(y) = (i.q')
21. p  p'
22. q  q'
  s is a Hanoi(n-1 disk) seq on a..x


By: BackThru: 
Thm*  n':n:{n'...}, a:z:{a...}, s:({a...z}{1...n}Peg).
Thm*  s is a Hanoi(n disk) seq on a..z
Thm*  
Thm*  (x:{a...z}, i:{n'+1...n}. s(a,i) = s(x,i))
Thm*  
Thm*  s is a Hanoi(n' disk) seq on a..z


Generated subgoals:

1   s is a Hanoi(n disk) seq on a..x
1 step
2 23. x1 : {a...x}
24. i : {n-1+1...n}
  s(a,i) = s(x1,i)

1 step

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

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