diff -r 1e4a79cd8332 -r e73184c3928f damecco.tex
--- a/damecco.tex	Wed Nov 23 20:51:09 2016 +0100
+++ b/damecco.tex	Wed Nov 23 20:59:40 2016 +0100
@@ -538,7 +538,7 @@
 $\tilde{s}$. Otherwise, $\tilde{s}$ is not consistent by $PT$ or it
 can be proved that $s$ can not be extended to a whole mapping.
 
-In order to make sure of the correctness see
+In order to make sure of the correctness, see
 \begin{claim}
 Through consistent mappings, only consistent whole mappings can be
 reached, and all of the whole mappings are reachable through
@@ -693,45 +693,6 @@
 \tilde{T}_{large}(s)| < |\Gamma_{small}(u)\cap \tilde{T}_{small}(s)|$
 is \textbf{not} a cutting function by $SUB$.
 \end{claim}
-\begin{proof}$ $\\
-\vspace*{-0.5cm}
-
-\begin{figure}
-\begin{center}
-\begin{tikzpicture}
-  [scale=.8,auto=left,every node/.style={circle,fill=black!15}]
-  \node[rectangle,fill=black!15] at (4,6) {$G_{small}$}; \node (u4) at
-  (2.5,10) {$u_4$}; \node (u3) at (5.5,10) {$u_3$}; \node (u1) at
-  (2.5,7) {$u_1$}; \node (u2) at (5.5,7) {$u_2$};
-  
-  \node[rectangle,fill=black!30] at (13.5,6) {$G_{large}$};
-  \node[fill=black!30] (v4) at (12,10) {$v_4$}; \node[fill=black!30]
-  (v3) at (15,10) {$v_3$}; \node[fill=black!30] (v1) at (12,7)
-       {$v_1$}; \node[fill=black!30] (v2) at (15,7) {$v_2$};
-  
-
-  \foreach \from/\to in {u1/u2,u2/u3,u3/u4,u4/u1} \draw (\from) --
-  (\to); \foreach \from/\to in {v1/v2,v2/v3,v3/v4,v4/v1,v1/v3} \draw
-  (\from) -- (\to);
-%    \draw[dashed] (\from) -- (\to);
-\end{tikzpicture}
-\caption{Graphs for the proof of Claim~\ref{claimSUB}}
-\label{fig:proofSUB}
-\end{center}
-\end{figure}
-Let the two graphs of Figure~\ref{fig:proofSUB} be the input
-graphs.  Suppose the total ordering relation is $u_1 \prec u_2 \prec
-u_3 \prec u_4$,$M(s)\!=\{(u_1,v_1)\}$, and VF2 tries to add
-$(u_2,v_2)\in P(s)$.\newline $Cons_{SUB}((u_2,v_2),M(s))=true$, so
-$M\cup \{(u_2,v_2)\}$ is consistent by $SUB$. The cutting function
-$Cut_{SUB}((u_2,v_2),M(s))$ is false, so it does not let cut the
-tree.\newline On the other hand $Cut_{SUB}'((u_2,v_2),M(s))$ is true,
-since\\$0=|\Gamma_{large}(v_2)\cap
-\tilde{T}_{large}(s)|<|\Gamma_{small}(u_2)\cap
-\tilde{T}_{small}(s)|=1$ is true, but still the tree can not be
-pruned, because otherwise the
-$\{(u_1,v_1)(u_2,v_2)(u_3,v_3)(u_4,v_4)\}$ mapping can not be found.
-\end{proof}
 
 \section{The VF2++ Algorithm}
 Although any total ordering relation makes the search space of VF2 a