(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 otherpeg diff2 1 1
1. x : Peg
2. y : Peg
3. x  y
  otherPeg(y; x)  y
By: BackThru: Thm*  x,y:Peg. x  y  otherPeg(x; y)  x

Generated subgoal:

1   y  x
1 step

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

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