(28steps total) 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 via permshift 2 1 3

1. n : 
2. 0<n
3. p,q:Peg.
3. p  q
3. 
3. (z:{1...}, s:({1...z}{1...n-1}Peg).
3. (s is a Hanoi(n-1 disk) seq on 1..z & s(1) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. p  otherPeg(pq)
8. otherPeg(pq q
9. m : {1...}
10. s1 : {1...m}{1...n-1}Peg
11. s1 is a Hanoi(n-1 disk) seq on 1..m
12. s1(1) = (i.p)
13. s1(m) = (i.otherPeg(pq))
  z:{1...}, m:{1...z-1}, s1:({1...m}{1...n}Peg),
  s2:({m+1...z}{1...n}Peg).
  (s1 @(ms2) is a Hanoi(n disk) seq on 1..z
  s1(1) = (i.p {1...n}Peg
  s2(z) = (i.q)


By: (q  p  Peg  By SimilarTo: p = q  Peg ; Id)
THEN
FwdThru: 
Thm*  n:a,z:s:({a...z}{1...n}Peg).
Thm*  s is a Hanoi(n disk) seq on a..z
Thm*  
Thm*  (f:(PegPeg). 
Thm*  (Inj(Peg; Peg; f (x,if(s(x,i))) is a Hanoi(n disk) seq on a..z)
on [ Hyp:11 ]
Using:[permute(p to otherPeg(pq) ; otherPeg(pq) to q)]


Generated subgoals:

1   Inj(Peg; Peg; permute(p to otherPeg(pq) ; otherPeg(pq) to q))
1 step
2 14. (x,i. permute(p to otherPeg(pq) ; otherPeg(pq) to q)(s1(x,i)))
14. is a Hanoi(n-1 disk) seq on 1..m
  z:{1...}, m:{1...z-1}, s1:({1...m}{1...n}Peg),
  s2:({m+1...z}{1...n}Peg).
  (s1 @(ms2) is a Hanoi(n disk) seq on 1..z
  s1(1) = (i.p {1...n}Peg
  s2(z) = (i.q)

13 steps

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

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