RingIndex(I, J): trait 
  introduces  
     first:             -> I
     left, right: I     -> I
     name:        I     -> J
     inbetween: I, I, I -> Bool
  asserts with i, j, k: I
    sort I generated by first, right;
    \E i (right(i) = first);
    right(i) = right(j) <=> i = j;
    left(right(i)) = i;
    name(i) = name(j) <=> i = j;
%inbetween(i,j,k) holds when j occurs on the shortest path from i to k
    inbetween(i,j,j);
    (inbetween(i,j,k) /\ right(k) ~= i) => inbetween(i,j,right(k));
    (inbetween(i,j,k) /\ i ~= j /\ j ~= k ) => ~ inbetween(k,j,i)