section ‹IMAP-CRDT Definitions›

text‹We begin by defining the operations on a mailbox state. In addition to the interpretation of 
the operations, we define valid behaviours for the operations as assumptions for the network.
We use the \texttt{network\_with\_constrained\_ops} locale from the framework.›

theory
  "IMAP-def"
  imports
    "CRDT.Network"
begin

datatype ('id, 'a) operation = 
  Create "'id" "'a" | 
  Delete "'id set" "'a" | 
  Append "'id" "'a" | 
  Expunge "'a" "'id" "'id" | 
  Store "'a" "'id" "'id"

type_synonym ('id, 'a) state = "'a ⇒ ('id set × 'id set)"

definition op_elem :: "('id, 'a) operation ⇒ 'a" where
  "op_elem oper ≡ case oper of 
    Create i e ⇒ e | 
    Delete is e ⇒ e | 
    Append i e ⇒ e | 
    Expunge e mo i ⇒ e | 
    Store e mo i ⇒ e"

definition interpret_op :: "('id, 'a) operation ⇒ ('id, 'a) state ⇀ ('id, 'a) state" 
  ("⟨_⟩" [0] 1000) where
  "interpret_op oper state ≡
    let metadata = fst (state (op_elem oper));
        files = snd (state (op_elem oper));
        after  = case oper of 
          Create i e ⇒ (metadata ∪ {i}, files) |
          Delete is e ⇒ (metadata - is, files - is) |
          Append i e ⇒ (metadata, files ∪ {i}) |
          Expunge e mo i ⇒ (metadata ∪ {i}, files - {mo}) |
          Store e mo i ⇒ (metadata, insert i (files - {mo}))
    in  Some (state ((op_elem oper) := after))"

text‹In the definition of the valid behaviours of the operations, we define additional assumption 
the state where the operation is executed. In essence, a the tag of a \create, \append, \expunge,  
and \store\ operation is identical to the message number and therefore unique. A \delete\ operation 
deletes all metadata and the content of a folder. The \store\ and \expunge\ operations must refer 
to an existing message.›

definition valid_behaviours :: "('id, 'a) state ⇒ 'id × ('id, 'a) operation ⇒ bool" where
  "valid_behaviours state msg ≡
    case msg of
      (i, Create j e) ⇒ i = j |
      (i, Delete is e) ⇒ is = fst (state e) ∪ snd (state e) |
      (i, Append j e) ⇒ i = j |
      (i, Expunge e mo j) ⇒ i = j ∧ mo ∈ snd (state e) |
      (i, Store e mo j) ⇒ i = j ∧ mo ∈ snd (state e)"

locale imap = network_with_constrained_ops _ interpret_op "λx. ({},{})" valid_behaviours

end

section ‹Commutativity of IMAP Commands›

text‹In this section we prove the commutativity of operations and identify the edge cases.›

theory
  "IMAP-proof-commute"
  imports
    "IMAP-def"  
begin

lemma (in imap) create_create_commute:
  shows "⟨Create i1 e1⟩ ⊳ ⟨Create i2 e2⟩ = ⟨Create i2 e2⟩ ⊳ ⟨Create i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) create_delete_commute:
  assumes "i ∉ is"
  shows "⟨Create i e1⟩ ⊳ ⟨Delete is e2⟩ = ⟨Delete is e2⟩ ⊳ ⟨Create i e1⟩"
  using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)

lemma (in imap) create_append_commute:
  shows "⟨Create i1 e1⟩ ⊳ ⟨Append i2 e2⟩ = ⟨Append i2 e2⟩ ⊳ ⟨Create i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) create_expunge_commute:
  shows "⟨Create i1 e1⟩ ⊳ ⟨Expunge e2 mo i2⟩ = ⟨Expunge e2 mo i2⟩ ⊳ ⟨Create i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) create_store_commute:
  shows "⟨Create i1 e1⟩ ⊳ ⟨Store e2 mo i2⟩ = ⟨Store e2 mo i2⟩ ⊳ ⟨Create i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) delete_delete_commute:
  shows "⟨Delete i1 e1⟩ ⊳ ⟨Delete i2 e2⟩ = ⟨Delete i2 e2⟩ ⊳ ⟨Delete i1 e1⟩"
  by(unfold interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) delete_append_commute:
  assumes "i ∉ is"
  shows "⟨Delete is e1⟩ ⊳ ⟨Append i e2⟩ = ⟨Append i e2⟩ ⊳ ⟨Delete is e1⟩"
  using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)

lemma (in imap) delete_expunge_commute:
  assumes "i ∉ is"
  shows "⟨Delete is e1⟩ ⊳ ⟨Expunge e2 mo i⟩ = ⟨Expunge e2 mo i⟩ ⊳ ⟨Delete is e1⟩"
  using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)

lemma (in imap) delete_store_commute:
  assumes "i ∉ is"
  shows "⟨Delete is e1⟩ ⊳ ⟨Store e2 mo i⟩ = ⟨Store e2 mo i⟩ ⊳ ⟨Delete is e1⟩"
  using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)

lemma (in imap) append_append_commute:
  shows "⟨Append i1 e1⟩ ⊳ ⟨Append i2 e2⟩ = ⟨Append i2 e2⟩ ⊳ ⟨Append i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) append_expunge_commute:
  assumes "i1 ≠ mo"
  shows "(⟨Append i1 e1⟩ ⊳ ⟨Expunge e2 mo i2⟩) = (⟨Expunge e2 mo i2⟩ ⊳ ⟨Append i1 e1⟩)"
proof
  fix x
  show "(⟨Append i1 e1⟩ ⊳ ⟨Expunge e2 mo i2⟩) x = (⟨Expunge e2 mo i2⟩ ⊳ ⟨Append i1 e1⟩) x"
    using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def)
qed

lemma (in imap) append_store_commute:
  assumes "i1 ≠ mo"
  shows "(⟨Append i1 e1⟩ ⊳ ⟨Store e2 mo i2⟩) = (⟨Store e2 mo i2⟩ ⊳ ⟨Append i1 e1⟩)"
proof
  fix x
  show "(⟨Append i1 e1⟩ ⊳ ⟨Store e2 mo i2⟩) x = (⟨Store e2 mo i2⟩ ⊳ ⟨Append i1 e1⟩) x"
    using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def)
qed

lemma (in imap) expunge_expunge_commute:
  shows "(⟨Expunge e1 mo1 i1⟩ ⊳ ⟨Expunge e2 mo2 i2⟩) = (⟨Expunge e2 mo2 i2⟩ ⊳ ⟨Expunge e1 mo1 i1⟩)"
proof
  fix x
  show "(⟨Expunge e1 mo1 i1⟩ ⊳ ⟨Expunge e2 mo2 i2⟩) x 
       = (⟨Expunge e2 mo2 i2⟩ ⊳ ⟨Expunge e1 mo1 i1⟩) x"
    by(auto simp add: interpret_op_def kleisli_def op_elem_def) qed

lemma (in imap) expunge_store_commute:
  assumes "i1 ≠ mo2" and "i2 ≠ mo1"
  shows "(⟨Expunge e1 mo1 i1⟩ ⊳ ⟨Store e2 mo2 i2⟩) = (⟨Store e2 mo2 i2⟩ ⊳ ⟨Expunge e1 mo1 i1⟩)"
proof
  fix x
  show "(⟨Expunge e1 mo1 i1⟩ ⊳ ⟨Store e2 mo2 i2⟩) x = (⟨Store e2 mo2 i2⟩ ⊳ ⟨Expunge e1 mo1 i1⟩) x"
    unfolding  interpret_op_def kleisli_def op_elem_def using assms(2) by (simp, fastforce)
qed

lemma (in imap) store_store_commute:
  assumes "i1 ≠ mo2" and "i2 ≠ mo1"
  shows "(⟨Store e1 mo1 i1⟩ ⊳ ⟨Store e2 mo2 i2⟩) = (⟨Store e2 mo2 i2⟩ ⊳ ⟨Store e1 mo1 i1⟩)"
proof
  fix x
  show "(⟨Store e1 mo1 i1⟩ ⊳ ⟨Store e2 mo2 i2⟩) x = (⟨Store e2 mo2 i2⟩ ⊳ ⟨Store e1 mo1 i1⟩) x"
    unfolding  interpret_op_def kleisli_def op_elem_def using assms by (simp, fastforce)
qed

end

section ‹Proof Helpers›

text‹In this section we define and prove lemmas that help to show that all identified critical 
conditions hold for concurrent operations. Many of the following parts are derivations from the 
definitions and lemmas of Gomes et al.›

theory
  "IMAP-proof-helpers"
  imports
    "IMAP-def"  

begin

lemma (in imap) apply_operations_never_fails:
  assumes "xs prefix of i"
  shows "apply_operations xs ≠ None"
  using assms proof(induction xs rule: rev_induct, clarsimp)
  case (snoc x xs) thus ?case
  proof (cases x)
    case (Broadcast e) thus ?thesis
      using snoc by force
  next
    case (Deliver e) thus ?thesis
      using snoc apply clarsimp unfolding interp_msg_def apply_operations_def
      by (metis (no_types, lifting) bind.bind_lunit interpret_op_def prefix_of_appendD)
  qed
qed

lemma (in imap) create_id_valid:
  assumes "xs prefix of j"
    and "Deliver (i1, Create i2 e) ∈ set xs"
  shows "i1 = i2"
proof -
  have "∃s. valid_behaviours s (i1, Create i2 e)"
    using assms deliver_in_prefix_is_valid by blast
  thus ?thesis
    by(simp add: valid_behaviours_def)
qed

lemma (in imap) append_id_valid:
  assumes "xs prefix of j"
    and "Deliver (i1, Append i2 e) ∈ set xs"
  shows "i1 = i2"
proof -
  have "∃s. valid_behaviours s (i1, Append i2 e)"
    using assms deliver_in_prefix_is_valid by blast
  thus ?thesis
    by(simp add: valid_behaviours_def)
qed

lemma (in imap) expunge_id_valid:
  assumes "xs prefix of j"
    and "Deliver (i1, Expunge e mo i2) ∈ set xs"
  shows "i1 = i2"
proof -
  have "∃s. valid_behaviours s (i1, Expunge e mo i2)"
    using assms deliver_in_prefix_is_valid by blast
  thus ?thesis
    by(simp add: valid_behaviours_def)
qed

lemma (in imap) store_id_valid:
  assumes "xs prefix of j"
    and "Deliver (i1, Store e mo i2) ∈ set xs"
  shows "i1 = i2"
proof -
  have "∃s. valid_behaviours s (i1, Store e mo i2)"
    using assms deliver_in_prefix_is_valid by blast
  thus ?thesis
    by(simp add: valid_behaviours_def)
qed

definition (in imap) added_ids :: "('id × ('id, 'b) operation) event list ⇒ 'b ⇒ 'id list" where
  "added_ids es p ≡ List.map_filter (λx. case x of 
    Deliver (i, Create j e) ⇒ if e = p then Some j else None | 
    Deliver (i, Expunge e mo j) ⇒ if e = p then Some j else None |
    _ ⇒ None) es"

definition (in imap) added_files :: "('id × ('id, 'b) operation) event list ⇒ 'b ⇒ 'id list" where
  "added_files es p ≡ List.map_filter (λx. case x of 
    Deliver (i, Append j e) ⇒ if e = p then Some j else None |
    Deliver (i, Store e mo j) ⇒ if e = p then Some j else None |
    _ ⇒ None) es"

― ‹added files simplifier›

lemma (in imap) [simp]:
  shows "added_files [] e = []"
  by (auto simp: added_files_def map_filter_def)

lemma (in imap) [simp]:
  shows "added_files (xs @ ys) e = added_files xs e @ added_files ys e"
  by (auto simp: added_files_def map_filter_append)

lemma (in imap) added_files_Broadcast_collapse [simp]:
  shows "added_files ([Broadcast e]) e' = []"
  by (auto simp: added_files_def map_filter_append map_filter_def)

lemma (in imap) added_files_Deliver_Delete_collapse [simp]:
  shows "added_files ([Deliver (i, Delete is e)]) e' = []"
  by (auto simp: added_files_def map_filter_append map_filter_def)

lemma (in imap) added_files_Deliver_Create_collapse [simp]:
  shows "added_files ([Deliver (i, Create j e)]) e' = []"
  by (auto simp: added_files_def map_filter_append map_filter_def)

lemma (in imap) added_files_Deliver_Expunge_collapse [simp]:
  shows "added_files ([Deliver (i, Expunge e mo j)]) e' = []"
  by (auto simp: added_files_def map_filter_append map_filter_def)

lemma (in imap) added_files_Deliver_Append_diff_collapse [simp]:
  shows "e ≠ e' ⟹ added_files ([Deliver (i, Append j e)]) e' = []"
  by (auto simp: added_files_def map_filter_append map_filter_def)

lemma (in imap) added_files_Deliver_Append_same_collapse [simp]:
  shows "added_files ([Deliver (i, Append j e)]) e = [j]"
  by (auto simp: added_files_def map_filter_append map_filter_def)

lemma (in imap) added_files_Deliver_Store_diff_collapse [simp]:
  shows "e ≠ e' ⟹ added_files ([Deliver (i, Store e mo j)]) e' = []"
  by (auto simp: added_files_def map_filter_append map_filter_def)

lemma (in imap) added_files_Deliver_Store_same_collapse [simp]:
  shows "added_files ([Deliver (i, Store e mo j)]) e = [j]"
  by (auto simp: added_files_def map_filter_append map_filter_def)


― ‹added ids simplifier›

lemma (in imap) [simp]:
  shows "added_ids [] e = []"
  by (auto simp: added_ids_def map_filter_def)

lemma (in imap) split_ids [simp]:
  shows "added_ids (xs @ ys) e = added_ids xs e @ added_ids ys e"
  by (auto simp: added_ids_def map_filter_append)

lemma (in imap) added_ids_Broadcast_collapse [simp]:
  shows "added_ids ([Broadcast e]) e' = []"
  by (auto simp: added_ids_def map_filter_append map_filter_def)

lemma (in imap) added_ids_Deliver_Delete_collapse [simp]:
  shows "added_ids ([Deliver (i, Delete is e)]) e' = []"
  by (auto simp: added_ids_def map_filter_append map_filter_def)

lemma (in imap) added_ids_Deliver_Append_collapse [simp]:
  shows "added_ids ([Deliver (i, Append j e)]) e' = []"
  by (auto simp: added_ids_def map_filter_append map_filter_def)

lemma (in imap) added_ids_Deliver_Store_collapse [simp]:
  shows "added_ids ([Deliver (i, Store e mo j)]) e' = []"
  by (auto simp: added_ids_def map_filter_append map_filter_def)

lemma (in imap) added_ids_Deliver_Create_diff_collapse [simp]:
  shows "e ≠ e' ⟹ added_ids ([Deliver (i, Create j e)]) e' = []"
  by (auto simp: added_ids_def map_filter_append map_filter_def)

lemma (in imap) added_ids_Deliver_Expunge_diff_collapse [simp]:
  shows "e ≠ e' ⟹ added_ids ([Deliver (i, Expunge e mo j)]) e' = []"
  by (auto simp: added_ids_def map_filter_append map_filter_def)

lemma (in imap) added_ids_Deliver_Create_same_collapse [simp]:
  shows "added_ids ([Deliver (i, Create j e)]) e = [j]"
  by (auto simp: added_ids_def map_filter_append map_filter_def)

lemma (in imap) added_ids_Deliver_Expunge_same_collapse [simp]:
  shows "added_ids ([Deliver (i, Expunge e mo j)]) e = [j]"
  by (auto simp: added_ids_def map_filter_append map_filter_def)

lemma (in imap) expunge_id_not_in_set:
  assumes "i1 ∉ set (added_ids [Deliver (i, Expunge e mo i2)] e)"
  shows "i1 ≠ i2"
  using assms by simp

lemma (in imap) apply_operations_added_ids:
  assumes "es prefix of j"
    and "apply_operations es = Some f"
  shows "fst (f x) ⊆ set (added_ids es x)"
  using assms proof (induct es arbitrary: f rule: rev_induct, force)
  case (snoc x xs) thus ?case
  proof (cases x, force)
    case (Deliver e)
    moreover obtain a b where "e = (a, b)" by force
    ultimately show ?thesis
      using snoc by(case_tac b; clarsimp simp: interp_msg_def split: bind_splits,
          force split: if_split_asm simp add: op_elem_def interpret_op_def)
  qed
qed

lemma (in imap) apply_operations_added_files:
  assumes "es prefix of j"
    and "apply_operations es = Some f"
  shows "snd (f x) ⊆ set (added_files es x)"
  using assms proof (induct es arbitrary: f rule: rev_induct, force)
  case (snoc x xs) thus ?case
  proof (cases x, force)
    case (Deliver e)
    moreover obtain a b where "e = (a, b)" by force
    ultimately show ?thesis
      using snoc by(case_tac b; clarsimp simp: interp_msg_def split: bind_splits,
          force split: if_split_asm simp add: op_elem_def interpret_op_def)
  qed
qed

lemma (in imap) Deliver_added_files:
  assumes "xs prefix of j"
    and "i ∈ set (added_files xs e)"
  shows "Deliver (i, Append i e) ∈ set xs ∨ (∃ mo . Deliver (i, Store e mo i) ∈ set xs)"
  using assms proof (induct xs rule: rev_induct, clarsimp)
  case (snoc x xs) thus ?case
  proof (cases x, force)
    case X: (Deliver e')
    moreover obtain a b where E: "e' = (a, b)" by force
    ultimately show ?thesis using snoc 
      apply (case_tac b; clarify) apply (simp,metis prefix_of_appendD,force)
      using append_id_valid apply simp 
      using E apply (metis 
          added_files_Deliver_Append_diff_collapse added_files_Deliver_Append_same_collapse 
          empty_iff in_set_conv_decomp list.set(1) prefix_of_appendD set_ConsD, simp)
      using E apply_operations_added_files apply (blast,simp) 
      using E apply_operations_added_files 
      by (metis Un_iff 
          added_files_Deliver_Store_diff_collapse added_files_Deliver_Store_same_collapse empty_iff 
          empty_set list.set_intros(1) prefix_of_appendD set_ConsD set_append store_id_valid)
  qed
qed

end

section ‹Independence of IMAP Commands›

text‹In this section we show that two concurrent operations that reference to the same tag must be 
identical.›

theory
  "IMAP-proof-independent"
  imports
    "IMAP-def"
    "IMAP-proof-helpers"  
begin

lemma (in imap) Broadcast_Expunge_Deliver_prefix_closed:
  assumes "xs @ [Broadcast (i, Expunge e mo i)] prefix of j"
  shows "Deliver (mo, Append mo e) ∈ set xs ∨ 
    (∃ mo2 . Deliver (mo, Store e mo2 mo) ∈ set xs)"
proof -  
  obtain y where "apply_operations xs = Some y"
    using assms broadcast_only_valid_msgs by blast
  moreover hence "mo ∈ snd (y e)"
    using broadcast_only_valid_msgs[of xs "(i, Expunge e mo i)" j] 
      valid_behaviours_def[of y "(i, Expunge e mo i)"] assms by auto
  ultimately show ?thesis
    using assms Deliver_added_files apply_operations_added_files by blast
qed

lemma (in imap) Broadcast_Store_Deliver_prefix_closed:
  assumes "xs @ [Broadcast (i, Store e mo i)] prefix of j"
  shows "Deliver (mo, Append mo e) ∈ set xs ∨ 
    (∃ mo2 . Deliver (mo, Store e mo2 mo) ∈ set xs)"
proof -  
  obtain y where "apply_operations xs = Some y"
    using assms broadcast_only_valid_msgs by blast
  moreover hence "mo ∈ snd (y e)"
    using broadcast_only_valid_msgs[of xs "(i, Store e mo i)" j] 
      valid_behaviours_def[of y "(i, Store e mo i)"] assms by auto
  ultimately show ?thesis
    using assms Deliver_added_files apply_operations_added_files by blast
qed

lemma (in imap) Deliver_added_ids:
  assumes "xs prefix of j"
    and "i ∈ set (added_ids xs e)"
  shows "Deliver (i, Create i e) ∈ set xs ∨ 
    (∃ mo . Deliver (i, Expunge e mo i) ∈ set xs)"
  using assms proof (induct xs rule: rev_induct, clarsimp)
  case (snoc x xs) thus ?case
  proof (cases x, force)
    case X: (Deliver e')
    moreover obtain a b where "e' = (a, b)" by force
    ultimately show ?thesis
      using snoc apply (case_tac b; clarify)
          apply (simp, metis added_ids_Deliver_Create_diff_collapse 
          added_ids_Deliver_Create_same_collapse empty_iff list.set(1) set_ConsD create_id_valid 
          in_set_conv_decomp prefix_of_appendD, force)
      using append_id_valid apply (simp, metis (no_types, lifting)  prefix_of_appendD, simp, metis 
          Un_iff added_ids_Deliver_Expunge_diff_collapse added_ids_Deliver_Expunge_same_collapse 
          empty_iff expunge_id_valid list.set(1) list.set_intros(1) prefix_of_appendD set_ConsD 
          set_append)
      by (simp, blast)
  qed
qed

lemma (in imap) Broadcast_Deliver_prefix_closed:
  assumes "xs @ [Broadcast (r, Delete ix e)] prefix of j"
    and "i ∈ ix"
  shows "Deliver (i, Create i e) ∈ set xs ∨ 
    Deliver (i, Append i e) ∈ set xs ∨ 
    (∃ mo . Deliver (i, Expunge e mo i) ∈ set xs) ∨ 
    (∃ mo . Deliver (i, Store e mo i) ∈ set xs)"
proof -  
  obtain y where "apply_operations xs = Some y"
    using assms broadcast_only_valid_msgs by blast
  moreover hence "ix = fst (y e) ∪ snd (y e)"
    by (metis (mono_tags, lifting) assms(1) broadcast_only_valid_msgs operation.case(2)
        option.simps(1) valid_behaviours_def case_prodD)
  ultimately show ?thesis
    using assms Deliver_added_ids apply_operations_added_ids
    by (metis Deliver_added_files Un_iff apply_operations_added_files le_iff_sup prefix_of_appendD)
qed

lemma (in imap) concurrent_create_delete_independent_technical:
  assumes "i ∈ is"
    and "xs prefix of j"
    and "(i, Create i e) ∈ set (node_deliver_messages xs)" 
    and "(ir, Delete is e) ∈ set (node_deliver_messages xs)"
  shows "hb (i, Create i e) (ir, Delete is e)"
proof -
  have f1: "Deliver (i, Create i e) ∈ set (history j)"
    using assms prefix_msg_in_history by blast
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f2: "Deliver (i, Create i e) ∈ set pre ∨ 
                  Deliver (i, Append i e) ∈ set pre ∨ 
                  (∃ mo . Deliver (i, Expunge e mo i) ∈ set pre) ∨ 
                  (∃ mo . Deliver (i, Store e mo i) ∈ set pre)"
    using Broadcast_Deliver_prefix_closed assms by auto
  have f3: "Deliver (i, Append i e) ∉ set pre" using f1 P 
    by (metis (full_types) Pair_inject fst_conv network.delivery_has_a_cause network.msg_id_unique 
        network_axioms operation.simps(9) prefix_elem_to_carriers prefix_of_appendD)
  have f4: "∀ mo . Deliver (i, Expunge e mo i) ∉ set pre" using f1 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique old.prod.inject operation.simps(11)
        prefix_elem_to_carriers prefix_of_appendD)
  have "∀ mo . Deliver (i, Store e mo i) ∉ set pre" using f1 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique old.prod.inject operation.simps(13)
        prefix_elem_to_carriers prefix_of_appendD) 
  thus ?thesis using f2 f3 f4  P events_in_local_order hb_deliver by blast
qed

lemma (in imap) concurrent_store_expunge_independent_technical:
  assumes "xs prefix of j"
    and "(i, Store e mo i) ∈ set (node_deliver_messages xs)" 
    and "(r, Expunge e i r) ∈ set (node_deliver_messages xs)"
  shows "hb (i, Store e mo i) (r, Expunge e i r)"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Expunge e i r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  moreover hence f1: "Deliver (i, Append i e) ∈ set pre ∨ 
  (∃ mo2 . Deliver (i, Store e mo2 i) ∈ set pre)"
    using Broadcast_Expunge_Deliver_prefix_closed assms(1) by auto
  hence f2: "Deliver (i, Append i e) ∉ set (history k)"
    by (metis Pair_inject assms(1) assms(2) fst_conv msg_id_unique network.delivery_has_a_cause 
        network_axioms operation.distinct(17) prefix_msg_in_history)
  from f1 obtain mo2 :: 'a where
    "Deliver (i, Store e mo2 i) ∈ set (history k)" using f2
    using P prefix_elem_to_carriers by blast  
  hence "Deliver (i, Store e mo i) ∈ set (history k)" using assms f1 f2 P 
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        prefix_msg_in_history)    
  then show ?thesis
    using hb.intros(2) events_in_local_order f1 f2 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique node_histories.prefix_of_appendD 
        node_histories_axioms prefix_elem_to_carriers)
qed

lemma (in imap) concurrent_store_expunge_independent_technical2:
  assumes "xs prefix of j"
    and "(i, Store e1 mo2 i) ∈ set (node_deliver_messages xs)" 
    and "(r, Expunge e mo r) ∈ set (node_deliver_messages xs)"
  shows "mo2 ≠ r"
proof -
  obtain oid :: "'a × ('a, 'b) operation ⇒ nat" where
    oid: "∀p n. Deliver p ∉ set (history n) ∨ Broadcast p ∈ set (history (oid p))"
    by (metis (no_types) delivery_has_a_cause)
  hence f1: "Broadcast (r, Expunge e mo r) ∈ set (history (oid (r, Expunge e mo r)))"
    using assms(1) assms(3) prefix_msg_in_history by blast
  obtain k :: "'a ⇒ 'b ⇒ ('a × ('a, 'b) operation) event list ⇒ 'a" where k: 
    "∀i e pre. (∃mo. Deliver (i, Store e mo i) ∈ set pre) = 
    (Deliver (i, Store e (k i e pre) i) ∈ set pre)"
    by moura
  obtain pre :: "nat ⇒ ('a × ('a, 'b) operation) event ⇒ ('a × ('a, 'b) operation) event list" 
    where pre: "∀k op1. (∃op2. op2 @ [op1] prefix of k) = (pre k op1 @ [op1] prefix of k)"
    by moura
  hence f2: "∀e n. e ∉ set (history n) ∨ pre n e @ [e] prefix of n"
    using events_before_exist by simp
  hence f3: "pre (oid (i, Store e1 mo2 i)) (Broadcast (i, Store e1 mo2 i))
  prefix of oid (i, Store e1 mo2 i)"
    using oid  assms(1) assms(2) prefix_msg_in_history by blast
  have f4: "Deliver (r, Append r e1) ∉ set (history (oid (i, Store e1 mo2 i)))"
    by (metis (no_types) oid f1 fst_conv msg_id_unique old.prod.inject operation.distinct(15))
  have "Deliver (r, Store e1 (k r e1 (pre (oid (i, Store e1 mo2 i)) 
  (Broadcast (i, Store e1 mo2 i)))) r) ∉ set (history (oid (i, Store e1 mo2 i)))"
    by (metis (no_types) oid f1 fst_conv msg_id_unique old.prod.inject operation.distinct(19))
  thus ?thesis using oid k f2 f3 f4 assms
    by (metis (no_types, lifting) Broadcast_Store_Deliver_prefix_closed 
        network.prefix_msg_in_history network_axioms prefix_elem_to_carriers)
qed

lemma (in imap) concurrent_store_delete_independent_technical:
  assumes "i ∈ is"
    and "xs prefix of j"
    and "(i, Store e mo i) ∈ set (node_deliver_messages xs)" 
    and "(ir, Delete is e) ∈ set (node_deliver_messages xs)"
  shows "hb (i, Store e mo i) (ir, Delete is e)"
proof -
  have f1: "Deliver (i, Store e mo i) ∈ set (history j)" using assms prefix_msg_in_history by auto
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f2: "Deliver (i, Create i e) ∈ set pre ∨ 
  Deliver (i, Append i e) ∈ set pre ∨
  (∃ mo . Deliver (i, Expunge e mo i) ∈ set pre) ∨ 
  (∃ mo . Deliver (i, Store e mo i) ∈ set pre)"  
    using Broadcast_Deliver_prefix_closed assms(1) by auto    
  have f3: "Deliver (i, Create i e) ∉ set pre" using f1 P 
    by (metis Pair_inject delivery_has_a_cause fst_conv msg_id_unique operation.distinct(7) 
        prefix_elem_to_carriers prefix_of_appendD)
  have f4: "Deliver (i, Append i e) ∉ set pre" using f1 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique operation.distinct(17) 
        prefix_elem_to_carriers prefix_of_appendD prod.inject)
  have "∀ mo . Deliver (i, Expunge e mo i) ∉ set pre" using f1 P
    by (metis Pair_inject delivery_has_a_cause fst_conv msg_id_unique operation.simps(25) 
        prefix_elem_to_carriers prefix_of_appendD)
  hence "Deliver (i, Store e mo i) ∈ set pre" using f1 f2 f3 f4 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique node_histories.prefix_of_appendD 
        node_histories_axioms prefix_elem_to_carriers)     
  thus ?thesis using P events_in_local_order hb_deliver by blast
qed

lemma (in imap) concurrent_append_delete_independent_technical:
  assumes "i ∈ is"
    and "xs prefix of j"
    and "(i, Append i e) ∈ set (node_deliver_messages xs)" 
    and "(ir, Delete is e) ∈ set (node_deliver_messages xs)"
  shows "hb (i, Append i e) (ir, Delete is e)"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f1: "Deliver (i, Create i e) ∈ set pre ∨ 
  Deliver (i, Append i e) ∈ set pre ∨ 
  (∃ mo . Deliver (i, Expunge e mo i) ∈ set pre) ∨ 
  (∃ mo . Deliver (i, Store e mo i) ∈ set pre)"
    using Broadcast_Deliver_prefix_closed assms(1) by auto
  hence "Deliver (i, Append i e) ∈ set pre" using assms P f1
    by (metis (no_types, hide_lams) delivery_has_a_cause events_in_local_order fst_conv 
        hb_broadcast_exists1 hb_deliver msg_id_unique prefix_msg_in_history)
  thus ?thesis using P events_in_local_order hb_deliver by blast
qed

lemma (in imap) concurrent_append_expunge_independent_technical:
  assumes "i = mo"
    and "xs prefix of j"
    and "(i, Append i e) ∈ set (node_deliver_messages xs)" 
    and "(r, Expunge e mo r) ∈ set (node_deliver_messages xs)"
  shows "hb (i, Append i e) (r, Expunge e mo r)"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Expunge e mo r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f1: "Deliver (mo, Append mo e) ∈ set pre ∨ 
  (∃ mo2 . Deliver (mo, Store e mo2 mo) ∈ set pre)"
    using Broadcast_Expunge_Deliver_prefix_closed assms(1) by auto
  hence "(∀ mo2 . Deliver (mo, Store e mo2 mo) ∉ set pre)" using P assms 
  proof -
    have "Deliver (mo, Append mo e) ∈ set (history j)"
      using assms(1) assms(2) assms(3) prefix_msg_in_history by blast
    thus ?thesis
      by (metis (no_types) P Pair_inject delivery_has_a_cause fst_conv msg_id_unique 
          operation.simps(23) prefix_elem_to_carriers prefix_of_appendD)
  qed
  thus ?thesis
    using hb.intros(2) events_in_local_order assms(1) P f1 by blast
qed

lemma (in imap) concurrent_append_store_independent_technical:
  assumes "i = mo"
    and "xs prefix of j"
    and "(i, Append i e) ∈ set (node_deliver_messages xs)" 
    and "(r, Store e mo r) ∈ set (node_deliver_messages xs)"
  shows "hb (i, Append i e) (r, Store e mo r)"
proof -
  obtain pre k where pre: "pre@[Broadcast (r, Store e mo r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  moreover hence f1: "Deliver (mo, Append mo e) ∈ set pre ∨ 
  (∃ mo2 . Deliver (mo, Store e mo2 mo) ∈ set pre)"
    using Broadcast_Store_Deliver_prefix_closed assms(1) by auto
  have f2: "Deliver (i, Append i e) ∈ set (history j)"
    by (meson assms network.prefix_msg_in_history network_axioms)
  then show ?thesis using assms f1 
    by (metis  pre delivery_has_a_cause events_in_local_order fst_conv hb_deliver 
        msg_id_unique node_histories.prefix_of_appendD node_histories_axioms 
        prefix_elem_to_carriers)
qed

lemma (in imap) concurrent_expunge_delete_independent_technical:
  assumes "i ∈ is"
    and "xs prefix of j"
    and "(i, Expunge e mo i) ∈ set (node_deliver_messages xs)" 
    and "(ir, Delete is e) ∈ set (node_deliver_messages xs)"
  shows "hb (i, Expunge e mo i) (ir, Delete is e)"
proof -
  obtain pre k where pre: "pre@[Broadcast (ir, Delete is e)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  moreover hence A: "Deliver (i, Create i e) ∈ set pre ∨ 
  Deliver (i, Append i e) ∈ set pre ∨ 
  (∃ mo . Deliver (i, Expunge e mo i) ∈ set pre) ∨ 
  (∃ mo . Deliver (i, Store e mo i) ∈ set pre)"
    using Broadcast_Deliver_prefix_closed assms(1) by auto      
  hence "Deliver (i, Expunge e mo i) ∈ set pre" using assms
  proof -
    have f1: "⋀e. e ∉ set pre ∨ e ∈ set (history k)"
      using pre prefix_elem_to_carriers by blast
    have f2: "Deliver (i, Expunge e mo i) ∈ set (history j)"
      by (meson assms network.prefix_msg_in_history network_axioms)
    then show ?thesis using f1 A 
      by (metis (no_types, lifting) fst_conv msg_id_unique network.delivery_has_a_cause 
          network_axioms)
  qed     
  ultimately show ?thesis
    using hb.intros(2) events_in_local_order by blast
qed

lemma (in imap) concurrent_store_store_independent_technical:
  assumes "xs prefix of j"
    and "(i, Store e mo i) ∈ set (node_deliver_messages xs)" 
    and "(r, Store e i r) ∈ set (node_deliver_messages xs)"
  shows "hb (i, Store e mo i) (r, Store e i r)"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Store e i r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f1: "∀e. e ∉ set pre ∨ e ∈ set (history k)"
    using prefix_elem_to_carriers by blast
  have f2: "Deliver (i, Append i e) ∈ set pre ∨ (∃ mo2 . Deliver (i, Store e mo2 i) ∈ set pre)"
    using Broadcast_Store_Deliver_prefix_closed assms(1) P by auto     
  hence "Deliver (i, Store e mo i) ∈ set pre" using assms f1 
    by (metis delivery_has_a_cause fst_conv msg_id_unique prefix_msg_in_history)
  then show ?thesis
    using hb.intros(2) events_in_local_order P by blast
qed

lemma (in imap) expunge_delete_tag_causality:
  assumes "i ∈ is"
    and "xs prefix of j"
    and "(i, Expunge e1 mo i) ∈ set (node_deliver_messages xs)" 
    and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)" 
    and "pre@[Broadcast (ir, Delete is e2)] prefix of k"
  shows "Deliver (i, Expunge e2 mo i) ∈ set (history k)"
proof- 
  have f1: "Deliver (i, Append i e2) ∉ set (history k)" using assms
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.distinct(15) prefix_msg_in_history)
  have f2: "Deliver (i, Create i e2) ∉ set (history k)" using assms
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.distinct(5) prefix_msg_in_history)
  have f3: "∀ mo. Deliver (i, Store e2 mo i) ∉ set (history k)" using assms
    by (metis Pair_inject fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        operation.simps(25) prefix_msg_in_history)
  hence "∃ mo1. Deliver (i, Expunge e2 mo1 i) ∈ set (history k)" using assms f1 f2 
    by (meson imap.Broadcast_Deliver_prefix_closed imap_axioms node_histories.prefix_of_appendD 
        node_histories_axioms prefix_elem_to_carriers)
  then obtain mo1 :: 'a where
    "Deliver (i, Expunge e2 mo1 i) ∈ set (history k)" by blast
  then show ?thesis  using assms f1 f2 f3
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.inject(4) prefix_msg_in_history)
qed

lemma (in imap) expunge_delete_ids_imply_messages_same:
  assumes "i ∈ is"
    and "xs prefix of j"
    and "(i, Expunge e1 mo i) ∈ set (node_deliver_messages xs)" 
    and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  hence "Deliver (i, Expunge e2 mo i) ∈ set (history k)" using assms expunge_delete_tag_causality
    by blast
  then show ?thesis using assms
    by (metis delivery_has_a_cause fst_conv network.msg_id_unique network_axioms 
        operation.inject(4) prefix_msg_in_history prod.inject)
qed

lemma (in imap) store_delete_ids_imply_messages_same:
  assumes "i ∈ is"
    and "xs prefix of j"
    and "(i, Store e1 mo i) ∈ set (node_deliver_messages xs)" 
    and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast 
  have f1: "Deliver (i, Append i e2) ∉ set (history k)" using assms
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.distinct(17) prefix_msg_in_history)
  have f2: "∀ mo. Deliver (i, Expunge e2 mo i) ∉ set (history k)" using assms
    by (metis Pair_inject fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        operation.distinct(19) prefix_msg_in_history)
  have f3: "Deliver (i, Create i e2) ∉ set (history k)" using assms
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.distinct(8) prefix_msg_in_history)
  hence "(∃ mo1. Deliver (i, Store e2 mo1 i) ∈ set pre)" using assms P f1 f2 imap_axioms 
    by (meson imap.Broadcast_Deliver_prefix_closed prefix_elem_to_carriers prefix_of_appendD)
  then obtain mo1 :: 'a where
    f3: "Deliver (i, Store e2 mo1 i) ∈ set pre" by blast
  then have f4: "Deliver (i, Store e2 mo1 i) ∈ set (history k)"
    using P prefix_elem_to_carriers by blast 
  hence "Deliver (i, Store e2 mo i) ∈ set pre" using f2 f3 assms 
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.inject(5) prefix_msg_in_history)
  moreover have "Deliver(i, Store e1 mo i) ∈ set (history j)"
    using assms(2) assms(3) prefix_msg_in_history by blast 
  ultimately show ?thesis using f4
    by (metis delivery_has_a_cause fst_conv msg_id_unique old.prod.inject operation.inject(5))
qed

lemma (in imap) create_delete_ids_imply_messages_same:
  assumes "i ∈ is"
    and "xs prefix of j"
    and "(i, Create i e1) ∈ set (node_deliver_messages xs)" 
    and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  have f1: "Deliver (i, Append i e2) ∉ set (history k)"
    by (metis assms(2) assms(3) delivery_has_a_cause fst_conv network.msg_id_unique 
        network.prefix_msg_in_history network_axioms operation.distinct(3) prod.inject)
  have f2: "∀ mo. Deliver (i, Expunge e2 mo i) ∉ set (history k)"
    by (metis assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        old.prod.inject operation.distinct(5) prefix_msg_in_history)
  have f3: "∀ mo. Deliver (i, Store e2 mo i) ∉ set (history k)"
    by (metis Pair_inject assms(2) assms(3) delivery_has_a_cause fst_conv msg_id_unique 
        operation.distinct(7) prefix_msg_in_history)
  hence "Deliver (i, Create i e2) ∈ set pre" using assms P f2 f1 imap_axioms
    by (meson imap.Broadcast_Deliver_prefix_closed  prefix_elem_to_carriers prefix_of_appendD)
  then show ?thesis using f1 f2 f3
    by (metis (no_types, lifting) P assms(2) assms(3) delivery_has_a_cause fst_conv msg_id_unique 
        node_histories.prefix_of_appendD node_histories_axioms old.prod.inject operation.inject(1) 
        prefix_elem_to_carriers prefix_msg_in_history)
qed

lemma (in imap) append_delete_ids_imply_messages_same:
  assumes "i ∈ is"
    and "xs prefix of j"
    and "(i, Append i e1) ∈ set (node_deliver_messages xs)" 
    and "(ir, Delete is e2) ∈ set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  hence f1: "⋀e. e ∈ set pre ⟹ e ∈ set (history k)" using prefix_elem_to_carriers by blast
  have f2: "Deliver (i, Create i e2) ∉ set pre" using P f1
    by (metis assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        old.prod.inject operation.distinct(3) prefix_msg_in_history)
  moreover have D1: "∀ mo. Deliver (i, Expunge e2 mo i) ∉ set pre" using P f1
    by (metis Pair_inject assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause 
        network_axioms operation.distinct(15) prefix_msg_in_history)
  moreover have D2: "∀ mo. Deliver (i, Store e2 mo i) ∉ set pre" using P f1
    by (metis Pair_inject assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause 
        network_axioms operation.simps(23) prefix_msg_in_history)
  moreover hence "Deliver (i, Append i e2) ∈ set pre" 
    using P D1 D2 f2 assms(1) Broadcast_Deliver_prefix_closed by blast
  moreover have "Deliver (i, Append i e1) ∈ set (history j)"
    using assms(2) assms(3) prefix_msg_in_history by blast
  ultimately show ?thesis using assms 
    by (metis f1 msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.inject(3) prod.sel(1))
qed

lemma (in imap) append_expunge_ids_imply_messages_same:
  assumes "i = mo"
    and "xs prefix of j"
    and "(i, Append i e1) ∈ set (node_deliver_messages xs)" 
    and "(r, Expunge e2 mo r) ∈ set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where pre: "pre@[Broadcast (r, Expunge e2 mo r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  moreover hence "Deliver (mo, Append mo e2) ∈ set pre ∨ 
  (∃ mo2 . Deliver (mo, Store e2 mo2 mo) ∈ set pre)"
    using Broadcast_Expunge_Deliver_prefix_closed assms(1)
    by (meson imap.Broadcast_Deliver_prefix_closed imap_axioms)      
  hence "Deliver (i, Append i e2) ∈ set pre" using assms
    by (metis (no_types, lifting) pre delivery_has_a_cause fst_conv hb_broadcast_exists1 
        msg_id_unique network.hb_deliver network.prefix_msg_in_history network_axioms 
        node_histories.events_in_local_order node_histories_axioms operation.distinct(17) 
        prod.inject)     
  moreover have "Deliver (i, Append i e1) ∈ set (history j)"
    using assms(2) assms(3) prefix_msg_in_history by blast
  ultimately show ?thesis
    by (metis (no_types, lifting) fst_conv network.delivery_has_a_cause network.msg_id_unique 
        network_axioms operation.inject(3) prefix_elem_to_carriers prefix_of_appendD prod.inject)
qed

lemma (in imap) append_store_ids_imply_messages_same:
  assumes "i = mo"
    and "xs prefix of j"
    and "(i, Append i e1) ∈ set (node_deliver_messages xs)" 
    and "(r, Store e2 mo r) ∈ set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Store e2 mo r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  moreover hence A: "Deliver (mo, Append mo e2) ∈ set pre ∨ 
  (∃ mo2 . Deliver (mo, Store e2 mo2 mo) ∈ set pre)"
    using Broadcast_Store_Deliver_prefix_closed assms(1)
    by (meson imap.Broadcast_Deliver_prefix_closed imap_axioms)
  have f1: "Deliver (i, Append i e1) ∈ set (history j)"
    using assms(2) assms(3) prefix_msg_in_history by blast
  hence "Deliver (i, Append i e2) ∈ set pre" using assms P A
    by (metis Pair_inject assms(1) P delivery_has_a_cause fst_conv msg_id_unique 
        operation.simps(23) prefix_elem_to_carriers prefix_of_appendD)
  then show ?thesis using f1
    by (metis P delivery_has_a_cause fst_conv msg_id_unique 
        node_histories.prefix_of_appendD node_histories_axioms operation.inject(3) 
        prefix_elem_to_carriers prod.inject)
qed

lemma (in imap) expunge_store_ids_imply_messages_same:
  assumes "xs prefix of j"
    and "(i, Store e1 mo i) ∈ set (node_deliver_messages xs)" 
    and "(r, Expunge e2 i r) ∈ set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Expunge e2 i r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast 
  hence pprefix: "pre prefix of k"
    using P by blast
  have A: "Deliver (i, Append i e2) ∈ set pre ∨ 
  (∃ mo2 . Deliver (i, Store e2 mo2 i) ∈ set pre)"
    using Broadcast_Expunge_Deliver_prefix_closed assms(1) P by blast      
  have "Deliver (i, Store e2 mo i) ∈ set pre" using assms A P
  proof -
    obtain op1 :: "'a × ('a, 'b) operation ⇒ nat" where
      f1: "Broadcast (i, Store e1 mo i) ∈ set (history (op1 (i, Store e1 mo i)))"
      by (meson assms(1) assms(2) delivery_has_a_cause prefix_msg_in_history)
    then show ?thesis 
      using f1 A pprefix delivery_has_a_cause network.msg_id_unique network_axioms 
        node_histories.prefix_to_carriers node_histories_axioms 
      by fastforce
  qed
  moreover have "Deliver (i, Store e1 mo i) ∈ set (history j)"
    using assms(1) assms(2) prefix_msg_in_history by auto
  ultimately show ?thesis using assms P
    by (metis delivery_has_a_cause fst_conv msg_id_unique operation.inject(5) 
        prefix_elem_to_carriers prefix_of_appendD prod.inject) 
qed

lemma (in imap) store_store_ids_imply_messages_same:
  assumes "xs prefix of j"
    and "(i, Store e1 mo i) ∈ set (node_deliver_messages xs)" 
    and "(r, Store e2 i r) ∈ set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Store e2 i r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  moreover hence A: "Deliver (i, Append i e2) ∈ set pre ∨
    (∃ mo2 . Deliver (i, Store e2 mo2 i) ∈ set pre)"
    using Broadcast_Store_Deliver_prefix_closed assms(1) by blast
  have "∀e. e ∉ set pre ∨ e ∈ set (history k)"
    using P prefix_elem_to_carriers by auto
  hence "Deliver (i, Store e2 mo i) ∈ set pre" 
    by (metis A assms(1) assms(2) delivery_has_a_cause fst_conv msg_id_unique 
        operation.distinct(17) operation.inject(5) prefix_msg_in_history prod.inject)
  moreover have "Deliver (i, Store e1 mo i) ∈ set (history j)"
    using assms(1) assms(2) prefix_msg_in_history by auto
  ultimately show ?thesis using assms
    by (metis Pair_inject delivery_has_a_cause msg_id_unique operation.simps(5) 
        prefix_elem_to_carriers prefix_of_appendD prod.sel(1))
qed 

end