1.1 --- a/damecco.tex	Wed Nov 23 20:51:09 2016 +0100
     1.2 +++ b/damecco.tex	Wed Nov 23 20:59:40 2016 +0100
     1.3 @@ -538,7 +538,7 @@
     1.4  $\tilde{s}$. Otherwise, $\tilde{s}$ is not consistent by $PT$ or it
     1.5  can be proved that $s$ can not be extended to a whole mapping.
     1.6  
     1.7 -In order to make sure of the correctness see
     1.8 +In order to make sure of the correctness, see
     1.9  \begin{claim}
    1.10  Through consistent mappings, only consistent whole mappings can be
    1.11  reached, and all of the whole mappings are reachable through
    1.12 @@ -693,45 +693,6 @@
    1.13  \tilde{T}_{large}(s)| < |\Gamma_{small}(u)\cap \tilde{T}_{small}(s)|$
    1.14  is \textbf{not} a cutting function by $SUB$.
    1.15  \end{claim}
    1.16 -\begin{proof}$ $\\
    1.17 -\vspace*{-0.5cm}
    1.18 -
    1.19 -\begin{figure}
    1.20 -\begin{center}
    1.21 -\begin{tikzpicture}
    1.22 -  [scale=.8,auto=left,every node/.style={circle,fill=black!15}]
    1.23 -  \node[rectangle,fill=black!15] at (4,6) {$G_{small}$}; \node (u4) at
    1.24 -  (2.5,10) {$u_4$}; \node (u3) at (5.5,10) {$u_3$}; \node (u1) at
    1.25 -  (2.5,7) {$u_1$}; \node (u2) at (5.5,7) {$u_2$};
    1.26 -  
    1.27 -  \node[rectangle,fill=black!30] at (13.5,6) {$G_{large}$};
    1.28 -  \node[fill=black!30] (v4) at (12,10) {$v_4$}; \node[fill=black!30]
    1.29 -  (v3) at (15,10) {$v_3$}; \node[fill=black!30] (v1) at (12,7)
    1.30 -       {$v_1$}; \node[fill=black!30] (v2) at (15,7) {$v_2$};
    1.31 -  
    1.32 -
    1.33 -  \foreach \from/\to in {u1/u2,u2/u3,u3/u4,u4/u1} \draw (\from) --
    1.34 -  (\to); \foreach \from/\to in {v1/v2,v2/v3,v3/v4,v4/v1,v1/v3} \draw
    1.35 -  (\from) -- (\to);
    1.36 -%    \draw[dashed] (\from) -- (\to);
    1.37 -\end{tikzpicture}
    1.38 -\caption{Graphs for the proof of Claim~\ref{claimSUB}}
    1.39 -\label{fig:proofSUB}
    1.40 -\end{center}
    1.41 -\end{figure}
    1.42 -Let the two graphs of Figure~\ref{fig:proofSUB} be the input
    1.43 -graphs.  Suppose the total ordering relation is $u_1 \prec u_2 \prec
    1.44 -u_3 \prec u_4$,$M(s)\!=\{(u_1,v_1)\}$, and VF2 tries to add
    1.45 -$(u_2,v_2)\in P(s)$.\newline $Cons_{SUB}((u_2,v_2),M(s))=true$, so
    1.46 -$M\cup \{(u_2,v_2)\}$ is consistent by $SUB$. The cutting function
    1.47 -$Cut_{SUB}((u_2,v_2),M(s))$ is false, so it does not let cut the
    1.48 -tree.\newline On the other hand $Cut_{SUB}'((u_2,v_2),M(s))$ is true,
    1.49 -since\\$0=|\Gamma_{large}(v_2)\cap
    1.50 -\tilde{T}_{large}(s)|<|\Gamma_{small}(u_2)\cap
    1.51 -\tilde{T}_{small}(s)|=1$ is true, but still the tree can not be
    1.52 -pruned, because otherwise the
    1.53 -$\{(u_1,v_1)(u_2,v_2)(u_3,v_3)(u_4,v_4)\}$ mapping can not be found.
    1.54 -\end{proof}
    1.55  
    1.56  \section{The VF2++ Algorithm}
    1.57  Although any total ordering relation makes the search space of VF2 a