diff --git a/docs/atomic.pdf b/docs/atomic.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..118d0812e2b21877c37ede777935ca9593297369
Binary files /dev/null and b/docs/atomic.pdf differ
diff --git a/docs/flat.md b/docs/flat.md
deleted file mode 100644
index 08c962097ab70723c87f8412cdb9cb52d4c2e9f9..0000000000000000000000000000000000000000
--- a/docs/flat.md
+++ /dev/null
@@ -1,82 +0,0 @@
-Flat combiner
-=====
-
-The flat combiner proofs is based on three major components:
-
-1. Extensive use of *evidence map*, a general implementation of a heap-like structure
-2. treiber's stack with per-item invariants
-3. helping protocols encoded by exclusive monoids
-
-## Evidence map
-
-The idea is to simulate the heap we already have -- but generalize `loc` as `K` and `val` as `V`. So we can break down the fragmental ownerships, establish agreement over the `K`'s value etc. It is called that way because its generality and a definition called `ev`, which existentially equalifies over the fraction thus serves as kind of a duplicable evidence of existence of some agreed value pointed by certain key.
-
-Concretely:
-
-$$EvMap(K, V) = AUTH(FINMAP(K, FRAC \times AG(V)))$$
-
-$$ev_\gamma(k, v) = \exists q, own_\gamma(\circ \{ k \mapsto (q, Agree(v))\})$$
-
-## Treiber's stack
-
-This stack contains all the "slots" that are used as a location pointing to request/response.
-
-The stack has two layer of specification: The first layer is logically atomic triple style spec, containing `push`, and `pop`. The second layer is built on top of first layer, featuring a global, per-item invariant; it has `push`, and `iter`.
-
-It is also built with the evidence map.
-
-So here is the point:
-
-1. `iter` doesn't have an atomic spec because the implementation just traverses along the link and doesn't enforce any atomicity, for example, guaranteeing that the traversed nodes will stay the same etc.
-2. `pop` doesn't have an invariant spec because the invariant is based the model of immutable sharing, thus we can only *know* that some `R` holds for certain element, but we can't get this `R` into local state (since we can't shrink the `evmap` simply by giving an `ev`).
-
-Here are the specs:
-
-### constructor
-
-$$\{ \top \} new\_stack \{s, is\_stack(s) \}$$
-
-### atomic ones
-
-push
-
-$$\langle xs, hd. s \mapsto \#hd* is\_list(hd, xs) \rangle \\
-  push(\#s, x) \\
-  \langle ret. ret = \#() \land \exists hd', s \mapsto \#hd'* hd' \mapsto SOME(x, \#hd) * is\_list(hd, xs) \rangle$$
-
-pop
-
-$$\langle xs, hd. s \mapsto \#hd* is\_list(hd, xs) \rangle \\
-  pop(\#s, x) \\
-  \langle ret. (ret = NONE \land xs = [] * s \mapsto \#hd * is\_list(hd, [])) \lor \\
-               (\exists x, xs', hd'.ret = SOME(x) \land xs = x::xs' * s \mapsto \#hd' * hd \mapsto_q SOME(x, \#hd') * is\_list(hd', xs'))\rangle$$
-
-### invariant ones
-
-
-## Protocol
-
-The protocol is based on the previous prototype of a simple helping example. The major difference is:
-
-1. Some of the ghost names are per-item, thus existentially packed inside the per-item invariant of the stack;
-2. One ghost name is global and locked, which will be used my the *sole* server.
-3. The precondition and post-condition are global, arbitrary timeless conditions that qualify over request. A frame `R` is also added to implement the syncer style spec.
-
-![](st.png)
-
-## Problems
-
-The major problem is current flat combiner spec qualifies over a fixed `P` and `Q` in the syncer style spec I derived, which is much more restricted than the universally qualified version. 
-
-The reason why this happens is simple: The `P Q` are encoded as part of the per-item invariant, that is to say, we enforce that for each item the `P, Q` in its state transitions are all the same.
-
-I tried to encode any `P Q` and a hoare triple involving `P, Q, f` inside the *INSTALLED* state. But it seems difficult to confirm that the final `y` satisfies the same `Q`: because when we installed `Q`, we know what `Q` is, but when it is installed, it is existentially qualified, and same till the time of $FINISHED$ state. Thus, when we open the $\exists Q, Q(x, y)$, we don't know if $Q' = Q$.
-
-
-## Stat
-
-`flat.v`: 440 lines, 1 minute and 30 seconds.
-
-`treiber_stack.v`: 450 lines
-
-`misc.v`: 200 lines
diff --git a/docs/st.png b/docs/st.png
deleted file mode 100644
index 94e39fe4f50f58c9bfc28d0dbc79950b4f118f13..0000000000000000000000000000000000000000
Binary files a/docs/st.png and /dev/null differ