In order to prove that R2 holds in $N$, we must show that no node other than $\n$ is confluent in $N$, i.e., that every node except for $\n$ is tree-like in $N$. Since $M$ is regular, there are no cycles in $M$ by lemma \ref{Lem4.14}. In addition, since $M$ is regular, R2 holds in $M$, and since $\ControlF^M(\Sys)=f6$, we have that there are no confluent nodes in $M$. Also, we have from the control-dependent invariants of Figure \ref{cdLM} that $\n\arrow\r$ in $M$. From these facts we can conclude that there is no path from $\ell_0$ to $\r$ in $M$, otherwise either $\r$ would be confluent in $M$ (if the path from $\ell_0$ to $\r$ does not go through $\n$), or there would be a cycle going through $\n$ (since $\n\arrow\r$ in $S$).

Additionally, since we know there are no cycles or confluent nodes in $M$, all of the path-connected nodes are tree-like in $M$, from which we can conclude that $\KeyF(\ell_0)<\KeyF(\n)<\KeyF(\rl)<\KeyF(\r)$. Note also that $\KeyF(\new)=\KeyF(\n)$ in $N$, and so $\KeyF(\ell_0)<\KeyF(\n)=\KeyF(\new)<\KeyF(\rl)<\KeyF(\r)$ in $N$. As a result, the addition of the arc $(\r, \new)$ such that $\LeftF(\r)=\new$ and the arc $(\new,\ell_0)$ such that $\LeftF(\new)=\ell_0$ cannot make any node from $M$ become non-tree-like in $N$, except for $\n$. Finally, since $\n$ is tree-like in $M$ and $\KeyF(\new)=\KeyF(\n)$ in $N$ and $\LeftF(\new)=\ell_0$ and $\RightF(\new)=\rl$, $\new$ is also tree-like in $N$. We conclude that $R2$ holds in $N$.

We prove that $\Set(N)=\Set(M)$: States $M$ and $N$ have the same extensions of
predicates \RemovedP\ and \DeletedP\ on the nodes of $M$, and Node \new\ has the same
key as node $\n$. We also showed that this step does not change the $k$-connectivity of any node from $M$ in $N$ for any $k$.
Thus, it must be the case that $\Set(N)=\Set(M)$.

\paragraph*{Assume $s\in\Step(\Sys, \rom{f7})$.} In this step, arc $(\n , \ell_0)$ of $M$ is replaced by arc $(\n,\r)$ of $N$.
As in the previous case ($s\in\Step(\Sys,rom{f6})$), any two nodes $x,y$ that are connected in $M$ are connected in $N$, because the removed
arc $(\n, \ell_0)$ can be replaced by the path $\n\arrow\r\arrow\new\arrow\ell_0$ of $N$. In the same manner as before, with the help of Step-property \ref{Cm2}, we can conclude that for every node $x$ in $M$ and any $k\in\KeyT$, if $x\neq\bot$ is potentially $k$-connected in $M$ then it is potentially $k$-connected in $N$. This gives us that $\prt$ is $\KeyF(\n)$-connected in $N$ and that $\nd_p$ and $\nxt_p\neq\bot$ are potentially $k_p$-connected for any $p$ in $N$, from which we get that R0 and R1 hold in $N$.

To prove that R2 holds in $N$, let $x$ be an address of $N$ that is path-connected
but not tree-like in $N$. Since obviously $\ControlF(\Sys)^T \in \{\rom{f7, f8, r7, r8}\}$, we must show that and that $x=\n$.
Assume that $x\neq \n$. Since $x\neq\n$, $y=\LeftF^M(x)=\LeftF^N(x)$
and $z=\RightF^M(x)=\RightF^N(x)$ (because only arc $(\n,\ell_0)$ is removed by the step). And just as any other node,
$y$ (and $z$) have the same descendants in $N$ as in $M$, meaning that $x$ is not tree-like in $M$, contradicting the regularity of $M$.
We conclude that such an $x$ does not exist, and R2 holds in $N$.

Finally, as was the case before, $\Set(N) = \Set(M)$, since $M$ and $N$ have the same addresses and same extension of predicate
$\DeletedP$, and the step does not change the $k$-connectivity of any node from $M$ in $N$ for any $k$.

\paragraph*{Assume $s\in\Step(\Sys,\rom{f8})$.} In this step, arc $(\prt, \n)$ of $M$ is replaced by arc $(\prt, \r)$ or $N$.
This case is slightly different from the previous two cases; this time we can show that the connectivity of every pair of nodes $x,y$ of $M$ is preserved by the step {\em if $y\neq\n$}: Since $\prt\neq\bot$ is not removed by the control-dependent invariants of Figure \ref{cdLM}, and by Corollary \ref{lemma:pdc-rem-or-locked}, we have that $\prt$ is path-connected in $M$. By the control-dependent invariants of Figure \ref{cdLM}, there are paths from $\prt$ to $\ell_0$ and from $\prt$ to $\r$ in $M$ (via $(\prt,\n)$,$(\n,\ell_0)$ and via $(\prt,\n)$,$(\n,\r)$, respectively). So, using the same arguments as before, the potential $k$-connectivity of any node $y$ for any $k\in\KeyT$ is preserved by the step except in a small number of cases:
\begin{enumerate}
\item $y=\n$ in $M$: If $\n$ is still path-connected in $N$, then nothing changes, and the claim holds. Otherwise, $\n$ is not path-connected in $N$, then it is pre-removed in $N$ by the fact that it is not removed (control-dependent invariants of Figure \ref{cdLM}) and by Corollary \ref{lemma:pdc-rem-or-locked}. So we must show that if $\n$ is $k$-connected for some $k\in\KeyT$ in $M$, then PT2$(\n,k)$ holds in $N$.

Since $M$ is regular and $\prt$ is path-connected, then $\prt$ is tree-like in $M$. We assumed that $\n=\LeftF(\prt)$ (we are proving the case that $\lft=\TRUE$), and so $\KeyF(\n)<\KeyF(\prt)$ and also $\KeyF(\r)<\KeyF(\prt)$ ($\r$ is a left-descendant of $\prt$). So for any $k$ for which $\n$ is $k$-connected in $M$, $k<\KeyF(\prt)$. Next, we know that $T\models\r=\LeftF(\prt)$, and so $\r$ is trivially $k$-connected in $N$. Thus PT2$(\n,k)$ must hold in $N$, since $\n\arrow\r$ in $N$.

\item $y\neq\n$ and PT3$(y,k)$ holds in $M$, and $\n$ is the $k$-connected ``anchor'' of $y$ from those definitions (see Definition \ref{DefPot}): As before, if $\n$ is still path-connected in $N$, then nothing changes, and the claim holds. Otherwise, by the previous bullet, PT2$(\n,k)$ and so PT3$(y,k)$ holds in $N$ by Definition \ref{DefPot}).

Note that it is impossible that PT2$(y,k)$ holds if $y\neq\n$, since by Inductive invariant \ref{inv:pre-rem}, only $\n$ can be pre-removed.
\end{enumerate}
Thus R1 holds in $N$.

Since $M$ is regular, $\prt$ is not a descendant of $\n$ in $M$. This follows from the fact that $(\prt, \n)$ is an arc of $M$, and there are no cycles in a regular state (by lemma \ref{Lem4.14}). From this and the proof that R1 holds in $N$, it follows that $\prt$ remains $\KeyF(\n)$-connected in $N$, since it is $\KeyF(\n)$-connected in $M$. Thus R0 holds in $N$.

We now prove R2 holds in $N$. Since $\ControlF(\Sys) = \rom{f9} \notin\{\rom{f7,f8,r7,r8}\}$ in $N$, we must show that all path-connected nodes are tree-like in
$N$. Since $M$ is regular and $\ControlF^M(\Sys) = \rom{f8}$, all path-connected nodes are tree-like, except for $\n$. We show that $\n$ is not path-connected in $N$, and that $\prt$ remains tree-like in $N$, from which we conclude that all path-connected nodes are tree-like in $N$ (since only $\LeftF(\prt)$ changes in the step, showing $\prt$ remains tree-like suffices). We argued above that $\prt$ is path-connected $M$, and so $\n$ is path-connected in $M$.

We claim that $\n$ is not confluent in $M$: If there were a path-connected node $x\neq\prt$ such that $x\arrow\n$ in $s$, then $\prt$ and $x$ would have some common ancestor $z$ such that $\n\in\LeftDes(z)$ and also $\n\in\RightDes(z)$. Since there are no cycles in $M$ (by lemma \ref{Lem4.14}), $z\neq\n$, meaning $z$ is not tree-like in $M$, contradicting the regularity of $M$. So $\n$ is path-connected in $M$ only via the arc $(\prt, \n)$, which is removed by the step, and so $\n$ is not path-connected in $N$.

That $\prt$ remains tree-like in $N$ is trivial, since we already know that $\LeftF(\prt)=\r$ in $N$, but $\r\in\LeftDes(\prt)$ in $M$. Thus R2 holds in $N$.

Finally, we show that $\Set(N) = \Set(M)$: $M$ and $N$ have the same addresses and same extension of predicate
$\DeletedP$. We also showed that this step does not change the $k$-connectivity of any node from $M$ in $N$ for any $k$, except for node $\n$.
So it remains to show that $\new$ is $\KeyF(\new)=\KeyF(\n)$-connected in $N$.
Lemma \ref{lemma:tree-like-path} states that if every path-connected node is tree-like then every $x$ is $\KeyF(x)$-connected.
This observation holds in our case, since we showed that R2 holds in $N$, which means that every path-connected node is tree-like in $N$.
Thus, it must be the case that $\Set(N)=\Set(M)$.

\paragraph*{Assume $s\in\Step(\Sys, \rom{f9})$.} In this step, $\LeftF$, $\RightF$ and $\AddressT$ have the same interpretations in both $M$ and $N$, $\nd_p^M=\nd_p^N$ and $\nxt_p^M=\nxt_p^N$ for every working process $p>0$, and likewise the denotations of $\n$ and $\prt$ do not change. It is obvious for every address $x\neq \n$ and key value $k$ that $x$ is potentially $k$-connected in $M$ if and only if $x$ is potentially $k$-connected in $N$.
Thus R0 holds in $N$.

Since $\n$ is marked as removed by the step, To prove that R1 holds in $N$,
we must show that for any $k\in\KeyT$, $\n$ is potentially $k$-connected in $N$ if and only if it is potentially $k$-connected in $M$.
Since $M$ is regular and $\ControlF(\Sys)=\rom{f9}\not\in \{\rom{f7, f8, r7, r8}\}$, every path connected node of $M$ is tree-like.
From the control-dependent invariants of Figure \ref{cdLM}, we have that $\n$ is focused, and so not tree-like, meaning it cannot be path-connected in $M$.
Since $\n$ is not removed in $M$, it is pre-removed in $M$.
If $\n$ is potentially $k$-connected in $M$, then PT2$(\n, k)$ holds in $M$, and since $\ControlF(\Sys)=\rom{f9}$, $\r$ is
$k$-connected in $M$. Thus $\r$ is $k$-connected in $N$, and so PT3$(\n,k)$ holds in $N$.
We conclude that R1 holds in $N$.

R2 trivially holds in $N$ if and only if it holds in $M$, since $\LeftF$, $\RightF$ and $\AddressT$ have the same interpretations in $M$ and in $N$.

Finally, $\Set(M)=\Set(N)$ holds trivially, since $\LeftF$, $\RightF$ and $\AddressT$ and $\DeletedP$ have the same interpretations in $M$ and in $N$.

\paragraph*{Assume $s\in\Step(\Sys,\rom{v6})$.} In this step, arc $(\prt,\n)$ of $M$ is replaced with arc $(\prt,\child)$ of $N$. The proof for this step is nearly identical to that of $s\in\Step(\Sys,\rom{f8})$ above, with the only real difference being in the proof that $\Set(M)=\Set(N)$.

R0 and R1 hold in $N$ by the same reasoning as for $s\in\Step(\Sys,\rom{f8})$: the connectivity of every pair of nodes $x,y$ of $M$ is preserved by the step {\em if $y\neq\n$}, using the same arguments. The same two special cases for where $\n$ is involved are handled in the same way, using $\child$ instead of $\r$.

The proof that R2 holds in $N$ is also very similar, once again substituting $\r$ with $\child$.

Finally, we show that $\Set(N) = \Set(M)$: $M$ and $N$ have the same addresses and same extension of predicate
$\DeletedP$. We also showed that this step does not change the $k$-connectivity of any node from $M$ in $N$ for any $k$, except for node $\n$,
which becomes non-path-connected in $N$. As a result, we must show that $\KeyF(\n)\notin\Set(M)$.
By the control-dependent invariants of Figure \ref{cdLM}, we know that $\DeletedP(\n)$ in $M$.
In addition, since $M$ is regular and $\ControlF(\Sys)=\rom{v6}$ in $M$, R2 implies that all path-connected nodes are tree-like in $M$.
Thus, by Corollary \ref{cor:tree-like-path}, there are no two path-connected nodes with the same key in $M$, and so $\KeyF(\n)\notin\Set(M)$, since $\DeletedP(\n)$.
Thus $\Set(N) = \Set(M)$, as required.

\paragraph*{Assume $s\in\Step(\Sys, \rom{v7})$.} In this step, arc $(\n,\bot)$ of $M$ is replaced by arc $(\n, \prt)$ of $N$.

Once again, we claim that for every pair of nodes $x,y$ such that there is a path form $x$ to $y$ in $M$, there is a path from $x$ to $y$ in $N$. This is trivial (recall that the only descendant of $\bot$ is $\bot$ itself), except for the case that $y=\bot$. As before, since $M$ is regular, and with the help of stop-property \ref{Cm2}, for every node $z\neq\bot$ in $M$ and every $k\in\KeyT$, if $z$ is $k$-connected in $M$ then it is $k$-connected in $N$. Thus R0 holds in $N$.

Since the only arc that is changed by the step is an outgoing arc of $\n$, to prove R1 holds in $N$, it suffices to show that for any $k\in\KeyT$, if $\n$ is potentially $k$-connected in $M$ then it is potentially $k$-connected in $N$. So we must show that for every $k\in\KeyT$ such that $\n\arrow_k\bot$ holds in $M$, $\prt$ is $k$-connected in $N$. If we can show that $\n$ is pre-removed in $M$, then we get this conclusion ``for free'' from the definition of PT2$(\n,k)$ (see Definition \ref{DefPot}).

To show that $\n$ is pre-removed in $M$, we check two possibilities:
\begin{enumerate}
\item If $\child\neq\bot$, then since $\prt$ is $\KeyF(\n)$-connected in $M$, then it must be path-connected in $M$, and from the control-dependent invariants of Figure \ref{cdLM} we have that $\prt\arrow\child$. So if $\n$ were path connected in $M$, then $\child$ would be confluent in $M$. However, since R2 holds in $M$ and since $\ControlF(\Sys)=\rom{v7}$, this cannot be.
\item Assume $\child=\bot$. Since R2 holds in $M$ and since $\ControlF(\Sys)=\rom{v7}$, then all path-connected nodes in $M$ are tree-like. Then if $\n$ is path-connected, we have from Corollary \ref{cor:tree-like-path} that there is a single $\KeyF(\n)$-path from $\Root$ to $\n$ in $M$. Since $\prt$ is $\KeyF(\n)$-connected in $M$ by R0, then $\n$ must be a descendant of $\prt$ in $M$. Since $\lft=\TRUE$, then by R0, $\KeyF(\n)<\KeyF(\prt)$, and since $\prt$ is tree-like in $M$, we have that $\n\in\LeftDes(\prt)$ in $M$. However, since $\lft=\TRUE$, $\LeftF(\prt)=\bot$ in $M$, and $\LeftDes(\prt)=\emptyset$ (see Definition \ref{def:descendants}).
\end{enumerate}
In both cases, $\n$ cannot be path-connected in $M$, as required, and so R1 holds in $N$.

Since in both $M$ and $N$, $\ControlF(\Sys)\notin\{\rom{f7,f8,r7,r8}\}$, to prove that R2 holds in $N$, we have to prove that all path-connected nodes are tree-like in $N$.
It is easy to check that $M$ and $N$ have the same path-connected nodes,
and that for any path-connected node $x$, the left (correspondingly right) descendants of $x$ in $M$ and in $N$ form the same set.
So R2 holds in $N$ as well.

That $\Set(N)=\Set(M)$ follows immediately from the fact that $\DeletedP$ has the same extension in $M$ as in $N$,
and from our observations that for any path-connected node $x$, the left (correspondingly right) descendants of $x$ in $M$ and in $N$ form the same set.

\paragraph*{Assume $s\in\Step(\Sys, \rom{v8})$.} In this step, arc $(\n, \child)$ of $M$ is replaced with arc $(\n, \prt)$ of $N$.

By control-dependent invariants of Figure \ref{cdLM}, we have that in $M$: $\prt\arrow\child$, $\n\arrow\prt$, $\prt$ is not removed, and $\prt\neq\nd$. With the help of \ref{inv:pre-rem}, these facts imply that $\prt$ cannot be pre-removed in $M$. Since $M$ is regular, $\prt$ is $\KeyF(\n)$-connected in $M$. It follows that $\n$ cannot be an ancestor of $\prt$ in $M$ (otherwise, the $\KeyF(\n)$-path would end at $\n$ and not continue to $\prt$). Thus, $\n$ must be pre-removed in $M$, otherwise $\prt$ would confluent in $M$, since $\n$ points to $\prt$ but is not on the path $\Root\arrow_{\KeyF(\n)}^*\prt$.

Since the only arc removed by the step of an outgoing arc of $\n$, we conclude that all nodes that are path connected in $M$ are path connected in $N$. Since $M$ is regular, and by Step-property \ref{Cm2}, for every node $x$ in $M$ and every $k\in\KeyT$, if $x$ is $k$-connected in $M$, then it is $k$-connected in $N$. Thus R0 holds in $N$.

As in previous steps, since the only arc that changed by the step is an outgoing arc of $\n$, in order to prove that R1 holds in $N$, it suffices to show that for every $k\in\KeyT$ such that $\n$ is potentially $k$-connected in $M$, it is potentially $k$-connected in $N$. By control-dependent invariants of Figure \ref{cdLM}, we have that $\n$ is not removed in $M$, and we already argued that $\n$ is not path-connected in $M$. Thus $\n$ is pre-removed, and if $\n$ is potentially $k$-connected in $M$, then PT2$(\n,k)$ must hold in $M$. By the definition of PT2 (see Definition \ref{DefPot}), we have that $\prt$ is $k$-connected in $M$ and we already concluded it must also be $k$-connected in $N$. Thus $\n$ is potentially $k$-connected in $N$ as well (since $\LeftF(\n)=\RightF(\n)=\prt$ in $N$), and R1 holds in $N$.

For R2, we prove that all path-connected nodes $x\notin \{\Root,\bot\}$ in $N$ are tree-like. If $x$ is path-connected in $N$ then
it is path-connected in $M$, and hence it is a tree-like node in $M$,
and this implies that it is tree-like in $N$. Similar to the proof of R1, all nodes that were path connected in $M$ are path connected in $N$, and so R2 holds in $N$ as well.

Once again, $\Set(N)=\Set(M)$ follows immediately from the fact that $\DeletedP$ has the same extension in $M$ as in $N$, and from our observations that for any path-connected node $x$, the left (correspondingly right) descendants of $x$ in $M$ and in $N$ form the same set.

\paragraph*{Assume $s\in\Step(\Sys,\rom{v9})$.} The proof for this case if identical to the proof for the case of $s\in\Step(\Sys,\rom{f9})$, for all practical purposes.

\underline{This ends the proof that regularity is an inductive invariant.}
\end{proof}

\begin{SP}
\label{sp:rem-children}
Let $(M, N)$ be a step of the algorithm. If $x\in\AddressT^M$ and $\RemovedP(x)^M$, then $\LeftF^M(x)=\LeftF^N(x)$ and $\RightF^M(x)=\RightF^N(x)$.
\end{SP}

\begin{proof}
This is exactly what Corollary \ref{cor:constantly-focused} states.
\end{proof}

\begin{SP}[uses: \ref{Cl4.9}, \ref{cor:tree-like-path}]
\label{sp:pkc-after-disconnect}
Let $(M, N)$ be a step such that $M$ is regular, let $x\neq\bot$ be an address of $M$, and let $k\in\omega$ be a key value
such that $M\models\Root\arrow_k^* x$ but $N\models\Root\notarrow_k^* x$. Then $x$ is potentially $k$-connected in $N$.

In addition, if $k=\KeyF(x)$, then both $\Root\arrow_k^*\LeftF(x)$ and $\Root\arrow_k^*\RightF(x)$ in $N$.
\end{SP}

\begin{proof}
Since $N\models\Root\notarrow_k^* x$, Step-Property \ref{Cm2} implies that $N\models \Root\notarrow^* x$.
Thus, by lemma \ref{Cl4.9}, $(M,N)$ executes either f8, r8 or v6, and so $x=\n$.

If the step executes f8, then $\n=\LR(\prt,\lft)$ in $M$, and $\r=\LR(\prt,\lft)$ in $N$, and $\RightF(\n)=\LeftF(\n)=\r$ in both $M$ and $N$.
By the regularity of $M$:
\begin{enumerate*}[label=(\arabic*)]
\item $\prt$ is $k$-connected in $M$, and so also in $N$ (arc $(\prt,\n)$ is not an arc of path $\Root\arrow^*\prt$);
\item $\n$ is not confluent in $M$, and so path-connected in $N$; and
\item since $\prt\arrow_k\n$ in $M$, then $\prt\arrow_k\r$ in $N$, and so PT2$(\n,k)$ holds in $N$.
\end{enumerate*}
We conclude that the claim holds.

If the step executes v6, then $\n=\LR(\prt,\lft)$ in $M$, and $\child=\LR(\prt,\lft)$ in $N$, and $\n\arrow\child\wedge \n\arrow\bot$ in both $M$ and $N$.
By the regularity of $M$:
\begin{enumerate*}[label=(\arabic*)]
\item $\prt$ is $k$-connected in $M$, and so also in $N$ (arc $(\prt,\n)$ is not an arc of path $\Root\arrow^*\prt$);
\item $\n$ is not confluent in $M$, and so path-connected in $N$; and
\item since $\prt\arrow_k\n$ in $M$, then $\prt\arrow_k\child$ in $N$.
\end{enumerate*}
We know that $\Set(M)=\Set(N)$. If $k\in\Set(N)=$ then $\n\notarrow_k\bot$ in $M$, and so PT2$(\n, k)$ holds in $N$ via $\n\arrow\child$.
Otherwise, $k\notin\Set(N)$, and so $\child\arrow^*_k\bot$, implying that $\bot$ is $k$-connected, and so PT2$(\n, k)$ holds in $N$ via $\n\arrow\bot$.
If $k=\KeyF(\n)$, then $k\notin\Set(N)$, and we already showed that both $\bot$ and $\child$ are $k$-connected in $N$.
\end{proof}

\begin{SP}
\label{sp:pdc-remains-pkc}
Let $s=(M, N)$ be a step such that $M$ is regular, let $k\in\omega$ be a key value, and let $x\in\AddressT$ such that $\Root\notarrow^* x$ and $x$ is potentially $k$-connected in $M$. Then $x$ is potentially $k$-connected in $N$.
\end{SP}

\begin{proof}
Since key-values are immutable, it suffices to prove the claim for steps that change $\LeftF$ or $\RightF$.

Note that $x\neq\bot$, since $\bot$ is always path-connected.

\begin{description}
\item[$s\in\Step(p,i3)$:] Since this step only removes arc $(y,\bot)$, it is impossible that the step changes the potential-connectivity of any node.
\item[$s\in\Step(\Sys,f6)$:] Clearly, any node $x$ that was potentially connected in a way dependent on the arc $(\r,\rl)$ remains potentially connected via the arcs $(\r,\new)$ and $(\new,\rl)$.
\item[$s\in\Step(\Sys,f7)$:] Clearly, any node $x$ that was potentially connected in a way dependent on the arc $(\n,\ell_0)$ remains potentially connected via the arcs $(\n,\r)$, $(\r,\new)$, and $(\new,\ell_0)$.
\item[$s\in\Step(\Sys,f7)$:] Clearly, any node $x$ that was potentially connected in a way dependent on the arc $(\prt,\n)$ remains potentially connected via the arcs $(\prt,\r)$.
\item[$s\in\Step(\Sys,v6)$:] Clearly, any node $x$ that was potentially connected in a way dependent on the arcs $(\prt,\n)(\n,\child)$ remains potentially connected via the arcs $(\prt,\child)$.
\item[$s\in\Step(\Sys,v7)$:] Since this step only disconnects $\bot$ from $\n$, the claim holds trivially.
\item[$s\in\Step(\Sys,v8)$:] Clearly, any node $x$ that was potentially connected in a way dependent on the arc $(\n,\child)$ remains potentially connected via the arcs $(\n,\prt)$ and $(\prt,\child)$.
\end{description}
\end{proof}

\begin{SP}
\label{sp:dc-chd-leads-to-chd}
Let $s=(M, N)$ be a step such that $M$ is regular, and let $x\in\AddressT$ such that $M\models\Root\notarrow^* x$, and either $\LeftF^M(x)\neq\LeftF^N(x)$ or $\RightF^M(x)\neq\RightF^N(x)$. Let $y$ be the new child of $x$ in $N$, and let $z$ be the child that did not change. Then for every $k\in\omega$ such that $N\models\Root\arrow_k^*z$, also $N\models\Root\arrow_k^*y$.
\end{SP}

\begin{proof}
There are only two types of steps that match this scenario:
\begin{description}
\item[$s\in\Step(\Sys,v7)$:] In this step, arc $(\n,\bot)$ is replaced with arc $(\n,\prt)$. Note that $x=\n$, $y=\prt$ and $z=\child$. Since $\Set(M)=\Set(N)$ and $\child=\LR(\prt,\lft)$ in both $M$ and $N$, the claim holds trivially.
\item[$s\in\Step(\Sys,v8)$:] In this step, arc $(\n,\child)$ is replaced with arc $(\n,\prt)$. Note that $x=\n$, $y=\prt$ and $z=\child$. Since $\Set(M)=\Set(T)$ and $\child=\LR(\prt,\lft)$ in both $M$ and $N$, the claim holds trivially.
\end{description}
\end{proof}

\begin{SP}[uses: \ref{inv:rem-chld-not-bot}]
\label{sp:rem-not-pc}
Let $s=(M,N)$ be a step such that $M$ is regular. Then for any $x\in\AddressT^M$, if $\neg\RemovedP(x)$ in $M$ and $\RemovedP(x)$ in $N$, then $\Root\notarrow^* x$ in $M$.
\end{SP}

\begin{proof}
Let $x$ be a removed node of $N$. From Inductive invariant \ref{inv:rem-chld-not-bot} we have that $\RightF(x)=\LeftF(x)$. Thus $x$ is not tree-like. If $x$ is path-connected, since $M$ is regular and regularity is an invariant, then $N$ is regular. Thus, R2 holds in $N$, and so $x=\n$. Since the step $s$ changes the extension of the $\RemovedP$ predicate, by observation of the algorithm, $s\in\Step(\Sys,\rom{f9})\cup\Step(\Sys,\rom{r9})\sup\Step(\Sys,\rom{v9})$.

If $s\in\Step(\Sys,\rom{f9})$, then the claim follows from the fact that $\prt$ is path-connected in $M$ by R0, and that both $\prt$ and $\n$ point to $\r$ (by the control-dependent invariants of Figure \ref{cdLM}), implying that $\n$ cannot be path-connected (otherwise $\r$ would be confluent, contradicting R2 in $M$).

If $s\in\Step(\Sys,\rom{v9})$, then the claim follows from the fact that $\prt$ is $\KeyF(\n)$-connected in $M$ by R0, and that $\n$ points to $\prt$ (by the control-dependent invariants of Figure \ref{cdLM}). In this case, if $\n$ were path-connected, then $\n$ would be a parent of $\prt$ in $M$ (contradicting R0).
\end{proof}

\begin{corollary}
\label{cor:rem-not-pc}
The combination step-properties \ref{InvRem}, \ref{Eq5a} and \ref{sp:rem-not-pc} implies that in any regular state $M$, for any address $x$, if $\RemovedP(x)$ then $\Root\notarrow^* x$ in $M$.
\end{corollary}

\section{Histories and their properties}
\label{SecHistory}
At this stage we know that regularity is an inductive invariant (Theorem \ref{InvReg}),
and hence we may {\em assume} that all states are regular.

\begin{definition}
A {\em history} is an infinite sequence of {\em regular} states $\oM =(M_i\mid i\in\omega)$ such that $M_0$ is an initial address structure, and for every index $i$ the
pair $(M_i,M_{i+1})$ is a step by one of the processes $p\in\{0,\ldots,N\}$.
\end{definition}

% An additional liveness assumption is made in this section:
% all operation executions are completed, no operation is pending forever.
% I.e. a process $p\geq 0$ never stops in midst of an operation execution;
% if $(M_i,M_{i+1})$ is any step by $p$ that is not
% a \return\ step, then for some index $j>i$, $(M_j,M_{j+1})$ is another step by $p$.

A history sequence models an execution of the CF algorithm.

We clarify the distinction between local and history statements:
A local statement $\varphi$ is a statement in the language $\mathcal{L}_{AS}$ of address structures,
and for any structure $M$, either $M\models \varphi$ or else $M\models \neg\varphi$.
The truth of a {\em history statement} is evaluated at any given history sequence \oM\ to be
true or false for that history.

A history statement may include quantification over history indexes,
which would be meaningless in local statements (which use language $\mathcal{L}_{AS}$).
% For example, the sentence
% \[\forall a\, \forall i\, ((\Root\, \notarrow^* a)^{M_i}\ \rightarrow \exists j\, \forall \ell \geq j\, (\RemovedP(a))^{M_\ell})\]
% says that a node $a$ that is not path-connected
% at state $M_i$ falls under predicate \RemovedP\ at
% all states after a certain state $M_j$.
A history statement involves local state statements of the form $(\varphi)^{M_i}$ where
$M_i$ is a reference to the $i$th state of a history sequence and $\varphi$ is a local statement.
If $\psi$ is a history statement, and $\oM$ a history,
then either $\psi$ holds in $\oM$ (denoted $\oM\models \psi$),
or its negation holds (denoted $\oM\models \neg \psi$).

The following is an example of a history statement which turns out to be useful.

\begin{lemma}[uses: \ref{Cm2}, \ref{Eq5a}]
\label{T4.4}
Let $\oM$ be a history, $x\neq \bot$ an address, and $i$ an index such that $M_i\models \Root\arrow_k ^* x$.
Let $j>i$ be an index such that $M_j\models \Root \arrow^* x$. Then $\Root\arrow_k ^* x$ in $M_j$ as well.
\end{lemma}
\begin{proof}
Let $j_0$ be the maximal index such that $j_0\leq j$ and $M_{j_0}\models  \Root\arrow^*_k x$.
Then $i\leq j_0$. We want to prove that $j_0=j$. Assume for a contradiction that $j_0< j$.
So $j_0+1\leq j$. Then Step-property \ref{Cm2} implies directly that $x$ is not path-connected in $M_{j_0+1}$
(since by the maximality of $j_0$, $x$ is not $k$-connected  in $M_{j_0+1}$).
By Invariant \ref{Eq5a}, a node that is not path connected, cannot later become path-connected,
contradiction to the assumption that $M_j\models \Root\arrow^* x$.
\end{proof}

% Note that the lemma does not hold without the assumption that $d\neq \bot$.

% Another useful history statement will serve in the Main Lemma \ref{Lm4.5}.

\begin{lemma}[uses: \ref{lemma:pdc-rem-or-locked}, \ref{Eq5a}]
\label{Lem4.4}
Let $\oM$ be a history.
Let $\ell$ be a history index, and let $y$ be an address such that $y$ is $k$-connected in $M_\ell$,
but not path-connected in $M_{\ell+1}$.
Then for every index $j\geq \ell$, $\DeletedP^{M_{\ell}}(y)\, \iff\, \DeletedP^{M_{j}}(y)$.
\end{lemma}

\begin{proof}
Since $y$ is not path-connected in $M_{\ell+1}$ and $y\neq \bot$, $y$ remains path-disconnected for all $M_i$ such that $i\geq\ell+1$, by Step-property \ref{Eq5a}.
It follows from Corollary \ref{lemma:pdc-rem-or-locked} that either $\RemovedP(y)$ or $\LockedP(y, \Sys)$ in $M_i$.
In either case, no step may change the truth of $\DeletedP(y)$.
\end{proof}

\begin{definition}[Abstract $k$-scanning]
\label{Ekpath}
Let $\oM= (M_i\mid i\in\omega)$ be a history.
For any key value $k\in \omega$, an {\em abstract $k$-scanning} in $\oM$ is a finite sequence of triples
\[T= (\langle \ell_0, x_0,y_0\rangle, \ldots, \langle\ell_i, x_i,y_{i}\rangle, \ldots, \langle\ell_n,x_n,y_{n}\rangle)\]
such that the following hold.

\begin{enumerate}
\item Each $\ell_i\in \omega$ is an index, and
the indexes are increasing: $\ell_0< \ell_1< \cdots< \ell_n$.

\item $x_i$ and $y_i$ are addresses in $M_{\ell_i}$, and $x_i\neq \bot$ and is potentially $k$-connected there.

\item For every $0\leq i<n$,
\begin{enumerate}
\item $y_i \neq\bot  \Rightarrow x_{i+1}=y_i$ (a handshake), or\label{item:handshake}
\item $(y_i=\bot \vee \KeyF(x_i)= k) \Rightarrow x_{i+1}= x_i$ (a traversal stutter).
\end{enumerate}

\item  For every $0\leq i\leq n$,
one of the following possibilities holds.
\begin{enumerate}
\item $M_{\ell_i} \models x_i\arrow_k y_{i}$ (a $k$-search triple);
\item $M_{\ell_i}\models \KeyF(x_i)=k  \wedge \RemovedP(x_i)\wedge y_i =\RightF(x_i)$ (a backtracking triple);\label{item:backtrack}
\item $M_{\ell_i}\models y_i=x_i$ (a delaying triple).
\end{enumerate}

\end{enumerate}
\end{definition}

The abstract $k$-scanning definition is meant to represent the abstract notion of a $k$-searching traversal, using the standard ``hand over hand'' approach.
In the case of the CF algorithm, the two ``hands'' of a working process $p>0$ are represented by the local variables $\nd_p$ and $\nxt_p$,
that match $x_i$ and $y_i$ in the $k$-scanning triples, respectively.
This is seen most clearly by analysing the diagrams of Figure~\ref{fig:flowcharts}.
Each triple $(\ell,x,y)$, represents a step
$(M_{\ell-1},M_\ell)$ where $x=\nd_p^{M_\ell}$,
and $y= \nxt^{M_\ell}$ is the candidate for the next value of $\nd_p$.
This abstract notion is introduced in order to formulate the minimal assumptions that are nevertheless
sufficiently strong to enable a proof of Theorem \ref{T4.2} which is the main tool in the linearizability proof of the
CF algorithm.

\begin{theorem}[The Scanning Theorem]
\label{T4.2}
Let $\oM= (M_i\mid i\in\omega)$ be a history,
and let $T= (\langle \ell_0,x_0,y_0\rangle,\ldots,\langle \ell_n, x_n, y_n\rangle)$
be an abstract $k$-scanning in $\oM$.
Suppose that $y_0\neq \bot$ is $k$-connected in $M_{\ell_0}$.
Then, for some index $j$ such that $\ell_0\leq j \leq \ell_n$, $y_{n}$ is $k$-connected in $M_j$,
and \linebreak{}$\DeletedP(y_{n})^{M_j} \iff \DeletedP(y_{n})^{M_{\ell_n}}$.
\end{theorem}

\begin{proof}
The proof is by induction on $n\geq 1$, and for any fixed $n>1$ the proof is by induction on
$\ell_n-\ell_0$. We start with the case $n=1$.
So $T=(\langle \ell_0,x_0,y_0\rangle, \langle \ell_1,x_1,y_1\rangle)$, $\ell_0<\ell_1$ and
$y_0\neq \bot$ is assumed to be $k$-connected in $M_{\ell_0}$.
$y_0\neq\bot$ implies (by item \ref{item:handshake} of Definition \ref{Ekpath}) that $x_1=y_0$ and so:

\begin{enumerate}[label=\Alph*.]
\item $M_{\ell_0} \models \Root\arrow^*_k\, y_0 = x_1$.
\item $M_{\ell_1} \models  y_1=x_1 \vee x_1\arrow_k y_1 \vee (\KeyF(x_1)=k\wedge \RemovedP(x_1)\wedge y_1=\RightF(x_1))$.\label{item-b}
\end{enumerate}

We have to prove that for some index $j$ such that $\ell_0\leq j \leq \ell_1$, $y_{1}$ is $k$-connected in $M_j$,
and $y_1$ is deleted in $M_{j}$ if and only if $y_1$ is deleted in $M_{\ell_1}$.

If $M_{\ell_1}\models\Root\arrow_k^* y_1$, the claim holds for $j=\ell_1$. So assume that
\begin{equation}
\label{eqn:y1-not-kc}
M_{\ell_1}\models\Root\notarrow_k^* y_1.
\end{equation}
It suffices to find an index $\ell$ such that
\begin{equation}
\label{eq:sufficient}
(\ell_0\leq \ell \leq \ell_1 \wedge \Root\arrow_k  y_1)^{M_\ell},
\end{equation}
because in that case we pick such $\ell$ that is maximal, which entails that $\ell<\ell_1$, $y_1$ is $k$-connected in $M_\ell$ but is not
$k$-connected in $M_{\ell+1}$, and hence $y_1$ is not path-connected in $M_{\ell+1}$ (by Step-Property \ref{Cm2}).
Then  by Lemma \ref{Lem4.4}, for every $m\geq \ell$, $\DeletedP(y_1)^{M_\ell} \iff \DeletedP(y_1)^{M_m}$, and $\ell$ is the required index.

We now check each of the possibilities of item \ref{item-b} above, and find in each case an index
$\ell$ as in (\ref{eq:sufficient}):
\begin{description}
\item[${M_{\ell_1}} \models y_1=x_1$:] In this case, $y_1$ is $k$-connected in
$M_{\ell_0}$, since $y_1=x_1=y_0$, and $y_0$ is $k$-connected in
$M_{\ell_0}$. Then the condition at (\ref{eq:sufficient}) holds and
the required index is $\ell=\ell_0$.

\item[$M_{\ell_1}\models x_1\arrow_k y_1$:] In this case, $x_1\neq y_1$, and $\KeyF(x_1)\neq k$ (by the definition of $\arrow_k$). This entails that
$M_{\ell_1}\models\Root\notarrow_k^* x_1$ (otherwise  $M_{\ell_1}\models\Root\arrow_k^* x_1\arrow_k y_1$ would contradict (\ref{eqn:y1-not-kc})). Taking into account Item A above, let $r\geq \ell_0$ be the maximal
index such that $r\leq \ell_1$ and $M_r\models\Root\arrow_k^* x_1$. Then $r<\ell_1$ (since $M_{\ell_1}
\models \Root\notarrow_k^* x_1$) and
\begin{equation}
\label{Eq24}
\mbox{$\Root\notarrow_k^* x_1$ at $M_{r+1}$ and all
subsequent indexes until $\ell_1$.}
\end{equation}
If $M_r\models x_1\arrow_k y_1$, then  $M_r\models\Root\arrow_k^* x_1\arrow_k y_1$ shows that (\ref{eq:sufficient}) holds for $\ell=r$ entailing that the required index can be found.

Hence we may assume that $M_r\models x_1\notarrow_k y_1$. Let
$s\in\{r+1,\ldots,\ell_1\}$ be the last index such that $M_s\models x_1\notarrow_k y_1$.
Then $s<\ell_1$ and $M_{s+1}\models x_1\arrow_k y_1$.
Thus step $(M_s,M_{s+1})$ changes the left or the right child of $x_1$ and this indicates that
\begin{equation}
\label{Eq25}
\mbox{$x_1$ is not removed at $M_s$ and at $M_{s+1}$,}
\end{equation}
(by Step-property \ref{sp:rem-children}).
By applying Step-property \ref{sp:pkc-after-disconnect} to the step $(M_r, M_{r+1})$
we deduce that $x_1$ is potentially $k$-connected at $M_{r+1}$. Then,
applying Step-property \ref{sp:pdc-remains-pkc} to all the steps from $M_{r+1}$ to
we conclude that $x_1$ is potentially $k$-connected in $M_{s+1}$.
Equations (\ref{Eq24}) and (\ref{Eq25}), imply that PT2($x_1,k)$ at $M_{s+1}$.
By Step-property \ref{sp:dc-chd-leads-to-chd} we have that $M_{s+1}\models\Root\arrow^*_k y_1$ must hold,
and so $y_1$ is $k$-connected at $M_{s+1}$.

\item[$M_{\ell_1}\models\KeyF(x_1)=k\wedge \RemovedP(x_1)\wedge y_1=\RightF(x_1))$:] In this case,
$x_1\neq \Root$ (as $k\in \omega$), and $x_1\neq y_1$ (as $y_1=\RightF(x_1)$; see Invariant \ref{inv:address-points-to-root}).
Since $M_{\ell_1}\models\RemovedP(x_1)$, by Corollary \ref{cor:rem-not-pc}, we have that $M_{\ell_1}\models\Root\notarrow^* x_1$.
Thus, as $x_1$ is $k$-connected at $M_{\ell_0}$, there is a maximal index $r\in\{\ell_0,\ldots,\ell_1\}$
such that $M_r\models\Root\arrow_k^* x_1$. Then $r<\ell_1$, and $x_1$ is not $k$-connected (and hence
not connected) at $M_{r+1}$
and at every subsequent structure until $M_{\ell_1}$ (see Lemma \ref{T4.4}).

Step-property \ref{sp:pkc-after-disconnect} can be applied to step $(M_r,M_{r+1})$ to conclude that
\begin{equation}
\mbox{$x_1$ is potentially $k$-connected at $M_{r+1}$.}
\end{equation}
Moreover, since $\KeyF(x_1)=k$,
if $x_1\arrow y_1$ at $M_r$, then $\Root\arrow_k^* y$ at $M_{r+1}$.
In this case an index satisfying (\ref{eq:sufficient}) is found.

Thus we may assume that $M_r\models x_1\notarrow y_1$. Let then  $s\in\{r+1,\ldots,\ell_1\}$ be the maximal index such that $M_s\models x_1\notarrow y_1$. Then $s<\ell_1$ (since
$M_{\ell_1}\models y_1=\RightF(x_1)$),
but $M_{s+1}\models x_1\arrow y_1$.

Applying Step-property \ref{sp:pdc-remains-pkc} to all the steps from step $(M_{r+1},M_{r+2})$ to step
$(M_s,M_{s+1})$, we have that $x_1$ is potentially $k$-connected at states $M_{r+1}$ to $M_{s+1}$.
We know that $x_1$ cannot be removed in $M_s$ or in $M_{s+1}$, since one of its children changed in step
$(M_s, M_{s+1})$.
Since $x_1$ is potentially $k$-connected, not $k$-connected and not removed in $M_{s}$, it must be that PT2$(x_1,k)$ holds in $M_{s}$.
By Step-property \ref{sp:dc-chd-leads-to-chd} we have that $M_{s+1}\models\Root\arrow^*_k y_1$ must hold. Since $M_{\ell_1}\models\Root\notarrow_k^* y_1$, there must be an index $t\in\{s+2,\ldots,\ell_1-1\}$ such that $M_t\models\Root\arrow_k^* y_1$ but $M_{t+1}\models\Root\notarrow_k^* y_1$, and again we are in a situation in which an index $\ell=t$ that satisfies (\ref{eq:sufficient}) is found.
\end{description}

This concludes the proof of the base case of the induction.

Now suppose that $n>1$. In case $y_1=\bot$, we have $x_2=x_1=y_0$, and then, by removing the triple
$(\ell_1,x_1,y_1)$ from the abstract scan $T$, a shorter abstract scan is obtained
to which the inductive hypothesis applies. So we may assume now that $y_1\neq \bot$.
Recall that $y_0$ is assumed to be $k$-connected in $M_{\ell_0}$.

The case $n=1$ of the theorem applies to the $k$-scan
$\left(\langle \ell_0,x_0,y_0\rangle, \langle \ell_1,x_1,y_1\rangle\right)$, and so there is an
index $\ell\in\{\ell_0,\ldots,\ell_1\}$ such that $y_1$ is $k$-connected in $M_\ell$.
Let $p$ be the node on the $k$-path before $y_1$ in $M_{\ell}$ (exists since
$y_1\neq\Root$). Then
apply the inductive assumption to the shorter path
$T' = (\langle \ell, p,y_1\rangle, \langle  \ell_2, x_2,y_2\rangle,\ldots, \langle \ell_n x_n,y_{n}\rangle)$
and get an index $\ell'$ such that $\ell\leq \ell'\leq \ell_n$ and $y_{n}$ is $k$-connected in $M_{\ell'}$, and
$\DeletedP(y_{n})^{M_j} \iff \DeletedP(y_{n})^{M_{\ell_n}}$.
\end{proof}

\section{Linearizability of the Contention-Friendly Algorithm}
\label{Sec6}
We are ready to prove the linearizability of the CF algorithm.
Let $\oM$ be an arbitrary history sequence of the algorithm.
For any index $i\in\omega$, let $\Set(M_i)\subset \KeyT$ be the set of key values
represented by state $M_i$ of the history (the key values $\infty$ and $-\infty$ are not
members of $Set(M_i)$; see Definition \ref{DefSet}).

We say that step $(M,N)$ is {\em set-preserving} if $\Set(M)=\Set(N)$, i.e. the step did not change
the \Set\ value. An operation is considered to be set-preserving if all its steps are set-preserving.

Let $E$ be a terminating data operation execution by process
$p>0$ in history \oM\ ($E$ is one of $\bfcontains(k)$, $\bfdelete(k)$ and $\bfinsert(k)$).
$E$ has a unique returning boolean value $\returnVal(E)$.
We say that $E$ is {\em successful} if and only if $\returnVal(E)=\TRUE$.
Let $i_0=\mathit{inv}(E)$ and $r=\mathit{res}(E)$ be the history
indexes such that $s_{i_0+1} =(M_{i_0}, M_{i_0+1}) = \Begin(E)\in\Step(p,\rom{m0},f)$ (where $f$ points to the first instruction of $E$) is the invocation of $E$,
and $s_{r+1}=(M_r,M_{r+1})=\End(E)\in \Step(p,rt,\rom{m0})$ (where $rt$ is a \return\ instruction) is the response of $E$\footnote{We denote step $(M_{i-1},M_i)$ by $s_i$ (rather than by $s_{i-1}$) so that $S_i$ is the consequence of step $s_i$.}.
The sequence of states $(M_{i_0},\ldots,M_r)$ is said to be the {\em extension interval} of $E$, and the steps $(M_i,M_{i+1})$ for $i_0\leq i\leq r$ are the steps
of that extension. So the invocation $\Begin(E)$ and the response $\End(E)$ are the first and last steps of
this extension of $E$; these are steps by $p$ but other steps
in this extension can be by other processes. We identify
$E$ with the set of all steps by $p$ that are in the extension of $E$, so
that $\Begin(E)$ and $\End(E)$ are the first and last steps of $E$. If we remove the last (returning) step from the terminating
operation execution $E$, then the resulting set of steps form the {\em search part} of
$E$, denoted $\search(E)$. The search part is thus, the set of steps $s_i$ by $p$ such that $i_0<i\leq r$.
%Operation $E$ consists of the steps $s_i=(M_{i-1},M_i)\in \search(E)$, together with the return step of $E$.
If we enumerate the set of the steps in $\search(E)$ in increasing order $\ell_0,\ldots,\ell_n$, then
the scanning steps of $E$ are the steps
$s_{\ell_0}=(M_{\ell_0-1}, M_{\ell_0}),\ldots, s_{\ell_n}=(M_{\ell_n-1},M_{\ell_n})$, and
$(M_{r},M_{r+1})$ is the return step of $E$.

Our aim is to define for every terminating operation execution $E$
by process $p>0$ an index $\mathit{inv}(E)\leq \ell(E)\leq \mathit{res}(E)$
which has the following `return' properties Ret1--Ret4.
$\ell$ is called the {\em linearization index} of $E$, and $(M_{\ell}, M_{\ell+1})$ its {\em linearization point}.

\begin{enumerate}
\item[Ret1:] If $E$ is a $\bfcontains(k_p)$ execution, then $E$ is set-preserving, and $\returnVal(E)=\TRUE$ if and only if $(k_p\in \Set(M_{\ell(E)}))$.

\item[Ret2:] If $E$ is a $\bfdelete(k_p)$ execution then one
of the following possibilities holds.
\begin{enumerate}
\item $\returnVal(E)=\TRUE$, and $k_p\in\Set(M_{\ell(E)})$ but $\Set(M_{{\ell(E)}+1}) = \Set(M_{\ell(E)})\setminus \{k_p\}$.
Any step in $E$ other than $(M_{\ell(E)},M_{{\ell(E)}+1})$ is set-preserving.
\item $\returnVal(E)=\FALSE$, $E$ is set-preserving and $k_p\notin \Set(M_{\ell(E)})$.
\end{enumerate}

\item[Ret3:] If $E$ is a $\bfinsert(k)$ execution then one of the
following possibilities holds.
\begin{enumerate}
\item $\returnVal(E)=\TRUE$, and $k_p\not\in \Set(M_{\ell(E)})$ but $\Set(M_{{\ell(E)}+1}) = \Set(M_{\ell(E)}) \cup \{k_p\}$.
Any step in $E$ other than $(M_{\ell(E)},M_{{\ell(E)}+1})$ is set-preserving.
\item $\returnVal(E)=\FALSE$, $E$ is set-preserving and $k_p\in \Set(M_{\ell(E)})$.
\end{enumerate}

\item[Ret4:] If $(M_i,M_{i+1})$ is any step by the \Sys\ process, then
That is, \Sys\ steps are set-preserving.
\end{enumerate}

Before we prove these four return properties, we prove Theorem~\ref{thm:operations-are-kscans} below,
which establishes that any terminating operation execution by a working process $p>0$
induces an abstract scanning sequence (Definition \ref{Ekpath}).
Then, the Scanning Theorem \ref{T4.2} applies, producing the linearization point $\ell(E)$.

\begin{theorem}
\label{thm:operations-are-kscans}
Let $\oM$ be a history of the CF algorithm, let $p>0$ be a working process, let $E$ be a terminating data operation executed by $p$ in $\oM$, and let $k$ be the value of $k_p$ during the execution of $E$. Then the scanning  steps $s_i$ of $p$ in the interval $\left[\Begin(E),\End(E)\right)$ induce an abstract $k$-scan.
\end{theorem}

Before we delve into the details of the proof, we present an intuitive overview of the intent of this theorem.

Recall the an abstract $k$-scanning (Definition \ref{Ekpath}) is meant to be an abstract representation of the traversal of a working process $p>0$ through the virtual graph.
In most cases, the steps of the data operations of the CF algorithm naturally induce an abstract $k$-scanning, even the backtracking steps.
For these steps, the proof that a valid abstract $k$-scanning is induced is a simple case-analysis process.
There is, however, one case that does not match the abstract $k$-scanning definition. This case arises when two concurrent insertion operations contend for the same insertion location:
Consider the case in which process $p$ is attempting to insert value $k$, and does not find a logically-deleted node with value $k$ to ``un-delete''. This means that a new node must be inserted as a leaf of the $k$-connected node referenced by $\nd_p$. This case is indicated by $\nxt_p$ referencing the $\bot$ node when $\ControlF(p)=\rom{i1}$. Before $p$ has a chance to ``discover'' that this is the case, and to ``decide'' to execute instruction i3, some other working process $q$ preempts $p$, and inserts a new node of its own in the same spot where $p$ wanted to insert $k$ (as a $k$-child of $\nd_p$). This creates a situation in which $\KeyF(\nd_p)\neq k_p$ but $\nd_p\notarrow_k\nxt_p=\bot$ (since $q$ inserted a node in between $\nd_p$ and $\bot$). The abstract $k$-scanning definition does not cover this situation, which may arise in some steps of the form $\Step(p,\rom{i1},\rom{i3})$.

The solution to this discrepancy arises from the fact that $\nd_p\arrow_k\nxt_p=\bot$ was true in a previous step of $p$ (the step in which $\bot$ was assigned to $\nxt_p$, before $q$ preempted $p$), yielding a valid $k$-scanning triple. Also, due to the preemption of $p$ by $q$, when executing i3, $p$ will go back to i1 to continue trying to find a spot to insert $k$. In this case, $\nxt_p$ will be re-defined to the current $k$-child of $\nd_p$, thus, inducing a valid $k$-scanning triple once again. Thus, in the case of a $k$-scan induced by \bfinsert, steps $\Step(p,\rom{i1},\rom{i3})$ are not included.

We now turn the proof itself. Recall that in the case of the CF algorithm, the $x_i$ component of a $k$-scan triple represents $\nd_p$, and $y_i$ represents $\nxt_p$. We consider each of the forms of non-returning steps of $p$ in $E$, and show that each step $s_{\ell_i}=(M_{{\ell_i}-1}, M_{\ell_i})$ induces a valid $k$-scan triple $(\ell_i,x_i,y_i)$ as defined in item 4 of Definition \ref{Ekpath}. Additionally, we show that every pair of these triples has a valid relationship, as defined in item 3 of Definition \ref{Ekpath}.

We prove the claim individually for each of the data operations. We recommend that the reader commences with the diagrams of Figure~\ref{fig:flowcharts} in hand.

\begin{lemma}
\label{lemma:contains-are-kscans}
Theorem \ref{thm:operations-are-kscans} holds if $E$ is a \bfcontains\ operation.
\end{lemma}

\begin{proof}
\begin{description}
\item[$s_i\in\Step(p,\rom{m0},\rom{c1})$:] In this case, $i=\ell_0$ by the definition of an operation. As illustrated in Figure \ref{FIGflowchart1}, $x_0=y_0 =\Root$ in $M_{\ell_0}$, and so $s_i$ is a delaying triple.
\item[$s_i\in\Step(p,\rom{c1},\rom{c1})$:] As illustrated in Figure \ref{FIGflowchart1}, $y_{i-1}\neq\bot$, and so $x_i=y_{i-1}$ (a handshake), and $\KeyF(x_i)\neq k$, and so $(x_i\arrow_k y_i)^{M_{\ell_i}}$ (k-search triple).
\item[$s_i\in\Step(p,\rom{c1},\rom{c2})$:] As illustrated in Figure \ref{FIGflowchart1}, $y_{i-1}\neq\bot$, and so $x_i=y_{i-1}$ (a handshake), and $\KeyF(x_i)=k$, and so $y_i=y_{i-1}$ (a delaying triple).
\end{description}

Thus the sequence of triples induced by the steps of $p$ in $E$ is an abstract $k$-scan as defined in \ref{Ekpath}.
\end{proof}

\begin{lemma}
\label{lemma:deletes-are-kscans}
Theorem \ref{thm:operations-are-kscans} holds if $E$ is a \bfdelete\ operation.
\end{lemma}

\begin{proof}
\begin{description}
\item[$s_i\in\Step(p,\rom{m0},\rom{d1})$:] In this case, $i=\ell_0$ by the definition of an operation. As illustrated in Figure \ref{FIGflowchart2}, $x_0=y_0 =\Root$ and so $s_i$ is a delaying triple.
\item[$s_i\in\Step(p,\rom{d1},\rom{d1})$:] As illustrated in Figure \ref{FIGflowchart2}, $y_{i-1}\neq\bot$, and so $x_i=y_{i-1}$ (a handshake), and $\KeyF(x_i)\neq k$, and so $(x_i\arrow_k y_i)^{M_{\ell_i}}$ (a k-search triple).
\item[$s_i\in\Step(p,\rom{d1},\rom{d2})$:] As illustrated in Figure \ref{FIGflowchart2}, $y_{i-1}\neq\bot$ and so $x_i=y_{i-1}$ (a handshake), and $\KeyF(x_i)=k$, and so $y_i=y_{i-1}$ (a delaying triple).
\item[$s_i\in\Step(p,\rom{d2},\rom{d1})$:] As illustrated in Figure \ref{FIGflowchart2}, $x_i=x_{i-1}$ (a traversal stutter), $\RemovedP(x_i)^{M{\ell_i}}$ and $y_i=\Right(x_i)$. Note that in any execution of \bfdelete, $s_i$ must be preceded by a step in $\Step(p,\rom{d1},\rom{d2})$, which means that $x_{i-1}=y_{i-1}$ and $\KeyF(x_{i-1})=k$. Since $x_i=x_{i-1}$, we have that $M_{\ell_i}\models\RemovedP(x_i)\wedge\KeyF(x_i)=k\wedge y_i=\RightF(x_i)$ (a backtracking triple).
\end{description}

Thus the sequence of triples induced by the steps of $p$ in $E$ is an abstract $k$-scan as defined in \ref{Ekpath}.
\end{proof}

\begin{lemma}
\label{lemma:inserts-are-kscans}
Theorem \ref{thm:operations-are-kscans} holds if $E$ is an \bfinsert\ operation.
\end{lemma}

\begin{proof}
\begin{description}
\item[$s_i\in\Step(p,\rom{m0},\rom{i1})$:] In this case, $i=\ell_0$ by the definition of an operation. As illustrated in Figure \ref{FIGflowchart3},  $x_0=y_0 =\Root$ and so $s_i$ is a delaying triple.
\item[$s_i\in\Step(p,\rom{i1},\rom{i1})$:] As illustrated in Figure \ref{FIGflowchart3}, $y_{i-1}\neq\bot$, and so $x_i=y_{i-1}$ (a handshake), and $\KeyF(x_i)\neq k$, and so $(x_i\arrow_k y_i)^{M_{\ell_i}}$ (a k-search triple).
\item[$s_i\in\Step(p,\rom{i1},\rom{i2})$:] As illustrated in Figure \ref{FIGflowchart3}, $y_{i-1}\neq\bot$, and so $x_i=y_{i-1}$ (a handshake), and $\KeyF(x_i)=k$, and so $y_i=y_{i-1}$ (a delaying triple).
\item[$s_i\in\Step(p,\rom{i2},\rom{i1})$:] As illustrated in Figure \ref{FIGflowchart3}, $x_i=x_{i-1}$ (a traversal stutter), $\RemovedP(x_i)^{M{\ell_i}}$ and $y_i=\Right(x_i)$. Note that in any execution of \bfinsert, $s_i$ must be preceded by a step in $\Step(p,\rom{i1},\rom{i2})$, which means that $x_{i-1}=y_{i-1}$ and $\KeyF(x_{i-1})=k$. Since $x_i=x_{i-1}$, we have that $M_{\ell_i}\models\RemovedP(x_i)\wedge\KeyF(x_i)=k\wedge y_i=\RightF(x_i)$ (a backtracking triple).
\item[$s_i\in\Step(p,\rom{i3},\rom{i1})$:] As illustrated in Figure \ref{FIGflowchart3}, $x_{i-1}\notarrow_k\bot$ and $y_{i-1}=\bot$, and so $x_i=x_{i-1}$ (a traversal stutter) and $(x_i\arrow_k y_i)^{M_{\ell_i}}$ (a k-search triple).
\item[$s_i\in\Step(p,\rom{i1},\rom{i3})$:] This step does not induce a valid triple. However, note that step $s_i$ must be followed by either a returning step (which is not part of any $k$-scan), or a step $s_{i+1}\in\Step(p,\rom{i3},\rom{i1})$. To see that $s_i$ does not interrupt the $k$-scan induced by steps $s_{i-1}$, $s_{i+1}$, observe that both $\nd_p$ and $\nxt_p$ are unchanged by step $s_i$. As a result, the analysis of the step $s_{i+1}\in\Step(p,\rom{i3},\rom{i1})$ shown above holds with $x_{i-1}$ and $y_{i-1}$ carrying over from step $s_{i-1}$.
\end{description}

Thus the sequence of triples induced by the steps of $p$ in $E$ is an abstract $k$-scan as defined in \ref{Ekpath}.
\end{proof}

\begin{corollary}
The data operations of the CF algorithm induce valid abstract scans.
\end{corollary}

We now turn to the proof the return properties Ret1 -- Ret4. We recommend that the reader commences with either the formal step definitions (Appendix \ref{Sec4.1}) or the code (Figure \ref{RLred}) in hand. As was the case before, we use $y$, $y_0$, $y_n$, etc., to denote the variable $\nxt_p$ in the various states, while $x$, $x_0$, $x_n$, etc., denotes the variable $\nd_p$ in the various states.

\begin{proof}[Proof of Ret1]
We must prove that the terminating $\bfcontains(k_p)$ operation $E$ is set-preserving, and we must find a linearization point $\ell(E)$ of operation $E$ such that $\returnVal_p(E)=\TRUE$ if and only if $k_p\in\Set(M_{\ell(E)})$.

In Theorem \ref{InvReg} we proved that the steps in $\Step(\rom{c1})\cup\Step(\rom{c2})$ are set-preserving, which means that $E$ is set-preserving.

Next, we find the linearization point of $E$. By Lemma \ref{lemma:contains-are-kscans}, $E$ induces a valid $k_p$-scan $T=(\langle \ell_0,x_0,y_0\rangle,\ldots,\langle \ell_n, x_n, y_n\rangle)$ such that $M_{\ell_0}\models y_0=\Root$ and so $y_0$ is $k_p$-connected in $M_{\ell_0}$.

Since $E$ is a terminating \bfcontains\ operation, the final step of $p$ in $E$, $s=(M_r, M_{r+1})$ (where $r\geq\ell_n+1$), is such that one of the following two possibilities holds:
\begin{enumerate}
\item $s\in\Step(p,\rom{c1},\rom{m0})$ is a \FALSE\ returning step. In this case, $\nxt_p^{M_r}=\bot$ (a precondition of the step), and so $y_n=\bot$. We apply the Scanning Theorem \ref{T4.2} to the $k_p$-scan $T$, and find that there is some index $j\in\{\ell_0,\ldots,\ell_n\}$ such that $y_n=\bot$ is $k_p$-connected in $M_j$. Take $\ell(E)=j$, and conclude that $k_p\notin \Set(M_j)$.

\item $s\in\Step(p,\rom{c2},\rom{m0})$. Step
$s=(M_{\ell_n-1}, M_{\ell_n})$, the last step before
the return step $(M_r,M_{r+1})$, is such that
$x_n=\nd_p^{M_{\ell_n}}=\nxt_p^{M_{\ell_n}}$, and we get that
$\KeyF(x_n)=k_p$ (so that $x_n\neq\bot$). The return value is
$\neg\DeletedP(\nd_p^{M_r})$. The abstract scanning
induced by $E$ has $(\ell_n, x_n, x_n)$
as its last triple. We add to that abstract scanning
another triple: $t= (\ell_{n+1}, x_{n+1},y_{n+1}) =
(r, x_n, x_n)$ and get a longer (by 1)
abstract scanning $T'=T\cdot t$.  $T'$ satisfies
the requirements of abstract scanning \ref{Ekpath} as $x_n=y_n\neq\bot$, $x_{n+1}=x_n$,
and since $M_r$ is a regular state, we get that $\nd_p^{M_r}=x_n$ is potentially $k_p$-connected.
We now apply the Scanning theorem  to $T'$\footnote{Note that applying the Scanning theorem directly to $T$ would give us an index $\ell_0\leq j \leq \ell_n$ such that $x_n$ is $k_p$ connected in $M_j$, but we would not know that the \DeletedP\ predicate for $x_n$ is agreed upon between $M_j$ and $M_r$.}, and find that there is an index $j\in\{\ell_0,\ldots,r\}$ such that $x_n=y_{n+1}=x_n$ is $k_p$-connected in $M_j$ and $\DeletedP(x_n)^{M_j}\iff\DeletedP(x_n)^{M_{r+1}}$. Take $\ell(E)=j$, and
%then $a$ is $k_p$-connected in $M_j$ and since $\DeletedP^{M_j}\iff \DeletedP^{M_r}$
the answer provided by the return step is the correct one.

\end{enumerate}
\end{proof}

\begin{proof}[Proof of Ret2]
We must find a linearization point $\ell(E)$ of a \bfdelete\ operation $E$, and prove
that it is correctly related with the value returned by the operation.

By Lemma \ref{lemma:deletes-are-kscans}, $E$ induces a valid $k_p$-scan $T=(\langle \ell_0,x_0,y_0\rangle,\ldots,\langle \ell_n, x_n, y_n\rangle)$ such that $M_{\ell_0}\models y_0=\Root$ and so $y_0$ is $k_p$-connected in $M_{\ell_0}$.

Since $E$ is a terminating \bfdelete\ operation, the returning step of $p$, $s=(M_r, M_{r+1})$ (where $r\geq\ell_n+1$), is such that one of the following holds:
\begin{enumerate}
\item $s\in\Step(p,\rom{d1},\rom{m0})$ and the returned value is
$\FALSE$. In this case, $\nxt_p^{M_r}=\bot$ (a precondition of the step), and so $y_n=\bot$. We apply Theorem \ref{T4.2} to the $k$-scan $T$, and find that there is some index $j\in\{\ell_0,\ldots,\ell_n\}$ such that $y_n=\bot$ is $k_p$-connected in $M_j$. So
$k_p\notin\Set(M_j)$, and the returned value corresponds correctly to
the choice of $\ell(E)=j$ as the linearization point. All steps of $E$ are set-preserving
in this case by Theorem \ref{InvReg}.

\item $s\in\Step(p,\rom{d2},\rom{m0})$.  In Figure \ref{fig:protocol-elementary-invariants} we have the control-dependent invariant $\ControlF(p)=d2\rightarrow\LockedP(\nd_p)\wedge
\KeyF(\nd_p)=k_p$. There are two possibilities:
\begin{enumerate}
\item $\returnVal_p(E)=\TRUE$, which implies that
\begin{equation}
\label{Eq:Mr-is-search-connected}
M_r\models \nd_p\neq\bot\wedge \neg\DeletedP(\nd_p)\wedge \neg\RemovedP(\nd_p) \wedge
\LockedP(\nd_p,p),
\end{equation}
and $M_{r+1}\models\DeletedP(\nd_p)$. As discussed in the proof of \ref{InvReg}, in this case, $\Set(M_{r+1})=\Set(M_r)\setminus\{k_p\}$.
Since $M_r$ is a regular state, $\nd_p$ is potentially $k_p$-connected there.
Equation (\ref{Eq:Mr-is-search-connected}) together with Corollary \ref{lemma:pdc-rem-or-locked}
implies that $\nd_p$ is path-connected. Hence necessarily $\nd_p$ is $k_p$-connected.
We can take $r+1=\ell(E)$ as the linearization point of $E$.

\item $\returnVal_p(E)=\FALSE$, and $M_r\models\DeletedP(\nd_p)$.
The last triple of $T$ is $(\ell_n,x_n,y_n)$, and thus, the last step
$s=(M_{\ell_n-1},M_\ell)$ before the return step $(M_r, M_{r+1})$ is
an execution of instruction in $\Step(p,\rom{d1, d2})$.
As illustrated in Figure \ref{FIGflowchart2}, it follows that $\nd_p=\nxt_p$ has key value $k_p$.
%and hence $M_{r+1}\models\DeletedP(\nd_p)$ as well (since process $p$ holds the lock on node $\nd_p$). As illustrated in Figure \ref{FIGflowchart2}, $\nd_p=\nxt_p$ in $M_r$, and $\nd_p$ is not changed by step $s$.
We use these facts, and define a $k_p$-scan triple for step $s$ as follows: $t=\langle r, x_n, x_n\rangle$. We use this triple to define $T'=T\cdot t$, which is a valid $k_p$-scan, by Definition \ref{Ekpath}. We now apply Theorem \ref{T4.2} to $T'$, and find that there is an index $j\in\{\ell_0,\ldots,r\}$ such that $x_n$ is $k_p$-connected in $M_j$ and $\DeletedP(x_n)^{M_j}\iff\DeletedP(x_n)^{M_{r+1}}$. But we know that $\DeletedP(x_n)^{M_{r+1}}$, and so $\DeletedP(x_n)^{M_j}$. Take $\ell(E)=j$, and conclude that the returned value \FALSE\ is correct
since $k_p\notin\Set(M_j)$.
\end{enumerate}
\end{enumerate}
\end{proof}

\begin{proof}[Proof of Ret3]
We must find a linearization point $\ell(E)$ of an \bfinsert\ operation $E$, and prove
that it is correctly related with the value returned by the operation.
% We must find a linearization point $\ell(E)$ of operation $E$ such that if $\returnVal_p(E)=\TRUE$, then $k_p\notin\Set(M_{\ell(E)})$ and $\Set(M_{\ell(E)+1})=\Set(M_{\ell(E)})\cup\{k_p\}$, and if $\returnVal_p(E)=\FALSE$, then $k_p\in\Set(M_{\ell(E)})$ and $E$ is set-preserving.

By lemma \ref{lemma:inserts-are-kscans}, $E$ induces a valid $k_p$-scan $T=(\langle \ell_0,x_0,y_0\rangle,\ldots,\langle \ell_n, x_n, y_n\rangle)$ such that $M_{\ell_0}\models y_0=\Root$ and so $y_0$ is $k_p$-connected in $M_{\ell_0}$.

Since $E$ is a terminating \bfinsert\ operation, the returning
step of $p$ (the one that follows $T$), is $s=(M_r, M_{r+1})$ (where $r\geq\ell_n+1$), is such that one of the following holds:
\begin{enumerate}
\item $s\in\Step(p,\rom{i2},\rom{m0})$. In Figure \ref{fig:protocol-elementary-invariants} we have the control-dependent invariant $\ControlF(p)=i2\rightarrow\LockedP(\nd_p)\wedge\KeyF(\nd_p)=k_p$. There are two possibilities:
\begin{enumerate}
\item $\returnVal_p(E)=\TRUE$.
This implies that
\begin{equation}
M_r\models \LockedP(\nd_p,p) \wedge \DeletedP(\nd_p) \wedge
\neg\RemovedP(\nd_p),
\end{equation}
and $M_{r+1}\models\neg\DeletedP(\nd_p)$. As discussed in the proof of \ref{InvReg}, in this case,\linebreak{}
$\Set(M_{r+1})=\Set(M_r)\cup\{k_p\}$, but we have to prove that $k_p\notin \Set(M_r)$ in order to
justify the return value. %Since $\DeletedP(\nd_p)$ in $M_r$, it must be the case that $\neg\RemovedP(\nd_p)$ in $M_r$ as well (otherwise, the step would be a backtracking step instead of a returning step).
The displayed equation together with \ref{lemma:pdc-rem-or-locked}
implies that $\nd_p$ is $k_p$-connected at $M_r$ and $M_{r+1}$,
so that $k_p\notin \Set(M_{r+1})$,
and we can take $r+1=\ell(E)$ as the linearization point of $E$.
\item $\returnVal_p(E)=\FALSE$. Then $M_r\models\neg\DeletedP(\nd_p)$ and so $M_{r+1}\models\neg\DeletedP(\nd_p)$ as well
since the return step does not change the \DeletedP\ predicate.
%(process $p$ holds the lock on node $\nd_p$).
As illustrated in Figure \ref{FIGflowchart3}, the last
triple of $T$ $(\ell_n, x_n, y_n)$ is such that
$x_n=y_n$, that is $\nd_p=\nxt_p$ in $M_{\ell_n}$ and hence
in $M_r$. We use these facts, and define a $k_p$-scan triple for step $s$ as follows: $t=\langle r, x_n, x_n\rangle$. We use this triple to define $T'=T\cdot t$, which is a valid $k_p$-scan, as
defined in \ref{Ekpath}. We now apply Theorem \ref{T4.2} to $T'$, and find that there is an index $j\in\{\ell_0,\ldots,r\}$ such that $x_n$ is $k_p$-connected in $M_j$ and $\DeletedP(x_n)^{M_j}\iff\DeletedP(x_n)^{M_{r+1}}$. But we know that $\neg\DeletedP(x_n)^{M_{r+1}}$, and so $\neg\DeletedP(x_n)^{M_j}$.
Thus $k_p\in \Set(S_j)$ and the return value \FALSE\ is justified
by the choice of $\ell(E)=j$ as the linearization point of $E$.
\end{enumerate}

\item $s\in\Step(p,\rom{i3},\rom{m0})$. If the returning step
is an execution of i3, then $\returnVal_p(E)=\TRUE$,
and as part of the proof of Theorem \ref{InvReg}, we showed that $\Set(M_{r+1}) = \Set(M_r)\cup\{k_p\}$. In order to prove that the returned
value is appropriate, we have to show that $k_p\notin\Set(M_r)$,
and for this we will show that $\bot$ is $k_p$-connected at $M_r$.
Since $\ControlF(p)=\rom{i3}$ in $M_r$, $\KeyF(\nd_p)\neq k_p$.
Since $\ControlF(p)=\rom{m0}$ in $M_{r+1}$, $\LR(\nd_p,k_p< \KeyF(\nd_p))=\bot$.
By the control-dependent invariant of Figure \ref{fig:protocol-elementary-invariants}, we know that $\LockedP(\nd_p,p)$
Since $M_r$ is regular, $\nd_p$ is potentially $k_p$-connected.
Since $\nd_p\arrow_{k_p} \bot$, and since $\nd_p$ is not removed at $M_r$ (see \ref{inv:rem-chld-not-bot}),
it is not the case that PT3$(\nd_p,k_p)$.
By the control-dependent invariant of Figure \ref{fig:protocol-elementary-invariants}, we know that $\LockedP(\nd_p,p)$,
which excludes the possibility that PT2$(\nd_p,k_p)$.
% then (by definition) $\nd_p\arrow_{k_p} \bot$ implies that
% $\bot$ is $k_p$-connected.
Thus PT1$(\nd_p,k_p)$, and so $\nd_p\arrow_{k_p}\bot$ implies immediately that $\bot$ is $k_p$-connected.
\end{enumerate}
\end{proof}

\begin{proof}[Proof of Ret4]
As part of the proof of Theorem \ref{InvReg}, we proved that the steps performed by the system process are set-preserving. Thus, Property 4 holds.
\end{proof}

This concludes the correctness proof of the CF algorithm.

\section{Related Work}
\label{subsec:related-work}
O'Hearn et al.~[13] described a proof framework for linked-list-based concurrent set algorithms. They used it to prove the correctness of the Lazy Set algorithm of to Heller et al.~[10]. Similar to our approach, theirs is two-tiered: they first formulate invariants and step-properties specific to the algorithm in question (some of which match some of our invariants and step-properties). They then formulate and prove the Hindsight Lemma in terms of these invariants and properties, which they use to prove the linearizability of the Lazy Set. As in our case, that lemma is formulated in a way that is abstracted away from the technical details of the algorithm they analyze.

In this chapter, we discussed our development of a framework for analyzing the behavior of BST-backed sets, which requires an approach different from that for the analysis of linked-list-backed sets, due to the differing constraints and more complex behavior of BSTs.

Feldman et al.~[9] presented a general framework for proving the correctness of concurrent tree- and list-based implementations of the set data structure. Their framework is based on temporal predicates on instructions of the operations of the implementation under inspection. A temporal predicate $\phi$ is said to hold at instruction $i$ of operation $o$ if $\phi$ holds \emph{at some moment} between the time $t$ at which $o$ was invoked and the time $t'$ when $i$ is executed. They use the convention $\DDiamond^{t'}_t(\phi)$ to represent such temporal predicates.

Feldman et al.~[9] used of their framework to prove the correctness of multiple concurrent tree-based implementations of the set data structure. Among these implementations is a variant of the CF algorithm of Crain et al.~[3, 4]. While the variant they proved is very similar to the original algorithm, there is one major behavioral difference in the \bfinsert\ and \bfdelete\ operations: it is possible that when the traversing process reaches a node $x$ where a logical deletion or insertion should take place, $x$ is found to be physically removed (by way of the \rem\ flag). In this case, the original algorithm continues the traversal process from $x$, relying on the clever backtracking mechanism. On the other hand, the variant that Feldman et al. analyzed restarts the traversal process from the \Root\ node all over again.

This difference stems from a condition of Feldman et al.'s proof framework, which they call the \emph{forepassed condition with respect to field $f$}. Intuitively, this condition requires that writes that may interfere with a concurrent traversal do not change the field $f$ of any node $x$ after $x$ has been disconnected, if $x$ was disconnected during said traversal.

Core to the proof of Feldman et al. is the past temporal logic predicate $\DDiamond(\Root\arrow^*_k y \wedge y.\key = k \wedge \neg y.\rem)$, which can be found in the assertion annotations of the \bfdelete\ and \bfinsert\ operations in the Appendix of~[9]. To prove the correctness of this predicate, it is required for the \emph{forepassed condition with respect to \rem} to hold. However, in the original algorithm, the \bfremove, \rotateLeft\, and \rotateRight\ operations first disconnect the node \n, and only then do they modify \n.\rem, thus violating this condition.

In this chapter, we proved the correctness of the original form of the algorithm, including its full backtracking mechanism.

\section{Conclusion}
In this chapter, we formally proved the correctness of the contention-friendly algorithm of Crain et al.~[3, 4].
To our knowledge, this is the first time this has been done for the original algorithm of Crain et al., which includes its full backtracking mechanism.

To facilitate the proof, we presented the abstract notions of ``potential-connectivity'', ``regularity'', and ``abstract scanning''.
We believe that these notions constitute a general framework for proving the correctness of concurrent BST algorithms.
We intend to explore this belief in the future by attempting to apply the tools developed here to other BST algorithms,
such as the Logically-Ordered tree algorithm~[5] and the Citrus tree algorithm~[2].

We supplemented our proof with a bounded model of the algorithm, encoded in TLA+,
and verified the various invariants and properties in Section~\ref{sec:invariants-and-props} against that model~[14].
While not a full verification of our proofs (due to the bounded nature of the model),
this model-checking process does act to validate the correctness of our proofs.

Our methodology of using model-checking to validate our manual work proved useful, helping us find and correct multiple minor issues. In addition, as detailed in footnote~\ref{footnote:pt2} of definition~\ref{DefPot}, TLA+ flagged a serious problem in this definition, which we corrected with the help of the problematic scenario provided by the model-checker as a counter example.

\bibliographystyle{abbrv}
\begin{thebibliography}{10}

[1]
\newblock {\em Models for Concurrency}, volume~11.
\newblock CRC Press, 1999.

[2]
M.~Arbel and H.~Attiya.
\newblock Concurrent updates with {RCU:} search tree as an example.
\newblock In M.~M. Halld{\'{o}}rsson and S.~Dolev, editors, {\em {ACM}
Symposium on Principles of Distributed Computing, {PODC} '14, Paris, France,
July 15-18, 2014}, pages 196--205. {ACM}, 2014.

[3]
T.~Crain, V.~Gramoli, and M.~Raynal.
\newblock A contention-friendly binary search tree.
\newblock In F.~Wolf, B.~Mohr, and D.~an~Mey, editors, {\em Euro-Par 2013
Parallel Processing - 19th International Conference, Aachen, Germany, August
26-30, 2013. Proceedings}, volume 8097 of {\em Lecture Notes in Computer
Science}, pages 229--240. Springer, 2013.

[4]
T.~Crain, V.~Gramoli, and M.~Raynal.
\newblock A fast contention-friendly binary search tree.
\newblock {\em Parallel Process. Lett.}, 26(3):1650015:1--1650015:17, 2016.

[5]
D.~Drachsler, M.~T. Vechev, and E.~Yahav.
\newblock Practical concurrent binary search trees via logical ordering.
\newblock In J.~E. Moreira and J.~R. Larus, editors, {\em {ACM} {SIGPLAN}
Symposium on Principles and Practice of Parallel Programming, PPoPP '14,
Orlando, FL, USA, February 15-19, 2014}, pages 343--356. {ACM}, 2014.

[6]
T.~Elmas, S.~Qadeer, and S.~Tasiran.
\newblock A calculus of atomic actions.
\newblock {\em ACM SIGPLAN Notices}, 44(1):2--15, 2009.

[7]
U.~Engberg, P.~Gr{\o}nning, and L.~Lamport.
\newblock Mechanical verification of concurrent systems with {TLA}.
\newblock In G.~von Bochmann and D.~K. Probst, editors, {\em Computer Aided
Verification, Fourth International Workshop, {CAV} '92, Montreal, Canada,
June 29 - July 1, 1992, Proceedings}, volume 663 of {\em Lecture Notes in
Computer Science}, pages 44--55. Springer, 1992.

[8]
Y.~M.~Y. Feldman, C.~Enea, A.~Morrison, N.~Rinetzky, and S.~Shoham.
\newblock Order out of chaos: Proving linearizability using local views.
\newblock In U.~Schmid and J.~Widder, editors, {\em 32nd International
Symposium on Distributed Computing, {DISC} 2018, New Orleans, LA, USA,
October 15-19, 2018}, volume 121 of {\em LIPIcs}, pages 23:1--23:21. Schloss
Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, 2018.

[9]
Y.~M.~Y. Feldman, A.~Khyzha, C.~Enea, A.~Morrison, A.~Nanevski, N.~Rinetzky,
and S.~Shoham.
\newblock Proving highly-concurrent traversals correct.
\newblock {\em Proc. {ACM} Program. Lang.}, 4({OOPSLA}):128:1--128:29, 2020.

[10]
S.~Heller, M.~Herlihy, V.~Luchangco, M.~Moir, W.~N.~S. III, and N.~Shavit.
\newblock A lazy concurrent list-based set algorithm.
\newblock {\em Parallel Process. Lett.}, 17(4):411--424, 2007.

[11]
M.~P. Herlihy and J.~M. Wing.
\newblock Linearizability: A correctness condition for concurrent objects.
\newblock {\em ACM Trans. Program. Lang. Syst.}, 12(3):463--492, July 1990.

[12]
\newblock Proving the correctness of multiprocess programs.
\newblock {\em IEEE transactions on software engineering}, 3(2):125--143, 1977.

[13]
P.~W. O'Hearn, N.~Rinetzky, M.~T. Vechev, E.~Yahav, and G.~Yorsh.
\newblock Verifying linearizability with hindsight.
\newblock In A.~W. Richa and R.~Guerraoui, editors, {\em Proceedings of the
29th Annual {ACM} Symposium on Principles of Distributed Computing, {PODC}
2010, Zurich, Switzerland, July 25-28, 2010}, pages 85--94. {ACM}, 2010.

[14]
{Accompanying Code Repository}.
\newblock \url{https://github.com/hayounav/Thesis_experiments}.
\newblock Last Accessed: Aug. 31, 2022.

[15]
H.~Zhu, G.~Petri, and S.~Jagannathan.
\newblock Poling: {SMT} aided linearizability proofs.
\newblock In D.~Kroening and C.~S. Pasareanu, editors, {\em Computer Aided
Verification - 27th International Conference, {CAV} 2015, San Francisco, CA,
USA, July 18-24, 2015, Proceedings, Part {II}}, volume 9207 of {\em Lecture
Notes in Computer Science}, pages 3--19. Springer, 2015.

\end{thebibliography}

\newpage
\appendix
\section{Steps of the Contention Friendly Algorithm}
\label{Sec4.1}

In this appendix we precisely define each of the steps of the contention friendly protocol presented in figures \ref{LM} and \ref{RLred}.
For the sake of brevity, in the definition of a step $(M,N)$, interpretations of the constituents of $N$ are assumed to be identical to those of $M$,
unless explicitly stated otherwise, and we list those variables whose denotations may change in {\em `` Possible changes''}.

We begin by describing the steps of process $p>0$ invoking one of its three operations:

Invocations of $\bfcontains(k)$ (respectively $\bfdelete(k)$ and $\bfinsert(k)$), where $k\in\omega$,
is the set of all steps $\Step(p,\rom{m0},\rom{c1})$ such that the following hold.
$\ControlF^M(p)=\rom{m0}$, $\ControlF^N(p)=\rom{c1}$ (respectively
$\ControlF^N(p)=\rom{d1}$ and $\ControlF^N(p)=\rom{i1}$), $k_p^N=k$, $\nd_p^N=\Root$,
and $\nxt_p^N=\Root$.

\paragraph*{Steps of process $p>0$ executing its $\bfcontains(k_p)$ for $k_p\in\omega$.}

\begin{enumerate}
\item
$(M,N) \in \Step(p,\rom{c1})$ if and only if $\ControlF^M(p)=\rom{c1}$ and
one of the following three possibilities occurs:
\begin{enumerate}
\item
$\nxt_p^M=\bot \wedge  \returnVal_p^N=\FALSE\wedge \ControlF(p)=\rom{m0}$.

\item $\nxt_p^M\neq\bot \wedge \nd_p^N=\nxt_p^M\wedge k_p=\KeyF(\nd_p^N)
\wedge \ControlF^N(p)=\rom{c2}$.

\item
$\nxt_p^M\neq\bot \wedge \nd_p^N=\nxt_p^M\wedge k_p\neq \KeyF(\nd_p^N)
\wedge \ControlF^N(p)=\rom{c1}\wedge(\nd_p\arrow_{k_p} \nxt_p)^N$.
\end{enumerate}
\possible\ $\ControlF(p), \nd_p, \nxt_p$.

\item
$(M,N)\in \Step(p,\rom{c2})$ if and only if:
\begin{equation*}
\ControlF^M(p)=\rom{c2} \wedge \ControlF^N(p)=\rom{m0}\wedge\returnVal_p^N \equiv (\neg\DeletedP(\nd_p))^M
\end{equation*}
\possible\ $\ControlF(p), \returnVal_p$.
\end{enumerate}

\paragraph*{Steps of process $p>0$ executing its $\bfdelete(k_p)$  for $k_p\in\omega$}.

\begin{enumerate}
\item
$(M,N) \in \Step(p,\rom{d1})$ if and only if $\ControlF^M(p)=\rom{d1}$ and
one of the following three possibilities occurs:
\begin{enumerate}
\item
$\nxt_p^M=\bot \wedge \ControlF^N=\rom{m0}\wedge \returnVal_p^N=\FALSE$.

\item $\nxt_p^M\neq\bot \wedge \nd_p^N=\nxt_p^M\wedge k=\KeyF(\nd_p^N)
\wedge \ControlF^N(p)=\rom{d2}$.

\item
$\nxt_p^M\neq\bot \wedge \nd_p^N=\nxt_p^M\wedge k\neq \KeyF(\nd_p^N)
\wedge \ControlF^N(p)=\rom{d1}\wedge(\nd_p\arrow_{k_p} \nxt_p)^N$.
\end{enumerate}
\possible\ $\ControlF(p), \nd_p, \nxt_p$.

\item $(M,N) \in \Step(p,\rom{d2})$ if and only if $\ControlF^M(p)=\rom{d2}$ and one of the following three possibilities occurs:
\begin{enumerate}
\item $\DeletedP(\nd)^M\rightarrow \ControlF^N(p)=\rom{m0}\wedge \returnVal_p^N=\FALSE$.
\item $\neg\DeletedP(\nd_p)^M\wedge\RemovedP(\nd_p)^M\rightarrow \nxt_p^N=\RightF(\nd_p^M)\wedge \ControlF^N(p)=\rom{d1}$.
\item $\neg\DeletedP(\nd_p)^M\wedge\neg\RemovedP(\nd_p)^M\rightarrow \DeletedP^N(\nd_p^M)\wedge \ControlF^N(p)=\rom{m0}\wedge\\ \returnVal_p^N=\TRUE$.
\end{enumerate}
\possible\ $\ControlF(p), \nxt_p, \DeletedP$.
\end{enumerate}

\paragraph*{Steps of process $p>0$ executing its $\bfinsert(k_p)$  for $k_p\in\omega$.}

\begin{enumerate}
\item $(M,N) \in \Step(p,\rom{i1})$ if and only if $\ControlF^M(p)=\rom{i1}$ and
one of the following three possibilities occurs:
\begin{enumerate}
\item
$\nxt_p^M=\bot \wedge \ControlF^N(p)=\rom{i3}$.

\item $\nxt_p^M\neq\bot \wedge \nd_p^N=\nxt_p^M\wedge k_p=\KeyF(\nd_p^N)
\wedge \ControlF^N(p)=\rom{i2}$.

\item
$\nxt_p^M\neq\bot \wedge \nd_p^N=\nxt_p^M\wedge k_p\neq \KeyF(\nd_p^N)
\wedge \ControlF^N(p)=\rom{i1}\wedge(\nd_p\arrow_{k_p} \nxt_p)^N$.
\end{enumerate}
\possible\ $\ControlF(p), \nd_p, \nxt_p$.

\item $(M,N) \in \Step(p,\rom{i2})$ if and only if $\ControlF^M(p)=\rom{i2}$ and one of the following three possibilities occurs:
\begin{enumerate}
\item $\neg\DeletedP(\nd)^M\rightarrow \ControlF^N(p)=\rom{m0}\wedge \returnVal_p^N=\FALSE$.
\item $\DeletedP(\nd_p)^M\wedge\RemovedP(\nd_p)^M\rightarrow \nxt_p^N=\RightF(\nd_p)^M\wedge \ControlF^N(p)=\rom{i1}$.
\item $\DeletedP(\nd_p)^M\wedge\neg\RemovedP(\nd_p)^M\rightarrow \neg\DeletedP^N(\nd_p^M)\wedge \ControlF^N(p)=\rom{m0}\wedge\\ \returnVal_p^N=\TRUE$.
\end{enumerate}
\possible\ $\ControlF(p), \nxt_p, \DeletedP$.

\item $(M,N) \in \Step(p,\rom{i3})$ if and only if $\ControlF^M(p)=\rom{i3}$ and one of the following three possibilities occurs:
\begin{enumerate}
\item $(\nd_p\notarrow_{k_p}\bot)^M\rightarrow(\nd_p\arrow_{k_p}\nxt_p)^N\wedge\ControlF^N(p)=\rom{i1}$.
\item $(\nd_p\arrow_{k_p}\bot)^M\rightarrow\exists\new\in\AddressT^N:$
\begin{equation*}
\begin{split}
& \AddressT^N\setminus\AddressT^M=\{\new\}\wedge(\nd_p\arrow_{k_p}\new)^N\wedge \\
& \KeyF(\new)=k_p\wedge\LeftF^N(\new)=\RightF^N(\new)=\bot\wedge\\
& \neg\DeletedP^N(\new)\wedge\neg\RemovedP^N(\new)
\end{split}
\end{equation*}
\end{enumerate}
\possible\ $\ControlF(p), \nd_p, \nxt_p, \LeftF, \RightF, \KeyF, \AddressT$.
\end{enumerate}

Next, we tackle the steps of process $\Sys$ (i.e. $p=0$) invoking one of its three operations:

\begin{enumerate}
\item Invocations of $\rotateLeft(\prt,\lft)$ is the set $\Step(\Sys,\rom{m0},\rom{f6})$ of steps
$(M,N)$ such that $\ControlF^M(\Sys)=\rom{m0}\wedge \ControlF^N(\Sys)=\rom{f5}$, and all the prerequisites
pr1--pr5 hold at state $N$.

\item Invocations of $\rotateRight(\prt,\lft)$ is the set defined symmetrically with r6 replacing f6.

\item Invocations of $\bfremove(\prt,\lft)$ is defined similarly.
\end{enumerate}

\paragraph*{Steps of process $\Sys$ executing its $\rotateLeft(\prt,\lft)$.}

\begin{enumerate}
\item $(M,N)\in \Step(\Sys,\rom{f6})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{f6}\wedge \ControlF^N(\Sys)=\rom{f7} \wedge\\
& \exists a \in \AddressT^N:\AddressT^N\setminus\AddressT^M=\{a\} \wedge \\
& \LeftF^N(a) = \ell_0^M \wedge \RightF^N(a) = \rl^M \wedge \KeyF^N(a) = \KeyF^M(\n) \wedge \\
&\DeletedP^N(a) = \DeletedP^M(\n) \wedge \LeftF^N(\r^N) = a \\
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \LeftF, \RightF, \KeyF, \AddressT$.

\item $(M,N)\in \Step(\Sys,\rom{f7})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{f7}\wedge \ControlF^N(\Sys)=\rom{f8} \wedge\\
& \LeftF^N(\n^N) = \r^M
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \LeftF$.

\item $(M,N)\in \Step(\Sys,\rom{f8})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{f8}\wedge \ControlF^N(\Sys)=\rom{f9} \wedge\\
& \lft^M = \TRUE \rightarrow \LeftF^N(\prt^N) = \r^M \wedge \\
& \lft^M = \FALSE \rightarrow \RightF^N(\prt^N) = \r^M
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \LeftF, \RightF$.

\item $(M,N)\in \Step(\Sys,\rom{f9})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{f9}\wedge \ControlF^N(\Sys)=\rom{m0} \wedge\\
& \RemovedP^N(\n^N) \wedge \neg\LockedP^N(\n^N, \Sys)
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \RemovedP$.
\end{enumerate}

\paragraph*{Steps of process $\Sys$ executing its $\rotateRight(\prt,\lft)$.}

\begin{enumerate}
\item $(M,N)\in \Step(\Sys,\rom{r6})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{r6}\wedge \ControlF^N(\Sys)=\rom{r7} \wedge\\
& \exists a \in \AddressT^N:\AddressT^N\setminus\AddressT^M=\{a\} \wedge \\
& \LeftF^N(a) = \lr^M \wedge \RightF^N(a) = \r^M \wedge \KeyF^N(a) = \KeyF^M(\n) \wedge \\
&\DeletedP^N(a) = \DeletedP^M(\n) \wedge \RightF^N(\ell_0^N) = a \\
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \LeftF, \RightF, \KeyF, \AddressT$.

\item $(M,N)\in \Step(\Sys,\rom{r7})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{r7}\wedge \ControlF^N(\Sys)=\rom{r8} \wedge\\
& \RightF^N(\n^N) = \ell_0^M
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \RightF$.

\item $(M,N)\in \Step(\Sys,\rom{r8})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{r8}\wedge \ControlF^N(\Sys)=\rom{r9} \wedge\\
& \lft^M = \TRUE \rightarrow \LeftF^N(\prt^N) = \ell_0^M \wedge \\
& \lft^M = \FALSE \rightarrow \RightF^N(\prt^N) = \ell_0^M
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \LeftF, \RightF$.

\item $(M,N)\in \Step(\Sys,\rom{r9})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{r9}\wedge \ControlF^N(\Sys)=\rom{m0} \wedge\\
& \RemovedP^N(\n^N) \wedge \neg\LockedP^N(\n^N, \Sys)
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \RemovedP$.
\end{enumerate}

\paragraph*{Steps of process $\Sys$ executing its $\bfremove(\prt,\lft)$.}

\begin{enumerate}

\item $(M,N)\in \Step(\Sys,\rom{v5})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{v5}\wedge \ControlF^N(\Sys)=\rom{v6} \wedge \\
& \lft^M = \TRUE \rightarrow \LeftF^N(\prt^N) = \child^M \wedge \\
& \lft^M = \FALSE \rightarrow \RightF^N(\prt^N) = \child^M
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \LeftF, \RightF$.

\item $(M,N)\in \Step(\Sys,\rom{v6})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{v6}\wedge \ControlF^N(\Sys)=\rom{v7} \wedge \\
& \LeftF^M(\n^M) = \bot \rightarrow \LeftF^N(\n^N) = \prt^M \wedge \\
& \LeftF^M(\n^M) \neq \bot \rightarrow \RightF^N(\n^N) = \prt^M
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \LeftF, \RightF$.

\item $(M,N)\in \Step(\Sys,\rom{v7})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{v7}\wedge \ControlF^N(\Sys)=\rom{v8} \wedge \\
& \LeftF^M(\n^M) = \prt^M \rightarrow \RightF^N(\n^N) = \prt^M \wedge \\
& \LeftF^M(\n^M) \neq \prt^M \rightarrow \LeftF^N(\n^N) = \prt^M
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \LeftF, \RightF$.

\item $(M,N)\in \Step(\Sys,\rom{v8})$ if and only if:
\begin{equation*}
\begin{split}
& \ControlF^M(\Sys)=\rom{v8}\wedge \ControlF^N(\Sys)=\rom{m0} \wedge\\
& \RemovedP^N(\n^N) \wedge \neg\LockedP^N(\n^N, \Sys)
\end{split}
\end{equation*}
\possible\ $\ControlF(\Sys), \RemovedP$.
\end{enumerate}

\end{document}