Def  permute(p to r ; q to s)(u) == if u=p r ; u=q s else otherPeg(r; s) fi

is mentioned by

Thm*  p,r,q,s:Peg. p  q  r  s  permute(p to r ; q to s)(q) = s	[hanoi_peg_perm_comp2]
Thm*  p,r,q,s:Peg. p  q  r  s  permute(p to r ; q to s)(p) = r	[hanoi_peg_perm_comp1]
Thm*  p,r,q,s:Peg. p  q  r  s  Inj(Peg; Peg; permute(p to r ; q to s))	[hanoi_peg_perm_is_inj]

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html