(2steps 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 comp1

  p,r,q,s:Peg. p  q  r  s  permute(p to r ; q to s)(p) = r

By: Compute
Copermute(p to r ; q to s)(p) * if p=p r ; p=q s else otherPeg(rs) fi


Generated subgoal:

1 1. p : Peg
2. r : Peg
3. q : Peg
4. s : Peg
5. p  q
6. r  s
  if p=p r ; p=q s else otherPeg(rs) fi = r

1 step

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

(2steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc