# binary tree with parent pointers and post-order successor pointers

type Node = {
  data left,right:Node;
  pointer post:Node[POST(this,post)]; /* post-order successor */
  pointer parent:Node[PARENT(this,parent)];
}

/* b is parent of a or null if root */
pred PARENT(pointer a,b:Node) = a^Node.left union a^Node.right={b};

/* a is leaf */
pred LEAF(pointer a:Node) = a.left=null & a.right=null;

/* p is root in some tree */
pred ROOT(pointer p:Node) = empty(p^Node.left union p^Node.right) & p!=null;

/* a is less than or equal to b and both nodes are below c in some tree */
pred LESSEQ(pointer a,b,c:Node) = 
 c<(left+right)*>b & b<(left+right)*>a |
 existpos d of Node: c<(left+right)*>d & d.left<(left+right)*>a & d.right<(left+right)*>b;

/* b is post-order cyclic successor of a, i.e.:
    if a is leaf:
      if a is root:  b is same as a
      if a is a right-successor: b is parent of a
      if a is a left-successor: 
         if a's parent has a right-successor: b is smallest element in right subtree of a's parent
         otherwise: b is parent of a
    if a is not leaf: b is smallest element in subtree of a */
pred POST(pointer a,b:Node) =
  a!=null & b!=null &
  (LEAF(a) => 
    (ROOT(a) => b=a) &
    (allpos p of Node: p.right=a => b=p) &
    (allpos p of Node: p.left=a  => 
      (p.right!=null => allpos c of Node: p.right<(left+right)*>c => LESSEQ(b,c,p.right)) &
      (p.right=null => b=p))) &
  (!LEAF(a) => allpos c of Node: a<(left+right)*>c => LESSEQ(b,c,a));

/* b is post-order cyclic successor of a, except if a=p in which case b is null */
pred ALMOSTPOST(pointer a,b,p:Node) = 
 (a!=p => POST(a,b)) &             
 (a=p => b=null);

data tree:Node;
pointer x:Node;

# nullify post pointer
proc destroy():void 
[x!=null]
{
  x.post = null;
}
[true {Node.post[ALMOSTPOST(this,post,x)]}]

# auxiliary procedure for finding smallest subnode
proc findsmallest(pointer t:Node):Node
  pointer T:Node;
[t!=null & T=t {Node.post[ALMOSTPOST(this,post,x)]}]
{
  while [t!=null & T<(left+right)*>t &
         allpos c of Node: LESSEQ(c,t,T) => t<(left+right)*>c
        {Node.post[ALMOSTPOST(this,post,x)]}]
        (t.left!=null | t.right!=null) {
    if (t.left!=null) {
      t = t.left;
    }
    else {
      t = t.right;
    }
  }
  return t;
}
[allpos c of Node: T<(left+right)*>c => LESSEQ(return,c,T) {Node.post[ALMOSTPOST(this,post,x)]}]

# reestablish valid post pointer
proc fix():void 
[x!=null {Node.post[ALMOSTPOST(this,post,x)]}]
{ 
  if (x.left=null & x.right=null) {
    if (x.parent=null) {
      x.post = x;
    }
    else {
      if (x.parent.right=null | x.parent.right=x) {
        x.post = x.parent;
      }
      else {
        x.post = findsmallest(x.parent.right) 
         [x!=null & x.left=null & x.right=null & x.parent!=null & x.parent.right!=null &
          x.parent.right!=x & findsmallest.T=x.parent.right];
      }
    }
  }
  else {
    x.post = findsmallest(x) [x!=null & (x.left!=null | x.right!=null) & findsmallest.T=x];
  }
}
[true]

# example application
proc main(pointer t:Node):void 
[t!=null]
{
  x = t;
  destroy() [x!=null];
  fix() [true];
}
[true]