diff --git a/framework.tex b/framework.tex
index 47a5432e42efcdd046983e9441b3a27374ec8705..3929752e965bf72b57ffa1a3ff04e85b858a2d38 100644
--- a/framework.tex
+++ b/framework.tex
@@ -403,11 +403,10 @@ We skip the binder of the predicate whenever the meta-level assertions does not
     & \STimeB).
   \end{align*}
   \begin{proof}~\\
-    We have $\dom{\SIndex} = \dom{\SProcs}^2$,~\\
+    We have $\dom{\SIndex} = \dom{\SProcs}^2$, 
     $\All \proc \in \dom{\SProcs}, (\loc, \_, \ts) \in \SProcs(\proc). \ts \le \STime(\loc)$,~\\
     and $\All (\proc, \procB) \in \dom{\SIndex}. 
-    \SIndex(\proc, \procB) \le \length{\SProcs(\procB)}$~\\
-    ${}\land \SProcs(\proc) \bsup \btake(\SProcs(\procB), \SIndex(\proc, \procB))$.
+    \SIndex(\proc, \procB) \le \length{\SProcs(\procB)} \land \SProcs(\proc) \bsup \btake(\SProcs(\procB), \SIndex(\proc, \procB))$.
     \begin{enumerate}
       \item $\dom{\SIndex} = \dom{\SProcs}^2$. By assumption.
       \item Suppose $\proc \in \dom{\SProcs}$, $(\loc, \val, \ts) \in \SProcsB(\proc)$.~\\
@@ -434,7 +433,7 @@ We skip the binder of the predicate whenever the meta-level assertions does not
 %
 %
 \begin{lem}[$\SInv$:Store]\label{lem:store-hinv}
-  $\All \STime, \fH, \loc_0 \in \dom{STime}, \val_0, \buf_0.$
+  $\All \STime, \fH, \loc_0 \in \dom{\STime}, \val_0, \buf_0.$
   \def\STimeB{\Iupd\STime[\loc_0 -+> 1]}%
   \def\fHB{\Cupd\fH[\loc_0 -::> ((\loc_0, \val_0, \STime(\loc_0)+1) :: \buf_0)]}%
   \begin{align*}
@@ -477,12 +476,12 @@ We skip the binder of the predicate whenever the meta-level assertions does not
 %
 %
 \begin{lem}[$\DBInv$:Store]\label{lem:store-dbinv}
-  $\All \fMB, \fH, \proc_0 \in \dom{\fMB}, \loc_0 \in \dom{STime}, \val_0, \ts_0, \buf_0.$
+  $\All \fMB, \fH, \proc_0 \in \dom{\fMB}, \loc_0 \in \dom{\fH}, \val_0, \ts_0, \buf_0.$
   \def\fHB{\Cupd\fH[\loc_0 -::> ((\loc_0, \val_0, \ts_0) :: \buf_0)]}%
   \def\fMBB{\Cupd\fMB[\proc_0 -::> (\loc_0, \val_0, \ts_0)]}%
   \begin{align*}
     \DBInv(\fMB, \fH) \Ra \DBInv(
-    & \Cupd\fMB[\proc_0 -::> (\loc_0, \val_0, \ts_0)], \\
+    & \fMBB, \\
     & \Fupd\fH[\loc_0 -> (\loc_0, \val_0, \ts_0) :: \fMB(\proc_0)])
   \end{align*}
   \begin{proof}~\\
@@ -510,6 +509,41 @@ We skip the binder of the predicate whenever the meta-level assertions does not
   \end{proof}
 \end{lem}
 %
+
+\begin{lem}\label{lem:process-small}
+  $\All \fMB, \fH, \proc \in \dom{\fMB}, \buf, \loc, \val,
+  \ts$.
+  \def\fMBB{\Cupd\fMB[\proc -::> (\loc, \val, \ts)]}%
+  \def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
+  \def\tup{(\loc, \val, \ts)}%
+  \begin{align*}
+    \multicolumn{2}{l}{\fMB(\proc) \bsup \buf 
+    \land (\Exists \buf' \bsub \buf. \tup :: \buf' \in \fH(\loc))}  \\
+    {}\implies{} & \tup :: \fMB(\proc) \bsup \tup :: \buf \\
+    & {} \land \Exists \buf'' \bsub \fMB(\proc). \tup :: \buf'' \in \fH(\loc)
+  \end{align*}
+\begin{proof}
+\janno{TODO}
+\end{proof}
+\end{lem}
+%
+\begin{lem}[$\DBInv+\SInv$:Process]\label{lem:process-ok}
+  $\All \fMB, \fH, \proc, \procB \in \dom{\fMB}, \buf, \loc, \val,
+  \ts$.
+  \def\fMBB{\Cupd\fMB[\proc -::> (\loc, \val, \ts)]}%
+  \def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
+  \def\tup{(\loc, \val, \ts)}%
+  \begin{align*}
+    \multicolumn{2}{l}{\SInv(\fMB, \SIndex, \STime) \land \DBInv(\fMB, \fH)} \\
+    \multicolumn{2}{l}{\state_I(\proc,\proc_1) < }
+    {}\implies{}
+  \end{align*}
+\begin{proof}
+\janno{TODO}
+\end{proof}
+\end{lem}
+%
+%
 \subsubsection{\ruleref{AtomicRead2}}
 %
 \begin{hproofenv}
@@ -694,19 +728,24 @@ We skip the binder of the predicate whenever the meta-level assertions does not
     \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB \ast \ofH}~\\
     Context: $\fMB(\proc) \bsup \buf$ \by def. $\GMB$~\\
     \begin{psubenv}{\ruleref{PROCESS-OK}}
-      Case: $\dom{\fMB} \supset \set\proc$~\\
-      Context: $$~\\
+      Case: $\Exists \procB. \length{\fMB(\procB)} > \state_I(\proc, \procB)$~\\
+      (cont'd): $(\loc, \val, \ts) = \fMB(\procB)_{\state_I(\proc, \procB)}$~\\
+      (cont'd): $\Exists \ts' < \ts. \mr{\fMB(\proc)}{(\loc, \_, \ts')}$~\\
       \begin{psubenv}{Frame}
         \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
         \cdline{\eprocess, \proc}~\\
-        \pline[-\set\ips]{}~\\
+        Define: $\fMB' \eqdef \Cupd\fMB[\loc -::> (\loc, \val, \ts)]$~\\
+        Define: $\state_I' \eqdef \Iupd\state_I[\proc, \procB -+> 1]$~\\
+        \pline[-\set\ips]{\ownPhys{(\fMB', \state_I', \state_T)}}~\\
       \end{psubenv}
     \end{psubenv}
     \hline
     \begin{psubenv}{\ruleref{PROCESS-SKIP}}
+      \pline[-\set\ips]{}~\\
     \end{psubenv}
     \hline
     \begin{psubenv}{all other cases}
+      \pline[-\set\ips]{}~\\
     \end{psubenv}
     \pline[\top]{\top}~\\
   \end{psubenv}