(5steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi peg perm comp2 1 2
1. p : Peg
2. r : Peg
3. q : Peg
4. s : Peg
5. p  q
6. r  s
7. q  p
  if q=q s else otherPeg(r; s) fi = s
By: SplitITE Concl

Generated subgoal:

1 8. q  q
  otherPeg(r; s) = s
1 step

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

(5steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc