(10steps total) 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 generalPROG wf
  n:, p,q:Peg.
  p  q
  
  (a:. 
  (HanoiSTD(n disks; from: p; to: q; indexing from: a)
  ( z:{a...}({a...z}{1...n}Peg))
By: CompNatInd Concl THEN UnivCD

Generated subgoal:

1 1. n : 
2. n1:. 
2. n1<n
2. 
2. (p,q:Peg.
2. (p  q
2. (
2. ((a:. 
2. ((HanoiSTD(n1 disks; from: p; to: q; indexing from: a)
2. (( z:{a...}({a...z}{1...n1}Peg)))
3. p : Peg
4. q : Peg
5. p  q
6. a : 
  HanoiSTD(n disks; from: p; to: q; indexing from: a)
   z:{a...}({a...z}{1...n}Peg)
9 steps

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

(10steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc