(7steps 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 general exists lemma2PROG endpoint 1 2 1 1
1. n : 
2. n1:. 
2. n1<n
2. 
2. (p,q:Peg.
2. (p  q
2. (
2. ((a:. 
2. ((1of(HanoiSTD(n1 disks; from: p; to: q; indexing from: a)) = a+(2^n1)-1))
3. p : Peg
4. q : Peg
5. p  q
6. a : 
7. n  0
8. p  otherPeg(p; q)
9. otherPeg(p; q)  q
10. 1of(HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a))
10. =
10. a+(2^(n-1))-1
11. m : {a...}
12. s1 : {a...m}{1...n-1}Peg
13. m = 1of(HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a))
  1of(HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)
  1of(/z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2>)
  =
  a+2(2^(n-1))-1
By: Inst: Hyp:2 Using:[n-1 | otherPeg(p; q) | q | m+1]
THEN
LetTuple
(<z,s2> = HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1))
THEN
Analyze-1 THEN Thin Hyp:-1 THEN OnAllClauses Reduce

Generated subgoal:

1 14. 1of(HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1))
14. =
14. m+1+(2^(n-1))-1
15. z : {m+1...}
16. {m+1...z}{1...n-1}Peg
17. z
17. =
17. 1of(HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1))
  z = a+2(2^(n-1))-1
Auto

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

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