(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
1. p : Peg
2. r : Peg
3. q : Peg
4. s : Peg
5. p  q
6. r  s
  if q=p r ; q=q s else otherPeg(r; s) fi = s
By: SplitITE Concl

Generated subgoals:

1 7. q = p
  r = s
1 step
2 7. q  p
  if q=q s else otherPeg(r; s) fi = s
2 steps

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

(5steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc