diff --git a/aneris/examples/crdt/statelib/proof/events.v b/aneris/examples/crdt/statelib/proof/events.v
index 91462e29ae135e4b418d7247d4c5516200b2e9b7..2a3d47d509cb447db13519e781ec9b18f2b61f11 100644
--- a/aneris/examples/crdt/statelib/proof/events.v
+++ b/aneris/examples/crdt/statelib/proof/events.v
@@ -1,63 +1,236 @@
-From stdpp Require Import base countable.
+From stdpp Require Import base countable list sets.
 From aneris.aneris_lang Require Import lang.
-From aneris.prelude Require Import time.
+From aneris.prelude Require Import time misc gset_map.
 From aneris.examples.crdt.spec Require Import crdt_time crdt_events.
-From aneris.examples.crdt.statelib.proof Require Import time.
+From aneris.examples.crdt.statelib.proof Require Import utils.
+From aneris.examples.crdt.statelib.time Require Import time maximality.
+
+Lemma set_choose_or_empty
+  {A: Type} {EqDecision0 : EqDecision A} {H : Countable A}
+         (X : gset A):
+  (∃ x : A, x ∈ X) ∨ X = ∅.
+Proof.
+  generalize X. apply set_ind;
+  [ intros?;set_solver | set_solver | ].
+  intros ???[?|?]; left; exists x; set_solver.
+Qed.
 
 (** * Instantiation of Statelib events *)
-(* Section Events. *)
-
-(*   Context `{!Log_Op LogOp}. *)
-
-(*   Record StLibEvent := { *)
-(*     ev_op : LogOp; *)
-(*     ev_orig : RepId; *)
-(*     ev_seqid : SeqNum; *)
-(*     (* valid events should include themselves as dependencies *) *)
-(*     ev_deps : Timestamp; *)
-(*   }. *)
-
-(*   Global Instance oplib_event_eqdec : EqDecision StLibEvent. *)
-(*   Proof. solve_decision. Defined. *)
-
-(*   Global Instance oplib_event_countable : Countable StLibEvent. *)
-(*   Proof. *)
-(*     (* *)
-(*     refine {| *)
-(*       encode ev := encode (ev.(ev_op), ev.(ev_orig), ev.(ev_vc)); *)
-(*       decode n := (λ tr, match tr with *)
-(*                          | (op, orig, vc) => Build_OpLibEvent op orig vc *)
-(*                          end)  <$> *)
-(*                    @decode (LogOp * nat * vector_clock) _ _ n; *)
-(*       |}. *)
-(*     intros []. rewrite /= decode_encode /=. done. *)
-(*   Qed. *) *)
-(*   Admitted. *)
-
-(*   Global Instance oplib_event_timed : Timed StLibEvent := { time := ev_deps }. *)
-
-(*   Global Instance OpLibEvent_LogEvents : Log_Events LogOp := { *)
-(*     Event := OpLibEvent; *)
-(*     EV_Op := ev_op; *)
-(*     EV_Orig := ev_orig; *)
-(*   }. *)
-
-(* End Events. *)
-
-(* Arguments OpLibEvent : clear implicits. *)
-
-(* Section ComputeMaximals. *)
-
-(*   Context `{!Log_Op LogOp}. *)
-
-(*   (* *)
-(*   Global Instance maximals_computing : Maximals_Computing (OpLibEvent LogOp). *)
-(*   Proof. *)
-(*     refine {| Maximals := compute_maximals ev_vc; *)
-(*               Maximum := compute_maximum ev_vc; |}. *)
-(*     - apply (compute_maximals_correct (@ev_vc LogOp)). *)
-(*     - apply compute_maximum_correct. *)
-(*   Qed. *)
-(*   *) *)
-
-(* End ComputeMaximals. *)
+Section Events.
+  Context {Op: Type}.
+  Context `{!EqDecision Op, !Countable Op}.
+  
+  Global Instance stlib_event_eqdec : EqDecision (Event Op).
+  Proof. solve_decision. Defined.
+
+  Global Instance stlib_event_timed : Timed (Event Op) := { time := EV_Time }.
+End Events.
+
+
+Section UsefulFunctions.
+  Context `{Op: Type, !EqDecision Op, !Countable Op}.
+
+  Definition get_seqnum (ev: Event Op) : SeqNum :=
+    size (filter (λ eid: EvId, eid.1 = ev.(EV_Orig)) ev.(EV_Time)).
+
+  Definition get_evid (ev: Event Op) : EvId :=
+    (ev.(EV_Orig), get_seqnum ev).
+
+  Definition depends_on  (ev ev': Event Op) := get_evid ev' ∈ ev.(EV_Time).
+
+  Definition get_deps (e: Event Op): gset EvId := e.(EV_Time).
+  Definition get_deps_set (s: event_set Op) : gset EvId :=
+    gset_flat_map get_deps s.
+
+  Definition fresh_event (s: event_set Op) (op: Op) (orig: RepId): Event Op :=
+      {|
+        EV_Op := op ;
+        EV_Orig := orig ;
+        EV_Time :=
+    match compute_maximum ( filter (λ ev, ev.(EV_Orig) = orig) s ) with
+    | None => get_deps_set s ∪ {[(orig, 1%nat)]}
+    | Some e =>
+      let seen_events := get_deps_set s in
+          seen_events
+          ∪ {[(orig,
+              S (size (filter (λ eid, eid.1 = orig) (get_deps_set s))))]}
+    end
+      |}.
+
+  Definition hproj (i: RepId) (st: event_set Op) :=
+    filter (λ ev, ev.(EV_Orig) = i) st.
+End UsefulFunctions.
+
+
+
+Section EventSets.
+  Context `{Op: Type, !EqDecision Op, !Countable Op}.
+
+  (* A set of events is `dep_closed` if it contains every causal dependency of
+     every element of the set. *)
+  Definition dep_closed (s : gset (Event Op)) : Prop :=
+    ∀ (e: Event Op) (evid: EvId),
+      e ∈ s →
+      evid ∈ e.(EV_Time) →
+      ∃ (e': Event Op), e' ∈ s ∧ get_evid e' = evid.
+
+  Definition events_ext_evid (s: event_set Op) : Prop :=
+    ∀ ev ev', ev ∈ s → ev' ∈ s → get_evid ev = get_evid ev' → ev = ev'.
+
+  Definition events_ext_time (s: event_set Op) : Prop :=
+    ∀ ev ev', ev ∈ s → ev' ∈ s → ev =_t ev' → ev = ev'.
+
+  Definition event_set_same_orig_comparable (st: event_set Op) : Prop :=
+    ∀ e e', e ∈ st → e' ∈ st → e.(EV_Orig) = e'.(EV_Orig) → e <_t e' ∨ e =_t e' ∨ e' <_t e.
+
+  Definition event_set_orig_lt {i: nat} (st: event_set Op) : Prop :=
+    ∀ ev, ev ∈ st → ev.(EV_Orig) < i.
+
+  Definition event_set_orig_deps_seq (st: event_set Op) : Prop :=
+    ∀ (e: Event Op),
+      e ∈ st →
+      ∀ (i: RepId) (sid: nat), O < sid → evid_le (i, sid) (get_evid e) →
+      (i, sid) ∈ e.(EV_Time).
+
+  Definition event_set_orig_max {nb: nat} (st: event_set Op) : Prop :=
+    ∀ (i: RepId), i < nb
+      → hproj i st = ∅ ∨ ∃ m, m ∈ st ∧ compute_maximum (hproj i st) = Some m.
+
+  Definition event_set_evid_mon (st: event_set Op) : Prop :=
+    ∀ ev ev', ev ∈ st → ev' ∈ st → ev.(EV_Orig) = ev'.(EV_Orig) →
+      ev <_t ev' → evid_le (get_evid ev) (get_evid ev').
+
+
+
+  Definition event_set_valid (s : gset (Event Op)) : Prop :=
+    dep_closed s
+    ∧ ∀ (e e': Event Op),
+      e ∈ s → e' ∈ s →
+      ((EV_Orig e = EV_Orig e' → (e ≤_t e' ∨ e' ≤_t e))
+      ∧ (e =_t e' → e = e')).
+
+
+
+  Lemma dep_closed_union (s s' : gset (Event Op)) :
+    dep_closed s -> dep_closed s' -> dep_closed (s ∪ s').
+  Proof.
+    intros Hdc Hdc'  ev eid [Hin|Hin]%elem_of_union Hdep;
+    [ destruct (Hdc ev eid Hin Hdep)
+        as (ev' & Hev'_in%(elem_of_union_l _ s s') & Heq)
+    | destruct (Hdc' ev eid Hin Hdep)
+        as (ev' & Hev'_in%(elem_of_union_r _ s s') & Heq) ];
+    by exists ev'.
+  Qed.
+End EventSets.
+
+Section Events.
+  Context {Op: Type}.
+  Context `{!EqDecision Op, !Countable Op}.
+
+  Definition cc_impl : relation (gset (Event Op)) :=
+    λ s s',
+      ∀ (e e' : Event Op),
+        e ∈ s' → e' ∈ s' →
+        e ≤_t e' ->
+        e' ∈ s →
+        e ∈ s.
+
+  Global Instance cc_impl_refl : Reflexive cc_impl.
+  Proof.
+    intros s e e' Hin Hin' Hlt Hin''.
+    done.
+  Qed.
+
+  Definition cc_subseteq : relation (gset (Event Op)) :=
+    λ s s', s ⊆ s' ∧ cc_impl s s'.
+
+  Global Instance cc_subseteq_preorder : PreOrder cc_subseteq.
+  Proof.
+    split; constructor.
+    - done.
+    - rewrite /cc_impl. eauto.
+    - destruct H as [H _].
+      destruct H0 as [H0 _].
+      set_solver.
+    - destruct H as [Hsub Hy].
+      destruct H0 as [Hsub' Hz].
+      intros e e' Hin Hin' Hle Hinx.
+      assert (e' ∈ y) as He'y by set_solver.
+      assert (e ∈ y) as Hey.
+      { apply (Hz e e'); auto. }
+      apply (Hy e e'); auto.
+  Qed.
+
+  Lemma cc_subseteq_union h h1 h2 :
+    cc_subseteq h1 h -> cc_subseteq h2 h -> cc_subseteq (h1 ∪ h2) h.
+  Proof.
+    intros [Hsub1 Hcc1] [Hsub2 Hcc2].
+    split; [set_solver |].
+    intros e e' Hin Hin' Hle [Hl | Hr]%elem_of_union.
+    - apply elem_of_union_l.
+      apply (Hcc1 e e'); auto.
+    - apply elem_of_union_r.
+      apply (Hcc2 e e'); auto.
+  Qed.
+End Events.
+
+Global Arguments cc_subseteq {_ _ _}.
+
+
+
+Section ComputeMaximumLemams.
+  Context `{Op: Type, !EqDecision Op, !Countable Op}.
+
+  Lemma event_set_maximum_exists (s: event_set Op) (orig: RepId):
+    (∃ e, e ∈ s ∧ e.(EV_Orig) = orig)
+      → event_set_same_orig_comparable s
+      → events_ext_time s
+      → ∃ m, compute_maximum (hproj orig s) = Some m.
+  Proof.
+    intros (e & He_in & He_orig) Hcomp Hext_t.
+    unfold compute_maximum.
+    destruct (set_choose_or_empty (compute_maximals (hproj orig s)))
+      as [(m & [Hm_max [Hm_orig Hm_in]%elem_of_filter]%elem_of_filter) | Hnil].
+    - assert (compute_maximals (hproj orig s) = {[ m ]}) as ->.
+      { apply set_eq. intros n. split.
+        - intros [[Hn_orig Hn_in]%elem_of_filter Hn_max]%compute_maximals_correct.
+          apply elem_of_singleton.
+          specialize Hn_max with m.
+          destruct (Hcomp n m) as [H | [H | H]]; try done.
+          + by rewrite Hn_orig Hm_orig.
+          + by destruct Hn_max; first apply elem_of_filter.
+          + by apply Hext_t.
+          + by destruct (Hm_max n); first apply elem_of_filter.
+        - intros ->%elem_of_singleton.
+          apply elem_of_filter. by split; last apply elem_of_filter. }
+      rewrite elements_singleton.
+      by exists m.
+    - rewrite set_eq -set_equiv compute_maximals_empty set_equiv -set_eq in Hnil.
+      assert (He_in': e ∈ hproj orig s); first by apply elem_of_filter.
+      set_solver.
+  Qed.
+End ComputeMaximumLemams.
+
+
+
+Section UsefulLemmas.
+  Context {Op: Type}.
+  Context `{!EqDecision Op, !Countable Op}.
+
+  Lemma maximals_union (X Y: event_set Op) (x: Event Op):
+    x ∈ compute_maximals (X ∪ Y)
+      → (x ∈ compute_maximals X ∨ x ∈ compute_maximals Y).
+  Proof.
+    intros Hx_in.
+    assert (x ∈ compute_maximals (X ∪ Y))
+      as [H|H]%elem_of_compute_maximals%elem_of_union;
+      first assumption;
+      [left|right];
+      apply compute_maximals_spec in Hx_in as [Hin Hmax];
+      apply compute_maximals_spec; (split; first assumption);
+      intros y Hy;
+      apply Hmax;
+    set_solver.
+  Qed.
+End UsefulLemmas.
+
diff --git a/aneris/examples/crdt/statelib/proof/time.v b/aneris/examples/crdt/statelib/proof/time.v
deleted file mode 100644
index f5e23e096f12bba3fd5ca2cfd4f2053f40735681..0000000000000000000000000000000000000000
--- a/aneris/examples/crdt/statelib/proof/time.v
+++ /dev/null
@@ -1,29 +0,0 @@
-From stdpp Require Import gmap.
-From aneris.examples.crdt.spec Require Import crdt_time.
-
-Section Time.
-
-  Definition RepId := nat.
-  Definition SeqNum := nat.
-  Definition EvId : Type := RepId * SeqNum.
-  Definition Timestamp := gset EvId.
-
-  Definition ts_le (ts1 ts2 : Timestamp) : Prop := ts1 ⊆ ts2.
-
-  Definition ts_lt (ts1 ts2 : Timestamp) : Prop := ts1 ⊂ ts2.
-
-  Global Instance timestamp_time : Log_Time.
-  Admitted.
-  (* TODO
-  Global Instance timestamp_time : Log_Time :=
-    {| Time := vector_clock;
-       TM_le := vector_clock_le;
-       TM_lt := vector_clock_lt;
-       TM_lt_irreflexive := vector_clock_lt_irreflexive;
-       TM_lt_TM_le := vector_clock_lt_le;
-       TM_le_eq_or_lt := vector_clock_le_eq_or_lt;
-       TM_le_lt_trans := vector_clock_le_lt_trans;
-       TM_lt_le_trans := vector_clock_lt_le_trans; |}.
-    *)
-
-End Time.
diff --git a/aneris/examples/crdt/statelib/proof/utils.v b/aneris/examples/crdt/statelib/proof/utils.v
new file mode 100644
index 0000000000000000000000000000000000000000..931ebc0e44c19089191de23860b625945d0a081d
--- /dev/null
+++ b/aneris/examples/crdt/statelib/proof/utils.v
@@ -0,0 +1,41 @@
+From stdpp Require Import gmap.
+From aneris.examples.crdt.spec Require Import crdt_time.
+
+Section Defs.
+
+  Definition RepId := nat.
+  Definition SeqNum := nat.
+  Definition EvId : Type := RepId * SeqNum.
+  Definition Timestamp : Type := gset EvId.
+
+
+  Definition evid_le (ts1 ts2 : EvId) : Prop.
+  Proof.
+    destruct ts1 as [rid sid]; destruct ts2 as [rid' sid'].
+    exact (rid = rid' ∧ (sid ≤ sid')%nat).
+  Defined.
+
+	Global Instance evid_le_refl: Reflexive evid_le.
+  Proof. by intros[]. Qed.
+
+  Global Instance evid_le_trans : Transitive evid_le.
+  Proof.
+    intros [r s][r' s'][r'' s''][-> Hle][<- Hle'].
+    split; [ reflexivity | by apply le_trans with s'].
+  Qed.
+
+  Global Instance evid_le_antisym: AntiSymm eq evid_le.
+  Proof.
+    intros[r s][r' s'] [-> Hle] [Heq Hle'].
+    apply pair_equal_spec; split; [reflexivity | by apply le_antisym].
+  Qed.
+
+	Global Instance evid_le_po: PartialOrder evid_le.
+  Proof. repeat split;  exact _. Qed.
+
+
+
+  Definition evid_lt := strict evid_le.
+
+End Defs.
+
diff --git a/aneris/examples/crdt/statelib/time/evtime.v b/aneris/examples/crdt/statelib/time/evtime.v
new file mode 100644
index 0000000000000000000000000000000000000000..ffabd3fb8a746a0b54aac7cf7984480ac9d62cc7
--- /dev/null
+++ b/aneris/examples/crdt/statelib/time/evtime.v
@@ -0,0 +1,62 @@
+From stdpp Require Import gmap.
+From aneris.aneris_lang Require Import lang resources.
+From aneris.examples.crdt.spec Require Import crdt_time.
+From aneris.examples.crdt.statelib.proof Require Import utils.
+From Coq.Logic Require Import Decidable.
+
+(** Implementation of Log_Time base don the event id (EvId != RepId * SeqNum) *)
+
+Section EVTime.
+  Lemma evid_lt_irreflexive: ∀ x: EvId, ~ evid_lt x x.
+  Proof. intros?[??]; eauto. Qed.
+
+  Lemma evid_lt_trans: ∀ x y z, evid_lt x y → evid_lt y z → evid_lt x z.
+  Proof.
+    intros [rid sid] [rid' sid'] [rid'' sid''] [[-> Hle] Hnle][[<- Hle'] Hnle'].
+    split; first by apply evid_le_trans with (rid', sid').
+    intros [_ Hle_].
+    destruct Hnle. split; [ reflexivity | by apply le_trans with sid'' ].
+  Qed.
+
+  Lemma evid_lt_TM_le: ∀ x x', evid_lt x x' → evid_le x x'.
+  Proof. by intros ??[? _]. Qed.
+
+  Lemma evid_le_eq_or_lt: ∀ x x', evid_le x x' → x = x' ∨ evid_lt x x'.
+  Proof.
+    intros[rid sid][rid' sid'][-> Hle].
+    apply le_lt_or_eq in Hle as [Hlt | ->]; [right | left]; last reflexivity.
+    split; first (split; [ reflexivity | lia]).
+    intros [_ Hle]. lia.
+  Qed.
+
+  Lemma evid_le_lt_trans: 
+    ∀ t t' t'' : EvId,
+      evid_le t t' → evid_lt t' t'' → evid_lt t t''.
+  Proof. exact strict_transitive_r. Qed.
+
+  Lemma evid_lt_le_trans: 
+    ∀ t t' t'' : EvId,
+      evid_lt t t' → evid_le t' t'' → evid_lt t t''.
+  Proof. exact strict_transitive_l. Qed.
+
+	Global Instance evid_lt_asym: Asymmetric evid_lt.
+  Proof.
+    intros[r s][r' s'] [[-> Hle] Hnle][[Heq Hle'] Hnle'].
+    by apply Hnle.
+	Qed.
+
+  Global Instance eviq_time : Log_Time :=
+    {| Time := EvId;
+       TM_le := evid_le;
+       TM_le_PO := evid_le_po;
+       TM_lt := evid_lt;
+       TM_lt_irreflexive := evid_lt_irreflexive;
+       TM_lt_trans := evid_lt_trans;
+       TM_le_eq_or_lt := evid_le_eq_or_lt;
+       TM_lt_TM_le := evid_lt_TM_le;
+       TM_le_lt_trans := evid_le_lt_trans;
+       TM_lt_le_trans := evid_lt_le_trans
+    |}.
+
+End EVTime.
+
diff --git a/aneris/examples/crdt/statelib/time/maximality.v b/aneris/examples/crdt/statelib/time/maximality.v
new file mode 100644
index 0000000000000000000000000000000000000000..62e26c0c9e2df38c95f79bf38ca6afeec0d96730
--- /dev/null
+++ b/aneris/examples/crdt/statelib/time/maximality.v
@@ -0,0 +1,351 @@
+From stdpp Require Import base gmap.
+From aneris.prelude Require Import misc.
+From aneris.examples.crdt.spec Require Import crdt_time.
+
+Lemma set_choose_or_empty
+  {A: Type} {EqDecision0 : EqDecision A} {H : Countable A}
+         (X : gset A):
+  (∃ x : A, x ∈ X) ∨ X = ∅.
+Proof.
+  generalize X. apply set_ind;
+  [ intros?;set_solver | set_solver | ].
+  intros ???[?|?]; left; exists x; set_solver.
+Qed.
+
+Section ComputeMaximals.
+  Context {T: Type}.
+  Context `{
+      !EqDecision T, !Countable T,
+      !Log_Time, !Timed T,
+      !RelDecision TM_lt}.
+
+  Definition compute_maximals (g: gset T): gset T :=
+    filter
+      (λ (x: T), set_Forall (λ (y: T), ¬  x <_t y) g) g.
+  
+  Definition compute_maximum (g: (gset T)): option T:=
+    match elements (compute_maximals g) with
+    | h :: [] => Some h
+    | _ => None
+    end.
+
+
+
+  Lemma set_singleton_elements
+    (X : gset T) (x: T):
+    elements X = [x] ↔ X = {[x]}.
+  Proof.
+    split.
+    - intros Helem.
+      apply set_eq. intros y.
+      split; intros Hy.
+      + apply elem_of_elements.
+        by rewrite elements_singleton, <-Helem, elem_of_elements.
+      + apply elem_of_elements.
+        by rewrite <-elem_of_elements, elements_singleton, <-Helem in Hy.
+    - intros Helem. by rewrite Helem, elements_singleton.
+  Qed.
+
+
+
+  Lemma compute_maximals_correct
+    (X : gset T): is_maximals X (compute_maximals X).
+  Proof.
+    pattern X. apply set_ind;
+    [intros ???; set_solver |
+      (split; [ set_solver | ]; by intros [? _]) |].
+    intros y Y Hy Hmax.
+    intros z. split; intros Hz.
+    - apply elem_of_filter in Hz as [Hz_forall Hz_in].
+      split; [ exact Hz_in |].
+      intros t Hi_in. by apply Hz_forall.
+    - apply elem_of_filter. split; by destruct Hz.
+  Qed.
+
+  (** The folliwing are usefull lemmas, most required for the proof of
+    [compute_maximum_correct] (conferre below) *)
+  Lemma elem_of_compute_maximals
+    (X : gset T) (x: T):
+    x ∈ compute_maximals X → x ∈ X.
+  Proof. unfold compute_maximals. rewrite elem_of_filter. by intros [_ ?]. Qed.
+
+  Lemma compute_maximals_spec_1 (g: gset T) (ev: T):
+    ev ∈ (compute_maximals g) →
+      ev ∈ g ∧ ∀ ev', (ev' ∈ g → ¬ ev <_t ev').
+  Proof.
+    intros Hev_in%elem_of_filter.
+    by destruct Hev_in as [Hv_max Hev_in].
+  Qed.
+
+  Lemma compute_maximals_spec_2 (g: gset T) (ev: T):
+    ev ∈ g → (∀ ev', (ev' ∈ g → ¬ ev <_t ev'))
+      → ev ∈ (compute_maximals g).
+  Proof.
+    intros Hev_in Hev_max.
+    apply elem_of_filter.
+    split; [| exact Hev_in].
+    intros x Hx_in. by apply Hev_max.
+  Qed.
+
+  Lemma compute_maximals_spec (g: gset T) (ev: T):
+    ev ∈ (compute_maximals g) ↔ (ev ∈ g ∧ ∀ ev', (ev' ∈ g → ¬ ev <_t ev')).
+  Proof.
+    split.
+    - apply compute_maximals_spec_1.
+    - intros [??]; by apply compute_maximals_spec_2.
+  Qed.
+
+
+  Lemma find_one_maximal_in_compute_maximals
+    (g: gset T) (x: T):
+    x ∈ g
+      → find_one_maximal (fun a => time a) TM_lt x (elements g)
+        ∈ (compute_maximals g).
+  Proof.
+    (** TODO: remove this assertion *)
+    assert (Hrex: ∀ a b, TM_lt a b → TM_lt b a → False);
+      first apply TM_lt_exclusion.
+    (**)
+    intros Hxl.
+    apply compute_maximals_spec_2;
+      first by destruct ( find_one_maximal_eq_or_elem_of (fun a => time a) TM_lt x
+        (elements g)) as [Hyp|Hyp%elem_of_elements]; first by rewrite Hyp.
+    intros ev' Hev'l%elem_of_elements Hneg.
+    by apply (find_one_maximal_maximal (fun a => time a) TM_lt TM_le
+      TM_lt_TM_le TM_le_eq_or_lt TM_lt_irreflexive Hrex TM_le_lt_trans
+      x (elements g) ev').
+  Qed.
+
+  Lemma compute_maximals_nin' (g: gset T) (x: T):
+    g ≠ ∅ → x ∈ g →
+    x ∉ compute_maximals g → ∃ y, y ∈ g ∧ ¬ y <_t x.
+  Proof.
+    intros Hnempty Hx_in Hx_nin.
+    exists (find_one_maximal (λ a, time a) TM_lt x (elements g));
+    pose (find_one_maximal_in_compute_maximals g x Hx_in) as Hfm;
+    apply compute_maximals_correct in Hfm as [Hin Hmax].
+    split; first assumption.
+    by apply Hmax.
+  Qed.
+
+  Lemma compute_maximals_nin (g: gset T) (x: T):
+    x ∉ (compute_maximals ({[x]} ∪ g))
+    → compute_maximals ({[x]} ∪ g) = compute_maximals g.
+  Proof.
+    intros Hx_nin.
+    assert (HnP: ¬ set_Forall (λ y, ¬ x <_t y) ({[x]} ∪ g)).
+    { unfold compute_maximals in Hx_nin; rewrite elem_of_filter in Hx_nin.
+      intros Hyp. apply Hx_nin.
+      split; set_solver. }
+    apply set_eq. intros y. split.
+    - intros [[->%elem_of_singleton|Hy_in]%elem_of_union Hy_max]%compute_maximals_correct.
+      + exfalso. destruct HnP. intros?. by apply Hy_max.
+      + apply compute_maximals_correct. split; [ assumption |].
+        intros z Hz_in. apply Hy_max. set_solver.
+    - intros [Hy_in Hy_max]%compute_maximals_correct.
+      apply compute_maximals_correct. split; [ set_solver |].
+      intros ev [->%elem_of_singleton|Hev]%elem_of_union;
+        [| by apply Hy_max].
+      intros Himp.
+      destruct  Hx_nin.
+      apply compute_maximals_spec_2;
+        first by apply elem_of_union_l, elem_of_singleton.
+      intros e [->%elem_of_singleton | He_in]%elem_of_union;
+        first by apply TM_lt_irreflexive.
+      intros Hlt. apply (Hy_max e); first assumption.
+      by apply TM_lt_trans with (time x).
+  Qed.
+
+
+
+  Lemma compute_maximals_empty (X: gset T):
+    compute_maximals X ≡ ∅ ↔ X ≡ ∅.
+  Proof.
+    generalize X; apply set_ind; [(intros?; set_solver)|set_solver|].
+    intros x Y Hw_nin HY_empty_iff. split; last set_solver.
+    intros Hyp. exfalso.
+    assert (H': x ∉ compute_maximals ({[x]} ∪ Y));
+      try by rewrite Hyp.
+    rewrite compute_maximals_nin in Hyp; try exact H'.
+    apply H', elem_of_filter. 
+    split; last set_solver.
+    intros x'.
+    intros [->%elem_of_singleton | Hx'_in]%elem_of_union.
+    - by apply TM_lt_irreflexive.
+    - by replace Y with (∅: gset T) in *; last set_solver.
+  Qed.
+
+  Lemma compute_maximals_bigger (g: gset T) (ev: T):
+    ev ∈ g → ∃ maxev, maxev ∈ (compute_maximals g) ∧ ev ≤_t maxev.
+  Proof.
+    intros Hev_in.
+    destruct (set_choose_or_empty g) as [eqn|eqn];
+      last (apply compute_maximals_empty in Hev_in; set_solver).
+    exists (find_one_maximal (fun a => time a) TM_lt ev (elements g)).
+    split; first by apply find_one_maximal_in_compute_maximals.
+    apply (find_one_maximal_rel (λ a, time a) TM_lt TM_le).
+    apply TM_lt_TM_le.
+  Qed.
+
+  Lemma compute_maximum_correct:
+    ∀ X : gset T,
+      (∀ x y : T, x ∈ X → y ∈ X → x =_t y → x = y)
+      → ∀ x : T, compute_maximum X = Some x ↔ is_maximum x X.
+  Proof.
+    intros g Hmaxeq x. split; intros Hmax.
+    - unfold compute_maximum in Hmax.
+      assert (Heq: compute_maximals g = {[x]}).
+      { destruct (set_choose_or_empty (compute_maximals g)) as [eqn|eqn];
+          last by rewrite eqn in Hmax.
+        destruct (elements (compute_maximals g)) as [|h t] eqn:E1;
+          [|destruct t eqn:E2]; try done.
+        apply set_singleton_elements. by simplify_eq. } clear Hmax.
+      assert (Hin: x ∈ g).
+      { apply elem_of_compute_maximals. set_solver. }
+      split; first assumption.
+      intros t Htin Htne.
+      destruct (compute_maximals_bigger g t Htin) as (y & Hyn & Hle_ty).
+      rewrite Heq in Hyn. apply elem_of_singleton in Hyn. simplify_eq.
+      by apply TM_le_eq_or_lt in Hle_ty as [Heq_ty| Hlt_ty];
+      first by rewrite (Hmaxeq t x Htin Hin Heq_ty) in Htne.
+    - unfold compute_maximum. destruct Hmax as [Hin Hlt].
+      destruct (elements (compute_maximals g)) eqn: E.
+      { apply elements_empty_inv in E.
+        rewrite compute_maximals_empty in E. set_solver. }
+      destruct l.
+      * f_equal.
+        assert (x ∈ compute_maximals g) as Hxin%elem_of_elements.
+        { assert (t ∈ compute_maximals g)
+            as [Ht_in Ht_max]%compute_maximals_correct;
+            last assert (x = t) as ->.
+          - apply elem_of_elements. rewrite E. apply elem_of_list_here.
+          - destruct (decide(x = t)); first done.
+            apply Hmaxeq; try done.
+            destruct (Ht_max x Hin).
+            by apply Hlt.
+          - apply elem_of_elements. rewrite E. apply elem_of_list_here. }
+        rewrite E in Hxin. set_solver.
+      * exfalso. (** replace s ans s0 with x*)
+        assert (H1: t ∈ elements (compute_maximals g)).
+        { rewrite E. apply elem_of_list_here. }
+        assert (H2: t0 ∈ elements (compute_maximals g)).
+        { rewrite E. apply elem_of_list_further, elem_of_list_here. }
+        destruct (compute_maximals_spec_1 g t)
+          as [Hsing Hs]; first by apply elem_of_elements in H1.
+        destruct (compute_maximals_spec_1 g t0)
+          as [Hs0ing Hs0]; first by apply elem_of_elements in H2.
+        apply (Hs x); first assumption.
+        apply (Hlt t); first assumption.
+        intros Hsx.
+        apply (Hs0 x); first assumption.
+        apply (Hlt t0); first assumption.
+        intros Hs0x.
+        simplify_eq.
+        pose (NoDup_elements (compute_maximals g)) as Hyp.
+        replace (elements (compute_maximals g)) with (x :: x :: l) in Hyp.
+        apply NoDup_cons_1_1 in Hyp.
+        apply Hyp, elem_of_list_here.
+  Qed.
+
+
+
+  Global Instance maximals_computing : Maximals_Computing T:=
+    {|
+        Maximals := λ g, compute_maximals g;
+        Maximum := λ g, compute_maximum g;
+        Maximals_correct := compute_maximals_correct;
+        Maximum_correct := compute_maximum_correct |}.
+End ComputeMaximals.
+
+Section UsefulLemmas.
+  Context {T: Type}.
+  Context `{
+      !EqDecision T, !Countable T,
+      !Log_Time, !Timed T,
+      !RelDecision TM_lt}.
+
+  Lemma maximals_union (X Y: gset T) (x: T):
+    x ∈ compute_maximals (X ∪ Y)
+      → (x ∈ compute_maximals X ∨ x ∈ compute_maximals Y).
+  Proof.
+    intros Hx_in.
+    assert (x ∈ compute_maximals (X ∪ Y))
+      as [Hyp|Hyp]%elem_of_compute_maximals%elem_of_union;
+      first assumption;
+      [left|right];
+      apply compute_maximals_spec in Hx_in as [Hin Hmax];
+      apply compute_maximals_spec; (split; first assumption);
+      intros y Hy;
+      apply Hmax;
+    set_solver.
+  Qed.
+
+  Lemma compute_maximum_empty:
+    compute_maximum (∅: gset T) = None.
+  Proof. reflexivity. Qed.
+
+  Lemma compute_maximals_simgleton (t: T):
+    compute_maximals ({[ t ]}: gset T) = ({[ t ]}: gset T).
+  Proof.
+    unfold compute_maximals.
+    apply set_eq.
+    intros x; split.
+    - by intros [_ Hx_in]%elem_of_filter.
+    - intros ->%elem_of_singleton.
+      apply elem_of_filter; split.
+      + intros y ->%elem_of_singleton. apply TM_lt_irreflexive.
+      + by apply elem_of_singleton.
+  Qed.
+
+  Lemma compute_maximum_simgleton (t: T):
+    compute_maximum {[ t ]} = Some t.
+  Proof.
+    unfold compute_maximum.
+    by rewrite compute_maximals_simgleton, elements_singleton.
+  Qed.
+
+  Lemma compute_maximals_non_empty {X: gset T} {x: T}
+    (_: x ∈ X): compute_maximals X ≠ ∅.
+  Proof.
+    intros Hcm_empty.
+    pose proof (compute_maximals_empty X).
+    set_solver.
+  Qed.
+
+  Lemma set_singleton_eq (X: gset T) (x: T):
+    (x ∈ X ∧ (∀ y, y ∈ X → y = x)) ↔ X = {[ x ]}.
+  Proof. set_solver. Qed.
+
+  Lemma compute_maximum_non_empty (X: gset T):
+    (∀ (x y: T), x ∈ X → y ∈ X → x <_t y ∨ x =_t y ∨ y <_t x)
+    → (∀ (x y: T), x ∈ X → y ∈ X → x =_t y → x = y)
+    → (X ≠ ∅ ↔ (∃ (m: T), compute_maximum X = Some m)).
+  Proof.
+    intros Hcomp Hext. split.
+    - intros [m Hm_in]%set_choose_L.
+      pose proof (compute_maximals_non_empty Hm_in) as [o [Ho_in Ho_max]%compute_maximals_correct]%set_choose_L.
+      exists o.
+      unfold compute_maximum.
+      assert (compute_maximals X = {[ o ]}) as ->.
+      { apply set_singleton_eq.
+        split; first by apply compute_maximals_correct.
+        intros n [Hn_in Hn_max]%compute_maximals_correct.
+        pose proof (Hcomp o n Ho_in Hn_in) as [Himp | [Heq | Himp]].
+        - exfalso. by apply (Ho_max n).
+        - by apply Hext.
+        - exfalso. by apply (Hn_max o). }
+      by rewrite elements_singleton.
+    - intros [m [Hm_in Hm_max]%compute_maximum_correct];
+        first set_solver.
+      exact Hext.
+  Qed.
+
+  Lemma compute_maximum_empty' `{!LeibnizEquiv (gset T)} :
+    compute_maximum (∅: gset T) = None.
+  Proof.
+    unfold compute_maximum, compute_maximals.
+    rewrite filter_empty_L; last assumption.
+    by rewrite elements_empty.
+  Qed.
+End UsefulLemmas.
+
diff --git a/aneris/examples/crdt/statelib/time/time.v b/aneris/examples/crdt/statelib/time/time.v
new file mode 100644
index 0000000000000000000000000000000000000000..374d392817808641e5f665380375e8cc71dc6eeb
--- /dev/null
+++ b/aneris/examples/crdt/statelib/time/time.v
@@ -0,0 +1,56 @@
+From stdpp Require Import gmap.
+From aneris.examples.crdt.spec Require Import crdt_time.
+From aneris.examples.crdt.statelib.proof Require Import utils.
+
+Section Time.
+  Definition ts_le (ts1 ts2 : Timestamp) : Prop :=
+    ts1 ⊆ ts2.
+
+  Definition ts_lt := strict ts_le.
+
+  Lemma ts_lt_irreflexive: ∀ x: Timestamp, ~ ts_lt x x.
+  Proof. by intros s [H H']. Qed.
+  Lemma ts_lt_trans: ∀ x y z, ts_lt x y → ts_lt y z → ts_lt x z.
+  Proof. set_solver. Qed.
+  Lemma ts_lt_TM_le: ∀ x x', ts_lt x x' → ts_le x x'.
+  Proof. exact strict_include. Qed.
+
+  Lemma ts_le_eq_or_lt: ∀ x x', ts_le x x' → x = x' ∨ ts_lt x x'.
+  Proof.
+    intros ???.
+    destruct (set_subseteq_inv x x' H);
+    [by right | left; by apply set_eq].
+  Qed.
+
+  Lemma ts_le_lt_trans: 
+    ∀ t t' t'' : Timestamp,
+                       ts_le t t' → ts_lt t' t'' → ts_lt t t''.
+  Proof. set_solver. Qed.
+
+  Lemma ts_lt_le_trans: 
+    ∀ t t' t'' : Timestamp,
+                       ts_lt t t' → ts_le t' t'' → ts_lt t t''.
+  Proof. set_solver. Qed.
+
+  Global Instance ts_le_trans: Transitive ts_le.
+  Proof. intros?. set_solver.  Qed.
+  Global Instance ts_le_refl: Reflexive ts_le.
+  Proof. intros ?. set_solver.  Qed.
+
+  Global Instance ts_lt_asym: Asymmetric ts_lt.
+  Proof. intros?. set_solver. Qed.
+
+  Global Instance timestamp_time : Log_Time :=
+    {| Time := Timestamp;
+       TM_le := ts_le;
+       TM_le_PO := set_subseteq_partialorder;
+       TM_lt := ts_lt;
+       TM_lt_irreflexive := ts_lt_irreflexive;
+       TM_lt_trans := ts_lt_trans;
+       TM_le_eq_or_lt := ts_le_eq_or_lt;
+       TM_lt_TM_le := ts_lt_TM_le;
+       TM_le_lt_trans := ts_le_lt_trans;
+       TM_lt_le_trans := ts_lt_le_trans
+    |}.
+
+End Time.