(4steps 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 generalPROGcomp 1 1
1. n : 
2. p : Peg
3. q : Peg
4. p  q
5. 
6. n  0
  p  otherPeg(p; q)
By: BackThru: Thm*  x,y:Peg. x  y  x  otherPeg(x; y)

Generated subgoals:

None

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

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