Theory Compactification_Synchronization_Product_Generalized

(***********************************************************************************
 * 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 Generalized›

(*<*)
theory Compactification_Synchronization_Product_Generalized
  imports Compactification_Synchronization_Product
    Combining_Synchronization_Product_Generalized
begin
  (*>*)


section ‹Iterated Combine›

subsection ‹Definitions›

fun iterated_combined_Syncptick :: ‹'e set ⇒ ('σ, 'e, 'r) Ad list ⇒ ('σ list, 'e, 'r list) Ad› (‹⟪d⨂⟦_⟧✓ _⟫› [0, 0])
  where ‹⟪d⨂⟦E⟧✓ []⟫ = ⦇τ = λσs a. ◇, ω = λσs. ◇⦈›
  |     ‹⟪d⨂⟦E⟧✓ [A0]⟫ = d⟪A0⟫singl↪list›
  |     ‹⟪d⨂⟦E⟧✓ A0 # A1 # As⟫ = ⟪A0 d⊗⟦E⟧✓Rlist ⟪d⨂⟦E⟧✓ A1 # As⟫⟫›

fun iterated_combinend_Syncptick :: ‹'e set ⇒ ('σ, 'e, 'r) And list ⇒ ('σ list, 'e, 'r list) And› (‹⟪nd⨂⟦_⟧✓ _⟫› [0, 0])
  where ‹⟪nd⨂⟦E⟧✓ []⟫ = ⦇τ = λσs a. {}, ω = λσs. {}⦈›
  |     ‹⟪nd⨂⟦E⟧✓ [A0]⟫ = nd⟪A0⟫singl↪list›
  |     ‹⟪nd⨂⟦E⟧✓ A0 # A1 # As⟫ = ⟪A0 nd⊗⟦E⟧✓Rlist ⟪nd⨂⟦E⟧✓ A1 # As⟫⟫›


lemma iterated_combined_Syncptick_simps_bis: ‹As ≠ [] ⟹ ⟪d⨂⟦E⟧✓ A0 # As⟫ = ⟪A0 d⊗⟦E⟧✓Rlist ⟪d⨂⟦E⟧✓ As⟫⟫›
  and iterated_combinend_Syncptick_simps_bis: ‹Bs ≠ [] ⟹ ⟪nd⨂⟦E⟧✓ B0 # Bs⟫ = ⟪B0 nd⊗⟦E⟧✓Rlist ⟪nd⨂⟦E⟧✓ Bs⟫⟫›
  by (induct As, simp_all) (induct Bs, simp_all)



subsection ‹First Results›

lemma τ_iterated_combine_Syncptick:
  ‹τ ⟪d⨂⟦E⟧✓ As⟫ = τ ⟪d⨂⟦E⟧ As⟫› ‹τ ⟪nd⨂⟦E⟧✓ Bs⟫ = τ ⟪nd⨂⟦E⟧ Bs⟫›
  by (intro ext, induct rule: induct_list012;
      simp add: σ_σs_conv_defs singl_list_conv_defs
      combineRlist_Sync_defs combineRlist_Syncptick_defs ε_simps)+

corollary ε_iterated_combine_Syncptick:
  ‹ε ⟪d⨂⟦E⟧✓ As⟫ σs = ε ⟪d⨂⟦E⟧ As⟫ σs›
  ‹ε ⟪nd⨂⟦E⟧✓ Bs⟫ σs = ε ⟪nd⨂⟦E⟧ Bs⟫ σs›
  by (simp_all add: ε_simps τ_iterated_combine_Syncptick)

corollary ℛ_iterated_combine_Syncptick:
  ‹ℛd ⟪d⨂⟦E⟧✓ As⟫ = ℛd ⟪d⨂⟦E⟧ As⟫› ‹ℛnd ⟪nd⨂⟦E⟧✓ Bs⟫ = ℛnd ⟪nd⨂⟦E⟧ Bs⟫›
  by (intro ext same_τ_implies_same_ℛd same_τ_implies_same_ℛnd,
      simp add: τ_iterated_combine_Syncptick)+


lemma combineListslenL_Syncptick_combineRlist_Syncptick_eq:
  ‹ε ⟪d⟪A0⟫singl↪list d⊗⟦1, E⟧✓ListslenL A1⟫ σs = ε ⟪A0 d⊗⟦E⟧✓Rlist A1⟫ σs›
  ‹τ ⟪d⟪A0⟫singl↪list d⊗⟦1, E⟧✓ListslenL A1⟫ (s0 # σs) e = τ ⟪A0 d⊗⟦E⟧✓Rlist A1⟫ (s0 # σs) e›
  ‹ε ⟪nd⟪B0⟫singl↪list nd⊗⟦1, E⟧✓ListslenL B1⟫ σs = ε ⟪B0 nd⊗⟦E⟧✓Rlist B1⟫ σs›
  ‹τ ⟪nd⟪B0⟫singl↪list nd⊗⟦1, E⟧✓ListslenL B1⟫ (s0 # σs) e = τ ⟪B0 nd⊗⟦E⟧✓Rlist B1⟫ (s0 # σs) e›
  by (simp_all add: ε_combineListslenL_Syncptick ε_combineRlist_Syncptick drop_Suc combine_Sync_ε_def,
      auto simp add: combineListslenL_Syncptick_defs combineRlist_Syncptick_defs singl_list_conv_defs ε_simps) 
    (metis append_Cons append_Nil)



lemma combinePairlist_Syncptick_and_iterated_combinend_Syncptick_eq:
  ‹ε ⟪A0 d⊗⟦E⟧✓Pairlist A1⟫ [s0, s1] = ε ⟪d⨂⟦E⟧✓ [A0, A1]⟫ [s0, s1]›
  ‹τ ⟪A0 d⊗⟦E⟧✓Pairlist A1⟫ [s0, s1] e = τ ⟪d⨂⟦E⟧✓ [A0, A1]⟫ [s0, s1] e›
  ‹ε ⟪B0 nd⊗⟦E⟧✓Pairlist B1⟫ [s0, s1] = ε ⟪nd⨂⟦E⟧✓ [B0, B1]⟫ [s0, s1]›
  ‹τ ⟪B0 nd⊗⟦E⟧✓Pairlist B1⟫ [s0, s1] e = τ ⟪nd⨂⟦E⟧✓ [B0, B1]⟫ [s0, s1] e›
  by (simp_all add: ε_combinePairlist_Syncptick ε_combineRlist_Syncptick)
    (auto simp add: combinePairlist_Syncptick_defs combineRlist_Syncptick_defs singl_list_conv_defs 
      option.case_eq_if ε_simps combine_Sync_ε_def)



lemmas combinePairlist_Syncptick_and_combineRlist_Syncptick_eq =
  combinePairlist_Syncptick_and_iterated_combinend_Syncptick_eq[simplified]



subsection ‹Transmission of Properties›

lemma finite_trans_transmission_to_iterated_combinend_Syncptick:
  ‹(⋀A. A ∈ set As ⟹ finite_trans A) ⟹ finite_trans ⟪nd⨂⟦E⟧✓ As⟫›
  by (induct As rule: induct_list012) 
    (auto simp add: singl_list_conv_defs combineRlist_Syncptick_defs finite_trans_def finite_image_set2)

lemma ρ_disjoint_ε_transmission_to_iterated_combined_Syncptick:
  ‹(⋀A. A ∈ set As ⟹ ρ_disjoint_ε A) ⟹ ρ_disjoint_ε ⟪d⨂⟦E⟧✓ As⟫›
  by (induct As rule: induct_list012)
    (simp_all add: ρ_combineRlist_Syncptick ε_combineRlist_Syncptick ρ_disjoint_ε_def combine_Sync_ε_def)

lemma ρ_disjoint_ε_transmission_to_iterated_combinend_Syncptick:
  ‹∀B ∈ set Bs. ρ_disjoint_ε B ⟹ ρ_disjoint_ε ⟪nd⨂⟦E⟧✓ Bs⟫›
  by (induct Bs rule: induct_list012)
    (simp_all add: ρ_combineRlist_Syncptick ε_combineRlist_Syncptick ρ_disjoint_ε_def combine_Sync_ε_def)


lemma same_length_indep_transmission_to_iterated_combined_Syncptick:
  ‹indep_enabl A0 s0 E ⟪d⨂⟦E⟧✓ As⟫ σs›
  if ‹length σs = length As›
    ‹⋀i j. ⟦i ≤ length As; j ≤ length As; i ≠ j⟧ ⟹ 
            indep_enabl ((A0 # As) ! i) ((s0 # σs) ! i) E ((A0 # As) ! j) ((s0 # σs) ! j)›
  using same_length_indep_transmission_to_iterated_combined_Sync[OF that]
  by (simp add: indep_enabl_def ε_iterated_combine_Syncptick
      τ_iterated_combine_Syncptick ℛ_iterated_combine_Syncptick that(1))


lemma ω_iterated_combined_Syncptick :
  ‹length σs = length As ⟹
   ω ⟪d⨂⟦E⟧✓ As⟫ σs = (if As = [] then ◇ else those (map2 ω As σs))›
  by (induct σs As rule: induct_2_lists012)
    (simp_all add: singl_list_conv_defs combineRlist_Syncptick_defs split: option.split)


lemma ω_iterated_combinend_Syncptick :
  ‹length σs = length As ⟹
   ω ⟪nd⨂⟦E⟧✓ As⟫ σs =
   (if As = [] then {} else {rs. length rs = length As ∧ (∀i < length As. rs ! i ∈ ω (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: singl_list_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 rs assume ‹rs ∈ ω ⟪nd⨂⟦E⟧✓ A1 # A2 # As⟫ (σ1 # σ2 # σs)›
    then obtain r1 rs' where ‹rs = r1 # rs'› ‹r1 ∈ ω A1 σ1›
      ‹rs' ∈ ω ⟪nd⨂⟦E⟧✓ A2 # As⟫ (σ2 # σs)›
      by (auto simp add: combineRlist_Syncptick_defs)
    from this(3) Cons.hyps(3) obtain r2 rs''
      where ‹rs' = r2 # rs''› ‹length rs'' = length As›
        ‹∀i<Suc (length As). (r2 # rs'') ! i ∈ ω ((A2 # As) ! i) ((σ2 # σs) ! i)›
      by simp (metis (no_types, lifting) length_Suc_conv)
    with ‹r1 ∈ ω A1 σ1› show ‹rs ∈ ?rhs σ1 σ2 σs A1 A2 As›
      by (auto simp add: ‹rs = r1 # rs'› less_Suc_eq_0_disj)
  next
    from Cons.hyps(3)
    show ‹rs ∈ ?rhs σ1 σ2 σs A1 A2 As ⟹
          rs ∈ ω ⟪nd⨂⟦E⟧✓ A1 # A2 # As⟫ (σ1 # σ2 # σs)› for rs
      by (cases rs; cases ‹tl rs›, simp_all add: combineRlist_Syncptick_defs) auto
  qed
qed


subsection ‹Normalization›

lemma ω_iterated_combinend_Syncptick_det_ndet_conv:
  ‹length σs = length As ⟹
   ω ⟪nd⨂⟦E⟧✓ map (λA. ⟪A⟫d↪nd) As⟫ σs = ω ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σ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_singl_list_conv_commute)
next
  case (Cons σ1 σ2 σs A1 A2 As)
  thus ?case
    by (auto simp add: det_ndet_conv_defs combineRlist_Syncptick_defs split: option.split)
qed

lemma τ_iterated_combinend_Syncptick_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↪nd σs e = τ ⟪nd⨂⟦E⟧✓ map (λA. ⟪A⟫d↪nd) 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_singl_list_conv_commute(1))
next
  case (Cons σ1 σ2 σs A1 A2 As)
  have * : ‹τ ⟪⟪d⨂⟦E⟧✓ A2 # As⟫⟫d↪nd (σ2 # σs) e =
            τ ⟪nd⨂⟦E⟧✓ map (λA. ⟪A⟫d↪nd) (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↪nd (σ1 # σ2 # σs) e =
        τ ⟪⟪A1⟫d↪nd nd⊗⟦E⟧✓Rlist ⟪⟪d⨂⟦E⟧✓ A2 # As⟫⟫d↪nd⟫ (σ1 # σ2 # σs) e›
  proof (subst iterated_combined_Syncptick.simps(3), rule τ_combineRlist_Syncptick_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_combined_Syncptick)
    qed
  qed
  also have ‹… = τ ⟪nd⨂⟦E⟧✓ map (λA. ⟪A⟫d↪nd) (A1 # A2 # As)⟫ (σ1 # σ2 # σs) e›
    by (use "*" in ‹simp add: combineRlist_Syncptick_defs ε_simps›)
      (metis empty_from_det_to_ndet_is_None_trans option.exhaust)
  finally show ?case .
qed



lemma PSKIPS_iterated_combinend_Syncptick_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 ‹PSKIPS⟪⟪d⨂⟦E⟧✓ As⟫⟫d σs = PSKIPS⟪⟪nd⨂⟦E⟧✓ map (λA. ⟪A⟫d↪nd) As⟫⟫nd σs›
proof (fold PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d, rule PSKIPS_nd_eqI_strong_id)
  show ‹σs' ∈ ℛnd ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs ⟹
        τ ⟪nd⨂⟦E⟧✓ map (λA. ⟪A⟫d↪nd) As⟫ σs' e = τ ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs' e› for σs' e
  proof (rule τ_iterated_combinend_Syncptick_behaviour_when_indep[symmetric])
    show ‹σs' ∈ ℛnd ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs ⟹ length σs' = length As›
      by (metis ℛnd_from_det_to_ndet ℛ_iterated_combine_Syncptick(1) same_length
          same_length_ℛd_iterated_combined_Sync_description)
  next
    show ‹⟦σs' ∈ ℛnd ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs; i < length As; j < length As; i ≠ j⟧
          ⟹ indep_enabl (As ! i) (σs' ! i) E (As ! j) (σs' ! j)› for i j
      by (unfold ℛnd_from_det_to_ndet ℛ_iterated_combine_Syncptick,
          drule same_length_ℛd_iterated_combined_Sync_description[OF same_length])
        (meson ℛd_trans indep_enabl_def indep)
  qed
next
  show ‹σs' ∈ ℛnd ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs ⟹
        ω ⟪nd⨂⟦E⟧✓ map (λA. ⟪A⟫d↪nd) As⟫ σs' = ω ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs'› for σs'
    by (metis ℛnd_from_det_to_ndet ℛ_iterated_combine_Syncptick(1)
        ω_iterated_combinend_Syncptick_det_ndet_conv same_length
        same_length_ℛd_iterated_combined_Sync_description)
qed


lemma P_d_iterated_combinend_Syncptick_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⟪⟪nd⨂⟦E⟧✓ map (λA. ⟪A⟫d↪nd) As⟫⟫nd σs›
proof (fold P_nd_from_det_to_ndet_is_P_d, rule P_nd_eqI_strong_id)
  show ‹σs' ∈ ℛnd ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs ⟹
        τ ⟪nd⨂⟦E⟧✓ map (λA. ⟪A⟫d↪nd) As⟫ σs' e = τ ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs' e› for σs' e
  proof (rule τ_iterated_combinend_Syncptick_behaviour_when_indep[symmetric])
    show ‹σs' ∈ ℛnd ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs ⟹ length σs' = length As›
      by (metis ℛnd_from_det_to_ndet ℛ_iterated_combine_Syncptick(1) same_length
          same_length_ℛd_iterated_combined_Sync_description)
  next
    show ‹⟦σs' ∈ ℛnd ⟪⟪d⨂⟦E⟧✓ As⟫⟫d↪nd σs; i < length As; j < length As; i ≠ j⟧
          ⟹ indep_enabl (As ! i) (σs' ! i) E (As ! j) (σs' ! j)› for i j
      by (unfold ℛnd_from_det_to_ndet ℛ_iterated_combine_Syncptick,
          drule same_length_ℛd_iterated_combined_Sync_description[OF same_length])
        (meson ℛd_trans indep_enabl_def indep)
  qed
qed



section ‹Compactification Theorems›

subsection ‹Binary›

subsubsection ‹Pair›

theorem PSKIPS_nd_combinePair_Syncptick :
  fixes E :: ‹'a set›
  assumes ρ_disjoint_ε : ‹ρ_disjoint_ε A0› ‹ρ_disjoint_ε A1›
  defines A_def: ‹A ≡ ⟪A0 nd⊗⟦E⟧✓Pair A1⟫›      
  defines P_def: ‹P ≡ PSKIPS⟪A0⟫nd› and Q_def: ‹Q ≡ PSKIPS⟪A1⟫nd› and S_def: ‹S ≡ PSKIPS⟪A⟫nd›
  shows ‹P σ0 ⟦E⟧✓Pair Q σ1 = S (σ0, σ1)›
proof -
  let ?f = ‹PSKIPS_nd_step (ε A) (τ A) (ω A) (λσ'. case σ' of (σ0, σ1) ⇒ P σ0 ⟦E⟧✓Pair Q σ1)›
  note cartprod_rwrt = GlobalNdet_cartprod[of _ _ ‹λx y. _ (x, y)›, simplified]
  note Ndet_and_SyncPair = SyncPair.Syncptick_distrib_GlobalNdet_left
    SyncPair.Syncptick_distrib_GlobalNdet_right
  note Mprefix_SyncPair_constant =
    SyncPair.SKIP_Syncptick_Mprefix SyncPair.Mprefix_Syncptick_SKIP
    SyncPair.STOP_Syncptick_Mprefix SyncPair.Mprefix_Syncptick_STOP
  note P_rec = restriction_fix_eq[OF PSKIPS_nd_step_constructive_bis[of A0], folded PSKIPS_nd_def P_def, THEN fun_cong]
  note Q_rec = restriction_fix_eq[OF PSKIPS_nd_step_constructive_bis[of A1], folded PSKIPS_nd_def Q_def, THEN fun_cong]
  have ω_A : ‹ω A (σ0', σ1') = ω A0 σ0' × ω A1 σ1'› for σ0' σ1'
    by (auto simp add: A_def combinePair_Syncptick_defs)
  have ε_A : ‹ε A (σ0', σ1') = combine_sets_Sync (ε A0 σ0') E (ε A1 σ1')› for σ0' σ1'
    by (simp add: A_def ε_combinePair_Syncptick combine_Sync_ε_def)
  show ‹P σ0 ⟦E⟧✓Pair Q σ1 = S (σ0, σ1)›
  proof (rule fun_cong[of ‹λ(σ0, σ1). P σ0 ⟦E⟧✓Pair Q σ1› _ ‹(σ0, σ1)›, simplified])
    show ‹(λ(σ0, σ1). P σ0 ⟦E⟧✓Pair Q σ1) = S›
    proof (rule restriction_fix_unique[OF PSKIPS_nd_step_constructive_bis[of A],
          symmetric, folded PSKIPS_nd_def S_def])
      show ‹?f = (λ(σ0, σ1). P σ0 ⟦E⟧✓Pair Q σ1)›
      proof (rule ext, clarify)
        have ρ_disjoint_ε_bis : ‹ω A0 σ0 ≠ {} ⟹ ε A0 σ0 = {}›
          ‹ω A1 σ1 ≠ {} ⟹ ε A1 σ1 = {}› for σ0 σ1
          by (simp_all add: ρ_simps ρ_disjoint_εD ρ_disjoint_ε)
        show ‹?f (σ0, σ1) = P σ0 ⟦E⟧✓Pair Q σ1› for σ0 σ1
        proof (cases ‹ω A0 σ0 = {}›; cases ‹ω A1 σ1 = {}›)
          assume ‹ω A0 σ0 = {}› ‹ω A1 σ1 = {}›
          hence P_rec' : ‹P σ0 = P_nd_step (ε A0) (τ A0) P σ0›
            and Q_rec' : ‹Q σ1 = P_nd_step (ε A1) (τ A1) Q σ1›
            and S_rec' : ‹PSKIPS_nd_step (ε A) (τ A) (ω A) (λ(σ0, σ1). P σ0 ⟦E⟧✓Pair Q σ1) (σ0, σ1) =
                        P_nd_step (ε A) (τ A) (λ(σ0, σ1). P σ0 ⟦E⟧✓Pair Q σ1) (σ0, σ1)›
            by (simp_all add: P_rec[of σ0] Q_rec[of σ1] ω_A)
          show ‹?f (σ0, σ1) = P σ0 ⟦E⟧✓Pair Q σ1›
            unfolding P_rec' Q_rec' S_rec' SyncPair.Mprefix_Syncptick_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_SyncPair cartprod_rwrt
                combinePair_Syncptick_defs ε_simps GlobalNdet_sets_commute[of ‹τ A1 _ _›]
                simp flip: GlobalNdet_factorization_union
                intro!: mono_GlobalNdet_eq arg_cong2[where f = ‹(⊓)›])
        next
          assume ‹ω A0 σ0 ≠ {}› ‹ω A1 σ1 = {}›
          from ρ_disjoint_ε(1) ‹ω A0 σ0 ≠ {}› have ‹ε A0 σ0 = {}›
            by (simp add: ρ_disjoint_ε_def ρ_simps)
          have ‹?f (σ0, σ1) = □b∈(ε A1 σ1 - E) → (⊓σ1'∈τ A1 σ1 b. (SKIPS (ω A0 σ0) ⟦E⟧✓Pair Q σ1'))›
            by (auto simp add: ω_A ε_A ‹ω A1 σ1 = {}› ‹ε A0 σ0 = {}› intro!: mono_Mprefix_eq,
                auto simp add: A_def combinePair_Syncptick_defs ‹ω A0 σ0 ≠ {}›
                ‹ε A0 σ0 = {}› cartprod_rwrt P_rec[of σ0] intro!: mono_GlobalNdet_eq)
          also have ‹… = P σ0 ⟦E⟧✓Pair Q σ1›
            by (unfold P_rec[of σ0] Q_rec[of σ1])
              (auto simp add: SKIPS_def Ndet_and_SyncPair Mprefix_SyncPair_constant ‹ω A0 σ0 ≠ {}›
                GlobalNdet_Mprefix_distr GlobalNdet_sets_commute[of ‹τ A1 _ _›] ‹ω A1 σ1 = {}›
                intro!: mono_Mprefix_eq mono_GlobalNdet_eq)
          finally show ‹?f (σ0, σ1) = …› .
        next
          assume ‹ω A0 σ0 = {}› ‹ω A1 σ1 ≠ {}›
          from ρ_disjoint_ε(2) ‹ω A1 σ1 ≠ {}› have ‹ε A1 σ1 = {}›
            by (simp add: ρ_disjoint_ε_def ρ_simps)
          have ‹?f (σ0, σ1) = □a∈(ε A0 σ0 - E) → (⊓σ0'∈τ A0 σ0 a. (P σ0' ⟦E⟧✓Pair SKIPS (ω A1 σ1)))›
            by (auto simp add: ω_A ε_A ‹ω A0 σ0 = {}› ‹ε A1 σ1 = {}› intro!: mono_Mprefix_eq,
                auto simp add: A_def combinePair_Syncptick_defs ‹ω A1 σ1 ≠ {}›
                ‹ε A1 σ1 = {}› cartprod_rwrt Q_rec[of σ1] intro!: mono_GlobalNdet_eq)
          also have ‹… = P σ0 ⟦E⟧✓Pair Q σ1›
            by (unfold P_rec[of σ0] Q_rec[of σ1])
              (auto simp add: SKIPS_def Ndet_and_SyncPair Mprefix_SyncPair_constant ‹ω A1 σ1 ≠ {}›
                GlobalNdet_Mprefix_distr GlobalNdet_sets_commute[of ‹τ A0 _ _›] ‹ω A0 σ0 = {}›
                intro!: mono_Mprefix_eq mono_GlobalNdet_eq)
          finally show ‹?f (σ0, σ1) = …› .
        next
          assume ‹ω A0 σ0 ≠ {}› ‹ω A1 σ1 ≠ {}›
          with ρ_disjoint_ε have ‹ε A0 σ0 = {}› ‹ε A1 σ1 = {}›
            by (simp_all add: ρ_disjoint_ε_def ρ_simps)
          show ‹ω A0 σ0 ≠ {} ⟹ ω A1 σ1 ≠ {} ⟹ ?f (σ0, σ1) = P σ0 ⟦E⟧✓Pair Q σ1›
            by (simp add: ‹ω A0 σ0 ≠ {}› ‹ω A1 σ1 ≠ {}› ω_A P_rec[of σ0] Q_rec[of σ1] SKIPS_def
                Ndet_and_SyncPair cartprod_rwrt GlobalNdet_sets_commute[of ‹ω A0 _›])
        qed
      qed
    qed
  qed
qed

corollary P_nd_combinePair_Syncptick :
  ‹P⟪A0⟫nd σ0 ⟦E⟧✓Pair P⟪A1⟫nd σ1 = P⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⟫nd (σ0, σ1)›
proof -
  have ‹P⟪A0⟫nd σ0 ⟦E⟧✓Pair P⟪A1⟫nd σ1 =
        PSKIPS⟪A0⦇ω := λσ. {}⦈⟫nd σ0 ⟦E⟧✓Pair PSKIPS⟪A1⦇ω := λσ. {}⦈⟫nd σ1›
    by (simp add: PSKIPS_nd_updated_ω)
  also have ‹… = PSKIPS⟪⟪A0⦇ω := λσ. {}⦈ nd⊗⟦E⟧✓Pair A1⦇ω := λσ. {}⦈⟫⟫nd (σ0, σ1)›
    by (rule PSKIPS_nd_combinePair_Syncptick) simp_all
  also have ‹⟪A0⦇ω := λσ. {}⦈ nd⊗⟦E⟧✓Pair A1⦇ω := λσ. {}⦈⟫ = ⟪A0 nd⊗⟦E⟧✓Pair A1⟫⦇ω := λσ. {}⦈›
    by (auto simp add: combinePair_Syncptick_defs)
  also have ‹PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⦇ω := λσ. {}⦈⟫nd = P⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⟫nd›
    by (simp add: PSKIPS_nd_updated_ω)
  finally show ?thesis .
qed

corollary PSKIPS_d_combinePair_Syncptick:
  ‹PSKIPS⟪A0⟫d σ0 ⟦E⟧✓Pair PSKIPS⟪A1⟫d σ1 = PSKIPS⟪⟪A0 d⊗⟦E⟧✓Pair A1⟫⟫d (σ0, σ1)›
  if ‹ρ_disjoint_ε A0› and ‹ρ_disjoint_ε A1› and ‹indep_enabl A0 σ0 E A1 σ1›
proof -
  have ‹PSKIPS⟪A0⟫d σ0 ⟦E⟧✓Pair PSKIPS⟪A1⟫d σ1 = PSKIPS⟪⟪A0⟫d↪nd⟫nd σ0 ⟦E⟧✓Pair PSKIPS⟪⟪A1⟫d↪nd⟫nd σ1›
    by (simp flip: PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
  also have ‹… = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pair ⟪A1⟫d↪nd⟫⟫nd (σ0, σ1)›
    by (rule PSKIPS_nd_combinePair_Syncptick)
      (metis ρ_disjoint_ε_def det_ndet_conv_ε(1) det_ndet_conv_ρ(1) ‹ρ_disjoint_ε A0›,
        metis ρ_disjoint_ε_def det_ndet_conv_ε(1) det_ndet_conv_ρ(1) ‹ρ_disjoint_ε A1›)
  also have ‹… = PSKIPS⟪⟪A0 d⊗⟦E⟧✓Pair A1⟫⟫d (σ0, σ1)›
    by (simp add: PSKIPS_combinePair_Syncptick_behaviour_when_indep ‹indep_enabl A0 σ0 E A1 σ1›)
  finally show ?thesis .
qed

corollary P_d_combinePair_Syncptick:
  ‹P⟪A0⟫d σ0 ⟦E⟧✓Pair P⟪A1⟫d σ1 = P⟪⟪A0 d⊗⟦E⟧✓Pair A1⟫⟫d (σ0, σ1)›
  if ‹indep_enabl A0 σ0 E A1 σ1›
proof -
  have ‹P⟪A0⟫d σ0 ⟦E⟧✓Pair P⟪A1⟫d σ1 =
        PSKIPS⟪A0⦇ω := λσ. ◇⦈⟫d σ0 ⟦E⟧✓Pair PSKIPS⟪A1⦇ω := λσ. ◇⦈⟫d σ1›
    by (simp add: PSKIPS_d_updated_ω)
  also have ‹… = PSKIPS⟪⟪A0⦇ω := λσ. ◇⦈ d⊗⟦E⟧✓Pair A1⦇ω := λσ. ◇⦈⟫⟫d (σ0, σ1)›
    by (subst PSKIPS_d_combinePair_Syncptick, simp_all add: ρ_simps ρ_disjoint_ε_def)
      (rule indep_enablI,
        use ‹indep_enabl A0 σ0 E A1 σ1›[THEN indep_enablD] in ‹simp add: ε_simps›)
  also have ‹⟪A0⦇ω := λσ. ◇⦈ d⊗⟦E⟧✓Pair A1⦇ω := λσ. ◇⦈⟫ = ⟪A0 d⊗⟦E⟧✓Pair A1⟫⦇ω := λσ. ◇⦈›
    by (simp add: combinePair_Syncptick_defs, intro ext, simp)
  also have ‹PSKIPS⟪⟪A0 d⊗⟦E⟧✓Pair A1⟫⦇ω := λσ. ◇⦈⟫d = P⟪⟪A0 d⊗⟦E⟧✓Pair A1⟫⟫d›
    by (simp add: PSKIPS_d_updated_ω)
  finally show ?thesis .
qed



subsubsection ‹Pairlist›

theorem PSKIPS_nd_combinePairlist_Syncptick :
  fixes E :: ‹'a set›
  assumes ρ_disjoint_ε : ‹ρ_disjoint_ε A0› ‹ρ_disjoint_ε A1›
  shows ‹PSKIPS⟪A0⟫nd σ0 ⟦E⟧✓Pairlist PSKIPS⟪A1⟫nd σ1 = PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pairlist A1⟫⟫nd [σ0, σ1]›
proof -
  let ?A = ‹⦇τ = τ ⟪A0 nd⊗⟦E⟧✓Pair A1⟫, ω = λσ. (λ(r, s). [r, s]) ` ω ⟪A0 nd⊗⟦E⟧✓Pair A1⟫ σ⦈›
  have ‹PSKIPS⟪A0⟫nd σ0 ⟦E⟧✓Pairlist PSKIPS⟪A1⟫nd σ1 =
        RenamingTick (PSKIPS⟪A0⟫nd σ0 ⟦E⟧✓Pair PSKIPS⟪A1⟫nd σ1) (λ(r, s). [r, s])›
    by (simp only: SyncPair_to_SyncPairlist)
  also have ‹… = RenamingTick (PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⟫nd (σ0, σ1)) (λ(r, s). [r, s])›
    by (simp add: PSKIPS_nd_combinePair_Syncptick ρ_disjoint_ε)
  also have ‹… = PSKIPS⟪?A⟫nd (σ0, σ1)›
    by (simp only: RenamingTick_PSKIPS_nd)
  also have ‹… = PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pairlist A1⟫⟫nd [σ0, σ1]›
    by (auto intro!: PSKIPS_nd_eqI_strong[of ‹λ(r, s). [r, s]› _ ‹(σ0, σ1)›, simplified] inj_onI)
      (auto simp add: combine_Syncptick_defs split: if_split_asm)
  finally show ?thesis .
qed

corollary P_nd_combinePairlist_Syncptick :
  ‹P⟪A0⟫nd σ0 ⟦E⟧✓Pairlist P⟪A1⟫nd σ1 = P⟪⟪A0 nd⊗⟦E⟧✓Pairlist A1⟫⟫nd [σ0, σ1]›
proof -
  have ‹P⟪A0⟫nd σ0 ⟦E⟧✓Pairlist P⟪A1⟫nd σ1 =
        PSKIPS⟪A0⦇ω := λσ. {}⦈⟫nd σ0 ⟦E⟧✓Pairlist PSKIPS⟪A1⦇ω := λσ. {}⦈⟫nd σ1›
    by (simp add: PSKIPS_nd_updated_ω)
  also have ‹… = PSKIPS⟪⟪A0⦇ω := λσ. {}⦈ nd⊗⟦E⟧✓Pairlist A1⦇ω := λσ. {}⦈⟫⟫nd [σ0, σ1]›
    by (rule PSKIPS_nd_combinePairlist_Syncptick) simp_all
  also have ‹⟪A0⦇ω := λσ. {}⦈ nd⊗⟦E⟧✓Pairlist A1⦇ω := λσ. {}⦈⟫ = ⟪A0 nd⊗⟦E⟧✓Pairlist A1⟫⦇ω := λσ. {}⦈›
    by (simp add: combinePairlist_Syncptick_defs, intro ext, simp)
  also have ‹PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pairlist A1⟫⦇ω := λσ. {}⦈⟫nd = P⟪⟪A0 nd⊗⟦E⟧✓Pairlist A1⟫⟫nd›
    by (simp add: PSKIPS_nd_updated_ω)
  finally show ?thesis .
qed

corollary PSKIPS_d_combinePairlist_Syncptick :
  ‹PSKIPS⟪A0⟫d σ0 ⟦E⟧✓Pairlist PSKIPS⟪A1⟫d σ1 = PSKIPS⟪⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⟫d [σ0, σ1]›
  if ‹ρ_disjoint_ε A0› and ‹ρ_disjoint_ε A1› and ‹indep_enabl A0 σ0 E A1 σ1›
proof -
  have ‹PSKIPS⟪A0⟫d σ0 ⟦E⟧✓Pairlist PSKIPS⟪A1⟫d σ1 = PSKIPS⟪⟪A0⟫d↪nd⟫nd σ0 ⟦E⟧✓Pairlist PSKIPS⟪⟪A1⟫d↪nd⟫nd σ1›
    by (simp flip: PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
  also have ‹… = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pairlist ⟪A1⟫d↪nd⟫⟫nd [σ0, σ1]›
    by (rule PSKIPS_nd_combinePairlist_Syncptick)
      (metis ρ_disjoint_ε_def det_ndet_conv_ε(1) det_ndet_conv_ρ(1) ‹ρ_disjoint_ε A0›,
        metis ρ_disjoint_ε_def det_ndet_conv_ε(1) det_ndet_conv_ρ(1) ‹ρ_disjoint_ε A1›)
  also have ‹… = PSKIPS⟪⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⟫d [σ0, σ1]›
    by (simp add: PSKIPS_combinePairlist_Syncptick_behaviour_when_indep ‹indep_enabl A0 σ0 E A1 σ1›)
  finally show ?thesis .
qed

corollary P_d_combinePairlist_Syncptick :
  ‹P⟪A0⟫d σ0 ⟦E⟧✓Pairlist P⟪A1⟫d σ1 = P⟪⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⟫d [σ0, σ1]›
  if ‹indep_enabl A0 σ0 E A1 σ1›
proof -
  have ‹P⟪A0⟫d σ0 ⟦E⟧✓Pairlist P⟪A1⟫d σ1 =
        PSKIPS⟪A0⦇ω := λσ. ◇⦈⟫d σ0 ⟦E⟧✓Pairlist PSKIPS⟪A1⦇ω := λσ. ◇⦈⟫d σ1›
    by (simp add: PSKIPS_d_updated_ω)
  also have ‹… = PSKIPS⟪⟪A0⦇ω := λσ. ◇⦈ d⊗⟦E⟧✓Pairlist A1⦇ω := λσ. ◇⦈⟫⟫d [σ0, σ1]›
    by (subst PSKIPS_d_combinePairlist_Syncptick, simp_all)
      (rule indep_enablI,
        use ‹indep_enabl A0 σ0 E A1 σ1›[THEN indep_enablD] in simp)
  also have ‹⟪A0⦇ω := λσ. ◇⦈ d⊗⟦E⟧✓Pairlist A1⦇ω := λσ. ◇⦈⟫ = ⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⦇ω := λσ. ◇⦈›
    by (simp add: combinePairlist_Syncptick_defs, intro ext, simp)
  also have ‹PSKIPS⟪⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⦇ω := λσ. ◇⦈⟫d = P⟪⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⟫d›
    by (simp add: PSKIPS_d_updated_ω)
  finally show ?thesis .
qed



subsection ‹Rlist›

theorem PSKIPS_nd_combineRlist_Syncptick :
  fixes E :: ‹'a set›
  assumes ρ_disjoint_ε : ‹ρ_disjoint_ε A0› ‹ρ_disjoint_ε A1›
  defines A_def: ‹A ≡ ⟪A0 nd⊗⟦E⟧✓Rlist A1⟫›      
  defines P_def: ‹P ≡ PSKIPS⟪A0⟫nd› and Q_def: ‹Q ≡ PSKIPS⟪A1⟫nd› and S_def: ‹S ≡ PSKIPS⟪A⟫nd›
  shows ‹P σ0 ⟦E⟧✓Rlist Q σs = S (σ0 # σs)›
proof -
  let ?A' = ‹⦇τ = τ ⟪A0 nd⊗⟦E⟧✓Pair A1⟫, ω = λσ. (λ(x, y). x # y) ` ω ⟪A0 nd⊗⟦E⟧✓Pair A1⟫ σ⦈›
  from PSKIPS_nd_combinePair_Syncptick[OF ρ_disjoint_ε]
  have ‹P σ0 ⟦E⟧✓Pair Q σs = PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⟫nd (σ0, σs)› by (simp add: P_def Q_def)
  hence ‹RenamingTick (P σ0 ⟦E⟧✓Pair Q σs) (λ(σ0, σs). σ0 # σs) =
         RenamingTick (PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⟫nd (σ0, σs)) (λ(σ0, σs). σ0 # σs)› by simp
  also have ‹RenamingTick (P σ0 ⟦E⟧✓Pair Q σs) (λ(σ0, σs). σ0 # σs) = P σ0 ⟦E⟧✓Rlist Q σs›
    by (auto intro: inj_onI SyncPair.inj_on_RenamingTick_Syncptick
        [of ‹λ(σ0, σs). σ0 # σs›, simplified])
  also have ‹RenamingTick (PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⟫nd (σ0, σs)) (λ(σ0, σs). σ0 # σs) = S (σ0 # σs)›
  proof (unfold RenamingTick_PSKIPS_nd S_def,
      rule PSKIPS_nd_eqI_strong[of ‹λ(σ0, σs). σ0 # σs› ?A' ‹(σ0, σs)›, simplified])
    show ‹inj_on (λ(σ0, σs). σ0 # σs) (ℛnd ?A' (σ0, σs))› by (auto intro: inj_onI)
  next
    show ‹τ A (case σ' of (σ0, σs) ⇒ σ0 # σs) e =
          (λσ''. case σ'' of (σ0, σs) ⇒ σ0 # σs) ` τ ⟪A0 nd⊗⟦E⟧✓Pair A1⟫ σ' e› for σ' e
      by (cases σ') (auto simp add: A_def combineRlist_Syncptick_defs combinePair_Syncptick_defs)
  next
    show ‹ω A (case σ' of (σ0, σs) ⇒ σ0 # σs) =
          (λσ''. case σ'' of (σ0, σs) ⇒ σ0 # σs) ` ω ⟪A0 nd⊗⟦E⟧✓Pair A1⟫ σ'› for σ'
      by (cases σ') (auto simp add: A_def combineRlist_Syncptick_defs combinePair_Syncptick_defs)
  qed
  finally show ‹P σ0 ⟦E⟧✓Rlist Q σs = S (σ0 # σs)› .
qed

corollary P_nd_combineRlist_Syncptick :
  ‹P⟪A0⟫nd σ0 ⟦E⟧✓Rlist P⟪A1⟫nd σs = P⟪⟪A0 nd⊗⟦E⟧✓Rlist A1⟫⟫nd (σ0 # σs)›
proof -
  have ‹P⟪A0⟫nd σ0 ⟦E⟧✓Rlist P⟪A1⟫nd σs =
        PSKIPS⟪A0⦇ω := λσ. {}⦈⟫nd σ0 ⟦E⟧✓Rlist PSKIPS⟪A1⦇ω := λσ. {}⦈⟫nd σs›
    by (simp add: PSKIPS_nd_updated_ω)
  also have ‹… = PSKIPS⟪⟪A0⦇ω := λσ. {}⦈ nd⊗⟦E⟧✓Rlist A1⦇ω := λσ. {}⦈⟫⟫nd (σ0 # σs)›
    by (rule PSKIPS_nd_combineRlist_Syncptick)
      (simp_all add: ρ_simps ρ_disjoint_ε_def)
  also have ‹⟪A0⦇ω := λσ. {}⦈ nd⊗⟦E⟧✓Rlist A1⦇ω := λσ. {}⦈⟫ = ⟪A0 nd⊗⟦E⟧✓Rlist A1⟫⦇ω := λσ. {}⦈›
    by (simp add: combineRlist_Syncptick_defs, intro ext, simp add: ε_simps)
  also have ‹PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Rlist A1⟫⦇ω := λσ. {}⦈⟫nd = P⟪⟪A0 nd⊗⟦E⟧✓Rlist A1⟫⟫nd›
    by (simp add: PSKIPS_nd_updated_ω)
  finally show ?thesis .
qed

corollary PSKIPS_d_combineRlist_Syncptick:
  ‹PSKIPS⟪A0⟫d σ0 ⟦E⟧✓Rlist PSKIPS⟪A1⟫d σs = PSKIPS⟪⟪A0 d⊗⟦E⟧✓Rlist A1⟫⟫d (σ0 # σs)›
  if ‹ρ_disjoint_ε A0› and ‹ρ_disjoint_ε A1› and ‹indep_enabl A0 σ0 E A1 σs›
proof -
  have ‹PSKIPS⟪A0⟫d σ0 ⟦E⟧✓Rlist PSKIPS⟪A1⟫d σs = PSKIPS⟪⟪A0⟫d↪nd⟫nd σ0 ⟦E⟧✓Rlist PSKIPS⟪⟪A1⟫d↪nd⟫nd σs›
    by (simp flip: PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
  also have ‹… = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Rlist ⟪A1⟫d↪nd⟫⟫nd (σ0 # σs)›
    by (rule PSKIPS_nd_combineRlist_Syncptick)
      (metis ρ_disjoint_ε_def det_ndet_conv_ε(1) det_ndet_conv_ρ(1) ‹ρ_disjoint_ε A0›,
        metis ρ_disjoint_ε_def det_ndet_conv_ε(1) det_ndet_conv_ρ(1) ‹ρ_disjoint_ε A1›)
  also have ‹… = PSKIPS⟪⟪A0 d⊗⟦E⟧✓Rlist A1⟫⟫d (σ0 # σs)›
    by (simp add: PSKIPS_combineRlist_Syncptick_behaviour_when_indep ‹indep_enabl A0 σ0 E A1 σs›)
  finally show ?thesis .
qed

corollary P_d_combineRlist_Syncptick:
  ‹P⟪A0⟫d σ0 ⟦E⟧✓Rlist P⟪A1⟫d σs = P⟪⟪A0 d⊗⟦E⟧✓Rlist A1⟫⟫d (σ0 # σs)›
  if ‹indep_enabl A0 σ0 E A1 σs›
proof -
  have ‹P⟪A0⟫d σ0 ⟦E⟧✓Rlist P⟪A1⟫d σs =
        PSKIPS⟪A0⦇ω := λσ. ◇⦈⟫d σ0 ⟦E⟧✓Rlist PSKIPS⟪A1⦇ω := λσ. ◇⦈⟫d σs›
    by (simp add: PSKIPS_d_updated_ω)
  also have ‹… = PSKIPS⟪⟪A0⦇ω := λσ. ◇⦈ d⊗⟦E⟧✓Rlist A1⦇ω := λσ. ◇⦈⟫⟫d (σ0 # σs)›
    by (rule PSKIPS_d_combineRlist_Syncptick, simp_all add: ρ_simps ρ_disjoint_ε_def)
      (rule indep_enablI,
        use ‹indep_enabl A0 σ0 E A1 σs›[THEN indep_enablD] in ‹simp add: ε_simps›)
  also have ‹⟪A0⦇ω := λσ. ◇⦈ d⊗⟦E⟧✓Rlist A1⦇ω := λσ. ◇⦈⟫ = ⟪A0 d⊗⟦E⟧✓Rlist A1⟫⦇ω := λσ. ◇⦈›
    by (simp add: combineRlist_Syncptick_defs, intro ext, simp add: ε_simps)
  also have ‹PSKIPS⟪⟪A0 d⊗⟦E⟧✓Rlist A1⟫⦇ω := λσ. ◇⦈⟫d = P⟪⟪A0 d⊗⟦E⟧✓Rlist A1⟫⟫d›
    by (simp add: PSKIPS_d_updated_ω)
  finally show ?thesis .
qed



subsection ‹ListslenL›

theorem PSKIPS_nd_combineListslenL_Syncptick :
  fixes E :: ‹'a set›
  assumes same_length_reach0 : ‹⋀σ0'. σ0' ∈ ℛnd A0 σ0 ⟹ length σ0' = len0›
    and same_length_term0 : ‹⋀σ0' rs. σ0' ∈ ℛnd A0 σ0 ⟹ rs ∈ ω A0 σ0' ⟹ length rs = len0›
    and ρ_disjoint_ε : ‹ρ_disjoint_ε A0› ‹ρ_disjoint_ε A1›
  defines A_def: ‹A ≡ ⟪A0 nd⊗⟦len0, E⟧✓ListslenL A1⟫›      
  defines P_def: ‹P ≡ PSKIPS⟪A0⟫nd› and Q_def: ‹Q ≡ PSKIPS⟪A1⟫nd› and S_def: ‹S ≡ PSKIPS⟪A⟫nd›
  shows ‹P σ0 ⇘len0⇙⟦E⟧✓ListslenL Q σ1 = S (σ0 @ σ1)›
proof -
  let ?A' = ‹⦇τ = τ ⟪A0 nd⊗⟦E⟧✓Pair A1⟫, ω = λσ. (λ(x, y). x @ y) ` ω ⟪A0 nd⊗⟦E⟧✓Pair A1⟫ σ⦈›
  let ?RT = RenamingTick
  have * : ‹σ' ∈ ℛnd ?A' (σ0, σ1) ⟹ length (fst σ') = len0› for σ'
    by (metis (no_types, lifting) ℛnd_combinendPair_Syncptick_subset mem_Sigma_iff prod.collapse
        same_τ_implies_same_ℛnd same_length_reach0 select_convs(1) subset_iff)

  from PSKIPS_nd_combinePair_Syncptick[OF ρ_disjoint_ε]
  have ‹P σ0 ⟦E⟧✓Pair Q σ1 = PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⟫nd (σ0, σ1)›
    by (simp add: P_def Q_def)

  hence ‹?RT (P σ0 ⟦E⟧✓Pair Q σ1) (λ(σ0, σs). σ0 @ σs) =
         ?RT (PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⟫nd (σ0, σ1)) (λ(σ0, σs). σ0 @ σs)› by simp
  also have ‹?RT (P σ0 ⟦E⟧✓Pair Q σ1) (λ(σ0, σs). σ0 @ σs) = P σ0 ⇘len0⇙⟦E⟧✓ListslenL Q σ1›
    by (rule SyncPair_to_SyncListslenL[OF is_ticks_length_PSKIPS_nd[of A0, folded P_def]])
      (fact same_length_term0)
  also have ‹?RT (PSKIPS⟪⟪A0 nd⊗⟦E⟧✓Pair A1⟫⟫nd (σ0, σ1)) (λ(σ0, σs). σ0 @ σs) = S (σ0 @ σ1)›
    by (auto simp add: RenamingTick_PSKIPS_nd S_def dest!: "*"
        intro!: PSKIPS_nd_eqI_strong[of ‹λ(σ0, σs). σ0 @ σs› ?A' ‹(σ0, σ1)›, simplified] inj_onI)
      (force simp add: image_iff A_def combineListslenL_Syncptick_defs combinePair_Syncptick_defs split: if_split_asm)+
  finally show ?thesis .
qed

corollary P_nd_combineListslenL_Syncptick :
  ‹P⟪A0⟫nd σ0 ⇘len0⇙⟦E⟧✓ListslenL P⟪A1⟫nd σ1 = P⟪⟪A0 nd⊗⟦len0, E⟧✓ListslenL A1⟫⟫nd (σ0 @ σ1)›
  if same_length_reach0 : ‹⋀σ0'. σ0' ∈ ℛnd A0 σ0 ⟹ length σ0' = len0›
proof -
  have * : ‹σs ∈ ℛnd ⟪A0⦇ω := λσ0. {}⦈ nd⊗⟦len0, E⟧✓ListslenL A1⦇ω := λσ1. {}⦈⟫ (σ0 @ σ1) ⟹ len0 ≤ length σs› for σs
    by (auto dest: set_rev_mp[OF _ ℛnd_combinendListslenL_Syncptick_subset]
        simp add: same_length_reach0)
  have ‹P⟪A0⟫nd σ0 ⇘len0⇙⟦E⟧✓ListslenL P⟪A1⟫nd σ1 =
        PSKIPS⟪A0⦇ω := λσ0. {}⦈⟫nd σ0 ⇘len0⇙⟦E⟧✓ListslenL PSKIPS⟪A1⦇ω := λσ1. {}⦈⟫nd σ1›
    by (simp only: PSKIPS_nd_updated_ω)
  also have ‹… = PSKIPS⟪⟪A0⦇ω := λσ0. {}⦈ nd⊗⟦len0, E⟧✓ListslenL A1⦇ω := λσ1. {}⦈⟫⟫nd (σ0 @ σ1)›
    by (auto intro: PSKIPS_nd_combineListslenL_Syncptick simp add: same_length_reach0)
  also have ‹… = PSKIPS⟪⟪A0 nd⊗⟦len0, E⟧✓ListslenL A1⟫⦇ω := λσ1. {}⦈⟫nd (σ0 @ σ1)›
    by (auto intro!: PSKIPS_nd_eqI_strong_id dest!: "*")
      (auto simp add: combineListslenL_Syncptick_defs split: if_split_asm)
  also have ‹… = P⟪⟪A0 nd⊗⟦len0, E⟧✓ListslenL A1⟫⟫nd (σ0 @ σ1)›
    by (simp only: PSKIPS_nd_updated_ω)
  finally show ?thesis .
qed

corollary PSKIPS_d_combineListslenL_Syncptick :
  assumes same_length_reach0 : ‹⋀σ0'. σ0' ∈ ℛd A0 σ0 ⟹ length σ0' = len0›
    and same_length_term0 : ‹⋀σ0'. σ0' ∈ ℛd A0 σ0 ⟹ ω A0 σ0' ≠ ◇ ⟹ length ⌈ω A0 σ0'⌉ = len0›
    and ρ_disjoint_ε : ‹ρ_disjoint_ε A0› ‹ρ_disjoint_ε A1›
    and indep_enabl : ‹indep_enabl A0 σ0 E A1 σ1›
  shows ‹PSKIPS⟪A0⟫d σ0 ⇘len0⇙⟦E⟧✓ListslenL PSKIPS⟪A1⟫d σ1 =
         PSKIPS⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⟫d (σ0 @ σ1)›
proof -
  have * : ‹σs ∈ ℛnd ⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧✓ListslenL ⟪A1⟫d↪nd⟫ (σ0 @ σ1) ⟹
            ∃σ0' σ1'. σs = σ0' @ σ1' ∧ σ0' ∈ ℛd A0 σ0 ∧ σ1' ∈ ℛd A1 σ1› for σs
    by (auto dest!: set_rev_mp[OF _ ℛnd_combinendListslenL_Syncptick_subset]
        simp add: ℛnd_from_det_to_ndet same_length_reach0)+
  have ‹PSKIPS⟪A0⟫d σ0 ⇘len0⇙⟦E⟧✓ListslenL PSKIPS⟪A1⟫d σ1 =
        PSKIPS⟪⟪A0⟫d↪nd⟫nd σ0 ⇘len0⇙⟦E⟧✓ListslenL PSKIPS⟪⟪A1⟫d↪nd⟫nd σ1›
    by (simp only: PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
  also from same_length_term0 have ‹… = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧✓ListslenL ⟪A1⟫d↪nd⟫⟫nd (σ0 @ σ1)›
    by (auto intro!: PSKIPS_nd_combineListslenL_Syncptick split: option.split_asm
        simp add: ρ_disjoint_ε ℛnd_from_det_to_ndet same_length_reach0 ω_from_det_to_ndet)
      (metis option.sel)
  also from indep_enabl have ‹… = PSKIPS⟪⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⟫d↪nd⟫nd (σ0 @ σ1)›
    by (auto intro!: PSKIPS_nd_eqI_strong_id
        τ_combineListslenL_Syncptick_behaviour_when_indep ω_combineListslenL_Syncptick_behaviour
        simp add: same_length_reach0 dest!: "*" indep_enablD)
  also have ‹… = PSKIPS⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⟫d (σ0 @ σ1)›
    by (simp only: PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
  finally show ?thesis .
qed

corollary P_d_combineListslenL_Syncptick :
  assumes same_length_reach0 : ‹⋀σ0'. σ0' ∈ ℛd A0 σ0 ⟹ length σ0' = len0›
    and indep_enabl : ‹indep_enabl A0 σ0 E A1 σ1›
  shows ‹P⟪A0⟫d σ0 ⇘len0⇙⟦E⟧✓ListslenL P⟪A1⟫d σ1 =
         P⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⟫d (σ0 @ σ1)›
proof -
  have * : ‹σs ∈ ℛd ⟪A0⦇ω := λσ0. ◇⦈ d⊗⟦len0, E⟧✓ListslenL A1⦇ω := λσ1. ◇⦈⟫ (σ0 @ σ1) ⟹ len0 ≤ length σs› for σs
    by (auto dest: set_rev_mp[OF _ ℛd_combinedListslenL_Syncptick_subset]
        simp add: same_length_reach0)
  have ‹P⟪A0⟫d σ0 ⇘len0⇙⟦E⟧✓ListslenL P⟪A1⟫d σ1 =
        PSKIPS⟪A0⦇ω := λσ0. ◇⦈⟫d σ0 ⇘len0⇙⟦E⟧✓ListslenL PSKIPS⟪A1⦇ω := λσ1. ◇⦈⟫d σ1›
    by (simp only: PSKIPS_d_updated_ω)
  also from indep_enabl
  have ‹… = PSKIPS⟪⟪A0⦇ω := λσ0. ◇⦈ d⊗⟦len0, E⟧✓ListslenL A1⦇ω := λσ1. ◇⦈⟫⟫d (σ0 @ σ1)›
    by (auto intro: PSKIPS_d_combineListslenL_Syncptick simp add: same_length_reach0)
  also have ‹… = PSKIPS⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⦇ω := λσ0. ◇⦈⟫d (σ0 @ σ1)›
    by (auto intro!: PSKIPS_d_eqI_strong_id dest!: "*")
      (auto simp add: combineListslenL_Syncptick_defs split: if_split_asm)
  also have ‹… = P⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⟫d (σ0 @ σ1)›
    by (simp only: PSKIPS_d_updated_ω)
  finally show ?thesis .
qed



subsection ‹Multiple›

theorem PSKIPS_nd_compactification_Syncptick:
  ‹length σs = length As ⟹ (⋀A. A ∈ set As ⟹ ρ_disjoint_ε A) ⟹
   ⟦E⟧✓ (σ, A) ∈@ zip σs As. PSKIPS⟪A⟫nd σ = PSKIPS⟪⟪nd⨂⟦E⟧✓ As⟫⟫nd σs›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by (simp, subst PSKIPS_nd_rec, simp)
next
  case (single σ0 A0) show ?case
    by (auto simp add: RenamingTick_PSKIPS_nd singl_list_conv_defs
        intro!: inj_onI PSKIPS_nd_eqI_strong)
next
  case (Cons σ0 σ1 σs A0 A1 As)
  have ρ_disjoint_ε : ‹A ∈ set (A1 # As) ⟹ ρ_disjoint_ε A› for A
    by (simp add: Cons.prems)
  show ?case
    by (simp add: Cons.hyps(3)[OF ρ_disjoint_ε, simplified] Cons.prems
        PSKIPS_nd_combineRlist_Syncptick ρ_disjoint_ε_transmission_to_iterated_combinend_Syncptick)
qed

corollary P_nd_compactification_Syncptick:
  ‹length σs = length As ⟹ ⟦E⟧✓ (σ, A) ∈@ zip σs As. P⟪A⟫nd σ = P⟪⟪nd⨂⟦E⟧✓ As⟫⟫nd σs›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by (simp, subst P_nd_rec, simp)
next
  case (single σ0 A0) show ?case
    by (simp, subst (1 2) PSKIPS_nd_updated_ω)
      (auto simp add: RenamingTick_PSKIPS_nd singl_list_conv_defs
        intro!: inj_onI PSKIPS_nd_eqI_strong)
next
  case (Cons σ0 σ1 σs A0 A1 As)
  show ?case
    by (simp add: Cons.hyps(3)[simplified] Cons.prems
        P_nd_combineRlist_Syncptick ρ_disjoint_ε_transmission_to_iterated_combinend_Syncptick)
qed

corollary PSKIPS_d_compactification_Syncptick:
  ‹⟦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) ∈@ zip σs As. PSKIPS⟪A⟫d σ = PSKIPS⟪⟪d⨂⟦E⟧✓ As⟫⟫d σs›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by (simp, subst PSKIPS_d_rec, simp)
next
  case (single σ0 A0) show ?case
    by (auto simp add: RenamingTick_PSKIPS_d singl_list_conv_defs
        intro!: inj_onI PSKIPS_d_eqI_strong split: option.split)
next
  case (Cons σ0 σ1 σs A0 A1 As)
  have ρ_disjoint_ε : ‹A ∈ set (A1 # As) ⟹ ρ_disjoint_ε A› for A
    by (simp add: Cons.prems(1))
  have indep_enabl :
    ‹⟦i < length (A1 # As); j < length (A1 # As); i ≠ j⟧ ⟹
     indep_enabl ((A1 # As) ! i) ((σ1 # σs) ! i) E ((A1 # 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_ε A0› by (simp add: Cons.prems(1))
  moreover have ‹ρ_disjoint_ε ⟪d⨂⟦E⟧✓ A1 # As⟫›
    by (meson ρ_disjoint_ε ρ_disjoint_ε_transmission_to_iterated_combined_Syncptick)
  moreover have ‹indep_enabl A0 σ0 E ⟪d⨂⟦E⟧✓ A1 # As⟫ (σ1 # σs)›
    by (metis Cons.hyps(1) Cons.prems(2) length_Cons less_Suc_eq_le
        same_length_indep_transmission_to_iterated_combined_Syncptick)
  ultimately show ?case 
    by (simp add: PSKIPS_d_combineRlist_Syncptick
        Cons.hyps(3)[OF ρ_disjoint_ε indep_enabl, simplified])
qed

corollary P_d_compactification_Syncptick:
  ‹⟦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) ∈@ 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 A0) show ?case
    by (simp, subst (1 2) PSKIPS_d_updated_ω)
      (auto simp add: RenamingTick_PSKIPS_d singl_list_conv_defs
        intro!: inj_onI PSKIPS_d_eqI_strong split: option.split)
next
  case (Cons σ0 σ1 σs A0 A1 As)
  have indep_enabl :
    ‹⟦i < length (A1 # As); j < length (A1 # As); i ≠ j⟧ ⟹
     indep_enabl ((A1 # As) ! i) ((σ1 # σs) ! i) E ((A1 # 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 A0 σ0 E ⟪d⨂⟦E⟧✓ A1 # As⟫ (σ1 # σs)›
    by (metis Cons.hyps(1) Cons.prems length_Cons less_Suc_eq_le
        same_length_indep_transmission_to_iterated_combined_Syncptick)
  thus ?case 
    by (simp add: P_d_combineRlist_Syncptick
        Cons.hyps(3)[OF indep_enabl, simplified])
qed



(* 

corollary P_nd_compactification_Sync_order_is_arbitrary:
  ‹P⟪nd⨂⟦E⟧✓ As⟫nd σs = P⟪nd⨂⟦E⟧✓ As'⟫nd σs'›
  if ‹mset (zip σs As) = mset (zip σs' As')› and ‹length σs = length As› and ‹length σs' = length As'›
    and ‹∀A ∈ set As. finite_trans A› and ‹∀A ∈ set As. ρ_disjoint_ε A›
proof -
  have ‹P⟪nd⨂⟦E⟧✓ As⟫nd σs = PSKIPS⟪nd⨂⟦E⟧✓ (map (λA. A⦇𝒮F := {}⦈) As)⟫nd σs›
    apply (subst PSKIPS_nd_empty_𝒮F_bis, simp add: finite_trans_transmission_to_iterated_combinend_Syncptick that(4))
    by (rule PSKIPS_ndI_strong_id)
      (simp_all add: finite_trans_transmission_to_iterated_combinend_Syncptick that(4) prem_old_compact)
  moreover have ‹… = PSKIPS⟪nd⨂⟦E⟧✓ (map (λA. A⦇𝒮F := {}⦈) As')⟫nd σs'›
    by (rule PSKIPS_nd_compactification_Sync_order_is_arbitrary) (simp_all add: that zip_map2)
  moreover have ‹… = P⟪nd⨂⟦E⟧✓ As'⟫nd σs'›
    apply (subst PSKIPS_nd_empty_𝒮F_bis, metis in_set_impl_in_set_zip2 set_mset_mset set_zip_rightD
        finite_trans_transmission_to_iterated_combinend_Syncptick that(1, 3, 4))
    by (rule PSKIPS_ndI_strong_id, simp_all add: prem_old_compact)
      (metis in_set_impl_in_set_zip2 set_mset_mset set_zip_rightD
        finite_trans_transmission_to_iterated_combinend_Syncptick that(1, 3, 4))+
  ultimately show ‹P⟪nd⨂⟦E⟧✓ As⟫nd σs = P⟪nd⨂⟦E⟧✓ As'⟫nd σs'› by presburger
qed


corollary P_d_compactification_Sync_order_is_arbitrary:
  ‹P⟪d⨂⟦E⟧✓ As⟫d σs = P⟪d⨂⟦E⟧✓ As'⟫d σs'›
  if ‹mset (zip σs As) = mset (zip σs' As')› and ‹length σs = length As› and ‹length σs' = length As'›
    and ‹∀i<length As. ∀j<length As. i ≠ j ⟶ indep_enabl (As ! i) (σs ! i) E (As ! j) (σs ! j)›
    and ‹∀A ∈ set As. ρ_disjoint_ε A›
proof -
  have ‹P⟪d⨂⟦E⟧✓ As⟫d σs = PSKIPS⟪d⨂⟦E⟧✓ (map (λA. A⦇𝒮F := {}⦈) As)⟫d σs›
    apply (subst PSKIPS_d_empty_𝒮F_bis)
    by (rule PSKIPS_dI_strong_id) (simp_all add: prem_old_compact option.map_id)
  moreover have ‹… = PSKIPS⟪d⨂⟦E⟧✓ (map (λA. A⦇𝒮F := {}⦈) As')⟫d σs'›
    using that(4) by (intro PSKIPS_d_compactification_Sync_order_is_arbitrary)
      (simp_all add: that zip_map2 ℛd_𝒮F_useless ε_simps)
  moreover have ‹… = P⟪d⨂⟦E⟧✓ As'⟫d σs'›
    apply (subst PSKIPS_d_empty_𝒮F_bis)
    by (rule PSKIPS_dI_strong_id) (simp_all add: prem_old_compact option.map_id)
  ultimately show ‹P⟪d⨂⟦E⟧✓ As⟫d σs = P⟪d⨂⟦E⟧✓ As'⟫d σs'› by presburger
qed






 *)



section ‹Derived Versions›

lemma PSKIPS_nd_compactification_Syncptick_upt_version:
  ‹⟦E⟧✓ P ∈@ map Q [0..<n]. P = PSKIPS⟪⟪nd⨂⟦E⟧✓ map A [0..<n]⟫⟫nd (replicate n 0)›
  if ‹⋀i. i < n ⟹ ρ_disjoint_ε (A i)›
    ‹⋀i. i < n ⟹ PSKIPS⟪A i⟫nd 0 = Q i›
proof -
  have ‹⟦E⟧✓ P ∈@ map Q [0..<n]. P = ⟦E⟧✓ i ∈@ [0..<n]. Q i›
    by (auto intro: mono_MultiSyncptick_eq2)
  also have ‹… = ⟦E⟧✓ i ∈@ [0..<n]. PSKIPS⟪A i⟫nd 0›
    by (auto simp add: that(2) intro: mono_MultiSyncptick_eq)
  also have ‹… = ⟦E⟧✓ (σ, A) ∈@ zip (replicate n 0) (map A [0..<n]). PSKIPS⟪A⟫nd σ›
  proof (induct n rule: nat_induct_012)
    case (Suc k)
    have ‹⟦E⟧✓ i∈@ [0..<Suc k]. PSKIPS⟪A i⟫nd 0 =
          ⟦E⟧✓ i∈@ [0..<k]. PSKIPS⟪A i⟫nd 0 ⟦E⟧✓Llist PSKIPS⟪A k⟫nd 0›
      using Suc.hyps(1) by (simp add: MultiSyncptick_snoc)
    also have ‹… = ⟦E⟧✓ (σ, A) ∈@ zip (replicate k 0) (map A [0..<k]). PSKIPS⟪A⟫nd σ ⟦E⟧✓Llist PSKIPS⟪A k⟫nd 0›
      by (simp only: Suc.hyps(2))
    also have ‹… = ⟦E⟧✓ (σ, A) ∈@ zip (replicate (Suc k) 0) (map A [0..<Suc k]). PSKIPS⟪A⟫nd σ›
      using Suc.hyps(1) by (simp flip: replicate_append_same add: MultiSyncptick_snoc)
    finally show ?case .
  qed simp_all
  also have ‹… = PSKIPS⟪⟪nd⨂⟦E⟧✓ map A [0..<n]⟫⟫nd (replicate n 0)›
    by (rule PSKIPS_nd_compactification_Syncptick) (auto simp add: that(1))
  finally show ?thesis .
qed

lemma P_nd_compactification_Syncptick_upt_version:
  ‹⟦E⟧✓ P ∈@ map Q [0..<n]. P = P⟪⟪nd⨂⟦E⟧✓ map A [0..<n]⟫⟫nd (replicate n 0)›
  if ‹⋀i. i < n ⟹ P⟪A i⟫nd 0 = Q i›
proof -
  have ‹⟦E⟧✓ P ∈@ map Q [0..<n]. P = ⟦E⟧✓ i ∈@ [0..<n]. Q i›
    by (auto intro: mono_MultiSyncptick_eq2)
  also have ‹… = ⟦E⟧✓ i ∈@ [0..<n]. P⟪A i⟫nd 0›
    by (auto simp add: that intro: mono_MultiSyncptick_eq)
  also have ‹… = ⟦E⟧✓ (σ, A) ∈@ zip (replicate n 0) (map A [0..<n]). P⟪A⟫nd σ›
  proof (induct n rule: nat_induct_012)
    case (Suc k)
    have ‹⟦E⟧✓ i∈@ [0..<Suc k]. P⟪A i⟫nd 0 =
          ⟦E⟧✓ i∈@ [0..<k]. P⟪A i⟫nd 0 ⟦E⟧✓Llist P⟪A k⟫nd 0›
      using Suc.hyps(1) by (simp add: MultiSyncptick_snoc)
    also have ‹… = ⟦E⟧✓ (σ, A) ∈@ zip (replicate k 0) (map A [0..<k]). P⟪A⟫nd σ ⟦E⟧✓Llist P⟪A k⟫nd 0›
      by (simp only: Suc.hyps(2))
    also have ‹… = ⟦E⟧✓ (σ, A) ∈@ zip (replicate (Suc k) 0) (map A [0..<Suc k]). P⟪A⟫nd σ›
      using Suc.hyps(1) by (simp flip: replicate_append_same add: MultiSyncptick_snoc)
    finally show ?case .
  qed simp_all
  also have ‹… = P⟪⟪nd⨂⟦E⟧✓ map A [0..<n]⟫⟫nd (replicate n 0)›
    by (rule P_nd_compactification_Syncptick) simp
  finally show ?thesis .
qed

lemma PSKIPS_d_compactification_Syncptick_upt_version:
  ‹⟦E⟧✓ P ∈@ map Q [0..<n]. P = PSKIPS⟪⟪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 ⟹ PSKIPS⟪A i⟫d 0 = Q i›
proof -
  have ‹⟦E⟧✓ P ∈@ map Q [0..<n]. P = ⟦E⟧✓ i ∈@ [0..<n]. Q i›
    by (auto intro: mono_MultiSyncptick_eq2)
  also have ‹… = ⟦E⟧✓ i ∈@ [0..<n]. PSKIPS⟪A i⟫d 0›
    by (auto simp add: that(3) intro: mono_MultiSyncptick_eq)
  also have ‹… = ⟦E⟧✓ (σ, A) ∈@ zip (replicate n 0) (map A [0..<n]). PSKIPS⟪A⟫d σ›
  proof (induct n rule: nat_induct_012)
    case (Suc k)
    have ‹⟦E⟧✓ i∈@ [0..<Suc k]. PSKIPS⟪A i⟫d 0 =
          ⟦E⟧✓ i∈@ [0..<k]. PSKIPS⟪A i⟫d 0 ⟦E⟧✓Llist PSKIPS⟪A k⟫d 0›
      using Suc.hyps(1) by (simp add: MultiSyncptick_snoc)
    also have ‹… = ⟦E⟧✓ (σ, A) ∈@ zip (replicate k 0) (map A [0..<k]). PSKIPS⟪A⟫d σ ⟦E⟧✓Llist PSKIPS⟪A k⟫d 0›
      by (simp only: Suc.hyps(2))
    also have ‹… = ⟦E⟧✓ (σ, A) ∈@ zip (replicate (Suc k) 0) (map A [0..<Suc k]). PSKIPS⟪A⟫d σ›
      using Suc.hyps(1) by (simp flip: replicate_append_same add: MultiSyncptick_snoc)
    finally show ?case .
  qed simp_all
  also have ‹… = PSKIPS⟪⟪d⨂⟦E⟧✓ map A [0..<n]⟫⟫d (replicate n 0)›
    by (rule PSKIPS_d_compactification_Syncptick) (auto simp add: that(1, 2))
  finally show ?thesis .
qed

lemma P_d_compactification_Syncptick_upt_version:
  ‹⟦E⟧✓ P ∈@ map Q [0..<n]. P = P⟪⟪d⨂⟦E⟧✓ map A [0..<n]⟫⟫d (replicate n 0)›
  if ‹⋀i j. i < n ⟹ j < n ⟹ i ≠ j ⟹ indep_enabl (A i) 0 E (A j) 0›
    ‹⋀i. i < n ⟹ P⟪A i⟫d 0 = Q i›
proof -
  have ‹⟦E⟧✓ P ∈@ map Q [0..<n]. P = ⟦E⟧✓ i ∈@ [0..<n]. Q i›
    by (auto intro: mono_MultiSyncptick_eq2)
  also have ‹… = ⟦E⟧✓ i ∈@ [0..<n]. P⟪A i⟫d 0›
    by (auto simp add: that intro: mono_MultiSyncptick_eq)
  also have ‹… = ⟦E⟧✓ (σ, A)∈@ (zip (replicate n 0) (map A [0..<n])). P⟪A⟫d σ›
  proof (induct n rule: nat_induct_012)
    case (Suc k)
    have ‹⟦E⟧✓ i∈@ [0..<Suc k]. P⟪A i⟫d 0 =
          ⟦E⟧✓ i∈@ [0..<k]. P⟪A i⟫d 0 ⟦E⟧✓Llist P⟪A k⟫d 0›
      using Suc.hyps(1) by (simp add: MultiSyncptick_snoc)
    also have ‹… = ⟦E⟧✓ (σ, A)∈@ zip (replicate k 0) (map A [0..<k]). P⟪A⟫d σ ⟦E⟧✓Llist P⟪A k⟫d 0›
      by (simp only: Suc.hyps(2))
    also have ‹… = ⟦E⟧✓ (σ, A)∈@ zip (replicate (Suc k) 0) (map A [0..<Suc k]). P⟪A⟫d σ›
      using Suc.hyps(1) by (simp flip: replicate_append_same add: MultiSyncptick_snoc)
    finally show ?case .
  qed simp_all
  also have ‹… = P⟪⟪d⨂⟦E⟧✓ map A [0..<n]⟫⟫d (replicate n 0)›
    by (rule P_d_compactification_Syncptick) (auto simp add: that(1))
  finally show ?thesis .
qed



section ‹More on Iterated Combine and Events›

text ‹
Through @{thm [source] τ_iterated_combine_Syncptick ε_iterated_combine_Syncptick ℛ_iterated_combine_Syncptick},
we immediately recover the results proven in
theory‹HOL-CSP_Proc-Omata.Compactification_Synchronization_Product›.
›


(*<*)
end
  (*>*)