diff --git a/theories/ro.v b/theories/ro.v
index ec404fec146fcf4ae798f43add4a6b4f39aa6e01..657a8edb9624e9bb1fd076819a132b071ae04cf2 100644
--- a/theories/ro.v
+++ b/theories/ro.v
@@ -1,61 +1,36 @@
 From iris.program_logic Require Import weakestpre.
-From igps Require Import proofmode na weakestpre.
+From iris.base_logic Require Import lib.cancelable_invariants.
+From igps Require Import proofmode na weakestpre fractor.
 
 Section RO.
- Context {Σ : gFunctors} `{fG : foundationG Σ}.
+ Context {Σ : gFunctors} `{fG : foundationG Σ} `{cG : cinvG Σ}.
 
- Definition own_loc_ro l v V: vProp Σ := MonPred (λ _, monPred_at (own_loc_prim l {[v, V]}) V)%I _.
+ Definition own_loc_ro l v V : vProp Σ := ⎡∃q, (l ↦{q} v) V⎤%I.
 
- Lemma make_ro l v: own_loc_na l v -∗ ∃V, own_loc_ro l v V ∗ monPred_in V.
+ Lemma ro_split l v V: monPred_in V ∗ own_loc_ro l v V -∗ own_loc_ro l v V ∗ ∃q, l ↦{q} v.
  Proof.
-   rewrite /own_loc_na /own_loc_ro /own_loc_prim valloc_local_eq /valloc_local_def.
    iStartProof (uPred _).
-   iIntros (?) "H"; simpl.
-   iDestruct "H" as (V i) "(% & ? & ?)".
-   destruct H as (? & ? & Heq%elem_of_singleton & ? & ?); inversion Heq; subst.
-   iExists V; iSplit; last done.
-   iExists i; iSplit; last by iFrame.
-   iPureIntro; unfold alloc_local.
-   exists v, V; split; last done.
-   by apply elem_of_singleton.
+   iIntros (i) "[% oL]"; iDestruct "oL" as (q) "oL".
+   iPoseProof (na_frac_split_2 with "oL") as "[oL1 oL2]".
+   iSplitL "oL1"; first by iExists (q/2)%Qp.
+   iDestruct "oL2" as (V') "[??]"; eauto.
  Qed.
 
- Lemma ro_own l v V: own_loc_ro l v V ∗ monPred_in V -∗ own_loc_na l v.
+ Lemma ro_join l v V q' v': own_loc_ro l v V ∗ l ↦{q'} v' ={↑fracN.@l}=∗ own_loc_ro l v V.
  Proof.
-   rewrite /own_loc_na /own_loc_ro /own_loc_prim valloc_local_eq /valloc_local_def.
    iStartProof (uPred _).
-   iIntros (?) "[H %]"; simpl.
-   iDestruct "H" as (i) "(% & ? & ?)"; simpl.
-   iExists V, i; iFrame.
-   iPureIntro; eapply alloc_local_proper; eauto.
- Qed.
- 
- Lemma na_read_ro: ∀ (E : coPset) (l : positive) (v : Z) V,
-    ↑physN ⊆ E →
-    {{{ ⎡PSCtx⎤ ∗ own_loc_ro l (VInj v) V ∗ monPred_in V }}}
-      ([ #l]_na) @ E
-    {{{ z, RET (#z); ⌜z = v⌝ ∗ own_loc_ro l (VInj v) V }}}.
- Proof.
-   intros.
-   rewrite /own_loc_ro /own_loc_prim /= valloc_local_eq /valloc_local_def.
-   rewrite WP_Def.wp_eq /WP_Def.wp_def /bi_affinely.
-   iStartProof (uPred _). iIntros (?) "(#kI & oNA & %)".
-   simpl; iDestruct "oNA" as (i) "(Halloc & oH & oI)".
-   iIntros (Va Ha) "Post". iIntros (? H1 π) "S".
-   setoid_rewrite H1.
-   iDestruct "Halloc" as %Halloc.
-   iApply program_logic.weakestpre.wp_mask_mono;
-      last (iApply (f_read_na with "[$kI $S $oH]")); first auto.
-   - iSplit; iPureIntro;
-       [apply alloc_local_singleton_na_safe|
-        apply alloc_local_singleton_value_init]; by rewrite -H1 -Ha -H0.
-   - iNext. iIntros (v_r V') "(% & $ & oH & % & H)".
-     iDestruct "H" as (V_1) "(% & % & %)".
-     move: H6 => /value_at_hd_singleton [[->] ->].
-     iApply ("Post" $! v_r).
-     iSplit; first done.
-     simpl.
-     iExists _. iFrame "oH oI". iPureIntro.
-     exists (VInj v_r), V_1. by rewrite elem_of_singleton.
- Qed.
+   iIntros (i) "[oL oL']"; iDestruct "oL" as (q) "oL".
+   iExists (q + q')%Qp.
+   iApply (na_frac_join with "[>-]").
+   rewrite /own_loc_na_frac valloc_local_eq /=.
+   iDestruct "oL" as (V0) "[% oL]"; iDestruct "oL'" as (V') "[% oL']".
+(*   iMod (fractor_open with "oL") as (?) "(? & ? & ?)"; first done.*)
+   iAssert (⌜V0 = V'⌝)%I as %?.
+   { admit. }
+   iAssert ⌜v = v'⌝%I as %?.
+   { iPoseProof (fractor_join_l with "[$oL $oL']") as "oL".
+     iDestruct "oL" as (?) "[[%%] _]"; subst.
+     apply encode_inj in H4; inversion H4; done. }
+   subst; iSplitL "oL"; eauto.
+ Admitted.   
 End RO.
\ No newline at end of file