# from 'Introduction to Algorithms', chapter 14 type Node = { bool color; # false=red, true=black data left,right:Node; pointer p:Node[this^Node.left union this^Node.right={p}]; } pred red(pointer p:Node) = p.color=false; pred black(pointer p:Node) = p.color=true | p=null; pred almostinv1(pointer p,r:Node) = allpos q of Node: p<(left+right)*>q => (red(q) => (black(q.left) | q.left=r) & (black(q.right) | q.right=r)); pred almostinv2(pointer p,r:Node) = allpos q of Node: p<(left+right)*>q => (red(q) => (black(q.left) | q.left=r | q=r) & (black(q.right) | q.right=r | q=r)); data root:Node; proc rightrotate(pointer x:Node):void pointer B,X,Y,P,Q:Node; [root!=null & root<(left+right)*>x & x.left!=null & (almostinv1(root,x.left) | almostinv1(root,x)) & red(x) & B=x.left.right & X=x & Y=x.left & P=x.p & Q=root] { pointer y:Node; y = x.left; x.left = y.right; if (y.right!=null) { y.right.p = x; } y.p = x.p; if (x.p=null) { root = y; } else { if (x=x.p.right) { x.p.right = y; } else { x.p.left = y; } } y.right = x; x.p = y; } [Y.right=X & X.left=B & P=Y.p & root<(left+right)*>X & almostinv2(root,X) & red(X) & (P=null => root=Y) & (P!=null => root=Q)]