+\begin{proof}
+In the algorithm showed in Figure~\ref{fig:algorithmConsistentHistory}, during
+each iteration it can have a set of load operations $l'$
+(Line~\ref{line:loadSet}) to be moved up across the most recent store operation
+$w'$. For any load opeartion $l''$ in the set $l'$, as showed in the proof of
+Lemma~\ref{seqHistoryExistence}, no other operation on the same memory location
+exists between $w'$ and $l''$. When $l''$ moves across an operation $o$ that
+happens before $l''$, we make a transform $t$ on the happens-before relation on
+$o$ and $l''$. When it finishes generating $H$, we have a finite steps of
+transform taken on the happens-before graph, denoted as $T$. We also denote that
+\textit{hb}$_T$ as the happens before relation after $T$.
+\end{proof}
+