Theory Compactification_Synchronization_Product

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


chapter ‹Compactification of Synchronization Product›

(*<*)
theory Compactification_Synchronization_Product
  imports Combining_Synchronization_Product Process_Normalization_Properties
begin
  (*>*)


section ‹Iterated Combine›

subsection ‹Definitions›

fun iterated_combine⇩d_Sync :: ‹'e set ⇒ ('σ, 'e, 'r) A⇩d list ⇒ ('σ list, 'e, 'r) A⇩d› (‹⟪⇩d⨂⟦_⟧ _⟫› [0, 0])
  where ‹⟪⇩d⨂⟦E⟧ []⟫ = ⦇τ = λσs a. ◇, ω = λσs. ◇⦈›
  |     ‹⟪⇩d⨂⟦E⟧ [A⇩0]⟫ = ⇩d⟪A⇩0⟫⇩σ⇩↪⇩σ⇩s›
  |     ‹⟪⇩d⨂⟦E⟧ A⇩0 # A⇩1 # As⟫ = ⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t ⟪⇩d⨂⟦E⟧ A⇩1 # As⟫⟫›

fun iterated_combine⇩n⇩d_Sync :: ‹'e set ⇒ ('σ, 'e, 'r) A⇩n⇩d list ⇒ ('σ list, 'e, 'r) A⇩n⇩d› (‹⟪⇩n⇩d⨂⟦_⟧ _⟫› [0, 0])
  where ‹⟪⇩n⇩d⨂⟦E⟧ []⟫ = ⦇τ = λσs a. {}, ω = λσs. {}⦈›
  |     ‹⟪⇩n⇩d⨂⟦E⟧ [A⇩0]⟫ = ⇩n⇩d⟪A⇩0⟫⇩σ⇩↪⇩σ⇩s›
  |     ‹⟪⇩n⇩d⨂⟦E⟧ A⇩0 # A⇩1 # As⟫ = ⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t ⟪⇩n⇩d⨂⟦E⟧ A⇩1 # As⟫⟫›


lemma iterated_combine⇩d_Sync_simps_bis: ‹As ≠ [] ⟹ ⟪⇩d⨂⟦E⟧ A⇩0 # As⟫ = ⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t ⟪⇩d⨂⟦E⟧ As⟫⟫›
  and iterated_combine⇩n⇩d_Sync_simps_bis: ‹Bs ≠ [] ⟹ ⟪⇩n⇩d⨂⟦E⟧ B⇩0 # Bs⟫ = ⟪B⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t ⟪⇩n⇩d⨂⟦E⟧ Bs⟫⟫›
  by (induct As, simp_all) (induct Bs, simp_all)


fun iterated_combine⇩d_Sync_ε :: ‹('σ, 'e, 'r, 'α) A⇩d_scheme list ⇒ 'e set ⇒ 'σ list ⇒ 'e set›
  where ‹iterated_combine⇩d_Sync_ε [] E σs = {}› 
  |     ‹iterated_combine⇩d_Sync_ε [A⇩0] E σs = ε A⇩0 (hd σs)›
  |     ‹iterated_combine⇩d_Sync_ε (A⇩0 # A⇩1 # As) E σs = 
         combine_sets_Sync (ε A⇩0 (hd σs)) E (iterated_combine⇩d_Sync_ε (A⇩1 # As) E (tl σs))›

fun iterated_combine⇩n⇩d_Sync_ε :: ‹('σ, 'e, 'r, 'α) A⇩n⇩d_scheme list ⇒ 'e set ⇒ 'σ list ⇒ 'e set›
  where ‹iterated_combine⇩n⇩d_Sync_ε [] E σs = {}› 
  |     ‹iterated_combine⇩n⇩d_Sync_ε [A⇩0] E σs = ε A⇩0 (hd σs)›
  |     ‹iterated_combine⇩n⇩d_Sync_ε (A⇩0 # A⇩1 # As) E σs = 
         combine_sets_Sync (ε A⇩0 (hd σs)) E (iterated_combine⇩n⇩d_Sync_ε (A⇩1 # As) E (tl σs))›


lemma iterated_combine⇩d_Sync_ε_simps_bis:
  ‹As ≠ [] ⟹ iterated_combine⇩d_Sync_ε (A⇩0 # As) E σs = 
                combine_sets_Sync (ε A⇩0 (hd σs)) E (iterated_combine⇩d_Sync_ε As E (tl σs))›
  and iterated_combine⇩n⇩d_Sync_ε_simps_bis: 
  ‹Bs ≠ [] ⟹ iterated_combine⇩n⇩d_Sync_ε (B⇩0 # Bs) E σs = 
                 combine_sets_Sync (ε B⇩0 (hd σs)) E (iterated_combine⇩n⇩d_Sync_ε Bs E (tl σs))›
  by (induct As, simp_all) (induct Bs, simp_all)



subsection ‹First Results›

lemma ε_iterated_combine⇩d_Sync:
  ‹length σs = length As ⟹ ε ⟪⇩d⨂⟦E⟧ As⟫ σs = iterated_combine⇩d_Sync_ε As E σs›
  by (induct σs As rule: induct_2_lists012)
    (simp_all add: ε_combine⇩R⇩l⇩i⇩s⇩t_Sync combine_Sync_ε_def)

lemma ε_iterated_combine⇩n⇩d_Sync:
  ‹length σs = length Bs ⟹ ε ⟪⇩n⇩d⨂⟦E⟧ Bs⟫ σs = iterated_combine⇩n⇩d_Sync_ε Bs E σs›
  by (induct σs Bs rule: induct_2_lists012)
    (simp_all add: ε_combine⇩R⇩l⇩i⇩s⇩t_Sync combine_Sync_ε_def)


lemma combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync_combine⇩R⇩l⇩i⇩s⇩t_Sync_eq:
  ‹ε ⟪⇩d⟪A⇩0⟫⇩σ⇩↪⇩σ⇩s ⇩d⊗⟦1, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫ σs = ε ⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫ σs›
  ‹τ ⟪⇩d⟪A⇩0⟫⇩σ⇩↪⇩σ⇩s ⇩d⊗⟦1, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫ (s⇩0 # σs) e = τ ⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫ (s⇩0 # σs) e›
  ‹ε ⟪⇩n⇩d⟪B⇩0⟫⇩σ⇩↪⇩σ⇩s ⇩n⇩d⊗⟦1, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L B⇩1⟫ σs = ε ⟪B⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t B⇩1⟫ σs›
  ‹τ ⟪⇩n⇩d⟪B⇩0⟫⇩σ⇩↪⇩σ⇩s ⇩n⇩d⊗⟦1, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L B⇩1⟫ (s⇩0 # σs) e = τ ⟪B⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t B⇩1⟫ (s⇩0 # σs) e›
  by (simp_all add: ε_combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync ε_combine⇩R⇩l⇩i⇩s⇩t_Sync drop_Suc combine_Sync_ε_def,
      auto simp add: combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync_defs combine⇩R⇩l⇩i⇩s⇩t_Sync_defs σ_σs_conv_defs ε_simps) 
    (metis append_Cons append_Nil)



lemma combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync_and_iterated_combine⇩n⇩d_Sync_eq:
  ‹ε ⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫ [s⇩0, s⇩1] = ε ⟪⇩d⨂⟦E⟧ [A⇩0, A⇩1]⟫ [s⇩0, s⇩1]›
  ‹τ ⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫ [s⇩0, s⇩1] e = τ ⟪⇩d⨂⟦E⟧ [A⇩0, A⇩1]⟫ [s⇩0, s⇩1] e›
  ‹ε ⟪B⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t B⇩1⟫ [s⇩0, s⇩1] = ε ⟪⇩n⇩d⨂⟦E⟧ [B⇩0, B⇩1]⟫ [s⇩0, s⇩1]›
  ‹τ ⟪B⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t B⇩1⟫ [s⇩0, s⇩1] e = τ ⟪⇩n⇩d⨂⟦E⟧ [B⇩0, B⇩1]⟫ [s⇩0, s⇩1] e›
  by (simp_all add: ε_combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync ε_combine⇩R⇩l⇩i⇩s⇩t_Sync)
    (auto simp add: combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync_defs combine⇩R⇩l⇩i⇩s⇩t_Sync_defs σ_σs_conv_defs 
      option.case_eq_if ε_simps combine_Sync_ε_def)



lemmas combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync_and_combine⇩R⇩l⇩i⇩s⇩t_Sync_eq =
  combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync_and_iterated_combine⇩n⇩d_Sync_eq[simplified]



subsection ‹Reachability›

lemma same_length_ℛ⇩d_iterated_combine⇩d_Sync_description:
  ‹length σs = length As ⟹ σs' ∈ ℛ⇩d ⟪⇩d⨂⟦E⟧ As⟫ σs ⟹
   length σs' = length As ∧ (∀i < length As. σs' ! i ∈ ℛ⇩d (As ! i) (σs ! i))›
proof (induct σs As arbitrary: σs' rule: induct_2_lists012)
  case Nil thus ?case by simp
next
  case (single σ1 A1)
  thus ?case by (auto simp add: ℛ⇩d_from_σ_to_σs_description)
next
  case (Cons σ1 σ2 σs A1 A2 As)
  from set_mp[OF ℛ⇩d_combine⇩d⇩R⇩l⇩i⇩s⇩t_Sync_subset, OF Cons.prems[simplified]]
  obtain σ1' σs'' where ‹σs' = σ1' # σs''› ‹σ1' ∈ ℛ⇩d A1 σ1›
    ‹σs'' ∈ ℛ⇩d ⟪⇩d⨂⟦E⟧ A2 # As⟫ (σ2 # σs)› by blast
  from Cons.hyps(3)[OF this(3)] this(1, 2)
  show ?case using less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc by simp auto
qed


lemma same_length_ℛ⇩n⇩d_iterated_combine⇩n⇩d_Sync_description:
  ‹length σs = length Bs ⟹ σs' ∈ ℛ⇩n⇩d ⟪⇩n⇩d⨂⟦E⟧ Bs⟫ σs ⟹
   length σs' = length Bs ∧ (∀i < length Bs. σs' ! i ∈ ℛ⇩n⇩d (Bs ! i) (σs ! i))›
proof (induct σs Bs arbitrary: σs' rule: induct_2_lists012)
  case Nil thus ?case by simp
next
  case (single σ1 B1)
  thus ?case by (auto simp add: ℛ⇩n⇩d_from_σ_to_σs_description)
next
  case (Cons σ1 σ2 σs A1 A2 As)
  from set_mp[OF ℛ⇩n⇩d_combine⇩n⇩d⇩R⇩l⇩i⇩s⇩t_Sync_subset, OF Cons.prems[simplified]]
  obtain σ1' σs'' where ‹σs' = σ1' # σs''› ‹σ1' ∈ ℛ⇩n⇩d A1 σ1›
    ‹σs'' ∈ ℛ⇩n⇩d ⟪⇩n⇩d⨂⟦E⟧ A2 # As⟫ (σ2 # σs)› by blast
  from Cons.hyps(3)[OF this(3)] this(1, 2)
  show ?case using less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc by simp auto
qed



subsection ‹Transmission of Properties›

lemma finite_trans_transmission_to_iterated_combine⇩n⇩d_Sync:
  ‹(⋀A. A ∈ set As ⟹ finite_trans A) ⟹ finite_trans ⟪⇩n⇩d⨂⟦E⟧ As⟫›
  by (induct As rule: induct_list012) 
    (auto simp add: σ_σs_conv_defs combine⇩R⇩l⇩i⇩s⇩t_Sync_defs finite_trans_def finite_image_set2)

lemma ρ_disjoint_ε_transmission_to_iterated_combine⇩d_Sync:
  ‹(⋀A. A ∈ set As ⟹ ρ_disjoint_ε A) ⟹ ρ_disjoint_ε ⟪⇩d⨂⟦E⟧ As⟫›
  by (induct As rule: induct_list012)
    (simp_all add: ρ_combine⇩R⇩l⇩i⇩s⇩t_Sync ε_combine⇩R⇩l⇩i⇩s⇩t_Sync ρ_disjoint_ε_def combine_Sync_ε_def)

lemma ρ_disjoint_ε_transmission_to_iterated_combine⇩n⇩d_Sync:
  ‹(⋀A. A ∈ set As ⟹ ρ_disjoint_ε A) ⟹ ρ_disjoint_ε ⟪⇩n⇩d⨂⟦E⟧ As⟫›
  by (induct As rule: induct_list012)
    (simp_all add: ρ_combine⇩R⇩l⇩i⇩s⇩t_Sync ε_combine⇩R⇩l⇩i⇩s⇩t_Sync ρ_disjoint_ε_def combine_Sync_ε_def)

lemma at_most_1_elem_term_transmission_to_iterated_combine⇩n⇩d_Sync:
  ‹(⋀A. A ∈ set As ⟹ at_most_1_elem_term A) ⟹ at_most_1_elem_term ⟪⇩n⇩d⨂⟦E⟧ As⟫›
  by (induct As rule: induct_list012,
      simp_all add: at_most_1_elem_term_def σ_σs_conv_defs combine⇩R⇩l⇩i⇩s⇩t_Sync_defs)
    fastforce


lemma same_length_indep_transmission_to_iterated_combine⇩d_Sync:
  ‹length σs = length As ⟹
   (⋀i j. i ≤ length As ⟹ j ≤ length As ⟹ i ≠ j ⟹ 
   indep_enabl ((A⇩0 # As) ! i) ((s⇩0 # σs) ! i) E ((A⇩0 # As) ! j) ((s⇩0 # σs) ! j)) ⟹
   indep_enabl A⇩0 s⇩0 E ⟪⇩d⨂⟦E⟧ As⟫ σs›
proof (induct σs As rule: induct_2_lists012)
  case Nil
  then show ?case by (simp add: indep_enablI)
next
  case (single σ⇩1 A⇩1)
  from single.prems[of 0 1] show ?case
    by (auto simp add: ℛ⇩d_from_σ_to_σs_description
        intro!: indep_enablI dest!: indep_enablD)
next
  case (Cons σ⇩1 σ⇩2 σs A⇩1 A⇩2 As)
  show ?case
  proof (rule indep_enablI)
    fix t⇩0 ts assume assms : ‹t⇩0 ∈ ℛ⇩d A⇩0 s⇩0› ‹ts ∈ ℛ⇩d ⟪⇩d⨂⟦E⟧ A⇩1 # A⇩2 # As⟫ (σ⇩1 # σ⇩2 # σs)›
    from assms(2) obtain t⇩1 ts' where ‹ts = t⇩1 # ts'›
      by (metis Cons.hyps(1) Zero_not_Suc length_Cons list.exhaust_sel list.size(3)
          same_length_ℛ⇩d_iterated_combine⇩d_Sync_description)
    with assms(2)[simplified, THEN set_mp[OF ℛ⇩d_combine⇩d⇩R⇩l⇩i⇩s⇩t_Sync_subset]]
    have ‹ts' ∈ ℛ⇩d ⟪⇩d⨂⟦E⟧ A⇩2 # As⟫ (σ⇩2 # σs)› by simp

    have ‹indep_enabl A⇩0 s⇩0 E ⟪⇩d⨂⟦E⟧ A⇩2 # As⟫ (σ⇩2 # σs)›
    proof (rule Cons.hyps(3))
      show ‹i ≤ length (A⇩2 # As) ⟹ j ≤ length (A⇩2 # As) ⟹ i ≠ j ⟹
            indep_enabl ((A⇩0 # A⇩2 # As) ! i) ((s⇩0 # σ⇩2 # σs) ! i) E
                            ((A⇩0 # A⇩2 # As) ! j) ((s⇩0 # σ⇩2 # σs) ! j)› for i j
        using Cons.prems[of ‹if i = 0 then 0 else Suc i› ‹if j = 0 then 0 else Suc j›]
        by (cases i; cases j) simp_all
    qed
    from this[THEN indep_enablD, OF assms(1) ‹ts' ∈ ℛ⇩d ⟪⇩d⨂⟦E⟧ A⇩2 # As⟫ (σ⇩2 # σs)›]
    have ‹ε A⇩0 t⇩0 ∩ ε ⟪⇩d⨂⟦E⟧ A⇩2 # As⟫ ts' ⊆ E› .
    moreover from Cons.prems[THEN indep_enablD, of 0 ‹Suc 0› t⇩0 t⇩1]
      assms(2)[simplified, THEN set_mp[OF ℛ⇩d_combine⇩d⇩R⇩l⇩i⇩s⇩t_Sync_subset]] assms(1)
    have ‹ε A⇩0 t⇩0 ∩ ε A⇩1 t⇩1 ⊆ E› by (simp add: ‹ts = t⇩1 # ts'›)
    ultimately show ‹ε A⇩0 t⇩0 ∩ ε ⟪⇩d⨂⟦E⟧ A⇩1 # A⇩2 # As⟫ ts ⊆ E›
      by (auto simp add: ε_combine⇩R⇩l⇩i⇩s⇩t_Sync ‹ts = t⇩1 # ts'› combine_Sync_ε_def)
  qed
qed


lemma ω_iterated_combine⇩d_Sync :
  ‹length σs = length As ⟹
   ω ⟪⇩d⨂⟦E⟧ As⟫ σs = (case those (map2 ω As σs) of ◇ ⇒ ◇
    | ⌊terms⌋ ⇒ if card (set terms) = Suc 0 then ⌊THE r. set terms = {r}⌋ else ◇)›
  by (induct σs As rule: induct_2_lists012)
    (auto simp add: σ_σs_conv_defs combine⇩R⇩l⇩i⇩s⇩t_Sync_defs card_1_singleton_iff the_equality split: option.split)

lemma ω_iterated_combine⇩n⇩d_Sync :
  ‹length σs = length As ⟹
   ω ⟪⇩n⇩d⨂⟦E⟧ As⟫ σs = (if As = [] then {} else {r. ∀i < length As. r ∈ ω (As ! i) (σs ! i)})›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by simp
next
  case (single σ1 A1)
  from length_Suc_conv show ?case
    by (auto simp add: σ_σs_conv_defs)
next
  case (Cons σ1 σ2 σs A1 A2 As)
  show ?case (is ‹_ = ?rhs σ1 σ2 σs A1 A2 As›)
  proof (intro subset_antisym subsetI)
    fix r assume ‹r ∈ ω ⟪⇩n⇩d⨂⟦E⟧ A1 # A2 # As⟫ (σ1 # σ2 # σs)›
    hence ‹r ∈ ω A1 σ1› ‹r ∈ ω ⟪⇩n⇩d⨂⟦E⟧ A2 # As⟫ (σ2 # σs)›
      by (simp_all add: combine⇩R⇩l⇩i⇩s⇩t_Sync_defs split: if_split_asm)
    from this(2) have ‹∀i<Suc (length As). r ∈ ω ((A2 # As) ! i) ((σ2 # σs) ! i)›
      by (simp add: Cons.hyps(3))
    with ‹r ∈ ω A1 σ1› show ‹r ∈ ?rhs σ1 σ2 σs A1 A2 As›
      by (auto simp add: less_Suc_eq_0_disj)
  next
    from Cons.hyps(3)
    show ‹r ∈ ?rhs σ1 σ2 σs A1 A2 As ⟹
          r ∈ ω ⟪⇩n⇩d⨂⟦E⟧ A1 # A2 # As⟫ (σ1 # σ2 # σs)› for r
      by (auto simp add: combine⇩R⇩l⇩i⇩s⇩t_Sync_defs)
  qed
qed


subsection ‹Normalization›

lemma ω_iterated_combine⇩n⇩d_Sync_det_ndet_conv:
  ‹length σs = length As ⟹
   ω ⟪⇩n⇩d⨂⟦E⟧ map (λA. ⟪A⟫⇩d⇩↪⇩n⇩d) As⟫ σs = ω ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs›
proof (induct σs As rule: induct_2_lists012)
  case Nil
  show ?case by (simp add: base_trans_det_ndet_conv(1))
next
  case (single σ1 A1)
  show ?case by (simp add: from_det_to_ndet_σ_σs_conv_commute)
next
  case (Cons σ1 σ2 σs A1 A2 As)
  thus ?case
    by (auto simp add: det_ndet_conv_defs combine⇩R⇩l⇩i⇩s⇩t_Sync_defs split: option.split)
qed

lemma τ_iterated_combine⇩n⇩d_Sync_behaviour_when_indep:
  ‹length σs = length As ⟹
   (⋀i j. ⟦i < length As; j < length As; i ≠ j⟧
    ⟹ indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)) ⟹ 
   τ ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs e = τ ⟪⇩n⇩d⨂⟦E⟧ map (λA. ⟪A⟫⇩d⇩↪⇩n⇩d) As⟫ σs e›
proof (induct σs As rule: induct_2_lists012)
  case Nil
  show ?case by simp
next
  case (single σ1 A1)
  show ?case by (simp add: from_det_to_ndet_σ_σs_conv_commute(1))
next
  case (Cons σ1 σ2 σs A1 A2 As)
  have * : ‹τ ⟪⟪⇩d⨂⟦E⟧ A2 # As⟫⟫⇩d⇩↪⇩n⇩d (σ2 # σs) e =
            τ ⟪⇩n⇩d⨂⟦E⟧ map (λA. ⟪A⟫⇩d⇩↪⇩n⇩d) (A2 # As)⟫ (σ2 # σs) e›
  proof (rule Cons.hyps(3))
    show ‹⟦i < length (A2 # As); j < length (A2 # As); i ≠ j⟧
          ⟹ indep_enabl ((A2 # As) ! i) ((σ2 # σs) ! i) E
                              ((A2 # As) ! j) ((σ2 # σs) ! j)› for i j
      using Cons.prems[of ‹Suc i› ‹Suc j›] by simp
  qed
  have ‹τ ⟪⟪⇩d⨂⟦E⟧ A1 # A2 # As⟫⟫⇩d⇩↪⇩n⇩d (σ1 # σ2 # σs) e =
        τ ⟪⟪A1⟫⇩d⇩↪⇩n⇩d ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t ⟪⟪⇩d⨂⟦E⟧ A2 # As⟫⟫⇩d⇩↪⇩n⇩d⟫ (σ1 # σ2 # σs) e›
  proof (subst iterated_combine⇩d_Sync.simps(3), rule τ_combine⇩R⇩l⇩i⇩s⇩t_Sync_behaviour_when_indep)
    show ‹ε A1 σ1 ∩ ε ⟪⇩d⨂⟦E⟧ A2 # As⟫ (σ2 # σs) ⊆ E›
    proof (rule indep_enablD[OF _ ℛ⇩d.init ℛ⇩d.init])
      show ‹indep_enabl A1 σ1 E ⟪⇩d⨂⟦E⟧ A2 # As⟫ (σ2 # σs)›
        by (simp add: Cons.hyps(1) Cons.prems order_le_less_trans
            same_length_indep_transmission_to_iterated_combine⇩d_Sync)
    qed
  qed
  also have ‹… = τ ⟪⇩n⇩d⨂⟦E⟧ map (λA. ⟪A⟫⇩d⇩↪⇩n⇩d) (A1 # A2 # As)⟫ (σ1 # σ2 # σs) e›
    by (use "*" in ‹simp add: combine⇩R⇩l⇩i⇩s⇩t_Sync_defs ε_simps›)
      (metis empty_from_det_to_ndet_is_None_trans option.exhaust)
  finally show ?case .
qed



lemma P⇩S⇩K⇩I⇩P⇩S_iterated_combine⇩n⇩d_Sync_behaviour_when_indep:
  assumes same_length: ‹length σs = length As›
    and indep: ‹⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
                      indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)›
  shows ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ map (λA. ⟪A⟫⇩d⇩↪⇩n⇩d) As⟫⟫⇩n⇩d σs›
proof (fold P⇩S⇩K⇩I⇩P⇩S_nd_from_det_to_ndet_is_P⇩S⇩K⇩I⇩P⇩S_d, rule P⇩S⇩K⇩I⇩P⇩S_nd_eqI_strong_id)
  show ‹σs' ∈ ℛ⇩n⇩d ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs ⟹
        τ ⟪⇩n⇩d⨂⟦E⟧ map (λA. ⟪A⟫⇩d⇩↪⇩n⇩d) As⟫ σs' e = τ ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs' e› for σs' e
  proof (rule τ_iterated_combine⇩n⇩d_Sync_behaviour_when_indep[symmetric])
    show ‹σs' ∈ ℛ⇩n⇩d ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs ⟹ length σs' = length As›
      by (metis ℛ⇩n⇩d_from_det_to_ndet same_length same_length_ℛ⇩d_iterated_combine⇩d_Sync_description)
  next
    show ‹⟦σs' ∈ ℛ⇩n⇩d ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs; i < length As; j < length As; i ≠ j⟧
          ⟹ indep_enabl (As ! i) (σs' ! i) E (As ! j) (σs' ! j)› for i j
      by (subst (asm) ℛ⇩n⇩d_from_det_to_ndet,
          drule same_length_ℛ⇩d_iterated_combine⇩d_Sync_description[OF same_length])
        (meson ℛ⇩d_trans indep_enabl_def indep)
  qed
next
  show ‹σs' ∈ ℛ⇩n⇩d ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs ⟹
        ω ⟪⇩n⇩d⨂⟦E⟧ map (λA. ⟪A⟫⇩d⇩↪⇩n⇩d) As⟫ σs' = ω ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs'› for σs'
    by (metis ℛ⇩n⇩d_from_det_to_ndet ω_iterated_combine⇩n⇩d_Sync_det_ndet_conv same_length
        same_length_ℛ⇩d_iterated_combine⇩d_Sync_description)
qed


lemma P_d_iterated_combine⇩n⇩d_Sync_behaviour_when_indep:
  assumes same_length: ‹length σs = length As›
    and indep: ‹⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
                      indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)›
  shows ‹P⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs = P⟪⟪⇩n⇩d⨂⟦E⟧ map (λA. ⟪A⟫⇩d⇩↪⇩n⇩d) As⟫⟫⇩n⇩d σs›
proof (fold P_nd_from_det_to_ndet_is_P_d, rule P_nd_eqI_strong_id)
  show ‹σs' ∈ ℛ⇩n⇩d ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs ⟹
        τ ⟪⇩n⇩d⨂⟦E⟧ map (λA. ⟪A⟫⇩d⇩↪⇩n⇩d) As⟫ σs' e = τ ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs' e› for σs' e
  proof (rule τ_iterated_combine⇩n⇩d_Sync_behaviour_when_indep[symmetric])
    show ‹σs' ∈ ℛ⇩n⇩d ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs ⟹ length σs' = length As›
      by (metis ℛ⇩n⇩d_from_det_to_ndet same_length same_length_ℛ⇩d_iterated_combine⇩d_Sync_description)
  next
    show ‹⟦σs' ∈ ℛ⇩n⇩d ⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d⇩↪⇩n⇩d σs; i < length As; j < length As; i ≠ j⟧
          ⟹ indep_enabl (As ! i) (σs' ! i) E (As ! j) (σs' ! j)› for i j
      by (subst (asm) ℛ⇩n⇩d_from_det_to_ndet,
          drule same_length_ℛ⇩d_iterated_combine⇩d_Sync_description[OF same_length])
        (meson ℛ⇩d_trans indep_enabl_def indep)
  qed
qed



section ‹Compactification Theorems›

subsection ‹Binary›

subsubsection ‹Pair›

theorem P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩P⇩a⇩i⇩r_Sync :
  fixes E :: ‹'a set› and A⇩0 :: ‹('σ, 'a, 'r, 'α) A⇩n⇩d_scheme›
  assumes ρ_disjoint_ε : ‹ρ_disjoint_ε A⇩0› ‹ρ_disjoint_ε A⇩1›
    and at_most_1_elem_term : ‹at_most_1_elem_term A⇩0› ‹at_most_1_elem_term A⇩1›
  defines A_def: ‹A ≡ ⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫›      
  defines P_def: ‹P ≡ P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩n⇩d› and Q_def: ‹Q ≡ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩n⇩d› and S_def: ‹S ≡ P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d›
  shows ‹P σ⇩0 ⟦E⟧ Q σ⇩1 = S (σ⇩0, σ⇩1)›
proof -
  let ?f = ‹P⇩S⇩K⇩I⇩P⇩S_nd_step (ε A) (τ A) (ω A) (λσ'. case σ' of (σ⇩0, σ⇩1) ⇒ P σ⇩0 ⟦E⟧ Q σ⇩1)›
  note cartprod_rwrt = GlobalNdet_cartprod[of _ _ ‹λx y. _ (x, y)›, simplified]
  note Ndet_and_Sync = Sync_distrib_GlobalNdet_left
    Sync_distrib_GlobalNdet_right
  note Mprefix_Sync_constant =
    SKIP_Sync_Mprefix Mprefix_Sync_SKIP
    STOP_Sync_Mprefix Mprefix_Sync_STOP
  note P_rec = restriction_fix_eq[OF P⇩S⇩K⇩I⇩P⇩S_nd_step_constructive_bis[of A⇩0], folded P⇩S⇩K⇩I⇩P⇩S_nd_def P_def, THEN fun_cong]
  note Q_rec = restriction_fix_eq[OF P⇩S⇩K⇩I⇩P⇩S_nd_step_constructive_bis[of A⇩1], folded P⇩S⇩K⇩I⇩P⇩S_nd_def Q_def, THEN fun_cong]
  have ω_A : ‹ω A (σ⇩0', σ⇩1') = ω A⇩0 σ⇩0' ∩ ω A⇩1 σ⇩1'› for σ⇩0' σ⇩1'
    by (auto simp add: A_def combine⇩P⇩a⇩i⇩r_Sync_defs)
  have ε_A : ‹ε A (σ⇩0', σ⇩1') = combine_sets_Sync (ε A⇩0 σ⇩0') E (ε A⇩1 σ⇩1')› for σ⇩0' σ⇩1'
    by (simp add: A_def ε_combine⇩P⇩a⇩i⇩r_Sync combine_Sync_ε_def)
  have Mprefix_Sync_Mprefix_for_procomata :
    ‹□a∈A → P a ⟦E⟧ □b∈B → Q b =
     (□a∈(A - E - B) → (P a ⟦E⟧ □b∈B → Q b))                            □
     (□b∈(B - E - A) → (□a∈A → P a ⟦E⟧ Q b))                            □
     (□x∈(A ∩ B - E) → (P x ⟦E⟧ □b∈B → Q b) ⊓ (□a∈A → P a ⟦E⟧ Q x)) □
     (□x∈(A ∩ B ∩ E) → (P x ⟦E⟧ Q x))› (is ?eq) for A B and P Q :: ‹'a ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  proof -
    have  * : ‹□a∈(A - E) → (P a ⟦E⟧ □b∈B → Q b) =
              (□a∈(A - E - B) → (P a ⟦E⟧ □b∈B → Q b)) □
              (□a∈(A ∩ B - E) → (P a ⟦E⟧ □b∈B → Q b))›
      by (metis Diff_Int2 Diff_Int_distrib2 Mprefix_Un_distrib Un_Diff_Int)
    have ** : ‹□b∈(B - E) → (□a∈A → P a ⟦E⟧ Q b) =
               (□b∈(B - E - A) → (□a∈A → P a ⟦E⟧ Q b)) □
               (□b∈(A ∩ B - E) → (□a∈A → P a ⟦E⟧ Q b))›
      by (metis (no_types) Int_Diff Int_commute Mprefix_Un_distrib Un_Diff_Int)
    have ‹□a∈A → P a ⟦E⟧ □b∈B → Q b =
          (□a∈(A - E - B) → (P a ⟦E⟧ □b∈B → Q b))    □
          (□b∈(B - E - A) → (□a∈A → P a ⟦E⟧ Q b))    □
          ((□a∈(A ∩ B - E) → (P a ⟦E⟧ □b∈B → Q b))   □
           (□b∈(A ∩ B - E) → (□a∈A → P a ⟦E⟧ Q b)))  □
          (□x∈(A ∩ B ∩ E) → (P x ⟦E⟧ Q x))›
      unfolding Mprefix_Sync_Mprefix
      by (auto simp add: "**" Det_assoc intro!: arg_cong[where f = ‹λP. P □ _›])
        (subst (3) Det_commute, subst Det_assoc,
          auto simp add: "*" Det_commute intro: arg_cong[where f = ‹λP. P □ _›])
    also have ‹(□a∈(A ∩ B - E) → (P a ⟦E⟧ □b∈B → Q b)) □
                (□b∈(A ∩ B - E) → (□a∈A → P a ⟦E⟧ Q b)) =
                □x∈(A ∩ B - E) → ((P x ⟦E⟧ □b∈B → Q b)) ⊓ (□a∈A → P a ⟦E⟧ Q x)›
      by (simp add: Mprefix_Det_Mprefix, rule mono_Mprefix_eq, simp)
    finally show ?thesis .
  qed
  show ‹P σ⇩0 ⟦E⟧ Q σ⇩1 = S (σ⇩0, σ⇩1)›
  proof (rule fun_cong[of ‹λ(σ⇩0, σ⇩1). P σ⇩0 ⟦E⟧ Q σ⇩1› _ ‹(σ⇩0, σ⇩1)›, simplified])
    show ‹(λ(σ⇩0, σ⇩1). P σ⇩0 ⟦E⟧ Q σ⇩1) = S›
    proof (rule restriction_fix_unique[OF P⇩S⇩K⇩I⇩P⇩S_nd_step_constructive_bis[of A],
          symmetric, folded P⇩S⇩K⇩I⇩P⇩S_nd_def S_def])
      show ‹?f = (λ(σ⇩0, σ⇩1). P σ⇩0 ⟦E⟧ Q σ⇩1)›
      proof (rule ext, clarify)
        have ρ_disjoint_ε_bis : ‹ω A⇩0 σ⇩0 ≠ {} ⟹ ε A⇩0 σ⇩0 = {}›
          ‹ω A⇩1 σ⇩1 ≠ {} ⟹ ε A⇩1 σ⇩1 = {}› for σ⇩0 σ⇩1
          by (simp_all add: ρ_simps ρ_disjoint_εD ρ_disjoint_ε)
        show ‹?f (σ⇩0, σ⇩1) = P σ⇩0 ⟦E⟧ Q σ⇩1› for σ⇩0 σ⇩1
        proof (cases ‹ω A⇩0 σ⇩0 = {}›; cases ‹ω A⇩1 σ⇩1 = {}›)
          assume ‹ω A⇩0 σ⇩0 = {}› ‹ω A⇩1 σ⇩1 = {}›
          hence P_rec' : ‹P σ⇩0 = P_nd_step (ε A⇩0) (τ A⇩0) P σ⇩0›
            and Q_rec' : ‹Q σ⇩1 = P_nd_step (ε A⇩1) (τ A⇩1) Q σ⇩1›
            and S_rec' : ‹P⇩S⇩K⇩I⇩P⇩S_nd_step (ε A) (τ A) (ω A) (λ(σ⇩0, σ⇩1). P σ⇩0 ⟦E⟧ Q σ⇩1) (σ⇩0, σ⇩1) =
                        P_nd_step (ε A) (τ A) (λ(σ⇩0, σ⇩1). P σ⇩0 ⟦E⟧ Q σ⇩1) (σ⇩0, σ⇩1)›
            by (simp_all add: P_rec[of σ⇩0] Q_rec[of σ⇩1] ω_A)
          show ‹?f (σ⇩0, σ⇩1) = P σ⇩0 ⟦E⟧ Q σ⇩1›
            unfolding P_rec' Q_rec' S_rec' Mprefix_Sync_Mprefix_for_procomata
            unfolding ε_A Mprefix_Un_distrib
            by (intro arg_cong2[where f = ‹(□)›] mono_Mprefix_eq, fold P_rec' Q_rec',
                auto simp add: A_def Ndet_and_Sync cartprod_rwrt
                combine⇩P⇩a⇩i⇩r_Sync_defs ε_simps GlobalNdet_sets_commute[of ‹τ A⇩1 _ _›]
                simp flip: GlobalNdet_factorization_union
                intro!: mono_GlobalNdet_eq arg_cong2[where f = ‹(⊓)›])
        next
          assume ‹ω A⇩0 σ⇩0 ≠ {}› ‹ω A⇩1 σ⇩1 = {}›
          from ρ_disjoint_ε(1) ‹ω A⇩0 σ⇩0 ≠ {}› have ‹ε A⇩0 σ⇩0 = {}›
            by (simp add: ρ_disjoint_ε_def ρ_simps)
          have ‹?f (σ⇩0, σ⇩1) = □b∈(ε A⇩1 σ⇩1 - E) → (⊓σ⇩1'∈τ A⇩1 σ⇩1 b. (SKIPS (ω A⇩0 σ⇩0) ⟦E⟧ Q σ⇩1'))›
            by (auto simp add: ω_A ε_A ‹ω A⇩1 σ⇩1 = {}› ‹ε A⇩0 σ⇩0 = {}› intro!: mono_Mprefix_eq,
                auto simp add: A_def combine⇩P⇩a⇩i⇩r_Sync_defs ‹ω A⇩0 σ⇩0 ≠ {}›
                ‹ε A⇩0 σ⇩0 = {}› cartprod_rwrt P_rec[of σ⇩0] intro!: mono_GlobalNdet_eq)
          also have ‹… = P σ⇩0 ⟦E⟧ Q σ⇩1›
            by (unfold P_rec[of σ⇩0] Q_rec[of σ⇩1])
              (auto simp add: SKIPS_def Ndet_and_Sync Mprefix_Sync_constant ‹ω A⇩0 σ⇩0 ≠ {}›
                GlobalNdet_Mprefix_distr GlobalNdet_sets_commute[of ‹τ A⇩1 _ _›] ‹ω A⇩1 σ⇩1 = {}›
                intro!: mono_Mprefix_eq mono_GlobalNdet_eq)
          finally show ‹?f (σ⇩0, σ⇩1) = …› .
        next
          assume ‹ω A⇩0 σ⇩0 = {}› ‹ω A⇩1 σ⇩1 ≠ {}›
          from ρ_disjoint_ε(2) ‹ω A⇩1 σ⇩1 ≠ {}› have ‹ε A⇩1 σ⇩1 = {}›
            by (simp add: ρ_disjoint_ε_def ρ_simps)
          have ‹?f (σ⇩0, σ⇩1) = □a∈(ε A⇩0 σ⇩0 - E) → (⊓σ⇩0'∈τ A⇩0 σ⇩0 a. (P σ⇩0' ⟦E⟧ SKIPS (ω A⇩1 σ⇩1)))›
            by (auto simp add: ω_A ε_A ‹ω A⇩0 σ⇩0 = {}› ‹ε A⇩1 σ⇩1 = {}› intro!: mono_Mprefix_eq,
                auto simp add: A_def combine⇩P⇩a⇩i⇩r_Sync_defs ‹ω A⇩1 σ⇩1 ≠ {}›
                ‹ε A⇩1 σ⇩1 = {}› cartprod_rwrt Q_rec[of σ⇩1] intro!: mono_GlobalNdet_eq)
          also have ‹… = P σ⇩0 ⟦E⟧ Q σ⇩1›
            by (unfold P_rec[of σ⇩0] Q_rec[of σ⇩1])
              (auto simp add: SKIPS_def Ndet_and_Sync Mprefix_Sync_constant ‹ω A⇩1 σ⇩1 ≠ {}›
                GlobalNdet_Mprefix_distr GlobalNdet_sets_commute[of ‹τ A⇩0 _ _›] ‹ω A⇩0 σ⇩0 = {}›
                intro!: mono_Mprefix_eq mono_GlobalNdet_eq)
          finally show ‹?f (σ⇩0, σ⇩1) = …› .
        next
          assume ‹ω A⇩0 σ⇩0 ≠ {}› ‹ω A⇩1 σ⇩1 ≠ {}›
          with ρ_disjoint_ε have ‹ε A⇩0 σ⇩0 = {}› ‹ε A⇩1 σ⇩1 = {}›
            by (simp_all add: ρ_disjoint_ε_def ρ_simps)
          from at_most_1_elem_term
          show ‹ω A⇩0 σ⇩0 ≠ {} ⟹ ω A⇩1 σ⇩1 ≠ {} ⟹ ?f (σ⇩0, σ⇩1) = P σ⇩0 ⟦E⟧ Q σ⇩1›
            by (auto simp add: ‹ω A⇩0 σ⇩0 ≠ {}› ‹ω A⇩1 σ⇩1 ≠ {}› ω_A P_rec[of σ⇩0] Q_rec[of σ⇩1]
                SKIPS_def Ndet_and_Sync cartprod_rwrt GlobalNdet_sets_commute[of ‹ω A⇩0 _›]
                ε_A ‹ε A⇩0 σ⇩0 = {}› ‹ε A⇩1 σ⇩1 = {}› elim!: at_most_1_elem_termE)
        qed
      qed
    qed
  qed
qed

corollary P_nd_combine⇩P⇩a⇩i⇩r_Sync :
  ‹P⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩n⇩d σ⇩1 = P⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⟫⇩n⇩d (σ⇩0, σ⇩1)›
proof -
  have ‹P⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩n⇩d σ⇩1 =
        P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⦇ω := λσ. {}⦈⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⦇ω := λσ. {}⦈⟫⇩n⇩d σ⇩1›
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_nd_updated_ω)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⦇ω := λσ. {}⦈ ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⦇ω := λσ. {}⦈⟫⟫⇩n⇩d (σ⇩0, σ⇩1)›
    by (rule P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩P⇩a⇩i⇩r_Sync) simp_all
  also have ‹⟪A⇩0⦇ω := λσ. {}⦈ ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⦇ω := λσ. {}⦈⟫ = ⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⦇ω := λσ. {}⦈›
    by (simp add: combine⇩P⇩a⇩i⇩r_Sync_defs, intro ext, simp)
  also have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⦇ω := λσ. {}⦈⟫⇩n⇩d = P⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⟫⇩n⇩d›
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_nd_updated_ω)
  finally show ?thesis .
qed

corollary P⇩S⇩K⇩I⇩P⇩S_d_combine⇩P⇩a⇩i⇩r_Sync:
  ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⟫⇩d (σ⇩0, σ⇩1)›
  if ‹ρ_disjoint_ε A⇩0› and ‹ρ_disjoint_ε A⇩1› and ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›
proof -
  have ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⟫⇩d⇩↪⇩n⇩d⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩1⟫⇩d⇩↪⇩n⇩d⟫⇩n⇩d σ⇩1›
    by (simp flip: P⇩S⇩K⇩I⇩P⇩S_nd_from_det_to_ndet_is_P⇩S⇩K⇩I⇩P⇩S_d)
  also from that(1, 2) have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪⟪A⇩0⟫⇩d⇩↪⇩n⇩d ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r ⟪A⇩1⟫⇩d⇩↪⇩n⇩d⟫⟫⇩n⇩d (σ⇩0, σ⇩1)›
    by (auto intro: P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩P⇩a⇩i⇩r_Sync)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⟫⇩d (σ⇩0, σ⇩1)›
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_combine⇩P⇩a⇩i⇩r_Sync_behaviour_when_indep ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›)
  finally show ?thesis .
qed

corollary P_d_combine⇩P⇩a⇩i⇩r_Sync:
  ‹P⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩d σ⇩1 = P⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⟫⇩d (σ⇩0, σ⇩1)›
  if ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›
proof -
  have ‹P⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩d σ⇩1 =
        P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⦇ω := λσ. ◇⦈⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⦇ω := λσ. ◇⦈⟫⇩d σ⇩1›
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_d_updated_ω)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⦇ω := λσ. ◇⦈ ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⦇ω := λσ. ◇⦈⟫⟫⇩d (σ⇩0, σ⇩1)›
    by (subst P⇩S⇩K⇩I⇩P⇩S_d_combine⇩P⇩a⇩i⇩r_Sync, simp_all add: ρ_simps ρ_disjoint_ε_def)
      (rule indep_enablI,
        use ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›[THEN indep_enablD] in ‹simp add: ε_simps›)
  also have ‹⟪A⇩0⦇ω := λσ. ◇⦈ ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⦇ω := λσ. ◇⦈⟫ = ⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⦇ω := λσ. ◇⦈›
    by (simp add: combine⇩P⇩a⇩i⇩r_Sync_defs, intro ext, simp)
  also have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⦇ω := λσ. ◇⦈⟫⇩d = P⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⟫⇩d›
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_d_updated_ω)
  finally show ?thesis .
qed



subsubsection ‹Pairlist›

theorem P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync :
  ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩n⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩n⇩d [σ⇩0, σ⇩1]›
  if ‹ρ_disjoint_ε A⇩0› ‹ρ_disjoint_ε A⇩1› ‹at_most_1_elem_term A⇩0› ‹at_most_1_elem_term A⇩1›
proof -
  from P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩P⇩a⇩i⇩r_Sync that
  have ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩n⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⟫⇩n⇩d (σ⇩0, σ⇩1)› .
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩n⇩d [σ⇩0, σ⇩1]›
    by (auto intro!: P⇩S⇩K⇩I⇩P⇩S_nd_eqI_strong[of ‹λ(r, s). [r, s]› _ ‹(σ⇩0, σ⇩1)›, simplified] inj_onI)
      (auto simp add: combine_Sync_defs split: if_split_asm)
  finally show ?thesis .
qed

corollary P_nd_combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync :
  ‹P⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩n⇩d σ⇩1 = P⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩n⇩d [σ⇩0, σ⇩1]›
proof -
  have ‹P⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩n⇩d σ⇩1 =
        P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⦇ω := λσ. {}⦈⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⦇ω := λσ. {}⦈⟫⇩n⇩d σ⇩1›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_nd_updated_ω)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⦇ω := λσ. {}⦈ ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⦇ω := λσ. {}⦈⟫⟫⇩n⇩d [σ⇩0, σ⇩1]›
    by (rule P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync) simp_all
  also have ‹⟪A⇩0⦇ω := λσ. {}⦈ ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⦇ω := λσ. {}⦈⟫ = ⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⦇ω := λσ. {}⦈›
    by (simp add: combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync_defs, intro ext, simp)
  also have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⦇ω := λσ. {}⦈⟫⇩n⇩d = P⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩n⇩d›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_nd_updated_ω)
  finally show ?thesis .
qed

corollary P⇩S⇩K⇩I⇩P⇩S_d_combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync :
  ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩d [σ⇩0, σ⇩1]›
  if ‹ρ_disjoint_ε A⇩0› and ‹ρ_disjoint_ε A⇩1› and ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›
proof -
  have ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⟫⇩d⇩↪⇩n⇩d⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩1⟫⇩d⇩↪⇩n⇩d⟫⇩n⇩d σ⇩1›
    by (simp flip: P⇩S⇩K⇩I⇩P⇩S_nd_from_det_to_ndet_is_P⇩S⇩K⇩I⇩P⇩S_d)
  also from that(1, 2) have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪⟪A⇩0⟫⇩d⇩↪⇩n⇩d ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t ⟪A⇩1⟫⇩d⇩↪⇩n⇩d⟫⟫⇩n⇩d [σ⇩0, σ⇩1]›
    by (auto intro: P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩d [σ⇩0, σ⇩1]›
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync_behaviour_when_indep ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›)
  finally show ?thesis .
qed

corollary P_d_combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync :
  ‹P⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩d σ⇩1 = P⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩d [σ⇩0, σ⇩1]›
  if ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›
proof -
  have ‹P⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩d σ⇩1 =
        P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⦇ω := λσ. ◇⦈⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⦇ω := λσ. ◇⦈⟫⇩d σ⇩1›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_d_updated_ω)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⦇ω := λσ. ◇⦈ ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⦇ω := λσ. ◇⦈⟫⟫⇩d [σ⇩0, σ⇩1]›
    by (subst P⇩S⇩K⇩I⇩P⇩S_d_combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync, simp_all)
      (rule indep_enablI,
        use ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›[THEN indep_enablD] in simp)
  also have ‹⟪A⇩0⦇ω := λσ. ◇⦈ ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⦇ω := λσ. ◇⦈⟫ = ⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⦇ω := λσ. ◇⦈›
    by (simp add: combine⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t_Sync_defs, intro ext, simp)
  also have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⦇ω := λσ. ◇⦈⟫⇩d = P⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩d›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_d_updated_ω)
  finally show ?thesis .
qed



subsection ‹Rlist›

theorem P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩R⇩l⇩i⇩s⇩t_Sync :
  ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩n⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩n⇩d (σ⇩0 # σ⇩1)›
  if ‹ρ_disjoint_ε A⇩0› ‹ρ_disjoint_ε A⇩1› ‹at_most_1_elem_term A⇩0› ‹at_most_1_elem_term A⇩1›
proof -
  from P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩P⇩a⇩i⇩r_Sync that
  have ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩n⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⟫⇩n⇩d (σ⇩0, σ⇩1)› .
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩n⇩d (σ⇩0 # σ⇩1)›
    by (auto intro!: P⇩S⇩K⇩I⇩P⇩S_nd_eqI_strong[of ‹λ(r, s). r # s› _ ‹(σ⇩0, σ⇩1)›, simplified] inj_onI)
      (auto simp add: combine_Sync_defs split: if_split_asm)
  finally show ?thesis .
qed

corollary P_nd_combine⇩R⇩l⇩i⇩s⇩t_Sync :
  ‹P⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩n⇩d σ⇩1 = P⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩n⇩d (σ⇩0 # σ⇩1)›
proof -
  have ‹P⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩n⇩d σ⇩1 =
        P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⦇ω := λσ. {}⦈⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⦇ω := λσ. {}⦈⟫⇩n⇩d σ⇩1›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_nd_updated_ω)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⦇ω := λσ. {}⦈ ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⦇ω := λσ. {}⦈⟫⟫⇩n⇩d (σ⇩0 # σ⇩1)›
    by (rule P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩R⇩l⇩i⇩s⇩t_Sync) simp_all
  also have ‹⟪A⇩0⦇ω := λσ. {}⦈ ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⦇ω := λσ. {}⦈⟫ = ⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⦇ω := λσ. {}⦈›
    by (simp add: combine⇩R⇩l⇩i⇩s⇩t_Sync_defs, intro ext, simp)
  also have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⦇ω := λσ. {}⦈⟫⇩n⇩d = P⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩n⇩d›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_nd_updated_ω)
  finally show ?thesis .
qed

corollary P⇩S⇩K⇩I⇩P⇩S_d_combine⇩R⇩l⇩i⇩s⇩t_Sync :
  ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩d (σ⇩0 # σ⇩1)›
  if ‹ρ_disjoint_ε A⇩0› and ‹ρ_disjoint_ε A⇩1› and ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›
proof -
  have ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⟫⇩d⇩↪⇩n⇩d⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩1⟫⇩d⇩↪⇩n⇩d⟫⇩n⇩d σ⇩1›
    by (simp flip: P⇩S⇩K⇩I⇩P⇩S_nd_from_det_to_ndet_is_P⇩S⇩K⇩I⇩P⇩S_d)
  also from that(1, 2) have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪⟪A⇩0⟫⇩d⇩↪⇩n⇩d ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t ⟪A⇩1⟫⇩d⇩↪⇩n⇩d⟫⟫⇩n⇩d (σ⇩0 # σ⇩1)›
    by (auto intro: P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩R⇩l⇩i⇩s⇩t_Sync)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩d (σ⇩0 # σ⇩1)›
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_combine⇩R⇩l⇩i⇩s⇩t_Sync_behaviour_when_indep ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›)
  finally show ?thesis .
qed

corollary P_d_combine⇩R⇩l⇩i⇩s⇩t_Sync :
  ‹P⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩d σ⇩1 = P⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩d (σ⇩0 # σ⇩1)›
  if ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›
proof -
  have ‹P⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩d σ⇩1 =
        P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⦇ω := λσ. ◇⦈⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⦇ω := λσ. ◇⦈⟫⇩d σ⇩1›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_d_updated_ω)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⦇ω := λσ. ◇⦈ ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⦇ω := λσ. ◇⦈⟫⟫⇩d (σ⇩0 # σ⇩1)›
    by (subst P⇩S⇩K⇩I⇩P⇩S_d_combine⇩R⇩l⇩i⇩s⇩t_Sync, simp_all)
      (rule indep_enablI,
        use ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›[THEN indep_enablD] in simp)
  also have ‹⟪A⇩0⦇ω := λσ. ◇⦈ ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⦇ω := λσ. ◇⦈⟫ = ⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⦇ω := λσ. ◇⦈›
    by (simp add: combine⇩R⇩l⇩i⇩s⇩t_Sync_defs, intro ext, simp)
  also have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⦇ω := λσ. ◇⦈⟫⇩d = P⟪⟪A⇩0 ⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t A⇩1⟫⟫⇩d›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_d_updated_ω)
  finally show ?thesis .
qed



subsection ‹ListslenL›

theorem P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync :
  assumes same_length_reach0 : ‹⋀σ⇩0'. σ⇩0' ∈ ℛ⇩n⇩d A⇩0 σ⇩0 ⟹ length σ⇩0' = len⇩0›
    and ρ_disjoint_ε : ‹ρ_disjoint_ε A⇩0› ‹ρ_disjoint_ε A⇩1› ‹at_most_1_elem_term A⇩0› ‹at_most_1_elem_term A⇩1›
  shows ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩n⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⟫⇩n⇩d (σ⇩0 @ σ⇩1)›
proof -
  from set_mp[OF ℛ⇩n⇩d_combine⇩n⇩d⇩P⇩a⇩i⇩r_Sync_subset]
  have * : ‹σ' ∈ ℛ⇩n⇩d ⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫ (σ⇩0, σ⇩1) ⟹
            ∃σ⇩0' σ⇩1'. σ' = (σ⇩0', σ⇩1') ∧ σ⇩0' ∈ ℛ⇩n⇩d A⇩0 σ⇩0 ∧ σ⇩1' ∈ ℛ⇩n⇩d A⇩1 σ⇩1› for σ' by fast
  from P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩P⇩a⇩i⇩r_Sync assms(2-5)
  have ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩n⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩P⇩a⇩i⇩r A⇩1⟫⟫⇩n⇩d (σ⇩0, σ⇩1)› .
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⟫⇩n⇩d (σ⇩0 @ σ⇩1)›
    by  (auto intro!: P⇩S⇩K⇩I⇩P⇩S_nd_eqI_strong[of ‹λ(r, s). r @ s› _ ‹(σ⇩0, σ⇩1)›, simplified] inj_onI
        dest!: "*" same_length_reach0 simp add: same_length_reach0 image_iff)
      (auto simp add: combine_Sync_defs ε_simps split: if_split_asm,
        (metis SigmaI UnCI case_prod_conv insertI1)+)
  finally show ?thesis .
qed

corollary P_nd_combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync :
  ‹P⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩n⇩d σ⇩1 = P⟪⟪A⇩0 ⇩n⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⟫⇩n⇩d (σ⇩0 @ σ⇩1)›
  if ‹⋀σ⇩0'. σ⇩0' ∈ ℛ⇩n⇩d A⇩0 σ⇩0 ⟹ length σ⇩0' = len⇩0›
proof -
  have ‹P⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩n⇩d σ⇩1 =
        P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⦇ω := λσ. {}⦈⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⦇ω := λσ. {}⦈⟫⇩n⇩d σ⇩1›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_nd_updated_ω)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⦇ω := λσ. {}⦈ ⇩n⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⦇ω := λσ. {}⦈⟫⟫⇩n⇩d (σ⇩0 @ σ⇩1)›
    by (rule P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync) (simp_all add: that)
  also have ‹⟪A⇩0⦇ω := λσ. {}⦈ ⇩n⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⦇ω := λσ. {}⦈⟫ = ⟪A⇩0 ⇩n⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⦇ω := λσ. {}⦈›
    by (simp add: combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync_defs, intro ext, simp)
  also have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⦇ω := λσ. {}⦈⟫⇩n⇩d = P⟪⟪A⇩0 ⇩n⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⟫⇩n⇩d›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_nd_updated_ω)
  finally show ?thesis .
qed

corollary P⇩S⇩K⇩I⇩P⇩S_d_combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync :
  ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⟫⇩d (σ⇩0 @ σ⇩1)›
  if ‹⋀σ⇩0'. σ⇩0' ∈ ℛ⇩d A⇩0 σ⇩0 ⟹ length σ⇩0' = len⇩0›
    ‹ρ_disjoint_ε A⇩0› ‹ρ_disjoint_ε A⇩1› ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›
proof -
  have ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⟫⇩d σ⇩1 = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⟫⇩d⇩↪⇩n⇩d⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩1⟫⇩d⇩↪⇩n⇩d⟫⇩n⇩d σ⇩1›
    by (simp flip: P⇩S⇩K⇩I⇩P⇩S_nd_from_det_to_ndet_is_P⇩S⇩K⇩I⇩P⇩S_d)
  also from that(1-3) have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪⟪A⇩0⟫⇩d⇩↪⇩n⇩d ⇩n⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L ⟪A⇩1⟫⇩d⇩↪⇩n⇩d⟫⟫⇩n⇩d (σ⇩0 @ σ⇩1)›
    by (auto simp add: ℛ⇩n⇩d_from_det_to_ndet intro!: P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⟫⇩d (σ⇩0 @ σ⇩1)›
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync_behaviour_when_indep that(1, 4))
  finally show ?thesis .
qed

corollary P_d_combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync :
  ‹P⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩d σ⇩1 = P⟪⟪A⇩0 ⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⟫⇩d (σ⇩0 @ σ⇩1)›
  if ‹⋀σ⇩0'. σ⇩0' ∈ ℛ⇩d A⇩0 σ⇩0 ⟹ length σ⇩0' = len⇩0› ‹indep_enabl A⇩0 σ⇩0 E A⇩1 σ⇩1›
proof -
  have ‹P⟪A⇩0⟫⇩d σ⇩0 ⟦E⟧ P⟪A⇩1⟫⇩d σ⇩1 =
        P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⦇ω := λσ. ◇⦈⟫⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪A⇩1⦇ω := λσ. ◇⦈⟫⇩d σ⇩1›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_d_updated_ω)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0⦇ω := λσ. ◇⦈ ⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⦇ω := λσ. ◇⦈⟫⟫⇩d (σ⇩0 @ σ⇩1)›
    by (subst P⇩S⇩K⇩I⇩P⇩S_d_combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync) (simp_all add: that)
  also have ‹⟪A⇩0⦇ω := λσ. ◇⦈ ⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⦇ω := λσ. ◇⦈⟫ = ⟪A⇩0 ⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⦇ω := λσ. ◇⦈›
    by (simp add: combine⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L_Sync_defs, intro ext, simp)
  also have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⦇ω := λσ. ◇⦈⟫⇩d = P⟪⟪A⇩0 ⇩d⊗⟦len⇩0, E⟧⇩L⇩i⇩s⇩t⇩s⇩l⇩e⇩n⇩L A⇩1⟫⟫⇩d›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_d_updated_ω)
  finally show ?thesis .
qed



subsection ‹Multiple›

theorem P⇩S⇩K⇩I⇩P⇩S_nd_compactification_Sync:
  ‹⟦length σs = length As; ⋀A. A ∈ set As ⟹ ρ_disjoint_ε A;
    ⋀A. A ∈ set As ⟹ at_most_1_elem_term A⟧
   ⟹ ❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ As⟫⟫⇩n⇩d σs›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by (simp, subst P⇩S⇩K⇩I⇩P⇩S_nd_rec, simp)
next
  case (single σ⇩0 A⇩0) show ?case
    by (auto simp add: σ_σs_conv_defs intro!: inj_onI P⇩S⇩K⇩I⇩P⇩S_nd_eqI_strong)
next
  case (Cons σ⇩0 σ⇩1 σs A⇩0 A⇩1 As)
  have ‹❙⟦E❙⟧ (σ, A) ∈# mset (zip (σ⇩0 # σ⇩1 # σs) (A⇩0 # A⇩1 # As)). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ =
        P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ ❙⟦E❙⟧ (σ, A) ∈# mset (zip (σ⇩1 # σs) (A⇩1 # As)). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ› by simp
  also have ‹❙⟦E❙⟧ (σ, A) ∈# mset (zip (σ⇩1 # σs) (A⇩1 # As)). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ =
             P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ A⇩1 # As⟫⟫⇩n⇩d (σ⇩1 # σs)›
    by (rule Cons.hyps(3)) (simp_all add: Cons.prems)
  also have ‹P⇩S⇩K⇩I⇩P⇩S⟪A⇩0⟫⇩n⇩d σ⇩0 ⟦E⟧ P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ A⇩1 # As⟫⟫⇩n⇩d (σ⇩1 # σs) =
             P⇩S⇩K⇩I⇩P⇩S⟪⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t ⟪⇩n⇩d⨂⟦E⟧ A⇩1 # As⟫⟫⟫⇩n⇩d (σ⇩0 # σ⇩1 # σs)›
    by (rule P⇩S⇩K⇩I⇩P⇩S_nd_combine⇩R⇩l⇩i⇩s⇩t_Sync
        [OF _ ρ_disjoint_ε_transmission_to_iterated_combine⇩n⇩d_Sync
          _ at_most_1_elem_term_transmission_to_iterated_combine⇩n⇩d_Sync])
      (simp_all add: Cons.prems)
  also have ‹⟪A⇩0 ⇩n⇩d⊗⟦E⟧⇩R⇩l⇩i⇩s⇩t ⟪⇩n⇩d⨂⟦E⟧ A⇩1 # As⟫⟫ = ⟪⇩n⇩d⨂⟦E⟧ A⇩0 # A⇩1 # As⟫› by simp
  finally show ?case .
qed

lemma P_nd_compactification_Sync:
  ‹length σs = length As ⟹
   ❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⟪A⟫⇩n⇩d σ = P⟪⟪⇩n⇩d⨂⟦E⟧ As⟫⟫⇩n⇩d σs›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by (simp, subst P_nd_rec, simp)
next
  case (single σ⇩0 A⇩0) show ?case
    by (simp add: P_nd_from_σ_to_σs_is_P_nd)
next
  case (Cons σ⇩0 σ⇩1 σs A⇩0 A⇩1 As) thus ?case
    by (simp add: P_nd_combine⇩R⇩l⇩i⇩s⇩t_Sync)
qed

lemma P⇩S⇩K⇩I⇩P⇩S_d_compactification_Sync:
  ‹⟦length σs = length As; ⋀A. A ∈ set As ⟹ ρ_disjoint_ε A;
    ⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
          indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)⟧ ⟹
   ❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩d σ = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by (simp, subst P⇩S⇩K⇩I⇩P⇩S_d_rec, simp)
next
  case (single σ⇩0 A⇩0) show ?case
    by (auto simp add: RenamingTick_P⇩S⇩K⇩I⇩P⇩S_d σ_σs_conv_defs
        intro!: inj_onI P⇩S⇩K⇩I⇩P⇩S_d_eqI_strong split: option.split)
next
  case (Cons σ⇩0 σ⇩1 σs A⇩0 A⇩1 As)
  have ρ_disjoint_ε : ‹A ∈ set (A⇩1 # As) ⟹ ρ_disjoint_ε A› for A
    by (simp add: Cons.prems(1))
  have indep_enabl :
    ‹⟦i < length (A⇩1 # As); j < length (A⇩1 # As); i ≠ j⟧ ⟹
     indep_enabl ((A⇩1 # As) ! i) ((σ⇩1 # σs) ! i) E ((A⇩1 # As) ! j) ((σ⇩1 # σs) ! j)› for i j
    by (metis Cons.prems(2) Suc_less_eq length_Cons nat.inject nth_Cons_Suc)
  have ‹ρ_disjoint_ε A⇩0› by (simp add: Cons.prems(1))
  moreover have ‹ρ_disjoint_ε ⟪⇩d⨂⟦E⟧ A⇩1 # As⟫›
    by (meson ρ_disjoint_ε ρ_disjoint_ε_transmission_to_iterated_combine⇩d_Sync)
  moreover have ‹indep_enabl A⇩0 σ⇩0 E ⟪⇩d⨂⟦E⟧ A⇩1 # As⟫ (σ⇩1 # σs)›
    by (metis Cons.hyps(1) Cons.prems(2) length_Cons less_Suc_eq_le
        same_length_indep_transmission_to_iterated_combine⇩d_Sync)
  ultimately show ?case 
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_d_combine⇩R⇩l⇩i⇩s⇩t_Sync
        Cons.hyps(3)[OF ρ_disjoint_ε indep_enabl, simplified])
qed

lemma P_d_compactification_Sync:
  ‹⟦length σs = length As;
    ⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
          indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)⟧ ⟹
   ❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⟪A⟫⇩d σ = P⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by (simp, subst P_d_rec, simp)
next
  case (single σ⇩0 A⇩0) show ?case
    by (simp, subst (1 2) P⇩S⇩K⇩I⇩P⇩S_d_updated_ω)
      (auto simp add: RenamingTick_P⇩S⇩K⇩I⇩P⇩S_d σ_σs_conv_defs
        intro!: inj_onI P⇩S⇩K⇩I⇩P⇩S_d_eqI_strong split: option.split)
next
  case (Cons σ⇩0 σ⇩1 σs A⇩0 A⇩1 As)
  have indep_enabl :
    ‹⟦i < length (A⇩1 # As); j < length (A⇩1 # As); i ≠ j⟧ ⟹
     indep_enabl ((A⇩1 # As) ! i) ((σ⇩1 # σs) ! i) E ((A⇩1 # As) ! j) ((σ⇩1 # σs) ! j)› for i j
    by (metis Cons.prems Suc_less_eq length_Cons nat.inject nth_Cons_Suc)
  have ‹indep_enabl A⇩0 σ⇩0 E ⟪⇩d⨂⟦E⟧ A⇩1 # As⟫ (σ⇩1 # σs)›
    by (metis Cons.hyps(1) Cons.prems length_Cons less_Suc_eq_le
        same_length_indep_transmission_to_iterated_combine⇩d_Sync)
  thus ?case 
    by (simp add: P_d_combine⇩R⇩l⇩i⇩s⇩t_Sync
        Cons.hyps(3)[OF indep_enabl, simplified])
qed




corollary P⇩S⇩K⇩I⇩P⇩S_nd_compactification_Sync_order_is_arbitrary:
  ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ As⟫⟫⇩n⇩d σs = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ As'⟫⟫⇩n⇩d σs'›
  if ‹length σs = length As› ‹length σs' = length As'›
    ‹mset (zip σs As) = mset (zip σs' As')› 
    ‹⋀A. A ∈ set As ⟹ ρ_disjoint_ε A›
    ‹⋀A. A ∈ set As ⟹ at_most_1_elem_term A›
proof -
  have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ As⟫⟫⇩n⇩d σs = ❙⟦E❙⟧ (σ, A)∈#mset (zip σs As). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ›
    by (rule P⇩S⇩K⇩I⇩P⇩S_nd_compactification_Sync[OF that(1, 4, 5), symmetric])
  also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip σs' As'). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ›
    by (simp only: that(3))
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ As'⟫⟫⇩n⇩d σs'›
  proof (rule P⇩S⇩K⇩I⇩P⇩S_nd_compactification_Sync[OF that(2)])
    show ‹A ∈ set As' ⟹ ρ_disjoint_ε A› for A
      by (metis in_set_impl_in_set_zip2 set_mset_mset set_zip_rightD that(2-4))
  next
    show ‹A ∈ set As' ⟹ at_most_1_elem_term A› for A
      by (metis in_set_impl_in_set_zip2 set_mset_mset set_zip_rightD that(2, 3, 5))
  qed
  finally show ?thesis .
qed

corollary P_nd_compactification_Sync_order_is_arbitrary:
  ‹P⟪⟪⇩n⇩d⨂⟦E⟧ As⟫⟫⇩n⇩d σs = P⟪⟪⇩n⇩d⨂⟦E⟧ As'⟫⟫⇩n⇩d σs'›
  if ‹length σs = length As› ‹length σs' = length As'›
    ‹mset (zip σs As) = mset (zip σs' As')› 
proof -
  have ‹P⟪⟪⇩n⇩d⨂⟦E⟧ As⟫⟫⇩n⇩d σs = ❙⟦E❙⟧ (σ, A)∈#mset (zip σs As). P⟪A⟫⇩n⇩d σ›
    by (fact P_nd_compactification_Sync[OF that(1), symmetric])
  also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip σs' As'). P⟪A⟫⇩n⇩d σ›
    by (simp only: that(3))
  also have ‹… = P⟪⟪⇩n⇩d⨂⟦E⟧ As'⟫⟫⇩n⇩d σs'›
    by (fact P_nd_compactification_Sync[OF that(2)])
  finally show ?thesis .
qed

corollary P⇩S⇩K⇩I⇩P⇩S_d_compactification_Sync_order_is_arbitrary:
  ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩d⨂⟦E⟧ As'⟫⟫⇩d σs'›
  if ‹length σs = length As› ‹length σs' = length As'›
    ‹mset (zip σs As) = mset (zip σs' As')› 
    ‹⋀A. A ∈ set As ⟹ ρ_disjoint_ε A›
    ‹⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
            indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)›
proof -
  have ‹P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs = ❙⟦E❙⟧ (σ, A)∈#mset (zip σs As). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩d σ›
    by (rule P⇩S⇩K⇩I⇩P⇩S_d_compactification_Sync[OF that(1, 4, 5), symmetric])
  also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip σs' As'). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩d σ›
    by (simp only: that(3))
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩d⨂⟦E⟧ As'⟫⟫⇩d σs'›
  proof (rule P⇩S⇩K⇩I⇩P⇩S_d_compactification_Sync[OF that(2)])
    show ‹A ∈ set As' ⟹ ρ_disjoint_ε A› for A
      by (metis in_set_impl_in_set_zip2 set_mset_mset set_zip_rightD that(2-4))
  next
    from ‹length σs = length As› ‹length σs' = length As'› ‹mset (zip σs As) = mset (zip σs' As')›
    obtain n where * : ‹length σs = n› ‹length σs' = n› ‹length As = n› ‹length As' = n›
      by (metis length_zip min_less_iff_conj nat_neq_iff size_mset)
    from that(3)[symmetric, THEN permutation_Ex_bij] obtain f
      where ** : ‹bij_betw f {..<n} {..<n}›
        ‹i < n ⟹ zip σs' As' ! i = zip σs As ! f i› for i by (auto simp add: "*")
    { fix i assume ‹i < n›
      hence ‹f i < n› using "**"(1) bij_betwE by blast
      from ‹i < n› have ‹zip σs' As' ! i = (σs' ! i, As' ! i)› by (simp add: "*"(2, 4))
      moreover from ‹f i < n› have ‹zip σs As ! f i = (σs ! f i, As ! f i)›
        by (simp add: "*"(1, 3))
      ultimately have ‹σs' ! i = σs ! f i› ‹As' ! i = As ! f i›
        using "**"(2)[OF ‹i < n›] by simp_all
    } note *** = this
    fix i j assume ‹i < length As'› ‹j < length As'› ‹i ≠ j›
    hence ‹i < n› ‹j < n› by (simp_all add: "*"(2, 4))
    with bij_betw_imp_surj_on[OF "**"(1)] bij_betw_imp_inj_on[OF "**"(1)] ‹i ≠ j›
    have ‹f i < length As› ‹f j < length As› ‹f i ≠ f j›
      by (auto simp add: "*" dest: inj_onD)
    from that(5)[OF this]
    show ‹indep_enabl (As' ! i) (σs' ! i) E (As' ! j) (σs' ! j)›
      by (simp add: "***"(1, 2) ‹i < n› ‹j < n›)
  qed
  finally show ?thesis .
qed

corollary P_d_compactification_Sync_order_is_arbitrary:
  ‹P⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs = P⟪⟪⇩d⨂⟦E⟧ As'⟫⟫⇩d σs'›
  if ‹length σs = length As› ‹length σs' = length As'›
    ‹mset (zip σs As) = mset (zip σs' As')› 
    ‹⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
            indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)›
proof -
  have ‹P⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs = ❙⟦E❙⟧ (σ, A)∈#mset (zip σs As). P⟪A⟫⇩d σ›
    by (rule P_d_compactification_Sync[OF that(1, 4), symmetric])
  also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip σs' As'). P⟪A⟫⇩d σ›
    by (simp only: that(3))
  also have ‹… = P⟪⟪⇩d⨂⟦E⟧ As'⟫⟫⇩d σs'›
  proof (rule P_d_compactification_Sync[OF that(2)])
    from ‹length σs = length As› ‹length σs' = length As'› ‹mset (zip σs As) = mset (zip σs' As')›
    obtain n where * : ‹length σs = n› ‹length σs' = n› ‹length As = n› ‹length As' = n›
      by (metis length_zip min_less_iff_conj nat_neq_iff size_mset)
    from that(3)[symmetric, THEN permutation_Ex_bij] obtain f
      where ** : ‹bij_betw f {..<n} {..<n}›
        ‹i < n ⟹ zip σs' As' ! i = zip σs As ! f i› for i by (auto simp add: "*")
    { fix i assume ‹i < n›
      hence ‹f i < n› using "**"(1) bij_betwE by blast
      from ‹i < n› have ‹zip σs' As' ! i = (σs' ! i, As' ! i)› by (simp add: "*"(2, 4))
      moreover from ‹f i < n› have ‹zip σs As ! f i = (σs ! f i, As ! f i)›
        by (simp add: "*"(1, 3))
      ultimately have ‹σs' ! i = σs ! f i› ‹As' ! i = As ! f i›
        using "**"(2)[OF ‹i < n›] by simp_all
    } note *** = this
    fix i j assume ‹i < length As'› ‹j < length As'› ‹i ≠ j›
    hence ‹i < n› ‹j < n› by (simp_all add: "*"(2, 4))
    with bij_betw_imp_surj_on[OF "**"(1)] bij_betw_imp_inj_on[OF "**"(1)] ‹i ≠ j›
    have ‹f i < length As› ‹f j < length As› ‹f i ≠ f j›
      by (auto simp add: "*" dest: inj_onD)
    from that(4)[OF this]
    show ‹indep_enabl (As' ! i) (σs' ! i) E (As' ! j) (σs' ! j)›
      by (simp add: "***"(1, 2) ‹i < n› ‹j < n›)
  qed
  finally show ?thesis .
qed



section ‹Derived Versions›

lemma P⇩S⇩K⇩I⇩P⇩S_nd_compactification_Sync_upt_version:
  ‹❙⟦E❙⟧ P ∈# mset (map Q [0..<n]). P = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ map A [0..<n]⟫⟫⇩n⇩d (replicate n 0)›
  if ‹⋀i. i < n ⟹ ρ_disjoint_ε (A i)›
    ‹⋀i. i < n ⟹ at_most_1_elem_term (A i)›
    ‹⋀i. i < n ⟹ P⇩S⇩K⇩I⇩P⇩S⟪A i⟫⇩n⇩d 0 = Q i›
proof -
  have ‹❙⟦E❙⟧ P ∈# mset (map Q [0..<n]). P = ❙⟦E❙⟧ i ∈# (mset_set {0..<n}). Q i›
    by (auto intro: mono_MultiSync_eq2)
  also have ‹… = ❙⟦E❙⟧ i ∈# (mset_set {0..<n}). P⇩S⇩K⇩I⇩P⇩S⟪A i⟫⇩n⇩d 0›
    by (auto simp add: that(3) intro: mono_MultiSync_eq)
  also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate n 0) (map A [0..<n])). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ›
  proof (induct n rule: nat_induct_012)
    case (Suc k)
    have ‹❙⟦E❙⟧ i∈#mset_set {0..<Suc k}. P⇩S⇩K⇩I⇩P⇩S⟪A i⟫⇩n⇩d 0 =
          P⇩S⇩K⇩I⇩P⇩S⟪A k⟫⇩n⇩d 0 ⟦E⟧ ❙⟦E❙⟧ i∈#mset_set {0..<k}. P⇩S⇩K⇩I⇩P⇩S⟪A i⟫⇩n⇩d 0›
      by (subst atLeastLessThanSuc, simp, rule MultiSync_add)
        (metis Suc.hyps(1) atLeastLessThan_empty_iff2 finite_lessThan
          gr0_conv_Suc lessThan_atLeast0 mset_set_empty_iff order_less_le_trans)
    also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪A k⟫⇩n⇩d 0 ⟦E⟧
                    ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate k 0) (map A [0..<k])). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ›
      by (simp only: Suc.hyps(2))
    also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate (Suc k) 0) (map A [0..<Suc k])). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ›
      by (simp flip: replicate_append_same, subst MultiSync_add)
        (use Suc.hyps(1) in auto)
    finally show ?case .
  qed (simp_all add: atLeastLessThanSuc Sync_commute)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ map A [0..<n]⟫⟫⇩n⇩d (replicate n 0)›
    by (rule P⇩S⇩K⇩I⇩P⇩S_nd_compactification_Sync)
      (auto simp add: that(1, 2))
  finally show ?thesis .
qed

lemma P_nd_compactification_Sync_upt_version:
  ‹❙⟦E❙⟧ P ∈# mset (map Q [0..<n]). P = P⟪⟪⇩n⇩d⨂⟦E⟧ map A [0..<n]⟫⟫⇩n⇩d (replicate n 0)›
  if ‹⋀i. i < n ⟹ P⟪A i⟫⇩n⇩d 0 = Q i›
proof -
  have ‹❙⟦E❙⟧ P ∈# mset (map Q [0..<n]). P = ❙⟦E❙⟧ i ∈# (mset_set {0..<n}). Q i›
    by (auto intro: mono_MultiSync_eq2)
  also have ‹… = ❙⟦E❙⟧ i ∈# (mset_set {0..<n}). P⟪A i⟫⇩n⇩d 0›
    by (auto simp add: that(1) intro: mono_MultiSync_eq)
  also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate n 0) (map A [0..<n])). P⟪A⟫⇩n⇩d σ›
  proof (induct n rule: nat_induct_012)
    case (Suc k)
    have ‹❙⟦E❙⟧ i∈#mset_set {0..<Suc k}. P⟪A i⟫⇩n⇩d 0 =
          P⟪A k⟫⇩n⇩d 0 ⟦E⟧ ❙⟦E❙⟧ i∈#mset_set {0..<k}. P⟪A i⟫⇩n⇩d 0›
      by (subst atLeastLessThanSuc, simp, rule MultiSync_add)
        (metis Suc.hyps(1) atLeastLessThan_empty_iff2 finite_lessThan
          gr0_conv_Suc lessThan_atLeast0 mset_set_empty_iff order_less_le_trans)
    also have ‹… = P⟪A k⟫⇩n⇩d 0 ⟦E⟧ ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate k 0) (map A [0..<k])). P⟪A⟫⇩n⇩d σ›
      by (simp only: Suc.hyps(2))
    also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate (Suc k) 0) (map A [0..<Suc k])). P⟪A⟫⇩n⇩d σ›
      by (simp flip: replicate_append_same, subst MultiSync_add)
        (use Suc.hyps(1) in auto)
    finally show ?case .
  qed (simp_all add: atLeastLessThanSuc Sync_commute)
  also have ‹… = P⟪⟪⇩n⇩d⨂⟦E⟧ map A [0..<n]⟫⟫⇩n⇩d (replicate n 0)›
    by (auto intro: P_nd_compactification_Sync)
  finally show ?thesis .
qed

lemma P⇩S⇩K⇩I⇩P⇩S_d_compactification_Sync_upt_version:
  ‹❙⟦E❙⟧ P ∈# mset (map Q [0..<n]). P = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩d⨂⟦E⟧ map A [0..<n]⟫⟫⇩d (replicate n 0)›
  if ‹⋀i. i < n ⟹ ρ_disjoint_ε (A i)›
    ‹⋀i j. i < n ⟹ j < n ⟹ i ≠ j ⟹ indep_enabl (A i) 0 E (A j) 0›
    ‹⋀i. i < n ⟹ P⇩S⇩K⇩I⇩P⇩S⟪A i⟫⇩d 0 = Q i›
proof -
  have ‹❙⟦E❙⟧ P ∈# mset (map Q [0..<n]). P = ❙⟦E❙⟧ i ∈# (mset_set {0..<n}). Q i›
    by (auto intro: mono_MultiSync_eq2)
  also have ‹… = ❙⟦E❙⟧ i ∈# (mset_set {0..<n}). P⇩S⇩K⇩I⇩P⇩S⟪A i⟫⇩d 0›
    by (auto simp add: that(3) intro: mono_MultiSync_eq)
  also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate n 0) (map A [0..<n])). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩d σ›
  proof (induct n rule: nat_induct_012)
    case (Suc k)
    have ‹❙⟦E❙⟧ i∈#mset_set {0..<Suc k}. P⇩S⇩K⇩I⇩P⇩S⟪A i⟫⇩d 0 =
          P⇩S⇩K⇩I⇩P⇩S⟪A k⟫⇩d 0 ⟦E⟧ ❙⟦E❙⟧ i∈#mset_set {0..<k}. P⇩S⇩K⇩I⇩P⇩S⟪A i⟫⇩d 0›
      by (subst atLeastLessThanSuc, simp, rule MultiSync_add)
        (metis Suc.hyps(1) atLeastLessThan_empty_iff2 finite_lessThan
          gr0_conv_Suc lessThan_atLeast0 mset_set_empty_iff order_less_le_trans)
    also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪A k⟫⇩d 0 ⟦E⟧
                    ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate k 0) (map A [0..<k])). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩d σ›
      by (simp only: Suc.hyps(2))
    also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate (Suc k) 0) (map A [0..<Suc k])). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩d σ›
      by (simp flip: replicate_append_same, subst MultiSync_add)
        (use Suc.hyps(1) in auto)
    finally show ?case .
  qed (simp_all add: atLeastLessThanSuc Sync_commute)
  also have ‹… = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩d⨂⟦E⟧ map A [0..<n]⟫⟫⇩d (replicate n 0)›
    by (rule P⇩S⇩K⇩I⇩P⇩S_d_compactification_Sync)
      (auto simp add: that(1, 2))
  finally show ?thesis .
qed

lemma P_d_compactification_Sync_upt_version:
  ‹❙⟦E❙⟧ P ∈# mset (map Q [0..<n]). P = P⟪⟪⇩d⨂⟦E⟧ map A [0..<n]⟫⟫⇩d (replicate n 0)›
  if ‹⋀i. i < n ⟹ P⟪A i⟫⇩d 0 = Q i›
    ‹⋀i j. i < n ⟹ j < n ⟹ i ≠ j ⟹ indep_enabl (A i) 0 E (A j) 0›
proof -
  have ‹❙⟦E❙⟧ P ∈# mset (map Q [0..<n]). P = ❙⟦E❙⟧ i ∈# (mset_set {0..<n}). Q i›
    by (auto intro: mono_MultiSync_eq2)
  also have ‹… = ❙⟦E❙⟧ i ∈# (mset_set {0..<n}). P⟪A i⟫⇩d 0›
    by (auto simp add: that(1) intro: mono_MultiSync_eq)
  also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate n 0) (map A [0..<n])). P⟪A⟫⇩d σ›
  proof (induct n rule: nat_induct_012)
    case (Suc k)
    have ‹❙⟦E❙⟧ i∈#mset_set {0..<Suc k}. P⟪A i⟫⇩d 0 =
          P⟪A k⟫⇩d 0 ⟦E⟧ ❙⟦E❙⟧ i∈#mset_set {0..<k}. P⟪A i⟫⇩d 0›
      by (subst atLeastLessThanSuc, simp, rule MultiSync_add)
        (metis Suc.hyps(1) atLeastLessThan_empty_iff2 finite_lessThan
          gr0_conv_Suc lessThan_atLeast0 mset_set_empty_iff order_less_le_trans)
    also have ‹… = P⟪A k⟫⇩d 0 ⟦E⟧ ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate k 0) (map A [0..<k])). P⟪A⟫⇩d σ›
      by (simp only: Suc.hyps(2))
    also have ‹… = ❙⟦E❙⟧ (σ, A)∈#mset (zip (replicate (Suc k) 0) (map A [0..<Suc k])). P⟪A⟫⇩d σ›
      by (simp flip: replicate_append_same, subst MultiSync_add)
        (use Suc.hyps(1) in auto)
    finally show ?case .
  qed (simp_all add: atLeastLessThanSuc Sync_commute)
  also have ‹… = P⟪⟪⇩d⨂⟦E⟧ map A [0..<n]⟫⟫⇩d (replicate n 0)›
    by (rule P_d_compactification_Sync) (simp_all add: that(2))
  finally show ?thesis .
qed



section ‹More on Iterated Combine›

lemma ε_iterated_combine⇩n⇩d_Sync_general_form:
  ‹length σs = length As ⟹ ε ⟪⇩n⇩d⨂⟦E⟧ As⟫ σs =
   (if As = [] then {}
    else (⋃i < length As. ε (As ! i) (σs ! i)) - E ∪ (⋂i < length As. ε (As ! i) (σs ! i)))›
  for As :: ‹('σ, 'e, 'r) A⇩n⇩d list›
proof (subst ε_iterated_combine⇩n⇩d_Sync, assumption, induct σs As rule: induct_2_lists012)
  case Nil show ?case by simp
next
  case (single σ⇩0 A⇩0) show ?case by auto
next
  case (Cons σ⇩0 σ⇩1 σs A⇩0 A⇩1 As)
  define U and I
    where U_def : ‹U As σs ≡ ⋃i<length As. ε (As ! i) (σs ! i)›
      and I_def : ‹I As σs ≡ ⋂i<length As. ε (As ! i) (σs ! i)›
    for As :: ‹('σ, 'e, 'r) A⇩n⇩d list› and σs
  have * : ‹U (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) = ε A⇩0 σ⇩0 ∪ U (A⇩1 # As) (σ⇩1 # σs)›
    by (auto simp add: U_def nth_Cons split: nat.split_asm)
  have ** : ‹I (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) = ε A⇩0 σ⇩0 ∩ I (A⇩1 # As) (σ⇩1 # σs)›
    by (auto simp add: I_def nth_Cons split: nat.splits)
  have ‹iterated_combine⇩n⇩d_Sync_ε (A⇩0 # A⇩1 # As) E (σ⇩0 # σ⇩1 # σs) =
        combine_sets_Sync (ε A⇩0 σ⇩0) E (U (A⇩1 # As) (σ⇩1 # σs) - E ∪ (I (A⇩1 # As) (σ⇩1 # σs)))›
    by (simp add: U_def I_def Cons.hyps(3))
  also have ‹… = U (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) - E ∪ I (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs)›
    unfolding "*" "**" by (auto simp add: U_def I_def)
  finally show ?case by (simp add: U_def I_def)
qed

lemma ε_iterated_combine⇩d_Sync_general_form:
  ‹length σs = length As ⟹ ε ⟪⇩d⨂⟦E⟧ As⟫ σs =
   (if As = [] then {}
    else (⋃i < length As. ε (As ! i) (σs ! i)) - E ∪ (⋂i < length As. ε (As ! i) (σs ! i)))›
  for As :: ‹('σ, 'e, 'r) A⇩d list›
proof (subst ε_iterated_combine⇩d_Sync, assumption, induct σs As rule: induct_2_lists012)
  case Nil show ?case by simp
next
  case (single σ⇩0 A⇩0) show ?case by auto
next
  case (Cons σ⇩0 σ⇩1 σs A⇩0 A⇩1 As)
  define U and I
    where U_def : ‹U As σs ≡ ⋃i<length As. ε (As ! i) (σs ! i)›
      and I_def : ‹I As σs ≡ ⋂i<length As. ε (As ! i) (σs ! i)›
    for As :: ‹('σ, 'e, 'r) A⇩d list› and σs
  have * : ‹U (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) = ε A⇩0 σ⇩0 ∪ U (A⇩1 # As) (σ⇩1 # σs)›
    by (auto simp add: U_def nth_Cons split: nat.split_asm)
  have ** : ‹I (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) = ε A⇩0 σ⇩0 ∩ I (A⇩1 # As) (σ⇩1 # σs)›
    by (auto simp add: I_def nth_Cons split: nat.splits)
  have ‹iterated_combine⇩d_Sync_ε (A⇩0 # A⇩1 # As) E (σ⇩0 # σ⇩1 # σs) =
        combine_sets_Sync (ε A⇩0 σ⇩0) E (U (A⇩1 # As) (σ⇩1 # σs) - E ∪ (I (A⇩1 # As) (σ⇩1 # σs)))›
    by (simp add: U_def I_def Cons.hyps(3))
  also have ‹… = U (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) - E ∪ I (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs)›
    unfolding "*" "**" by (auto simp add: U_def I_def)
  finally show ?case by (simp add: U_def I_def)
qed


lemma τ_iterated_combine⇩n⇩d_Sync_general_form:
  ‹⟦length σs = length As; σs' ∈ τ ⟪⇩n⇩d⨂⟦E⟧ As⟫ σs a; i < length As⟧ ⟹
   σs' ! i ∈ insert (σs ! i) (τ (As ! i) (σs ! i) a)›
proof (induct σs As arbitrary: σs' i rule: induct_2_lists012)
  case Nil thus ?case by simp
next
  case (single σ⇩0 A⇩0)
  from single.prems show ?case by (auto simp add: behaviour_σ_σs_conv)
next
  case (Cons σ⇩0 σ⇩1 σs A⇩0 A⇩1 As)
  from ‹length σs = length As› have ‹length (σ⇩0 # σ⇩1 # σs) = length (A⇩0 # A⇩1 # As)› by simp
  from same_length_ℛ⇩n⇩d_iterated_combine⇩n⇩d_Sync_description[OF this]
  have ‹length σs' = length (A⇩0 # A⇩1 # As)›
    by (metis Cons.prems(1) ℛ⇩n⇩d.init ℛ⇩n⇩d.step)
  then obtain σ⇩0' σ⇩1' σs'' where ‹σs' = σ⇩0' # σ⇩1' # σs''› by (metis length_Suc_conv)
  with Cons.prems Cons.hyps(3)[of ‹σ⇩1' # σs''› ‹nat.pred i›] show ?case
    by (auto simp add: combine_Sync_defs nth_Cons split: if_split_asm nat.splits)
qed


lemma τ_iterated_combine⇩d_Sync_general_form:
  ‹length σs = length As ⟹
   τ ⟪⇩d⨂⟦E⟧ As⟫ σs a =
   (if As = [] then ◇ else
    if a ∈ (⋃i < length As. ε (As ! i) (σs ! i)) - E ∪ (⋂i < length As. ε (As ! i) (σs ! i))
    then ⌊map2 (λσ A. if a ∈ ε A σ then ⌈τ A σ a⌉ else σ) σs As⌋ else ◇)›
  for As :: ‹('σ, 'e, 'r) A⇩d list›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by simp
next
  case (single σ⇩0 A⇩0) show ?case by (auto simp add: behaviour_σ_σs_conv ε_simps)
next
  case (Cons σ⇩0 σ⇩1 σs A⇩0 A⇩1 As)
  let ?U = ‹λAs σs. ⋃i<length As. ε (As ! i) (σs ! i)›
  let ?I = ‹λAs σs. ⋂i<length As. ε (As ! i) (σs ! i)›
  show ?case
  proof (split if_split, split if_split, intro conjI impI)
    show ‹A⇩0 # A⇩1 # As = [] ⟹ τ ⟪⇩d⨂⟦E⟧ A⇩0 # A⇩1 # As⟫ (σ⇩0 # σ⇩1 # σs) a = ◇›
      and ‹A⇩0 # A⇩1 # As = [] ⟹ τ ⟪⇩d⨂⟦E⟧ A⇩0 # A⇩1 # As⟫ (σ⇩0 # σ⇩1 # σs) a = ◇› by simp_all
  next
    assume ‹a ∉ ?U (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) - E ∪ ?I (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs)›
    hence ‹a ∉ ε ⟪⇩d⨂⟦E⟧ A⇩0 # A⇩1 # As⟫ (σ⇩0 # σ⇩1 # σs)›
      by (subst ε_iterated_combine⇩d_Sync_general_form)
        (simp_all add: Cons.hyps(1))
    thus ‹τ ⟪⇩d⨂⟦E⟧ A⇩0 # A⇩1 # As⟫ (σ⇩0 # σ⇩1 # σs) a = ◇›
      by (simp add: ε_simps)
  next
    assume * : ‹a ∈ ?U (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) - E ∪ ?I (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs)›
    have ** : ‹?U (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) = ε A⇩0 σ⇩0 ∪ ?U (A⇩1 # As) (σ⇩1 # σs)›
      by (auto simp add: nth_Cons split: nat.split_asm)
    have *** : ‹?I (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) = ε A⇩0 σ⇩0 ∩ ?I (A⇩1 # As) (σ⇩1 # σs)›
      by (auto simp add: nth_Cons split: nat.splits)
    have **** : ‹?U (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) - E ∪ ?I (A⇩0 # A⇩1 # As) (σ⇩0 # σ⇩1 # σs) =
                 combine_sets_Sync (ε A⇩0 σ⇩0) E (?U (A⇩1 # As) (σ⇩1 # σs) - E ∪ ?I (A⇩1 # As) (σ⇩1 # σs))›
      unfolding "**" "***" by auto
    have $ : ‹?U (A⇩1 # As) (σ⇩1 # σs) - E ∪ ?I (A⇩1 # As) (σ⇩1 # σs) = ε ⟪⇩d⨂⟦E⟧ A⇩1 # As⟫ (σ⇩1 # σs)›
      by (subst ε_iterated_combine⇩d_Sync_general_form)
        (simp_all add: Cons.hyps(1))

    from Cons.hyps(1) have ‹a ∉ ?U As σs ⟹
            map2 (λσ A. if a ∈ ε A σ then ⌈τ A σ a⌉ else σ) σs As = σs›
      by (induct σs As rule: induct_2_lists012)
        (auto simp add: ε_simps lessThan_def, fastforce)
    moreover have ‹?U As σs ⊆ ?U (A⇩1 # As) (σ⇩1 # σs)› by force
    ultimately show ‹τ ⟪⇩d⨂⟦E⟧ A⇩0 # A⇩1 # As⟫ (σ⇩0 # σ⇩1 # σs) a =
                  ⌊map2 (λx y. if a ∈ ε y x then ⌈τ y x a⌉ else x) (σ⇩0 # σ⇩1 # σs) (A⇩0 # A⇩1 # As)⌋›
      using "*" unfolding "****" "$"
      by (simp add: ε_combine⇩R⇩l⇩i⇩s⇩t_Sync combine_Sync_ε_def, safe,
          auto simp add: combine⇩R⇩l⇩i⇩s⇩t_Sync_defs ε_simps Cons.hyps(3) lessThan_def subset_iff
          split: option.splits if_splits)
        (metis (no_types, lifting) not_less_eq nth_Cons_Suc)
  qed
qed


lemma indep_implies_only_one_enabled':
  ‹∃!i. i < length As ∧ a ∈ ε (As ! i) (σs ! i)›
  if ‹length σs = length As›
    and ‹⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
            ε (As ! i) (σs ! i) ∩ ε (As ! j) (σs ! j) ⊆ E›
    and ‹a ∈ (⋃i<length As. ε (As ! i) (σs ! i)) - E›
proof (rule ex_ex1I)
  from that(3) show ‹∃i<length As. a ∈ ε (As ! i) (σs ! i)› by auto
next
  fix i j assume ‹i < length As ∧ a ∈ ε (As ! i) (σs ! i)›
    ‹j < length As ∧ a ∈ ε (As ! j) (σs ! j)›
  moreover from that(3) have ‹a ∉ E› by blast
  ultimately show ‹i = j› using that(2)[of i j] by auto
qed

lemma indep_implies_only_one_enabled:
  ‹⟦length σs = length As;
    ⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
           indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j);
    a ∈ (⋃i<length As. ε (As ! i) (σs ! i)) - E⟧ ⟹
    ∃!i. i < length As ∧ a ∈ ε (As ! i) (σs ! i)›
  by (erule indep_implies_only_one_enabled'[where E = E])
    (simp_all add: indep_enabl_def subset_iff, meson IntI ℛ⇩d.init)


lemma τ_iterated_combine⇩d_Sync_general_form_when_indep:
  ‹τ ⟪⇩d⨂⟦E⟧ As⟫ σs a =
   (if As = [] then ◇
    else   if a ∈ (⋂i<length As. ε (As ! i) (σs ! i))
         then ⌊map2 (λσ A. ⌈τ A σ a⌉) σs As⌋
         else   if a ∈ (⋃i<length As. ε (As ! i) (σs ! i)) - E
              then let i = THE i. i < length As ∧  a ∈ ε (As ! i) (σs ! i)
                    in ⌊σs[i := ⌈τ (As ! i) (σs ! i) a⌉]⌋
              else ◇)›
  (is ‹_ = (if As = [] then ◇ else 
            if a ∈ ?I As σs then ⌊map2 (λσ A. ⌈τ A σ a⌉) σs As⌋ else
            if a ∈ ?U As σs - E then ?upd As σs else ◇)›)
    if ‹length σs = length As›
      ‹⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
            indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)›
proof (subst τ_iterated_combine⇩d_Sync_general_form[OF that(1)], rule if_cong)
  show ‹(if a ∈ ?U As σs - E ∪ ?I As σs
         then ⌊map2 (λx y. if a ∈ ε y x then ⌈τ y x a⌉ else x) σs As⌋ else ◇) =
        (if a ∈ ?I As σs then ⌊map2 (λx y. ⌈τ y x a⌉) σs As⌋ else
         if a ∈ ?U As σs - E then ?upd As σs else ◇)›
  proof (split if_split, intro conjI impI)
    assume * : ‹a ∈ ?I As σs›
    with that(1) have ‹(σ, A) ∈ set (zip σs As) ⟹ a ∈ ε A σ› for σ A
      by (induct σs As rule: list_induct2) (use lessThan_Suc_eq_insert_0 in auto)
    with "*" show ‹(if a ∈ ?U As σs - E ∪ ?I As σs
                    then ⌊map2 (λx y. if a ∈ ε y x then ⌈τ y x a⌉ else x) σs As⌋ else ◇) =
                   ⌊map2 (λx y. ⌈τ y x a⌉) σs As⌋› by auto
  next
    assume * : ‹a ∉ ?I As σs›
    show ‹(if a ∈ ?U As σs - E ∪ ?I As σs
           then ⌊map2 (λx y. if a ∈ ε y x then ⌈τ y x a⌉ else x) σs As⌋ else ◇) =
          (if a ∈ ?U As σs - E then ?upd As σs else ◇)›
    proof (rule if_cong)
      assume ‹a ∈ ?U As σs - E›
      from indep_implies_only_one_enabled[OF that this]
      obtain i where $ : ‹i < length As›  ‹a ∈ ε (As ! i) (σs ! i)›
        ‹j < length As ⟹ j ≠ i ⟹ a ∉ ε (As ! j) (σs ! j)› for j by blast
      have $$ : ‹(THE i. i < length As ∧ a ∈ ε (As ! i) (σs ! i)) = i›
        using "$" by blast
      have ‹⌊map2 (λx y. if a ∈ ε y x then ⌈τ y x a⌉ else x) σs As⌋ =
            ⌊σs[i := ⌈τ (As ! i) (σs ! i) a⌉]⌋›
        by (auto intro!: nth_equalityI simp add: that(1))
          (use that(1) "$"(3) in fastforce, metis "$"(2) nth_list_update_neq)
      also have ‹… = ?upd As σs›
        using "$$" by auto
      finally show ‹⌊map2 (λx y. if a ∈ ε y x then ⌈τ y x a⌉ else x) σs As⌋ = ?upd As σs› .
    qed (use "*" in auto)
  qed
qed simp_all



section ‹More on Events›

lemma events_of_MultiSync_P⇩S⇩K⇩I⇩P⇩S_nd : 
  ‹α(❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ) =
   (if As = [] then {} else
    ⋃ σs' ∈ ℛ⇩n⇩d ⟪⇩n⇩d⨂⟦E⟧ As⟫ σs. (⋃i<length As. ε (As ! i) (σs' ! i)) - E ∪
                                 (⋂i<length As. ε (As ! i) (σs' ! i)))›
  (is ‹_ = ?rhs›) if ‹length σs = length As›
  ‹⋀A. A ∈ set As ⟹ ρ_disjoint_ε A› ‹⋀A. A ∈ set As ⟹ at_most_1_elem_term A›
proof -
  have ‹❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩n⇩d σ = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩n⇩d⨂⟦E⟧ As⟫⟫⇩n⇩d σs›
    by (simp only: P⇩S⇩K⇩I⇩P⇩S_nd_compactification_Sync[OF that])
  also have ‹α(…) = ⋃ (ε ⟪⇩n⇩d⨂⟦E⟧ As⟫ ` ℛ⇩n⇩d ⟪⇩n⇩d⨂⟦E⟧ As⟫ σs)› 
  proof (rule events_of_P⇩S⇩K⇩I⇩P⇩S_nd)
    show ‹ρ_disjoint_ε ⟪⇩n⇩d⨂⟦E⟧ As⟫›
      by (simp only: ρ_disjoint_ε_transmission_to_iterated_combine⇩n⇩d_Sync that(2))
  qed
  also from same_length_ℛ⇩n⇩d_iterated_combine⇩n⇩d_Sync_description[OF that(1)]
  have ‹… = ?rhs› by (auto simp add: ε_iterated_combine⇩n⇩d_Sync_general_form)
  finally show ?thesis .
qed


lemma events_of_MultiSync_P_nd : 
  ‹α(❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⟪A⟫⇩n⇩d σ) =
   (if As = [] then {} else
    ⋃ σs' ∈ ℛ⇩n⇩d ⟪⇩n⇩d⨂⟦E⟧ As⟫ σs. (⋃i<length As. ε (As ! i) (σs' ! i)) - E ∪
                                 (⋂i<length As. ε (As ! i) (σs' ! i)))›
  (is ‹_ = ?rhs›) if ‹length σs = length As›
proof -
  have ‹❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⟪A⟫⇩n⇩d σ = P⟪⟪⇩n⇩d⨂⟦E⟧ As⟫⟫⇩n⇩d σs›
    by (fact P_nd_compactification_Sync[OF that])
  also have ‹α(…) = ⋃ (ε ⟪⇩n⇩d⨂⟦E⟧ As⟫ ` ℛ⇩n⇩d ⟪⇩n⇩d⨂⟦E⟧ As⟫ σs)› by (fact events_of_P_nd)
  also from same_length_ℛ⇩n⇩d_iterated_combine⇩n⇩d_Sync_description[OF that(1)]
  have ‹… = ?rhs› by (auto simp add: ε_iterated_combine⇩n⇩d_Sync_general_form)
  finally show ?thesis .
qed



lemma events_of_MultiSync_P⇩S⇩K⇩I⇩P⇩S_d : 
  ‹α(❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩d σ) =
   (if As = [] then {} else
    ⋃ σs' ∈ ℛ⇩d ⟪⇩d⨂⟦E⟧ As⟫ σs. (⋃i<length As. ε (As ! i) (σs' ! i) - E ∪
                               (⋂i<length As. ε (As ! i) (σs' ! i))))›
  (is ‹_ = ?rhs›) if ‹length σs = length As› ‹⋀A. A ∈ set As ⟹ ρ_disjoint_ε A›
  ‹⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
          indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)›
proof -
  have ‹❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⇩S⇩K⇩I⇩P⇩S⟪A⟫⇩d σ = P⇩S⇩K⇩I⇩P⇩S⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs›
    by (simp add: P⇩S⇩K⇩I⇩P⇩S_d_compactification_Sync[OF that])
  also have ‹α(…) = ⋃ (ε ⟪⇩d⨂⟦E⟧ As⟫ ` ℛ⇩d ⟪⇩d⨂⟦E⟧ As⟫ σs)› 
  proof (rule events_of_P⇩S⇩K⇩I⇩P⇩S_d)
    show ‹ρ_disjoint_ε ⟪⇩d⨂⟦E⟧ As⟫›
      by (simp only: ρ_disjoint_ε_transmission_to_iterated_combine⇩d_Sync that(2))
  qed
  also from same_length_ℛ⇩d_iterated_combine⇩d_Sync_description[OF that(1)]
  have ‹… = ?rhs› by (auto simp add: ε_iterated_combine⇩d_Sync_general_form)
  finally show ?thesis .
qed


lemma events_of_MultiSync_P_d : 
  ‹α(❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⟪A⟫⇩d σ) =
   (if As = [] then {} else
    ⋃ σs' ∈ ℛ⇩d ⟪⇩d⨂⟦E⟧ As⟫ σs. (⋃i<length As. ε (As ! i) (σs' ! i) - E ∪
                                (⋂i<length As. ε (As ! i) (σs' ! i))))›
  (is ‹_ = ?rhs›) if ‹length σs = length As›
  and ‹⋀i j. ⟦i < length As; j < length As; i ≠ j⟧ ⟹
             indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)›
proof -
  have ‹❙⟦E❙⟧ (σ, A) ∈# mset (zip σs As). P⟪A⟫⇩d σ = P⟪⟪⇩d⨂⟦E⟧ As⟫⟫⇩d σs›
    by (simp add: P_d_compactification_Sync[OF that])
  also have ‹α(…) = ⋃ (ε ⟪⇩d⨂⟦E⟧ As⟫ ` ℛ⇩d ⟪⇩d⨂⟦E⟧ As⟫ σs)› by (fact events_of_P_d)
  also from same_length_ℛ⇩d_iterated_combine⇩d_Sync_description[OF that(1)]
  have ‹… = ?rhs› by (auto simp add: ε_iterated_combine⇩d_Sync_general_form)
  finally show ?thesis .
qed



(*<*)
end
  (*>*)