diff --git a/appendix.tex b/appendix.tex
index 9c257d7cdbf2c9a40d6e59467da8992b86691969..e5443a0d95b9f8df8529feaa265a4e0ac9a7c26b 100644
--- a/appendix.tex
+++ b/appendix.tex
@@ -58,8 +58,11 @@
 \input{rsl/cas}
 \input{rsl/ma}
 \chapter{GPS}
-\input{gps/multiproto}
+% \input{gps/multiproto}
 \input{gps/protocols}
+\input{gps/protocols-sw}
+\input{gps/protocols-frac}
+\input{gps/protocols-plain}
 \input{gps/escrows}
 \chapter{Examples}
 \input{examples/cirbuf}
diff --git a/examples/cirbuf.tex b/examples/cirbuf.tex
index 4b8fe7a664b0788fc5d5a0f9fb734c059f3b7ecd..461cbe52d9f424a4be1ea340b41362f38bfa7067 100644
--- a/examples/cirbuf.tex
+++ b/examples/cirbuf.tex
@@ -36,8 +36,8 @@ Let $\ptwi = 0, \ptri = 0, \ptbuf = 0$.
   \cdline{\enewb() \eqdef}~\\
   \pind{
     \cdline{\elet{\q}{\ealloc{\bSize+2}}{}}~\\
-    \cdline{\ewrite{\rtna}{\q+\ptri}{0};}~\\
-    \cdline{\ewrite{\rtna}{\q+\ptwi}{0};}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptri}{0};}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptwi}{0};}~\\
     \cdline{\q}~\\
   }~\\
   \cdline{\eprod(\q) \eqdef}~\\
@@ -48,8 +48,8 @@ Let $\ptwi = 0, \ptri = 0, \ptbuf = 0$.
     \cdline{\eif \; w' == r \ethen \; 0}~\\
     \cdline{\eelse}~\\
     \pind{
-      \cdline{\ewrite{\rtna}{\q+\ptbuf+w}{x}}~\\
-      \cdline{\ewrite{\rtat}{\q+\ptwi}{w'}}~\\
+      \cdline{\ewrite{\wtna}{\q+\ptbuf+w}{x}}~\\
+      \cdline{\ewrite{\wtat}{\q+\ptwi}{w'}}~\\
       \cdline{1}~\\
     }~\\
   }~\\
@@ -61,7 +61,7 @@ Let $\ptwi = 0, \ptri = 0, \ptbuf = 0$.
     \cdline{\eelse}~\\
     \pind{
       \cdline{\elet{x}{\eread{\rtna}{\q+\ptbuf+r}}{}}~\\
-      \cdline{\ewrite{\rtat}{\q+\ptri}{r+1 \bmod \bSize}}~\\
+      \cdline{\ewrite{\wtat}{\q+\ptri}{r+1 \bmod \bSize}}~\\
       \cdline{x}~\\
     }~\\
   }~\\
@@ -122,12 +122,12 @@ Let $\ptwi = 0, \ptri = 0, \ptbuf = 0$.
                 \bigast_{0 \le i < N} [\escprod(\gname,\q,i)]
                 \ast \bigast_{k \ge 0} \ownGhost{\gname}{\prodtok(k)}
                 \ast \bigast_{k \ge 0} \ownGhost{\gname}{\constok(k)}}~\\
-  \cdline{\ewrite{\rtna}{\q+\ptri}{0};}~\\
+  \cdline{\ewrite{\wtna}{\q+\ptri}{0};}~\\
   \pline[]{\efracn{\q+\ptwi}{\Alloc} 
            \ast \Prtcl{\q+\ptri : 0 | \prcons(\gname, \q)}_W 
            \ast \bigast_{k \ge 0} \ownGhost{\gname}{\prodtok(k)}
            \ast \bigast_{k \ge 0} \ownGhost{\gname}{\constok(k)}}~\\
-  \cdline{\ewrite{\rtna}{\q+\ptwi}{0};}~\\
+  \cdline{\ewrite{\wtna}{\q+\ptwi}{0};}~\\
   \pline[]{\Prtcl{\q+\ptwi : 0 | \prprod(\gname, \q)}_W 
            \ast \Prtcl{\q+\ptri : 0 | \prcons(\gname, \q)}_W 
            \ast \bigast_{k \ge 0} \ownGhost{\gname}{\prodtok(k)}
@@ -210,7 +210,7 @@ Let $\ptwi = 0, \ptri = 0, \ptbuf = 0$.
       \ast \bigast_{k \ge i+1} \ownGhost{\gname}{\prodtok(k)}
       \ast \efracn{\q+\ptbuf+w}{\any}
     }~\\
-    \cdline{\ewrite{\rtna}{\q+\ptbuf+w}{x}}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptbuf+w}{x}}~\\
     \pline[]{
       \Prtcl{\q+\ptwi : i | \prprod(\gname, \q)}_W
       \ast \Prtcl{\q+\ptri : j | \prcons(\gname, \q)}_R
@@ -224,7 +224,7 @@ Let $\ptwi = 0, \ptri = 0, \ptbuf = 0$.
       \ast \esccons(\gname,\q,i)
       \ast \bigast_{k \ge i+1} \ownGhost{\gname}{\prodtok(k)}
     }~\\
-    \cdline{\ewrite{\rtat}{\q+\ptwi}{w'}}~\\
+    \cdline{\ewrite{\wtat}{\q+\ptwi}{w'}}~\\
     \pline[]{
       \Prtcl{\q+\ptwi : i+1 | \prprod(\gname, \q)}_W
       \ast \Prtcl{\q+\ptri : j | \prcons(\gname, \q)}_R
@@ -302,7 +302,7 @@ Let $\ptwi = 0, \ptri = 0, \ptbuf = 0$.
       \ast P(x) 
       \ast [\escprod(\gname,\q,j)]
     }~\\
-    \cdline{\ewrite{\rtat}{\q+\ptri}{r+1 \bmod \bSize}}~\\
+    \cdline{\ewrite{\wtat}{\q+\ptri}{r+1 \bmod \bSize}}~\\
     \pline[]{
       \Prtcl{\q+\ptwi : i | \prprod(\gname, \q)}_R
       \ast \Prtcl{\q+\ptri : j+1 | \prcons(\gname, \q)}_W
diff --git a/examples/def.tex b/examples/def.tex
index 44770e1905be2fcd88ac6a78793ef0c8160c5e1e..b0a106461310b07eef2bfd3091fa741cb30079f7 100644
--- a/examples/def.tex
+++ b/examples/def.tex
@@ -13,4 +13,6 @@
 
 % Predicates
 \def\abseen{\textrm{Seen}}
-\def\node{\ensuremath{\textsf{Node}}}
\ No newline at end of file
+\def\node{\ensuremath{\textsf{Node}}}
+
+\def\prule{\rule[0.2em]{\linewidth}{0.1em}}
\ No newline at end of file
diff --git a/examples/michaelscott.tex b/examples/michaelscott.tex
index 453cc0deaa9273015ec910e4a0437ea3320c9920..7556fbcb538a870e203cd73dc6c9ee7c1f535239 100644
--- a/examples/michaelscott.tex
+++ b/examples/michaelscott.tex
@@ -57,10 +57,10 @@ Let $\ptlink = 0, \ptdata = 1, \pthead = 0, \pttail = 1$.
   \cdline{\enew() \eqdef}~\\
   \pind{
     \cdline{\elet{\sent}{\ealloc{1}}{}}~\\
-    \cdline{\ewrite{\rtna}{\sent + \ptlink}{0};}~\\
+    \cdline{\ewrite{\wtna}{\sent + \ptlink}{0};}~\\
     \cdline{\elet{\q}{\ealloc{2}}{}}~\\
-    \cdline{\ewrite{\rtna}{\q+\pthead}{\sent};}~\\
-    \cdline{\ewrite{\rtna}{\q+\pttail}{\sent};}~\\
+    \cdline{\ewrite{\wtna}{\q+\pthead}{\sent};}~\\
+    \cdline{\ewrite{\wtna}{\q+\pttail}{\sent};}~\\
     \cdline{\q}~\\
   }~\\
   \cdline{\efindTail(\q) \eqdef}~\\
@@ -68,7 +68,7 @@ Let $\ptlink = 0, \ptdata = 1, \pthead = 0, \pttail = 1$.
     \cdline{\elet{n}{\eread{\rtat}{\q + \pttail}}{}}~\\
     \cdline{\elet{n'}{\eread{\rtat}{n + \ptlink}}{}}~\\
     \cdline{\eif \; n' == 0 \ethen \; n}~\\
-    \cdline{\eelse \; \ewrite{\rtat}{\q+\pttail}{n'}; 0}~\\
+    \cdline{\eelse \; \ewrite{\wtat}{\q+\pttail}{n'}; 0}~\\
   }
 \end{hproofenv}
 
@@ -76,12 +76,12 @@ Let $\ptlink = 0, \ptdata = 1, \pthead = 0, \pttail = 1$.
   \cdline{\eenq(\q,x) \eqdef}~\\
   \pind{
     \cdline{\elet{n}{\ealloc{2}}{}}~\\
-    \cdline{\ewrite{\rtna}{n+\ptdata}{x};}~\\
-    \cdline{\ewrite{\rtna}{n+\ptlink}{0};}~\\
+    \cdline{\ewrite{\wtna}{n+\ptdata}{x};}~\\
+    \cdline{\ewrite{\wtna}{n+\ptlink}{0};}~\\
     \cdline{\elet{t}{\erepeat{\efindTail(\q)}}{}}~\\
     \cdline{\eif \; \ecas{t+\ptlink}{0}{n} \; \ethen}~\\
     \pind{
-      \cdline{\ewrite{\rtat}{\q+\pttail}{n}; 1}~\\
+      \cdline{\ewrite{\wtat}{\q+\pttail}{n}; 1}~\\
     }~\\
     \cdline{\eelse \; 0}~\\
   }
@@ -251,7 +251,7 @@ STS at $\gamma_o$, $\iname_o$:
   \pline[\top]{\varPsi(\nil, \nil)}~\\
   \cdline{\elet{\sent}{\ealloc{1}}{}}~\\
   \pline[\top]{\varPsi(\nil, \nil) \ast \lraw(\sent+\ptlink,\None)}~\\
-  \cdline{\ewrite{\rtna}{\sent + \ptlink}{0};}~\\
+  \cdline{\ewrite{\wtna}{\sent + \ptlink}{0};}~\\
   \pline[\top]{\varPsi(\nil, \nil) 
               \ast \Prtcl{\sent+\ptlink:\snull|\prlink(\gname)}
               \ast \ownGhost{\gname}{\diamond}
@@ -263,7 +263,7 @@ STS at $\gamma_o$, $\iname_o$:
               \ast \ownGhost{\gname_L}{\authfull \set{\sent}}
               \ast \lraw(\q+\pthead,\None) 
               \ast \lraw(\q+\pttail,\None)}~\\
-  \cdline{\ewrite{\rtna}{\q+\pthead}{\sent};}~\\
+  \cdline{\ewrite{\wtna}{\q+\pthead}{\sent};}~\\
   \pline[\top]{
     \varPsi(\nil, \nil) 
     \ast \Prtcl{\sent+\ptlink:\snull|\prlink(\gname)}
@@ -271,7 +271,7 @@ STS at $\gamma_o$, $\iname_o$:
     \ast \Prtcl{\q + \pthead : \sinv(\sent) | \prhead}_W
     \ast \lraw(\q+\pttail,\None)
   }~\\
-  \cdline{\ewrite{\rtna}{\q+\pttail}{\sent};}~\\
+  \cdline{\ewrite{\wtna}{\q+\pttail}{\sent};}~\\
   \pline[\top]{ 
     \varPsi(\nil, \nil)
     \ast \ownGhost{\gname_L}{\authfull \set{\sent}}
@@ -311,7 +311,7 @@ STS at $\gamma_o$, $\iname_o$:
     \pline[\top]{
       \node(n') 
       \ast \Exists \gname'. \Prtcl{n' + \ptlink : \snull | \prlink(\gname')}}~\\
-    \cdline{\ewrite{\rtat}{\q+\pttail}{n'};}~\\
+    \cdline{\ewrite{\wtat}{\q+\pttail}{n'};}~\\
     \pline[\top]{\Prtcl{\q + \pttail : \sinv | \prtail}}~\\
     \cdline{0}~\\
     \pline[\top]{\Ret z. z = 0 \ast \msq(\q, \popped, \pushed) }~\\
@@ -336,11 +336,11 @@ STS at $\gamma_o$, $\iname_o$:
   \pline[\top]{P(\val) \ast Q
                \ast \lraw(n+\ptdata,\None)
                \ast \lraw(n+\ptlink,\None)}~\\
-  \cdline{\ewrite{\rtna}{n+\ptdata}{v};}~\\
+  \cdline{\ewrite{\wtna}{n+\ptdata}{v};}~\\
   \pline[\top]{P(\val) \ast Q
                \ast \efracn{n+\ptdata}{v}
                \ast \lraw(n+\ptlink,\None)}~\\
-  \cdline{\ewrite{\rtna}{n+\ptlink}{0};}~\\
+  \cdline{\ewrite{\wtna}{n+\ptlink}{0};}~\\
   \pline[\top]{P(\val) \ast Q
                \ast \efracn{n+\ptdata}{v}
                \ast \Exists \gname'. 
@@ -363,7 +363,7 @@ STS at $\gamma_o$, $\iname_o$:
         \ast \Prtcl{n+\ptlink: \snull | \prlink(\gname')}
         \ast \node(n)
     }~\\
-    \cdline{\ewrite{\rtat}{\q+\pttail}{n};}~\\
+    \cdline{\ewrite{\wtat}{\q+\pttail}{n};}~\\
     \pline[\top]{
       \Exists \popped' \supseq \popped, \pushed' \supseq \pushed.
         \ast \msq(\q,\popped', \pushed' \mdoubleplus [\val]) \ast T
diff --git a/examples/msq-gc.tex b/examples/msq-gc.tex
index 5b02d1fbb3c85b3060fd9184ce5d37b429a15b32..f21a628c45fd976e8c2faed5e8f23a4204a9b5f5 100644
--- a/examples/msq-gc.tex
+++ b/examples/msq-gc.tex
@@ -46,19 +46,19 @@ Let $\ptlink = 0, \ptdata = 1, \pthead = 0, \pttail = 1, \ptlast = 2, \ptcc = 3,
   \cdline{\enew() \eqdef}~\\
   \pind{
     \cdline{\elet{\sent}{\ealloc{1}}{}}~\\
-    \cdline{\ewrite{\rtna}{\sent + \ptlink}{0};}~\\
+    \cdline{\ewrite{\wtna}{\sent + \ptlink}{0};}~\\
     \cdline{\elet{\q}{\ealloc{4+N}}{}}~\\
-    \cdline{\ewrite{\rtna}{\q+\pthead}{\sent};}~\\
-    \cdline{\ewrite{\rtna}{\q+\pttail}{\sent};}~\\
-    \cdline{\ewrite{\rtna}{\q+\ptlast}{\sent};}~\\
-    \cdline{\ewrite{\rtna}{\q+\ptcc}{0};}~\\
+    \cdline{\ewrite{\wtna}{\q+\pthead}{\sent};}~\\
+    \cdline{\ewrite{\wtna}{\q+\pttail}{\sent};}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptlast}{\sent};}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptcc}{0};}~\\
     \cdline{\elet{\c}{\ealloc{1}}{}}~\\
-    \cdline{\ewrite{\rtna}{\c}{0};}~\\
+    \cdline{\ewrite{\wtna}{\c}{0};}~\\
     \cdline{\erepeat{}}~\\
     \pind{
       \cdline{\elet{i}{\eread{\rtna}{\c}}{}}~\\
-      \cdline{\ewrite{\rtna}{\q+\ptuc+i}{0};}~\\
-      \cdline{\ewrite{\rtna}{\c}{i+1};}~\\
+      \cdline{\ewrite{\wtna}{\q+\ptuc+i}{0};}~\\
+      \cdline{\ewrite{\wtna}{\c}{i+1};}~\\
       \cdline{i+1 == \nThreads}~\\
     }~\\
     \cdline{\efree(\c)}~\\
@@ -70,18 +70,18 @@ Let $\ptlink = 0, \ptdata = 1, \pthead = 0, \pttail = 1, \ptlast = 2, \ptcc = 3,
     \cdline{\elet{n'}{\eread{\rtat}{n + \ptlink}}{}}~\\
     \cdline{\eif \; n' == 0}~\\
     \cdline{\ethen \; n}~\\
-    \cdline{\eelse \; \ewrite{\rtat}{\q+\pttail}{n'}; 0}~\\
+    \cdline{\eelse \; \ewrite{\wtat}{\q+\pttail}{n'}; 0}~\\
   }~\\
   \cdline{\eenq(\q,x) \eqdef}~\\
   \pind{
     \cdline{\elet{n}{\ealloc{2}}{}}~\\
-    \cdline{\ewrite{\rtna}{n+\ptdata}{x};}~\\
-    \cdline{\ewrite{\rtna}{n+\ptlink}{0};}~\\
+    \cdline{\ewrite{\wtna}{n+\ptdata}{x};}~\\
+    \cdline{\ewrite{\wtna}{n+\ptlink}{0};}~\\
     \cdline{\elet{t}{\erepeat{\eftl(\q)}}{}}~\\
     \cdline{\eif \; \ecas{t+\ptlink}{0}{n}}~\\
     \cdline{\ethen}~\\
     \pind{
-      \cdline{\ewrite{\rtat}{\q+\pttail}{n}; 1}~\\
+      \cdline{\ewrite{\wtat}{\q+\pttail}{n}; 1}~\\
     }~\\
     \cdline{\eelse}~\\
     \pind{
@@ -113,7 +113,7 @@ Let $\ptlink = 0, \ptdata = 1, \pthead = 0, \pttail = 1, \ptlast = 2, \ptcc = 3,
   \pind{
     \cdline{\elet{o}{\eread{\rtna}{\q+\ptlast}}{}}~\\
     \cdline{\elet{n}{\eread{\rtat}{\q+\pthead}}{}}~\\
-    \cdline{\ewrite{\rtna}{\q+\ptlast}{n};}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptlast}{n};}~\\
     \cdline{\esync(\q);}~\\
     \cdline{\efreeL(o,n)}~\\
   }~\\
@@ -126,9 +126,9 @@ Let $\ptlink = 0, \ptdata = 1, \pthead = 0, \pttail = 1, \ptlast = 2, \ptcc = 3,
   \pind{
     \cdline{\elet{o}{\eread{\rtat}{\q+\ptcc}}{}}~\\
     \cdline{\elet{n}{o+1}{}}~\\
-    \cdline{\ewrite{\rtat}{\q+\ptcc}{n}}~\\
+    \cdline{\ewrite{\wtat}{\q+\ptcc}{n}}~\\
     \cdline{\elet{\c}{\ealloc{1}}{}}~\\
-    \cdline{\ewrite{\rtna}{\c}{0};}~\\
+    \cdline{\ewrite{\wtna}{\c}{0};}~\\
     \cdline{\erepeat{}}~\\
     \pind{
       \cdline{\elet{i}{\eread{\rtna}{\c}}{}}~\\
@@ -137,7 +137,7 @@ Let $\ptlink = 0, \ptdata = 1, \pthead = 0, \pttail = 1, \ptlast = 2, \ptcc = 3,
         \cdline{\elet{c_i}{\eread{\rtat}{\q+\ptuc+i}}{}}~\\
         \cdline{c_i == n}~\\
       }
-      \cdline{\ewrite{\rtna}{\c}{i+1};}~\\
+      \cdline{\ewrite{\wtna}{\c}{i+1};}~\\
       \cdline{i+1 == \nThreads}~\\
     }~\\
     \cdline{\efree(\c)}~\\
@@ -151,12 +151,12 @@ Let $\ptlink = 0, \ptdata = 1, \pthead = 0, \pttail = 1, \ptlast = 2, \ptcc = 3,
     \cdline{\eelse}~\\
     \pind{
       \cdline{\elet{\c}{\ealloc{1}}{}}~\\
-      \cdline{\ewrite{\rtna}{\c}{o};}~\\
+      \cdline{\ewrite{\wtna}{\c}{o};}~\\
       \cdline{\erepeat{}}~\\
       \pind{
         \cdline{\elet{n'}{\eread{\rtna}{\c}}{}}~\\
         \cdline{\elet{n''}{\eread{\rtna}{n'+\ptlink}}{}}~\\
-        \cdline{\ewrite{\rtna}{\c}{n''};}~\\
+        \cdline{\ewrite{\wtna}{\c}{n''};}~\\
         \cdline{\efree(n'+\ptlink);}~\\
         \cdline{n'' == n}~\\
       }
@@ -323,7 +323,7 @@ STS at $\gname_o$, $\iota_o$:
   \pline[\top]{
     \varPsi(\emptyset,\emptyset)
     \ast \lraw(\sent)}~\\
-  \cdline{\ewrite{\rtna}{\sent + \ptlink}{0};}~\\
+  \cdline{\ewrite{\wtna}{\sent + \ptlink}{0};}~\\
   \pline[\top]{
     \varPsi(\emptyset,\emptyset)
     \ast \Prtcl{\sent+\ptlink:\snull|\prlink(\gname)}^1
@@ -344,8 +344,8 @@ STS at $\gname_o$, $\iota_o$:
     \ast \Prtcl{\sent+\ptlink:\snull|\prlink(\gname)}^{1/(\nThreads+1)}
     \ast \bigast_{i<4+\nThreads} \lraw(\q+i)
   }~\\
-  \cdline{\ewrite{\rtna}{\q+\pthead}{\sent};}~\\
-  \cdline{\ewrite{\rtna}{\q+\pttail}{\sent};}~\\
+  \cdline{\ewrite{\wtna}{\q+\pthead}{\sent};}~\\
+  \cdline{\ewrite{\wtna}{\q+\pttail}{\sent};}~\\
   \pline[\top]{
     \begin{aligned}
     & \varPsi(\emptyset,\emptyset)
@@ -355,8 +355,8 @@ STS at $\gname_o$, $\iota_o$:
       \ast \Prtcl{\q+\pttail:\sinv(\sent)|\prtail}_W \\
     \end{aligned}
   }~\\
-  \cdline{\ewrite{\rtna}{\q+\ptlast}{\sent};}~\\
-  \cdline{\ewrite{\rtna}{\q+\ptcc}{0};}~\\
+  \cdline{\ewrite{\wtna}{\q+\ptlast}{\sent};}~\\
+  \cdline{\ewrite{\wtna}{\q+\ptcc}{0};}~\\
   \pline[\top]{
     \begin{aligned}
     & \varPsi(\emptyset,\emptyset)
@@ -371,7 +371,7 @@ STS at $\gname_o$, $\iota_o$:
   \begin{psubenv}{Frame}
     \pline[\top]{\bigast_{\tid<\nThreads} \lraw(\q+\ptuc+\tid)}~\\
     \cdline{\elet{\c}{\ealloc{1}}{}}~\\
-    \cdline{\ewrite{\rtna}{\c}{0};}~\\
+    \cdline{\ewrite{\wtna}{\c}{0};}~\\
     \pline[\top]{\efracn{\c}{0} \ast \bigast_{\tid<\nThreads} \lraw(\q+\ptuc+\tid)}~\\
     \cdline{\erepeat{}}~\\
     \pind{
@@ -385,8 +385,8 @@ STS at $\gname_o$, $\iota_o$:
         \ast \efracn{\c}{m} 
         \ast \bigast_{j<m} \Prtcl{\q+\ptuc+j:\sinv(0,\emptyset)|\prucount(j)}_W
         \ast \bigast_{m \leq j<\nThreads} \lraw(\q+\ptuc+j)}~\\
-      \cdline{\ewrite{\rtna}{\q+\ptuc+i}{0};}~\\
-      \cdline{\ewrite{\rtna}{\c}{i+1};}~\\
+      \cdline{\ewrite{\wtna}{\q+\ptuc+i}{0};}~\\
+      \cdline{\ewrite{\wtna}{\c}{i+1};}~\\
       \pline[\top]{
         \efracn{\c}{m+1} 
         \ast \bigast_{j<m+1} \Prtcl{\q+\ptuc+j:\sinv(0,\emptyset)|\prucount(j)}_W
@@ -480,7 +480,7 @@ STS at $\gname_o$, $\iota_o$:
   \cdline{\elet{n'}{\eread{\rtat}{n + \ptlink}}{}}~\\
   \cdline{\eif \; n' == 0}~\\
   \cdline{\ethen \; n}~\\
-  \cdline{\eelse \; \ewrite{\rtat}{\q+\pttail}{n'}; 0}~\\
+  \cdline{\eelse \; \ewrite{\wtat}{\q+\pttail}{n'}; 0}~\\
   \pline[\top]{
     \begin{aligned}
       \Ret x. & x = 0 \ast \user(\q,\tid,n,p) \\
diff --git a/examples/rcu.tex b/examples/rcu.tex
index 5f5a8c1c84f032405d6497164f6933b1cdbb9b0f..5fbeaeed3fd74bf8fc8c4958be5178d5b661373e 100644
--- a/examples/rcu.tex
+++ b/examples/rcu.tex
@@ -78,20 +78,20 @@
   \cdline{\rcuNew() \eqdef} ~\\
   \pind{
     \cdline{\elet{\q}{\ealloc{\nThreads+4}}{}} ~\\
-    \cdline{\ewrite{\rtna}{\q+\ptlink}{0};}~\\
-    \cdline{\ewrite{\rtna}{\q+\ptwc}{0};}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptlink}{0};}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptwc}{0};}~\\
     \cdline{\elet{sc}{\ealloc{1}}{}}~\\
-    \cdline{\ewrite{\rtna}{sc}{0};}~\\
+    \cdline{\ewrite{\wtna}{sc}{0};}~\\
     \cdline{\erepeat{}}~\\
     \pind{
       \cdline{\elet{i}{\eread{\rtna}{sc}}{}}~\\
-      \cdline{\ewrite{\rtna}{\q+\ptrc+i}{0};}~\\
-      \cdline{\ewrite{\rtna}{sc}{i+1};}~\\
+      \cdline{\ewrite{\wtna}{\q+\ptrc+i}{0};}~\\
+      \cdline{\ewrite{\wtna}{sc}{i+1};}~\\
       \cdline{i+1 == \nThreads}~\\
     }~\\
     \cdline{\efree{sc};}~\\
-    \cdline{\ewrite{\rtna}{\q+\ptnmr}{0};}~\\
-    \cdline{\ewrite{\rtna}{\q+\ptdel}{\newStack()};}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptnmr}{0};}~\\
+    \cdline{\ewrite{\wtna}{\q+\ptdel}{\newStack()};}~\\
     \cdline{\q}
   }~\\
   \\
@@ -103,7 +103,7 @@
   \cdline{\rcuQsc(\q,\tid) \eqdef}~\\
   \pind{
     \cdline{\elet{t}{\eread{\rtat}{\q+\ptwc}}{}}~\\
-    \cdline{\ewrite{\rtat}{\q+\ptrc+\tid}{t};}~\\
+    \cdline{\ewrite{\wtat}{\q+\ptrc+\tid}{t};}~\\
     \cdline{0}~\\
   }~\\
   \\
@@ -111,7 +111,7 @@
   \pind{
     \cdline{\elet{oldgc}{\eread{\rtat}{\q+\ptwc}}{}}~\\
     \cdline{\elet{newgc}{oldgc+1}{}}~\\
-    \cdline{\ewrite{\rtat}{\q+\ptwc}{newgc};}~\\
+    \cdline{\ewrite{\wtat}{\q+\ptwc}{newgc};}~\\
     \cdline{\elet{x}{\min(\eFAI(\q+\ptnmr,0),\nThreads)}{}}~\\
     \cdline{\eif \; x == 0 \; \ethen \; 0}~\\
     \cdline{\eelse \; \rcuCollect(\q,x,newgc)}~\\
@@ -122,12 +122,12 @@
   \cdline{\rcuCollect(\q,n,newgc) \eqdef}~\\
   \pind{
     \cdline{\elet{sc}{\ealloc{1}}{}}~\\
-    \cdline{\ewrite{\rtna}{sc}{0}}~\\
+    \cdline{\ewrite{\wtna}{sc}{0}}~\\
     \cdline{\erepeat{}}~\\
     \pind{
       \cdline{\elet{i}{\eread{\rtna}{sc}}{}}~\\
       \cdline{\erepeat{\eread{\rtat}{\q+\ptrc+i} == newgc};}~\\
-      \cdline{\ewrite{\rtna}{sc}{i+1}}~\\
+      \cdline{\ewrite{\wtna}{sc}{i+1}}~\\
       \cdline{i+1 == n}
     }~\\
     \cdline{\efree{sc};}~\\
@@ -136,9 +136,9 @@
   \cdline{\rcuApp(\q,p,\val) \eqdef}~\\
   \pind{
     \cdline{\elet{x}{\ealloc{2}}{}}~\\
-    \cdline{\ewrite{\rtna}{x+\ptdata}{\val'};}~\\
-    \cdline{\ewrite{\rtna}{x+\ptlink}{0};}~\\
-    \cdline{\ewrite{\rtat}{p+\ptlink}{x};}~\\
+    \cdline{\ewrite{\wtna}{x+\ptdata}{\val'};}~\\
+    \cdline{\ewrite{\wtna}{x+\ptlink}{0};}~\\
+    \cdline{\ewrite{\wtat}{p+\ptlink}{x};}~\\
     \cdline{x}~\\
   }~\\
   \\
@@ -146,9 +146,9 @@
   \pind{
     \cdline{\elet{c}{\eread{\rtat}{x+\ptlink}}{}}~\\
     \cdline{\elet{x'}{\ealloc{2}}{}}~\\
-    \cdline{\ewrite{\rtna}{x'+\ptdata}{\val};}~\\
-    \cdline{\ewrite{\rtna}{x'+\ptlink}{c};}~\\
-    \cdline{\ewrite{\rtat}{p+\ptlink}{x'};}~\\
+    \cdline{\ewrite{\wtna}{x'+\ptdata}{\val};}~\\
+    \cdline{\ewrite{\wtna}{x'+\ptlink}{c};}~\\
+    \cdline{\ewrite{\wtat}{p+\ptlink}{x'};}~\\
     \cdline{\rcuDealloc(\q,x);}~\\
     \cdline{x'}~\\
   }~\\
@@ -156,7 +156,7 @@
   \cdline{\rcuDel(\q,x,p) \eqdef}~\\
   \pind{
     \cdline{\elet{c}{\eread{\rtat}{x+\ptlink}}{}}~\\
-    \cdline{\ewrite{\rtat}{p+\ptlink}{c};}~\\
+    \cdline{\ewrite{\wtat}{p+\ptlink}{c};}~\\
     \cdline{\rcuDealloc(\q,x);}~\\
   }~\\
   \\
@@ -173,8 +173,8 @@
     \pind{
       \cdline{\elet{v}{\eread{\rtna}{p+\ptdata}}{}}~\\
       \cdline{\elet{p'}{\eread{\rtat}{p+\ptlink}}{}}~\\
-      \cdline{\ewrite{\rtna}{rptr}{\val};}~\\
-      \cdline{\ewrite{\rtna}{nptr}{p'};}~\\
+      \cdline{\ewrite{\wtna}{rptr}{\val};}~\\
+      \cdline{\ewrite{\wtna}{nptr}{p'};}~\\
       \cdline{0}~\\
     }~\\
   }~\\
@@ -472,8 +472,6 @@ states in $\List^{+}(\Nat \cup \set{\nullv})$.
 
 \subsection{Proofs}
 
-\def\prule{\rule[0.2em]{\linewidth}{0.1em}}
-
 \subsubsection{$\rcuNew$}
 
 {
@@ -506,7 +504,7 @@ states in $\List^{+}(\Nat \cup \set{\nullv})$.
           \ast \bigast_{\tid < \nThreads} \efracn{\q+\ptrc+\tid}{\Alloc}
         \end{aligned}
       } \\
-      \cdline{\ewrite{\rtna}{\q+\ptlink}{0};}~\\
+      \cdline{\ewrite{\wtna}{\q+\ptlink}{0};}~\\
       \RES{
         \begin{aligned}
         & \ownwx{[0,\nThreads] \times \Nat}
@@ -521,7 +519,7 @@ states in $\List^{+}(\Nat \cup \set{\nullv})$.
         \end{aligned}
       } \\
       \CTX{\Prtcl{\q+\ptlink:\hst(j)|\llp(\env,j)}, \snapshotValid(\env,\hst)} \\
-      \cdline{\ewrite{\rtna}{\q+\ptwc}{0};}~\\
+      \cdline{\ewrite{\wtna}{\q+\ptwc}{0};}~\\
       \RES{
         \begin{aligned}
         & \ownwx{[0,\nThreads] \times \Nat}
@@ -544,7 +542,7 @@ states in $\List^{+}(\Nat \cup \set{\nullv})$.
               \ast \bigast_{m \le \tid < \nThreads} \efracn{\q+\ptrc+\tid}{\Alloc}
         } \\
         \cdline{\elet{sc}{\ealloc{1}}{}}~\\
-        \cdline{\ewrite{\rtna}{sc}{0};}~\\
+        \cdline{\ewrite{\wtna}{sc}{0};}~\\
         \RES{\Exists m < \nThreads. \efracn{sc}{m} \ast \uRdr(m)} \\
         \cdline{\erepeat{}}
         \IND
@@ -559,7 +557,7 @@ states in $\List^{+}(\Nat \cup \set{\nullv})$.
             \ast \uRdr(m)
             \ast \bigast_{\tid < m} \rdsafe(\q,\hst,\tid)
           } \\
-          \cdline{\ewrite{\rtna}{\q+\ptrc+i}{0};}~\\
+          \cdline{\ewrite{\wtna}{\q+\ptrc+i}{0};}~\\
           \RES{
             \begin{aligned}
               &\efracn{sc}{m} 
@@ -575,7 +573,7 @@ states in $\List^{+}(\Nat \cup \set{\nullv})$.
             \ast \uRdr(m+1)
             \ast \bigast_{\tid < m+1} \rdsafe(\q,\hst,\tid)
           } \\
-          \cdline{\ewrite{\rtna}{sc}{i+1};}~\\
+          \cdline{\ewrite{\wtna}{sc}{i+1};}~\\
           \RES{\efracn{sc}{m+1}
             \ast \uRdr(m+1) 
             \ast \bigast_{\tid < m+1} \rdsafe(\q,\hst,\tid)
@@ -600,7 +598,7 @@ states in $\List^{+}(\Nat \cup \set{\nullv})$.
           \ast \bigast_{\tid < \nThreads} \rdsafe(\q,\hst,\tid)
         \end{aligned}
       } \\
-      \cdline{\ewrite{\rtna}{\q+\ptnmr}{0};}~\\
+      \cdline{\ewrite{\wtna}{\q+\ptnmr}{0};}~\\
       \RES{
         \begin{aligned}
         & \ownwx{[0,\nThreads] \times \Nat}
@@ -613,7 +611,7 @@ states in $\List^{+}(\Nat \cup \set{\nullv})$.
         \end{aligned}
       } \\
       \CTX{\Prtcl{\q+\ptnmr:(\hst,0)|\nrp(\env)}} \\
-      \cdline{\ewrite{\rtna}{\q+\ptdel}{\newStack()};}~\\
+      \cdline{\ewrite{\wtna}{\q+\ptdel}{\newStack()};}~\\
       \RES{
         \begin{aligned}
         & \ownwx{[0,\nThreads] \times \Nat}
@@ -872,8 +870,8 @@ taken out by a $\eFAI$.
         \ast \efracn{eptr}{\any}
       \end{aligned}
     }\\
-    \cdline{\ewrite{\rtna}{rptr}{\val};}~\\
-    \cdline{\ewrite{\rtna}{nptr}{p'};}~\\
+    \cdline{\ewrite{\wtna}{rptr}{\val};}~\\
+    \cdline{\ewrite{\wtna}{nptr}{p'};}~\\
     \RES{
       \begin{aligned}
         & \rcValid(\env,\hst,\tid)
@@ -952,7 +950,7 @@ taken out by a $\eFAI$.
       \ast \All i \in \dead(\hst''). \modX(\env,\tid,i)
     \end{aligned}
   }\\
-  \cdline{\ewrite{\rtat}{\q+\ptrc+\tid}{t};}~\\
+  \cdline{\ewrite{\wtat}{\q+\ptrc+\tid}{t};}~\\
   \RES{
     \begin{aligned}
     & \ownrx{\set{\tid}\times(\Nat\setminus\dead(\hst''))} 
@@ -977,7 +975,7 @@ taken out by a $\eFAI$.
       \ast \ownwx{[0,n-1] \times (\dead(\hst_2) \setminus \dead(\hst_1))}
   }\\
   \cdline{\elet{sc}{\ealloc{1}}{}}~\\
-  \cdline{\ewrite{\rtna}{sc}{0}}~\\
+  \cdline{\ewrite{\wtna}{sc}{0}}~\\
   \RES{
     \begin{aligned}
       &\Prtcl{\q+\ptwc:(\hst_2, newgc)|\wcp(\env)}_W
@@ -1036,7 +1034,7 @@ taken out by a $\eFAI$.
         \ast \ownrx{[0,i] \times (\dead(\hst_2) \setminus \dead(\hst_1))}
       \end{aligned}
     }\\
-    \cdline{\ewrite{\rtna}{sc}{i+1}}~\\
+    \cdline{\ewrite{\wtna}{sc}{i+1}}~\\
     \RES{
       \begin{aligned}
         &\efracn{sc}{i+1}
@@ -1084,7 +1082,7 @@ taken out by a $\eFAI$.
     \end{aligned}
   }\\
   \CTX{oldgc = n, newgc = n+1} \\
-  \cdline{\ewrite{\rtat}{\q+\ptwc}{newgc};}~\\
+  \cdline{\ewrite{\wtat}{\q+\ptwc}{newgc};}~\\
   \RES{
     \begin{aligned}
       &\Prtcl{\q+\ptwc:(\hst_2,newgc)|\wcp(\env)}_W
@@ -1434,7 +1432,7 @@ Both rules are trivial after unfolding the definition of $\tracespine$.~\\
   \CTX{P(\val')}\\
   \RES{\wrsafe(\q,\qcont \cons (p,\val))}\\
   \cdline{\elet{x}{\ealloc{2}}{}}~\\
-  \cdline{\ewrite{\rtna}{x+\ptdata}{\val'};}~\\
+  \cdline{\ewrite{\wtna}{x+\ptdata}{\val'};}~\\
   \RES{\wrsafe(\q,\qcont \cons (p,\val))
       \ast \fracn{x+\ptdata}{\top}{\val'}
       \ast \efracn{x+\ptlink}{\Alloc}} \\
@@ -1473,7 +1471,7 @@ Both rules are trivial after unfolding the definition of $\tracespine$.~\\
       \ast \tracespine(\env,\hst_3,\qcont \cons (p,\val))
     \end{aligned}
   }\\
-  \cdline{\ewrite{\rtna}{x+\ptlink}{0};}~\\
+  \cdline{\ewrite{\wtna}{x+\ptlink}{0};}~\\
   \RES{
     \begin{aligned}
       &\revoked(\env,\hst_1)
@@ -1497,7 +1495,7 @@ Both rules are trivial after unfolding the definition of $\tracespine$.~\\
       \ast \All \tid < \nThreads. \permX(\env,x,\tid,j)
     \end{aligned}
   }\\
-  \cdline{\ewrite{\rtat}{p+\ptlink}{x};}~\\
+  \cdline{\ewrite{\wtat}{p+\ptlink}{x};}~\\
   We can update the state of $p+\ptlink$ to 
   $\Prtcl{p+\ptlink: \hst'_3(i) | \llp(\env,i)}$ 
     or  $\Prtcl{p+\ptlink: \hst'_3(i) | \llp(\env,i)}^{\nThreads}$, \\
@@ -1560,7 +1558,7 @@ Both rules are trivial after unfolding the definition of $\tracespine$.~\\
       \ast \master{\hst'_3}
     \end{aligned}
   }\\
-  \cdline{\ewrite{\rtat}{p+\ptlink}{c};}~\\
+  \cdline{\ewrite{\wtat}{p+\ptlink}{c};}~\\
   We can update the state of $p+\ptlink$ to 
   $\Prtcl{p+\ptlink: \hst'_3(i) | \llp(\env,i)}$ 
     or  $\Prtcl{p+\ptlink: \hst'_3(i) | \llp(\env,i)}^{\nThreads}$, \\
@@ -1610,7 +1608,7 @@ $\rcuUpd$ is a combination of $\rcuApp$ and $\rcuDel$.~\\
     (c \neq 0 \land \Exists \qcont'',\val_2. \qcont' = (c,\val_2) \cons  \qcont'')}\\
   \RES{\wrsafe(\q, \qcont \cons (p,\val_0) \cons (x,\val_1) \cons \qcont')}\\
   \cdline{\elet{x'}{\ealloc{2}}{}}~\\
-  \cdline{\ewrite{\rtna}{x'+\ptdata}{\val'_1};}~\\
+  \cdline{\ewrite{\wtna}{x'+\ptdata}{\val'_1};}~\\
   \RES{\wrsafe(\q, \qcont \cons (p,\val_0) \cons (x,\val_1) \cons \qcont')
       \ast \fracn{x'+\ptdata}{\top}{\val'_1}
       \ast \efracn{x'+\ptlink}{\Alloc}} \\
@@ -1654,7 +1652,7 @@ $\rcuUpd$ is a combination of $\rcuApp$ and $\rcuDel$.~\\
       \ast \master{\hst'_3}
     \end{aligned}
   }\\
-  \cdline{\ewrite{\rtna}{x'+\ptlink}{c};}~\\
+  \cdline{\ewrite{\wtna}{x'+\ptlink}{c};}~\\
   \RES{
     \begin{aligned}
       &\revoked(\env,\hst_1) 
@@ -1676,7 +1674,7 @@ $\rcuUpd$ is a combination of $\rcuApp$ and $\rcuDel$.~\\
       \ast \All \tid < \nThreads. \permX(\env,x',\tid,j_0)
     \end{aligned}
   }\\
-  \cdline{\ewrite{\rtat}{p+\ptlink}{x'};}~\\
+  \cdline{\ewrite{\wtat}{p+\ptlink}{x'};}~\\
   We can update the state of $p+\ptlink$ to 
   $\Prtcl{p+\ptlink: \hst'_3(i) | \llp(\env,i)}$ 
     or  $\Prtcl{p+\ptlink: \hst'_3(i) | \llp(\env,i)}^{\nThreads}$, \\
diff --git a/examples/stack.tex b/examples/stack.tex
index 9bbb6021587fc87126851dc35155968dc5c5af94..87fef4b5ad110fbae614330b629db7514042c949 100644
--- a/examples/stack.tex
+++ b/examples/stack.tex
@@ -184,12 +184,12 @@ $(\popped,\pushed)$.
   \cdline{\elet{\stk}{\ealloc{2}}{}}~\\
   \pline[\top]{\varPsi(\emptyset,\emptyset)
                \ast \lraw(\stk+\pthead,\None) \ast \lraw(\stk+\ptoffer,\None)}~\\
-  \cdline{\ewrite{\rtna}{\stk+\pthead}{\nullv};}~\\
+  \cdline{\ewrite{\wtna}{\stk+\pthead}{\nullv};}~\\
   \pline[\top]{\varPsi(\emptyset,\emptyset)
               \ast \Prtcl{\stk + \pthead : \sinv(\emptyset,\emptyset) | \prhead}_W
               \ast \Prtcl{\stk + \pthead : \sinv(\emptyset,\emptyset) | \prhead}_R
               \ast \lraw(\stk+\ptoffer,\None)}~\\
-  \cdline{\ewrite{\rtna}{\stk+\ptoffer}{\nullv};}~\\
+  \cdline{\ewrite{\wtna}{\stk+\ptoffer}{\nullv};}~\\
   \pline[\top]{
     \varPsi(\emptyset,\emptyset)
     \ast \ownGhost{\gname_T}{\emptyset}
@@ -220,7 +220,7 @@ $(\popped,\pushed)$.
   \cdline{\elet{n}{\ealloc{2}}{}}~\\
   \pline[\top]{\estack(\stk,\popped,\pushed) \ast Q \ast P(\val)
                \ast \lraw(n+\ptdata,\None) \ast \lraw(n+\ptnext,\None)}~\\
-  \cdline{\ewrite{\rtna}{s+\ptdata}{\val};}~\\
+  \cdline{\ewrite{\wtna}{s+\ptdata}{\val};}~\\
   \pline[\top]{\estack(\stk,\popped,\pushed) \ast Q
                \ast \ffracn{n+\ptdata}{\val} \ast P(\val)
                \ast \lraw(n+\ptnext,\None)}~\\
@@ -228,7 +228,7 @@ $(\popped,\pushed)$.
   \pline[\top]{\estack(\stk,\popped,\pushed) \ast Q
                \ast \ffracn{n+\ptdata}{\val} \ast P(\val)
                \ast \lraw(n+\ptnext,\None)}~\\
-  \cdline{\ewrite{\rtna}{n+\ptnext}{h};}~\\
+  \cdline{\ewrite{\wtna}{n+\ptnext}{h};}~\\
   \pline[\top]{\estack(\stk,\popped,\pushed) \ast Q
                \ast \ffracn{n+\ptdata}{\val} \ast P(\val)
                \ast \ffracn{n+\ptnext}{h}}~\\
@@ -249,16 +249,16 @@ $(\popped,\pushed)$.
     \cdline{\elet{o}{\ealloc{2}}{}}~\\
     \pline[\top]{\estack(\stk,\popped,\pushed) \ast Q \ast P(\val)
                \ast \lraw(o+\ptstate,\None) \ast \lraw(o+\ptdata,\None)}~\\
-    \cdline{\ewrite{\rtna}{o+\ptdata}{\val};}~\\
+    \cdline{\ewrite{\wtna}{o+\ptdata}{\val};}~\\
     \pline[\top]{\estack(\stk,\popped,\pushed) \ast Q \ast P(\val)
                \ast \lraw(o+\ptstate,\None) \ast \ffracn{o+\ptdata}{\val}
                \ast \Exists \gname. \ownGhost{\gname}{\diamond}}~\\
-    \cdline{\ewrite{\rtna}{o+\ptstate}{0};}~\\
+    \cdline{\ewrite{\wtna}{o+\ptstate}{0};}~\\
     \pline[\top]{\estack(\stk,\popped,\pushed)
                 \ast \Prtcl{o + \ptstate: \soffr | \proffer(o+\ptdata,\gname,\val,Q,S,\popped,\pushed)}
                 \ast \ownGhost{\gname}{\diamond}}~\\
-    \cdline{\ewrite{\rtat}{\stk+\ptoffer}{o};}~\\
-    \cdline{\ewrite{\rtat}{\stk+\ptoffer}{\nullv};}~\\
+    \cdline{\ewrite{\wtat}{\stk+\ptoffer}{o};}~\\
+    \cdline{\ewrite{\wtat}{\stk+\ptoffer}{\nullv};}~\\
     \pline[\top]{\estack(\stk,\popped,\pushed)
                 \ast \Prtcl{o + \ptstate: \soffr | \proffer(o+\ptdata,\gname,\val,Q,S,\popped,\pushed)}
                 \ast \ownGhost{\gname}{\diamond}}~\\
diff --git a/fi.tex b/fi.tex
index a79180d2b75777d8bdf2b6ff09012042c6e65e29..73332fad035e8a4c4d79cb219891f96e2033aa9e 100644
--- a/fi.tex
+++ b/fi.tex
@@ -11,11 +11,13 @@
 \def\FType{\mathcal{X}}
 \def\persist{\ensuremath{\textsf{persistent}}}
 
-\paragraph{Fractionalizer} With 
-$\FType$ some first-order type (to avoid $\later$'s),
-$\varphi \in \Loc \ra \FType \ra \PropDom$, and
-$P \in \Loc \ra \Rat \ra \FType \ra \PropDom$,
-define $\fraclize{\any(\any)}{\any}{\any}$ as:
+\paragraph{Fractionalizer} We assume
+$\varphi \in \Loc \ra \Nat \ra \PropDom$, and
+$P \in \Loc \ra \Rat \ra \Nat \ra \PropDom$.
+We also assume that a parameter $X \in \Nat$ is pre-encoded from some value of 
+some first-order type $\FType$. This encoding is not known to the fractionalizer.
+
+Define $\fraclize{\any(\any)}{\any}{\any}$ as:
 
 \begin{align*}
   \fracInv(\loc,\varphi,\nspace,X,\gname) \eqdef{}& 
@@ -40,21 +42,30 @@ fractions to be in the range $\fracrng$.
 We want the following rule for splitting and merging fractions:
 
 \begin{mathpar}
+  \inferH{Fractionalizer-Imp}{
+    \All X. P(\loc,X) \implies Q(\loc,X)
+  }{
+    \fraclize{P(\loc)}{\varphi}{\pfrac} 
+    \implies \fraclize{Q(\loc)}{\varphi}{\pfrac}
+  }\\
+  \inferH{Fractionalizer-Drop}{}{
+    \fraclize{P(\loc)}{\varphi}{\pfrac} \implies \Exists X. P(\loc,\pfrac,X)
+  }\\
   \inferH{FSplitJoin}{}
   {
     \fraclize{P_1(\loc)}{\varphi}{\pfrac_1} \ast \fraclize{P_2(\loc)}{\varphi}{\pfrac_2}
-    \vsE[\nspace]
-    \fraclize{\lambda (\pfrac_x+\pfrac_y) \; X.\;
-                P_1(\loc,\pfrac_x,X)\ast P_2(\loc,\pfrac_y,X)}
+    \iff
+    \fraclize{\lambda \pfrac \; X.\;
+              P_1(\loc,\pfrac_1,X)\ast P_2(\loc,\pfrac_2,X)}
              {\varphi}{\pfrac_1 + \pfrac_2}
   }\\
   \and
   \inferH{FJoin}{}
   {
     \fraclize{P_1(\loc)}{\varphi_1}{\pfrac_1} \ast \fraclize{P_2(\loc)}{\varphi_2}{\pfrac_2}
-    \vs[\nspace]
-    \fraclize{\lambda (\pfrac_x+\pfrac_y) \; X.\;
-                P_1(\loc,\pfrac_x,X)\ast P_2(\loc,\pfrac_y,X)}
+    \implies
+    \fraclize{\lambda \pfrac \; X.\;
+              P_1(\loc,\pfrac_1,X)\ast P_2(\loc,\pfrac_2,X)}
              {\varphi_i}{\pfrac_1 + \pfrac_2}
   }\\
   \and
@@ -86,54 +97,79 @@ We want the following rule for splitting and merging fractions:
   }
 \end{mathpar}
 
-\paragraph{Persister} with $P \in \Loc \ra \FType \ra \PropDom$,
-define $\perslize{\any(\any)}{\any}$ as:
+\paragraph{Persister} We assume a predicate $P \in \Loc \ra \Nat \ra \PropDom$
+and fix a namespace $\nspace_2$ and ghost name $\gname_p$
+for the whole persister module.
+
+\def\perInv{\textsf{PersisterInv}}
+\def\perinf{\rho}
+\def\PerInfo{\textsc{PerInfo}}
 
 \begin{align*}
-  \perslize{P(\loc)}{\varphi, \nspace_1, \nspace_2, X} \eqdef{}&
-      P(\loc,X)
-      \ast \knowInv{\nspace_1}{\varphi(\loc,X)}
-      \ast \knowInv{\nspace_2}{\Exists  \pfrac. \linfo^{\pfrac}(\loc, (X,\nspace_1))} \\
-  \perslize{P(\loc)}{\varphi,\nspace_1,\nspace_2}  \eqdef{}&
-    \Exists X. \perslize{P(\loc)}{\varphi,\nspace_1, \nspace_2,X}
+  \perinf \in \PerInfo \eqdef{}
+  & \fpfunm{\Loc}{\Nat} \\
+\end{align*}
+
+
+Define $\perslize{\any(\any)}{\any}$ as:
+
+\begin{align*}
+  \psi(\rho) \eqdef{}
+  & \bigast_{\loc \in \dom{\rho}} \linfo^{\ffrac}(\loc, \rho(\loc))\\
+  \perInv(\gname,\nspace) \eqdef{}
+  & \Auth(\PerInfo, \psi, \gname, \nspace)\\
+  \perslize{P(\loc)}{\varphi, \nspace_1, X} \eqdef{}&
+    P(\loc,X)
+    \ast \knowInv{\nspace_1}{\varphi(\loc,X)}
+    \ast \ownGhost{\gname_p}{\authfrag \loc \pointsto (X,\nspace_1)}
+    \ast \perInv(\gname_p, \nspace_2) \\
+  \perslize{P(\loc)}{\varphi,\nspace_1}  \eqdef{}&
+    \Exists X. \perslize{P(\loc)}{\varphi,\nspace_1,X}
 \end{align*}
 
 \begin{mathpar}
-  \inferH{PSplitJoin}{}
+  \inferH{Persister-Imp}{
+    \All X. P(\loc,X) \implies Q(\loc,X)
+  }{
+    \perslize{P(\loc)}{\varphi} \implies \perslize{Q(\loc)}{\varphi}
+  }\\
+  \inferH{Persister-Drop}{}{
+    \perslize{P(\loc)}{\varphi} \implies \Exists X. P(\loc,X)
+  }\\
+  \inferH{Persister-SplitJoin}{}
   {
     \perslize{P_1(\loc)}{\varphi} \ast \perslize{P_2(\loc)}{\varphi}
-    \vsE[\nspace_1,\nspace_2]
+    \iff
     \perslize{\lambda X.\; P_1(\loc,X)\ast P_2(\loc,X)}{\varphi}
   }\\
   \and
-  \inferH{PViewshift}
+  \inferH{Persister-Viewshift}
   {
     \All X.
       P' \ast P(\loc,X) \ast \later\varphi(\loc,X)
-      \vs[-\nspace_1,\nspace_2] Q' \ast Q(\loc,X) \ast \later\varphi(\loc,X)
+      \vs[-\nspace_1] Q' \ast Q(\loc,X) \ast \later\varphi(\loc,X)
   }
   {
     P' \ast \perslize{P(\loc)}{\varphi}
-    \vs[\nspace_1,\nspace_2] Q' \ast \perslize{Q(\loc)}{\varphi}
+    \vs[\nspace_1] Q' \ast \perslize{Q(\loc)}{\varphi}
   } \\
   \and
-  \inferH{PHoare}
-  { \textlog{atomic}(e)
+  \inferH{Persister-Hoare}{
+    \textlog{atomic}(e)
     \\
-    \All X.\hoare%
-              {P' \ast P(\loc,X) \ast \later\varphi(\loc,X)}%
-              {e}%
-              {\Ret\val. Q' \ast Q(\loc,X) \ast \later\varphi(\loc,X)}%
-              [-\nspace_1,\nspace_2]%
-  }
-  {
+    \All X.
+    \hoare{P' \ast P(\loc,X) \ast \later\varphi(\loc,X)}%
+          {e}%
+          {\Ret\val. Q' \ast Q(\loc,X) \ast \later\varphi(\loc,X)}%
+          [-\nspace_1]
+  }{
     \hoare{P' \ast \perslize{P(\loc)}{\varphi}}%
           {e}%
           {\Ret\val. Q' \ast \perslize{Q(\loc)}{\varphi}}%
-          [\nspace_1,\nspace_2]%
+          [\nspace_1]%
   }
   \and
-  \inferH{PPersistent}{
+  \inferH{Persister-Persistent}{
     \All X. \persist(P(\loc,X))
   }{
     \persist(\perslize{P(\loc)}{\varphi})
@@ -146,7 +182,8 @@ define $\perslize{\any(\any)}{\any}$ as:
 \begin{mathpar}
   \inferH{FInvAlloc}{}{
     \linfo^{\ffrac}(\loc,\any)
-    \ast \later \varphi(\loc,X)
+    \ast \Exists X. 
+    \later\varphi(\loc,X)
     \ast P(\loc,\ffrac,X) 
     \vs[\nspace] \fraclize{P(\loc)}{\varphi}{\ffrac}
   } \\
@@ -158,47 +195,231 @@ define $\perslize{\any(\any)}{\any}$ as:
       \Exists X. \later \varphi(\loc,X) \ast P(\loc,\ffrac,X) 
   }\\
   \and
-  \inferH{PInvAlloc}{}{
-    \linfo^{\ffrac}(\loc,\any)
-    \ast \later \varphi(\loc,X)
+  \inferH{Persister-InvAlloc}{}{
+    \perInv(\gname_p, \nspace_2)
+    \ast \linfo^{\ffrac}(\loc,\any)
+    \ast \Exists X. 
+    \later\varphi(\loc,X)
     \ast P(\loc,X) 
-    \vs[\nspace_1,\nspace_2] \perslize{P(\loc)}{\varphi,\nspace_1,\nspace_2}
+    \vs[\nspace_1,\nspace_2] \perslize{P(\loc)}{\varphi,\nspace_1}
   } \\
 \end{mathpar}
 
-% \begin{mathpar}
-%   \inferH{}
-%   {P_1, P_2 \in \AssnClass(\loc)}
-%   {
-%      [P_1]_{\pfrac_1} \ast [P_2]_{\pfrac_2} \vs \; [P_i]_{\pfrac_1+\pfrac_2}
-%   }
-% \end{mathpar}
-
-% \paragraph{GPS} for any $\loc$ governed by a GPS protocol, define $\AssnClass(\loc)$ as
-
-% \begin{align*}
-%   \AssnClass(\loc) \; \eqdef & \;
-%     \setComp{\Prtcl{\loc:\protst|\prot}}
-%             {\protst \in \STATE \land \prot \in \STATE \rightarrow \PropDom}
-% \end{align*}
-
-% \paragraph{GPS-SW} for any $\loc$ governed by a GPS single-writer protocol
-
-% \begin{align*}
-%   \AssnClass(\loc) \; \eqdef & \;
-%     \setComp{\lam \gname \; \iname. \Prtcl{\loc:\protst|\prot}_R(\gname,\iname)}
-%             {\protst \in \STATE \land \prot \in \STATE \rightarrow \PropDom} \\
-%   & \cup
-%     \setComp{\lam \gname \; \iname. \Prtcl{\loc:\protst|\prot}_W(\gname,\iname)}
-%             {\protst \in \STATE \land \prot \in \STATE \rightarrow \PropDom}
-% \end{align*}
-
-
-% \paragraph{RSL} for any $\loc$ governed by an RSL construction
-
-% \begin{align*}
-%   \AssnClass(\loc) \; \eqdef & \;
-%     \setComp{\lam \gname \; \iname.\relp{\loc}{Q}(\gname,\iname)}{Q \in \VAL \rightarrow \PropDom} \\
-%     & \cup \setComp{\lam \gname \; \iname.\acqp{\loc}{Q}(\gname,\iname)}{Q \in \VAL \rightarrow \PropDom} \\
-%     & \cup \set{\lam \gname \; \iname.\linit{\loc}(\gname,\iname)}\\
-% \end{align*}
+
+\subsection{Proofs}
+
+\subsubsection{\ruleref{FSplitJoin}}
+
+\begin{proofoutline*}
+  $\fraclize{P_1(\loc)}{\varphi}{\pfrac_1} 
+        \ast \fraclize{P_2(\loc)}{\varphi}{\pfrac_2}$\\
+  \CTX{\pfrac_1,\pfrac_2 \in \fracrng}\\
+  \VARS{X_1,X_2,\gname_1,\gname_2,}\\
+  \CTX{\fracInv(\loc,\varphi,\nspace,X_1,\gname_1),\fracInv(\loc,\varphi,\nspace,X_2,\gname_2)}\\
+  ${}\implies
+      P_1(\loc,\pfrac_1,X_1) 
+      \ast \ownGhost{\gname_1}{\authfrag \pfrac_1}
+      \ast \linfo^{\pfrac_1}(\loc, (X_1,\gname_1,\nspace))
+      \ast P_2(\loc,\pfrac_2,X_2)
+      \ast \ownGhost{\gname_2}{\authfrag \pfrac_2}
+      \ast \linfo^{\pfrac_2}(\loc, (X_2,\gname_2,\nspace))$\\
+  \CTX{X_1 = X_2, \gname_1 = \gname_2} \BY agreement of $\linfo$ \\
+  ${}\implies
+      P_1(\loc,\pfrac_1,X_1) 
+      \ast P_2(\loc,\pfrac_2,X_1)
+      \ast \ownGhost{\gname_1}{\authfrag \pfrac_1 + \pfrac_2}
+      \ast \linfo^{\pfrac_1+\pfrac_2}(\loc, (X_1,\gname_1,\nspace))$ \\
+  ${}\implies
+      \left(\Lam \pfrac \; X. P_1(\loc,\pfrac_1,X) \ast P_2(\loc,\pfrac_2,X)\right)(\pfrac_1+\pfrac_2,X_1)
+      \ast \ownGhost{\gname_1}{\authfrag \pfrac_1 + \pfrac_2}
+      \ast \linfo^{\pfrac_1+\pfrac_2}(\loc, (X_1,\gname_1,\nspace))$ \\
+  ${}\implies
+      \fraclize{\Lam \pfrac \; X. P_1(\loc,\pfrac_1,X) \ast P_2(\loc,\pfrac_2,X)}
+               {\varphi}
+               {\pfrac_1 + \pfrac_2}$ \\
+\end{proofoutline*}
+
+
+\begin{proofoutline*}
+  $\fraclize{\Lam \pfrac \; X. P_1(\loc,\pfrac_1,X) \ast P_2(\loc,\pfrac_2,X)}
+           {\varphi}
+           {\pfrac_1 + \pfrac_2}$ \\
+  \VARS{X,\gname}\\
+  \CTX{\pfrac_1,\pfrac_2 \in \fracrng}\\
+  \CTX{\fracInv(\loc,\varphi,\nspace,X,\gname)}\\
+  ${}\implies\left(\Lam \pfrac \; X. P_1(\loc,\pfrac_1,X) \ast P_2(\loc,\pfrac_2,X)\right)(\pfrac_1+\pfrac_2,X)
+    \ast \ownGhost{\gname}{\authfrag \pfrac_1 + \pfrac_2}
+    \ast \linfo^{\pfrac_1+\pfrac_2}(\loc, (X,\gname,\nspace))$ \\
+  ${}\implies
+      P_1(\loc,\pfrac_1,X_1) 
+      \ast P_2(\loc,\pfrac_2,X_1)
+      \ast \ownGhost{\gname_1}{\authfrag \pfrac_1 + \pfrac_2}
+      \ast \linfo^{\pfrac_1+\pfrac_2}(\loc, (X_1,\gname_1,\nspace))$ \\
+  ${}\implies
+      P_1(\loc,\pfrac_1,X) 
+      \ast \ownGhost{\gname}{\authfrag \pfrac_1}
+      \ast \linfo^{\pfrac_1}(\loc, (X,\gname,\nspace))
+      \ast P_2(\loc,\pfrac_2,X)
+      \ast \ownGhost{\gname_2}{\authfrag \pfrac_2}
+      \ast \linfo^{\pfrac_2}(\loc, (X,\gname,\nspace))$\\
+  ${}\implies\fraclize{P_1(\loc)}{\varphi}{\pfrac_1} 
+        \ast \fraclize{P_2(\loc)}{\varphi}{\pfrac_2}$\\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{FJoin}}
+\begin{proofoutline*}
+  $\fraclize{P_1(\loc)}{\varphi}{\pfrac_1} 
+        \ast \fraclize{P_2(\loc)}{\varphi}{\pfrac_2}$\\
+  \CTX{\pfrac_1,\pfrac_2 \in \fracrng}\\
+  \VARS{X_1,X_2,\gname_1,\gname_2,}\\
+  \CTX{\fracInv(\loc,\varphi_1,\nspace,X_1,\gname_1),\fracInv(\loc,\varphi_2,\nspace,X_2,\gname_2)}\\
+  ${}\implies
+      P_1(\loc,\pfrac_1,X_1) 
+      \ast \ownGhost{\gname_1}{\authfrag \pfrac_1}
+      \ast \linfo^{\pfrac_1}(\loc, (X_1,\gname_1,\nspace))
+      \ast P_2(\loc,\pfrac_2,X_2)
+      \ast \ownGhost{\gname_2}{\authfrag \pfrac_2}
+      \ast \linfo^{\pfrac_2}(\loc, (X_2,\gname_2,\nspace))$\\
+  \CTX{X_1 = X_2, \gname_1 = \gname_2} \BY agreement of $\linfo$ \\
+  ${}\implies
+      P_1(\loc,\pfrac_1,X_1) 
+      \ast P_2(\loc,\pfrac_2,X_1)
+      \ast \ownGhost{\gname_1}{\authfrag \pfrac_1 + \pfrac_2}
+      \ast \linfo^{\pfrac_1+\pfrac_2}(\loc, (X_1,\gname_1,\nspace))$ \\
+  ${}\implies
+      \left(\Lam \pfrac \; X. P_1(\loc,\pfrac_1,X) \ast P_2(\loc,\pfrac_2,X)\right)(\pfrac_1+\pfrac_2,X_1)
+      \ast \ownGhost{\gname_1}{\authfrag \pfrac_1 + \pfrac_2}
+      \ast \linfo^{\pfrac_1+\pfrac_2}(\loc, (X_1,\gname_1,\nspace))$ \\
+  ${}\implies
+      \fraclize{\Lam \pfrac \; X. P_1(\loc,\pfrac_1,X) \ast P_2(\loc,\pfrac_2,X)}
+               {\varphi_i}
+               {\pfrac_1 + \pfrac_2}$ \\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{FViewshift}}
+\begin{proofoutline*} 
+  \CTX{\All X.
+      P' \ast P(\loc,\pfrac,X) \ast \later\varphi(\loc,X)
+      \vs[-\nspace] Q' \ast Q(\loc,\pfrac,X) \ast \later\varphi(\loc,X)}\\
+  \RES{P' \ast \fraclize{P(\loc)}{\varphi}{\pfrac}}\\
+  \VARS{X, \gname}\\
+  \CTX{\pfrac \in \fracrng, \fracInv(\loc,\varphi,\nspace,X,\gname)}\\
+  \RES{P'
+      \ast P(\loc,\pfrac,X) 
+      \ast \ownGhost{\gname}{\authfrag \pfrac}
+      \ast \linfo^{\pfrac}(\loc, (X,\gname,\nspace))}\\
+  \RES{P'
+      \ast P(\loc,\pfrac,X) 
+      \ast \ownGhost{\gname}{\authfrag \pfrac}
+      \ast \later\left(\varphi(\loc,X) \ast \ownGhost{\gname}{\authfull \ffrac}
+              \lor \ownGhost{\gname}{\authfull \ffrac,\authfrag \ffrac}\right)
+      \ast \linfo^{\pfrac}(\loc, (X,\gname,\nspace))}[-\nspace]\\
+  \RES{P'
+      \ast P(\loc,\pfrac,X) 
+      \ast \ownGhost{\gname}{\authfrag \pfrac}
+      \ast \later\varphi(\loc,X) 
+      \ast \ownGhost{\gname}{\authfull \ffrac}
+      \ast \linfo^{\pfrac}(\loc, (X,\gname,\nspace))}[-\nspace]\\
+  \RES{Q'
+      \ast Q(\loc,\pfrac,X) 
+      \ast \ownGhost{\gname}{\authfrag \pfrac}
+      \ast \later\varphi(\loc,X)
+      \ast \ownGhost{\gname}{\authfull \ffrac}
+      \ast \linfo^{\pfrac}(\loc, (X,\gname,\nspace))}[-\nspace] \BY assm.\\
+  \RES{Q' \ast \fraclize{Q(\loc)}{\varphi}{\pfrac}}\\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{FHoare}}
+
+Follows from \ruleref{FViewshift}.
+
+\subsubsection{\ruleref{Persister-Imp}}
+\begin{proofoutline*}
+  \CTX{\All X. P(\loc,X) \implies Q(\loc,X)} \\
+  $\perslize{P(\loc)}{\varphi}$\\
+  \VARS{X}\\
+  \CTX{\knowInv{\nspace_1}{\varphi(\loc,X)},\perInv(\gname_p, \nspace_2)}\\
+  ${}\implies P(\loc,X)
+      \ast \ownGhost{\gname_p}{\authfrag \loc \pointsto (X,\nspace_1)}$\\
+  ${}\implies Q(\loc,X)
+      \ast \ownGhost{\gname_p}{\authfrag \loc \pointsto (X,\nspace_1)}$ \BY assm.\\
+  ${}\implies \perslize{Q(\loc)}{\varphi}$\\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{Persister-Drop}}
+
+Trivial after unfolding definition.
+
+\subsubsection{\ruleref{Persister-Viewshift}}
+Similar to \ruleref{FViewshift}.
+
+\subsubsection{\ruleref{Persister-Hoare}}
+Follows from \ruleref{Persister-Viewshift}
+
+\subsubsection{\ruleref{Persister-Persistent}}
+Trivial since other components of the persister are already persistent.
+
+
+\subsubsection{\ruleref{FInvAlloc}}
+
+\begin{proofoutline*}
+  \RES{\linfo^{\ffrac}(\loc,\any)
+    \ast \later \varphi(\loc,X)
+    \ast P(\loc,\ffrac,X)}\\
+  \RES{\Exists \gname. \ownGhost{\gname}{\authfull \ffrac, \authfrag \ffrac}
+    \ast \linfo^{\ffrac}(\loc,\any)
+    \ast \later \varphi(\loc,X)
+    \ast P(\loc,\ffrac,X)}\\
+  \RES{\Exists \gname. \ownGhost{\gname}{\authfull \ffrac, \authfrag \ffrac}
+    \ast \linfo^{\ffrac}(\loc,(X,\gname,\nspace))
+    \ast \later \varphi(\loc,X)
+    \ast P(\loc,\ffrac,X)}\\
+  \RES{\Exists \gname. \ownGhost{\gname}{\authfrag \ffrac}
+    \ast \linfo^{\ffrac}(\loc,(X,\gname,\nspace))
+    \ast \fracInv(\loc,\varphi,\nspace,X,\gname)
+    \ast P(\loc,\ffrac,X)}\\
+  \RES{\fraclize{P(\loc)}{\varphi}{\ffrac}}
+\end{proofoutline*}
+
+\subsubsection{\ruleref{FInvDealloc}}
+\begin{proofoutline*}
+  \RES{\fraclize{P(\loc)}{\varphi}{\ffrac}}\\
+  \VARS{X,\gname}\\
+  \CTX{\fracInv(\loc,\varphi,\nspace,X,\gname)}\\
+  \RES{\ownGhost{\gname}{\authfrag \ffrac}
+    \ast \linfo^{\ffrac}(\loc,(X,\gname,\nspace))
+    \ast P(\loc,\ffrac,X)}\\
+  \RES{\later\left(\varphi(\loc,X) \ast \ownGhost{\gname}{\authfull \ffrac}
+              \lor \ownGhost{\gname}{\authfull \ffrac,\authfrag \ffrac}\right)
+      \ast \ownGhost{\gname}{\authfrag \ffrac}
+      \ast \linfo^{\ffrac}(\loc,(X,\gname,\nspace))
+      \ast P(\loc,\ffrac,X)}[-\nspace]\\
+  \RES{\later\varphi(\loc,X) 
+      \ast \ownGhost{\gname}{\authfull \ffrac,\authfrag \ffrac}
+      \ast \linfo^{\ffrac}(\loc,(X,\gname,\nspace))
+      \ast P(\loc,\ffrac,X)}[-\nspace]\\
+  \RES{\later\varphi(\loc,X) 
+      \ast \linfo^{\ffrac}(\loc,(X,\gname,\nspace))
+      \ast P(\loc,\ffrac,X)}\\
+  \RES{\linfo^{\ffrac}(\loc,\any) \ast
+      \Exists X. \later \varphi(\loc,X) \ast P(\loc,\ffrac,X) }\\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{Persister-InvAlloc}}
+\begin{proofoutline*}
+  \RES{
+    \perInv(\gname_p, \nspace_2)
+    \ast \linfo^{\ffrac}(\loc,\any)
+    \ast \later \varphi(\loc,X)
+    \ast P(\loc,X)}\\
+  \CTX{\perInv(\gname_p, \nspace_2)}\\
+  \RES{
+    \ownGhost{\gname_p}{\authfrag \loc \pointsto (X,\nspace_1)}
+    \ast \later \varphi(\loc,X)
+    \ast P(\loc,X)}\\
+  \RES{
+    \ownGhost{\gname_p}{\authfrag \loc \pointsto (X,\nspace_1)}
+    \ast \knowInv{\nspace_1}{\varphi(\loc,X)}
+    \ast P(\loc,X)}\\
+  \RES{\perslize{P(\loc)}{\varphi,\nspace_1}}\\
+\end{proofoutline*}
diff --git a/gps/escrows.tex b/gps/escrows.tex
index 30db8916ea9bb0df26cb0a5a643109eb34918fad..5cf8461cd249e15028b253d070025331bf842a12 100644
--- a/gps/escrows.tex
+++ b/gps/escrows.tex
@@ -1,12 +1,96 @@
+\section{Exchanges}
+\subsection{Proof Rules}
+\begin{mathpar}
+  \iinferH{Exchange-Intro-Left}{}{
+    \later P \vs \Exists \bname. \Exchange{P <~> Q}_\bname
+  }
+  \and
+  \iinferH{Exchange-Intro-Right}{}{
+    \later Q \vs \Exists \bname. \Exchange{P <~> Q}_\bname
+  } \\
+  \and
+  \iinferH{Exchange-Elim-Left}{
+    P \ast P \implies \bot
+  }{
+    \Exchange{P <~> Q}_\bname \vdash \later\o[P]_\bname \vs \later\o[Q]_\bname
+  }
+  \and
+  \iinferH{Exchange-Elim-Right}{
+    Q \ast Q \implies \bot
+  }{
+    \Exchange{P <~> Q}_\bname \vdash \later\o[Q]_\bname \vs \later\o[P]_\bname
+  }
+\end{mathpar}
+
+\subsection{Proof Setup}
+%
+\def\absBuffer{\textsf{abstract}}
+\begin{align*}
+  \intrB{\Exchange{P <~> Q}_\bname}(\buf) \eqdef{}
+  & \Exists \buf_0 \bsub \buf.
+    \absBuffer(\bname,\buf_0)
+    \ast \knowInv{\nspace}{\intr{P}(\buf_0) \lor \intr{Q}(\buf_0)}
+\end{align*}
+
+Note that the definition subsumes $\bnseen(\bname)$ and $\o[P]_\bname$:
+
+\begin{align*}
+  \intr{\bnseen(\bname)}(\buf) \eqdef{}
+  & \Exists \buf_0 \bsub \buf. \absBuffer(\bname,\buf_0) \\
+  \intr{\o[P]_\bname}(\any) \eqdef{}
+  & \Exists \buf_0. \absBuffer(\bname,\buf_0) \ast \intr{P}(\buf_0)
+\end{align*}
+
+\subsection{Proofs}
+
+\paragraph{\ruleref{Exchange-Intro-Left}}
+
+\begin{proofoutline*}
+  \VARS{\buf} \\
+  \RES{\later \intr{P}(\buf)} \\
+  \RES{\Exists \bname. \absBuffer(\bname,\buf) \ast \later \intr{P}(\buf)} \\
+  \RES{\Exists \bname. \absBuffer(\bname,\buf)
+         \ast \knowInv{\nspace}{\intr{P}(\buf) \lor \intr{Q}(\buf)}}\\
+  \RES{\Exists \bname. \Exchange{P <~> Q}_\bname}
+\end{proofoutline*}
+
+\paragraph{\ruleref{Exchange-Intro-Right}} similar to \ruleref{Exchange-Intro-Left}.
+
+\paragraph{\ruleref{Exchange-Elim-Left}}
+
+\begin{proofoutline*}
+  \VARS{\buf} \\
+  \CTX{\All \buf. \intr{P}(\buf) \ast \intr{P}(\buf) \implies \bot}\\
+  \RES{\later\intr{\o[P]_\bname}(\buf) \ast \intr{\Exchange{P <~> Q}_\bname}(\buf)}\\
+  \VARS{\buf_0, \buf_1}
+  \CTX{\buf_0 \bsub \buf} \\
+  \RES{\later\absBuffer(\bname,\buf_1)
+       \ast \intr{P}(\buf_1) 
+       \ast \absBuffer(\bname,\buf_0)
+       \ast \knowInv{\nspace}{\intr{P}(\buf_0) \lor \intr{Q}(\buf_0)}} \\
+  \CTX{\later\buf_0 = \buf_1} \BY agreement of $\absBuffer$\\
+  \CTX{\absBuffer(\bname,\buf_0)}\\
+  \RES{\later\intr{P}(\buf_0)
+       \ast \knowInv{\nspace}{\intr{P}(\buf_0) \lor \intr{Q}(\buf_0)}}\\
+  \RES{\later\intr{P}(\buf_0)
+       \ast \later\left(\intr{P}(\buf_0) \lor \intr{Q}(\buf_0)\right)}[-\nspace]\\
+  \RES{\later\intr{P}(\buf_0) \ast \later\intr{Q}(\buf_0)}[-\nspace] \BY assm. \\
+  \RES{\knowInv{\nspace}{\intr{P}(\buf_0) \lor \intr{Q}(\buf_0)}
+       \ast \later\intr{Q}(\buf_0)}\\
+  \RES{\later\intr{\o[Q]_\bname}(\buf) \ast \intr{\Exchange{P <~> Q}_\bname}(\buf)}\\
+\end{proofoutline*}
+
+\paragraph{\ruleref{Exchange-Elim-Right}} similar to \ruleref{Exchange-Elim-Left}.
+
 \section{Escrows}
 \subsection{Proof Rules}
 %
 \begin{mathpar}
-  \iinferH{Escrow-Init}{P \ast P \implies \bot}{
+  \iinferH{Escrow-Init}{}{
     \later Q \vs \Escrow{P ~> Q}
   }
   \and
-  \iinferH{Escrow-Apply}{}{
+  \iinferH{Escrow-Apply}{P \ast P \implies \bot}{
     \Escrow{P ~> Q} \ast \later P \vs \later Q 
   }
 \end{mathpar}
@@ -15,41 +99,22 @@
 \subsection{Proof Setup}
 %
 \begin{align*}
-  \mathbb{E}_{P,Q} \eqdef{}
-  & \set{0, 1} \times \Buf \\
-  (\stst_1, \buf_1) \ra (\stst_2, \buf_2) \eqdef{}
-  & \stst_1 = 0 \land \stst_2 = 1 \\
-  \varphi_{P,Q}((\stst, \buf)) \eqdef{}
-  & (\stst = 0 \implies Q (\buf)) 
-    \land (\stst = 1 \implies P(\buf)) \\
-  \intrB{\Escrow{P ~> Q}}(\buf) \eqdef{}
-  & \Exists \buf_0 \bsub \buf, \gname. \ownGhost{\gname}{(0, \buf_0)} \ast \All \buf. P(\buf) \ast P(\buf) \implies \bot
+  \Escrow{P ~> Q} \eqdef{}
+  & \Exists \bname. \Exchange{\bobj(P) <~> Q}_\bname
 \end{align*}
 %
 %
 \subsection{Proofs}
 %
-\janno{TODO}
-%
-\section{Exchanges}
-\subsection{Proof Rules}
-\begin{mathpar}
-  \iinferH{Exchange-Intro}{
-    P \ast P \implies \bot
-    \\ Q \ast Q \implies \bot
-  }{
-    \later (P \lor Q) \vs \Exists \bname. \Exchange{P <~> Q}_\bname
-  }
-  \and
-  \iinferH{Exhange-Elim-Left}{}{
-    \Exchange{P <~> Q}_\bname \vdash \later\o[P]_\bname \vs \later\o[Q]_\bname
-  }
-  \and
-  \iinferH{Exhange-Elim-Right}{}{
-    \Exchange{P <~> Q}_\bname \vdash \later\o[Q]_\bname \vs \later\o[P]_\bname
-  }
-\end{mathpar}
+\paragraph{\ruleref{Escrow-Init}} Follows from \ruleref{Exchange-Intro-Right}.
+
+\paragraph{\ruleref{Escrow-Apply}} Note from $P \ast P \implies \bot$ we have
+$\bobj(P) \ast \bobj(P) \implies \bobj(P \ast P) \implies \bot$. The proof then
+follows from \ruleref{Exchange-Elim-Left}, since $P \implies \o[\bobj(P)]_\bname$
+and $\bnseen(\bname) \ast \later \o[Q]_\bname \implies \later Q$.
+
 %
+
 %
 %%% Local Variables:
 %%% mode: latex
diff --git a/gps/layer2def.tex b/gps/layer2def.tex
index 0e0047fab9f6f04edbc3779b1a0ddd8f2bd2cd2a..04e0380f1f6318fe49fbcd179b721026c469b336 100644
--- a/gps/layer2def.tex
+++ b/gps/layer2def.tex
@@ -1,6 +1,6 @@
-\def\td{{\prot_{\mathrm{dup}}}}%
+\def\td{{\protint_{\mathrm{dup}}}}%
 \def\intd{\intr{\td}}%
-\def\int{\intr{\prot}}%
+\def\int{\intr{\protint}}%
 
 
 \newcommand{\GT}{\textrm{T}}
@@ -12,40 +12,113 @@
 %% \newcommand\ereadH {\intr{\All \stst' \sqsupseteq_\prot \stst, \val. \prot(\stst, \val) \ast P \implies \always Q}(\buf)}
 %% \newcommand\ereadPreC {\kmq{\proc}{\buf} \ast \Exists \buf_0 \bsub \buf. \STSone{\gamma_\prot}{\stst, \buf_0} \ast \intr P(\buf)}%
 %% \newcommand\ereadPostC {\Ret\val'. \; \Exists \buf' \futb \buf, \stst' \sqsupseteq_\prot \stst. \kmq{\proc}{\buf'} \ast \STSone{\gamma_\prot}{\stst', \buf'} \ast \intr{\always Q}(\buf')}%
+
+\def\LBeinitPre{
+  \lraw(\loc) 
+  \ast \protst \in \prot.\protspace(x) 
+  \ast \later\prot.\protint(x)(\protst, \val)
+}
+\def\LBeinitPrewBuf{
+  \intr{\lraw(\loc)}(\buf)
+  \ast \protst \in \prot.\protspace(x) 
+  \ast \later \intr{\prot.\protint(x)(\protst, \val)}(\buf)
+}
 \newcommand\LBereadHyp{%
   \All \protst' \futst_\prot \protst. 
   \left(
     \All \val.%
-    \td(\protst', \val) \ast P \vs[\uspace] Q
+    \prot.\td(x)(\protst', \val) \ast P \vs[\uspace] Q
   \right) 
   \lor 
   \left(
-    \All \protst'' \futst \protst'. 
-    \prot(\protst'', \any) \ast P \vs[\uspace] \bot 
+    \All \protst'' \futst_\prot \protst'. 
+    \prot.\protint(x)(\protst'', \any) \ast P \vs[\uspace] \bot 
   \right)%
 }%
-\newcommand\LBereadPre{\protAt{\loc}{\protst}{\prot} \ast P}%
+\def\LBereadHypwBuf{
+  \All \buf. \All \protst' \futst_\prot \protst. 
+  \left(
+    \All \val.%
+    \intr{\prot.\td(x)(\protst', \val)}(\buf) 
+    \ast \intr{P}(\buf) 
+    \vs[\uspace] 
+    \intr{Q}(\buf)
+  \right) 
+  \lor 
+  \left(
+    \All \protst'' \futst_\prot \protst'. 
+    \intr{\prot.\protint(x)(\protst'', \any)}(\buf) 
+    \ast \intr{P}(\buf) \vs[\uspace] \bot 
+  \right)%
+}
+\newcommand\LBereadPre{P \ast \protAt{\loc}{\protst}{\prot(x)}}%
 \newcommand\LBereadPost{\Exists \protst'.
-  \protAt{\loc}{\protst'}{\prot} \ast Q}
+  \protAt{\loc}{\protst'}{\prot(x)} \ast Q}
 %
-\newcommand\LBewriteHypA{P \vs \prot(\stst'', \val) * Q}
+\newcommand\LBewriteHypA{P \vs \prot.\protint(x)(\stst'', \val) \ast Q}
 \newcommand\LBewriteHypB{
   \All \stst' \futst_\prot \stst. 
-  \prot(\stst', \_) \ast P 
+  \prot.\protint(x)(\stst', \_) \ast P 
   \implies \stst'' \futst_\prot \stst'
 }
-\newcommand\LBewritePre{\protAt{\loc}{\protst}{\prot} \ast P}%
-\newcommand\LBewritePost{\protAt{\loc}{\protst''}{\prot} \ast Q}%
+\def\LBewriteHypAwBuf{
+  \All \buf.
+  \intr{P}(\buf)
+  \vs 
+  \intr{\prot.\protint(x)(\stst'', \val)}(\buf)
+  \ast \intr{Q}(\buf)
+}
+\def\LBewriteHypBwBuf{
+  \All \buf.
+  \All \stst' \futst_\prot \stst. 
+  \intr{\prot.\protint(x)(\stst', \_)}(\buf) 
+  \ast \intr{P} (\buf)
+  \implies \stst'' \futst_\prot \stst'
+}
+\newcommand\LBewritePre{P \ast \protAt{\loc}{\protst}{\prot(x)}}%
+\newcommand\LBewritePost{\protAt{\loc}{\protst''}{\prot(x)} \ast Q}%
 %
 %
-\newcommand\LBecasHypA{{\All \stst' \futst_\prot \stst. \prot(\stst', \val_o) \ast P \vs \Exists \stst'' \futst_\prot \stst. \prot(\stst'', \val_n) * Q}}
-\newcommand\LBecasHypB{\All \stst' \futst_\prot \stst. \All \valB \neq \val_o.
-  \td(\stst', \valB) \ast P \vs R }
+\newcommand\LBecasHypA{{
+  \All \stst' \futst_\prot \stst. 
+  \prot.\protint(x)(\stst', \val_o) 
+  \ast P 
+  \vs 
+  \Exists \stst'' \futst_\prot \stst. 
+  \prot.\protint(x)(\stst'', \val_n) 
+  \ast Q}}
+\newcommand\LBecasHypB{
+  \All \stst' \futst_\prot \stst. 
+  \All \valB \neq \val_o.
+    \prot.\td(x)(\stst', \valB) 
+    \ast P 
+    \vs 
+    R
+}
+\def\LBecasHypAwBuf{
+  \All \buf.
+  \All \stst' \futst_\prot \stst. 
+  \intr{\prot.\protint(x)(\stst', \val_o)}(\buf)
+  \ast \intr{P }(\buf)
+  \vs 
+  \Exists \stst'' \futst_\prot \stst. 
+  \intr{\prot.\protint(x)(\stst'', \val_n)}(\buf)
+  \ast \intr{Q}(\buf)
+}
+\def\LBecasHypBwBuf{
+  \All \buf.
+  \All \stst' \futst_\prot \stst. 
+  \All \valB \neq \val_o.
+    \intr{\prot.\td(x)(\stst', \valB)}(\buf)
+    \ast \intr{P}(\buf)
+    \vs 
+    \intr{R}(\buf)
+}
 \newcommand\LBecasPre{%
-  \protAt{\loc}{\protst}{\prot} \ast P%
+  P \ast \protAt{\loc}{\protst}{\prot(x)}
 }%
 \newcommand\LBecasPost{\Ret\val.
-    \Exists \protst'' \futst_\prot \protst. \Proto[\loc : \protst'' | \prot] 
+    \Exists \protst'' \futst_\prot \protst. \Prtcl{\loc : \protst'' | \prot(x)}
     \ast \left((\val = 1\ast Q) \lor 
      (\val = 0 \ast R)\right) 
 }
diff --git a/gps/protocols-frac.tex b/gps/protocols-frac.tex
new file mode 100644
index 0000000000000000000000000000000000000000..3ee0974f76dd33e5c29065350df4e2d86ad40c77
--- /dev/null
+++ b/gps/protocols-frac.tex
@@ -0,0 +1,513 @@
+\section{Fractional Protocols}
+
+\subsection{Definitions}
+
+\def\PrFRaw{\textlog{FracRaw}}
+\begin{align*}
+  \PrFRaw(\protspace,x,\protst,\buf)(\loc,\pfrac,n) \eqdef{}
+  & \protst \in \protspace(x) 
+    \ast \Exists \gname. n = \rawEncoder((\gname,x))
+    \ast \PrR(\protst,\buf,\gname) \\
+  &{}\ast \knowInv{\nspace'.\loc}{\Exists \ststs.\writer(\gname)(\ststs)} \\
+  \intr{\Prtcl{\loc : \protst \in \protspace | \protint(x)}^{\pfrac}}(\buf) \eqdef{}
+  & \pfrac \in \fracrng
+    \ast \fraclize{\PrFRaw(\protspace,x,\protst,\buf)(\loc)}
+                  {\PrInvRaw(\protspace,\protint),\nspace.\loc}
+                  {\pfrac}\\
+  \Prtcl{\loc : \protst | \prot(x)}^{\pfrac} \eqdef{}
+  & \Prtcl{\loc : \protst \in \prot.\protspace | \prot.\protint(x)}^{\pfrac}
+\end{align*}
+
+\subsection{Proofs}
+
+\subsubsection{\ruleref{FracProto-SplitJoin}}
+
+\begin{align*}
+  & \intr{\Prtcl{\loc : \protst | \prot(x)}^p}(\buf)
+    \ast \intr{\Prtcl{\loc : \protst | \prot(x)}^q}(\buf) \\
+  {}\equiv{}
+  & p \in \fracrng
+    \ast \fraclize{\PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\protint),\nspace.\loc}
+                  {p} \\
+  &{}\ast q \in \fracrng
+    \ast \fraclize{\PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\protint),\nspace.\loc}
+                  {q}\\
+  {}\Lra{}& 
+    (p+q) \in \fracrng
+    \ast \fraclize{\Lam n.
+                    \PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc,p,n)
+                    \ast \PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc,q,n)}
+                  {\PrInvRaw(\prot.\protspace,\protint),\nspace.\loc}
+                  {p+q}\\
+  & \quad \by \ruleref{FSplitJoin}\\
+  {}\Lra{}& 
+    (p+q) \in \fracrng
+    \ast \fraclize{\Lam n.
+                    \PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc,p+q,n)}
+                  {\PrInvRaw(\prot.\protspace,\protint),\nspace.\loc}
+                  {p+q}\\
+  & \quad \by \ruleref{Fractionalizer-Imp}\\
+  {}\equiv{}
+  & \intr{\Prtcl{\loc : \protst | \prot(x)}^{p+q}}(\buf)
+\end{align*}
+
+\subsubsection{\ruleref{FracProto-Agree}}
+
+Similar to \ruleref{SWProto-Readers-Agree}.
+
+\begin{align*}
+  & \intr{\Prtcl{\loc : \protst_1 | \prot(x_1)}^p}(\buf)
+    \ast \intr{\Prtcl{\loc : \protst_2 | \prot(x_2)}^q}(\buf) \\
+  {}\equiv{}
+  & p \in \fracrng
+    \ast \fraclize{\PrFRaw(\prot.\protspace,x_1,\protst_1,\buf)(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\protint),\nspace.\loc}
+                  {p} \\
+  &{}\ast q \in \fracrng
+    \ast \fraclize{\PrFRaw(\prot.\protspace,x_2,\protst_2,\buf)(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\protint),\nspace.\loc}
+                  {q}\\
+  {}\implies{}& 
+    p,q \in \fracrng
+    \ast \fraclize{\Lam n.
+                    \PrFRaw(\prot.\protspace,x_1,\protst_1,\buf)(\loc,p,n)
+                    \ast \PrFRaw(\prot.\protspace,x_2,\protst_2,\buf)(\loc,q,n)}
+                  {\PrInvRaw(\prot.\protspace,\protint),\nspace.\loc}
+                  {p+q}\\
+  & \quad \by \ruleref{FSplitJoin}\\
+  {}\implies{}& 
+    p,q \in \fracrng
+    \ast \Exists n. 
+      \PrFRaw(\prot.\protspace,x_1,\protst_1,\buf)(\loc,p,n)
+      \ast \PrFRaw(\prot.\protspace,x_2,\protst_2,\buf)(\loc,q,n)\\
+  & \quad \by \ruleref{Fractionalizer-Drop}\\
+  {}\implies{}&
+    \Exists \gname_1,\gname_2. 
+    n = \rawEncoder((\gname_1,x_1)) = \rawEncoder((\gname_2,x_2))
+    \ast \protst_1 \in \prot.\protspace(x_1)
+    \ast \protst_2 \in \prot.\protspace(x_2) \\
+  &
+    {}\ast \PrR(\protst_1,\buf,\gname_1)
+    \ast \PrR(\protst_2,\buf,\gname_2) \\
+  {}\implies{}
+  & \gname_1 = \gname_2 \ast x_1 = x_2 
+    \ast \protst_1 \in \prot.\protspace(x_1)
+    \ast \protst_2 \in \prot.\protspace(x_2)\\
+  &{} \ast \Exists \buf_1, \buf_2. 
+    \buf_1 \bsub \buf \ast \buf_2 \bsub \buf
+    \ast \reader(\gname_1)((\protst_1,\buf_1)::\any)
+    \ast \reader(\gname_2)((\protst_2,\buf_2)::\any) \\
+  {}\implies{}
+  & x_1 = x_2
+    \ast (\protst_1 \futst_\prot \protst_2
+          \lor \protst_2 \futst_\prot \protst_1) \\
+  &\quad \by \ruleref{lem:rawprt-reader-ordered} 
+            \text{ and } \ruleref{lem:rawprt-state-ordered}
+\end{align*}
+
+\subsubsection{\ruleref{FracProto-Init}}
+
+Similar to \ruleref{SWProto-Init}.
+
+\begin{proofoutline*}
+  \VARS{\buf,\proc} \\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{\LBeinitPrewBuf}\\
+  \CTX{\protst \in \prot.\protspace(x)}\\
+  \cdline{\ewrite{\wtna}{\loc}{\val}}\\
+  \RES{
+    \begin{aligned}
+      \Exists \buf' \futb \buf. 
+      & \bseen{\proc}{\buf'}
+      \ast \Exists \gname, \ststs, n. n = \rawEncoder(\gname, x)
+      \ast \ststs = ((\protst,\buf')::\any)\\
+      &{}
+      \ast \writer(\gname)(\ststs) 
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+      \ast \linfo^{\ffrac}(\loc,\any)
+    \end{aligned}
+  } \\
+  \CTX{\buf',\gname,n, \buf' \futb \buf, \bseen{\proc}{\buf'},
+       \ststs = ((\protst,\buf')::\any), n = \rawEncoder(\gname, x)}\\
+  \RES{
+    \writer(\gname)(\ststs) 
+    \ast \reader(\gname)(\ststs) 
+    \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  } \BY \ruleref{lem:rawprt-writer-fork}\\
+  \RES{
+    \knowInv{\nspace'.\loc}{\Exists \ststs. \writer(\gname)(\ststs)}
+    \ast \PrR(\protst,\buf',\gname) 
+    \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  }\\
+  \RES{
+    \PrFRaw(\prot.\protspace,x,\protst,\buf')(\loc,\ffrac,n) 
+    \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  }\\
+  \RES{
+    \fraclize{\PrFRaw(\prot.\protspace,x,\protst,\buf')(\loc)}
+             {\PrInvRaw(\prot.\protspace,\prot.\protint)}
+             {\ffrac}
+  } \BY \ruleref{FInvAlloc}\\
+  \RES{\Exists \buf' \futb \buf. 
+    \bseen{\proc}{\buf'}
+    \ast \intr{\Prtcl{\loc:\protst|\prot(x)}^{\ffrac}}(\buf')
+  }\\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{FracProto-Read}}
+
+Similar to \ruleref{SWProto-Read}.
+
+\begin{proofoutline*}
+  \CTX{\LBereadHypwBuf}\\
+  \VARS{\buf,\proc} \\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{
+    \intr{P}(\buf) 
+    \ast \intr{\Prtcl{\loc : \protst | \prot(x)}^{\pfrac}}(\buf)
+  } \\
+  \CTX{\pfrac \in \fracrng}\\
+  \RES{
+    \intr{P}(\buf)
+    \ast \fraclize{\PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+                  {\pfrac}
+  }
+  \IND
+    \VARS{n}\\
+    \RES{\intr{P}(\buf)
+        \ast \PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc,\pfrac,n)
+        \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    }[-\nspace.\loc] \BY \ruleref{FHoare} \\
+    \VARS{\gname,\gname',x'}\\
+    \CTX{\protst \in \prot.\protspace(x), 
+        n = \rawEncoder((\gname,x)),
+        \later n = \rawEncoder((\gname',x')),
+        \knowInv{\nspace'.\loc}{\Exists \ststs.\writer(\gname)(\ststs)}}\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrR(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname',x')
+    }[-\nspace.\loc]\\
+    \PFHAVE{\gname = \gname', x = x'} \BY agreement on $n$\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrR(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    }[-\nspace.\loc]\\
+    \cdline{\eread{\rtat}{\loc}}\\
+    \RES{
+      \Ret\val.
+        \Exists \buf' \futb \buf, \protst' \futst_\prot \protst.
+        \bseen{\proc}{\buf'}
+        \ast \intr{Q}(\buf')
+        \ast \PrR(\protst', \buf',\gname)
+        \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    }[-\nspace.\loc]
+      \BY \ruleref{RawProto-Read}\\
+    \RES{
+      \Ret\val.
+        \Exists \buf' \futb \buf, \protst' \futst_\prot \protst.
+        \bseen{\proc}{\buf'}
+        \ast \intr{Q}(\buf')
+        \ast \PrFRaw(\prot.\protspace,x,\protst', \buf')(\loc,\pfrac,n)
+        \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    }[-\nspace.\loc]
+  \UNIND
+  \RES{
+      \Ret\val.
+        \Exists \buf' \futb \buf, \protst' \futst_\prot \protst.
+        \bseen{\proc}{\buf'}
+        \ast \intr{Q}(\buf')
+        \ast \fraclize{\PrFRaw(\prot.\protspace,x,\protst',\buf')(\loc)}
+                      {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+                      {\pfrac}
+    }\\
+    \RES{\Ret\val. 
+      \Exists \buf' \futb \buf.
+      \Exists \protst' \futst_\prot \protst. 
+      \bseen{\proc}{\buf'}
+      \ast \intr{\Prtcl{\loc : \protst' | \prot(x)}^{\pfrac}}(\buf') 
+      \ast \intr{Q}(\buf')
+    } \\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{FracProto-Write}}
+\begin{proofoutline*}
+  \CTX{\LBewriteHypAwBuf}\\
+  \CTX{\LBewriteHypBwBuf}\\
+  \VARS{\buf,\proc} \\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{
+      \intr{P}(\buf) 
+      \ast \intr{\Prtcl{\loc : \protst | \prot(x)}^{\pfrac}}(\buf)
+    } \\
+    \RES{
+      \intr{P}(\buf)
+      \ast \fraclize{\PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc)}
+                    {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+                    {\pfrac}
+    }
+    \IND
+      \VARS{n}\\
+      \RES{\intr{P}(\buf)
+          \ast \PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc,n)
+          \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+      }[-\nspace.\loc] \BY \ruleref{Persister-Hoare} \\
+      \VARS{\gname,\gname',x'}\\
+      \CTX{\protst \in \protspace(x), 
+          n = \rawEncoder((\gname,x)),
+          \later n = \rawEncoder((\gname',x')),
+          \knowInv{\nspace'.\loc}{\Exists \ststs.\writer(\gname)(\ststs)}}\\
+      \RES{
+        \intr{P}(\buf)
+        \ast \PrR(\protst,\buf,\gname)
+        \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname',x')
+      }[-\nspace.\loc]\\
+      \PFHAVE{\gname = \gname', x = x'} \BY agreement on $n$\\
+      \RES{
+        \intr{P}(\buf)
+        \ast \PrR(\protst,\buf,\gname)
+        \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+      }[-\nspace.\loc]\\
+      Open $\nspace'.\loc$
+      \IND
+        \RES{
+          \intr{P}(\buf)
+          \ast \later\Exists \ststs. \writer(\gname)(\ststs)
+          \ast \PrR(\protst,\buf,\gname)
+          \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+        }[-\nspace.\loc,-\nspace'.\loc]\\
+        \RES{
+          \intr{P}(\buf)
+          \ast \Exists \ststs. \writer(\gname)(\ststs)
+          \ast \PrR(\protst,\buf,\gname)
+          \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+        }[-\nspace.\loc,-\nspace'.\loc]\\
+        \RES{
+          \intr{P}(\buf)
+          \ast \Exists \buf_0, \protst' \futst_\prot \protst. 
+          \PrW(\protst',\buf_0,\gname)
+          \ast \PrR(\protst,\buf,\gname)
+          \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+        }[-\nspace.\loc,-\nspace'.\loc]\\
+        \CTX{\buf_0, \protst' \futst_\prot \protst}
+        \RES{
+          \intr{P}(\buf)
+          \ast \PrW(\protst',\buf_0,\gname)
+          \ast \PrR(\protst,\buf,\gname)
+          \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+        }[-\nspace.\loc,-\nspace'.\loc]\\
+        \cdline{\ewrite{\wtat}{\loc}{\val},\proc}\\
+        \RES{
+          \Exists \buf' \futb \buf.
+          \bseen{\proc}{\buf'}
+          \ast \intr{Q}(\buf')
+          \ast \PrW(\protst'', \buf',\gname)
+          \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+        }[-\nspace.\loc]
+          \BY \ruleref{RawProto-Write}\\
+        \prule\\
+        \GOAL{
+          \All \buf' \futb \buf, \buf_1 \bsub \buf_0. 
+          \intr{\prot.\protint(x)(\protst', \any)}(\buf_1)
+          \ast \intr{P}(\buf')
+          \vs[-\nspace]
+          \protst'' \futst_\prot \protst'
+          \ast\later\intr{\prot.\protint(x)(\protst'', \val)}(\buf') 
+          \ast \intr{Q}(\buf')
+        } 
+        \IND
+          First, 
+          $\intr{\prot.\protint(x)(\protst, \any)}(\buf')
+              \ast \intr{P}(\buf)
+            \implies
+            \Exists \buf''. \buf'' \futb \buf' 
+              \ast \buf'' \futb \buf_1
+              \ast \intr{\prot.\protint(x)(\protst, \any)}(\buf'')
+              \ast \intr{P}(\buf'')
+            \implies \protst'' \futst_\prot \protst'
+            $, \\ by 2nd assm. So:\\
+          \RES{\intr{\prot.\protint(x)(\protst, \any)}(\buf_1)
+                \ast \intr{P}(\buf')
+                \ast \protst'' \futst_\prot \protst'}\\
+          \RES{\protst'' \futst_\prot \protst'
+                \ast\later\intr{\prot.\protint(x)(\protst'', \val)}(\buf') 
+                \ast \intr{Q}(\buf')} \BY 1st assm.
+        \UNIND
+        \prule
+      \UNIND
+      \RES{
+        \Exists \buf' \futb \buf.
+        \bseen{\proc}{\buf'}
+        \ast \intr{Q}(\buf')
+        \ast \PrFRaw(\prot.\protspace,x,\protst'', \buf')(\loc,n)
+        \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+      }[-\nspace.\loc]
+    \UNIND
+    \RES{
+      \Exists \buf' \futb \buf.
+      \bseen{\proc}{\buf'}
+      \ast \intr{Q}(\buf')
+      \ast \fraclize{\PrFRaw(\prot.\protspace,x,\protst'', \buf')(\loc)}
+                    {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+                    {\pfrac}
+    }\\
+    \RES{
+      \Exists \buf' \futb \buf.
+      \bseen{\proc}{\buf'}
+      \ast \intr{\Prtcl{\loc : \protst' | \prot(x)}^{\pfrac}}(\buf') 
+      \ast \intr{Q}(\buf')
+    } \\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{FracProto-CAS}}
+\begin{proofoutline*}
+  \CTX{\LBecasHypAwBuf}\\
+  \CTX{\LBecasHypBwBuf}\\
+  \VARS{\buf,\proc} \\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{\intr{P}(\buf)
+    \ast \intr{\Prtcl{\loc : \protst | \prot(x)}^{\pfrac}}(\buf)
+  } \\
+  \CTX{\pfrac \in \fracrng}
+  \RES{
+    \intr{P}(\buf)
+    \ast \fraclize{\PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+                  {\pfrac}
+  }
+  \IND
+    \VARS{n}\\
+    \RES{\intr{P}(\buf)
+        \ast \PrFRaw(\prot.\protspace,x,\protst,\buf)(\loc,\pfrac,n)
+        \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    }[-\nspace.\loc] \BY \ruleref{FHoare} \\
+    \VARS{\gname,\gname',x'}\\
+    \CTX{\protst \in \prot.\protspace(x), 
+        n = \rawEncoder((\gname,x)),
+        \later n = \rawEncoder((\gname',x')),
+        \knowInv{\nspace'.\loc}{\Exists \ststs.\writer(\gname)(\ststs)}}\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrR(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname',x')
+    }[-\nspace.\loc]\\
+    \PFHAVE{\gname = \gname', x = x'} \BY agreement on $n$\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrR(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    }[-\nspace.\loc]\\
+    Open $\nspace'.\loc$
+    \IND
+      \RES{
+        \intr{P}(\buf)
+        \ast \later\Exists \ststs. \writer(\gname)(\ststs)
+        \ast \PrR(\protst,\buf,\gname)
+        \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+      }[-\nspace.\loc,-\nspace'.\loc]\\
+      \RES{
+        \intrB{P \ast \later\Exists \ststs. \writer(\gname)(\ststs)}(\buf)
+        \ast \PrR(\protst,\buf,\gname)
+        \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+      }[-\nspace.\loc,-\nspace'.\loc]\\
+      \cdline{\ecas{\loc}{\val_o}{\val_n}, \proc}\\
+      \RES{
+        \begin{aligned}
+          \Ret\val. \Exists \buf' \futb \buf, \protst'' \futst_\prot \protst. 
+          & \bseen{\proc}{\buf'}
+            \ast \PrR(\protst'',\buf',\gname) 
+            \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)\\ 
+          &{}
+            \ast \later\Exists \ststs. \writer(\gname)(\ststs)
+            \ast (\val = 1 \ast \intr{Q}(\buf'))
+            \ast (\val = 0 \ast \intr{R}(\buf'))
+        \end{aligned}
+      }[-\nspace.\loc,-\nspace'.\loc] \\
+        \BY \ruleref{RawProto-CAS} \\
+      \prule\\
+      \GOAL{
+        \begin{aligned}
+          \All \buf. \All \protst' \futst_\prot \protst.
+          & \intr{\prot.\protint(x)(\protst', \val_o)}(\buf) 
+          \ast \intrB{P\ast \later\Exists \ststs. \writer(\gname)(\ststs)}(\buf) \\
+          & {}\vs[\mask_1][\mask_2]{}
+          \Exists \protst'' \futst_\prot \protst', \protst_w. 
+            \writer(\gname)((\protst_w,\any)::\any)
+            \ast \intrB{Q \ast \prot.\protint(x)(\protst'', \val_n)}(\buf))
+        \end{aligned}
+      }\\
+      Follows trivially from the first assumption.\\
+      \prule\\
+      \GOAL{
+        \begin{aligned}
+          \All \buf. \All \protst', \protst'' \futst_\prot \protst'.
+          & \writer(\gname)((\protst'',\any)::\any)
+          \ast \intrB{(Q \ast \prot.\protint(x)(\protst'', \val_n))\subst{\protst_w}{\protst'}}(\buf) \\
+          &{}\vs[\mask_2][\mask_1]{}
+          \later\intr{\prot.\protint(x)(\protst'', \val_n)}(\buf) 
+          \ast \intrB{Q \ast \later\Exists \ststs. \writer(\gname)(\ststs)}(\buf)
+        \end{aligned}
+      }\\
+      Trivially.\\
+      \prule\\
+      \GOAL{
+        \All \buf.
+        \All \valB \neq \val_o. 
+        \intr{\prot.\td(x)(\protst, \valB)}(\buf) 
+        \ast \intrB{P \ast \later\Exists \ststs. \writer(\gname)(\ststs)}(\buf)
+        \vs
+        \intrB{R \ast \later\Exists \ststs. \writer(\gname)(\ststs)}(\buf)
+      } \\
+      Follows trivially from the second assumption.\\
+      \prule
+    \UNIND
+    Close $\nspace'.\loc$\\
+    \RES{
+      \begin{aligned}
+        \Ret\val. \Exists \buf' \futb \buf, \protst'' \futst_\prot \protst. 
+        & \bseen{\proc}{\buf'}
+          \ast \PrR(\protst'',\buf',\gname) 
+          \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)\\ 
+        &{}
+          \ast (\val = 1 \ast \intr{Q}(\buf'))
+          \ast (\val = 0 \ast \intr{R}(\buf'))
+      \end{aligned}
+    }[-\nspace.\loc]\\
+    \RES{
+      \begin{aligned}
+        \Ret\val. \Exists \buf' \futb \buf, \protst'' \futst_\prot \protst. 
+        & \bseen{\proc}{\buf'}
+          \ast \PrFRaw(\prot.\protspace,x,\protst'',\buf')(\loc,\pfrac,n) 
+          \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)\\ 
+        &{}
+          \ast (\val = 1 \ast \intr{Q}(\buf'))
+          \ast (\val = 0 \ast \intr{R}(\buf'))
+      \end{aligned}
+    }[-\nspace.\loc]
+  \UNIND
+  \RES{
+    \begin{aligned}
+      \Ret\val. \Exists \buf' \futb \buf, \protst'' \futst_\prot \protst. 
+      & \bseen{\proc}{\buf'}
+        \ast \fraclize{\PrFRaw(\prot.\protspace,x,\protst'',\buf')(\loc)}
+                      {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+                      {\pfrac} \\
+      & \ast (\val = 1 \ast \intr{Q}(\buf'))
+        \ast (\val = 0 \ast \intr{R}(\buf'))
+    \end{aligned}
+  } \\
+  \RES{
+    \Ret\val. \Exists \buf' \futb \buf, \protst'' \futst_\prot \protst. 
+      \bseen{\proc}{\buf'}
+      \ast \intr{\Prtcl{\loc:\protst''|\prot(x)}^{\pfrac}}(\buf')
+      \ast (\val = 1 \ast \intr{Q}(\buf'))
+      \ast (\val = 0 \ast \intr{R}(\buf'))
+  }
+\end{proofoutline*}
\ No newline at end of file
diff --git a/gps/protocols-plain.tex b/gps/protocols-plain.tex
new file mode 100644
index 0000000000000000000000000000000000000000..8f484ea89bdae1c6640076949c3599a8d7295636
--- /dev/null
+++ b/gps/protocols-plain.tex
@@ -0,0 +1,41 @@
+\section{Plain Protocols}
+
+\subsection{Definitions}
+
+\def\PrPRaw{\textlog{PlainRaw}}
+\begin{align*}
+  \PrPRaw(\protspace,x,\protst,\buf)(\loc,n) \eqdef{}
+  & \protst \in \protspace(x) 
+    \ast \Exists \gname. n = \rawEncoder((\gname,x))
+    \ast \PrR(\protst,\buf)(\loc,\gname,x) \\
+  &{}\ast \knowInv{\nspace'.\loc}{\Exists \ststs.\writer(\gname)(\ststs)} \\
+  \intr{\Prtcl{\loc : \protst \in \prot.\protspace | \prot.\protint(x)}}(\buf) \eqdef{}
+  & \perslize{\PrPRaw(\protspace,x,\protst,\buf)(\loc)}{\PrInvRaw(\protspace,\protint),\nspace.\loc}\\
+  \Prtcl{\loc : \protst | \prot(x)} \eqdef{}
+  & \Prtcl{\loc : \protst \in \prot.\protspace | \prot.\protint(x)}
+\end{align*}
+
+\subsection{Proofs}
+
+\subsubsection{\ruleref{Proto-Agree}}
+Similar to \ruleref{SWProto-Readers-Agree}.
+
+\subsubsection{\ruleref{Proto-Init}}
+
+Similar to \ruleref{SWProto-Init} and \ruleref{FracProto-Init}.
+
+\subsubsection{\ruleref{Proto-Read}}
+
+Similar to \ruleref{SWProto-Read} and \ruleref{FracProto-Read}.
+
+\subsubsection{\ruleref{Proto-Write}}
+
+Similar to \ruleref{FracProto-Write}.
+
+\subsubsection{\ruleref{Proto-CAS}}
+
+Similar to \ruleref{FracProto-CAS}.
+
+\subsubsection{\ruleref{Proto-Persistent}}
+
+Follows from \ruleref{Persister-Persistent}, since $\PrPRaw$ is persistent.
\ No newline at end of file
diff --git a/gps/protocols-sw.tex b/gps/protocols-sw.tex
new file mode 100644
index 0000000000000000000000000000000000000000..962617d470df74524643d1013b87265afc127f41
--- /dev/null
+++ b/gps/protocols-sw.tex
@@ -0,0 +1,490 @@
+\section{Single-Writer Protocols}
+
+\subsection{Definitions}
+
+\def\rawEncoder{\textsf{encode}}
+\def\PrInvRaw{\textlog{PrInvRaw}}
+We assume that we can construct for each first-order type $\FType$ 
+an injective function $\rawEncoder: \FType \ra \Nat$.
+
+\begin{align*}
+  \PrWRaw(\protspace,x,\protst,\buf)(\loc,n) \eqdef{}
+  & s \in \protspace(x)
+    \ast \Exists \gname. n = \rawEncoder((\gname,x))
+    \ast \PrW(\protst,\buf,\gname)\\
+  \PrRRaw(\protspace,x,\protst,\buf)(\loc,n) \eqdef{}
+  & s \in \protspace(x)
+    \ast \Exists \gname. n = \rawEncoder((\gname,x))
+    \ast \PrR(\protst,\buf,\gname)\\
+  \PrInvRaw(\protspace,\protint)(\loc,n) \eqdef{}
+  & \Exists \gname, x. n = \rawEncoder((\gname,x))
+    \ast \PrInv(\protspace,\protint)(\loc,\gname,x)\\
+   \intr{\Prtcl{\loc : \protst \in \protspace(x)| \protint(x)}_R}(\buf) \eqdef{}
+  & \perslize{\PrRRaw(\protspace,x,\protst,\buf)(\loc)}{\PrInvRaw(\protspace,\protint),\nspace.\loc} \\
+   \intr{\Prtcl{\loc : \protst \in \protspace(x)| \protint(x)}_W}(\buf) \eqdef{}
+  & \perslize{\PrWRaw(\protspace,x,\protst,\buf)(\loc)}{\PrInvRaw(\protspace,\protint),\nspace.\loc} \\
+  \Prtcl{\loc : \protst | \prot(x)}_R \eqdef{}
+  & \Prtcl{\loc : \protst \in \prot.\protspace(x)| \prot.\protint(x)}_R\\
+  \Prtcl{\loc : \protst | \prot(x)}_W \eqdef{}
+  & \Prtcl{\loc : \protst \in \prot.\protspace(x)| \prot.\protint(x)}_W
+\end{align*}
+
+
+\subsection{Proofs}
+
+\subsubsection{\ruleref{SWProto-Writer-Reader-Fork}}
+
+\begin{align*}
+  &\intr{\Prtcl{\loc : \protst | \tau(x)}_W}(\buf)\\
+  {}\equiv{}&
+    \perslize{\PrWRaw(\prot.\protspace,x,\protst,\buf)(\loc)}%
+             {\PrInvRaw(\prot.\protspace,\prot.\protint)} \\
+  {}\implies{}&
+    \perslize{\Lam n. \PrWRaw(\prot.\protspace,x,\protst,\buf)(\loc,n)
+            \ast \PrRRaw(\prot.\protspace,x,\protst,\buf)(\loc,n)
+              }%
+             {\PrInvRaw(\prot.\protspace,\prot.\protint)} \\
+  & \quad \by \ruleref{Persister-Imp} \text{ and } \ruleref{lem:rawprt-writer-fork}\\
+  {}\implies{}&
+    \perslize{\PrWRaw(\prot.\protspace,x,\protst,\buf)(\loc,n)}%
+             {\PrInvRaw(\prot.\protspace,\prot.\protint)} 
+    \ast 
+    \perslize{\PrRRaw(\prot.\protspace,x,\protst,\buf)(\loc,n)}%
+             {\PrInvRaw(\prot.\protspace,\prot.\protint)} \\
+  & \quad \by \ruleref{Persister-SplitJoin}\\
+  {}\equiv{}&
+    \intr{\Prtcl{\loc : \protst | \tau(x)}_W}(\buf)
+    \ast \intr{\Prtcl{\loc : \protst | \tau(x)}_R}(\buf)
+\end{align*}
+
+\subsubsection{\ruleref{SWProto-Readers-Agree}}
+
+\begin{align*}
+  &\intr{\Prtcl{\loc : \protst_1 | \tau(x_1)}_R}(\buf)
+    \ast 
+   \intr{\Prtcl{\loc : \protst_2 | \tau(x_2)}_R}(\buf)\\
+  {}\equiv{}
+  &\perslize{\PrRRaw(\prot.\protspace,x_1,\protst,\buf)(\loc)}%
+            {\PrInvRaw(\prot.\protspace,\prot.\protint)}
+    \ast
+   \perslize{\PrRRaw(\prot.\protspace,x_2,\protst,\buf)(\loc)}%
+            {\PrInvRaw(\prot.\protspace,\prot.\protint)} \\
+  {}\implies{}
+  &\perslize{\Lam n. \PrRRaw(\prot.\protspace(x_1),x_1,\protst,\buf)(\loc,n)
+             \ast \PrRRaw(\protspace(x_2),x_2,\protst,\buf)(\loc,n)}%
+            {\PrInvRaw(\prot.\protspace,\prot.\protint)}\\
+  &\quad \by \ruleref{Persister-SplitJoin} \\
+  {}\implies{}
+  & \Exists n. 
+    \PrRRaw(\prot.\protspace,x_1,\protst,\buf)(\loc,n)
+    \ast \PrRRaw(\prot.\protspace,x_2,\protst,\buf)(\loc,n)\\
+  &\quad \by \ruleref{Persister-Drop} \\
+  {}\equiv{}
+  & \Exists n, \gname_1, \gname_2.
+    n = \rawEncoder(\gname_1,x_1) = \rawEncoder(\gname_2,x_2)
+    \ast \protst_1 \in \prot.\protspace(x_1)
+    \ast \protst_2 \in \prot.\protspace(x_2) \\
+  &{}\ast \PrR(\protst_1,\buf,\gname_1)
+    \ast \PrR(\protst_2,\buf,\gname_2)\\
+  {}\implies{}
+  & \gname_1 = \gname_2 \ast x_1 = x_2 
+    \ast \protst_1 \in \prot.\protspace(x_1)
+    \ast \protst_2 \in \prot.\protspace(x_2)\\
+  &{} \ast \Exists \buf_1, \buf_2. 
+    \buf_1 \bsub \buf \ast \buf_2 \bsub \buf
+    \ast \reader(\gname_1)((\protst_1,\buf_1)::\any)
+    \ast \reader(\gname_2)((\protst_2,\buf_2)::\any) \\
+  {}\implies{}
+  & x_1 = x_2
+    \ast (\protst_1 \futst_\prot \protst_2
+          \lor \protst_2 \futst_\prot \protst_1) \\
+  &\quad \by \ruleref{lem:rawprt-reader-ordered} 
+            \text{ and } \ruleref{lem:rawprt-state-ordered}
+\end{align*}
+
+
+\subsubsection{\ruleref{SWProto-Init}}
+
+\begin{proofoutline*}
+  \VARS{\buf,\proc} \\
+  \CTX{\bseen{\proc}{\buf}, \perInv(\gname_p, \nspace_2)}\\
+  \RES{\LBeinitPrewBuf}\\
+  \CTX{\protst \in \prot.\protspace(x)}\\
+  \cdline{\ewrite{\wtna}{\loc}{\val}}\\
+  \RES{
+    \Exists \buf' \futb \buf.
+    \bseen{\proc}{\buf'}
+    \ast \writer(\gname)((\protst,\buf')::\any)
+    \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  } \BY \ruleref{RawProto-Init}\\
+  \RES{
+    \Exists \buf' \futb \buf.
+    \bseen{\proc}{\buf'}
+    \ast \Exists n. n = \rawEncoder(\gname, x)
+    \ast \writer(\gname)((\protst,\buf')::\any)
+    \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  }\\
+  \RES{
+    \Exists n. 
+    \PrWRaw(\prot.\protspace,x,\protst,\buf')(\loc,n)
+    \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  }\\
+  \RES{
+    \perslize{\PrWRaw(\prot.\protspace,x,\protst,\buf')(\loc)}
+             {\PrInvRaw(\prot.\protspace,\prot.\protint)}
+  } \BY \ruleref{Persister-InvAlloc}\\
+  \RES{
+    \Exists \buf' \futb \buf.
+    \bseen{\proc}{\buf'}
+    \ast \intr{\Prtcl{\loc:\protst|\prot(x)}_W}(\buf')
+  }\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{SWProto-Writer-Reader-Agree}} 
+
+Similar to \ruleref{SWProto-Readers-Agree}, but note that from 
+$\writer(\gname)((\protst_1,\any)::\any) \ast \reader(\gname)((\protst_2,\any)::\any)$
+we have $\protst_1 \futst_\prot \protst_2$, by \ruleref{lem:rawprt-writer-latest} and
+\ruleref{lem:rawprt-state-ordered}.
+
+\subsubsection{\ruleref{SWProto-Read}}
+
+\begin{proofoutline*}
+  \CTX{\LBereadHypwBuf}\\
+  \VARS{\buf,\proc} \\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{
+    \intr{P}(\buf) 
+    \ast \intr{\Prtcl{\loc : \protst | \prot(x)}_R}(\buf)
+  } \\
+  \RES{
+    \intr{P}(\buf)
+    \ast \perslize{\PrRRaw(\prot.\protspace,x,\protst,\buf)(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+  }
+  \IND
+    \VARS{n}\\
+    \RES{\intr{P}(\buf)
+        \ast \PrRRaw(\prot.\protspace,x,\protst,\buf)(\loc,n)
+        \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    }[-\nspace.\loc] \BY \ruleref{Persister-Hoare} \\
+    \VARS{\gname,\gname',x'}\\
+    \CTX{\protst \in \prot.\protspace(x), 
+        n = \rawEncoder((\gname,x)),
+        \later n = \rawEncoder((\gname',x'))}\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrR(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname',x')
+    }[-\nspace.\loc]\\
+    \PFHAVE{\gname = \gname', x = x'} \BY agreement on $n$\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrR(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    }[-\nspace.\loc]\\
+    \cdline{\eread{\rtat}{\loc}}\\
+    \RES{
+      \Ret\val.
+        \Exists \buf' \futb \buf, \protst' \futst_\prot \protst.
+        \bseen{\proc}{\buf'}
+        \ast \intr{Q}(\buf')
+        \ast \PrR(\protst',\buf',\gname)
+        \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    }[-\nspace.\loc]
+      \BY \ruleref{RawProto-Read}\\
+    \RES{
+      \Ret\val.
+        \Exists \buf' \futb \buf, \protst' \futst_\prot \protst.
+        \bseen{\proc}{\buf'}
+        \ast \intr{Q}(\buf')
+        \ast \PrRRaw(\prot.\protspace,x,\protst', \buf')(\loc,n)
+        \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    }[-\nspace.\loc]
+  \UNIND
+  \RES{
+    \Ret\val.
+      \Exists \buf' \futb \buf, \protst' \futst_\prot \protst.
+      \bseen{\proc}{\buf'}
+      \ast \intr{Q}(\buf')
+      \ast \perslize{\PrRRaw(\prot.\protspace,x,\protst', \buf')(\loc)}
+                    {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+  }\\
+  \RES{\Ret\val. 
+    \Exists \buf' \futb \buf.
+    \Exists \protst' \futst_\prot \protst. 
+    \bseen{\proc}{\buf'}
+    \ast \intr{\Prtcl{\loc : \protst' | \prot(x)}_R}(\buf') 
+    \ast \intr{Q}(\buf')
+  } \\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{SWProto-Write}}
+\begin{proofoutline*}
+  \CTX{
+    \All \buf. 
+    \intr{\prot.\protint(x)(\stst, \any)}(\buf)
+    \ast \intr{P}(\buf)
+    \vs[-\nspace]
+    \stst' \futst_\prot \stst
+    \ast \later\intr{\prot.\protint(x)(\stst', \val)}(\buf) 
+    \ast \intr{Q}(\buf)
+  }\\
+  \VARS{\buf,\proc} \\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{
+    \intr{P}(\buf) 
+    \ast \intr{\Prtcl{\loc : \protst | \prot(x)}_W}(\buf)
+  } \\
+  \RES{
+    \intr{P}(\buf)
+    \ast \perslize{\PrWRaw(\prot.\protspace,x,\protst,\buf)(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+  }
+  \IND
+    \VARS{n}\\
+    \RES{\intr{P}(\buf)
+        \ast \PrWRaw(\prot.\protspace,x,\protst,\buf)(\loc,n)
+        \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    }[-\nspace.\loc] \BY \ruleref{Persister-Hoare} \\
+    \VARS{\gname,\gname',x'}\\
+    \CTX{\protst \in \protspace(x), 
+        n = \rawEncoder((\gname,x)),
+        \later n = \rawEncoder((\gname',x'))}\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrW(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname',x')
+    }[-\nspace.\loc]\\
+    \PFHAVE{\gname = \gname', x = x'} \BY agreement on $n$\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrW(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    }[-\nspace.\loc]\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrW(\protst,\buf,\gname)
+      \ast \PrR(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    }[-\nspace.\loc]\\
+    \cdline{\ewrite{\wtat}{\loc}{\val},\proc}\\
+    \RES{
+      \Exists \buf' \futb \buf.
+      \bseen{\proc}{\buf'}
+      \ast \intr{Q}(\buf')
+      \ast \PrW(\protst', \buf',\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    }[-\nspace.\loc]
+      \BY \ruleref{RawProto-Write}\\
+    \prule\\
+    \GOAL{
+      \All \buf' \futb \buf, \buf_1 \bsub \buf. 
+      \intr{\prot.\protint(x)(\stst, \any)}(\buf_1)
+      \ast \intr{P}(\buf')
+      \vs[-\nspace]
+      \stst' \futst_\prot \stst
+      \ast\later\intr{\prot.\protint(x)(\stst', \val)}(\buf') 
+      \ast \intr{Q}(\buf)
+    } 
+    \IND
+      \RES{\intr{\prot.\protint(x)(\stst, \any)}(\buf_1)
+            \ast \intr{P}(\buf')}\\
+      \RES{\intr{\prot.\protint(x)(\stst, \any)}(\buf')
+            \ast \intr{P}(\buf')} since $\buf_1 \bsub \buf \bsub \buf'$\\
+      \RES{\stst' \futst_\prot \stst
+            \ast\later\intr{\prot.\protint(x)(\stst', \val)}(\buf') 
+            \ast \intr{Q}(\buf')} \BY assm.
+    \UNIND
+    \prule\\
+    \RES{
+      \Exists \buf' \futb \buf.
+      \bseen{\proc}{\buf'}
+      \ast \intr{Q}(\buf')
+      \ast \PrWRaw(\prot.\protspace,x,\protst', \buf')(\loc,n)
+      \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    }[-\nspace.\loc]
+  \UNIND
+  \RES{
+    \Exists \buf' \futb \buf.
+    \bseen{\proc}{\buf'}
+    \ast \intr{Q}(\buf')
+    \ast \perslize{\PrWRaw(\prot.\protspace,x,\protst', \buf')(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+  }\\
+  \RES{
+    \Exists \buf' \futb \buf.
+    \bseen{\proc}{\buf'}
+    \ast \intr{\Prtcl{\loc : \protst' | \prot(x)}_W}(\buf') 
+    \ast \intr{Q}(\buf')
+  } \\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{SWProto-CAS}}
+\begin{proofoutline*}
+  \CTX{\All \buf.
+    \All \protst' \futst_\prot \protst.
+    \intr{\prot.\protint(x)(\protst', \val_o)}(\buf) 
+    \ast \intr{P}(\buf)
+    \vs[\mask_1][\mask_2]
+    \Exists \protst'' \futst_\prot \protst', \protst_w. 
+      \intr{\Prtcl{\loc : \protst_w | \prot(x)}_W}(\any))
+      \ast \intr{T}(\buf))
+  }\\
+  \CTX{\All \buf.
+    \All \protst',\protst'' \futst_\prot \protst' \futst_\prot \protst.
+    \intr{\Prtcl{\loc : \protst'' | \prot(x)}_W}(\buf)
+    \ast \intr{T\subst{\protst_w}{\protst'}}(\buf)
+    \vs[\mask_2][\mask_1]
+    \later\intr{\prot.\protint(x)(\protst'', \val_n)}(\buf) 
+    \ast \intr{Q}(\buf)
+  }\\
+  \CTX{\All \buf.
+    \All \valB \neq \val_o. 
+    \intr{\prot.\td(x)(\protst, \valB)}(\buf)
+    \ast \intr{P}(\buf)
+    \vs
+    \intr{R}(\buf)}\\
+  \VARS{\buf} \\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{\intr{P}(\buf)
+    \ast \intr{\Prtcl{\loc : \protst | \prot(x)}_R}(\buf)
+  } \\
+  \RES{
+    \intr{P}(\buf)
+    \ast \perslize{\PrRRaw(\prot.\protspace,x,\protst,\buf)(\loc)}
+                  {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}
+  }
+  \IND
+    \VARS{n}\\
+    \RES{\intr{P}(\buf)
+        \ast \PrRRaw(\prot.\protspace,x,\protst,\buf)(\loc,n)
+        \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+    }[-\nspace.\loc] \BY \ruleref{Persister-Hoare} \\
+    \VARS{\gname,\gname',x'}\\
+    \CTX{\protst \in \prot.\protspace(x), 
+        n = \rawEncoder((\gname,x)),
+        \later n = \rawEncoder((\gname',x')),
+        \ownGhost{\gname_p}{\authfrag \loc \pointsto (n,\nspace_1)}}\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrR(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname',x')
+    }[-\nspace.\loc]\\
+    \PFHAVE{\gname = \gname', x = x'} \BY agreement on $n$\\
+    \RES{
+      \intr{P}(\buf)
+      \ast \PrR(\protst,\buf,\gname)
+      \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+    }[-\nspace.\loc]\\
+    \cdline{\ecas{\loc}{\val_o}{\val_n}}\\
+    \RES{
+      \Ret\val.
+      \begin{array}[t]{l}
+        \Exists \buf' \futb \buf, \protst'' \futst_\prot \protst.
+        \bseen{\proc}{\buf'}
+        \ast \PrR(\protst'',\buf',\gname)
+        \\ 
+        \ast (\val = 1 \ast \intr{Q}(\buf'))
+        \ast (\val = 0 \ast \intr{R}(\buf'))
+        \ast \later\PrInv(\prot.\protspace,\prot.\protint)(\loc,\gname,x)
+      \end{array}
+    }[-\nspace.\loc] \BY \ruleref{RawProto-CAS}\\
+    \prule\\
+    \GOAL{
+      \All \buf.
+      \All \protst' \futst_\prot \protst.
+      \intr{\prot.\protint(x)(\protst', \val_o)}(\buf) 
+      \ast \intr{P}(\buf)
+      \vs[\mask_1][\mask_2]
+      \Exists \protst'' \futst_\prot \protst', \protst_w. 
+        \writer(\gname)((\protst_w,\any)::\any)
+        \ast \intr{T}(\buf))
+    } \IND
+        \RES{\intr{\prot.\protint(x)(\protst', \val_o)}(\buf) 
+            \ast \intr{P}(\buf)} \\
+        $\vs[\mask_1][\mask_2]$
+        \RES{\Exists \protst'' \futst_\prot \protst', \protst_w. 
+                    \intr{\Prtcl{\loc : \protst_w | \prot(x)}_W}(\any))
+                    \ast \intr{T}(\buf)} \BY assm.\\
+        \CTX{\protst'' \futst_\prot \protst',\protst_w}\\
+        \RES{\Exists \buf', n'.
+            \PrWRaw(\prot.\protspace,x,\protst_w,\buf')(\loc,n')
+            \ast \ownGhost{\gname_p}{\authfrag \loc \pointsto (n',\nspace_1)}
+            \ast \intr{T}(\buf)
+        } \\
+        \VARS{\buf',n',\gname''}\\
+        \RES{
+          \ownGhost{\gname_p}{\authfrag \loc \pointsto (n',\nspace_1)}
+          \ast  n' = \rawEncoder(\gname'',x)
+          \ast \PrW(\protst_w,\buf',\gname'')
+          \ast \intr{T}(\buf)
+        }\\
+        \CTX{n = n', \gname = \gname''} \\
+        \RES{\PrW(\protst_w,\buf',\gname) 
+          \ast \intr{T}(\buf)}\\
+        \RES{\writer(\gname)((\protst_w,\any)::\any)
+          \ast \intr{T}(\buf)}
+      \UNIND
+    \prule\\
+    \GOAL{
+       \All \buf',\buf \futb \buf'.
+       \All \protst' \futst_\prot \protst.
+       \writer(\gname)((\protst',\buf')::\any)
+       \ast \intr{T\subst{\protst_w}{\protst'}}(\buf)
+       \vs[\mask_2][\mask_1]
+       \Exists \protst'' \futst_\prot \protst'. 
+       \later\intr{\prot.\protint(x)(\protst'', \val_n)}(\buf) 
+       \ast \intr{Q}(\buf)
+    } \IND
+        \RES{\writer(\gname)((\protst',\buf')::\any)
+              \ast \intr{T\subst{\protst_w}{\protst'}}(\buf)}\\
+        \RES{\PrWRaw(\prot.\protspace,x,\protst',\buf)(\loc,n)
+              \ast \intr{T\subst{\protst_w}{\protst'}}(\buf)}\\\
+        \RES{\intr{\Prtcl{\loc:\protst'|\prot(x)}_W}(\buf)
+              \ast \intr{T\subst{\protst_w}{\protst'}}(\buf)}\\
+        $\vs[\mask_2][\mask_1]$
+        \RES{
+          \Exists \protst'' \futst_\prot \protst'. 
+          \later\intr{\prot.\protint(x)(\protst'', \val_n)}(\buf) 
+          \ast \intr{Q}(\buf)
+        } \BY 1st assm.
+      \UNIND
+    \prule\\
+    \RES{
+      \Ret\val.
+      \begin{array}[t]{l}
+        \Exists \buf' \futb \buf, \protst'' \futst_\prot \protst.
+        \bseen{\proc}{\buf'}
+        \ast \PrRRaw(\prot.\protspace,x,\protst'',\buf')(\loc,n)
+        \\ 
+        \ast (\val = 1 \ast \intr{Q}(\buf'))
+        \ast (\val = 0 \ast \intr{R}(\buf'))
+        \ast \later\PrInvRaw(\prot.\protspace,\prot.\protint)(\loc,n)
+      \end{array}
+    }[-\nspace.\loc]
+  \UNIND
+  \RES{
+    \begin{aligned}
+      \Ret\val.
+      \Exists \buf' \futb \buf. \Exists \protst'' \futst_\prot \protst.
+      &\bseen{\proc}{\buf'}
+      \ast \perslize{\PrRRaw(\prot.\protspace,x,\protst'', \buf')(\loc)}
+                    {\PrInvRaw(\prot.\protspace,\prot.\protint),\nspace.\loc}\\
+      &{}\ast (\val = 1 \ast \intr{Q}(\buf')) \lor
+              (\val = 0 \ast \intr{R}(\buf'))
+    \end{aligned}} \\
+  \RES{\Ret\val.
+    \Exists \buf' \futb \buf. \Exists \protst'' \futst_\prot \protst.
+    \bseen{\proc}{\buf'}
+    \ast \intr{\Prtcl{\loc : \protst'' | \prot(x)}_R}(\buf')
+    \ast (\val = 1 \ast \intr{Q}(\buf')) \lor
+    (\val = 0 \ast \intr{R}(\buf'))} \\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{SWProto-Read-Persistent}}
+
+Follows from \ruleref{Persister-Persistent}, since $\PrRRaw$ is persistent.
\ No newline at end of file
diff --git a/gps/protocols.tex b/gps/protocols.tex
index 4f9be9c25aa69108ca8401e1dae7c8b41e76cd27..755611ba1867bb838ac7a988802a656cc8ff6e9c 100644
--- a/gps/protocols.tex
+++ b/gps/protocols.tex
@@ -1,216 +1,294 @@
 
 \section{GPS Proof Rules}
 %
-\subsection{Protocol Names}
+% \subsection{Protocol Names}
+% %
+% \begin{mathpar}
+%   \iinferH{Proto-Create}{
+%     n \in \Nat
+%     \\ \futst \subseteq \protspace \times \protspace
+%     \\ \protint \in \protspace \times \Value \to Prop
+%   }{
+%     \top \vs \Exists \prot. \protocol(\prot, n, \protspace, \futst, \protint)
+%   }
+%   \and
+%   \iinferH{Proto-Persists}{}{
+%     \protocol(\prot, n, \protspace, \futst, \protint)
+%     \vs
+%     \always\protocol(\prot, n, \protspace, \futst, \protint)
+%   }
+%   \and
+%   \iinferH{Proto-Unique}{}{
+%     \protocol(\prot, n_1, \protspace_1, \futst_1, \protint_1)
+%     \ast 
+%     \protocol(\prot, n_2, \protspace_2, \futst_2, \protint_2)
+%     \implies
+%     n_1 = n_2
+%     \land \protspace_1 = \protspace_2
+%     \land {}\futst_1{} = {}\futst_2{}
+%     \land \later (\protint_1 = \protint_2)
+%   }
+% \end{mathpar}
+% %
+% In the following sections, we assume an ambient
+% $\always\protocol(\prot, n, \protspace, \prot)$ assertion for all triples.
+% Note the overloading of the identifier $\prot$, used both for the name and the
+% interpretation predicate.
+% ~\\
+% \janno{Fix this}
 %
+% 
+\subsection{Single-Writer Protocols}
+
+\def\SWReadPre{P \ast \Prtcl{\loc : \protst | \prot(x)}_R}
+\def\SWReadPost{
+  \Ret\val.
+  \Exists \protst' \futst_\prot \protst. 
+  \Prtcl{\loc : \protst' | \prot(x)}_R \ast Q
+}
+\def\SWWritePrem{
+  \prot.\protint(x)(\protst, \any)
+  \ast P
+  \vs
+  \protst' \futst_\prot \protst
+  \ast \later\prot.\protint(x)(\protst', \val) \ast Q
+}
+\def\SWWritePre{P \ast \Prtcl{\loc : \protst | \prot(x)}_W}
+\def\SWWritePost{\Prtcl{\loc : \protst' | \prot(x)}_W \ast Q}
+\def\SWCASPremA{
+  \All \protst' \futst_\prot \protst.
+  \prot.\protint(x)(\protst', \val_o) \ast P
+  \vs[\mask_1][\mask_2]
+  \Exists \protst'' \futst_\prot \protst', \protst_w. 
+    \bobj(\Prtcl{\loc : \protst_w | \prot(x)}_W)
+    \ast T)
+}
+\def\SWCASPremB{
+  \All \protst',\protst'' \futst_\prot \protst' \futst_\prot \protst.
+  \Prtcl{\loc : \protst'' | \prot(x)}_W
+  \ast T\subst{\protst_w}{\protst'}
+  \vs[\mask_2][\mask_1]
+  \later\prot.\protint(x)(\protst'', \val_n) \ast Q
+}
+\def\SWCASPremC{
+  \All \valB \neq \val_o. 
+  \prot.\td(x)(\protst, \valB) \ast P
+  \vs
+  R
+}
+\def\SWCASPre{P \ast \Prtcl{\loc : \protst | \prot(x)}_R}
+\def\SWCASPost{
+  \Ret\val.
+  \Exists \protst'' \futst_\prot \protst.
+  \Prtcl{\loc : \protst'' | \prot(x)}_R
+  \ast (\val = 1 \ast Q) \lor
+  (\val = 0 \ast R)
+}
+
 \begin{mathpar}
-  \iinferH{Proto-Create}{
-    n \in \Nat
-    \\ \futst \subseteq \protspace \times \protspace
-    \\ \protint \in \protspace \times \Value \to Prop
-  }{
-    \top \vs \Exists \prot. \protocol(\prot, n, \protspace, \futst, \protint)
-  }
-  \and
-  \iinferH{Proto-Persists}{}{
-    \protocol(\prot, n, \protspace, \futst, \protint)
-    \vs
-    \always\protocol(\prot, n, \protspace, \futst, \protint)
+  \iinferH{SWProto-Writer-Reader-Fork}{}{
+    \Prtcl{\loc : \protst | \prot(x)}_W
+    \Ra
+    \Prtcl{\loc : \protst | \prot(x)}_W
+    \ast \Prtcl{\loc : \protst | \prot(x)}_R
   }
   \and
-  \iinferH{Proto-Unique}{}{
-    \protocol(\prot, n_1, \protspace_1, \futst_1, \protint_1)
-    \ast 
-    \protocol(\prot, n_2, \protspace_2, \futst_2, \protint_2)
+  \iinferH{SWProto-Readers-Agree}{}{
+    \Prtcl{\loc : \protst_1 | \prot(x_1)}_R
+    \ast \Prtcl{\loc : \protst_2 | \prot(x_2)}_R
     \implies
-    n_1 = n_2
-    \land \protspace_1 = \protspace_2
-    \land {}\futst_1{} = {}\futst_2{}
-    \land \later (\protint_1 = \protint_2)
-  }
-\end{mathpar}
-%
-In the following sections, we assume an ambient
-$\always\protocol(\tau, n, \protspace, \prot)$ assertion for all triples.
-Note the overloading of the identifier $\prot$, used both for the name and the
-interpretation predicate.
-~\\
-\janno{Fix this}
-%
-% 
-\subsection{Single-Writer Protocols}
-\begin{mathpar}
-  \iinferH{SWProto-Writer-Reader}{
-    \janno{write permission assertion}
-  }{
-    \Prtcl{\loc : \protst | \tau}_W
-    \iff
-    \Prtcl{\loc : \protst | \tau}_W
-    \ast \Prtcl{\loc : \protst | \tau}_R
+    x_1 = x_2
+    \ast (\protst_1 \futst \protst_2
+          \lor \protst_2 \futst \protst_1)
   }
   \and
-  \iinferH{SWProto-Agree}{}{
-    \Prtcl{\loc : \protst_1 | \tau_1}_R
-    \ast \Prtcl{\loc : \protst_2 | \tau_2}_R
+  \iinferH{SWProto-Writer-Reader-Agree}{}{
+    \Prtcl{\loc : \protst_1 | \prot(x_1)}_W
+    \ast \Prtcl{\loc : \protst_2 | \prot(x_2)}_R
     \implies
-    \tau_1 = \tau_2
-    \ast (
-    \protst_1 \futst \protst_2
-    \lor \protst_2 \futst \protst_1
-    )
+    x_1 = x_2
+    \ast \protst_1 \futst \protst_2
   }
-  \\
-  \iinferH{SWProto-Init}{
-    \protocol(\tau, \any, \protspace, \prot)
-    \\
-    P
-    \ast \Prtcl{\loc : \protst | \prot}_W
-    \vs
-    \later\prot(\protst, \val)
-    \ast Q
-    \\ \janno{TODO write permission}
-  }{
+  \and
+  \iinferH{SWProto-Init}{}{
     \hoare%
-    {\lraw(\loc, \any) \ast P}%
+    {\LBeinitPre}%
     {\ewrite{\wtna}{\loc}{\val}}%
-    {\Ret\val. \Prtcl{\loc : \protst | \prot}_R \ast Q}
-  }%
-  \\
-  \iinferH{SWProto-Read}{
-    \LBereadHyp
-  }{
+    {\Prtcl{\loc : \protst | \prot(x)}_W}
+  }
+  \and
+  \iinferH{SWProto-Read}{\LBereadHyp}{
     \hoare%
-    {P \ast \Prtcl{\loc : \protst | \prot}_R}%
+    {\SWReadPre}%
     {\eread{\rtat}{\loc}}%
-    {\Exists \protst' \futst_\prot \protst. \Prtcl{\loc : \protst' | \prot}_R \ast Q}
+    {\SWReadPost}
   }%
   \\
-  \iinferH{SWProto-Write}{
-    \prot(\protst, \any)
-    \ast P
-    \ast \Prtcl{\loc : \protst'' | \prot}_W
-    \vs
-    \protst'' \futst_\prot \protst
-    \ast \later\prot(\protst'', \val) \ast Q
-  }{
+  \iinferH{SWProto-Write}{\SWWritePrem}{
     \hoare%
-    {P \ast \Prtcl{\loc : \protst | \prot}_W}%
+    {\SWWritePre}%
     {\ewrite{\wtat}{\loc}{\val}}%
-    {\Ret\val. \Prtcl{\loc : \protst'' | \prot}_R \ast Q}
+    {\SWWritePost}
   }%
   \\
-  \iinferH{SWProto-RCAS}{
-    \All \protst' \futst_\prot \protst.
-    \later\prot(\protst', \val_o) \ast P
-    \vs[\mask_1][\mask_2]
-    \later(\Exists \protst_w. \bobj(\Prtcl{\loc : \protst_w | \prot}_W)
-    \ast T)
-    \\
-    \All \protst' \futst_\prot \protst.
-    \ast \Prtcl{\loc : \protst' | \prot}_W
-    \ast T\subst{\protst_w}{\protst'}
-    \vs[\mask_2][\mask_1]
-    \Exists \protst'' \futst_\prot \protst'. 
-    \later\prot(\protst'', \val_n) \ast Q
-    \\\\
-    \All \valB \neq \val_o. 
-    \td(\protst, \valB) \ast P
-    \vs
-    R
-  }{
+  \iinferH{SWProto-CAS}{\SWCASPremA \\ \SWCASPremB \\\\ \SWCASPremC}{
     \hoare%
-    {\Prtcl{\loc : \protst | \prot}_R \ast P}%
+    {\SWCASPre}%
     {\ecas{\loc}{\val_o}{\val_n}}%
-    {\Ret\val.
-      \Exists \protst'' \futst_\prot \protst.
-      \Prtcl{\loc : \protst'' | \prot}_R
-      \ast (\val = 1 \ast Q) \lor
-      (\val = 0 \ast R)}
-  }%
+    {\SWCASPost}
+  }\\
+  \iinferH{SWProto-Read-Persistent}{}{
+    \Prtcl{\loc:\protst|\prot(x)}_R 
+    \implies \always \Prtcl{\loc:\protst|\prot(x)}_R
+  }
 \end{mathpar}
+
+% \begin{mathpar}
+%   \iinferH{SWProto-Writer-Reader}{
+%     \janno{write permission assertion}
+%   }{
+%     \Prtcl{\loc : \protst | \prot}_W
+%     \iff
+%     \Prtcl{\loc : \protst | \prot}_W
+%     \ast \Prtcl{\loc : \protst | \prot}_R
+%   }
+%   \and
+%   \iinferH{SWProto-Agree}{}{
+%     \Prtcl{\loc : \protst_1 | \prot_1}_R
+%     \ast \Prtcl{\loc : \protst_2 | \prot_2}_R
+%     \implies
+%     \prot_1 = \prot_2
+%     \ast (
+%     \protst_1 \futst \protst_2
+%     \lor \protst_2 \futst \protst_1
+%     )
+%   }
+%   \\
+%   \iinferH{SWProto-Init}{
+%     \protocol(\prot, \any, \protspace, \prot)
+%     \\
+%     P
+%     \ast \Prtcl{\loc : \protst | \prot}_W
+%     \vs
+%     \later\prot(\protst, \val)
+%     \ast Q
+%     \\ \janno{TODO write permission}
+%   }{
+%     \hoare%
+%     {\lraw(\loc, \any) \ast P}%
+%     {\ewrite{\wtna}{\loc}{\val}}%
+%     {\Ret\val. \Prtcl{\loc : \protst | \prot}_R \ast Q}
+%   }%
+%   \\
+%   \iinferH{SWProto-Read}{
+%     \LBereadHyp
+%   }{
+%     \hoare%
+%     {P \ast \Prtcl{\loc : \protst | \prot}_R}%
+%     {\eread{\rtat}{\loc}}%
+%     {\Exists \protst' \futst_\prot \protst. \Prtcl{\loc : \protst' | \prot}_R \ast Q}
+%   }%
+%   \\
+%   \iinferH{SWProto-Write}{
+%     \prot(\protst, \any)
+%     \ast P
+%     \ast \Prtcl{\loc : \protst'' | \prot}_W
+%     \vs
+%     \protst'' \futst_\prot \protst
+%     \ast \later\prot(\protst'', \val) \ast Q
+%   }{
+%     \hoare%
+%     {P \ast \Prtcl{\loc : \protst | \prot}_W}%
+%     {\ewrite{\wtat}{\loc}{\val}}%
+%     {\Ret\val. \Prtcl{\loc : \protst'' | \prot}_R \ast Q}
+%   }%
+%   \\
+%   \iinferH{SWProto-RCAS}{
+%     \All \protst' \futst_\prot \protst.
+%     \later\prot(\protst', \val_o) \ast P
+%     \vs[\mask_1][\mask_2]
+%     \later(\Exists \protst_w. \bobj(\Prtcl{\loc : \protst_w | \prot}_W)
+%     \ast T)
+%     \\
+%     \All \protst' \futst_\prot \protst.
+%     \ast \Prtcl{\loc : \protst' | \prot}_W
+%     \ast T\subst{\protst_w}{\protst'}
+%     \vs[\mask_2][\mask_1]
+%     \Exists \protst'' \futst_\prot \protst'. 
+%     \later\prot(\protst'', \val_n) \ast Q
+%     \\\\
+%     \All \valB \neq \val_o. 
+%     \td(\protst, \valB) \ast P
+%     \vs
+%     R
+%   }{
+%     \hoare%
+%     {\Prtcl{\loc : \protst | \prot}_R \ast P}%
+%     {\ecas{\loc}{\val_o}{\val_n}}%
+%     {\Ret\val.
+%       \Exists \protst'' \futst_\prot \protst.
+%       \Prtcl{\loc : \protst'' | \prot}_R
+%       \ast (\val = 1 \ast Q) \lor
+%       (\val = 0 \ast R)}
+%   }%
+% \end{mathpar}
 % 
 % 
 \subsection{Fractional Protocols}
 % 
 \begin{mathpar}
-  \iinferH{FracProto-Combine}{}{
-    \Prtcl{\loc : \protst | \tau}^{p}
-    \ast \Prtcl{\loc : \protst | \tau}^{q}
-    \vs
-    \Prtcl{\loc : \protst | \tau}^{p+q}
-    \ast p + q \le 1
-  }
-  \and
-  \iinferH{FracProto-Split}{}{
-    \Prtcl{\loc : \protst | \tau}^{p+q}
-    \vs
-    \Prtcl{\loc : \protst | \tau}^{p}
-    \ast \Prtcl{\loc : \protst | \tau}^{q}
+  \iinferH{FracProto-SplitJoin}{}{
+    \Prtcl{\loc : \protst | \prot(x)}^{p}
+    \ast \Prtcl{\loc : \protst | \prot(x)}^{q}
+    \iff
+    \Prtcl{\loc : \protst | \prot(x)}^{p+q}
   }
   \and
   \iinferH{FracProto-Agree}{}{
-    \Prtcl{\loc : \protst_1 | \tau_1}^{p}
-    \ast \Prtcl{\loc : \protst_2 | \tau_2}^{q}
+    \Prtcl{\loc : \protst_1 | \prot(x_1)}^{p}
+    \ast \Prtcl{\loc : \protst_2 | \prot(x_2)}^{q}
     \implies
-    \tau_1 = \tau_2
-    \ast (
-    \protst_1 \futst \protst_2
-    \lor \protst_2 \futst \protst_1
-    )
+    x_1 = x_2
+    \ast (\protst_1 \futst_\prot \protst_2
+      \lor \protst_2 \futst_\prot \protst_1)
   }
   \\
-  \iinferH{FracProto-Init}{
-    \protocol(\tau, \any, \protspace, \protint)
-    \\
-    P
-    \vs
-    \later\prot(\protst, \val)
-    \ast Q
-  }{
+  \iinferH{FracProto-Raw}{}{
+    \hoare{\Prtcl{\loc: \any | \any}^{\ffrac}}
+          {\ewrite{\wtat}{\loc}{\val}}
+          {\lraw(\loc,\Some \val)}
+  }
+  \\
+  \iinferH{FracProto-Init}{}{
     \hoare%
-    {\lraw(\loc, \any) \ast P}%
-    {\ewrite{\wtat}{\loc}{\val}}%
-    {\Ret\val. \Prtcl{\loc : \protst | \prot}_1 \ast Q}
+    {\LBeinitPre}%
+    {\ewrite{\wtna}{\loc}{\val}}%
+    {\Prtcl{\loc : \protst | \prot(x)}^{\ffrac}}
   }%
   \\
-  \iinferH{FracProto-Read}{
-    \LBereadHyp
-  }{
+  \iinferH{FracProto-Read}{\LBereadHyp}{
     \hoare%
-    {\Prtcl{\loc : \protst | \tau}^q}%
+    {P \ast \Prtcl{\loc : \protst | \prot(x)}^q}%
     {\eread{\rtat}{\loc}}%
-    {\Ret \val. \Prtcl{\loc : \protst | \tau}^q}%
+    {\Ret \val. \Prtcl{\loc : \protst | \prot(x)}^q \ast Q}%
   }
   \\
-  \iinferH{FracProto-Write}{
-    \LBewriteHypA
-    \\ \LBewriteHypB
-  }{
-    \hoare{
-      \Prtcl{\loc : \protst | \tau}^q \ast P
-    }{
-      \ewrite{\wtat}{\loc}{\val}
-    }{
-      \Prtcl{\loc : \protst'' | \tau}^q \ast Q
-    }
+  \iinferH{FracProto-Write}{\LBewriteHypA \\ \LBewriteHypB}{
+    \hoare{P \ast \Prtcl{\loc : \protst | \prot(x)}^q}
+          {\ewrite{\wtat}{\loc}{\val}}
+          {\Prtcl{\loc : \protst'' | \prot(x)}^q \ast Q}
   }
   \\
-  \iinferH{FracProto-CAS}{
-    \LBecasHypA \\ \LBecasHypB
-  }{
-    \hoare{
-      \Prtcl{\loc : \protst | \tau}^q \ast P
-    }{
-      \ecas{\loc}{v_o}{v_n}, \proc
-    }{
-      \Ret \val.
-      \Exists \protst'' \futst_\prot \protst.
-      \Prtcl{\loc : \protst'' | \tau}^q
-      \ast \left(
-        (\val = 1 \ast Q)
-        \ast (\val = 0 \ast R)
-      \right)
-    }
+  \iinferH{FracProto-CAS}{\LBecasHypA \\ \LBecasHypB}{
+    \hoare{\Prtcl{\loc : \protst | \prot(x)}^q \ast P}
+          {\ecas{\loc}{v_o}{v_n}, \proc}
+          {\Ret \val.
+            \Exists \protst'' \futst_\prot \protst.
+            \Prtcl{\loc : \protst'' | \prot(x)}^q
+            \ast \left(
+                (\val = 1 \ast Q)
+                \ast (\val = 0 \ast R)
+              \right)}
   }
 \end{mathpar}
 % 
@@ -218,23 +296,40 @@ interpretation predicate.
 \subsection{Plain Protocols}
 % 
 \begin{mathpar}
-  \iinferH{Proto-Init}{
-    \protocol(\tau, \any, \protspace, \protint)
-    \\
-    P
-    \vs
-    \later\prot(\protst, \val)
-    \ast Q
-  }{
-    \hoare%
-    {\lraw(\loc, \any) \ast P}%
-    {\ewrite{\wtat}{\loc}{\val}}%
-    {\Ret\val. \Prtcl{\loc : \protst | \prot} \ast Q}
+  \iinferH{Proto-Agree}{}{
+      \Prtcl{\loc : \protst_1 | \prot(x_1)}
+      \ast \Prtcl{\loc : \protst_2 | \prot(x_2)}
+      \implies
+      x_1 = x_2
+      \ast (\protst_1 \futst_\prot \protst_2
+        \lor \protst_2 \futst_\prot \protst_1)
+    }
+  \\
+  \iinferH{Proto-Init}{}{
+    \hoare{\LBeinitPre}%
+          {\ewrite{\wtna}{\loc}{\val}}%
+          {\Prtcl{\loc : \protst | \prot(x)}}
   }%
   \\
-  \iinferH{Proto-Read}{\LBereadHyp}{\hoare{\LBereadPre}{\eread{\rtat}{\loc}}{\Ret \val. \LBereadPost } } \\
-  \iinferH{Proto-Write}{\LBewriteHypA \\ \LBewriteHypB}{\hoare{\LBewritePre}{\ewrite{\wtat}{\loc}{\val}}{\LBewritePost}} \\
-  \iinferH{Proto-CAS}{\LBecasHypA \\ \LBecasHypB}{\hoare{\LBecasPre}{\ecas{\loc}{v_o}{v_n}}{\LBecasPost }} \\
+  \iinferH{Proto-Read}{\LBereadHyp}{
+    \hoare{\LBereadPre}
+          {\eread{\rtat}{\loc}}
+          {\Ret \val. \LBereadPost} 
+  } \\
+  \iinferH{Proto-Write}{\LBewriteHypA \\ \LBewriteHypB}{
+    \hoare{\LBewritePre}
+          {\ewrite{\wtat}{\loc}{\val}}
+          {\LBewritePost}
+  } \\
+  \iinferH{Proto-CAS}{\LBecasHypA \\ \LBecasHypB}{
+    \hoare{\LBecasPre}
+          {\ecas{\loc}{v_o}{v_n}}
+          {\LBecasPost}
+  } \\
+  \iinferH{Proto-Persistent}{}{
+    \Prtcl{\loc:\protst|\prot(x)} 
+    \implies \always \Prtcl{\loc:\protst|\prot(x)}
+  }
 \end{mathpar}
 
 \section{Terminology}
@@ -259,24 +354,26 @@ to write events to the location.
 In our encoding, this is a straight-forward extension to GPS protocols.
 
 \subsection{Proof Setup}
-For every GPS protocol name $\prot$ with state space $\protspace$, interpretation
-$\prot(\stst, \val)$, and transition relation $\futst_\prot$, we define the monoid
-$\Prot_\prot \eqdef \STSMon{\mathbb{S}(S)}$, where 
+For every GPS protocol name $\prot$ associated with a location $\loc$ and having 
+an STS $\protspace$ whose transition relation is $\pastst_\prot$, and an
+interpretation $\protint(\stst, \val)$, we define the monoid
+$\Prot_\prot \eqdef \STSMon{\States(S)}$, where 
 \[
-  \ststs \in \States(\protspace) \eqdef \OrdList(\irecordSig[\Sstate][S][\Sbuf][\Buf], \pastst^{\Sstate}_\prot).
+  \ststs \in \States(\protspace) \eqdef \OrdList(\irecordSig[\Sstate][S][\Sbuf][\Buf], \pastst_\prot).
 \]
 
-The transition relation of the STS is defined as follows
+The transition relation $\pastst_\prot$ of the new STS is defined as follows
 \begin{mathpar}
-  \inferrule{}{\nil \ra_{\Prot{\prot}} ((\stst, \buf)::nil)}
-  \and\inferrule{\stst \ra_\prot \stst' }{((\stst, \buf)::\ststs) \ra_{\Prot{\prot}} ((\stst',\buf')::(\stst, \buf)::\ststs) }
+  \inferrule{}{\nil \pastst^{\Sstate}_\prot ((\stst, \buf)::nil)}
+  \and
+  \inferrule{\stst \pastst_\prot \stst'}{((\stst, \buf)::\ststs) \pastst^{\Sstate}_\prot ((\stst',\buf')::(\stst, \buf)::\ststs) }
 \end{mathpar}
 
 We add an additional component to protocols: the duplicable
 interpretation, denoted $\td(\protst, \val)$.
 We assume throughout the rest of the document that 
-\[ \intr{\All \protst \in S, \val. \prot(\protst, \val) 
-    \vs \prot(\protst,\val) \ast \td(\protst, \val)} \]
+\[ \intr{\All \protst \in S, \val. \protint(\protst, \val) 
+    \vs \protint(\protst,\val) \ast \td(\protst, \val)} \]
 and
 \[ \intr{\All \protst \in S, \val. \td(\protst, \val) 
     \vs \td(\protst,\val) \ast \td(\protst, \val)}. \]
@@ -289,26 +386,26 @@ the following STS interpretation predicates.
 \newcommand{\TailInv}[0]{\mathrm{TailInv}}
 \newcommand{\ProtoInv}[0]{\mathrm{ProtoInv}}
 \begin{align*}
-  \varphi_\prot(\ststs) \eqdef{}
+  \varphi_{\loc,\protint}(\ststs) \eqdef{}
   & 
     \Exists \hist. \lhist{\loc}{\hist} 
-    \ast \ProtoInv(\ststs)
+    \ast \ProtoInv_\protint(\ststs)
     \land \hinit(\hist)
     \land \Consistent(\ststs, \hist)
   \\
-  \ProtoInv_\prot(\ststs) \eqdef{}
-  & \HeadInv_\prot(\ststs)
-    \ast \TailInv_\prot(\ststs) \\
-  \HeadInv_\prot(\ststs) \eqdef{}
+  \ProtoInv_\protint(\ststs) \eqdef{}
+  & \HeadInv_\protint(\ststs)
+    \ast \TailInv_\protint(\ststs) \\
+  \HeadInv_\protint(\ststs) \eqdef{}
   & \All \stst, \buf. \ststs = (\stst, \buf) :: \any \implies
-    \int(\stst, \buf{.}\weval)(\buf) \\
-  \TailInv_\prot(\ststs) \eqdef{}
-  & \bigast_{(\stst, \buf) \in \ststs}
-    \intd(\stst, \buf{.}\weval)(\buf) \\
+    \intr{\protint(\stst, \buf{.}\weval)}(\buf) \\
+  \TailInv_\protint(\ststs) \eqdef{}
+  & \bigast_{(\stst, \buf) \in \tl(\ststs)}
+    \intr{\td(\stst, \buf{.}\weval)}(\buf) \\
   \Consistent(\ststs, \hist) \eqdef{}& \dedup(\map(\snd, \ststs)) = \hist
 \end{align*}
 
-\section{Single-Writer Protocols}
+\section{Raw Protocols}
 \def\Toks{\mathcal{T}}%
 \def\toksof{\mathcal{L}}%
 \def\toksfor#1{\mathcal{T}_{-#1}}%
@@ -334,10 +431,10 @@ The writer holds all tokens necessary to have exact knowledge on the current
 state of the STS and, therefore, of the GPS protocol.
 As a consequence, the writer is the only one who can move the STS to a new state.
 \begin{align*}
-  \writer(\gamma)(\ststs) \eqdef{}
-  & \ownGhost{\gamma}{\STSfrag(\set{\ststs}, \toksfor\ststs)} \\
-  \reader(\gamma)(\ststs) \eqdef{}
-  & \ownGhost{\gamma}{\STSfrag(\upclose(\ststs, \emptyset), \emptyset)}
+  \writer(\gname)(\ststs) \eqdef{}
+  & \ownGhost{\gname}{\STSfrag(\set{\ststs}, \toksfor\ststs)} \\
+  \reader(\gname)(\ststs) \eqdef{}
+  & \ownGhost{\gname}{\STSfrag(\upclose(\ststs, \emptyset), \emptyset)}
 \end{align*}
 % 
 % 
@@ -349,199 +446,387 @@ As a consequence, the writer is the only one who can move the STS to a new state
 \def\PrWRaw{\textlog{WriterRaw}}%
 \def\PrRRaw{\textlog{ReaderRaw}}%
 \begin{align*}
-  \PrInv(\prot)(X) \eqdef{}
-  & \Exists \protspace, \futst, \protint.
-    \ot{\prot}{(\protspace, \futst, \protint)}
-    \ast \Exists \ststs \in \States(\protspace).
-    \ownGhost{X}{\STSauth(\ststs, \toksof(\ststs))}
-    \ast \varphi_\protint(\ststs)
+  \PrInv(\protspace,\protint)(\loc,\gname,x) \eqdef{}
+  & \STSInv(\States(\protspace(x)),\varphi_{\loc,\protint(x)},\gname)
   \\
-  % & \STSInv(\States(\prot{.}S), \varphi_\prot, X) \\
+  % & \STSInv(\States(\prot{.}S), \varphi_\prot, x) \\
   % \eqdef{}
   % & \Exists \ststs.
-  %   \ownGhost{X}{\STSauth(\ststs, \toksof(\ststs))}
+  %   \ownGhost{x}{\STSauth(\ststs, \toksof(\ststs))}
   %   \ast \varphi_\prot(\ststs) \\
-  \PrW(\prot, \protst, \buf)(\loc, X) \eqdef{}
+  \PrW(\protst,\buf,\gname) \eqdef{}
   & \Exists \buf_0 \pastb \buf.
-    \writer(X)((\protst, \buf_0) :: \any) \\
-  \PrR(\prot, \protst, \buf)(\loc, X) \eqdef{}
+    \writer(\gname)((\protst, \buf_0) :: \any) \\
+  \PrR(\protst, \buf,\gname) \eqdef{}
   & \Exists \buf_0 \pastb \buf.
-    \reader(X)((\protst, \buf_0) :: \any) \\
-  \PrWRaw(\prot, \protst, \buf)(\loc, q, X) \eqdef{}
-  & \protocol(\prot, \any, \any, \any)
-    \ast \PrW(\prot, \protst, \buf)(\loc, X) \\
-  \PrRRaw(\prot, \protst, \buf)(\loc, q, X) \eqdef{}
-  & \protocol(\prot, \any, \any, \any)
-    \ast \PrR(\prot, \protst, \buf)(\loc, X) \\
+    \reader(\gname)((\protst, \buf_0) :: \any) \\
 \end{align*}
 % 
 % 
 \subsection{Raw Triples}
-% 
+
+\def\RawProtoInitPre{
+  \bseen{\proc}{\buf}
+  \ast \intr{\lraw(\loc)}(\buf)
+  \ast \protst \in \protspace(x)
+  \ast \later\intr{\prot.\protint(x)(\protst,\val)}(\buf)
+}
+\def\RawProtoInitPost{
+  \Exists \buf' \futb \buf.
+    \bseen{\proc}{\buf'}
+    \ast \writer(\gname)((\protst,\buf')::\any)
+    \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+    \ast \linfo^{\ffrac}(\loc,\any)
+}
+
+\def\RawProtoReadPrem{
+  \All \buf. 
+  \All \protst' \futst_\prot \protst.
+  \left(
+    \All \val.
+    \intr{\td(x)(\protst', \val)}(\buf) \ast \intr{P}(\buf)
+    \vs[-\nspace]
+    \intr{Q}(\buf)
+  \right)
+  \lor
+  \left(
+    \All \protst'' \futst_\prot \protst'.
+    \intr{\protint(x)(\protst'', \val)}(\buf) \ast \intr{P}(\buf)
+    \vs[-\nspace]
+    \bot
+  \right)
+}
+\def\RawProtoReadPre{
+  \bseen{\proc}{\buf}
+  \ast \intr{P}(\buf)
+  \ast \PrR(\protst,\buf,\gname)
+  \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+}
+\def\RawProtoReadPost{
+  \Ret\val.
+    \Exists \buf' \futb \buf, \protst' \futst_\prot \protst.
+    \bseen{\proc}{\buf'}
+    \ast \intr{Q}(\buf')
+    \ast \PrR(\protst', \buf',\gname)
+    \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+}
+\def\RawProtoWritePrem{
+  \All \buf' \futb \buf, \buf_1 \bsub \buf_0. 
+  \intr{\protint(x)(\stst', \any)}(\buf_1)
+  \ast \intr{P}(\buf')
+  \vs[-\nspace]
+  \stst'' \futst_\prot \stst'
+  \ast\later\intr{\protint(x)(\stst'', \val)}(\buf') 
+  \ast \intr{Q}(\buf')
+}
+\def\RawProtoWritePre{
+  \bseen{\proc}{\buf}
+  \ast \intr{P}(\buf)
+  \ast \PrW(\protst', \buf_0,\gname)
+  \ast \PrR(\protst, \buf,\gname)
+  \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+}
+\def\RawProtoWritePost{
+  \Exists \buf' \futb \buf.
+  \bseen{\proc}{\buf'}
+  \ast \intr{Q}(\buf')
+  \ast \PrW(\protst'', \buf',\gname)
+  \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+}
+\def\RawProtoCASPremA{
+  \All \buf.
+  \All \protst' \futst_\prot \protst.
+  \intr{\protint(x)(\protst', \val_o)}(\buf) 
+  \ast \intr{P}(\buf)
+  \vs[\mask_1][\mask_2]
+  \Exists \protst'' \futst_\prot \protst',\protst_w. 
+    \writer(\gname)((\protst_w,\any)::\any)
+    \ast \intr{T}(\buf)
+}
+\def\RawProtoCASPremB{
+  \All \buf .
+  \All \protst'' \futst_\prot \protst' \futst_\prot \protst.
+    \writer(\gname)((\protst'',\any)::\any)
+  \ast \intr{T\subst{\protst_w}{\protst'}}(\buf)
+  \vs[\mask_2][\mask_1]
+  \later\intr{\protint(x)(\protst'', \val_n)}(\buf) 
+  \ast \intr{Q}(\buf)
+}
+\def\RawProtoCASPremC{
+  \All \buf.
+  \All \protst' \futst_\prot \protst,\valB.
+  \intr{\td(x)(\protst', \valB)}(\buf) 
+  \ast \intr{P}(\buf)
+  \vs
+  \intr{R}(\buf)
+}
+\def\RawProtoCASPre{
+  \bseen{\proc}{\buf}
+  \ast \intr{P}(\buf)
+  \ast \PrR(\protst, \buf,\gname)
+  \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+}
+\def\RawProtoCASPost{
+  \Ret\val.
+  \begin{array}[t]{l}
+    \Exists \buf' \futb \buf, \protst'' \futst_\prot \protst.
+    \bseen{\proc}{\buf'}
+    \ast \PrR(\protst'', \buf',\gname)
+    \\ 
+    \ast (\val = 1 \ast \intr{Q}(\buf'))
+    \ast (\val = 0 \ast \intr{R}(\buf'))
+    \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+  \end{array}
+}
 \begin{mathpar}
-  \inferH{RawProto-Read}{
-    \All \buf. 
-    \All \protst' \futst_\prot \protst.
-    \left(
-      \All \val.
-      \td(\protst', \val)(\buf) \ast P(\buf)
-      \vs[-\nspace]
-      Q(\buf)
-    \right)
-    \lor
-    \left(
-      \All \protst'' \futst_\prot \protst'.
-      \prot(\protst'', \val)(\buf) \ast P(\buf)
-      \vs[-\nspace]
-      \bot
-    \right)
-  }{
-    \protocol(\prot, \any, \protspace, \prot)
+  \inferH{RawProto-Init}{}{
+    \perInv(\gname_p,\nspace_2)
     \proves
     \All \buf.
-    \hoareV[t]{
-      \bseen{\proc}{\buf}
-      \ast P(\buf)
-      \ast \PrR(\prot, \protst, \buf)(\loc, \any, X)
-      \ast \later\PrInv(\prot)(\loc, X)
-    }{
-      \eread{\rtat}{\loc}{\val}, \proc
-    }{\Ret\val.
-      \Exists \buf' \futb \buf.
-      \bseen{\proc}{\buf'}
-      \ast Q(\buf')
-      \ast \PrR(\prot, \protst, \buf')(\loc, \any, X)
-      \ast \later\PrInv(\prot)(\loc, X)
-    }_{\nspace_1}
+    \hoareV[t]{\RawProtoInitPre}
+              {\ewrite{\wtna}{\loc}{\val}, \proc}
+              {\RawProtoInitPost}_{\nspace_1}
   }
   \\
-  \inferH{RawProto-Write}{
-    \All \buf. 
-    \prot(\stst, \any)(\buf)
-    \ast P(\buf)
-    \ast \writer(X)(\stst)
-    \vs[-\nspace]
-    \stst'' \futst_\prot \stst
-    \ast \later\prot(\stst'', \val)(\buf) \ast Q(\buf)
-  }{
-    \protocol(\prot, \any, \protspace, \prot)
+  \inferH{RawProto-Read}{\RawProtoReadPrem}{
+    \protst \in \protspace(x)
     \proves
     \All \buf.
-    \hoareV[t]{
-      \bseen{\proc}{\buf}
-      \ast P(\buf)
-      \ast \PrW(\prot, \protst, \buf)(\loc, \any, X)
-      \ast \later\PrInv(\prot)(\loc, X)
-    }{
-      \ewrite{\wtat}{\loc}{\val}, \proc
-    }{
-      \Exists \buf' \futb \buf.
-      \bseen{\proc}{\buf'}
-      \ast Q(\buf')
-      \ast \PrR(\prot, \protst, \buf')(\loc, \any, X)
-      \ast \later\PrInv(\prot)(\loc, X)
-    }_{\nspace_1}
+    \hoareV[t]{\RawProtoReadPre}
+              {\eread{\rtat}{\loc}, \proc}
+              {\RawProtoReadPost}_{\nspace_1}
+  }
+  \\
+  \inferH{RawProto-Write}{\RawProtoWritePrem}{
+    \protst,\protst',\protst'' \in \protspace(x)
+    \proves
+    \hoareV[t]{\RawProtoWritePre}
+              {\ewrite{\wtat}{\loc}{\val}, \proc}
+              {\RawProtoWritePost}_{\nspace_1}
   }
   \\
   \inferH{RawProto-CAS}{
-    \All \buf.
-    \All \protst' \futst_\prot \protst.
-    \later\prot(\protst', \val_o)(\buf) \ast P(\buf)
-    \vs[\mask_1][\mask_2]
-    \later(
-    \Exists \protst_w. \writer(X)(\protst_w)
-    \ast T(\buf)
-    )
+    \RawProtoCASPremA
     \\
-    \All \buf.
-    \All \protst' \futst_\prot \protst.
-    \writer(X)(\protst')
-    \ast T\subst{\protst_w}{\protst'}(\buf)
-    \vs[\mask_2][\mask_1]
-    \Exists \protst'' \futst_\prot \protst'. 
-    \later\prot(\protst'', \val_n)(\buf) \ast Q(\buf)
+    \RawProtoCASPremB
     \\
-    \All \buf.
-    \All \valB \neq \val_o. 
-    \td(\protst, \valB)(\buf) \ast P(\buf)
-    \vs
-    R(\buf)
+    \RawProtoCASPremC
     \\
     \mask_1 \supseteq \mask_2
     \\
     \mask_1 \disj \nspace_1
   }{
-    \protocol(\prot, \any, \protspace, \prot)
+    \protst \in \protspace(x)
     \proves
     \All \buf.
-    \hoareV[t]{
-      \bseen{\proc}{\buf}
-      \ast P(\buf)
-      \ast \PrW(\prot, \protst, \buf)(\loc, \any, X)
-      \ast \later\PrInv(\prot)(\loc, X)
-    }{
-      \ecas{\loc}{\val_o}{\val_n}, \proc
-    }{
-      \Ret\val.
-      \begin{array}[t]{l}
-        \Exists \buf' \futb \buf.
-        \bseen{\proc}{\buf'}
-        \ast \PrR(\prot, \protst, \buf')(\loc, \any, X)
-        \\ 
-        \ast (\val = 1 \ast Q(\buf'))
-        \ast (\val = 0 \ast R(\buf'))
-        \ast \later\PrInv(\prot)(\loc, X)
-      \end{array}
-    }_{\nspace_1}
+    \hoareV[t]{\RawProtoCASPre}
+              {\ecas{\loc}{\val_o}{\val_n}, \proc}
+              {\RawProtoCASPost}_{\nspace_1}
   }
 \end{mathpar}
+% % 
+% \begin{mathpar}
+%   \inferH{RawProto-Read}{
+%     \All \buf. 
+%     \All \protst' \futst_\prot \protst.
+%     \left(
+%       \All \val.
+%       \td(x)(\protst', \val)(\buf) \ast P(\buf)
+%       \vs[-\nspace]
+%       Q(\buf)
+%     \right)
+%     \lor
+%     \left(
+%       \All \protst'' \futst_\prot \protst'.
+%       \protint(x)(\protst'', \val)(\buf) \ast P(\buf)
+%       \vs[-\nspace]
+%       \bot
+%     \right)
+%   }{
+%     \protst \in \protspace(x)
+%     \proves
+%     \All \buf.
+%     \hoareV[t]{
+%       \bseen{\proc}{\buf}
+%       \ast P(\buf)
+%       \ast \PrR(\protst,\buf)(\loc,\gname,x)
+%       \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+%     }{
+%       \eread{\rtat}{\loc}{\val}, \proc
+%     }{\Ret\val.
+%       \Exists \buf' \futb \buf.
+%       \bseen{\proc}{\buf'}
+%       \ast Q(\buf')
+%       \ast \PrR(\protst, \buf')(\loc,\gname,x)
+%       \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+%     }_{\nspace_1}
+%   }
+%   \\
+%   \inferH{RawProto-Write}{
+%     \All \buf. 
+%     \protint(x)(\stst, \any)(\buf)
+%     \ast P(\buf)
+%     \ast \writer(\gname)(\stst)
+%     \vs[-\nspace]
+%     \stst'' \futst_\prot \stst
+%     \ast \later\protint(x)(\stst'', \val)(\buf) \ast Q(\buf)
+%   }{
+%     \protst \in \protspace(x)
+%     \proves
+%     \All \buf.
+%     \hoareV[t]{
+%       \bseen{\proc}{\buf}
+%       \ast P(\buf)
+%       \ast \PrW(\protst, \buf)(\loc,\gname,x)
+%       \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+%     }{
+%       \ewrite{\wtat}{\loc}{\val}, \proc
+%     }{
+%       \Exists \buf' \futb \buf.
+%       \bseen{\proc}{\buf'}
+%       \ast Q(\buf')
+%       \ast \PrR(\protst, \buf')(\loc,\gname,x)
+%       \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+%     }_{\nspace_1}
+%   }
+%   \\
+%   \inferH{RawProto-CAS}{
+%     \All \buf.
+%     \All \protst' \futst_\prot \protst.
+%     \later\protint(x)(\protst', \val_o)(\buf) \ast P(\buf)
+%     \vs[\mask_1][\mask_2]
+%     \later(
+%     \Exists \protst_w. \writer(\gname)(\protst_w)
+%     \ast T(\buf)
+%     )
+%     \\
+%     \All \buf.
+%     \All \protst' \futst_\prot \protst.
+%     \writer(\gname)(\protst')
+%     \ast T\subst{\protst_w}{\protst'}(\buf)
+%     \vs[\mask_2][\mask_1]
+%     \Exists \protst'' \futst_\prot \protst'. 
+%     \later\protint(x)(\protst'', \val_n)(\buf) \ast Q(\buf)
+%     \\
+%     \All \buf.
+%     \All \valB \neq \val_o. 
+%     \td(x)(\protst, \valB)(\buf) \ast P(\buf)
+%     \vs
+%     R(\buf)
+%     \\
+%     \mask_1 \supseteq \mask_2
+%     \\
+%     \mask_1 \disj \nspace_1
+%   }{
+%     \protst \in \protspace(x)
+%     \proves
+%     \All \buf.
+%     \hoareV[t]{
+%       \bseen{\proc}{\buf}
+%       \ast P(\buf)
+%       \ast \PrW(\protst, \buf)(\loc,\gname,x)
+%       \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+%     }{
+%       \ecas{\loc}{\val_o}{\val_n}, \proc
+%     }{
+%       \Ret\val.
+%       \begin{array}[t]{l}
+%         \Exists \buf' \futb \buf.
+%         \bseen{\proc}{\buf'}
+%         \ast \PrR(\protst, \buf')(\loc,\gname,x)
+%         \\ 
+%         \ast (\val = 1 \ast Q(\buf'))
+%         \ast (\val = 0 \ast R(\buf'))
+%         \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+%       \end{array}
+%     }_{\nspace_1}
+%   }
+% \end{mathpar}
 % 
 %
 \subsection{Lemmas}
 %
-\begin{lemH}[lem:writer-exact]{Reader-Sufficient}
+\begin{lemH}[lem:rawprt-state-ordered]{RawProto-State-Ordered}
+  \[
+    ((\protst_1,\any)::\any) \pastst^{\Sstate}_\prot ((\protst_2,\any)::\any)
+    \implies 
+    \protst_1 \pastst_\prot \protst_2
+  \]
+\end{lemH}
+%
+\begin{lemH}[lem:rawprt-reader-ordered]{RawProto-Reader-Ordered}
   \[
-    \ownGhost{\gname}{\STSauth(\ststs', \toksof(\ststs'))} \ast \reader(\ststs)(\gname)
-    \implies \ststs \pastst_\prot \ststs'
+    \reader(\gname)(\ststs_1) \ast \reader(\gname)(\ststs_2)
+    \implies 
+      \ststs_1 \pastst^{\Sstate}_\prot \ststs_2 \lor \ststs_2 \pastst^{\Sstate}_\prot \ststs_1
   \]
 \end{lemH}
 %
-\begin{lemH}[lem:writer-exact]{Writer-Exact}
+\begin{lemH}[lem:rawprt-reader-sufficient]{RawProto-Reader-Sufficient}
   \[
-    \ownGhost{\gname}{\STSauth(\ststs', \Toks')} \ast \writer(\ststs)(\gname)
+    \ownGhost{\gname}{\STSauth(\ststs', \toksof(\ststs'))} 
+    \ast \reader(\gname)(\ststs)
+    \implies \ststs \pastst^{\Sstate}_\prot \ststs'
+  \]
+\end{lemH}
+%
+\begin{lemH}[lem:rawprt-writer-latest]{RawProto-Writer-Latest}
+  \[
+    \writer(\gname)(\ststs)\ast \reader(\gname)(\ststs')
+    \implies \ststs' \pastst^{\Sstate}_\prot \ststs
+  \]
+\end{lemH}
+%
+\begin{lemH}[lem:rawprt-writer-unique]{RawProto-Writer-Unique}
+  \[
+    \writer(\gname)(\any)\ast \writer(\gname)(\any)
+    \implies \bot
+  \]
+\end{lemH}
+%
+\begin{lemH}[lem:rawprt-writer-fork]{RawProto-Writer-Fork}
+  \[
+    \writer(\gname)(\ststs)
+    \implies \writer(\gname)(\ststs) \ast \reader(\gname)(\ststs)
+  \]
+\end{lemH}
+%
+\begin{lemH}[lem:rawprt-writer-exact]{RawProto-Writer-Exact}
+  \[
+    \ownGhost{\gname}{\STSauth(\ststs', \Toks')} \ast \writer(\gname)(\ststs)
     \implies \ststs' = \ststs \land \Toks' = \toksfor{\stst'}
   \]
 \end{lemH}
 %
-\begin{lemH}[lem:writer-exact]{Writer-Combine}
+\begin{lemH}[lem:rawprt-writer-combine]{RawProto-Writer-Combine}
   \[
-    \ownGhost{\gname}{\STSauth(\any, \toksof(\any))} \ast \writer(\ststs)(\gname)
+    \ownGhost{\gname}{\STSauth(\any, \toksof(\any))} \ast \writer(\gname)(\ststs)
     \implies \ownGhost{\gname}{\STSauth(\ststs, \Toks)}
   \]
 \end{lemH}
 %
-\begin{lemH}[lem:writer-exact]{Writer-Extract}
+\begin{lemH}[lem:rawprt-writer-extract]{RawProto-Writer-Extract}
   \[
     \ownGhost{\gname}{\STSauth(\ststs, \Toks)} 
     \implies
-    \ownGhost{\gname}{\STSauth(\ststs, \toksfor{\ststs})}
-    \ast \writer(\ststs)(\gname) 
+    \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \writer(\gname)(\ststs) 
   \]
 \end{lemH}
 %
-\begin{lemH}[lem:raw-write-unfold]{Write-Unfold}
+\begin{lemH}[lem:rawprt-writer-unfold]{RawProto-Writer-Unfold}
   \[
     \begin{array}{r@{}l}
-      & \later\Pr(\prot)(\loc, X)
-        \ast \PrW(\prot, \protst, \buf)(\loc, \any, X) \\
+      & \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+        \ast \PrW(\protst,\buf,\gname) \\
       {}\vsE{}
       & \Exists \ststs, \buf_0 \pastb \buf, \hist. 
         \lhist{\loc}{\hist}
-        \ast \ownGhost{X}{\STSauth(\ststs, \Toks)}
+        \ast \ownGhost{\gname}{\STSauth(\ststs, \Toks)}
         \ast \head(\ststs) = (\protst, \buf_0)
         \ast \linit(\hist, \buf) \ast \lat(\hist, \buf) \\
       &{}
-        \ast \later\prot(\protst, \buf_0.\weval)(\buf_0)
+        \ast \later\protint(x)(\protst, \buf_0.\weval)(\buf_0)
         \ast \later\TailInv(\ststs)
         \ast \hinit(\hist)
         \ast \Consistent(\ststs, \hist)
@@ -549,19 +834,18 @@ As a consequence, the writer is the only one who can move the STS to a new state
   \]
 \end{lemH}
 %
-\begin{lemH}[lem:raw-write-unfold]{Reader-Unfold}
+\begin{lemH}[lem:rawprt-reader-unfold]{RawProto-Reader-Unfold}
   \[
     \begin{array}{r@{}l}
-      & \later\Pr(\prot)(\loc, X)
-        \ast \PrR(\prot, \protst, \buf)(\loc, \any, X) \\
+      & \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+        \ast \PrR(\protst,\buf,\gname) \\
       {}\vsE{}
       & \Exists \ststs, \buf_0 \pastb \buf, \hist. 
         \lhist{\loc}{\hist}
-        \ast \ownGhost{X}{\STSauth(\ststs, \toksfor{\ststs})}
+        \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
         \ast (\protst, \buf_0) \in \ststs
         \ast \linit(\hist, \buf) \ast \lat(\hist, \buf) \\
       &{}
-        \ast \later\td(\protst, \buf_0.\weval)(\buf_0)
         \ast \later\HeadInv(\ststs)
         \ast \later\TailInv(\ststs)
         \ast \hinit(\hist)
@@ -570,23 +854,511 @@ As a consequence, the writer is the only one who can move the STS to a new state
   \]
 \end{lemH}
 %
-\begin{lemH}[lem:protocol-move]{Protocol-Move}
+\begin{lemH}[lem:rawprt-protocol-move]{RawProto-Protocol-Move}
   \[
-    \ststs \ststrans_{\Prot_\prot} \ststs' \vdash
+    \ststs \pastst^{\Sstate}_\prot \ststs' \vdash
     \ownGhost{\gamma}{\STSauth(\ststs, \Toks)} \vs
     \ownGhost{\gamma}{\STSauth(\ststs', \Toks)}
   \]
 \end{lemH}
 %
-\begin{lemH}[lem:writer-inv]{Writer-Invariant}
+\begin{lemH}[lem:rawprt-writer-inv]{RawProto-Writer-Invariant}
   \[
     \knowInv{\iname}{\Exists \ststs'.
-      \writer(\ststs')(\gname)} \vdash
-    \reader(\ststs)(\gname) 
+      \writer(\gname)(\ststs')} \vdash
+    \reader(\gname)(\ststs) 
     \vsE[\set\iname][\emptyset]
-    \Exists \ststs'' \ststransL \ststs. \writer(\ststs'')(\gname)
+    \Exists \ststs'' \futst^{\Sstate}_\prot \ststs. \writer(\gname)(\ststs'')
   \]
 \end{lemH}
+
+\subsection{Proofs of Raw Triples}
+
+\subsubsection{\ruleref{RawProto-Init}}
+
+
+\begin{proofoutline*}
+  \VARS{\buf,\proc} \\
+  \CTX{\bseen{\proc}{\buf}, \perInv(\gname_p, \nspace_2)}\\
+  \RES{
+    \intr{\lraw(\loc)}(\buf)
+    \ast \protst \in \protspace(x) 
+    \ast \later \intr{\protint(x)(\protst, \val)}(\buf)
+  }\\
+  \CTX{\protst \in \protspace(x)}\\
+  \cdline{\ewrite{\wtna}{\loc}{\val}}\\
+  \RES{
+    \Exists \buf' \futb \buf. \bseen{\proc}{\buf'}
+    \ast \intr{\lraw(\loc,\Some \val)}(\buf')
+    \ast \later \intr{\protint(x)(\protst, \val)}(\buf)}
+    \BY \ruleref{Raw-Write}\\
+  \RES{
+    \Exists \buf' \futb \buf. \bseen{\proc}{\buf'}
+    \ast \intr{\lraw(\loc,\Some \val)}(\buf')
+    \ast \later \intr{\protint(x)(\protst, \val)}(\buf')}\\
+  \CTX{\buf' \futb \buf, \bseen{\proc}{\buf'}}\\
+  Pick $\ststs \eqdef (\protst,\buf')::\nil$. \\
+  \RES{
+    \Exists \gname.
+    \ownGhost{\gname}{\STSauth(\ststs, \Toks)} 
+    \ast \intr{\lraw(\loc,\Some \val)}(\buf')
+    \ast \later \intr{\protint(x)(\protst, \val)}(\buf')
+  }\\
+  \RES{
+    \ownGhost{\gname}{\STSauth(\ststs, \Toks)} 
+    \ast \later\varphi_{\loc,\protint}(\ststs)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  }\\
+  \RES{
+    \writer(\gname)(\ststs)
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \later\varphi_{\loc,\protint}(\ststs)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  } \BY \ruleref{lem:rawprt-writer-extract}\\
+  \RES{
+    \writer(\gname)(\ststs)
+    \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  } \\
+  \RES{
+    \Exists \buf' \futb \buf.
+    \bseen{\proc}{\buf'}
+    \ast \writer(\gname)((\protst,\buf')::\any)
+    \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+    \ast \linfo^{\ffrac}(\loc,\any)
+  } \\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{RawProto-Read}}
+\begin{proofoutline*}
+  \CTX{\RawProtoReadPrem}\\
+  \CTX{\protst \in \protspace(x)}\\
+  \RES{\RawProtoReadPre}\\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{
+    \begin{aligned}
+      \intr{P}(\buf)
+      &{}
+        \ast \Exists \ststs, \buf_0 \pastb \buf, \hist. 
+        \lhist{\loc}{\hist}
+        \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+        \ast (\protst, \buf_0) \in \ststs
+        \ast \linit(\hist, \buf) \\
+      &{}
+        \ast \lat(\hist, \buf)
+        \ast \later\HeadInv(\ststs)
+        \ast \later\TailInv(\ststs)
+        \ast \hinit(\hist)
+        \ast \Consistent(\ststs, \hist)
+    \end{aligned}
+  } \BY \ruleref{lem:rawprt-reader-unfold}\\
+  \VARS{\ststs, \buf_0, \hist}\\
+  \CTX{
+    \buf_0 \pastb \buf,
+    (\protst, \buf_0) \in \ststs,
+    \linit(\hist, \buf),
+    \lat(\hist, \buf),
+    \hinit(\hist),
+    \Consistent(\ststs, \hist)
+  }\\
+  \RES{
+    \intr{P}(\buf)
+    \ast \lhist{\loc}{\hist}
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \later\HeadInv(\ststs)
+    \ast \later\TailInv(\ststs)
+  } \IND
+    \RES{\lhist{\loc}{\hist}} \BY Frame\\
+    \cdline{\eread{\rtat}{\loc}}\\
+    \RES{\Ret \val.
+      \Exists \buf' \futb \buf. 
+      \bseen{\proc}{\buf'}
+      \ast \lhist{\loc}{\hist} 
+      \ast \lat(\hist, \buf')
+      \ast \Exists \buf_1 \pastb \buf'.
+      \mr{\buf'}{\buf_1}
+      \ast \buf_1 \in \hist 
+      \ast \buf_1.\weval = \val 
+    } \BY \ruleref{Base-Read-AT}\\
+    \CTX{\buf' \futb \buf, 
+        \bseen{\proc}{\buf'},
+        \lat(\hist, \buf'),
+        \buf_1 \pastb \buf',
+        \mr{\buf'}{\buf_1},
+        \buf_1 \in \hist,
+        \buf_1.\weval = \val
+    }\\
+    \RES{\Ret \val.\lhist{\loc}{\hist}}\\
+    \CTX{\Exists \protst'. (\protst',\buf_1) \in \ststs}
+      from $\buf_1 \in \hist$ and $\Consistent(\ststs, \hist)$\\
+    From $\mr{\buf'}{\buf_1}$ and $\buf' \futb \buf \futb \buf_0$, we have
+    $\head(\buf_1).\wetime \ge \head(\buf_0).\wetime$. \\
+    From monotonicity of $\hist$ and $\buf_1, \buf_0 \in \hist$,
+    have $\protst' \futst \protst$.
+  \UNIND
+  \RES{
+    \intr{P}(\buf)
+    \ast \lhist{\loc}{\hist}
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \HeadInv(\ststs)
+    \ast \TailInv(\ststs)
+  } \\
+  \RES{
+    \intr{P}(\buf')
+    \ast \lhist{\loc}{\hist}
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \HeadInv(\ststs)
+    \ast \TailInv(\ststs)
+  } \\
+  \RES{
+    \intr{P}(\buf')
+    \ast \later\td(x)(\protst',\buf_1)
+    \ast \lhist{\loc}{\hist}
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \HeadInv(\ststs)
+    \ast \TailInv(\ststs)
+  } since $(\protst',\buf_1) \in \ststs$\\
+  \RES{
+    \intr{Q}(\buf')
+    \ast \lhist{\loc}{\hist}
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \HeadInv(\ststs)
+    \ast \TailInv(\ststs)
+  } \BY assm.\\
+  \RES{
+    \intr{Q}(\buf')
+    \ast \PrR(\protst',\buf',\gname)
+    \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+  } \BY \ruleref{lem:rawprt-reader-unfold}\\
+  \RES{\RawProtoReadPost}\\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{RawProto-Write}}
+\begin{proofoutline*}
+  \CTX{\RawProtoWritePrem}\\
+  \CTX{\protst \in \protspace(x)}\\
+  \RES{\RawProtoWritePre}\\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{
+    \begin{aligned}
+      & \intr{P}(\buf) 
+        \ast \Exists \buf_1 \bsub \buf_0. \writer(\gname)((\protst',\buf_1)::\any)\\
+      &{}
+        \ast \Exists \ststs, \buf'_0 \pastb \buf, \hist. 
+        \lhist{\loc}{\hist}
+        \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+        \ast (\protst, \buf'_0) \in \ststs
+        \ast \linit(\hist, \buf) \\
+      &{}
+        \ast \lat(\hist, \buf)
+        \ast \later\HeadInv(\ststs)
+        \ast \later\TailInv(\ststs)
+        \ast \hinit(\hist)
+        \ast \Consistent(\ststs, \hist)
+    \end{aligned}
+  } \BY \ruleref{lem:rawprt-reader-unfold}\\
+  \VARS{\ststs, \buf'_0, \buf_1, \hist}\\
+  \CTX{
+    \buf_1 \pastb \buf_0,  
+    \buf'_0 \pastb \buf,
+    (\protst, \buf'_0) \in \ststs,
+    \linit(\hist, \buf),
+    \lat(\hist, \buf),
+    \hinit(\hist),
+    \Consistent(\ststs, \hist)
+  }\\
+  \RES{
+    \intr{P}(\buf) 
+    \ast \writer(\gname)((\protst',\buf_1)::\any)
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \lhist{\loc}{\hist}
+    \ast \later\HeadInv(\ststs)
+    \ast \later\TailInv(\ststs)
+  } \\
+  \CTX{(\protst',\buf_1) = \head(\ststs)} 
+    follows from \ruleref{lem:rawprt-writer-exact}\\
+  \RES{
+    \intr{P}(\buf) 
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \Toks)}
+    \ast \lhist{\loc}{\hist}
+    \ast \later\HeadInv(\ststs)
+    \ast \later\TailInv(\ststs)
+  } \BY \ruleref{lem:rawprt-writer-combine}
+  \IND
+    \RES{\lhist{\loc}{\hist}} \BY Frame \\
+    \cdline{\ewrite{\wtat}{\loc}{\val},\proc}\\
+    \RES{\ewriteATPostB} \BY \ruleref{Base-Write-AT}\\
+    Pick $\hist' \eqdef \buf'::\hist$. \\
+    \CTX{
+      \buf' \futb \buf,
+      \bseen{\proc}{\buf'},
+      \lna(\hist', \buf'),
+      \buf'.\weval = \val,
+      \linit(\hist')
+    } \\
+    \RES{\lhist{\loc}{\hist'}}
+  \UNIND
+  \RES{
+    \intr{P}(\buf) 
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \Toks)}
+    \ast \lhist{\loc}{\hist'}
+    \ast \HeadInv(\ststs)
+    \ast \TailInv(\ststs)
+  } \\
+  \RES{
+    \intr{P}(\buf') 
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \Toks)}
+    \ast \lhist{\loc}{\hist'}
+    \ast \HeadInv(\ststs)
+    \ast \TailInv(\ststs)
+  } since $\buf \pastb \buf'$ \\
+  \RES{
+    \intr{P}(\buf') 
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \Toks)}
+    \ast \lhist{\loc}{\hist'}
+    \ast \intr{\protint(x)(s',\any)}(\buf_1)
+    \ast \TailInv(\ststs)
+  } since $(\protst',\buf_1) = \head(\ststs)$ \\
+  \RES{
+    \protst'' \futst_\prot \protst'
+    \ast \later\intr{\protint(x)(\protst'',\val)}(\buf')
+    \ast \intr{Q}(\buf')
+    \ast \intr{\td(x)(s',\any)}(\buf_1)
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \Toks)}
+    \ast \lhist{\loc}{\hist'}
+    \ast \TailInv(\ststs)
+  } \BY assm.\\
+  Pick $\ststs' \eqdef (\protst'',\buf')::\ststs \futst^{\Sstate}_\prot \ststs$.\\
+  \RES{
+    \intr{Q}(\buf')
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \Toks)}
+    \ast \lhist{\loc}{\hist'}
+    \ast \later\HeadInv(\ststs')
+    \ast \later\TailInv(\ststs')
+    \ast \Consistent(\ststs',\hist')
+  } \\
+  \RES{
+    \intr{Q}(\buf')
+    \ast \ownGhost{\gname}{\STSauth(\ststs', \Toks)}
+    \ast \lhist{\loc}{\hist'}
+    \ast \later\HeadInv(\ststs')
+    \ast \later\TailInv(\ststs')
+    \ast \Consistent(\ststs',\hist')
+  } \\ \quad \BY \ruleref{lem:rawprt-protocol-move} \\
+  \CTX{\lat(\hist',\buf'), (\protst'',\buf') = \head(\ststs')}\\
+  \RES{
+    \intr{Q}(\buf')
+    \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+    \ast \PrW(\protst'',\buf',\gname)
+  } \BY \ruleref{lem:rawprt-writer-unfold}\\
+  \RES{\RawProtoWritePost}\\
+\end{proofoutline*}
+
+\subsubsection{\ruleref{RawProto-CAS}}
+\begin{proofoutline*}
+  \CTX{\RawProtoCASPremA}\\
+  \CTX{\RawProtoCASPremB}\\
+  \CTX{\RawProtoCASPremC}\\
+  \CTX{\protst \in \protspace(x)}\\
+  \RES{\RawProtoCASPre}\\
+  \CTX{\bseen{\proc}{\buf}}\\
+  \RES{
+    \begin{aligned}
+      \intr{P}(\buf)
+      &{}
+        \ast \Exists \ststs, \buf_0 \pastb \buf, \hist. 
+        \lhist{\loc}{\hist}
+        \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+        \ast (\protst, \buf_0) \in \ststs
+        \ast \linit(\hist, \buf) \\
+      &{}
+        \ast \lat(\hist, \buf)
+        \ast \later\HeadInv(\ststs)
+        \ast \later\TailInv(\ststs)
+        \ast \hinit(\hist)
+        \ast \Consistent(\ststs, \hist)
+    \end{aligned}
+  } \BY \ruleref{lem:rawprt-reader-unfold}\\
+  \VARS{\ststs, \buf_0, \hist}\\
+  \CTX{
+    \buf_0 \pastb \buf,
+    (\protst, \buf_0) \in \ststs,
+    \linit(\hist, \buf),
+    \lat(\hist, \buf),
+    \hinit(\hist),
+    \Consistent(\ststs, \hist)
+  }\\
+  \RES{
+    \intr{P}(\buf)
+    \ast \lhist{\loc}{\hist}
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \later\HeadInv(\ststs)
+    \ast \later\TailInv(\ststs)
+  } \IND
+    \RES{\lhist{\loc}{\hist}}\\
+    \cdline{\ecas{\loc}{\val_o}{\val_n}, \proc}\\
+    \RES{\ecasPostB} \BY \ruleref{Base-CAS}\\ 
+    \CTX{
+      \buf' \futb \buf,
+      \bseen{\proc}{\buf'},
+      \linit(\hist', \buf')
+    }\\
+    \CTX{
+      \begin{aligned}
+        & \val = 1 
+        \ast \hist' = \buf' :: \hist
+        \ast \buf' \futb \head(\hist)
+        \ast \head(\hist).\weval = \val_o 
+        \ast \buf'.\weval = \val_n
+        \ast \lna(\hist', \buf') \\
+      {}\lor{}
+        & \val = 0 
+        \ast \hist' = \hist
+        \ast \head(\hist).\weval \neq \val_o
+        \ast \lat(\hist', \buf')
+        \ast \Exists \buf_1 \pastb \buf'.
+        \ast \buf_1 \in \hist
+        \ast \mr{\buf'}{\buf_1}
+      \end{aligned}
+    }\\
+    \CTX{\lhist{\loc}{\hist'}}
+  \UNIND
+  \RES{
+    \intr{P}(\buf)
+    \ast \lhist{\loc}{\hist'}
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \HeadInv(\ststs)
+    \ast \TailInv(\ststs)
+  }\\
+  \RES{
+    \intr{P}(\buf')
+    \ast \lhist{\loc}{\hist'}
+    \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+    \ast \HeadInv(\ststs)
+    \ast \TailInv(\ststs)
+  } \BY $\buf' \futb \buf$
+  \IND
+    \textbf{Case}: $\val = 1$ \\
+    \CTX{\hist' = \buf' :: \hist,
+        \buf' \futb \head(\hist),
+        \head(\hist).\weval = \val_o,
+        \buf'.\weval = \val_n,
+        \lna(\hist', \buf')} \\
+    \RES{
+      \intr{P}(\buf')
+      \ast \lhist{\loc}{\hist'}
+      \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+      \ast \Exists \protst' \futst_\prot \protst. 
+        (\protst',\head(\hist)) = \head(\ststs)
+        \ast \intr{\protint(x)(\protst', \val_o)}(\head(\hist))
+      \ast \TailInv(\ststs)
+    } \\
+    \CTX{\protst' \futst_\prot \protst,
+        (\protst',\head(\hist)) = \head(\ststs)}\\
+    \RES{
+      \intr{P}(\buf')
+      \ast \intr{\protint(x)(\protst', \val_o)}(\buf')
+      \ast \lhist{\loc}{\hist'}
+      \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+      \ast \intr{\td(x)(\protst', \val_o)}(\head(\hist))
+      \ast \TailInv(\ststs)
+    } since $\buf' \futb \head(\hist)$\\
+    \RES{
+      \begin{aligned}
+      & \Exists \protst'' \futst_\prot \protst', \protst_w.
+        \writer(\gname)((\protst_w,\any)::\any)
+        \ast \intr{T}(\buf')\\
+      &{}\ast \lhist{\loc}{\hist'}
+        \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+        \ast \intr{\td(x)(\protst', \val_o)}(\head(\hist))
+        \ast \TailInv(\ststs)
+      \end{aligned}
+    } \BY 1st assm.\\
+    \CTX{\protst'' \futst_\prot \protst', \protst' = \protst_w}\\
+    \RES{
+      \intr{T\subst{\protst_w}{\protst'}}(\buf')
+      \ast \ownGhost{\gname}{\STSauth(\ststs, \Toks)}
+      \ast \lhist{\loc}{\hist'}
+      \ast \intr{\td(x)(\protst', \val_o)}(\head(\hist))
+      \ast \TailInv(\ststs)
+    }\\ \quad \BY \ruleref{lem:rawprt-writer-combine}\\
+    Pick $\ststs' \eqdef (\protst'',\buf')::\ststs \futst^{\Sstate}_\prot$.
+    Have $\Consistent(\ststs',\hist')$.\\
+    \RES{
+      \intr{T\subst{\protst_w}{\protst'}}(\buf')
+      \ast \ownGhost{\gname}{\STSauth(\ststs', \Toks)}
+      \ast \lhist{\loc}{\hist'}
+      \ast \TailInv(\ststs')
+    } \BY \ruleref{lem:rawprt-protocol-move}\\
+    \RES{
+      \intr{T\subst{\protst_w}{\protst'}}(\buf')
+      \ast \writer(\gname)(\ststs')
+      \ast \ownGhost{\gname}{\STSauth(\ststs', \toksof(\ststs'))}
+      \ast \lhist{\loc}{\hist'}
+      \ast \later\TailInv(\ststs')
+    } \\ \quad \BY \ruleref{lem:rawprt-writer-extract}\\
+    \RES{
+      \intr{Q}(\buf')
+      \ast \later\intr{\protint(x)(\protst'', \val_n)}(\buf')
+      \ast \ownGhost{\gname}{\STSauth(\ststs', \toksof(\ststs'))}
+      \ast \lhist{\loc}{\hist'}
+      \ast \later\TailInv(\ststs')
+    } \BY 2nd assm.\\
+    \RES{
+      \intr{Q}(\buf')
+      \ast \ownGhost{\gname}{\STSauth(\ststs', \toksof(\ststs'))}
+      \ast \lhist{\loc}{\hist'}
+      \ast \later\HeadInv(\ststs')
+      \ast \later\TailInv(\ststs')
+    } \\
+    \RES{
+      \intr{Q}(\buf')
+      \ast \PrR(\protst'',\buf',\gname)
+      \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+    } \BY \ruleref{lem:rawprt-reader-unfold}\\
+    \prule\\
+    \textbf{Case}: $\val = 0$ \\
+    \CTX{\hist' = \hist,
+        \head(\hist).\weval \neq \val_o,
+        \lat(\hist', \buf'),
+        \buf_1 \pastb \buf',
+        \buf_1 \in \hist,
+        \mr{\buf'}{\buf_1}
+    }\\
+    \CTX{\Exists \protst_w \futst_\prot \protst. (\protst_w,\buf_1) \in \ststs},
+      from $\head(\buf_0).\wetime \le \head(\buf_1).\wetime$ and 
+      $\buf_0, \buf_1 \in \hist$. \\
+    \RES{
+      \intr{P}(\buf')
+      \ast \intr{\td(x)(\protst_w,\buf_1.\weval)}(\buf_1)
+      \ast \lhist{\loc}{\hist'}
+      \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+      \ast \HeadInv(\ststs)
+      \ast \TailInv(\ststs)
+    }\\
+    \RES{
+      \intr{P}(\buf')
+      \ast \intr{\td(x)(\protst_w,\buf_1.\weval)}(\buf')
+      \ast \lhist{\loc}{\hist'}
+      \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+      \ast \HeadInv(\ststs)
+      \ast \TailInv(\ststs)
+    } since $\buf_1 \pastb \buf'$\\
+    \RES{
+      \intr{R}(\buf')
+      \ast \lhist{\loc}{\hist'}
+      \ast \ownGhost{\gname}{\STSauth(\ststs, \toksof(\ststs))}
+      \ast \HeadInv(\ststs)
+      \ast \TailInv(\ststs)
+    } \BY 2nd assm.\\
+    \RES{
+      \intr{R}(\buf')
+      \ast \PrR(\protst_w,\buf',\gname)
+      \ast \later\PrInv(\protspace,\protint)(\loc,\gname,x)
+    } \BY \ruleref{lem:rawprt-reader-unfold}
+  \UNIND
+  \RES{\RawProtoCASPost}\\
+\end{proofoutline*}
 %
 %
 %%% Local Variables:
diff --git a/layer1.tex b/layer1.tex
index 0803aead5781df464b8d1c1771909f4b443795da..c2bc4337455c38744883ef2f6b26c1ebe2e7a461 100644
--- a/layer1.tex
+++ b/layer1.tex
@@ -158,11 +158,11 @@ The triples provided are:
   }
   \\
   \inferH{Base-Write-AT}{}{
-    \ki \vdash \hoare{\ewriteATPreB}{\ewrite{\rtat}{\loc}{\val}, \proc}{\ewriteATPostB}
+    \ki \vdash \hoare{\ewriteATPreB}{\ewrite{\wtat}{\loc}{\val}, \proc}{\ewriteATPostB}
   }
   \\
   \inferH{Base-Write-NA}{}{
-    \ki \vdash \hoare{\ewriteNAPreB}{\ewrite{\rtna}{\loc}{\val}, \proc}{\ewriteNAPostB}
+    \ki \vdash \hoare{\ewriteNAPreB}{\ewrite{\wtna}{\loc}{\val}, \proc}{\ewriteNAPostB}
   }
   % \\
   % \inferH{Base-CondUpd}{}{
@@ -738,7 +738,7 @@ a processor.
       \CTX{\wf(\fMB',\PSI, \state_T')} \BY \ruleref{lem:write-wellformed}
       \IND
         \RES{\PSOwnPhys}[-\nspace_1] \BY \textbf{Frame} \\
-        \cdline{\ewrite{\rtat}{\loc}{\val}, \proc}
+        \cdline{\ewrite{\wtat}{\loc}{\val}, \proc}
         \setPST{\state_T'} \setPSB{\fMB'} \\
         \RES{\ownPhys{(\PSB, \PSI, \PST)}}[-\nspace_1] 
       \UNIND
@@ -782,7 +782,7 @@ a processor.
       \CTX{\wf(\fMB',\PSI, \state_T')} \BY \ruleref{lem:write-wellformed}
       \IND
         \RES{\PSOwnPhys}[-\nspace_1] \BY \textbf{Frame} \\
-        \cdline{\ewrite{\rtna}{\loc}{\val}, \proc} 
+        \cdline{\ewrite{\wtna}{\loc}{\val}, \proc} 
         \setPST{\state_T'} \setPSB{\fMB'} \\
         \RES{\ownPhys{(\PSB, \PSI, \PST)}}[-\nspace_1] 
       \UNIND
diff --git a/layer1def.tex b/layer1def.tex
index 3a138e59aad7452fa1c7473561a4c9d60fe1abd2..0f181b52a83b561ec500f2cc61920669ba8467a1 100644
--- a/layer1def.tex
+++ b/layer1def.tex
@@ -222,6 +222,9 @@
     % \ast \buf' \futb \buf_0 
     \ast \head(\hist).\weval \neq \val_o
     \ast \lat(\hist', \buf')
+    \ast \Exists \buf_1 \pastb \buf'.
+    \ast \buf_1 \in \hist
+    \mr{\buf'}{\buf_1}
     ))
   \end{array}
 }
diff --git a/na.tex b/na.tex
index ff1ba9e0c96ed5bac3b4405cf5e63b9808094b7d..5ca7dd028423c9abdc67e69917d788b9669a0c8f 100644
--- a/na.tex
+++ b/na.tex
@@ -34,7 +34,7 @@
   \and
   \inferH{Raw-Write}{}{
     \hoare{\lraw(\loc)}
-          {\ewrite{\rtna}{\loc}{\val}}
+          {\ewrite{\wtna}{\loc}{\val}}
           {\lraw(\loc,\Some \val)}} \\
 \end{mathpar}
 
@@ -54,7 +54,7 @@ Follows from \ruleref{Base-Alloc}.
   \pline[\top]{
     \lhist{\loc}{\hist} \ast \lna(\hist,\buf)
     \ast \linfo^{\ffrac}(\loc,\any)}~\\
-  \cdline{\ewrite{\rtna}{\loc}{\val},\proc}~\\
+  \cdline{\ewrite{\wtna}{\loc}{\val},\proc}~\\
   \pline[\top]{\Exists \buf' \futb \buf. 
     \bseen{\proc}{\buf'} 
     \ast \lhist{\loc}{\buf'::\hist}
@@ -125,7 +125,7 @@ We want to support the following rules:
   \and
   \inferH{NA-Frac-Init}{}{
     \hoare{\lraw(\loc)}
-          {\ewrite{\rtna}{\loc}{\val}}
+          {\ewrite{\wtna}{\loc}{\val}}
           {\fracn{\loc}{\ffrac}{\val}}
   }
   \and
@@ -141,7 +141,7 @@ We want to support the following rules:
   \and
   \inferH{NA-Frac-Write}{}{
     \hoare{\fracn{\loc}{\ffrac}{\val}}
-          {\ewrite{\rtna}{\loc}{\val'}}
+          {\ewrite{\wtna}{\loc}{\val'}}
           {\fracn{\loc}{\ffrac}{\val'}}
   }
 \end{mathpar}
@@ -197,7 +197,7 @@ We want to support the following rules:
 
 \begin{hproofenv}
   \pline[\top]{\lraw(\loc)}~\\
-  \cdline{\ewrite{\rtna}{\loc}{\val}}~\\
+  \cdline{\ewrite{\wtna}{\loc}{\val}}~\\
   \pline[\top]{\lraw(\loc,\Some \val)} \by \ruleref{Raw-Write}~\\
   \pline[\top]{\fracn{\loc}{\ffrac}{\val}}\by \ruleref{NA-Raw-Frac}~\\
 \end{hproofenv}
@@ -284,7 +284,7 @@ We want to support the following rules:
       \ownGhost{\gname}{\authfull (\ffrac, \buf_0),\authfrag (\ffrac, \buf_0)}
       \ast \lhist{\loc}{\hist}
       \ast \lna(\hist,\buf)}~\\
-    \cdline{\ewrite{\rtna}{\loc}{\val'},\proc}~\\
+    \cdline{\ewrite{\wtna}{\loc}{\val'},\proc}~\\
     \pline[?]{
       \Exists \buf' \futb \buf. 
       \bseen{\proc}{\buf'} 
diff --git a/rsl/cas.tex b/rsl/cas.tex
index 0cfd8ecac7887d6980580f9e6ec3f4efe32ba79b..e013346500e26b66c0c44c1859761d32bf99adce 100644
--- a/rsl/cas.tex
+++ b/rsl/cas.tex
@@ -73,7 +73,7 @@ Rules in the previous subsection still holds.
   \and
   \inferH{RSL-Raw-Frac-RelRMWAcqInit-Write}{}{
     \hoare{\lraw(\loc) \ast \later P(\val)}
-          {\ewrite{\rtna}{\loc}{\val}}
+          {\ewrite{\wtna}{\loc}{\val}}
           {\relp(\loc,\pfrac_1,P)
             \ast \rmwp(\loc,\pfrac_2,P)
             \ast \initp(\loc,\ffrac-(\pfrac_1 + \pfrac_2))}
@@ -81,7 +81,7 @@ Rules in the previous subsection still holds.
   \and
   \inferH{RSL-Raw-RelRMWAcqInit-Write}{}{
     \hoare{\lraw(\loc) \ast \later P(\val)}
-          {\ewrite{\rtna}{\loc}{\val}}
+          {\ewrite{\wtna}{\loc}{\val}}
           {\relp(\loc,P) \ast \rmwp(\loc,P) \ast \initp(\loc)}
   } \\
 \end{mathpar}
diff --git a/rsl/relacq.tex b/rsl/relacq.tex
index 369575077b4c0a82dabcae187d6165ed87642a37..a4b2a4c288899c0a839c4186679b69a9c23cd2da 100644
--- a/rsl/relacq.tex
+++ b/rsl/relacq.tex
@@ -37,7 +37,7 @@ CAS is added in the next section.
 \begin{align*}
   \epconv(\loc,P,\idPred,\splset) \eqdef{}&
     \All \val_\loc, \buf. 
-      \intr{P(\val_\loc)}(\buf) \Lra 
+      \intr{P(\val_\loc)}(\buf) \iff 
       \bigast_{i \in \splset} \intr{\idPred(i)(\val_\loc)}(\buf) \\
   \ress{\loc}{P}{\idPred}{\splset} \eqdef{}&
     \bigast_{i \in \splset} i \Mapsto \idPred(i)
@@ -138,13 +138,13 @@ return only $C_{i_1}$ and $\idPred(i_1) \equiv \idPred(i)[\val:=\top]$ for later
   \and
   \inferH{RSL-Frac-Rel-Raw-Write}{}{
     \hoare{\relp(\loc,\ffrac,\any)}
-          {\ewrite{\rtat}{\loc}{\val}}
+          {\ewrite{\wtat}{\loc}{\val}}
           {\lraw(\loc,\Some \val)}
   } \\
   \and
   \inferH{RSL-Raw-Frac-RelAcqInit-Write}{}{
     \hoare{\lraw(\loc) \ast \later P(\val)}
-          {\ewrite{\rtna}{\loc}{\val}}
+          {\ewrite{\wtna}{\loc}{\val}}
           {\relp(\loc,\pfrac_1,P)
             \ast \acqp(\loc,\pfrac_2,P)
             \ast \initp(\loc,\ffrac-(\pfrac_1 + \pfrac_2))}
@@ -152,7 +152,7 @@ return only $C_{i_1}$ and $\idPred(i_1) \equiv \idPred(i)[\val:=\top]$ for later
   \and
   \inferH{RSL-Raw-RelAcqInit-Write}{}{
     \hoare{\lraw(\loc) \ast \later P(\val)}
-          {\ewrite{\rtna}{\loc}{\val}}
+          {\ewrite{\wtna}{\loc}{\val}}
           {\relp(\loc,P)\ast \acqp(\loc,P) \ast \initp(\loc)}
   } \\
 \end{mathpar}
@@ -163,7 +163,7 @@ return only $C_{i_1}$ and $\idPred(i_1) \equiv \idPred(i)[\val:=\top]$ for later
 \begin{mathpar}
  \inferH{RSL-Frac-WRel}{}{
     \hoare{\later Q(\val) \ast \relp(\loc,\pfrac_1 + \pfrac_2, Q)}
-          {\ewrite{\rtat}{\loc}{\val}}
+          {\ewrite{\wtat}{\loc}{\val}}
           {\initp(\loc,\pfrac_1) \ast \relp(\loc,\pfrac_2, Q)}} \\
   \and
   \inferH{RSL-Frac-RAcq}{}{
@@ -288,7 +288,7 @@ Similar to the proof of \ruleref{RSL-Frac-Rel-Acq-Subsume}.
     \linfo^{\ffrac}(\loc,\any)
     \ast \lhist{\loc}{\hist} 
     \ast \lat(\hist,\buf)}~\\
-  \cdline{\ewrite{\rtat}{\loc}{\val}}~\\
+  \cdline{\ewrite{\wtat}{\loc}{\val}}~\\
   \pline[\top]{
     \Exists \buf' \futb \buf. \bseen{\proc}{\buf'} 
     \ast \linfo^{\ffrac}(\loc,\any)
@@ -312,7 +312,7 @@ Similar to the proof of \ruleref{RSL-Frac-Rel-Acq-Subsume}.
     \ast \lhist{\loc}{\hist}
     \ast \lna(\hist,\buf)
     \ast \intr{\later P(\val)}(\buf)}~\\
-  \cdline{\ewrite{\rtna}{\loc}{\val}}~\\
+  \cdline{\ewrite{\wtna}{\loc}{\val}}~\\
   \pline[\top]{
     \Exists \buf' \futb \buf. \bseen{\proc}{\buf'} 
     \ast \linfo^{\ffrac}(\loc,\any)
@@ -447,7 +447,7 @@ Similar to the proof of \ruleref{RSL-Frac-Rel-Split} and \ruleref{RSL-Rel-Split}
                           \ast \later \ress{\loc}{P}{\idPred}{\splset}}~\\
         \begin{psubenv}{Frame}
           \pline[-\nspace.\loc]{\lhist{\loc}{\hist}}~\\
-          \cdline{\ewrite{\rtat}{\loc}{\val}, \proc}~\\
+          \cdline{\ewrite{\wtat}{\loc}{\val}, \proc}~\\
           \pline[-\nspace.\loc]{
             \Exists \buf' \futb \buf. \bseen{\proc}{\buf'}
               \ast \lhist{\loc}{\buf'}
@@ -490,7 +490,7 @@ Similar to the proof of \ruleref{RSL-Frac-Rel-Split} and \ruleref{RSL-Rel-Split}
                                 \later\later \intr{\idPred(i)(\buf_0.\weval)}(\buf_0)}~\\
         \begin{psubenv}{Frame}
           \pline[-\nspace.\loc]{\lhist{\loc}{\hist}}~\\
-          \cdline{\ewrite{\rtat}{\loc}{\val}, \proc}~\\
+          \cdline{\ewrite{\wtat}{\loc}{\val}, \proc}~\\
           \pline[-\nspace.\loc]{
             \Exists \buf' \futb \buf. \bseen{\proc}{\buf'}
               \ast \lhist{\loc}{\buf'::\hist}
@@ -625,7 +625,7 @@ Similar to the proof of \ruleref{RSL-Frac-Rel-Split} and \ruleref{RSL-Rel-Split}
     }~\\
     Allocate $i_1 \Mapsto \idPred(i_1), i_2 \Mapsto \idPred(i_2)$ where $i_1,i_2 \notin \splset$,
     $\idPred(i_1), \idPred(i_2)$ are defined as in \ref{sec:readsplit} for $\val_0 \eqdef \val$.
-    It's clear that $\All v, b. \idPred(i)(v)(b) \Lra \idPred(i_1)(v)(b) \ast \idPred(i_2)(v)(b)$.~\\
+    It's clear that $\All v, b. \idPred(i)(v)(b) \iff \idPred(i_1)(v)(b) \ast \idPred(i_2)(v)(b)$.~\\
     Pick $\splset'_1 \eqdef \splset_1 \setminus \set{i} \uplus \set{i_1,i_2},
           \splset'_2 \eqdef \splset_2 \setminus \set{i} \uplus \set{i_1},
           \stsstate' \eqdef (\splset'_1,\splset'_2,\hist)$.~\\
diff --git a/rsl/rslrules.tex b/rsl/rslrules.tex
index c19caaf06854d00d6ee22923c69c7dfee65e4a5d..b12dbb14c0068e42a883cefe7e31c573fc72d470 100644
--- a/rsl/rslrules.tex
+++ b/rsl/rslrules.tex
@@ -9,7 +9,7 @@ We can support the following version of RSL rules:
 \begin{mathpar}
   \inferH{RSL-WRel}{}{
     \hoare{\later Q(\val) \ast \relp(\loc,Q)}
-          {\ewrite{\rtat}{\loc}{\val}}
+          {\ewrite{\wtat}{\loc}{\val}}
           {\initp(\loc) \ast \relp(\loc,Q)}} \\
   \and
   \inferH{RSL-RAcq}{}{