+Z \relation{hb} Y \wedge \neg X \relation{hb} Y $.
+
+Under these analysis and assumptions, we present Lemma~\ref{seqHistoryExistence}.
+
+\begin{lemma} \label{seqHistoryExistence}
+For any legal C/C++11 execution, where store / load operations have release / acquire
+semantics and store operations to the same memory location are ordered by
+\textit{happens-before} relation, there exists a sequential history
+that is consistent with the modification order consistency and the
+happens-before relation in terms of store to store operations, load to store
+operations and operations on the same memory location.
+\end{lemma}
+
+\begin{proof}
+
+To prove Lemma~\ref{seqHistoryExistence}, we present our algorithm to generate
+such a sequential history and prove that such an algorithm is feasible. We first
+topologically sort the operations by the \hb relation and have a sequential
+history $H$. By C/C++11, \hb is acyclic. Since every store / load operations
+have release / acquire semantics, every reads-from edge is also a \hb edge.
+Thus, a load operation can only read from an old store in $H$. We iterate the
+load operations on the same memory location from the end of $H$. For each load
+operation $X$ that reads from some store $Y$ on location $M$, if no store
+operation on $M$ exists between $X$ and $Y$ in $H$, any load operations on $M$
+before $X$ and after $Y$ cannot be \mo consistency ordered after $Y$ so $Y$ is
+ordered consistently; otherwise, if there exists
+
+
+\end{proof}