Library iris.program_logic.refine_raw

From iris.prelude Require Export set irelations natmap mapset.
From iris.algebra Require Import dra cmra_tactics.
From iris.program_logic Require Import language wsat adequacy_inf.
Local Hint Extern 10 ( _) ⇒
  repeat match goal with
  | H : wsat _ _ _ _ _ |- _apply wsat_valid in H; last omega
  end; solve_valid.
Local Hint Extern 10 (✓{_} _) ⇒
  repeat match goal with
  | H : wsat _ _ _ _ _ |- _apply wsat_valid in H; last omega
  end; solve_validN.

Section refine_dra.
Context (Λ: language).
Context (K: nat).

Inductive refine_view : Set :=
  | master
  | snapshot.

Definition max_view (v1 v2: refine_view) :=
  match v1, v2 with
  | master, _master
  | _, mastermaster
  | _, _snapshot
  end.

Instance assoc_max_view: Assoc (=) max_view.
Proof.
  intros [|] [|] [|]; auto.
Qed.

Instance comm_max_view: Comm (=) max_view.
Proof.
  intros [|] [|]; auto.
Qed.

Record refine_car Λ' (K': nat) : Type := Refine { view: refine_view;
                                     tids: natset;
                                     cfgs: list (cfg Λ');
                                     idxs: list (nat) }.
Notation refine_car' := (refine_car Λ K).
Arguments view {_ _} _.
Arguments cfgs {_ _} _.
Arguments tids {_ _} _.
Arguments idxs {_ _} _.
Arguments Refine {_ _} _ _ _ _.

Implicit Type cs : list (cfg Λ).

Inductive valid_cfg_idx_seq: list (cfg Λ) list nat Prop :=
  | valid_ci_nil: valid_cfg_idx_seq [] []
  | valid_ci_single c: valid_cfg_idx_seq [c] []
  | valid_ci_step c c' cs i idxs:
      idx_step i c c'
      valid_cfg_idx_seq (c' :: cs) idxs
      valid_cfg_idx_seq (c :: c' :: cs) (i :: idxs).

Global Instance refine_equiv : Equiv (refine_car') := (=).
Global Instance refine_equivalence: Equivalence ((≡) : relation (refine_car')).
Proof. by split; eauto with ×. Qed.
Global Instance refine_leibniz: LeibnizEquiv refine_car'.
Proof. by intro. Qed.

Instance refine_valid : Valid (refine_car') :=
  λ r, (match last (cfgs r) with
          | Nonetids r
          | Some c i, i (tids r) i < length (fst c)
        end)
       (valid_cfg_idx_seq (cfgs r) (idxs r)).
Instance refine_core : Core (refine_car') :=
  λ r, Refine snapshot (cfgs r) (idxs r).
Definition prefix_of_valid_seq (t1: natset) cs1 is1 cs2 is2 :=
  prefix_of cs1 cs2 isext, is2 = is1 ++ isext ( i, i t1 ¬ i isext).

Inductive refine_disjoint : Disjoint (refine_car') :=
  | snap_snap_disjoint t1 t2 cs1 cs2 is1 is2 :
     t1 t2
     (prefix_of_valid_seq t1 cs1 is1 cs2 is2 prefix_of_valid_seq t2 cs2 is2 cs1 is1)
     Refine snapshot t1 cs1 is1 Refine snapshot t2 cs2 is2
  | snap_master_disjoint t1 t2 cs1 cs2 is1 is2:
     t1 t2 ( i, i t1 ¬ (i is2))
     Refine snapshot t1 cs1 is1 Refine master t2 (cs1 ++ cs2) (is1 ++ is2)
  | master_snapshot_disjoint t1 t2 cs1 cs2 is1 is2:
     t1 t2 ( i, i t1 ¬ (i is2))
     Refine master t2 (cs1 ++ cs2) (is1 ++ is2) Refine snapshot t1 cs1 is1.
Existing Instance refine_disjoint.

Instance refine_op : Op (refine_car') := λ r1 r2,
  match le_dec (length (cfgs r1)) (length (cfgs r2)) with
  | left _Refine (max_view (view r1) (view r2))
                   (tids r1 tids r2) (cfgs r2) (idxs r2)
  | right _Refine (max_view (view r1) (view r2))
                   (tids r1 tids r2) (cfgs r1) (idxs r1)
  end.


Inductive refine_step : Step (refine_car') :=
 | snap_block_step t1 t2 cs1 cs2 c1 c2 is1 is2:
      valid_cfg_idx_seq ([c1] ++ cs2 ++ [c2]) is2
      ( i, i t1 (i is2 ¬ (enabled idx_step c2 i)))
      ( i, i t1 (count_occ (nat_eq_dec) is2 i K))
      ( i, i is2 i t1)
      ( i, i t2 (length (fst c1) i length (fst c2) > i))
      Refine snapshot t1 (cs1 ++ [c1]) is1
      Refine snapshot (t1 t2) (cs1 ++ [c1] ++ cs2 ++ [c2]) (is1 ++ is2)
 | snap_spec_step t1 t2 cs1 c1 cspec cs2 is1 ispec is2:
      valid_cfg_idx_seq ([c1] ++ cspec) ispec
      ( i, i ispec i t1)
      (Refine snapshot t1 (cs1 ++ [c1] ++ cspec) (is1 ++ ispec)
       Refine snapshot t2 cs2 is2)
      Refine snapshot t1 (cs1 ++ [c1]) is1
      Refine snapshot t2 cs2 is2.

Existing Instance refine_step.

Lemma last_ne {A} (a: A) (l: list A):
  ¬ (last (a :: l) = None).
Proof.
  revert a; induction l; auto.
  intros a'. specialize (IHl a'); simpl in ×.
  destruct l; auto.
Qed.

Lemma length_le_last_none {A} (l1 l2: list A):
  length l1 length l2 last l2 = None last l1 = None.
Proof.
  intros.
  destruct l2.
  × destruct l1; auto; simpl in *; omega.
  × exfalso. eapply last_ne; eauto.
Qed.

Lemma valid_seq_tp_monotone_hd c c' cs1 is1:
  valid_cfg_idx_seq (c :: c' :: cs1) is1
  length (fst c) length (fst c').
Proof.
  inversion 1. subst.
  eapply length_cfg_idx_step; eauto.
Qed.

Lemma valid_seq_app cs1 cs2 ixs:
  valid_cfg_idx_seq (cs1 ++ cs2) ixs
   ixs1 ixs2, ixs1 ++ ixs2 = ixs valid_cfg_idx_seq cs2 ixs2.
Proof.
  revert cs2 ixs.
  induction cs1; intros cs2 ixs Hval.
  - [], ixs. auto.
  - simpl in Hval. inversion Hval as [ | | c c' cs i idxs ? ? (Heq1&Heq2) Heq3].
    × assert (cs1 = [] cs2 = []) as (?&?) by (eapply app_eq_nil; eauto).
      subst; [], []; split; auto.
      econstructor.
    × edestruct (IHcs1 cs2 idxs) as (ixs1&ixs2&?&?); eauto.
       { subst. rewrite -Heq2; eauto. }
        (i :: ixs1), ixs2. split; auto.
       simpl. f_equal. auto.
Qed.

Lemma valid_seq_tp_monotone_mid c c' cs1 cs2 cs3 ixs:
  valid_cfg_idx_seq (cs1 ++ [c] ++ cs2 ++ [c'] ++ cs3) ixs
  length (fst c) length (fst c').
Proof.
  revert cs1 cs3 ixs c c'.
  induction cs2 as [ | c0 cs2].
  - simpl; intros cs1 cs3 ixs c c' (?&?&?&?)%valid_seq_app.
    eapply valid_seq_tp_monotone_hd; eauto.
  - simpl; intros cs1 cs3 ixs c c' Hval.
    transitivity (length (c0.1)).
    × apply valid_seq_app in Hval as (?&?&?&?). eapply valid_seq_tp_monotone_hd; eauto.
    × eapply (IHcs2 (cs1 ++ [c])). simpl.
      rewrite -app_assoc. simpl. eauto.
Qed.

Lemma prefix_of_last {A: Type} (cs1 cs2: list A):
  prefix_of cs1 cs2
  match last cs1, last cs2 with
  | None, _True
  | Some _, NoneFalse
  | Some c1, Some c2
     (cs1' cs2': list A), cs1 = cs1' ++ [c1]
                  (cs2 = cs1' ++ [c1] ++ cs2' ++ [c2]
                   cs2 = cs1 c1 = c2)
  end.
Proof.
  intros (csext&Heq).
  induction cs1 using rev_ind.
  - simpl; auto.
  - rewrite Heq.
    induction csext using rev_ind.
    × simpl. rewrite app_nil_r. rewrite last_snoc.
       cs1, [].
      split_and!; eauto.
    × rewrite ?last_snoc.
      rewrite app_assoc. rewrite ?last_snoc.
       cs1, csext.
      split_and!; eauto.
      left. simpl. rewrite -?app_assoc. simpl. auto.
Qed.

Lemma prefix_tp_monotone cs1 cs2 is2:
  prefix_of cs1 cs2 valid_cfg_idx_seq cs2 is2
  match last cs1, last cs2 with
  | None, _True
  | Some _, NoneFalse
  | Some c1, Some c2
    length (fst c1) length (fst c2)
  end.
Proof.
  intros Hp Hv. specialize (prefix_of_last cs1 cs2 Hp); intros Hpre_last.
  destruct (last cs1), (last cs2); auto.
  destruct Hpre_last as (cs1'&cs2'&?&[Heq|(_&Heq)]).
  - rewrite Heq in Hv. eapply (valid_seq_tp_monotone_mid _ _ _ _ []); eauto.
  - subst. auto.
Qed.

Instance transitive_prefix_of {A: Type}: Transitive (@prefix_of A).
Proof.
  intros l1 l2 l3 (?&->) (?&->). rewrite -assoc; eexists; eauto.
Qed.

Lemma prefix_of_down_total {A: Type} (la lb lc: list A):
  la `prefix_of` lc
  lb `prefix_of` lc
  (la `prefix_of` lb lb `prefix_of` la).
Proof.
  intros (lc1&->) (lc2&Heq).
  revert lb lc1 lc2 Heq.
  induction la as [|a' la].
  - left; eexists; eauto.
  - intros. destruct lb; first (right; eexists; eauto).
    injection Heq. intros Heq' →.
    edestruct (IHla lb lc1 lc2) as [(?&->)|(?&->)]; eauto.
    × left; eexists; eauto.
    × right; eexists; eauto.
Qed.

Lemma valid_cfg_idx_length1 cs1 is1:
  valid_cfg_idx_seq cs1 is1
  length is1 length cs1.
Proof.
  induction 1; simpl in *; eauto; omega.
Qed.

Lemma valid_cfg_idx_length2 cs1 is1:
  valid_cfg_idx_seq cs1 is1
   S (length is1) length cs1.
Proof.
  induction 1; simpl in *; eauto; omega.
Qed.

Lemma valid_cfg_idx_length3 cs1 is1:
  valid_cfg_idx_seq cs1 is1
   (length is1 = 0 length cs1 = 0) (S (length is1) = length cs1).
Proof.
  induction 1; simpl in *; eauto; omega.
Qed.

Lemma valid_cfg_idx_length4 cs1 is1 c:
  valid_cfg_idx_seq (cs1 ++ [c]) is1
  length cs1 = length is1.
Proof.
  remember (cs1 ++ [c]) as cs eqn:Heqcs. intros Hval. revert c cs1 Heqcs.
  induction Hval; simpl in *; destruct cs1; simpl in *; try congruence.
  - intros. apply (f_equal length) in Heqcs. rewrite //= ?app_length //= in Heqcs.
    omega.
  - intros. inversion Heqcs. f_equal. edestruct IHHval; eauto.
Qed.

Lemma valid_cfg_idx_length5 cs1 is1 c:
  valid_cfg_idx_seq ([c] ++ cs1) is1
  length cs1 = length is1.
Proof.
  remember ([c] ++ cs1) as cs eqn:Heqcs. intros Hval. revert c cs1 Heqcs.
  induction Hval; simpl in *; destruct cs1; simpl in *; try congruence.
  - intros. f_equal. eapply IHHval. inversion Heqcs. auto.
Qed.

Lemma valid_cfg_idx_prefix_link cs1 cs2 is1 is2:
  valid_cfg_idx_seq cs1 is1
  valid_cfg_idx_seq cs2 is2
  cs1 `prefix_of` cs2
  is2 `prefix_of` is1
  is1 `prefix_of` is2.
Proof.
  intros Hv1 Hv2 (csext&->) (isext&->).
  edestruct (valid_cfg_idx_length3 _ _ Hv1) as [(Hlis1&Hlcs1)|Hl1]; eauto.
  - assert (isext = []).
    { rewrite app_length in Hlis1. destruct isext; auto; simpl in *; omega. }
    subst. rewrite app_nil_r; auto.
  - edestruct (valid_cfg_idx_length3 _ _ Hv2) as [(Hlis2&Hlcs2)|Hl2]; eauto.
    × exfalso. rewrite app_length in Hlcs2. omega.
    × assert (isext = []).
      { rewrite ?app_length in Hl1 Hl2. destruct isext; auto. simpl in *; omega. }
      subst. rewrite app_nil_r; auto.
Qed.

Lemma valid_cfg_idx_prefix_link' cs1 cs2 is1 isext:
  valid_cfg_idx_seq cs1 is1
  valid_cfg_idx_seq cs2 (is1 ++ isext)
  cs2 `prefix_of` cs1
  (cs1 `prefix_of` cs2 isext = [] ).
Proof.
  intros Hv1 Hv2 (csext&->).
  edestruct (valid_cfg_idx_length3 _ _ Hv1) as [(Hlis1&Hlcs1)|Hl1]; eauto.
  - assert (csext = []).
    { rewrite app_length in Hlcs1. destruct csext; auto; simpl in *; omega. }
    subst. rewrite app_nil_r; auto.
  - edestruct (valid_cfg_idx_length3 _ _ Hv2) as [(Hlis2&Hlcs2)|Hl2]; eauto.
    × right.
      rewrite ?app_length in Hl1 Hlis2. destruct isext; auto. simpl in *; omega.
    × destruct isext; auto.
      assert (csext = []).
      { simpl in *; rewrite ?app_length in Hl1 Hl2. destruct csext; auto; simpl in ×. omega. }
      subst. rewrite app_nil_r; auto.
Qed.

Lemma valid_cfg_idx_empty_ext cs1 c cs2 is1:
  valid_cfg_idx_seq (cs1 ++ [c]) is1
  valid_cfg_idx_seq (cs1 ++ [c] ++ cs2) is1
  cs2 = [].
Proof.
  intros Hv1 Hv2.
  edestruct (valid_cfg_idx_length3 _ _ Hv1) as [(Hlis1&Hlcs1)|Hl1]; eauto.
  - exfalso. rewrite app_length in Hlcs1. simpl in ×. omega.
  - edestruct (valid_cfg_idx_length3 _ _ Hv2) as [(Hlis2&Hlcs2)|Hl2]; eauto.
    × exfalso. rewrite app_length in Hlcs2. simpl in ×. omega.
    × rewrite ?app_length in Hl1 Hl2. destruct (cs2); auto. simpl in ×. omega.
Qed.

Global Instance : PreOrder (@prefix_of A).
Proof.
  split.
  × intros x; []; rewrite app_nil_r; auto.
  × by apply _.
Qed.
Global Instance: AntiSymm (=) (@prefix_of A).
Proof.
  intros A x y. intros (ex1&Heq1) (ex2&Heq2).
  rewrite Heq1 in Heq2.
  assert ([] = ex1 ++ ex2) as Happ_nil.
  { eapply app_inv_head. rewrite app_nil_r app_assoc. eauto. }
  symmetry in Happ_nil.
  eapply app_eq_nil in Happ_nil as (->&->).
  rewrite app_nil_r in Heq1. auto.
Qed.

Lemma prefix_of_op r1 r2:
  prefix_of (cfgs r1) (cfgs r2)
  r1 r2 = Refine (max_view (view r1) (view r2))
                   (tids r1 tids r2)
                   (cfgs r2)
                   (idxs r2).
Proof.
  intros Hprec. rewrite /op /refine_op.
  specialize (prefix_of_length _ _ Hprec); intros.
  destruct le_dec; auto.
  exfalso; eauto.
Qed.

Lemma cfgs_of_prefix_of_op_l r1 r2:
  prefix_of (cfgs r2) (cfgs r1)
  cfgs (r1 r2) = cfgs r1.
Proof.
  intros Hprec. rewrite /op /refine_op.
  specialize (prefix_of_length _ _ Hprec); intros.
  destruct le_dec; auto.
  destruct Hprec as (csext&Heq_ext).
  rewrite Heq_ext.
  apply (f_equal length) in Heq_ext.
  rewrite app_length in Heq_ext. destruct (csext); rewrite ?app_nil_r; simpl in *; auto.
  omega.
Qed.

Lemma prefix_of_strict_op' r1 r2:
  ( csext c, cfgs r1 = cfgs r2 ++ csext ++ [c])
  r1 r2 = Refine (max_view (view r1) (view r2))
                   (tids r1 tids r2)
                   (cfgs r1)
                   (idxs r1).
Proof.
  intros (csext&c&Hstrict_prec). rewrite /op /refine_op.
  rewrite Hstrict_prec. destruct le_dec as [l|n]; auto.
  rewrite ?app_length in l. simpl in ×. omega.
Qed.

Lemma prefix_of_op' r1 r2:
  prefix_of (cfgs r1) (cfgs r2)
  r2 r1 = Refine (max_view (view r2) (view r1))
                   (tids r2 tids r1)
                   (cfgs r2)
                   (idxs r2)
  (prefix_of (cfgs r2) (cfgs r1)
  r2 r1 = Refine (max_view (view r1) (view r2))
                   (tids r2 tids r1)
                   (cfgs r1)
                   (idxs r1)).
Proof.
  intros Hprec. rewrite /op /refine_op.
  specialize (prefix_of_length _ _ Hprec); intros.
  destruct le_dec as [l|r]; auto.
  right; split; auto.
  × destruct r1, r2; simpl in ×.
    destruct Hprec as (cs'&->). destruct cs'; auto.
    ** rewrite app_nil_r. auto.
    ** rewrite app_length in l; simpl in *; omega.
  × f_equal; destruct (view r2), (view r1); auto.
Qed.

Lemma prefix_of_op'' r1 r2:
  (prefix_of (cfgs r1) (cfgs r2) prefix_of (cfgs r2) (cfgs r1))
  (prefix_of (cfgs r1) (cfgs r2)
   r1 r2 = Refine (max_view (view r1) (view r2))
                   (tids r1 tids r2)
                   (cfgs r2)
                   (idxs r2))
  (prefix_of (cfgs r2) (cfgs r1)
   r1 r2 = Refine (max_view (view r1) (view r2))
                   (tids r1 tids r2)
                   (cfgs r1)
                   (idxs r1)).
Proof.
  intros Hprec. rewrite /op /refine_op.
  destruct le_dec as [l|r]; auto.
  - destruct Hprec as [Hprec|Hprec]; auto.
    assert (cfgs r1 = cfgs r2) as →.
    { destruct r1, r2; simpl in ×.
      destruct Hprec as (csext&->).
      destruct csext; first (rewrite app_nil_r; auto).
      rewrite app_length in l; simpl in *; omega.
    }
    auto.
  - destruct Hprec as [Hprec|Hprec]; auto.
    specialize (prefix_of_length _ _ Hprec); intros.
    omega.
Qed.

Lemma prefix_of_op''' r1 r2:
  valid_cfg_idx_seq (cfgs r1) (idxs r1)
  valid_cfg_idx_seq (cfgs r2) (idxs r2)
  prefix_of (cfgs r1) (cfgs r2)
  prefix_of (idxs r1) (idxs r2)
  r2 r1 = Refine (max_view (view r1) (view r2))
                   (tids r2 tids r1)
                   (cfgs r2)
                   (idxs r2).
Proof.
  intros Hv1 Hv2 Hprec Hprei. rewrite /op /refine_op.
  specialize (prefix_of_length _ _ Hprec); intros Hlc.
  specialize (prefix_of_length _ _ Hprei); intros Hli.
  destruct r1 as [v1 t1 cfgs1 is1];
  destruct r2 as [v2 t2 cfgs2 is2];
  destruct le_dec; auto; simpl in ×.
  - assert (cfgs1 = cfgs2) as →.
    { destruct Hprec as (csext&->).
      rewrite app_length in l.
      destruct csext; [| simpl in *; omega].
        by rewrite app_nil_r. }
    assert (is1 = is2) as →.
    { apply (anti_symm prefix_of); auto.
      eapply valid_cfg_idx_prefix_link; eauto.
    }
    f_equal. destruct v1, v2; auto.
  - f_equal. destruct v1, v2; auto.
Qed.

Lemma disjoint_up_closed_snapshot ts1 ts2 ts3 cs1 cs2 csext is1 is2 isext:
  ts1 ts2 =
  prefix_of_valid_seq ts1 cs1 is1 cs2 is2
  valid_cfg_idx_seq cs1 is1
  valid_cfg_idx_seq cs2 is2
  valid_cfg_idx_seq (cs2 ++ csext) (is2 ++ isext)
  Refine snapshot ts1 cs1 is1 Refine snapshot ts3 (cs2 ++ csext) (is2 ++ isext)
  Refine snapshot ts1 cs2 is2 Refine snapshot ts3 (cs2 ++ csext) (is2 ++ isext).
Proof.
  intros Hinter12 Hprefix12 Hval1 Hval2 Hval2ext Hdisj12ext.
  inversion Hdisj12ext as [? ? ? ? ? ? Hinter13 [Hprefix12ext|Hprefix2ext1] | |]; subst.
  - econstructor; eauto.
    left. econstructor; first (eexists; eauto).
     isext. split; auto.
    destruct Hprefix12ext as (_ & isext'&Heq_isext'&Hnin_isext').
    destruct Hprefix12 as (_ &isext0&Heq_isext0&Hnin_isext0).
    rewrite Heq_isext0 in Heq_isext'.
    rewrite -app_assoc in Heq_isext'. apply app_inv_head in Heq_isext'.
    intros i Hin_ts1 Hin_isext.
    apply (Hnin_isext' i); auto.
    set_solver.
  - assert (cs2 = cs2 ++ csext) as <-.
    { apply (anti_symm (prefix_of)).
      - eexists; eauto.
      - destruct Hprefix12 as (?&_).
        destruct Hprefix2ext1 as (?&_).
        etransitivity; eauto.
    }
    assert (is2 = is2 ++ isext) as <-.
    { apply (anti_symm (prefix_of)).
      - eexists; eauto.
      - destruct Hprefix12 as (_&?&?&?).
        destruct Hprefix2ext1 as (_&?&?&?).
        etransitivity; eexists; eauto.
    }
    econstructor; auto.
    right. split; eauto.
     []; rewrite ?app_nil_r; split; auto.
    set_solver.
Qed.

Lemma disjoint_down_closed_snapshot ts1 ts2 ts3 v cs1 cs2 cs3 is1 is2 is3:
  ts1 ts2
  prefix_of_valid_seq ts1 cs1 is1 cs2 is2
  valid_cfg_idx_seq cs1 is1
  valid_cfg_idx_seq cs2 is2
  valid_cfg_idx_seq cs3 is3
  Refine snapshot ts2 cs2 is2 Refine v ts3 cs3 is3
  Refine snapshot ts1 cs1 is1 Refine v ts3 cs3 is3.
Proof.
  intros Hst (Hps&(isext&Heq&?)) Hv1 Hv2 Hv3. subst is2.
  inversion_clear 1 as [? ? ? ? ? ? ? Hpres | ? | ?].
  - intros. constructor; auto.
    × set_solver.
    × destruct Hpres as [(?&(isext'&Heq&?))|(?&(isext'&Heq&?))].
      ** left; split; first (etransitivity; eauto).
          (isext ++ isext'); split.
         *** rewrite app_assoc; auto.
         *** intros i Hin Hf. apply elem_of_app in Hf as [?|?]; naive_solver.
      ** edestruct (prefix_of_down_total cs1 cs3 cs2); eauto;
         edestruct (prefix_of_down_total is1 is3 (is1 ++ isext)) as [Hpi|Hpi]; eauto;
         try (eexists; eauto; done).
         *** left.
             destruct Hpi as (isext0&->).
             rewrite -app_assoc in Heq.
             apply app_inv_head in Heq.
             subst.
             constructor; eauto.
             eexists. split; eauto.
             intros. set_solver.
         *** assert (is1 `prefix_of` is3) as Hpi' by (eapply valid_cfg_idx_prefix_link; eauto).
             left.
             destruct Hpi' as (isext0&->).
             rewrite -app_assoc in Heq.
             apply app_inv_head in Heq.
             subst.
             constructor; eauto.
             eexists. split; eauto.
             intros. set_solver.
         *** assert (is3 `prefix_of` is1) as Hpi' by (eapply valid_cfg_idx_prefix_link; eauto).
             right.
             destruct Hpi' as (isext0&->).
             rewrite -app_assoc in Heq.
             apply app_inv_head in Heq.
             subst.
             constructor; eauto.
             eexists. split; eauto.
             intros. set_solver.
         *** right.
             destruct Hpi as (isext0&->).
             rewrite -app_assoc in Heq.
             apply app_inv_head in Heq.
             subst.
             constructor; eauto.
             eexists. split; eauto.
             intros. set_solver.
  - destruct Hps as (csext&->). rewrite -?app_assoc.
     econstructor.
     × set_solver.
     × intros i Hin Hf. apply elem_of_app in Hf as [?|?]; naive_solver.
Qed.

Lemma disjoint_down_closed_master ts1 ts2 ts3 v cs1 cs2 cs3 is1 is2 is3:
  ts1 ts2
  prefix_of_valid_seq ts1 cs1 is1 cs2 is2
  valid_cfg_idx_seq cs1 is1
  valid_cfg_idx_seq cs2 is2
  valid_cfg_idx_seq cs3 is3
  Refine master ts2 cs2 is2 Refine v ts3 cs3 is3
  Refine snapshot ts1 cs1 is1 Refine v ts3 cs3 is3.
Proof.
  intros Hst (Hps&(isext&->&?)) Hv1 Hv2 Hv3.
  intros Hdisj.
  assert (is3 `prefix_of` (is1 ++ isext)) as Hpre1.
  { inversion Hdisj. subst. eexists; eauto. }
  edestruct (prefix_of_down_total is1 is3 (is1 ++ isext)) as [Hpre2|Hpre2]; try (eauto; eexists; eauto).
  - destruct Hpre1 as (isext1&Heq).
    destruct Hpre2 as (isext0&->).
    rewrite Heq in Hdisj.
    inversion Hdisj.
    subst. econstructor.
    × set_solver.
    × edestruct (prefix_of_down_total cs1 cs3); eauto.
      { eexists; eauto. }
      ** left. split; eauto. eexists; split; eauto.
         intros. intro Hf. eapply H; eauto.
         rewrite -app_assoc in Heq.
         apply app_inv_head in Heq. subst. set_solver.
      ** edestruct (valid_cfg_idx_prefix_link' cs1 cs3); eauto.
         *** left. split; eauto. eexists; split; eauto.
             intros. intro Hf. eapply H; eauto.
             rewrite -app_assoc in Heq.
             apply app_inv_head in Heq. subst. set_solver.
         *** subst. rewrite app_nil_r.
             right. split; eauto. []. rewrite app_nil_r. split; auto.
             intros. set_solver.
  - edestruct Hpre2 as (isext0&->).
     rewrite -app_assoc in Hdisj.
     inversion Hdisj as [ | | ? ? ? ? ? is2 Hdisj' Hnin]. subst.
     econstructor; first set_solver.
     edestruct (prefix_of_down_total cs1 cs3); eauto.
     { eexists; eauto. }
     × edestruct (valid_cfg_idx_prefix_link' cs3 cs1); eauto.
       ** right. split; eauto. eexists; split; eauto.
          intros. intro Hf. eapply Hnin; eauto.
          assert (is2 = isext0 ++ isext) asby (eapply app_inv_head; eauto).
          set_solver.
       ** subst. rewrite app_nil_r.
          left. split; eauto. []. rewrite app_nil_r. split; auto.
          intros. set_solver.
     × right. split; eauto. eexists; split; eauto.
       intros. intro Hf.
       assert (is2 = isext0 ++ isext) asby (eapply app_inv_head; eauto).
       set_solver.
Qed.

Instance prefix_of_valid_seq_proper:
  Proper ((≡) ==> eq ==> eq ==> eq ==> eq ==> iff) prefix_of_valid_seq.
Proof.
  intros x y Heq ??? ??? ??? ???. subst.
  split; destruct 1 as (?&(?&?&?));
  split; eauto;
  eexists; split; setoid_subst; eauto.
Qed.

Lemma prefix_of_valid_seq_inj t cs is1 is2:
  prefix_of_valid_seq t cs is1 cs is2
  valid_cfg_idx_seq cs is1
  valid_cfg_idx_seq cs is2
  is1 = is2.
Proof.
  intros (?&?&?&?) Hv1 Hv2.
  apply (anti_symm (prefix_of)).
  - eexists; eauto.
  - eapply valid_cfg_idx_prefix_link; eauto.
    eexists; eauto.
Qed.

Lemma prefix_of_valid_seq_op r1 r2 ts1 ts2:
  (prefix_of_valid_seq ts1 (cfgs r1) (idxs r1) (cfgs r2) (idxs r2)
   prefix_of_valid_seq ts2 (cfgs r2) (idxs r2) (cfgs r1) (idxs r1))
  valid_cfg_idx_seq (cfgs r1) (idxs r1)
  valid_cfg_idx_seq (cfgs r2) (idxs r2)
  (prefix_of_valid_seq ts1 (cfgs r1) (idxs r1) (cfgs r2) (idxs r2)
   r1 r2 = Refine (max_view (view r1) (view r2))
                   (tids r1 tids r2)
                   (cfgs r2)
                   (idxs r2))
  (prefix_of_valid_seq ts2 (cfgs r2) (idxs r2) (cfgs r1) (idxs r1)
   r1 r2 = Refine (max_view (view r1) (view r2))
                   (tids r1 tids r2)
                   (cfgs r1)
                   (idxs r1)).
Proof.
  intros Hprec Hv1 Hv2.
  destruct Hprec as [Hpre|Hpre].
  - left. split; auto.
    rewrite prefix_of_op; eauto.
    destruct Hpre; eauto.
  - right. split; auto.
    rewrite prefix_of_op'''; eauto.
    × f_equal; destruct (view r1), (view r2); auto.
    × destruct Hpre; eauto.
    × destruct Hpre as (_&(?&?&?)); eauto.
      eexists; eauto.
Qed.

Lemma valid_cfg_idx_seq_range cs c idxs:
  valid_cfg_idx_seq (cs ++ [c]) idxs
   i, i idxs i < (length (fst c)).
Proof.
  remember (cs ++ [c]) as cs' eqn:Heqcs.
  intros Hval. revert cs c Heqcs.
  induction Hval as [| | c' c'' cs_ i idxs Hstep Hval]; subst.
  - intros. set_solver.
  - intros ? ? ? i Hin. set_solver.
  - intros cs c Heq i' Hin.
    assert (i < length (fst c')) by eauto using length_cfg_idx_step2.
    eapply length_cfg_idx_step in Hstep.
    destruct cs; first (simpl in *; try congruence).
    inversion Heq as [[Heq1 Heq2]]; subst.
    assert (length (fst c'') length (fst c)).
    {
      destruct cs as [|c1 ?].
      × simpl in ×. inversion Heq2. subst. auto.
      × rewrite Heq2 in Hval. inversion Heq2. subst.
        eapply (valid_seq_tp_monotone_mid c1 c [] cs []) in Hval.
        omega.
    }
    inversion Hin; subst.
    × omega.
    × eapply IHHval; eauto.
Qed.

Lemma valid_seq_tp_monotone_all_tl c' cs1 is1:
  valid_cfg_idx_seq (cs1 ++ [c']) is1
   c, c cs1 ++ [c'] length (fst c) length (fst c').
Proof.
  intros Hval c [Hin|Hin']%elem_of_app.
  - assert ( cs1a cs1b, cs1 = cs1a ++ [c] ++ cs1b).
    {
      clear -Hin.
      induction cs1; first set_solver.
      inversion Hin; subst.
      × []. eexists. eauto.
      × edestruct IHcs1 as (cs1a&cs1b&->); auto.
         (a :: cs1a), cs1b. eauto.
    }
    destruct H as (cs1a & cs1b& ->).
    eapply (valid_seq_tp_monotone_mid _ _ cs1a cs1b []). rewrite -?app_assoc in Hval.
    simpl in ×. eauto.
  - assert (c = c') asby (set_solver); auto.
Qed.

Ltac gen_bounds H :=
  let Hdup := fresh "H" in
  generalize H; intros Hdup;
  repeat rewrite ?app_assoc ?app_comm_cons in Hdup;
  specialize (valid_cfg_idx_seq_range _ _ _ Hdup); intros;
  clear Hdup.

Lemma refine_step_prefix r1 r2:
  r1 r2
  (cfgs r1) `prefix_of` (cfgs r2)
  (idxs r1) `prefix_of` (idxs r2).
Proof.
  induction 1; simpl.
  - split.
    × (cs2 ++ [c2]). rewrite -assoc. auto.
    × eexists; eauto.
  - simpl in ×. destruct IHrefine_step as ((csext&->)&(isext&->)). split.
    × eexists. rewrite -?assoc. simpl. eauto.
    × eexists. rewrite -?assoc. simpl. eauto.
Qed.
Lemma valid_seq_join cs1 c is1 cs2 is2:
  valid_cfg_idx_seq (cs1 ++ [c]) is1
  valid_cfg_idx_seq ([c] ++ cs2) is2
  valid_cfg_idx_seq (cs1 ++ [c] ++ cs2) (is1 ++ is2).
Proof.
  remember (cs1 ++ [c]) as cs1c eqn:Heq_cs1c.
  intros Hval.
  revert cs1 c cs2 is2 Heq_cs1c.
  induction Hval.
  - intros. destruct cs1; simpl in *; congruence.
  - intros. destruct cs1.
    × simpl; eauto.
    × apply (f_equal length) in Heq_cs1c. rewrite //= ?app_length //= in Heq_cs1c.
      omega.
  - intros.
    rewrite assoc.
    rewrite -Heq_cs1c.
    destruct cs1; first (simpl in *; congruence).
    simpl in ×.
    inversion Heq_cs1c as [[Heqc Heqc']]; subst.
    econstructor; first eauto.
    rewrite app_comm_cons.
    rewrite Heqc'.
    rewrite -assoc. simpl. eauto.
Qed.

Lemma valid_seq_split cs1 c is1 cs2 is2:
  valid_cfg_idx_seq (cs1 ++ [c] ++ cs2) (is1 ++ is2)
  length cs1 = length is1
  valid_cfg_idx_seq ([c] ++ cs2) is2.
Proof.
  revert c cs2 is1 is2.
  induction cs1; simpl.
  × destruct is1; auto; simpl. intros. omega.
  × simpl in ×. intros c cs2 is1 is2 Hval.
    simpl in Hval. inversion Hval as [ | | c' c'' cs i idxs ? ? (Heq1&Heq2) Heq3].
    ** destruct cs1; simpl in *; congruence.
    ** destruct cs1; simpl in ×.
       *** inversion Heq2.
           subst. intros.
           destruct is1; first (simpl in *; omega).
           destruct is1; last (simpl in *; omega).
           inversion Heq3. subst. eauto.
       *** inversion Heq2. subst.
           destruct is1; first (simpl in *; omega).
           inversion Heq3. subst.
           intros. eapply IHcs1. eauto.
           simpl in ×.
           omega.
Qed.

Lemma valid_cfg_extract cs c is1:
  valid_cfg_idx_seq ([c] ++ cs) is1
   c', Some c' = last ([c] ++ cs)
        isteps (idx_step) is1 c c'.
Proof.
  intros Hval.
  remember ([c] ++ cs) as cs1 eqn:Heqcs1.
  revert cs c Heqcs1.
  induction Hval.
  - intros. destruct cs; simpl in *; congruence.
  - intros. assert (cs = []) asby (destruct cs; simpl in *; auto; congruence).
    rewrite app_nil_r in Heqcs1. inversion Heqcs1. subst.
    simpl.
    eexists; split; eauto. econstructor.
  - intros.
     simpl in ×. inversion Heqcs1.
     edestruct (IHHval) as (?&?&?); eauto. destruct cs.
     × eexists; split; eauto. econstructor; eauto.
       subst. eauto.
     × eexists; split; eauto.
       econstructor; eauto. subst. eauto.
Qed.

Lemma valid_cfg_extract' c1 cs c2 is1:
  valid_cfg_idx_seq ([c1] ++ cs ++ [c2]) is1
  isteps (idx_step) is1 c1 c2.
Proof.
  intros (c'&Heqc'&?)%valid_cfg_extract.
  rewrite app_assoc last_snoc in Heqc'.
  inversion Heqc'; subst; auto.
Qed.

Lemma valid_cfg_extract'' cinit c1 cs c2 is1:
  valid_cfg_idx_seq (cinit ++ [c1] ++ cs ++ [c2]) is1
   is1a is1b,
    is1 = is1a ++ is1b
    length is1a = length cinit
    length is1b = S (length cs)
    isteps (idx_step) is1b c1 c2.
Proof.
  intros Hval.
  assert (length (cinit ++ [c1] ++ cs) = length is1) as Hlen1.
  { eapply valid_cfg_idx_length4. rewrite -?app_assoc. eauto. }
  apply valid_seq_app in Hval as (is1a&is1b&Heq&Hval).
  assert (length is1b = length (cs ++ [c2])) as Hlen2.
  { symmetry. eapply valid_cfg_idx_length5; eauto. }
  rewrite ?app_length //= in Hlen1 Hlen2.
  eapply valid_cfg_extract' in Hval.
   is1a, is1b.
  split_and!; eauto.
  × apply (f_equal length) in Heq. rewrite ?app_length //= in Heq. omega.
  × simpl in ×. omega.
Qed.

Lemma valid_cfg_extract''' cinit c1 cs c2 isinit is1:
  valid_cfg_idx_seq (cinit ++ [c1] ++ cs ++ [c2]) (isinit ++ is1)
  valid_cfg_idx_seq (cinit ++ [c1]) isinit
    isteps (idx_step) is1 c1 c2.
Proof.
  intros Hval_full Hval_short.
  assert (length cinit = length isinit).
  {
    eapply valid_cfg_idx_length4; eauto.
  }
  eapply valid_seq_split in Hval_full; auto.
  eapply valid_cfg_extract'; eauto.
Qed.

Lemma valid_cfg_extract'''' c1 c2 cs is1:
  hd_error cs = Some c1
  last cs = Some c2
  valid_cfg_idx_seq (cs) is1
  isteps (idx_step) is1 c1 c2.
Proof.
  destruct cs as [| c1' cs].
  - simpl; intros; congruence.
  - destruct cs as [| c2' cs _] using rev_ind.
    × simpl in ×. inversion 1; subst. inversion 1; subst.
      inversion 1. subst. econstructor.
    × rewrite app_comm_cons. rewrite last_snoc.
         simpl. inversion 1; subst. inversion 1; subst.
         replace (c1 :: cs ++ [c2]) with ([c1] ++ cs ++ [c2]) by auto.
         eapply valid_cfg_extract'.
Qed.

Lemma refine_step_strict_prefix r1 r2:
  r1 r2
   cs0 c c' csext ixs,
    cfgs r1 = cs0 ++ [c]
    cfgs r2 = cs0 ++ [c] ++ csext ++ [c']
    idxs r2 = idxs r1 ++ ixs
    valid_cfg_idx_seq ([c] ++ csext ++ [c']) (ixs).
Proof.
  induction 1 as [t1 t2 cs1 cs2 c1 c2 is1 is2|t1 t2 cs1 c1 cspec cs2 is1 ispec is2 Hval0]; simpl.
  - cs1, c1, c2, cs2, is2. split_and!; eauto.
  - simpl in ×.
    destruct IHrefine_step as (cs0&c&c'&csext&ixs&Heq1&Heq2&Heq3&Hval).
    subst.
     cs1, c1. c', (cspec ++ csext).
     (ispec ++ ixs).
    split_and!; auto.
    × rewrite ?app_comm_cons.
      rewrite ?app_assoc.
      rewrite Heq1 //=. rewrite -?app_assoc. simpl. auto.
    × rewrite ?app_assoc. auto.
    × induction cspec as [|c_alt cspec] using rev_ind.
      ** apply app_inj_2 in Heq1 as (?&Heqc); auto. inversion Heqc; subst; simpl; auto.
         inversion Hval0. subst. auto.
      ** simpl. rewrite -?app_assoc.
         rewrite -?app_assoc in Heq1.
         rewrite app_comm_cons in Heq1.
         rewrite app_assoc in Heq1.
         apply app_inj_2 in Heq1 as (?&Heqc_alt); last (by simpl; auto).
         inversion Heqc_alt; subst.
         apply (valid_seq_join (c1 :: cspec) c ispec (csext ++ [c'])); simpl; auto.
Qed.

Lemma refine_step_inv r1 r2:
  r1 r2
   cs0 c c' cspec csext i' ispec isext,
    cfgs r1 = cs0 ++ [c]
    view r2 = snapshot
    cfgs r2 = cs0 ++ [c] ++ cspec ++ csext ++ [c']
    idxs r2 = idxs r1 ++ ispec ++ isext ++ [i']
    length ispec = length cspec
    ( i, i ispec i (tids r1))
    ( i, i (isext ++ [i']) i (tids r1))
    ( i, i (tids r2) (i tids r1 (( cinter, cinter c :: cspec length (fst cinter) i)
                                                          length (fst c') > i)))
    
    
    valid_cfg_idx_seq ([c] ++ cspec ++ csext ++ [c']) (ispec ++ isext ++ [i']).
Proof.
  induction 1 as [t1 t2 cs1 cs2 c1 c2 is1 is2|t1 t2 cs1 c1 cspec cs2 is1 ispec is2 Hval0]; simpl.
  - destruct is2 as [| i is2] using rev_ind.
    × exfalso.
      assert (length (cs2 ++ [c2]) = length ([]: list nat)) as Hlen.
      { eapply valid_cfg_idx_length5. eauto. }
      rewrite app_length in Hlen; simpl in *; omega.
    × cs1, c1, c2, [], cs2, i, [], is2. split_and!; eauto.
      ** set_solver.
      ** intros i'; split; set_solver.
  - simpl in ×.
    destruct IHrefine_step
      as (cs0&c&c'&cspec2&csext&i'&ispec2&ixs&Heq1&Heqv&Heq2&Heq3&Hlen&?&?&Hnew&Hval).
    subst.
     cs1, c1. c', (cspec ++ cspec2), csext.
     i', (ispec ++ ispec2), ixs.
    split_and!; auto.
    × rewrite ?app_comm_cons.
      rewrite ?app_assoc.
      rewrite Heq1 //=. rewrite -?app_assoc. simpl. auto.
    × rewrite ?app_assoc. auto.
    × rewrite ?app_length. f_equal; auto; symmetry.
      eapply valid_cfg_idx_length5; eauto.
    × intros i [Hin1|Hin2]%elem_of_app; set_solver.
    × intros i; split.
      ** intros. edestruct (Hnew i) as (Hin2&_).
         edestruct Hin2 as [|(Hmax&Hend)]; eauto. right.
         split; auto; [].
         destruct cspec as [|c_alt cspec] using rev_ind.
         *** apply app_inj_2 in Heq1 as (?&Heqc); last auto; [].
             assert (c1 = c) asby (inversion Heqc; auto).
             simpl. eauto.
         *** rewrite app_comm_cons in Heq1.
             rewrite app_assoc in Heq1.
             apply app_inj_2 in Heq1 as (?&Heqc_alt); last auto; [].
             assert (c_alt = c) asby (inversion Heqc_alt; auto).
             intros cinter. rewrite app_comm_cons.
             intros [Hin1'|Hin2']%elem_of_app.
             **** assert (length (fst cinter) length (fst c)).
                  {
                    eapply valid_seq_tp_monotone_all_tl.
                    rewrite app_comm_cons in Hval0.
                    eauto.
                    simpl. auto.
                  }
                  etransitivity; last eapply (Hmax c); auto.
                  left.
             **** eapply Hmax. right; auto.
      ** intros [Hin1|(Hmax&Hend)].
         *** naive_solver.
         *** eapply Hnew. right. split; auto.
             intros.
             eapply Hmax.
             destruct cspec as [|c_alt cspec] using rev_ind.
             **** apply app_inj_2 in Heq1 as (?&Heqc); last auto; [].
                  assert (c1 = c) asby (inversion Heqc; auto).
                  simpl. eauto.
             **** rewrite app_comm_cons in Heq1.
                  rewrite app_assoc in Heq1.
                  apply app_inj_2 in Heq1 as (?&Heqc_alt); last auto; [].
                  assert (c_alt = c) asby (inversion Heqc_alt; auto).
                  right. rewrite -app_assoc. simpl. apply elem_of_app.
                  right. auto.
    × induction cspec as [|c_alt cspec] using rev_ind.
      ** apply app_inj_2 in Heq1 as (?&Heqc); auto. inversion Heqc; subst; simpl; auto.
         inversion Hval0. subst. auto.
      ** simpl. rewrite -?app_assoc.
         rewrite -?app_assoc in Heq1.
         rewrite app_comm_cons in Heq1.
         rewrite app_assoc in Heq1.
         apply app_inj_2 in Heq1 as (?&Heqc_alt); last (by simpl; auto).
         inversion Heqc_alt; subst.
         apply (valid_seq_join (c1 :: cspec) c ispec (cspec2 ++ csext ++ [c'])); simpl; auto.
Qed.

Lemma refine_step_disjoint_all_threads ts1 cs1 is1 ts2 cs2 is2 ts3 cs3 is3 c v3:
  Refine snapshot ts1 cs1 is1 Refine v3 ts3 cs3 is3
  ts1 ts2 =
  ( i, i < length (fst c) i ts1 ts2)
  prefix_of_valid_seq ts1 cs1 is1 (cs2 ++ [c]) is2
  valid_cfg_idx_seq cs1 is1
  valid_cfg_idx_seq (cs2 ++ [c]) is2
  Refine snapshot ts2 (cs2 ++ [c]) is2 Refine v3 ts3 cs3 is3
   c' csext isext tsext, cs3 = (cs2 ++ [c]) ++ csext ++ [c'] is3 = is2 ++ isext
                          ts3 = ts1 tsext
                 ( i, i isext i ts1)
                 ( i, i ts1 (count_occ (nat_eq_dec) isext i K))
                 ( i, i tsext (length (fst c) i length (fst c') > i))
                 ( i, i ts1 (i isext
                             ¬ (enabled idx_step c' i)))
                 valid_cfg_idx_seq cs3 is3.
Proof.
  remember (Refine snapshot ts1 cs1 is1) as r1 eqn:Heq_r1.
  remember (Refine v3 ts3 cs3 is3) as r3 eqn:Heq_r3.
  intros Hstep. revert ts1 cs1 is1 ts2 cs2 is2 ts3 is3 cs3 v3 Heq_r1 Heq_r3.
  induction Hstep as [ts1' tsext cs0 csext c1 c3 is1' isext Hvalext ? ? Howned|
                      ts1' ts3' cs0 c1 cspec cs3' is1' ispec is3' Hvalspec Hnin1 Hstep].
  - intros ts1 cs1 is1 ts2 cs2 is2 ts3 is3 cs3 v3.
    intros Heq_r1 Heq_r2.
    assert (ts1' = ts1) as →. { apply (f_equal tids) in Heq_r1. auto. }
    assert (is1' = is1) as →. { apply (f_equal idxs) in Heq_r1. auto. }
    assert (v3 = snapshot) as →. { apply (f_equal view) in Heq_r2. auto. }
    inversion_clear Heq_r1; subst.
    inversion_clear Heq_r2; subst.
    intros Hinter Hall Hprefix Hvalid1 Hvalid2 Hdisj.
    destruct Hprefix as ((csalt&Heq_csalt)&(isalt&Heq_isalt&Hnin)).
    rewrite Heq_csalt in Hvalid2 Hdisj ×.
    destruct isext as [|i isext].
    × eapply valid_cfg_idx_length2 in Hvalext.
      rewrite ?app_length //= in Hvalext. omega.
    × rewrite Heq_isalt in Hdisj.
      rewrite Heq_isalt in Hvalid2.
      assert (isalt = []) as →.
      {
      destruct isalt as [|i' isalt]; auto.
      inversion Hdisj as [? ? ? ? ? ? Hinter' Hprefix | |]; subst; [].
      destruct Hprefix as [Hprefix|Hprefix].
      ** destruct Hprefix as (?&(isfurther&Heq_isfurther&?)).
         rewrite -app_assoc in Heq_isfurther.
         apply app_inv_head in Heq_isfurther.
         simpl in Heq_isfurther.
         assert (i = i') asby congruence.
         exfalso. eapply (Hnin i'); last set_solver +.
         eapply Howned; set_solver+.
      ** destruct Hprefix as (?&(isfurther&Heq_isfurther&?)).
         rewrite -app_assoc in Heq_isfurther.
         apply app_inv_head in Heq_isfurther.
         simpl in Heq_isfurther.
         assert (i = i') asby congruence.
         exfalso. eapply (Hnin i'); last set_solver +.
         eapply Howned; set_solver+.
      }
      assert (csalt = []) as →.
      {
        rewrite -app_assoc app_nil_r in Hvalid2.
        eapply valid_cfg_idx_empty_ext; eauto.
      }
      rewrite app_nil_r.
       c3, csext.
       (i :: isext).
       tsext.
      assert (c1 = c) as →.
      {
        rewrite app_nil_r in Heq_csalt.
        eapply app_inj_2 in Heq_csalt as (_&Heqc); auto.
        inversion Heqc. auto.
      }
      split_and!; eauto.
      ** rewrite -app_assoc //=.
      ** rewrite Heq_isalt. rewrite app_nil_r. auto.
      ** by (eapply valid_seq_join; eauto).
  - intros ts1 cs1 is1 ts2 cs2 is2 ts3 is3 cs3 v3.
    intros Heq_r1 Heq_r2.
    assert (ts1' = ts1) as →. { apply (f_equal tids) in Heq_r1. auto. }
    assert (is1' = is1) as →. { apply (f_equal idxs) in Heq_r1. auto. }
    assert (cs3' = cs3) as →. { apply (f_equal cfgs) in Heq_r2. auto. }
    assert (is3' = is3) as →. { apply (f_equal idxs) in Heq_r2. auto. }
    assert (ts3' = ts3) as →. { apply (f_equal tids) in Heq_r2. auto. }
    assert (v3 = snapshot) as →. { apply (f_equal view) in Heq_r2. auto. }
    inversion_clear Heq_r1; subst.
    inversion_clear Heq_r2; subst.
    intros Hinter Hall Hprefix Hvalid1 Hvalid2 Hdisj.
    assert (prefix_of_valid_seq ts1 (cs0 ++ [c1] ++ cspec)
                               (is1 ++ ispec) (cs2 ++ [c]) is2).
    {
      assert ((cs0 ++ [c1] ++ cspec `prefix_of` cs2 ++ [c]
               is1 ++ ispec `prefix_of` is2)
              
              (cs2 ++ [c] `prefix_of` cs0 ++ [c1] ++ cspec
                ispec0, is1 ++ ispec = is2 ++ ispec0 i, i ispec0 i ts2))
        as [(Hprecs&Hpreis)|(Hprecs&ispec2&Heq_ispec2&Hnin)].
      {
        inversion Hdisj as [? ? ? ? ? ? Hinter' Hprefix' | |]; subst.
        destruct Hprefix' as [Hprefix'|Hprefix'].
        assert (valid_cfg_idx_seq (cs0 ++ [c1] ++ cspec) (is1 ++ ispec)).
          by (eapply valid_seq_join; eauto).
        - edestruct (prefix_of_down_total (cs0 ++ [c1] ++ cspec) (cs2 ++ [c]) cs3).
          × eapply refine_step_prefix in Hstep as (?&?); eauto.
          × destruct Hprefix'; eauto.
          × left. split; auto.
            edestruct (prefix_of_down_total (is1 ++ ispec) is2 is3).
            ** eapply refine_step_prefix in Hstep as (?&?); eauto.
            ** destruct Hprefix' as (?&?&?&?); econstructor; eauto.
            ** eauto.
            ** eapply valid_cfg_idx_prefix_link; eauto.
          × right; split; auto.
            edestruct (prefix_of_down_total (is1 ++ ispec) is2 is3) as [Hpre|(ispec0&Heq_ispec0)].
            ** eapply refine_step_prefix in Hstep as (?&?); eauto.
            ** destruct Hprefix' as (?&?&?&?); econstructor; eauto.
            ** assert (is2 `prefix_of` is1 ++ ispec) by (eapply valid_cfg_idx_prefix_link; eauto).
               assert (is1 ++ ispec = is2) by (eapply (anti_symm prefix_of); eauto).
               subst. []. split; rewrite ?app_nil_r; auto.
               intros. set_solver.
            ** ispec0. split; eauto.
               intros.
               eapply refine_step_prefix in Hstep as (_&ispec'''&Heq_ispec'''); eauto. simpl in ×.
               destruct Hprefix' as (_&ispec''&Heq_ispec''&Hnin).
               destruct Hprefix as (_&ispec00&Heq_ispec00&Hnin').
               rewrite Heq_ispec'' in Heq_ispec'''.
               rewrite Heq_ispec0 in Heq_ispec'''.
               rewrite -assoc in Heq_ispec'''. apply app_inv_head in Heq_ispec'''.
               intros Hin_ts2. eapply Hnin.
               eauto. rewrite Heq_ispec'''.
               set_solver.
        - left. destruct Hprefix' as (?&?&?&?). split.
          × transitivity cs3; eauto.
            eapply refine_step_prefix in Hstep as (?&?); auto.
          × transitivity is3; last econstructor; eauto.
            eapply refine_step_prefix in Hstep as (?&?); auto.
      }
      - econstructor; eauto.
        destruct Hpreis as (ispec'&->).
         ispec'; split; eauto.
        destruct Hprefix as (_&ispec''&Heq_spec''&Hnin).
        intros i Hin Hfalse.
        rewrite -assoc in Heq_spec''.
        eapply app_inv_head in Heq_spec''.
        assert (i ispec''). rewrite -Heq_spec''. apply elem_of_app.
        auto.
        eapply Hnin; eauto.
      - destruct Hprefix as ((cspec1&Heq_cspec1)&ispec1&Heq_ispec1&?).
       rewrite Heq_cspec1 in Hprecs.
       rewrite Heq_ispec1 in Heq_ispec2.
       destruct Hprecs as (cspec2&Heq_cspec2).
       rewrite -?assoc in Heq_cspec2.
       do 2 apply app_inv_head in Heq_cspec2.
       rewrite -?assoc in Heq_ispec2.
       apply app_inv_head in Heq_ispec2.
       rewrite Heq_cspec1 Heq_ispec1 Heq_cspec2 Heq_ispec2.

       assert (length cs0 = length is1) by (eapply valid_cfg_idx_length4; eauto).
       assert (length cs2 = length is2) by (eapply valid_cfg_idx_length4; eauto).
       assert (length cspec = length ispec) by (eapply valid_cfg_idx_length5; eauto).
       assert (length cspec1 = length ispec1).
       {
         apply (f_equal length) in Heq_cspec1.
         apply (f_equal length) in Heq_ispec1. rewrite //= ?app_length //= in Heq_cspec1 Heq_ispec1.
         omega.
       }
       assert (length cspec2 = length ispec2).
       {
         apply (f_equal length) in Heq_cspec2.
         apply (f_equal length) in Heq_ispec2. rewrite //= ?app_length //= in Heq_cspec2 Heq_ispec2.
         omega.
       }
       
       destruct ispec2 as [|i ispec2].
        × destruct cspec2 as [|]; last (simpl in *; omega).
           rewrite ?app_nil_r. rewrite -app_assoc.
           split; eauto.
            []; rewrite ?app_nil_r. split; auto.
           intros. set_solver+.
        ×
          assert (valid_cfg_idx_seq (cs0 ++ [c1] ++ cspec) (is1 ++ ispec)) as Hval3
              by (eapply valid_seq_join; eauto).
          rewrite Heq_cspec2 in Hval3.
          rewrite ?app_assoc in Hval3.
          rewrite -Heq_cspec1 in Hval3.
          rewrite Heq_ispec2 in Hval3. rewrite app_assoc in Hval3.
          rewrite -Heq_ispec1 in Hval3.

          rewrite -?app_assoc in Hval3.
          eapply valid_seq_split in Hval3; eauto; [].
          simpl in Hval3.
          assert (i < length (fst c)) as Hi_lt.
          {
            inversion Hval3. subst. eapply length_cfg_idx_step2; eauto.
          }
          exfalso.
          eapply Hall in Hi_lt.
          apply elem_of_union in Hi_lt as [Hin1|Hin2].
          ** eapply (Hnin1 i); eauto.
             rewrite Heq_ispec2. set_solver.
          ** eapply (Hnin i); eauto.
             left; auto.
    }
    
    edestruct IHHstep; eauto.
    eapply valid_seq_join; eauto.
Qed.

Lemma sum_list_with_cons:
   (A : Type) (f : A nat) (a: A) (l : list A),
  sum_list_with f (a :: l) = f a + sum_list_with f l.
Proof. auto. Qed.

Lemma sum_list_with_Permutation:
   (A : Type) (f : A nat) (l l' : list A),
  Permutation l l' sum_list_with f l = sum_list_with f l'.
Proof.
  induction 1; auto.
  - simpl; by rewrite IHPermutation.
  - simpl. omega.
  - omega.
Qed.
Instance sum_list_with_perm: Proper (eq ==> Permutation ==> eq) (@sum_list_with A).
  intros A f f'l l' Hperm. eapply sum_list_with_Permutation; auto.
Qed.

Lemma sum_list_with_mono:
   (A : Type) (f f': A nat) (l : list A),
  ( a, a l f a f' a)
  sum_list_with f l sum_list_with f' l.
Proof.
  induction l as [| a l]; simpl; auto.
  intros Hmono. eapply plus_le_compat.
  - apply Hmono. set_solver.
  - apply IHl. intros a' Hin. eapply Hmono; set_solver.
Qed.

Lemma sum_list_with_equiv:
   (A : Type) (f f': A nat) (l : list A),
  ( a, a l f a = f' a)
  sum_list_with f l = sum_list_with f' l.
Proof.
  induction l as [| a l]; simpl; auto.
  intros Hmono. f_equal.
  - apply Hmono. set_solver.
  - apply IHl. intros a' Hin. eapply Hmono; set_solver.
Qed.

Lemma size_natset_elements (t1: natset): length (elements t1) = size t1.
Proof.
  revert t1.
  eapply collection_ind; eauto.
  intros t1 t2 Heq. rewrite Heq. auto.
Qed.

Lemma refine_step_disjoint_all_threads' r1 r2 r1':
   r1 r2 r1 r2 r1 r1' r2 r1'
  ( i, (i < default 0 (last (cfgs (r1 r2))) (length fst)) i (tids r1) (tids r2))
  
     cs0 c0 c' csext isext,
      (cfgs (r1 r2) = cs0 ++ [c0])
      (cfgs (r1' r2) = cfgs (r1 r2) ++ csext ++ [c'])
      (idxs (r1' r2) = idxs (r1 r2) ++ isext)
      ( i, i isext i tids r1)
      length isext K × size (tids r1 tids r2)
      ( i, (i < length (fst c') i (tids r1') (tids r2)))
      ( i, i tids r1 (i isext ¬ enabled idx_step c' i))
       isteps idx_step isext c0 c'.
Proof.
  intros Hval1 Hval2 Hdisj Hstep Hdisj' Hall.
  inversion Hdisj as [t1 t2 cs1 cs2 is1 is2 Hinter Hprefix |
                      t1 t2 cs1 cs2 is1 is2 Hinter Hnin1 |
                      ?].
  - simpl. destruct Hprefix as [Hprefix|Hprefix].
    × destruct cs2 as [|c cs2] using rev_ind.
      ** inversion Hprefix as [Hprecs ?]; subst.
         edestruct (refine_step_inv) as (cs1'&c&?&?&?&?&?&?&Heqcs1&?&?); eauto.
         exfalso. clear -Hprecs Heqcs1. simpl in ×. rewrite Heqcs1 in Hprecs.
         destruct Hprecs as (csext&Heqcs2). symmetry in Heqcs2.
         eapply app_eq_nil in Heqcs2 as (Hbad&_).
         eapply app_eq_nil in Hbad as (?&?).
         congruence.
      ** subst. destruct r1' as [v3 ts3 cs3 is3].
        edestruct (refine_step_disjoint_all_threads t1 cs1 is1 t2 cs2 is2 ts3 cs3 is3 c v3)
        as (c'&csext&isext&tsext&Heqcs3&Heqis3&Heqts3&Honlyts1&Hcountocc
            &Hnewtids&Hstep_enabled&Hval);
           eauto.
        { apply leibniz_equiv_iff in Hinter. eauto. }
        { rewrite prefix_of_op in Hall.
          - simpl in ×. rewrite last_snoc in Hall. simpl in Hall. eauto.
          - destruct Hprefix. simpl; eauto.
        }
        { inversion Hval1; eauto. }
        { inversion Hval2; eauto. }
        simpl. cs2, c, c', csext, isext.
        subst. simpl.
        simpl; split_and!; auto.
        *** rewrite prefix_of_op. simpl. auto; simpl. destruct Hprefix; auto.
        *** rewrite prefix_of_strict_op'; simpl; last eexists; eauto.
            rewrite prefix_of_op; simpl; auto.
            destruct Hprefix; auto.
        *** rewrite prefix_of_strict_op'; simpl; last eexists; eauto.
            rewrite prefix_of_op; simpl; auto.
            destruct Hprefix; auto.
        *** clear -Hcountocc Honlyts1 Hinter.

            cut (length isext sum_list_with (count_occ nat_eq_dec isext) (elements t1)).
            {
              intros Hle.
              etransitivity; first apply Hle.
              transitivity (K × size t1); last (rewrite size_union; last set_solver; eauto with × ).


              setoid_rewrite <-elem_of_elements in Honlyts1.
              setoid_rewrite <-elem_of_elements in Hcountocc.
              rewrite -size_natset_elements.
              clear Hinter t2 Hle.


              revert Honlyts1 Hcountocc.
              induction (elements t1).
              - intros. simpl. auto with ×.
              - intros. simpl in ×.
                etransitivity; first eapply (plus_le_compat _ K _ (sum_list_with (λ _, K) l)).
                × eapply Hcountocc. set_solver.
                × apply sum_list_with_mono. intros a' Hin. eapply Hcountocc. set_solver.
                × clear. induction l; simpl; first omega.
                  rewrite -mult_n_Sm.
                  rewrite plus_comm.
                  apply plus_le_compat; auto.
            }
            
            clear Hcountocc Hinter. induction isext; first (simpl; omega).
            simpl. etransitivity; first (apply le_n_S; eapply IHisext; set_solver).
            assert (t1 = {[a]} (t1 {[a]})) as →.
            {
              rewrite <-leibniz_equiv_iff.
              set_unfold. intros x'; split.
              - intros. case (decide (x' = a)); auto.
              - intros [eq|(?&?)]; first apply Honlyts1; auto.
            }
            rewrite ?elements_union_singleton; last set_solver.
            simpl. destruct nat_eq_dec; last congruence.
            rewrite -plus_Sn_m.
            apply plus_le_compat; auto.
            apply sum_list_with_mono. intros ? ?. destruct nat_eq_dec; auto.

        *** clear -Hnewtids Hall Hprefix Hval.
            destruct Hprefix as (?&_).
            rewrite prefix_of_op in Hall; simpl in *; auto.
            rewrite last_snoc in Hall; simpl in ×. intros i.
            assert (length (fst c) length (fst c')).
            { eapply valid_seq_tp_monotone_all_tl. rewrite app_assoc in Hval. eauto.
              set_solver+.
            }
            split.
            **** case (decide (i < length (fst c))); intros; first set_solver.
                 apply elem_of_union. left. apply elem_of_union. right. eapply Hnewtids.
                 omega.
            **** set_unfold.
                 intros [[Hin1|Hinext]|Hin2].
                 ***** eapply lt_le_trans; last eauto.
                       set_solver.
                 ***** eapply Hnewtids. auto.
                 ***** eapply lt_le_trans; last eauto.
                       set_solver.
        *** rewrite -app_assoc in Hval. eapply valid_cfg_extract'''; eauto.
            destruct Hval2; eauto.
    × destruct cs1 as [|c cs1] using rev_ind.
      ** edestruct (refine_step_inv) as (cs1'&c&?&?&?&?&?&?&Heqcs1&?&?); eauto.
         exfalso. subst. simpl in ×. destruct cs1'; simpl in *; congruence.
      ** subst. simpl in ×.
         assert (prefix_of_valid_seq t1 (cs1 ++ [c]) is1 (cs1 ++ [c]) is1).
         {
           econstructor. eauto. []; split; first rewrite app_nil_r; auto.
           set_solver+.
         }
        destruct r1' as [v3 ts3 cs3 is3].
        assert (v3 = snapshot) as →.
        {
          edestruct (refine_step_inv) as (?&?&?&?&?&?&?&?&Heqcs1&?&?); eauto.
        }
        assert (Refine snapshot t2 (cs1 ++ [c]) is1 Refine snapshot ts3 cs3 is3) as Hdisj''.
        {
          edestruct (refine_step_inv) as
              (cs1'&c'&c2&cspec&csext&i&ispec&isext
               &Heqcs1&?&Heqcs2&Heqidxs2&Hlen&Hin_spec&Hin_ext&Hnewtids&Hval); eauto.
          clear IHcs1. clear Hstep. simpl in ×.
          rewrite Heqcs2 Heqidxs2.
          apply app_inj_2 in Heqcs1 as (->&Heqcc'); auto.
          inversion Heqcc'; subst.
          replace (cs1' ++ c' :: cspec ++ csext ++ [c2]) with
                  ((cs1' ++ [c']) ++ (cspec ++ csext ++ [c2]));
            last (by rewrite //= -app_assoc //=).
          eapply (disjoint_up_closed_snapshot _ t1); eauto.
          - set_solver.
          - destruct Hval2; auto.
          - destruct Hval1; auto.
          - destruct Hval1; auto.
            rewrite -app_assoc.
            apply valid_seq_join; eauto.
          - rewrite -app_assoc.
            simpl. auto.
        }
        edestruct (refine_step_disjoint_all_threads t1 (cs1 ++ [c])
                                                    is1 t2 cs1 is1 ts3 cs3 is3 c snapshot)
        as (c'&csext&isext&tsext&Heqcs3&Heqis3&Heqts3&Honlyts1&Hcountocc
            &Hnewtids&Hstep_enabled&Hval);
           eauto.
        { apply leibniz_equiv_iff in Hinter. eauto. }
        { rewrite cfgs_of_prefix_of_op_l in Hall.
          - simpl in ×. rewrite last_snoc in Hall. simpl in Hall. eauto.
          - destruct Hprefix. simpl; eauto.
        }
        { inversion Hval1; eauto. }
        { inversion Hval1; eauto. }
        simpl. cs1, c, c', csext, isext.
        destruct Hprefix as ((csext0&Heqext0)&?&?&?).
        rewrite ?Heqcs3.
        rewrite ?Heqext0.
        split_and!; auto.
        *** rewrite cfgs_of_prefix_of_op_l. auto. simpl. eexists; eauto.
        *** rewrite prefix_of_strict_op'; auto; simpl; eauto;
             last ( (csext0 ++ csext), c'; rewrite ?app_assoc; auto; done).
             rewrite cfgs_of_prefix_of_op_l. auto. simpl. eexists; eauto.
        *** rewrite prefix_of_strict_op'; auto; simpl; eauto;
            last ( (csext0 ++ csext), c'; rewrite ?app_assoc; auto; done).
            rewrite Heqis3. rewrite ?prefix_of_op'''; simpl; auto.
            destruct Hval2. auto.
            rewrite Heqext0 in Hval1. destruct Hval1; auto.
            eexists; eauto. eexists; eauto.
        *** clear -Hcountocc Honlyts1 Hinter.

            cut (length isext sum_list_with (count_occ nat_eq_dec isext) (elements t1)).
            {
              intros Hle.
              etransitivity; first apply Hle.
              transitivity (K × size t1); last (rewrite size_union; last set_solver; eauto with × ).


              setoid_rewrite <-elem_of_elements in Honlyts1.
              setoid_rewrite <-elem_of_elements in Hcountocc.
              rewrite -size_natset_elements.
              clear Hinter t2 Hle.


              revert Honlyts1 Hcountocc.
              induction (elements t1).
              - intros. simpl. auto with ×.
              - intros. simpl in ×.
                etransitivity; first eapply (plus_le_compat _ K _ (sum_list_with (λ _, K) l)).
                × eapply Hcountocc. set_solver.
                × apply sum_list_with_mono. intros a' Hin. eapply Hcountocc. set_solver.
                × clear. induction l; simpl; first omega.
                  rewrite -mult_n_Sm.
                  rewrite plus_comm.
                  apply plus_le_compat; auto.
            }
            
            clear Hcountocc Hinter. induction isext; first (simpl; omega).
            simpl. etransitivity; first (apply le_n_S; eapply IHisext; set_solver).
            assert (t1 = {[a]} (t1 {[a]})) as →.
            {
              rewrite <-leibniz_equiv_iff.
              set_unfold. intros x'; split.
              - intros. case (decide (x' = a)); auto.
              - intros [eq|(?&?)]; first apply Honlyts1; auto.
            }
            rewrite ?elements_union_singleton; last set_solver.
            simpl. destruct nat_eq_dec; last congruence.
            rewrite -plus_Sn_m.
            apply plus_le_compat; auto.
            apply sum_list_with_mono. intros ? ?. destruct nat_eq_dec; auto.

        *** rewrite Heqcs3 in Hval. subst. clear -Hnewtids Hall Heqext0 Hval.
            rewrite cfgs_of_prefix_of_op_l in Hall; simpl in *; auto.
            rewrite last_snoc in Hall; simpl in ×. intros i.
            assert (length (fst c) length (fst c')).
            { eapply valid_seq_tp_monotone_all_tl. rewrite app_assoc in Hval. eauto.
              set_solver+.
            }
            split.
            **** case (decide (i < length (fst c))); intros; first set_solver.
                 apply elem_of_union. left. apply elem_of_union. right. eapply Hnewtids.
                 omega.
            **** set_unfold.
                 intros [[Hin1|Hinext]|Hin2].
                 ***** eapply lt_le_trans; last eauto.
                       set_solver.
                 ***** eapply Hnewtids. auto.
                 ***** eapply lt_le_trans; last eauto.
                       set_solver.
            **** eexists; eauto.
        *** rewrite Heqcs3 Heqis3 in Hval. rewrite -app_assoc in Hval.
            eapply valid_cfg_extract'''; eauto.
            destruct Hval1; eauto.
  - exfalso. subst. simpl in ×.
    destruct r1' as [v3 ts3 cs3 is3].
    edestruct (refine_step_inv) as
        (cs1'&c'&c2&cspec&csext&i&ispec&isext
         &Heqcs1&?&Heqcs2&Heqidxs2&Hlen&Hin_spec&Hin_ext&Hnewtids&?); eauto.
    subst. simpl in ×.
    inversion Hdisj' as [| |? ? ? ? is4 is5 Hinter' Hnin2 [Heqts Heqcs Heqis]]. subst; simpl in ×.
    clear -Hnin1 Hnin2 Hin_spec Hnewtids Hin_ext Heqis Hinter Hinter'.
    eapply (Hnin1 i).
    × eapply Hin_ext. set_solver.
    × rewrite -app_assoc in Heqis.
      apply app_inv_head in Heqis.
      subst. set_solver.
  - exfalso.
    subst. simpl in ×. clear -Hstep. inversion Hstep.
Qed.

Lemma refine_disjoint_prefix_idxs x y:
   x y
  refine_disjoint x y
  idxs x `prefix_of` idxs y
  idxs (x y) = idxs y.
Proof.
  intros (_&Hvalx) (_&Hvaly).
  inversion 1 as [? ? ? ? ? ? ? Hprefix| |]; subst; intros Hpre_isext.
  - simpl in ×. destruct Hprefix as [(?&?)|(Hpre_cs&isext'&Heq_isext'&?)]; eauto.
    × destruct Hpre_isext as (isext&->).
      rewrite /op /refine_op. simpl.
      destruct le_dec; auto.
      exfalso. eapply n. eapply prefix_of_length; eauto.
    × assert (is1 = is2) as →.
      {
        apply (anti_symm prefix_of); eauto. eexists; eauto.
      }
      rewrite /op /refine_op //=; destruct le_dec; auto.
  - simpl in ×. rewrite /op /refine_op //=. destruct le_dec; auto.
    exfalso. eapply n. rewrite app_length. omega.
  - simpl in ×. rewrite /op /refine_op //=. destruct le_dec; auto.
    simpl. apply (anti_symm prefix_of); auto. eexists; eauto.
Qed.

Lemma refine_disjoint_prefix_cfgs_post x y:
   x y
  refine_disjoint x y
  cfgs x `prefix_of` cfgs (x y).
Proof.
  intros (_&Hvalx) (_&Hvaly).
  inversion 1 as [? ? ? ? ? ? ? Hprefix| |]; subst.
  - simpl in ×. destruct Hprefix as [(Hpre_cs&isext'&Heq_isext'&?)
                                    |(Hpre_cs&isext'&Heq_isext'&?)]; eauto.
    × rewrite Heq_isext'.
      rewrite /op /refine_op. simpl.
      destruct le_dec; auto.
    × rewrite Heq_isext' in Hvalx ×.
      rewrite /op /refine_op. simpl.
      destruct le_dec as [l|n]; auto.
      simpl.
      destruct Hpre_cs as (csext&->).
      destruct csext as [|].
      ** rewrite app_nil_r; simpl; auto.
      ** rewrite app_length in l. simpl in ×. omega.
  - simpl. rewrite /op /refine_op. simpl.
      destruct le_dec; simpl; auto.
      eexists; eauto.
  - simpl. rewrite /op /refine_op. simpl.
    destruct le_dec as [l|n]; auto.
    simpl.
    assert (cs2 = []) as →.
    { destruct cs2; auto. rewrite app_length in l. simpl in ×. omega. }
    rewrite app_nil_r. auto.
Qed.

Lemma refine_disjoint_prefix_of_valid_idxs_post x y:
   x y
  refine_disjoint x y
  prefix_of_valid_seq (tids x) (cfgs x) (idxs x) (cfgs (x y)) (idxs (x y)).
Proof.
  intros (_&Hvalx) (_&Hvaly).
  inversion 1 as [? ? ? ? ? ? ? Hprefix| |]; subst.
  - simpl in ×. destruct Hprefix as [(Hpre_cs&isext'&Heq_isext'&?)
                                    |(Hpre_cs&isext'&Heq_isext'&?)]; eauto.
    × rewrite Heq_isext'.
      rewrite /op /refine_op. simpl.
      destruct le_dec as [l|n]; auto.
      ** eexists; eauto.
      ** exfalso. eapply n. eapply prefix_of_length. eauto.
    × rewrite Heq_isext' in Hvalx ×.
      rewrite /op /refine_op. simpl.
      destruct le_dec as [l|n]; auto.
      ** simpl.
         assert (cs1 = cs2) as →.
         {
           destruct Hpre_cs as (csext&->).
           destruct csext as [|].
           - rewrite app_nil_r; simpl; auto.
           - rewrite app_length in l. simpl in ×. omega.
         }
         econstructor; eauto.
         assert (is2 ++ isext' `prefix_of` is2).
         { eapply (valid_cfg_idx_prefix_link); eauto.
           eexists; eauto. }
         assert (is2 ++ isext' = is2) as →.
         {
           apply (anti_symm (prefix_of)); eauto.
           eexists; eauto.
         }
          []; split; rewrite ?app_nil_r; auto.
         set_solver+.
      ** simpl. split; auto.
          []; split; rewrite ?app_nil_r; auto.
         set_solver+.
  - simpl. rewrite /op /refine_op. simpl.
    destruct le_dec as [l|n]; auto.
    × simpl.
      econstructor.
      ** eexists; eauto.
      ** is2; split; auto.
    × simpl.
      simpl.
      econstructor; auto.
       []; split; rewrite ?app_nil_r; auto.
      set_solver+.
  - simpl. rewrite /op /refine_op. simpl.
    destruct le_dec as [l|n]; auto.
    × simpl.
      assert (cs2 = []) as →.
      { destruct cs2; auto. rewrite app_length in l. simpl in ×. omega. }
      rewrite app_nil_r.
      assert (is1 ++ is2 = is1) as →.
      {
        simpl in ×.
        rewrite app_nil_r in Hvalx.
        apply (anti_symm prefix_of); last (eexists; eauto).
        eapply valid_cfg_idx_prefix_link; eauto.
        eexists; eauto.
      }
      split; auto.
       []; split; rewrite ?app_nil_r; auto.
      set_solver+.
    × split; auto.
       []; split; rewrite ?app_nil_r; auto.
      set_solver+.
Qed.

Lemma refine_disjoint_prefix_of_idxs_post x y:
   x y
  refine_disjoint x y
  idxs x `prefix_of` (idxs (x y)).
Proof.
  intros; edestruct (refine_disjoint_prefix_of_valid_idxs_post x y) as (?&isext&?&?); eauto.
   isext. auto.
Qed.

Lemma refine_dra : DRAMixin refine_car'.
Proof.
  split.
  - by apply _.
  - do 2 destruct 1. rewrite /op /refine_op.
    destruct le_dec; constructor; setoid_subst; auto.
  - by destruct 1; constructor; setoid_subst.
  - destruct 1; simpl; intros (Hle&Hval); constructor; auto.
  - by intros x ? ? [].
  - intros x y Heq x' y' Heq'.
     inversion Heq; subst;
     inversion Heq'; subst.
     by intro.
  - intros x y (Hin1&Hv1) (Hin2&Hv2).
    destruct 1 as [? ? ? ? ? ? Hdisj [(Hprec&Hprei)|(Hprec&Hprei)]| | ].
    × rewrite /op /refine_op //=.
      assert (length cs1 length cs2) by (eapply prefix_of_length; eauto).
      destruct le_dec; try (exfalso; auto; done).
      constructor; simpl in ×.
      ** specialize (prefix_tp_monotone _ _ _ Hprec Hv2).
         destruct (last cs1), (last cs2);
           try (intros; exfalso; auto; done);
           try (rewrite Hin1; rewrite Hin2; set_solver+).
         intros ? i [Hin|Hin]%elem_of_union; auto.
         *** specialize (Hin1 i Hin); omega.
         *** setoid_subst. intros. eapply Hin2. set_solver.
      ** setoid_subst; auto.
    × rewrite /op /refine_op //=.
      assert (length cs2 length cs1) as Hle by (eapply prefix_of_length; eauto).
      destruct le_dec as [l | n].
      ** assert (cs1 = cs2).
         { destruct Hprec as (csext&->).
           rewrite app_length in l Hle.
           destruct csext; [| simpl in *; omega].
           by rewrite app_nil_r. }
         subst. constructor;
         simpl in *; auto. destruct (last cs2).
         *** intros i [|]%elem_of_union; eauto.
         *** rewrite Hin1 Hin2. set_solver.
      ** constructor.
         specialize (prefix_tp_monotone _ _ _ Hprec Hv1); simpl in ×.
         destruct (last cs2), (last cs1);
           try (intros; exfalso; auto; done);
           try (rewrite Hin1; rewrite Hin2; set_solver+);
           intros ? i [Hin|Hin]%elem_of_union; auto.
         *** specialize (Hin2 i Hin); omega.
         *** setoid_subst. inversion Hin.
         *** auto.
    × rewrite /op /refine_op //=.
      rewrite app_length.
      destruct le_dec; [| omega].
      constructor. simpl in ×.
      assert (prefix_of cs1 (cs1 ++ cs2)) as Hprec by (econstructor; eauto).
      specialize (prefix_tp_monotone _ _ _ Hprec Hv2); simpl in ×.
         destruct (last cs1), (last (cs1 ++ cs2));
           try (intros; exfalso; auto; done);
           try (rewrite Hin1; rewrite Hin2; set_solver+);
           intros ? i [Hin|Hin]%elem_of_union; auto.
         *** specialize (Hin1 i Hin); omega.
         *** setoid_subst. inversion Hin.
         *** auto.
    × rewrite /op /refine_op //=.
      rewrite app_length.
      destruct le_dec as [l | n].
      ** assert (cs2 = []).
         { destruct cs2; auto; simpl in *; try omega. }
         subst. rewrite app_nil_r in Hv1 Hin1. constructor;
         simpl in *; auto. destruct (last cs1).
         *** intros i [|]%elem_of_union; eauto.
         *** rewrite Hin1 Hin2. set_solver.
      ** constructor; simpl in ×.
         assert (prefix_of cs1 (cs1 ++ cs2)) as Hprec by (econstructor; eauto).
         specialize (prefix_tp_monotone _ _ _ Hprec Hv1); simpl in ×.
         destruct (last cs1), (last (cs1 ++ cs2));
           try (intros; exfalso; auto; done);
           try (rewrite Hin1; rewrite Hin2; set_solver+);
           intros ? i [Hin|Hin]%elem_of_union; auto.
         *** specialize (Hin2 i Hin); omega.
         *** setoid_subst. inversion Hin.
         *** auto.
  - intros x [? ?].
    destruct x; constructor; simpl in *; auto.
    destruct last.
    × inversion 1.
    × auto.
  - intros x y z.
    destruct x, y, z.
    rewrite /op /refine_op. simpl.
    repeat destruct le_dec; simpl in *;
    rewrite assoc;
    try (f_equal; eapply mapset_eq; set_solver);
    try (omega).
  - intros x y z [? ?] [? ?] [? ?].
    specialize (prefix_of_op'' x y); intros Hpop.
    inversion 1 as [? ? ? ? ? ? ? Hpre| ? ? ? ? ? ? ? Hpre |]; subst; simpl in ×.
    × destruct Hpop as [(?&->)|(?&->)]; intros.
      { destruct Hpre as [(?&?)|(?&?)]; eauto. }
      ** destruct z; destruct Hpre as [Hpre|Hpre].
         *** eapply (disjoint_down_closed_snapshot _ (t1 t2)); eauto; set_solver+.
         *** assert (cs2 = cs1) as →.
             {destruct Hpre as (?&?).
              eapply (anti_symm (prefix_of)); eauto.
             }
             
             assert (is2 = is1) asby (eapply prefix_of_valid_seq_inj; eauto).
             eapply (disjoint_down_closed_snapshot _ (t1 t2)); eauto; first set_solver+.
             split; nil; rewrite app_nil_r; auto.
             split; intros; auto; set_solver+.
      ** destruct z; destruct Hpre as [Hpre|Hpre].
         *** assert (cs1 = cs2) as →.
             { destruct Hpre as (?&?).
               eapply (anti_symm (prefix_of)); eauto.
             }
             
             assert (is1 = is2) asby (eapply prefix_of_valid_seq_inj; eauto).
             eapply (disjoint_down_closed_snapshot _ (t1 t2)); eauto; first set_solver+.
         *** eapply (disjoint_down_closed_snapshot _ (t1 t2)); eauto; first set_solver+.
             split; nil; rewrite app_nil_r; auto.
             split; intros; auto; set_solver+.
    × clear Hpop.
      rewrite prefix_of_op; simpl; last (eexists; eauto).
      intros. destruct z.
      eapply (disjoint_down_closed_master _ (t1 t2) _ _ cs1 (cs1++cs2) _ is1 (is1++is2)); eauto.
      ** set_solver.
      ** split; first eexists; eauto.
    × clear Hpop.
      rewrite prefix_of_op'''; eauto; simpl; try (eexists; eauto; done).
      remember (cs1 ++ cs2) as cs eqn:Heqcs.
      remember (is1 ++ is2) as ixs eqn:Heqis.
      inversion 1; subst.
      econstructor; eauto.
      set_solver.

  - intros x y z [? ?] [? ?] [? ?].
    specialize (prefix_of_valid_seq_op x y (tids x) (tids y)); intros Hpopxy.
    specialize (prefix_of_valid_seq_op y z (tids x tids y) (tids z)); intros Hpopyz.
    inversion 1 as [? ? ? ? ? ? ? Hpre| ? ? ? ? ? ? ? Hpre |]; subst; simpl in ×.
    × destruct Hpopxy as [(?&->)|(?&->)]; eauto.
      ** inversion 1 as [? ? ? ? ? ? ? Hpre2| ? ? ? ? ? ? ? Hpre2 |]; subst; simpl in ×.
         *** destruct Hpopyz as [(?&->)|(?&->)]; eauto.
             **** econstructor. set_solver.
                  destruct H7. destruct H10.
                  left. econstructor. etransitivity; eauto.
                  destruct H11 as (?&->&?).
                  destruct H12 as (?&->&?).
                  rewrite -app_assoc. eexists. split; eauto.
                  intros. set_solver.
             **** econstructor. set_solver.
                  left; auto.
         *** clear Hpopyz. rewrite prefix_of_op; eauto; last (eexists; eauto); simpl.
             destruct H7 as ((?&->)&?&(->&?)).
             rewrite -?app_assoc.
             econstructor; intros; set_solver.
      ** inversion 1 as [? ? ? ? ? ? ? Hpre2| ? ? ? ? ? ? ? ? |]; subst; simpl in ×.
         *** assert (cs2 `prefix_of` cs3 cs3 `prefix_of` cs2).
             {
               destruct Hpre2.
               *** left. destruct H7; destruct H10; etransitivity; eauto.
               *** edestruct (prefix_of_down_total cs2 cs3 cs1); eauto.
                   { destruct H7; eauto. }
                   { destruct H10; eauto. }
             }
             clear Hpopyz.
             edestruct prefix_of_op'' as [(?&->)|(?&->)]; simpl in *; eauto.
             **** econstructor. set_solver.
                  destruct Hpre2.
                  ***** left. destruct H12 as (?&?&->&?). econstructor; eauto.
                  eexists; split; eauto.
                  intros. set_solver.

                  ***** destruct Hpre as [Hpre|Hpre].
                  destruct H12.
                  assert (cs2 = cs1).
                  {
                    apply (anti_symm (prefix_of)). etransitivity; eauto.
                    destruct Hpre. eauto.
                  }
                  subst.
                  assert (cs3 = cs1).
                  {
                    apply (anti_symm (prefix_of)). etransitivity; eauto.
                    destruct Hpre. eauto.
                  }
                  subst.

                  assert (is3 = is1).
                  { eapply prefix_of_valid_seq_inj; eauto. econstructor.
                    eauto. eauto.
                  }
                  subst. left. econstructor. auto. []. split; rewrite ?app_nil_r. auto.
                  intros. set_solver.

                  right.
                  destruct H12 as (?&isx1&->&?).
                  assert (is2 `prefix_of` is3) as (x&->).
                  {
                    edestruct (prefix_of_down_total is2 is3 (is3++isx1)).
                    destruct H7 as (?&?&?&?); eexists; eauto.
                    eexists; eauto.
                    eauto.
                    eapply valid_cfg_idx_prefix_link; eauto.
                  }
                  destruct Hpre as (?&x'&?&?).
                  assert (x ++ isx1 = x') as <-. eapply app_inv_head. rewrite app_assoc; eauto.
                  econstructor. eauto.
                  eexists. split; eauto.
                  intros. set_solver.
             **** econstructor; first set_solver.
                  destruct Hpre2.
                  ***** destruct H12.
                  assert (cs2 = cs1).
                  {
                    apply (anti_symm (prefix_of)). etransitivity; eauto.
                    destruct H7; eauto.
                    etransitivity; eauto.
                  }
                  subst.
                  assert (cs3 = cs1).
                  {
                    apply (anti_symm (prefix_of)). etransitivity; eauto.
                    destruct H7; eauto.
                  }
                  subst.
                  assert (is2 = is1).
                  { eapply prefix_of_valid_seq_inj; eauto. }
                  subst. left. econstructor. auto. []. split; rewrite ?app_nil_r. auto.
                  intros. set_solver.

                  *****
                    right.
                  assert (is3 `prefix_of` is2) as (?&->).
                  {
                    edestruct (prefix_of_down_total is2 is3 is1).
                    destruct H7 as (?&?&?&?); eexists; eauto.
                    destruct H12 as (?&?&?&?); eauto.
                    eexists. eauto.
                    eapply valid_cfg_idx_prefix_link; eauto.
                    eauto.
                  }
                  destruct H11 as (?&->).
                  destruct H12 as ((?&->)&?&Heq&?).
                  destruct H7 as (?&?&->&?).
                  econstructor. eauto. eexists. split; eauto. intros i Hf.
                  eapply elem_of_union in Hf as [?|?].
                  set_solver.
                  assert (x ++ x3 = x2). { eapply app_inv_head. rewrite app_assoc. eauto. }
                  intros Hf. set_solver.
         *** clear Hpopyz.
             assert (cs2 `prefix_of` (cs1 ++ cs3)).
             {
               destruct H7 as (?&?); etransitivity; eauto.
               econstructor; auto.
             }
             rewrite prefix_of_op; eauto.
             simpl.
             econstructor; set_solver.
    × clear Hpopyz.
      rewrite prefix_of_op; simpl; last (eexists; eauto; done).
      inversion 1; subst.
      rewrite prefix_of_op'''; simpl; eauto; try (eexists; eauto; done);
      rewrite H9; rewrite H11; eauto.
      econstructor; set_solver.
    × clear Hpopyz.
      rewrite prefix_of_op'''; simpl; eauto; try (eexists; eauto; done).
      inversion 1; subst.
      simpl in ×.
      assert (cs0 `prefix_of` cs1 cs1 `prefix_of` cs0) as [?|?].
      {
        eapply (prefix_of_down_total _ _ (cs0 ++ cs3)); try (eexists; eauto).
      }
      **
        assert (is0 `prefix_of` is1).
        {
        edestruct (prefix_of_down_total is0 is1 (is0 ++ is3)); try (eexists; eauto; done); eauto.
        eapply valid_cfg_idx_prefix_link; eauto.
        }
        rewrite prefix_of_op'''; simpl; eauto; try (eexists; eauto; done).
        rewrite H10 H12.
        econstructor. set_solver.
        destruct H11 as (isext&->). assert (is3 = isext ++ is2).
        eapply app_inv_head. rewrite app_assoc.
        eauto.
        intros. set_solver.

      **
        assert (is1 `prefix_of` is0) as (isext&->).
        {
        edestruct (prefix_of_down_total is0 is1 (is0 ++ is3)); try (eexists; eauto; done); eauto.
        eapply valid_cfg_idx_prefix_link; eauto.
        }

        rewrite prefix_of_op; simpl; eauto; try (eexists; eauto; done); [].
        econstructor. set_solver.
        assert (is2 = isext ++ is3).
        eapply app_inv_head. rewrite app_assoc.
        eauto.
        intros. set_solver.

  - intros x y Hdisj; inversion Hdisj; subst; econstructor; eauto; set_solver.
  - intros x y (?&Hval1) (?&Hval2) Hdisj.
    destruct x, y. simpl in ×.
    assert (prefix_of_valid_seq tids0 cfgs0 idxs0 cfgs1 idxs1
            prefix_of_valid_seq tids1 cfgs1 idxs1 cfgs0 idxs0).
    {
      inversion Hdisj; auto.
      × left. econstructor; try (eexists; eauto).
      × right. econstructor; try (eexists; eauto).
    }
    assert (prefix_of_valid_seq tids1 cfgs1 idxs1 cfgs0 idxs0
            prefix_of_valid_seq tids0 cfgs0 idxs0 cfgs1 idxs1) by naive_solver.
    edestruct (prefix_of_valid_seq_op) as [(Hp1&->)|(Hp1&->)]; eauto; simpl in *;
    edestruct (prefix_of_valid_seq_op) as [(Hp2&->)|(Hp2&->)]; eauto; simpl in ×.
    × assert (cfgs0 = cfgs1) as →.
      {
        apply (anti_symm prefix_of); destruct Hp1, Hp2; eauto.
      }
      assert (idxs0 = idxs1) as →.
      {
        apply (anti_symm prefix_of).
        ** destruct Hp1 as (?&?&->&?), Hp2 as (?&?&->&?);
           try (econstructor; eexists; eauto).
        ** destruct Hp2 as (?&?&->&?), Hp1 as (?&?&->&?);
           try (econstructor; eexists; eauto).
      }
      destruct view0, view1; f_equal; set_solver.
    × destruct view0, view1; f_equal; set_solver.
    × destruct view0, view1; f_equal; set_solver.
    × assert (cfgs0 = cfgs1) as →.
      {
        apply (anti_symm prefix_of); destruct Hp1, Hp2; eauto.
      }
      assert (idxs0 = idxs1) as →.
      {
        apply (anti_symm prefix_of).
        ** destruct Hp2 as (?&?&->&?), Hp1 as (?&?&->&?);
           try (econstructor; eexists; eauto).
        ** destruct Hp1 as (?&?&->&?), Hp2 as (?&?&->&?);
           try (econstructor; eexists; eauto).
      }
      destruct view0, view1; f_equal; set_solver.
  - intros x Hval. destruct x. rewrite /core /refine_core; simpl.
    destruct view0.
    × rewrite -{2}(app_nil_r cfgs0).
      rewrite -{2}(app_nil_r idxs0).
      econstructor; set_solver.
    × econstructor; try set_solver.
      left. split; []; rewrite ?app_nil_r; auto.
      split; auto. set_solver.
  - intros x Hval. destruct x. rewrite /core /refine_core; simpl.
    rewrite /op /refine_op. simpl.
    destruct le_dec; last omega. destruct view0; auto; f_equal; set_solver.
  - intros x Hval. destruct x. rewrite /core /refine_core; simpl. auto.
  - intros x y. (core y).
    intros Hvalx Hvaly Hdisj. split_and!.
    × destruct x, y. rewrite /core /refine_core /op /refine_op //=.
      destruct le_dec; simpl; f_equal; set_solver.
    × destruct y. rewrite /core /refine_core //=.
      econstructor; simpl.
      ** destruct (last cfgs0); intros; set_solver.
      ** destruct Hvaly; eauto.
    × destruct Hdisj as [? ? ? ? ? ? ? Hpre | | ]; rewrite /core /refine_core //=.
      ** econstructor. set_solver.
         destruct Hpre as [(?&?&->&?)|(?&?&->&?)]; [left | right];
         econstructor; eauto;
         eexists; split; auto; try set_solver.
      ** econstructor. set_solver.
         left. econstructor; eauto; eexists; split; eauto.
         set_solver.
      ** econstructor. set_solver.
         right. econstructor; eauto; eexists; split; eauto.
         set_solver.
  - intros x y Hvalx Hvaly Hdisjcore.
    destruct x, y; rewrite /core /refine_core; simpl in *;
    rewrite /op /refine_op; destruct le_dec; simpl; f_equal;
    rewrite -leibniz_equiv_iff; rewrite ?right_id; auto.
Qed.

  Canonical Structure refineDR : draT := DRAT (refine_car') refine_dra.
  Instance refine_car'_empty : Empty (refine_car') := Refine snapshot [] [].
  Instance refine_discrete: CMRADiscrete (validityR (refineDR)).
  Proof.
    by apply: _.
  Qed.
  Notation refine_cmra := (validity (refineDR)).

  Global Instance refine_empty : Empty (refine_cmra) := to_validity (refine_car'_empty).
  Lemma refine_unit: UCMRAMixin (refine_cmra).
  Proof.
    split.
    - econstructor; unfold refine_car'_empty; simpl; auto.
      econstructor.
    - intro x. destruct x. rewrite /empty /refine_empty /refine_car'_empty //=.
      rewrite /op /cmra_op //= /validity_op //=.
      econstructor.
      × split.
        ** rewrite /valid //= /validity_valid.
           naive_solver.
        ** rewrite /valid //= /validity_valid.
           intros. split_and!; auto.
           *** econstructor; unfold refine_car'_empty; simpl; auto.
               econstructor.
           *** destruct validity_car.
               destruct view0.
               **** replace cfgs0 with ([] ++ cfgs0) by apply app_nil_l.
                    replace idxs0 with ([] ++ idxs0) by apply app_nil_l.
                    econstructor; try set_solver.
               **** econstructor; try set_solver.
                    left. econstructor. try (eexists; eauto).
                     idxs0; split; auto.
                    set_solver.
      × inversion 1.
        simpl. rewrite /op /dra_op //= /refine_op //=.
        destruct validity_car. simpl. destruct view0; f_equal; auto;
        set_solver.
    - intros y Heq.
      econstructor.
      × split; intros ?; eapply (cmra_discrete_valid_iff 0).
        ** rewrite -Heq; auto.
        ** rewrite Heq; auto.
      × intros Hval. inversion Heq. destruct y.
        simpl in ×. auto.
    - rewrite /pcore /cmra_pcore //= /validity_pcore //=. econstructor.
      rewrite /empty /refine_empty /refine_car'_empty //=.
  Qed.

  Canonical Structure refine_ucmra : ucmraT :=
  (UCMRAT refine_cmra (cmra_cofe_mixin _) (cmra_mixin _) refine_unit).

  Definition prim_step_nofork : (relation (expr Λ × state Λ)) :=
    λ c c', prim_step (fst c) (snd c) (fst c') (snd c') None.

    Lemma idx_step_diff j c c' i (e: expr Λ):
      idx_step i c c'
      nth_error (fst c) j = Some e
      i j
      nth_error (fst c') j = Some e.
    Proof.
      rewrite idx_step_equiv. intros Hidx. revert j e. induction Hidx; intros.
       - destruct j; [ omega | auto ].
         simpl in ×. rewrite nth_error_app1; auto.
         apply nth_error_Some; congruence.
       - destruct j; simpl in *; [ congruence | eapply IHHidx; auto ].
    Qed.

    Lemma nostep_fixed_extension cfgs1 e ts1 ts2 σ csext ixs1 ixs_ext n:
      valid_cfg_idx_seq (cfgs1 ++ [(ts1 ++ e :: ts2, σ)] ++ csext) (ixs1 ++ ixs_ext)
      length ixs1 = length cfgs1
      length ts1 = n
      n ixs_ext
       ts1' ts2' σ', length ts1' = n
                      last (cfgs1 ++ [(ts1 ++ e :: ts2, σ)] ++ csext) =
                      Some (ts1' ++ e :: ts2', σ').
    Proof.
      induction csext as [|c'] using rev_ind.
      - simpl. rewrite last_snoc; eauto.
      - intros (is1a&is1b&?&?&?&Histeps)%valid_cfg_extract'' Hlen.
        apply app_inj_1 in H as (->&->); auto.
        clear -Histeps.
        revert ts1 ts2 σ Histeps.
        induction is1b.
        × intros. inversion Histeps.
          subst. rewrite ?app_assoc last_snoc. eauto.
        × intros. inversion Histeps.
          subst.
          assert (nth_error (fst y) (length ts1) = Some e) as (ts1'&ts2'&Heq&Hlen)%nth_error_split.
          {
            eapply (idx_step_diff (length ts1)); eauto.
            { rewrite /fst. rewrite nth_error_app2; auto.
              replace (length ts1 - length ts1) with 0 by (omega); eauto. }
            { set_solver. }
          }
          destruct y as (yts&yσ).
          subst. edestruct (IHis1b ts1' ts2') as (ts1''&ts2''&σ''&Hlen''&Hlast); eauto.
          { rewrite -Heq. eauto. }
          { set_solver. }
           ts1'', ts2'', σ''.
          split; auto.
          rewrite ?assoc ?last_snoc in Hlast ×.
          auto.
        × rewrite Hlen. auto.
    Qed.

Lemma valid_seq_join' cs1 c is1 cs2 is2:
  valid_cfg_idx_seq (cs1) is1
  valid_cfg_idx_seq ([c] ++ cs2) is2
  last cs1 = Some c
  valid_cfg_idx_seq (cs1 ++ cs2) (is1 ++ is2).
Proof.
  destruct cs1 as [| c' cs1] using rev_ind.
  - simpl. congruence.
  - rewrite last_snoc. intros Hval1 Hval2. inversion 1. subst.
    rewrite -assoc. apply valid_seq_join; eauto.
Qed.

  Lemma prim_step_nofork_valid_cfg K' ts1 ts2 e sσ e' sσ':
    1 K'
    nsteps (prim_step_nofork) K' (e, sσ) (e', sσ')
     cs ixs,
    valid_cfg_idx_seq ([(ts1 ++ e :: ts2, sσ)] ++ cs ++ [(ts1 ++ e' :: ts2, sσ')]) ixs
      length ixs = K' i, i ixs i = length ts1.
  Proof.
    intros Hle Hnsteps.
    remember (e, sσ) as c eqn:Heqc.
    remember (e', sσ') as c' eqn:Heqc'.
    revert e sσ e' sσ' Heqc Heqc' Hle ts1 ts2. induction Hnsteps as [|???? Hprim Hnsteps IH].
    - intros; omega.
    - intros e sσ e' sσ' → → Hle ts1 ts2.
      destruct y as (e'', sσ'').
      destruct n.
      × [], [length ts1].
        split_and!; auto; last set_solver+.
        simpl. econstructor; last econstructor.
        rewrite /prim_step_nofork in Hprim.
        simpl in ×.
        inversion Hnsteps. subst.
        econstructor; simpl; eauto.
        rewrite ?app_nil_r //=.
      × edestruct IH as (cs'&ixs'&Hval&Hlen&Hin); eauto.
        { omega. }
         ((ts1 ++ e'' :: ts2, sσ'') :: cs').
         (length ts1 :: ixs').
        split_and!; simpl; auto.
        ** econstructor; simpl in *; last eauto.
           econstructor; eauto. rewrite ?app_nil_r. auto.
        ** intros i. clear -Hin. set_solver.
  Qed.

  Lemma count_occ_le_length {A: Type} (a: A) l eq_dec:
    count_occ eq_dec l a length l.
  Proof.
    induction l; auto.
    simpl. destruct eq_dec; omega.
  Qed.

  Lemma snap_master_stepshift_nofork i e e' ts ts' sσ sσ' sσ'' cs cs' ixs ixs' K':
    nth_error ts i = Some e
    (1 K' K' K)
    nsteps (prim_step_nofork) K' (e, sσ') (e', sσ'')
    (to_validity (Refine master (cs' ++ [(ts', sσ')]) ixs') : refine_cmra) #
    (to_validity (Refine snapshot {[i]} (cs ++ [(ts, sσ)]) ixs) : refine_cmra) ~~>>:
    (λ r rl, cs'' ts'' ixs'',
        nth_error ts'' i = Some e'
        r to_validity (Refine master (cs'' ++ [(ts'', sσ'')]) ixs'')
        rl to_validity (Refine snapshot {[i]} (cs'' ++ [(ts'', sσ'')]) ixs'')).
Proof.
  intros Hlookup K_bounds K'_steps.
  eapply cmra_total_step_updatePn z.
  rewrite (comm _ (to_validity _)).
  intros Hval.
  inversion Hval as (Hvalop&?&Hdisj_prod_z).
  inversion Hvalop as (Hval_snap&Hval_master&Hdisj_xy).
  inversion Hdisj_xy as [ | ?????? Hinter Hvalid_ext (Heqt&Heqcs_ext) (Heqcs&Heqcs') |].
  subst.
  rewrite //= -Heqcs' in Hdisj_prod_z.
  rewrite prefix_of_op in Hdisj_prod_z; last (eexists; auto).
  rewrite //= right_id_L in Hdisj_prod_z.
  inversion Hdisj_prod_z as [ | |
                              ?????? Hinter_z Hvalid_ext_z [Heqt_z Heqcs_ext_z Heqixs_ext_z]
                                     (Heq_vz)].
  subst.
  edestruct Hval_master as (_&Hval_cfg_master); simpl in ×.
  rewrite -Heqcs' in Hval_cfg_master.
  edestruct (nth_error_split ts) as (ts1&ts2&Heq_ts&Hlen); eauto.
  rewrite Heq_ts in Hval_cfg_master.
  edestruct (nostep_fixed_extension) as (ts1'&ts2'&sσ0'&Hlen'&Hlast'); first (rewrite assoc); eauto.
  { edestruct Hval_snap. simpl in ×. symmetry; eapply valid_cfg_idx_length4; eauto. }
  { set_solver. }
  edestruct (prim_step_nofork_valid_cfg K' ts1' ts2') as
      (cstep&ixstep&Hval_step&Hlen_step&Hidxs_step); eauto.
  { omega. }
  assert (sσ0' = sσ') as →.
  { rewrite -Heq_ts in Hlast'. rewrite app_assoc Heqcs' in Hlast'.
    rewrite last_snoc in Hlast'. inversion Hlast'; auto. }
   (to_validity {| view := master; tids := ∅;
                         cfgs := cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 ++ cstep
                                   ++ [(ts1' ++ e' :: ts2', sσ'')];
                         idxs := ixs ++ is2 ++ ixstep |}).
   (to_validity {| view := snapshot; tids := {[i]};
                         cfgs := cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 ++ cstep
                                   ++ [(ts1' ++ e' :: ts2', sσ'')];
                         idxs := ixs ++ is2 ++ ixstep |}).
  split_and!.
  - (cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 ++ cstep).
     (ts1' ++ e' :: ts2').
     (ixs ++ is2 ++ ixstep).
    split_and!.
    × rewrite nth_error_app2. replace (i - length ts1') with 0 by omega.
      auto. omega.
    × rewrite ?app_assoc. reflexivity.
    × rewrite ?app_assoc. reflexivity.
  - split_and!.
    × constructor; split_and!.
      ** simpl. rewrite ?app_assoc app_comm_cons ?app_assoc last_snoc. set_solver+.
      ** rewrite /cfgs /idxs.
         eapply valid_seq_join' in Hval_cfg_master; eauto.
         *** rewrite ?app_assoc in Hval_cfg_master ×. auto.
         *** rewrite -?app_assoc. auto.
      ** split_and!.
         *** simpl. rewrite ?app_assoc app_comm_cons ?app_assoc last_snoc. set_unfold.
             intros ? →. rewrite app_length. simpl. omega.
         *** rewrite /cfgs /idxs.
             eapply valid_seq_join' in Hval_cfg_master; eauto.
             **** rewrite ?app_assoc in Hval_cfg_master ×. auto.
             **** rewrite -?app_assoc. auto.
      ** simpl.
         rewrite -[P in {| view := _; tids := _; cfgs := P |}]app_nil_r.
         rewrite -[P in {| view := _; tids := _; cfgs := _; idxs := P |}]app_nil_r.
         eapply (master_snapshot_disjoint _ _ _ [] _ []).
         *** set_solver.
         *** set_solver.
    × auto.
    × simpl. rewrite prefix_of_op; simpl; last ( []; rewrite ?app_nil_r; done).
      rewrite -Heq_vz.
      rewrite ?assoc.
      rewrite -Heqixs_ext_z.
      rewrite app_comm_cons.
      rewrite assoc.
      rewrite app_comm_cons. rewrite assoc.
      rewrite -assoc //= Heq_ts in Heqcs_ext_z .
      rewrite -Heqcs_ext_z.
      rewrite -?app_assoc.
      econstructor.
      ** set_solver.
      ** set_solver.
  - rewrite Heq_ts. econstructor.
     × split; intros Hval'.
       ** econstructor.
         *** simpl. rewrite ?app_assoc app_comm_cons ?app_assoc last_snoc. set_unfold.
             intros ? →. rewrite app_length. simpl. omega.
         *** rewrite /cfgs /idxs.
             eapply valid_seq_join' in Hval_cfg_master; eauto.
             **** rewrite ?app_assoc in Hval_cfg_master ×. auto.
             **** rewrite -?app_assoc. auto.
       ** rewrite -Heq_ts. auto.
     × intros Hval'.
       rewrite /validity_car /to_validity.
       eapply (snap_spec_step {[i]} {[i]} cs _ cs2 _ ixs is2).
       ** rewrite -assoc in Hval_cfg_master. eapply valid_seq_split in Hval_cfg_master; eauto.
            destruct Hval' as (?&Hval_cfg'); eapply valid_cfg_idx_length4; eauto.
       ** clear -Hvalid_ext. set_solver.
       ** assert ( cs0, cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 =
                              cs0 ++ [(ts1' ++ e :: ts2', sσ')]) as (cs0'&Heq_cs0').
          { destruct cs2 as [| c' cs2'] using rev_ind.
            - rewrite ?app_nil_r last_snoc in Hlast' ×. inversion Hlast'. subst.
              eexists; eauto.
            - rewrite ?app_assoc last_snoc in Hlast'. inversion Hlast'. subst.
              rewrite ?assoc. eexists; eauto.
          }
          rewrite Heq_cs0'.
          rewrite ?app_assoc. rewrite -(app_assoc cs) Heq_cs0'.
          rewrite -?app_assoc. rewrite -[P in _ {| view := _; tids := P; |}]right_id_L.
          rewrite (app_assoc ixs).
          eapply snap_block_step; eauto.
          *** clear -Hidxs_step Hlen'. set_solver.
          ***

            intros. transitivity (length (ixstep)); first eapply count_occ_le_length.
            omega.
          *** set_solver.
          *** split.
              **** set_solver+.
              **** clear. rewrite ?app_length //=. omega.
Qed.

Lemma valid_seq_tp_monotone_last c' cs1 cs2 c'' is1:
  valid_cfg_idx_seq (cs1 ++ [c'] ++ cs2) is1
  last (cs1 ++ [c'] ++ cs2) = Some c''
  length (fst c') length (fst c'').
Proof.
  destruct cs2 as [| c''' cs2'] using rev_ind.
  - simpl. rewrite ?last_snoc. inversion 2. auto.
  - rewrite ?app_assoc last_snoc. intros Hval. inversion 1. subst.
    eapply valid_seq_tp_monotone_all_tl; eauto. set_solver.
Qed.

Lemma snap_master_simple_fork i e ef e' ts ts' sσ sσ' sσ'' cs cs' ixs ixs':
  K 0
  nth_error ts i = Some e
    prim_step e sσ' e' sσ'' (Some ef)
    (to_validity (Refine master (cs' ++ [(ts', sσ')]) ixs') : refine_cmra) #
    (to_validity (Refine snapshot {[i]} (cs ++ [(ts, sσ)]) ixs) : refine_cmra) ~~>>:
    (λ r rl, i' cs'' ts'' ixs'',
        nth_error ts'' i = Some e'
        nth_error ts'' i' = Some ef
        r to_validity (Refine master (cs'' ++ [(ts'', sσ'')]) ixs'')
        rl (to_validity (Refine snapshot {[i]} (cs'' ++ [(ts'', sσ'')]) ixs'') : refine_cmra)
              to_validity (Refine snapshot {[i']} (cs'' ++ [(ts'', sσ'')]) ixs'')).
Proof.
  intros Knz Hlookup step_fork.
  eapply cmra_total_step_updatePn z.
  rewrite (comm _ (to_validity _)).
  intros Hval.
  inversion Hval as (Hvalop&Hvalz&Hdisj_prod_z).
  inversion Hvalop as (Hval_snap&Hval_master&Hdisj_xy).
  inversion Hdisj_xy as [ | ?????? Hinter Hvalid_ext (Heqt&Heqcs_ext) (Heqcs&Heqcs') |].
  subst.
  rewrite //= -Heqcs' in Hdisj_prod_z.
  rewrite prefix_of_op in Hdisj_prod_z; last (eexists; auto).
  rewrite //= right_id_L in Hdisj_prod_z.
  inversion Hdisj_prod_z as [ | |
                              ?????? Hinter_z Hvalid_ext_z [Heqt_z Heqcs_ext_z Heqixs_ext_z]
                                     (Heq_vz)].
  subst.
  edestruct Hval_master as (Hmaximal&Hval_cfg_master); simpl in ×.
  rewrite -Heqcs' in Hval_cfg_master.
  edestruct (nth_error_split ts) as (ts1&ts2&Heq_ts&Hlen); eauto.
  rewrite Heq_ts in Hval_cfg_master.
  edestruct (nostep_fixed_extension) as (ts1'&ts2'&sσ0'&Hlen'&Hlast'); first (rewrite assoc); eauto.
  { edestruct Hval_snap. simpl in ×. symmetry; eapply valid_cfg_idx_length4; eauto. }
  { set_solver. }
   (to_validity {| view := master; tids := ∅;
                         cfgs := cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2
                                   ++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')];
                         idxs := ixs ++ is2 ++ [i] |}).
   (to_validity {| view := snapshot; tids := {[i]} {[length (ts1' ++ e' :: ts2')]};
                         cfgs := cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2
                                   ++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')];
                         idxs := ixs ++ is2 ++ [i] |}).
  assert (sσ0' = sσ') as →.
  { rewrite -Heq_ts in Hlast'. rewrite app_assoc Heqcs' in Hlast'.
    rewrite last_snoc in Hlast'. inversion Hlast'; auto. }
  split_and!.
  - (length (ts1' ++ e' :: ts2')).
     (cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2).
     (ts1' ++ e' :: ts2' ++ [ef]).
     (ixs ++ is2 ++ [i]).
    split_and!.
    × rewrite nth_error_app2. replace (i - length ts1') with 0 by omega.
      auto. omega.
    × rewrite app_comm_cons. rewrite app_assoc. rewrite nth_error_app2.
      replace (length (ts1' ++ e' :: ts2') - length (ts1' ++ e' :: ts2')) with 0 by omega.
      auto. omega.
    × rewrite ?app_assoc. reflexivity.
    × rewrite ?app_assoc.
      econstructor.
      ** split.
         *** intros Hval'.
             econstructor. destruct Hval' as (Hval1&Hval2). simpl in ×. econstructor.
             **** rewrite ?last_snoc in Hval1 ×. set_solver.
             **** simpl. auto.
             **** split; auto.
                  edestruct Hval' as (Hval1&Hval2). simpl in ×. econstructor; auto.
                  rewrite ?last_snoc in Hval1 ×. set_solver.
                  simpl. econstructor. set_unfold. rewrite ?app_length. simpl.
                  intros ?. omega.
                  left. econstructor. eauto. []. split; eauto using app_nil_r.
                  set_solver+.
         *** intros Hval_op. destruct Hval_op as ((Hl1&Hval1)&(Hl2&Hval2)&?Hdisj). econstructor; auto.
             rewrite ?last_snoc //= in Hl1 Hl2 ×.
             set_solver.
      ** intros ?Hval. simpl. rewrite ?prefix_of_op //=.
  -
    assert (valid_cfg_idx_seq ((ts1' ++ e :: ts2', sσ') :: (ts1' ++ e' :: ts2' ++ [ef], sσ'') :: nil)
                              [i]).
    { econstructor. econstructor; eauto. simpl; eauto.
      econstructor. }
    split_and!.
    × constructor; split_and!.
      ** rewrite /cfgs /tids.
         rewrite ?app_assoc last_snoc. set_solver+.
      ** rewrite /cfgs /idxs.
         eapply valid_seq_join' in Hval_cfg_master; rewrite ?app_assoc; eauto.
         *** rewrite -?app_assoc. auto.
      ** split_and!.
         *** rewrite /cfgs /tids ?app_assoc ?last_snoc. set_unfold.
             intros ? [->| ->]; rewrite ?app_length //= ?app_length //=;
             omega.
         *** rewrite /cfgs /idxs.
             eapply valid_seq_join' in Hval_cfg_master; rewrite ?app_assoc; eauto.
             **** rewrite -?app_assoc. auto.
      ** simpl.
         rewrite -[P in {| view := _; tids := _; cfgs := P |}]app_nil_r.
         rewrite -[P in {| view := _; tids := _; cfgs := _; idxs := P |}]app_nil_r.
         eapply (master_snapshot_disjoint _ _ _ [] _ []).
         *** set_solver.
         *** set_solver.
    × auto.
    × simpl. rewrite prefix_of_op; simpl; last ( []; rewrite ?app_nil_r; done).
      rewrite -Heq_vz.
      rewrite ?app_assoc.
      rewrite -Heqixs_ext_z.
      rewrite app_comm_cons.
      rewrite app_comm_cons. rewrite app_assoc.
      rewrite -assoc //= Heq_ts in Heqcs_ext_z .
      rewrite app_assoc.
      rewrite -Heqcs_ext_z.
      rewrite -?app_assoc.
      econstructor.
      ** clear -Heq_ts Hval_cfg_master Heqcs_ext_z Heqcs' Hinter_z Heq_vz Hvalz Hlast'.
         assert ( validity_car z) as Hval_vcz by (destruct z; auto).
         rewrite -Heq_vz in Hval_vcz.
         destruct Hval_vcz as (Hmaximal&Hval_cs1). simpl in Hmaximal, Hval_cs1.
         destruct cs1 as [| c1' cs1' _] using rev_ind.
         *** simpl in *; set_solver.
         *** rewrite last_snoc in Hmaximal. rewrite -?assoc //= -Heqcs_ext_z in Hval_cfg_master.
             assert (length (c1'.1) length (ts1' ++ e :: ts2')).

             rewrite -?app_assoc in Hval_cfg_master.
             eapply valid_seq_tp_monotone_last in Hval_cfg_master; last first.
             **** rewrite assoc Heqcs_ext_z. rewrite //= in Hlast'. rewrite Hlast'. auto.
             **** auto.
             **** rewrite ?left_id. set_unfold. intros i' (Hnot1&[->| ->]).
                  set_solver.
                  edestruct le_not_lt; eauto.
                  specialize (Hmaximal _ Hnot1). rewrite ?app_length //= in Hmaximal ×.
      ** set_solver.

  -
    assert (valid_cfg_idx_seq ((ts1' ++ e :: ts2', sσ') :: (ts1' ++ e' :: ts2' ++ [ef], sσ'') :: nil)
                              [i]).
    { econstructor. econstructor; eauto. simpl; eauto.
      econstructor. }
    rewrite Heq_ts. econstructor.
     × split; intros Hval'.
       ** econstructor.
         *** rewrite ?app_assoc last_snoc /tids. set_unfold.
             rewrite ?app_length //= ?app_length //=. intros ? [-> | ->]; omega.
         *** rewrite /cfgs /idxs.
             eapply valid_seq_join' in Hval_cfg_master; rewrite ?app_assoc; eauto.
             **** rewrite -?app_assoc. auto.
       ** rewrite -Heq_ts. auto.
     × intros Hval'.
       rewrite /validity_car /to_validity.
       eapply (snap_spec_step {[i]} ({[i]} {[length (ts1' ++ e' :: ts2')]}) cs _ cs2 _ ixs is2).
       ** rewrite -assoc in Hval_cfg_master. eapply valid_seq_split in Hval_cfg_master; eauto.
            destruct Hval' as (?&Hval_cfg'); eapply valid_cfg_idx_length4; eauto.
       ** clear -Hvalid_ext. set_solver.
       ** assert ( cs0, cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 =
                              cs0 ++ [(ts1' ++ e :: ts2', sσ')]) as (cs0'&Heq_cs0').
          { destruct cs2 as [| c' cs2'] using rev_ind.
            - rewrite ?app_nil_r last_snoc in Hlast' ×. inversion Hlast'. subst.
              eexists; eauto.
            - rewrite ?app_assoc last_snoc in Hlast'. inversion Hlast'. subst.
              rewrite ?assoc. eexists; eauto.
          }
          rewrite Heq_cs0'.
          rewrite ?app_assoc. rewrite -(app_assoc cs) Heq_cs0'.
          rewrite -?app_assoc. rewrite -[P in _ {| view := _; tids := P; |}]right_id_L.
          rewrite (app_assoc ixs).
          rewrite right_id_L.
          rewrite app_assoc.
          rewrite -(app_nil_l [(ts1' ++ e' :: ts2' ++ [ef], sσ'')]).
          rewrite -app_assoc.
          eapply (snap_block_step {[i]} {[length (ts1' ++ e' :: ts2')]}); eauto.
          *** set_solver+.
          *** simpl. intros; destruct nat_eq_dec. omega. omega.
          *** set_solver+.
          *** set_unfold. split.
              **** intros →. rewrite ?app_length //= ?app_length //=. omega.
              **** rewrite ?app_length //= ?app_length //=. omega.
Qed.

Lemma snap_master_fork_pre_post i n1 n2 e0 e ef e' e'' ts ts' sσ0 sσ sσ' sσ'' sσ''' cs cs' ixs ixs':
  K S (n1 + n2)
  1 n1
  1 n2
  nth_error ts i = Some e0
    nsteps prim_step_nofork n1 (e0, sσ) (e, sσ')
    prim_step e sσ' e' sσ'' (Some ef)
    nsteps prim_step_nofork n2 (e', sσ'') (e'', sσ''')
    (to_validity (Refine master (cs' ++ [(ts', sσ)]) ixs') : refine_cmra) #
    (to_validity (Refine snapshot {[i]} (cs ++ [(ts, sσ0)]) ixs) : refine_cmra) ~~>>:
    (λ r rl, i' cs'' ts'' ixs'',
        nth_error ts'' i = Some e''
        nth_error ts'' i' = Some ef
        r to_validity (Refine master (cs'' ++ [(ts'', sσ''')]) ixs'')
        rl (to_validity (Refine snapshot {[i]} (cs'' ++ [(ts'', sσ''')]) ixs'') : refine_cmra)
              to_validity (Refine snapshot {[i']} (cs'' ++ [(ts'', sσ''')]) ixs'')).
Proof.
  intros Kge Hn1 Hn2 Hlookup Hstep_pre Hstep_fork Hstep_post.
  eapply cmra_total_step_updatePn z.
  rewrite (comm _ (to_validity _)).
  intros Hval.
  inversion Hval as (Hvalop&Hvalz&Hdisj_prod_z).
  inversion Hvalop as (Hval_snap&Hval_master&Hdisj_xy).
  inversion Hdisj_xy as [ | ?????? Hinter Hvalid_ext (Heqt&Heqcs_ext) (Heqcs&Heqcs') |].
  subst.
  rewrite //= -Heqcs' in Hdisj_prod_z.
  rewrite prefix_of_op in Hdisj_prod_z; last (eexists; auto).
  rewrite //= right_id_L in Hdisj_prod_z.
  inversion Hdisj_prod_z as [ | |
                              ?????? Hinter_z Hvalid_ext_z [Heqt_z Heqcs_ext_z Heqixs_ext_z]
                                     (Heq_vz)].
  subst.
  edestruct Hval_master as (Hmaximal&Hval_cfg_master); simpl in ×.
  rewrite -Heqcs' in Hval_cfg_master.
  edestruct (nth_error_split ts) as (ts1&ts2&Heq_ts&Hlen); eauto.
  rewrite Heq_ts in Hval_cfg_master.
  edestruct (nostep_fixed_extension) as (ts1'&ts2'&sσ0'&Hlen'&Hlast'); first (rewrite assoc); eauto.
  { edestruct Hval_snap. simpl in ×. symmetry; eapply valid_cfg_idx_length4; eauto. }
  { set_solver. }
  edestruct (prim_step_nofork_valid_cfg n1 ts1' ts2') as
      (cstep1&ixstep1&Hval_step1&Hlen_step1&Hidxs_step1); eauto.
  edestruct (prim_step_nofork_valid_cfg n2 ts1' (ts2' ++ [ef])) as
      (cstep2&ixstep2&Hval_step2&Hlen_step2&Hidxs_step2); eauto.
   (to_validity {| view := master; tids := ∅;
                         cfgs := cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2 ++ cstep1
                                   ++ [(ts1' ++ e :: ts2', sσ')] ++
                                        [ (ts1' ++ e' :: ts2' ++ [ef], sσ'') ] ++ cstep2 ++
                                        [ (ts1' ++ e'' :: ts2' ++ [ef], sσ''')] ;
                         idxs := ixs ++ is2 ++ ixstep1 ++ [i] ++ ixstep2 |}).
   (to_validity {| view := snapshot; tids := {[i]} {[length (ts1' ++ e'' :: ts2')]};
                         cfgs := cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2 ++ cstep1
                                   ++ [(ts1' ++ e :: ts2', sσ')] ++
                                        [ (ts1' ++ e' :: ts2' ++ [ef], sσ'') ] ++ cstep2 ++
                                        [ (ts1' ++ e'' :: ts2' ++ [ef], sσ''')] ;
                         idxs := ixs ++ is2 ++ ixstep1 ++ [i] ++ ixstep2 |}).
  assert (sσ0' = sσ) as →.
  { rewrite -Heq_ts in Hlast'. rewrite app_assoc Heqcs' in Hlast'.
    rewrite last_snoc in Hlast'. inversion Hlast'; auto. }
  split_and!.
  - (length (ts1' ++ e'' :: ts2')).
     (cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2 ++ cstep1
           ++ [(ts1' ++ e :: ts2', sσ')]
           ++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')]
           ++ cstep2 ).
     (ts1' ++ e'' :: ts2' ++ [ef]).
     (ixs ++ is2 ++ ixstep1 ++ [i] ++ ixstep2).
    split_and!.
    × rewrite nth_error_app2. replace (i - length ts1') with 0 by omega.
      auto. omega.
    × rewrite app_comm_cons. rewrite app_assoc. rewrite nth_error_app2.
      replace (length (ts1' ++ e'' :: ts2') - length (ts1' ++ e'' :: ts2')) with 0 by omega.
      auto. omega.
    × rewrite -?assoc //=.
    × rewrite ?app_assoc.
      econstructor.
      ** split.
         *** intros Hval'.
             econstructor. destruct Hval' as (Hval1&Hval2). simpl in ×. econstructor.
             **** rewrite ?app_assoc last_snoc in Hval1 ×.
                  set_solver.
             **** simpl. auto.
             **** split; auto.
                  edestruct Hval' as (Hval1&Hval2). simpl in ×. econstructor; auto.
                  rewrite ?app_assoc ?last_snoc in Hval1 ×. simpl. intros i0.
                  rewrite ?app_length //= ?app_length //=. set_unfold. intros; omega.
                  simpl. econstructor. set_unfold. rewrite ?app_length. simpl.
                  intros ?. omega.
                  left. econstructor. eauto. []. split; eauto using app_nil_r.
                  set_solver+.
         *** intros Hval_op. destruct Hval_op as ((Hl1&Hval1)&(Hl2&Hval2)&?Hdisj). econstructor; auto.
             rewrite ?last_snoc //= in Hl1 Hl2 ×.
                  rewrite ?app_length //= ?app_length //=. set_unfold. intros; omega.
      ** intros ?Hval. simpl. rewrite ?prefix_of_op //=.
  -
    assert (valid_cfg_idx_seq ([(ts1' ++ e0 :: ts2', sσ)] ++ cstep1
                                 ++ [(ts1' ++ e :: ts2', sσ')]
                                 ++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')]
                                 ++ cstep2
                                 ++ [(ts1' ++ e'' :: ts2' ++ [ef], sσ''')])
                              (ixstep1 ++ [i] ++ ixstep2)).
    {
      replace _ with
      ((([(ts1' ++ e0 :: ts2', sσ)] ++ cstep1 ++
      ([(ts1' ++ e :: ts2', sσ')]))) ++ (([(ts1' ++ e' :: ts2' ++ [ef], sσ'')]) ++
      cstep2 ++ [(ts1' ++ e'' :: ts2' ++ [ef], sσ''')])) by (rewrite ?app_assoc //).
      eapply valid_seq_join'; first eauto; last first.
      { rewrite ?app_assoc last_snoc; auto. }
      simpl. econstructor.
      - econstructor; eauto. simpl. eauto.
      - eauto.
    }
    split_and!.
    × constructor; split_and!.
      ** rewrite /cfgs /tids.
         rewrite ?app_assoc last_snoc. set_solver+.
      ** rewrite /cfgs /idxs.
         rewrite ?app_assoc.
         eapply (valid_seq_join') in Hval_cfg_master; eauto.
         *** rewrite -?app_assoc in Hval_cfg_master ×. auto.
         *** rewrite -app_assoc; auto.
      ** split_and!.
         *** rewrite /cfgs /tids ?app_assoc ?last_snoc. set_unfold.
             intros ? [->| ->]; rewrite ?app_length //= ?app_length //=;
             omega.
         *** rewrite /cfgs /idxs.
             eapply (valid_seq_join') in Hval_cfg_master; eauto.
             **** rewrite -?app_assoc in Hval_cfg_master ×. auto.
             **** rewrite -app_assoc. auto.
      ** simpl.
         rewrite -[P in {| view := _; tids := _; cfgs := P |}]app_nil_r.
         rewrite -[P in {| view := _; tids := _; cfgs := _; idxs := P |}]app_nil_r.
         eapply (master_snapshot_disjoint _ _ _ [] _ []).
         *** set_solver.
         *** set_solver.
    × auto.
    × simpl. rewrite prefix_of_op; simpl; last ( []; rewrite ?app_nil_r; done).
      rewrite -Heq_vz.
      rewrite ?app_assoc.
      rewrite -Heqixs_ext_z.
      rewrite -assoc //= Heq_ts in Heqcs_ext_z .
      rewrite -?app_assoc.
      rewrite (app_comm_cons cs2).
      rewrite app_assoc.
      rewrite -Heqcs_ext_z.
      rewrite -?app_assoc.
      econstructor.
      ** clear -Heq_ts Hval_cfg_master Heqcs_ext_z Heqcs' Hinter_z Heq_vz Hvalz Hlast'.
         assert ( validity_car z) as Hval_vcz by (destruct z; auto).
         rewrite -Heq_vz in Hval_vcz.
         destruct Hval_vcz as (Hmaximal&Hval_cs1). simpl in Hmaximal, Hval_cs1.
         destruct cs1 as [| c1' cs1' _] using rev_ind.
         *** simpl in *; set_solver.
         *** rewrite last_snoc in Hmaximal. rewrite -?assoc //= -Heqcs_ext_z in Hval_cfg_master.
             assert (length (c1'.1) length (ts1' ++ e'' :: ts2')).

             rewrite -?app_assoc in Hval_cfg_master.
             eapply valid_seq_tp_monotone_last in Hval_cfg_master; last first.
             **** rewrite assoc Heqcs_ext_z. rewrite //= in Hlast'. rewrite Hlast'. auto.
             **** rewrite ?app_length //= in Hval_cfg_master ×.
             **** rewrite ?left_id. set_unfold. intros i' (Hnot1&[->| ->]).
                  set_solver.
                  edestruct le_not_lt; eauto.
      ** set_solver.

  -
    assert (valid_cfg_idx_seq ([(ts1' ++ e0 :: ts2', sσ)] ++ cstep1
                                 ++ [(ts1' ++ e :: ts2', sσ')]
                                 ++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')]
                                 ++ cstep2
                                 ++ [(ts1' ++ e'' :: ts2' ++ [ef], sσ''')])
                              (ixstep1 ++ [i] ++ ixstep2)).
    {
      replace _ with
      ((([(ts1' ++ e0 :: ts2', sσ)] ++ cstep1 ++
      ([(ts1' ++ e :: ts2', sσ')]))) ++ (([(ts1' ++ e' :: ts2' ++ [ef], sσ'')]) ++
      cstep2 ++ [(ts1' ++ e'' :: ts2' ++ [ef], sσ''')])) by (rewrite ?app_assoc //).
      eapply valid_seq_join'; first eauto; last first.
      { rewrite ?app_assoc last_snoc; auto. }
      simpl. econstructor.
      - econstructor; eauto. simpl. eauto.
      - eauto.
    }
    rewrite Heq_ts. econstructor.
     × split; intros Hval'.
       ** econstructor.
         *** rewrite ?app_assoc last_snoc /tids. set_unfold.
             rewrite ?app_length //= ?app_length //=. intros ? [-> | ->]; omega.
         *** rewrite /cfgs /idxs.
             eapply (valid_seq_join') in Hval_cfg_master; eauto.
             **** rewrite -?app_assoc in Hval_cfg_master ×. auto.
             **** rewrite -app_assoc. auto.
       ** rewrite -Heq_ts. auto.
     × intros Hval'.
       rewrite /validity_car /to_validity.
       eapply (snap_spec_step {[i]} ({[i]} {[length (ts1' ++ e'' :: ts2')]}) cs _ cs2 _ ixs is2).
       ** rewrite -assoc in Hval_cfg_master. eapply valid_seq_split in Hval_cfg_master; eauto.
            destruct Hval' as (?&Hval_cfg'); eapply valid_cfg_idx_length4; eauto.
       ** clear -Hvalid_ext. set_solver.
       ** assert ( cs0, cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2 =
                              cs0 ++ [(ts1' ++ e0 :: ts2', sσ)]) as (cs0'&Heq_cs0').
          { destruct cs2 as [| c' cs2'] using rev_ind.
            - rewrite ?app_nil_r last_snoc in Hlast' ×. inversion Hlast'. subst.
              eexists; eauto.
            - rewrite ?app_assoc last_snoc in Hlast'. inversion Hlast'. subst.
              rewrite ?assoc. eexists; eauto.
          }
          rewrite Heq_cs0'.
          rewrite ?app_assoc. rewrite -(app_assoc cs) Heq_cs0'.
          rewrite -?app_assoc. rewrite -[P in _ {| view := _; tids := P; |}]right_id_L.
          rewrite (app_assoc ixs).
          rewrite right_id_L.
          rewrite app_assoc.
          rewrite -app_assoc.
          replace (cs0' ++ [_] ++ cstep1 ++ _) with
          (cs0' ++
           [(ts1' ++ e0 :: ts2', sσ)] ++
           (cstep1 ++
           [(ts1' ++ e :: ts2', sσ')] ++
           [(ts1' ++ e' :: ts2' ++ [ef], sσ'')] ++
           cstep2) ++ [(ts1' ++ e'' :: ts2' ++ [ef], sσ''')]); last (rewrite ?app_assoc; auto; done).
          eapply (snap_block_step {[i]} {[length (ts1' ++ e'' :: ts2')]}); eauto.
          *** rewrite ?app_assoc in H ×. auto.
          *** set_solver+.
          *** simpl. set_unfold. intros ? →.
            intros. transitivity (length (ixstep1 ++ i :: ixstep2));
              first eapply count_occ_le_length.
            rewrite ?app_length //=; omega.
          *** set_solver.
          *** set_unfold. split.
              **** intros →. rewrite ?app_length //= ?app_length //=. omega.
              **** rewrite ?app_length //= ?app_length //=. omega.
Qed.


Lemma snap_master_fork_pre i n1 e0 e ef e' ts ts' sσ0 sσ sσ' sσ'' cs cs' ixs ixs':
  K S (n1)
  1 n1
  nth_error ts i = Some e0
    nsteps prim_step_nofork n1 (e0, sσ) (e, sσ')
    prim_step e sσ' e' sσ'' (Some ef)
    (to_validity (Refine master (cs' ++ [(ts', sσ)]) ixs') : refine_cmra) #
    (to_validity (Refine snapshot {[i]} (cs ++ [(ts, sσ0)]) ixs) : refine_cmra) ~~>>:
    (λ r rl, i' cs'' ts'' ixs'',
        nth_error ts'' i = Some e'
        nth_error ts'' i' = Some ef
        r to_validity (Refine master (cs'' ++ [(ts'', sσ'')]) ixs'')
        rl (to_validity (Refine snapshot {[i]} (cs'' ++ [(ts'', sσ'')]) ixs'') : refine_cmra)
              to_validity (Refine snapshot {[i']} (cs'' ++ [(ts'', sσ'')]) ixs'')).
Proof.
  intros Kge Hn1 Hlookup Hstep_pre Hstep_fork.
  eapply cmra_total_step_updatePn z.
  rewrite (comm _ (to_validity _)).
  intros Hval.
  inversion Hval as (Hvalop&Hvalz&Hdisj_prod_z).
  inversion Hvalop as (Hval_snap&Hval_master&Hdisj_xy).
  inversion Hdisj_xy as [ | ?????? Hinter Hvalid_ext (Heqt&Heqcs_ext) (Heqcs&Heqcs') |].
  subst.
  rewrite //= -Heqcs' in Hdisj_prod_z.
  rewrite prefix_of_op in Hdisj_prod_z; last (eexists; auto).
  rewrite //= right_id_L in Hdisj_prod_z.
  inversion Hdisj_prod_z as [ | |
                              ?????? Hinter_z Hvalid_ext_z [Heqt_z Heqcs_ext_z Heqixs_ext_z]
                                     (Heq_vz)].
  subst.
  edestruct Hval_master as (Hmaximal&Hval_cfg_master); simpl in ×.
  rewrite -Heqcs' in Hval_cfg_master.
  edestruct (nth_error_split ts) as (ts1&ts2&Heq_ts&Hlen); eauto.
  rewrite Heq_ts in Hval_cfg_master.
  edestruct (nostep_fixed_extension) as (ts1'&ts2'&sσ0'&Hlen'&Hlast'); first (rewrite assoc); eauto.
  { edestruct Hval_snap. simpl in ×. symmetry; eapply valid_cfg_idx_length4; eauto. }
  { set_solver. }
  edestruct (prim_step_nofork_valid_cfg n1 ts1' ts2') as
      (cstep1&ixstep1&Hval_step1&Hlen_step1&Hidxs_step1); eauto.
   (to_validity {| view := master; tids := ∅;
                         cfgs := cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2 ++ cstep1
                                   ++ [(ts1' ++ e :: ts2', sσ')] ++
                                        [ (ts1' ++ e' :: ts2' ++ [ef], sσ'') ];
                         idxs := ixs ++ is2 ++ ixstep1 ++ [i]|}).
   (to_validity {| view := snapshot; tids := {[i]} {[length (ts1' ++ e' :: ts2')]};
                         cfgs := cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2 ++ cstep1
                                   ++ [(ts1' ++ e :: ts2', sσ')] ++
                                        [ (ts1' ++ e' :: ts2' ++ [ef], sσ'') ];
                         idxs := ixs ++ is2 ++ ixstep1 ++ [i]|}).
  assert (sσ0' = sσ) as →.
  { rewrite -Heq_ts in Hlast'. rewrite app_assoc Heqcs' in Hlast'.
    rewrite last_snoc in Hlast'. inversion Hlast'; auto. }
  split_and!.
  - (length (ts1' ++ e' :: ts2')).
     (cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2 ++ cstep1
           ++ [(ts1' ++ e :: ts2', sσ')]).
     (ts1' ++ e' :: ts2' ++ [ef]).
     (ixs ++ is2 ++ ixstep1 ++ [i]).
    split_and!.
    × rewrite nth_error_app2. replace (i - length ts1') with 0 by omega.
      auto. omega.
    × rewrite app_comm_cons. rewrite app_assoc. rewrite nth_error_app2.
      replace (length (ts1' ++ e' :: ts2') - length (ts1' ++ e' :: ts2')) with 0 by omega.
      auto. omega.
    × rewrite -?assoc //=.
    × rewrite ?app_assoc.
      econstructor.
      ** split.
         *** intros Hval'.
             econstructor. destruct Hval' as (Hval1&Hval2). simpl in ×. econstructor.
             **** rewrite ?app_assoc last_snoc in Hval1 ×.
                  set_solver.
             **** simpl. auto.
             **** split; auto.
                  edestruct Hval' as (Hval1&Hval2). simpl in ×. econstructor; auto.
                  rewrite ?app_assoc ?last_snoc in Hval1 ×. simpl. intros i0.
                  rewrite ?app_length //= ?app_length //=. set_unfold. intros; omega.
                  simpl. econstructor. set_unfold. rewrite ?app_length. simpl.
                  intros ?. omega.
                  left. econstructor. eauto. []. split; eauto using app_nil_r.
                  set_solver+.
         *** intros Hval_op. destruct Hval_op as ((Hl1&Hval1)&(Hl2&Hval2)&?Hdisj). econstructor; auto.
             rewrite ?last_snoc //= in Hl1 Hl2 ×.
                  rewrite ?app_length //= ?app_length //=. set_unfold. intros; omega.
      ** intros ?Hval. simpl. rewrite ?prefix_of_op //=.
  -
    assert (valid_cfg_idx_seq ([(ts1' ++ e0 :: ts2', sσ)] ++ cstep1
                                 ++ [(ts1' ++ e :: ts2', sσ')]
                                 ++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')])
                              (ixstep1 ++ [i])).
    {
      replace _ with
      ((([(ts1' ++ e0 :: ts2', sσ)] ++ cstep1 ++
      ([(ts1' ++ e :: ts2', sσ')]))) ++ (([(ts1' ++ e' :: ts2' ++ [ef], sσ'')])))
        by (rewrite ?app_assoc //).
      eapply valid_seq_join'; first eauto; last first.
      { rewrite ?app_assoc last_snoc; auto. }
      simpl. econstructor.
      - econstructor; eauto. simpl. eauto.
      - econstructor.
    }
    split_and!.
    × constructor; split_and!.
      ** rewrite /cfgs /tids.
         rewrite ?app_assoc last_snoc. set_solver+.
      ** rewrite /cfgs /idxs.
         rewrite ?app_assoc.
         eapply (valid_seq_join') in Hval_cfg_master; eauto.
         *** rewrite -?app_assoc in Hval_cfg_master ×. auto.
         *** rewrite -app_assoc; auto.
      ** split_and!.
         *** rewrite /cfgs /tids ?app_assoc ?last_snoc. set_unfold.
             intros ? [->| ->]; rewrite ?app_length //= ?app_length //=;
             omega.
         *** rewrite /cfgs /idxs.
             eapply (valid_seq_join') in Hval_cfg_master; eauto.
             **** rewrite -?app_assoc in Hval_cfg_master ×. auto.
             **** rewrite -app_assoc. auto.
      ** simpl.
         rewrite -[P in {| view := _; tids := _; cfgs := P |}]app_nil_r.
         rewrite -[P in {| view := _; tids := _; cfgs := _; idxs := P |}]app_nil_r.
         eapply (master_snapshot_disjoint _ _ _ [] _ []).
         *** set_solver.
         *** set_solver.
    × auto.
    × simpl. rewrite prefix_of_op; simpl; last ( []; rewrite ?app_nil_r; done).
      rewrite -Heq_vz.
      rewrite ?app_assoc.
      rewrite -Heqixs_ext_z.
      rewrite -assoc //= Heq_ts in Heqcs_ext_z .
      rewrite -?app_assoc.
      rewrite (app_comm_cons cs2).
      rewrite app_assoc.
      rewrite -Heqcs_ext_z.
      rewrite -?app_assoc.
      econstructor.
      ** clear -Heq_ts Hval_cfg_master Heqcs_ext_z Heqcs' Hinter_z Heq_vz Hvalz Hlast'.
         assert ( validity_car z) as Hval_vcz by (destruct z; auto).
         rewrite -Heq_vz in Hval_vcz.
         destruct Hval_vcz as (Hmaximal&Hval_cs1). simpl in Hmaximal, Hval_cs1.
         destruct cs1 as [| c1' cs1' _] using rev_ind.
         *** simpl in *; set_solver.
         *** rewrite last_snoc in Hmaximal. rewrite -?assoc //= -Heqcs_ext_z in Hval_cfg_master.
             assert (length (c1'.1) length (ts1' ++ e' :: ts2')).

             rewrite -?app_assoc in Hval_cfg_master.
             eapply valid_seq_tp_monotone_last in Hval_cfg_master; last first.
             **** rewrite assoc Heqcs_ext_z. rewrite //= in Hlast'. rewrite Hlast'. auto.
             **** rewrite ?app_length //= in Hval_cfg_master ×.
             **** rewrite ?left_id. set_unfold. intros i' (Hnot1&[->| ->]).
                  set_solver.
                  edestruct le_not_lt; eauto.
      ** set_solver.

  -
    assert (valid_cfg_idx_seq ([(ts1' ++ e0 :: ts2', sσ)] ++ cstep1
                                 ++ [(ts1' ++ e :: ts2', sσ')]
                                 ++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')])
                              (ixstep1 ++ [i])).
    {
      replace _ with
      ((([(ts1' ++ e0 :: ts2', sσ)] ++ cstep1 ++
      ([(ts1' ++ e :: ts2', sσ')]))) ++ (([(ts1' ++ e' :: ts2' ++ [ef], sσ'')])))
        by (rewrite ?app_assoc //).
      eapply valid_seq_join'; first eauto; last first.
      { rewrite ?app_assoc last_snoc; auto. }
      simpl. econstructor.
      - econstructor; eauto. simpl. eauto.
      - econstructor.
    }
    rewrite Heq_ts. econstructor.
     × split; intros Hval'.
       ** econstructor.
         *** rewrite ?app_assoc last_snoc /tids. set_unfold.
             rewrite ?app_length //= ?app_length //=. intros ? [-> | ->]; omega.
         *** rewrite /cfgs /idxs.
             eapply (valid_seq_join') in Hval_cfg_master; eauto.
             **** rewrite -?app_assoc in Hval_cfg_master ×. auto.
             **** rewrite -app_assoc. auto.
       ** rewrite -Heq_ts. auto.
     × intros Hval'.
       rewrite /validity_car /to_validity.
       eapply (snap_spec_step {[i]} ({[i]} {[length (ts1' ++ e' :: ts2')]}) cs _ cs2 _ ixs is2).
       ** rewrite -assoc in Hval_cfg_master. eapply valid_seq_split in Hval_cfg_master; eauto.
            destruct Hval' as (?&Hval_cfg'); eapply valid_cfg_idx_length4; eauto.
       ** clear -Hvalid_ext. set_solver.
       ** assert ( cs0, cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2 =
                              cs0 ++ [(ts1' ++ e0 :: ts2', sσ)]) as (cs0'&Heq_cs0').
          { destruct cs2 as [| c' cs2'] using rev_ind.
            - rewrite ?app_nil_r last_snoc in Hlast' ×. inversion Hlast'. subst.
              eexists; eauto.
            - rewrite ?app_assoc last_snoc in Hlast'. inversion Hlast'. subst.
              rewrite ?assoc. eexists; eauto.
          }
          rewrite Heq_cs0'.
          rewrite ?app_assoc. rewrite -(app_assoc cs) Heq_cs0'.
          rewrite -?app_assoc. rewrite -[P in _ {| view := _; tids := P; |}]right_id_L.
          rewrite (app_assoc ixs).
          rewrite right_id_L.
          rewrite app_assoc.
          rewrite -app_assoc.
          replace (cs0' ++ [_] ++ cstep1 ++ _) with
          (cs0' ++
           [(ts1' ++ e0 :: ts2', sσ)] ++
           (cstep1 ++
           [(ts1' ++ e :: ts2', sσ')]) ++
           [(ts1' ++ e' :: ts2' ++ [ef], sσ'')] );
            last (rewrite ?app_assoc; auto; done).
          eapply (snap_block_step {[i]} {[length (ts1' ++ e' :: ts2')]}); eauto.
          *** rewrite ?app_assoc in H ×. auto.
          *** set_solver+.
          *** simpl. set_unfold. intros ? →.
            intros. transitivity (length (ixstep1 ++ [i]));
              first eapply count_occ_le_length.
            rewrite ?app_length //=; omega.
          *** set_solver.
          *** set_unfold. split.
              **** intros →. rewrite ?app_length //= ?app_length //=. omega.
              **** rewrite ?app_length //= ?app_length //=. omega.
Qed.

Lemma snap_master_fork_post i n2 e0 e ef e' ts ts' sσ0 sσ sσ' sσ'' cs cs' ixs ixs':
  K S (n2)
  1 n2
  nth_error ts i = Some e0
    prim_step e0 sσ e sσ' (Some ef)
    nsteps prim_step_nofork n2 (e, sσ') (e', sσ'')
    (to_validity (Refine master (cs' ++ [(ts', sσ)]) ixs') : refine_cmra) #
    (to_validity (Refine snapshot {[i]} (cs ++ [(ts, sσ0)]) ixs) : refine_cmra) ~~>>:
    (λ r rl, i' cs'' ts'' ixs'',
        nth_error ts'' i = Some e'
        nth_error ts'' i' = Some ef
        r to_validity (Refine master (cs'' ++ [(ts'', sσ'')]) ixs'')
        rl (to_validity (Refine snapshot {[i]} (cs'' ++ [(ts'', sσ'')]) ixs'') : refine_cmra)
              to_validity (Refine snapshot {[i']} (cs'' ++ [(ts'', sσ'')]) ixs'')).
Proof.
  intros Kge Hn1 Hlookup Hstep_pre Hstep_fork.
  eapply cmra_total_step_updatePn z.
  rewrite (comm _ (to_validity _)).
  intros Hval.
  inversion Hval as (Hvalop&Hvalz&Hdisj_prod_z).
  inversion Hvalop as (Hval_snap&Hval_master&Hdisj_xy).
  inversion Hdisj_xy as [ | ?????? Hinter Hvalid_ext (Heqt&Heqcs_ext) (Heqcs&Heqcs') |].
  subst.
  rewrite //= -Heqcs' in Hdisj_prod_z.
  rewrite prefix_of_op in Hdisj_prod_z; last (eexists; auto).
  rewrite //= right_id_L in Hdisj_prod_z.
  inversion Hdisj_prod_z as [ | |
                              ?????? Hinter_z Hvalid_ext_z [Heqt_z Heqcs_ext_z Heqixs_ext_z]
                                     (Heq_vz)].
  subst.
  edestruct Hval_master as (Hmaximal&Hval_cfg_master); simpl in ×.
  rewrite -Heqcs' in Hval_cfg_master.
  edestruct (nth_error_split ts) as (ts1&ts2&Heq_ts&Hlen); eauto.
  rewrite Heq_ts in Hval_cfg_master.
  edestruct (nostep_fixed_extension) as (ts1'&ts2'&sσ0'&Hlen'&Hlast'); first (rewrite assoc); eauto.
  { edestruct Hval_snap. simpl in ×. symmetry; eapply valid_cfg_idx_length4; eauto. }
  { set_solver. }
  edestruct (prim_step_nofork_valid_cfg n2 ts1' (ts2' ++ [ef])) as
      (cstep2&ixstep2&Hval_step2&Hlen_step2&Hidxs_step2); eauto.
   (to_validity {| view := master; tids := ∅;
                         cfgs := cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2
                                   ++ [(ts1' ++ e :: ts2' ++ [ef], sσ')] ++ cstep2 ++
                                        [ (ts1' ++ e' :: ts2' ++ [ef], sσ'')];
                         idxs := ixs ++ is2 ++ [i] ++ ixstep2|}).
   (to_validity {| view := snapshot; tids := {[i]} {[length (ts1' ++ e' :: ts2')]};
                         cfgs := cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2
                                   ++ [(ts1' ++ e :: ts2' ++ [ef], sσ')] ++ cstep2 ++
                                        [ (ts1' ++ e' :: ts2' ++ [ef], sσ'')];
                         idxs := ixs ++ is2 ++ [i] ++ ixstep2|}).
  assert (sσ0' = sσ) as →.
  { rewrite -Heq_ts in Hlast'. rewrite app_assoc Heqcs' in Hlast'.
    rewrite last_snoc in Hlast'. inversion Hlast'; auto. }
  split_and!.
  - (length (ts1' ++ e' :: ts2')).
     (cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2
           ++ [(ts1' ++ e :: ts2' ++ [ef], sσ')] ++ cstep2).
     (ts1' ++ e' :: ts2' ++ [ef]).
     (ixs ++ is2 ++ [i] ++ ixstep2).
    split_and!.
    × rewrite nth_error_app2. replace (i - length ts1') with 0 by omega.
      auto. omega.
    × rewrite app_comm_cons. rewrite app_assoc. rewrite nth_error_app2.
      replace (length (ts1' ++ e' :: ts2') - length (ts1' ++ e' :: ts2')) with 0 by omega.
      auto. omega.
    × rewrite -?assoc //=.
    × rewrite ?app_assoc.
      econstructor.
      ** split.
         *** intros Hval'.
             econstructor. destruct Hval' as (Hval1&Hval2). simpl in ×. econstructor.
             **** rewrite ?app_assoc last_snoc in Hval1 ×.
                  set_solver.
             **** simpl. auto.
             **** split; auto.
                  edestruct Hval' as (Hval1&Hval2). simpl in ×. econstructor; auto.
                  rewrite ?app_assoc ?last_snoc in Hval1 ×. simpl. intros i0.
                  rewrite ?app_length //= ?app_length //=. set_unfold. intros; omega.
                  simpl. econstructor. set_unfold. rewrite ?app_length. simpl.
                  intros ?. omega.
                  left. econstructor. eauto. []. split; eauto using app_nil_r.
                  set_solver+.
         *** intros Hval_op. destruct Hval_op as ((Hl1&Hval1)&(Hl2&Hval2)&?Hdisj). econstructor; auto.
             rewrite ?last_snoc //= in Hl1 Hl2 ×.
                  rewrite ?app_length //= ?app_length //=. set_unfold. intros; omega.
      ** intros ?Hval. simpl. rewrite ?prefix_of_op //=.
  -
    assert (valid_cfg_idx_seq ([(ts1' ++ e0 :: ts2', sσ)]
                                 ++ [(ts1' ++ e :: ts2' ++ [ef], sσ')] ++ cstep2
                                 ++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')])
                              ([i] ++ ixstep2)).
    {
      replace _ with
      ((([(ts1' ++ e0 :: ts2', sσ)] ++
      ([(ts1' ++ e :: ts2' ++ [ef], sσ')]))) ++ cstep2 ++ (([(ts1' ++ e' :: ts2' ++ [ef], sσ'')])))
        by (rewrite ?app_assoc //).
      eapply valid_seq_join'; first eauto; last first.
      { rewrite ?app_assoc last_snoc; auto. }
      simpl. eauto. econstructor.
      - econstructor; eauto. simpl. eauto.
      - econstructor.
    }
    split_and!.
    × constructor; split_and!.
      ** rewrite /cfgs /tids.
         rewrite ?app_assoc last_snoc. set_solver+.
      ** rewrite /cfgs /idxs.
         rewrite ?app_assoc.
         eapply (valid_seq_join') in Hval_cfg_master; eauto.
         *** rewrite -?app_assoc in Hval_cfg_master ×. auto.
         *** rewrite -app_assoc; auto.
      ** split_and!.
         *** rewrite /cfgs /tids ?app_assoc ?last_snoc. set_unfold.
             intros ? [->| ->]; rewrite ?app_length //= ?app_length //=;
             omega.
         *** rewrite /cfgs /idxs.
             eapply (valid_seq_join') in Hval_cfg_master; eauto.
             **** rewrite -?app_assoc in Hval_cfg_master ×. auto.
             **** rewrite -app_assoc. auto.
      ** simpl.
         rewrite -[P in {| view := _; tids := _; cfgs := P |}]app_nil_r.
         rewrite -[P in {| view := _; tids := _; cfgs := _; idxs := P |}]app_nil_r.
         eapply (master_snapshot_disjoint _ _ _ [] _ []).
         *** set_solver.
         *** set_solver.
    × auto.
    × simpl. rewrite prefix_of_op; simpl; last ( []; rewrite ?app_nil_r; done).
      rewrite -Heq_vz.
      rewrite ?app_assoc.
      rewrite -Heqixs_ext_z.
      rewrite -assoc //= Heq_ts in Heqcs_ext_z .
      rewrite -?app_assoc.
      rewrite (app_comm_cons cs2).
      rewrite app_assoc.
      rewrite -Heqcs_ext_z.
      rewrite -?app_assoc.
      econstructor.
      ** clear -Heq_ts Hval_cfg_master Heqcs_ext_z Heqcs' Hinter_z Heq_vz Hvalz Hlast'.
         assert ( validity_car z) as Hval_vcz by (destruct z; auto).
         rewrite -Heq_vz in Hval_vcz.
         destruct Hval_vcz as (Hmaximal&Hval_cs1). simpl in Hmaximal, Hval_cs1.
         destruct cs1 as [| c1' cs1' _] using rev_ind.
         *** simpl in *; set_solver.
         *** rewrite last_snoc in Hmaximal. rewrite -?assoc //= -Heqcs_ext_z in Hval_cfg_master.
             assert (length (c1'.1) length (ts1' ++ e' :: ts2')).

             rewrite -?app_assoc in Hval_cfg_master.
             eapply valid_seq_tp_monotone_last in Hval_cfg_master; last first.
             **** rewrite assoc Heqcs_ext_z. rewrite //= in Hlast'. rewrite Hlast'. auto.
             **** rewrite ?app_length //= in Hval_cfg_master ×.
             **** rewrite ?left_id. set_unfold. intros i' (Hnot1&[->| ->]).
                  set_solver.
                  edestruct le_not_lt; eauto.
      ** set_solver.

  -
    assert (valid_cfg_idx_seq ([(ts1' ++ e0 :: ts2', sσ)]
                                 ++ [(ts1' ++ e :: ts2' ++ [ef], sσ')] ++ cstep2
                                 ++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')])
                              ([i] ++ ixstep2)).
    {
      replace _ with
      ((([(ts1' ++ e0 :: ts2', sσ)] ++
      ([(ts1' ++ e :: ts2' ++ [ef], sσ')]))) ++ cstep2 ++ (([(ts1' ++ e' :: ts2' ++ [ef], sσ'')])))
        by (rewrite ?app_assoc //).
      eapply valid_seq_join'; first eauto; last first.
      { rewrite ?app_assoc last_snoc; auto. }
      simpl. eauto. econstructor.
      - econstructor; eauto. simpl. eauto.
      - econstructor.
    }
    rewrite Heq_ts. econstructor.
     × split; intros Hval'.
       ** econstructor.
         *** rewrite ?app_assoc last_snoc /tids. set_unfold.
             rewrite ?app_length //= ?app_length //=. intros ? [-> | ->]; omega.
         *** rewrite /cfgs /idxs.
             eapply (valid_seq_join') in Hval_cfg_master; eauto.
             **** rewrite -?app_assoc in Hval_cfg_master ×. auto.
             **** rewrite -app_assoc. auto.
       ** rewrite -Heq_ts. auto.
     × intros Hval'.
       rewrite /validity_car /to_validity.
       eapply (snap_spec_step {[i]} ({[i]} {[length (ts1' ++ e' :: ts2')]}) cs _ cs2 _ ixs is2).
       ** rewrite -assoc in Hval_cfg_master. eapply valid_seq_split in Hval_cfg_master; eauto.
            destruct Hval' as (?&Hval_cfg'); eapply valid_cfg_idx_length4; eauto.
       ** clear -Hvalid_ext. set_solver.
       ** assert ( cs0, cs ++ [(ts1 ++ e0 :: ts2, sσ0)] ++ cs2 =
                              cs0 ++ [(ts1' ++ e0 :: ts2', sσ)]) as (cs0'&Heq_cs0').
          { destruct cs2 as [| c' cs2'] using rev_ind.
            - rewrite ?app_nil_r last_snoc in Hlast' ×. inversion Hlast'. subst.
              eexists; eauto.
            - rewrite ?app_assoc last_snoc in Hlast'. inversion Hlast'. subst.
              rewrite ?assoc. eexists; eauto.
          }
          rewrite Heq_cs0'.
          rewrite ?app_assoc. rewrite -(app_assoc cs) Heq_cs0'.
          rewrite -?app_assoc. rewrite -[P in _ {| view := _; tids := P; |}]right_id_L.
          rewrite (app_assoc ixs).
          rewrite right_id_L.
          rewrite app_assoc.
          rewrite -app_assoc.
          replace (cs0' ++ [_] ++ [_] ++ cstep2 ++ _) with
          (cs0' ++
           [(ts1' ++ e0 :: ts2', sσ)] ++
           (([(ts1' ++ e :: ts2' ++ [ef], sσ')] ++ cstep2)) ++
           [(ts1' ++ e' :: ts2' ++ [ef], sσ'')]);
            last (rewrite ?app_assoc; auto; done).
          eapply (snap_block_step {[i]} {[length (ts1' ++ e' :: ts2')]}); eauto.
          *** set_solver+.
          *** intros i' Hin.
            transitivity (length ([i] ++ ixstep2));
              first eapply count_occ_le_length.
            rewrite ?app_length //=; omega.
          *** set_solver.
          *** set_unfold. split.
              **** intros →. rewrite ?app_length //= ?app_length //=. omega.
              **** rewrite ?app_length //= ?app_length //=. omega.
Qed.

Lemma snap_master_fork i n1 n2 e0 e ef e' e'' ts ts' sσ0 sσ sσ' sσ'' sσ''' cs cs' ixs ixs':
  K S (n1 + n2)
  nth_error ts i = Some e0
    nsteps prim_step_nofork n1 (e0, sσ) (e, sσ')
    prim_step e sσ' e' sσ'' (Some ef)
    nsteps prim_step_nofork n2 (e', sσ'') (e'', sσ''')
    (to_validity (Refine master (cs' ++ [(ts', sσ)]) ixs') : refine_cmra) #
    (to_validity (Refine snapshot {[i]} (cs ++ [(ts, sσ0)]) ixs) : refine_cmra) ~~>>:
    (λ r rl, i' cs'' ts'' ixs'',
        nth_error ts'' i = Some e''
        nth_error ts'' i' = Some ef
        r to_validity (Refine master (cs'' ++ [(ts'', sσ''')]) ixs'')
        rl (to_validity (Refine snapshot {[i]} (cs'' ++ [(ts'', sσ''')]) ixs'') : refine_cmra)
              to_validity (Refine snapshot {[i']} (cs'' ++ [(ts'', sσ''')]) ixs'')).
Proof.
  intros Hgt Hnth Hpre Hfork Hpost.
  destruct n1 as [| n1]; destruct n2 as [| n2].
  - inversion Hpre; inversion Hpost; subst.
    eapply snap_master_simple_fork; eauto. omega.
  - inversion Hpre; subst.
    eapply snap_master_fork_post; eauto. omega.
  - inversion Hpost; subst; simpl.
    eapply snap_master_fork_pre; eauto. omega.
    rewrite -plus_n_O; auto.
  - eapply snap_master_fork_pre_post; eauto; omega.
Qed.
End refine_dra.