# 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 inv(pointer p:Node) = 
  black(p) &
  allpos q of Node: p<(left+right)*>q  => 
   (red(q) => black(q.left) & black(q.right));

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));

data root:Node;

proc treeinsert(data z:Node):void
  pointer Z,Q:Node;
[z.left=null & z.right=null & Z=z & inv(root) & Q=root]
{
  pointer y,x:Node;
  bool c;
  x = root;
  while [Z=z & z.left=null & z.right=null & 
         (x!=root => root<(left+right)*>y & (y.left=x & c=true | y.right=x & c=false)) & 
         (x=root => y=null & x=root) & inv(root) & Q=root] 
        (x!=null) {
    y = x;
    c = ? /* z.key < x.key */; # ensure consistent choice
    if (c) {
      x = x.left;
    }
    else {
      x = x.right;
    }
  }
  z.p = y;
  if (y=null) {
    root = z;
  }
  else {
    if (c) {
      y.left = z;
    }
    else {
      y.right = z;
    }
  }
  z = null; # ensure disjointness
}
[root<(left+right)*>Z & Z.left=null & Z.right=null & almostinv1(root,Z) & 
 (black(root) | root=Z) & (Q!=null => root=Q)]