• English only

# Differences

This shows you the differences between two versions of the page.

vkuncak
Line 1: Line 1:
====== Insertion into Doubly-Linked List ====== ====== Insertion into Doubly-Linked List ======

Code: Code:
Line 21: Line 21:

Where $P$ is Where $P$ is
-$\begin{array}{l}+\begin{equation*}\begin{array}{l} n \neq null\ \land \\ n \neq null\ \land \\ ​next(n) = null \land prev(n)=null\ \land \\ ​next(n) = null \land prev(n)=null\ \land \\ ​prev(first) = null\ \land \ Q ​prev(first) = null\ \land \ Q \end{array} \end{array} -$+\end{equation*}
and where $Q$ is and where $Q$ is
-$\begin{array}{l}+\begin{equation*}\begin{array}{l} ​\forall x.\forall y. prev(x)=y\ \ \rightarrow \\ ​\forall x.\forall y. prev(x)=y\ \ \rightarrow \\ ​\qquad (y \neq null \rightarrow next(y)=x)\ \land \\ ​\qquad (y \neq null \rightarrow next(y)=x)\ \land \\ ​\qquad (y = null \land x \neq null \rightarrow (\forall z. next(z) \neq x)) ​\qquad (y = null \land x \neq null \rightarrow (\forall z. next(z) \neq x)) -\end{array}$+\end{array}\end{equation*}

Corresponding {{sav08:​simpledll.java.txt|Jahob file}} (call it dll-example.java). Corresponding {{sav08:​simpledll.java.txt|Jahob file}} (call it dll-example.java).