Theory Synchronization_Product_Sequential_Composition

(***********************************************************************************
 * Copyright (c) 2026 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, 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 ‹Advanced Laws about Synchronization Product of Sequential Compositions›

text ‹This is new in Isabelle26.›


(*<*)
theory Synchronization_Product_Sequential_Composition
  imports CSP_PTick_Laws Events_Ticks_CSP_PTick_Laws
begin
  (*>*)




section ‹LHS Move Together›

lemma SKIPS_FD_lhs_imp_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_is :
  ‹P ❙;⇩_✓ Q = ⊓r ∈ {r. ✓(r) ∈ P⇧⁰}. Q r› (is ‹?lhs = ?rhs›) if ‹SKIPS R ⊑⇩_F⇩_D P›
  by (subst SKIPS_FD_iff[OF that]) simp


lemma (in Synchro⇩_p⇩_t⇩_i⇩_c⇩_k) SKIPS_UNIV_FD_lhs_imp_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Seq⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2 = (P1 ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ❙;⇩_✓ (λ(r1, r2). (Q1 r1 ⟦S⟧⇩_✓ Q2 r2))›
  (is ‹?lhs = ?rhs›) if ‹SKIPS UNIV ⊑⇩_F⇩_D P1› ‹SKIPS UNIV ⊑⇩_F⇩_D P2›
proof -
  from that have * : ‹{r. ✓(r) ∈ P1⇧⁰} ≠ {}› ‹{r. ✓(r) ∈ P2⇧⁰} ≠ {}›
    by (metis SKIPS_FD_SKIPS_iff SKIPS_FD_iff empty_not_UNIV)+
  have ‹?lhs = ⊓r ∈ {r. ✓(r) ∈ P1⇧⁰}. Q1 r ⟦S⟧⇩_✓ ⊓r ∈ {r. ✓(r) ∈ P2⇧⁰}. Q2 r›
    by (subst SKIPS_FD_iff[OF that(1)], subst SKIPS_FD_iff[OF that(2)]) simp
  also from "*" have ‹… = ⊓r2 ∈ {r. ✓(r) ∈ P2⇧⁰}. ⊓r1 ∈ {r. ✓(r) ∈ P1⇧⁰}. (Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
    by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_left Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_right
        intro!: mono_GlobalNdet_eq)
  also have ‹... = ⊓(r1, r2) ∈ {r. ✓(r) ∈ P1⇧⁰} × {r. ✓(r) ∈ P2⇧⁰}. (Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
    by (simp flip: GlobalNdet_sets_commute[of ‹{r. ✓(r) ∈ P1⇧⁰}›] add: GlobalNdet_cartprod)
  also from that have ‹... = ?rhs›
    by (subst (2) SKIPS_FD_iff[OF that(1)], subst (2) SKIPS_FD_iff[OF that(2)])
      (simp add: Sync⇩_P⇩_a⇩_i⇩_r.SKIPS_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_SKIPS Sync⇩_P⇩_a⇩_i⇩_r_tj_def Seq⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_right)
  finally show ‹?lhs = ?rhs› .
qed




lemma together_lhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma :
  ‹Synchro⇩_p⇩_t⇩_i⇩_c⇩_k.Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) (P1 ❙;⇩_✓ Q1) S (P2 ❙;⇩_✓ Q2) =
   (P1 ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ❙;⇩_✓ (λ(r1, r2). Synchro⇩_p⇩_t⇩_i⇩_c⇩_k.Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) (Q1 r1) S (Q2 r2))›
  (is ‹?lhs = ?rhs›)
  if ‹P1⇧⁰ ⊆ ev ` S› ‹P2⇧⁰ ⊆ ev ` S›
    ‹⋀a. ev a ∈ P1⇧⁰ ⟹ ev a ∈ P2⇧⁰ ⟹
      Synchro⇩_p⇩_t⇩_i⇩_c⇩_k.Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) (After.After (λP a. STOP) P1 a ❙;⇩_✓ Q1) S (After.After (λP a. STOP) P2 a ❙;⇩_✓ Q2) =
     (After.After (λP a. STOP) P1 a ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r After.After (λP a. STOP) P2 a) ❙;⇩_✓ (λ(r1, r2). Synchro⇩_p⇩_t⇩_i⇩_c⇩_k.Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) (Q1 r1) S (Q2 r2))›
    ‹Synchro⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓)›
  for tj :: ‹'r ⇒ 's ⇒ 't option› (infixl ‹⊗✓› 100)
proof -
  interpret Synchro⇩_p⇩_t⇩_i⇩_c⇩_k ‹(⊗✓)› by (fact that(4))

  from that(1, 2) have non_BOT : ‹P1 ≠ ⊥› ‹P2 ≠ ⊥›
    and non_initial_tick_P : ‹✓(r1) ∉ P1⇧⁰› ‹✓(r2) ∉ P2⇧⁰› for r1 r2 by auto
  hence no_singl_tick_T_P : ‹¬ [✓(r1)] ∈ 𝒯 P1› ‹¬ [✓(r2)] ∈ 𝒯 P2› for r1 r2
    by (auto simp add: initials_def)
  show ‹?lhs = ?rhs›
  proof (rule After.Process_eq_AfterI[where Ψ = ‹λP a. STOP›])
    from non_BOT show ‹?lhs = ⊥ ⟷ ?rhs = ⊥›
      by (simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_is_BOT_iff Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_is_BOT_iff)
        (auto simp add: BOT_iff_Nil_D Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs
          Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs no_singl_tick_T_P Cons_eq_append_conv
          dest: Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k elim!: Cons_tick_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE)
  next
    from non_initial_tick_P non_BOT show ‹?lhs ≠ ⊥ ⟹ ?rhs ≠ ⊥ ⟹ ?lhs⇧⁰ = ?rhs⇧⁰›
      by (simp add: initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k Sync⇩_p⇩_t⇩_i⇩_c⇩_k_is_BOT_iff initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_is_BOT_iff)
        (auto simp add: BOT_iff_Nil_D Sync⇩_P⇩_a⇩_i⇩_r.initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
  next
    show ‹ℛ ?lhs = ℛ ?rhs› if ‹?lhs ≠ ⊥› ‹?rhs ≠ ⊥›
    proof (intro set_eqI iffI)
      fix X assume ‹X ∈ ℛ ?lhs›
      with ‹?lhs ≠ ⊥› obtain X1 X2
        where * : ‹X1 ∈ ℛ (P1 ❙;⇩_✓ Q1)› ‹X2 ∈ ℛ (P2 ❙;⇩_✓ Q2)›
          ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) X1 S X2›
        by (auto simp add: Refusals_def_bis BOT_iff_Nil_D Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs dest: Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k)
      from "*"(1, 2) non_BOT have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1 ∈ ℛ P1› ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2 ∈ ℛ P2›
        by (simp_all add: Refusals_def_bis Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs no_singl_tick_T_P BOT_iff_Nil_D)
      moreover have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k Sync⇩_P⇩_a⇩_i⇩_r_tj (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1) S (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2)›
        (is ‹?S1 ⊆ ?S2›)
      proof (rule subsetI)
        show ‹e ∈ ?S1 ⟹ e ∈ ?S2› for e
          using "*"(3)[THEN set_mp, of ‹ev (of_ev e)›]
          by (cases e, auto simp add: subset_iff ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_def image_iff) force+
      qed
      ultimately have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X ∈ ℛ (P1 ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
        by (fastforce simp add: Refusals_def_bis Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
      thus ‹X ∈ ℛ ?rhs› by (simp add: Refusals_def_bis Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
    next
      fix X assume ‹X ∈ ℛ ?rhs›
      with non_BOT have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X ∈ ℛ (P1 ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
        by (auto simp add: Refusals_def_bis Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs no_singl_tick_T_P BOT_iff_Nil_D Cons_eq_append_conv
            elim!: Cons_tick_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE dest!: Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k)
      with non_BOT obtain X1 X2 where ‹X1 ∈ ℛ P1› ‹X2 ∈ ℛ P2›
        and * : ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k Sync⇩_P⇩_a⇩_i⇩_r_tj X1 S X2›
        by (auto simp add: Refusals_def_bis Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs BOT_iff_Nil_D dest: Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k)
      have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1 ∈ ℛ (P1 ❙;⇩_✓ Q1)›
      proof -
        from ‹X1 ∈ ℛ P1› have ‹X1 ∪ range tick ∈ ℛ P1›
          by (auto simp add: Refusals_def_bis no_singl_tick_T_P dest: F_T intro!: is_processT5)
        also have ‹X1 ∪ range tick = ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1 :: ('a, 'r) refusal⇩_p⇩_t⇩_i⇩_c⇩_k)›
        proof (rule set_eqI)
          show ‹e ∈ X1 ∪ range tick ⟷ e ∈ ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1)› for e
            by (cases e; force simp add: ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def image_iff)
        qed
        finally have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1 :: ('a, 'r) refusal⇩_p⇩_t⇩_i⇩_c⇩_k) ∈ ℛ P1›
          by (simp add: Refusals_def_bis Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
        thus ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1 ∈ ℛ (P1 ❙;⇩_✓ Q1)›
          by (simp add: Refusals_def_bis Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
      qed
      moreover have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2 ∈ ℛ (P2 ❙;⇩_✓ Q2)›
      proof -
        from ‹X2 ∈ ℛ P2› have ‹X2 ∪ range tick ∈ ℛ P2›
          by (auto simp add: Refusals_def_bis no_singl_tick_T_P dest: F_T intro!: is_processT5)
        also have ‹X2 ∪ range tick = ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2 :: ('a, 's) refusal⇩_p⇩_t⇩_i⇩_c⇩_k)›
        proof (rule set_eqI)
          show ‹e ∈ X2 ∪ range tick ⟷ e ∈ ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2)› for e
            by (cases e; force simp add: ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def image_iff)
        qed
        finally have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2 :: ('a, 's) refusal⇩_p⇩_t⇩_i⇩_c⇩_k) ∈ ℛ P2›
          by (simp add: Refusals_def_bis Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
        thus ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2 ∈ ℛ (P2 ❙;⇩_✓ Q2)›
          by (simp add: Refusals_def_bis Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
      qed
      moreover have ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1) S (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2)›
      proof (rule subsetI)
        show ‹e ∈ X ⟹ e ∈ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1) S (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2)› for e
          using "*"[THEN set_mp, of ‹ev (of_ev e)›]
          by (cases e, simp_all add: subset_iff ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_def image_iff )
            (metis IntI event⇩_p⇩_t⇩_i⇩_c⇩_k.sel(1) rangeI, blast)
      qed
      ultimately show ‹X ∈ ℛ ?lhs›
        by (fastforce simp add: Refusals_def_bis Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
    qed
  next
    fix a assume ‹?lhs ≠ ⊥› ‹?rhs ≠ ⊥› ‹?lhs⇧⁰ = ?rhs⇧⁰›
    from non_BOT that(1, 2) show ‹ev a ∈ ?lhs⇧⁰ ⟹
        After.After (λP a. STOP) (P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2) a =
        After.After (λP a. STOP) ((P1 ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ❙;⇩_✓ (λ(r1, r2). Q1 r1 ⟦S⟧⇩_✓ Q2 r2)) a›
      apply (auto simp add: After_Synchro⇩_p⇩_t⇩_i⇩_c⇩_k.After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k[where Ψ⇩_p⇩_t⇩_i⇩_c⇩_k = ‹λP a. STOP› and Ψ⇩_l⇩_h⇩_s = ‹λP a. STOP› and Ψ⇩_r⇩_h⇩_s = ‹λP a. STOP›] BOT_iff_Nil_D Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs no_singl_tick_T_P initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k non_initial_tick_P After_Synchro⇩_p⇩_t⇩_i⇩_c⇩_k.intro Synchro⇩_p⇩_t⇩_i⇩_c⇩_k_axioms)
      apply (simp add: AfterDuplicated_same_events.After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[where Ψ⇩_α = ‹λP a. STOP› and Ψ⇩_β = ‹λP a. STOP›] non_initial_tick_P Sync⇩_P⇩_a⇩_i⇩_r.initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k BOT_iff_Nil_D)
      apply (auto simp add: After_Synchro⇩_p⇩_t⇩_i⇩_c⇩_k.After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k[where Ψ⇩_p⇩_t⇩_i⇩_c⇩_k = ‹λP a. STOP› and Ψ⇩_l⇩_h⇩_s = ‹λP a. STOP› and Ψ⇩_r⇩_h⇩_s = ‹λP a. STOP›] BOT_iff_Nil_D Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k After_Synchro⇩_p⇩_t⇩_i⇩_c⇩_k.intro Sync⇩_P⇩_a⇩_i⇩_r.Synchro⇩_p⇩_t⇩_i⇩_c⇩_k_axioms)
      using that(3) by auto
  qed
qed



theorem (in Synchro⇩_p⇩_t⇩_i⇩_c⇩_k) together_lhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2 = (P1 ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ❙;⇩_✓ (λ(r1, r2). (Q1 r1 ⟦S⟧⇩_✓ Q2 r2))›
  (is ‹?lhs = ?rhs›) if ‹A ⊆ S›
  ‹((λ X. (⊓a ∈ A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D P1›
  ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D P2›
  using that(2, 3)
proof (induct i arbitrary: P1 P2)
  case 0 thus ?case by (simp add: SKIPS_UNIV_FD_lhs_imp_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Seq⇩_p⇩_t⇩_i⇩_c⇩_k)
next
  case (Suc i)
  from Suc.prems[THEN anti_mono_initials_FD] ‹A ⊆ S›
  have ‹P1⇧⁰ ⊆ ev ` A› ‹P2⇧⁰ ⊆ ev ` A› ‹P1⇧⁰ ⊆ ev ` S› ‹P2⇧⁰ ⊆ ev ` S›
    by (auto simp add: subset_iff initials_Ndet initials_Mndetprefix)
  from Suc.prems have * : ‹(⊓a ∈ A → ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV)) ⊓ STOP ⊑⇩_F⇩_D P1›
    ‹(⊓a ∈ A → ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV)) ⊓ STOP ⊑⇩_F⇩_D P2› by simp_all
  have ‹ev a ∈ P1⇧⁰ ⟹ ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D After.After (λP a. STOP) P1 a›
    ‹ev a ∈ P2⇧⁰ ⟹ ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D After.After (λP a. STOP) P2 a› for a
    using "*"[THEN After.mono_After_FD[where a = a and Ψ = ‹λP a. STOP›, rotated]] ‹P1⇧⁰ ⊆ ev ` A› ‹P2⇧⁰ ⊆ ev ` A›
    by (auto simp add: After.After_Ndet initials_Mndetprefix After.After_Mndetprefix subset_iff image_iff split: if_splits)    
  from Suc.hyps[OF this] have ‹ev a ∈ P1⇧⁰ ⟹ ev a ∈ P2⇧⁰ ⟹
    After.After (λP a. STOP) P1 a ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ After.After (λP a. STOP) P2 a ❙;⇩_✓ Q2 =
    (After.After (λP a. STOP) P1 a ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r After.After (λP a. STOP) P2 a) ❙;⇩_✓ (λ(r1, r2). Q1 r1 ⟦S⟧⇩_✓ Q2 r2)› for a .
  from together_lhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma[OF ‹P1⇧⁰ ⊆ ev ` S› ‹P2⇧⁰ ⊆ ev ` S› this Synchro⇩_p⇩_t⇩_i⇩_c⇩_k_axioms]
  show ‹P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2 = (P1 ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ❙;⇩_✓ (λ(r1, r2). Q1 r1 ⟦S⟧⇩_✓ Q2 r2)› .
qed


hide_fact together_lhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma

lemma ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) Q ⊑⇩_F⇩_D P›
  if ‹((λX. ⊓a∈A → X) ^^ i) Q ⊑⇩_F⇩_D P›
    (* so we are weakening the assumption *)
proof -
  have ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) Q ⊑⇩_F⇩_D ((λX. ⊓a∈A → X) ^^ i) Q›
    by (induct i, simp_all)
      (meson Ndet_FD_self_left mono_Mndetprefix_FD order_trans)
  with that trans_FD show ?thesis by blast
qed



corollary (in Synchro⇩_p⇩_t⇩_i⇩_c⇩_k) together_lhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_through_Sync⇩_R⇩_l⇩_i⇩_s⇩_t :
  ‹P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2 = (P1 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t P2) ❙;⇩_✓ (λrs. Q1 (hd rs) ⟦S⟧⇩_✓ Q2 (tl rs))›
  (is ‹?lhs = ?rhs›) if ‹A ⊆ S›
  ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D P1›
  ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D P2›
proof -
  have * : ‹rs ∈ ❙✓❙s(P1 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t P2) ⟹
           (THE r_s. r_s ∈ ❙✓❙s(P1 ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ∧ rs = fst r_s # snd r_s) = (hd rs, tl rs)› for rs
    find_theorems strict_ticks_of RenamingTick
    by (auto simp flip: Sync⇩_P⇩_a⇩_i⇩_r_to_Sync⇩_R⇩_l⇩_i⇩_s⇩_t simp add: strict_ticks_of_RenamingTick)
  have ‹P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2 = (P1 ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ❙;⇩_✓ (λ(r1, r2). (Q1 r1 ⟦S⟧⇩_✓ Q2 r2))›
    by (fact together_lhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[OF that])
  also have ‹… = (P1 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t P2) ❙;⇩_✓ (λrs. (Q1 (hd rs) ⟦S⟧⇩_✓ Q2 (tl rs)))›
    by (subst inj_on_Renaming_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[of ‹λ(r, s). r # s› _ _ id id, simplified])
      (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r_to_Sync⇩_R⇩_l⇩_i⇩_s⇩_t prod.case_eq_if "*" intro!: inj_onI mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq)
  finally show ‹P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2 = …› .
qed



lemma compower_Sync⇩_P⇩_a⇩_i⇩_r_compower_eq_compower :
  ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r
   ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) = ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV)›
  if ‹A ⊆ S›
proof (induct i)
  case 0 from ‹A ⊆ S› show ?case
    by (simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Ndet_left Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Ndet_right Sync⇩_P⇩_a⇩_i⇩_r.STOP_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Mndetprefix
        Sync⇩_P⇩_a⇩_i⇩_r.Mndetprefix_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_STOP Sync⇩_P⇩_a⇩_i⇩_r.Mndetprefix_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Mndetprefix_subset Sync⇩_P⇩_a⇩_i⇩_r.SKIPS_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_SKIPS)
next
  case (Suc i) with ‹A ⊆ S› show ?case
    apply (simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Ndet_left Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Ndet_right Sync⇩_P⇩_a⇩_i⇩_r.STOP_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Mndetprefix
        Sync⇩_P⇩_a⇩_i⇩_r.Mndetprefix_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_STOP Sync⇩_P⇩_a⇩_i⇩_r.Mndetprefix_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Mndetprefix_subset)
    apply (simp add: subset_iff)
    apply safe
       apply auto
      apply (simp add: Ndet_aci(4) Ndet_commute mono_Ndet_FD mono_write0_FD)
     apply (simp add: Int_absorb2 that(1))
    by (metis (no_types, lifting) Mndetprefix_empty Ndet_assoc Ndet_id diff_shunt that(1))
qed

lemma compower_FD_compower_Sync⇩_R⇩_l⇩_i⇩_s⇩_t_compower_FD :
  ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D
   ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t
   ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV)›
  if ‹A ⊆ S›
proof -
  have ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS (UNIV - {[]}))›
    by (induct i)
      (auto simp add: mono_Mndetprefix_FD mono_Ndet_FD SKIPS_FD_SKIPS_iff)
  also have ‹… = RenamingTick (((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV)) (λ(r, s). r # s)›
    apply (induct i)
    by (auto simp add: prod.case_eq_if RenamingTick_Ndet RenamingTick_Mndetprefix intro!: arg_cong[where f = SKIPS])
      (metis (lifting) neq_Nil_conv prod.sel(1, 2) rangeI)
  also have ‹… = RenamingTick (((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⟦S⟧⇩_✓⇩_P⇩_a⇩_i⇩_r ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV)) (λ(r, s). r # s)›
    by (fact arg_cong[symmetric, OF compower_Sync⇩_P⇩_a⇩_i⇩_r_compower_eq_compower[OF ‹A ⊆ S›]])
  also have ‹… = ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t
                 ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV)›
    by (metis Sync⇩_P⇩_a⇩_i⇩_r_to_Sync⇩_R⇩_l⇩_i⇩_s⇩_t)
  finally show ?thesis .
qed



lemma compower_FD_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹⟦L ≠ []; ⋀l. l ∈ set L ⟹ ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D P l⟧ ⟹
    ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D ❙⟦S❙⟧⇩_✓ l ∈@ L. P l› if ‹A ⊆ S›
proof (induct L rule: induct_list012)
  case 1 thus ?case by simp
next
  case (2 l1)
  have ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D RenamingTick (((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV)) (λr. [r])›
    by (induct i)
      (simp_all add: SKIPS_FD_SKIPS_iff RenamingTick_Ndet RenamingTick_Mndetprefix mono_Mndetprefix_FD mono_Ndet_FD)
  also from "2.prems"(2) have ‹… ⊑⇩_F⇩_D RenamingTick (P l1) (λr. [r])›
    by (simp add: mono_Renaming_FD)
  finally show ?case by simp
next
  case (3 l1 l2 L)
  show ?case
    by (simp, rule trans_FD[OF compower_FD_compower_Sync⇩_R⇩_l⇩_i⇩_s⇩_t_compower_FD[OF ‹A ⊆ S›]])
      (auto intro!: Sync⇩_R⇩_l⇩_i⇩_s⇩_t.mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_FD "3.hyps"(2) simp add: "3.prems"(2))
qed




theorem together_lhs_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹❙⟦S❙⟧⇩_✓ l ∈@ L. (P l ❙;⇩_✓ Q l) = (❙⟦S❙⟧⇩_✓ l ∈@ L. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip L R. Q l r)›
  (is ‹?lhs = ?rhs›) if ‹A ⊆ S›
  ‹⋀l. l ∈ set L ⟹ ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D P l›
  using that(2)
proof (induct L rule: induct_list012)
  case 1
  show ?case by simp
next
  case (2 l0)
  have ‹❙⟦S❙⟧⇩_✓ l ∈@ [l0]. (P l ❙;⇩_✓ Q l) = RenamingTick (P l0 ❙;⇩_✓ Q l0) (λr. [r])› by simp
  also have ‹… = RenamingTick (P l0) (λr. [r]) ❙;⇩_✓ (λg_r. RenamingTick (Q l0 (THE r. r ∈ ❙✓❙s(P l0) ∧ g_r = [r])) (λr. [r]))›
    by (auto intro: inj_on_Renaming_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[of ‹λr. [r]›] inj_onI)
  also have ‹… = (❙⟦S❙⟧⇩_✓ l ∈@ [l0]. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip [l0] R. Q l r)›
    by (auto intro!: mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq simp add: strict_ticks_of_RenamingTick the_equality)
  finally show ?case .
next
  case (3 l0 l1 L)
  have ‹❙⟦S❙⟧⇩_✓ l ∈@ (l0 # l1 # L). (P l ❙;⇩_✓ Q l) =
        P l0 ❙;⇩_✓ Q l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). (P l ❙;⇩_✓ Q l)› by simp
  also have ‹❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). (P l ❙;⇩_✓ Q l) =
             (❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l1 # L) R. Q l r)›
    by (rule "3.hyps"(2)) (simp add: "3.prems")
  finally have ‹❙⟦S❙⟧⇩_✓ l ∈@ (l0 # l1 # L). (P l ❙;⇩_✓ Q l) =
                P l0 ❙;⇩_✓ Q l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t (❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l1 # L) R. Q l r)› .
  also have ‹… = (P l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l) ❙;⇩_✓
    (λrs. Q l0 (hd rs) ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ (x, y) ∈@ zip (l1 # L) (tl rs). Q x y)›
    by (auto intro!: Sync⇩_R⇩_l⇩_i⇩_s⇩_t.together_lhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_through_Sync⇩_R⇩_l⇩_i⇩_s⇩_t[OF ‹A ⊆ S›, of i]
        compower_FD_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k[OF ‹A ⊆ S›] simp add: "3.prems")

  also have ‹… = (❙⟦S❙⟧⇩_✓ l ∈@ (l0 # l1 # L). P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l0 # l1 # L) R. Q l r)›
  proof (rule mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq)
    show ‹P l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l = ❙⟦S❙⟧⇩_✓ l ∈@ (l0 # l1 # L). P l› by simp
  next
    fix R assume ‹R ∈ ❙✓❙s(P l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l)›
    from is_ticks_length_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k
      [THEN is_ticks_lengthD, of _ _ ‹l0 # l1 # L›, simplified, OF this]
    obtain r0 r1 R' where ‹R = r0 # r1 # R'› by (metis Suc_length_conv)
    thus ‹Q l0 (hd R) ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l1 # L) (tl R). Q l r =
          ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l0 # l1 # L) R. Q l r› by simp
  qed
  finally show ?case .
qed


theorem together_lhs_MultiSync_Seq⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹❙⟦S❙⟧ l ∈# mset L. (P l ❙;⇩_✓ Q l) = (❙⟦S❙⟧⇩_✓ l ∈@ L. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r) ∈# mset (zip L R). Q l r)›
  (is ‹?lhs = ?rhs›) if ‹A ⊆ S›
  ‹⋀l. l ∈ set L ⟹ ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D P l›
  using that(2)
proof (induct L rule: induct_list012)
  case 1
  show ?case by simp
next
  case (2 l0)
  have ‹❙⟦S❙⟧ l ∈# mset [l0]. (P l ❙;⇩_✓ Q l) = P l0 ❙;⇩_✓ Q l0› by simp
  also have ‹… = RenamingTick (P l0) (λr. [r]) ❙;⇩_✓ (λg_r. Q l0 (THE r. r ∈ ❙✓❙s(P l0) ∧ g_r = [r]))›
    by (auto intro: inj_on_Renaming_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[of ‹λr. [r]› _ _ id id, simplified] inj_onI)
  also have ‹… = (❙⟦S❙⟧⇩_✓ l ∈@ [l0]. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r) ∈# mset (zip [l0] R). Q l r)›
    by (auto intro!: mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq simp add: strict_ticks_of_RenamingTick the_equality)
  finally show ?case .
next
  case (3 l0 l1 L)
  have ‹❙⟦S❙⟧ l∈#mset (l0 # l1 # L). (P l ❙;⇩_✓ Q l) =
        P l0 ❙;⇩_✓ Q l0 ⟦S⟧ ❙⟦S❙⟧ l∈#mset (l1 # L). (P l ❙;⇩_✓ Q l)› by simp
  also have ‹❙⟦S❙⟧ l∈#mset (l1 # L). (P l ❙;⇩_✓ Q l) =
        ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r)∈#mset (zip (l1 # L) R). Q l r)›
    by (rule "3.hyps"(2)) (simp add: "3.prems")
  finally have ‹❙⟦S❙⟧ l∈#mset (l0 # l1 # L). (P l ❙;⇩_✓ Q l) =
                    P l0 ❙;⇩_✓ Q l0 ⟦S⟧ ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r)∈#mset (zip (l1 # L) R). Q l r)› .
  also have ‹… = (P l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l) ❙;⇩_✓
                      (λR. Q l0 (hd R) ⟦S⟧ ❙⟦S❙⟧ (l, r)∈#mset (zip (l1 # L) (tl R)). Q l r)›
    by (auto simp flip: Sync⇩_C⇩_l⇩_a⇩_s⇩_s⇩_i⇩_c_is_Sync intro!: Sync⇩_C⇩_l⇩_a⇩_s⇩_s⇩_i⇩_c.together_lhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_through_Sync⇩_R⇩_l⇩_i⇩_s⇩_t[OF ‹A ⊆ S›, of i]
        compower_FD_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k[OF ‹A ⊆ S›] simp add: "3.prems")
  also have ‹… = (❙⟦S❙⟧⇩_✓ l ∈@ (l0 # l1 # L). P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r) ∈# mset (zip (l0 # l1 # L) R). Q l r)›
  proof (rule mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq)
    show ‹P l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l = ❙⟦S❙⟧⇩_✓ l ∈@ (l0 # l1 # L). P l› by simp
  next
    fix R assume ‹R ∈ ❙✓❙s(P l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). P l)›
    from is_ticks_length_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k
      [THEN is_ticks_lengthD, of _ _ ‹l0 # l1 # L›, simplified, OF this]
    obtain r0 r1 R' where ‹R = r0 # r1 # R'› by (metis Suc_length_conv)
    thus ‹Q l0 (hd R) ⟦S⟧ ❙⟦S❙⟧ (l, r)∈#mset (zip (l1 # L) (tl R)). Q l r =
          ❙⟦S❙⟧ (l, r)∈#mset (zip (l0 # l1 # L) R). Q l r› by simp
  qed
  finally show ?case .
qed




lemma ‹SKIPS UNIV ⊓ STOP ⊑⇩_F⇩_D ❙⟦S❙⟧⇩_✓ l ∈@ L. P l \ I›
  if ‹A ⊆ I› ‹I ⊆ S› ‹L ≠ []› ‹⋀l. l ∈ set L ⟹ ((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D P l›
proof -
  have ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) ⊑⇩_F⇩_D ❙⟦S❙⟧⇩_✓ l ∈@ L. P l›
    by (rule compower_FD_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k[OF subset_trans[OF that(1, 2)] that(3, 4)])
  hence ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) \ I ⊑⇩_F⇩_D ❙⟦S❙⟧⇩_✓ l ∈@ L. P l \ I›
    by (fact mono_Hiding_FD)
  also have ‹((λX. (⊓a∈A → X) ⊓ STOP) ^^ i) (SKIPS UNIV) \ I = (if i = 0 then SKIPS UNIV else if A = {} then STOP else SKIPS UNIV ⊓ STOP)›
    by (induct i)
      (simp_all add: Hiding_SKIPS Hiding_Mndetprefix_subset[OF that(1)]
        Hiding_distrib_Ndet Ndet_aci(4) Ndet_commute split: if_split_asm)
  finally have ‹… ⊑⇩_F⇩_D ❙⟦S❙⟧⇩_✓ l ∈@ L. P l \ I› (is ‹?ugly ⊑⇩_F⇩_D _›) .
  also have ‹SKIPS UNIV ⊓ STOP ⊑⇩_F⇩_D ?ugly›
    by (simp add: Ndet_FD_self_left Ndet_FD_self_right)
  finally (trans_FD[rotated]) show ?thesis .
qed


lemma ‹ r ∈ ❙✓❙s(❙|❙|⇩_✓ l∈@L. P l a \ I) ⟹ length r = length L›
  by (meson is_ticks_length_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k is_ticks_length_def strict_ticks_of_Hiding_subset subset_iff)


lemma nonmt2:‹L ≠ [] ⟹ r ∈ ❙✓❙s(❙⟦UNIV❙⟧⇩_✓ l ∈@ L. P l a \ I) ⟹ r ≠ []› for r a L
  by (metis append_eq_append_conv is_ticks_lengthD is_ticks_length_Hiding
      is_ticks_length_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k list.size(3) self_append_conv2)

(* 
lemma length_ge_list_le_conv :
  ‹n ≤ length xs ⟹ xs ≤ ys ⟷ take n xs = take n ys ∧ drop n xs ≤ drop n ys›
  by (smt (verit, ccfv_SIG) Prefix_Order.prefixE append_eq_append_conv_if
          append_take_drop_id le_append le_length_mono length_take min.absorb_iff2 order_subst1)
 *)





section ‹Independent LHS and Waiting RHS›

subsection ‹General Lemmas›

lemma setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendL_waitingD :
  ‹set u1 ⊆ ev ` (- A) ⟹
   t setinterleaves⇩_✓⇘tj⇙ ((u1 @ u2, v), A) ⟹
   ∃t'. t = map (ev ∘ of_ev) u1 @ t' ∧
        t' setinterleaves⇩_✓⇘tj⇙ ((u2, v), A)›
  if ‹v = [] ∨ hd v ∈ ev ` A›
proof (induct u1 arbitrary: t)
  case Nil from Nil.prems(2) show ?case by simp
next
  case (Cons e u1)
  from Cons.prems(1) obtain a
    where ‹e = ev a› ‹a ∉ A› ‹set u1 ⊆ ev ` (- A)› by auto
  from Cons.prems(2) that obtain t'
    where ‹t = ev a # t'› ‹t' setinterleaves⇩_✓⇘tj⇙ ((u1 @ u2, v), A)›
    by (cases v)
      (auto simp add: setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps ‹e = ev a› ‹a ∉ A› comp_def image_iff
        split: event⇩_p⇩_t⇩_i⇩_c⇩_k.split_asm if_split_asm)
  from Cons.hyps[OF ‹set u1 ⊆ ev ` (- A)› this(2)] obtain t''
    where  ‹t = map (ev ∘ of_ev) (e # u1) @ t''›
      ‹t'' setinterleaves⇩_✓⇘tj⇙ ((u2, v), A)›
    by (auto simp add: ‹e = ev a› ‹t = ev a # t'›)
  thus ?case by blast
qed

corollary setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendR_waitingD :
  ‹u = [] ∨ hd u ∈ ev ` A ⟹ set v1 ⊆ ev ` (- A) ⟹
   t setinterleaves⇩_✓⇘tj⇙ ((u, v1 @ v2), A) ⟹
   ∃t'. t = map (ev ∘ of_ev) v1 @ t' ∧ t' setinterleaves⇩_✓⇘tj⇙ ((u, v2), A)›
  by (subst setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_dual, subst (asm) setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_dual)
    (rule setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendL_waitingD)



lemma ‹set u1 ⊆ ev ` (- S) ⟹ set u1 ∩ ev ` S = {}› by blast


lemma setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendLR_waitingD :
  ‹⟦set u1 ∩ ev ` S = {}; set u2 ∩ ev ` S = {};
   t setinterleaves⇩_✓⇘tj⇙ ((u1 @ v1, u2 @ v2), S)⟧ ⟹
   ∃u v. t = u @ v ∧ u setinterleaves⇩_✓⇘tj⇙ ((u1, u2), S) ∧
                     v setinterleaves⇩_✓⇘tj⇙ ((v1, v2), S)›
  if ‹v1 = [] ∨ hd v1 ∈ ev ` S› ‹v2 = [] ∨ hd v2 ∈ ev ` S›
proof (induct ‹(tj, u1, S, u2)› arbitrary: t u1 u2)
  case Nil_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_Nil
  thus ?case by simp
next
  case (ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_Nil a1 u1)
  from ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_Nil.prems(1) have ‹a1 ∉ S› by (simp add: image_iff)
  with ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_Nil.prems(1, 3) that(2) obtain t'
    where ‹t = ev a1 # t'› ‹t' setinterleaves⇩_✓⇘tj⇙ ((u1 @ v1, [] @ v2), S)› ‹set u1 ∩ ev ` S = {}›
    by (cases v2) (auto simp add: setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps)
  from ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_Nil.hyps[OF ‹a1 ∉ S› this(3) _ this(2)] obtain u v
    where * : ‹t' = u @ v› ‹u setinterleaves⇩_✓⇘tj⇙ ((u1, []), S)›
      ‹v setinterleaves⇩_✓⇘tj⇙ ((v1, v2), S)› by auto
  from "*"(1, 2) have ‹t = (ev a1 # u) @ v› ‹ev a1 # u setinterleaves⇩_✓⇘tj⇙ ((ev a1 # u1, []), S)›
    by (simp_all add: ‹t = ev a1 # t'› ‹a1 ∉ S›)
  with "*"(3) show ?case by blast
next
  case (tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_Nil r1 u1)
  from tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_Nil.prems(3) that(2) have False by (cases v2) auto
  thus ?case ..
next
  case (Nil_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev a2 u2)
  from Nil_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.prems(2) have ‹a2 ∉ S› by (simp add: image_iff)
  with Nil_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.prems(2, 3) that(1) obtain t'
    where ‹t = ev a2 # t'› ‹t' setinterleaves⇩_✓⇘tj⇙ (([] @ v1, u2 @ v2), S)› ‹set u2 ∩ ev ` S = {}›
    by (cases v1) (auto simp add: setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps)
  from Nil_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.hyps[OF ‹a2 ∉ S› _ this(3) this(2)]
  obtain u v where * : ‹t' = u @ v› ‹u setinterleaves⇩_✓⇘tj⇙ (([], u2), S)›
    ‹v setinterleaves⇩_✓⇘tj⇙ ((v1, v2), S)› by auto
  from "*"(1, 2) have ‹t = (ev a2 # u) @ v› ‹ev a2 # u setinterleaves⇩_✓⇘tj⇙ (([], ev a2 # u2), S)›
    by (simp_all add: ‹t = ev a2 # t'› ‹a2 ∉ S›)
  with "*"(3) show ?case by blast
next
  case (Nil_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick r2 u2)
  from Nil_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick.prems(3) that(1) have False by (cases v1) auto
  thus ?case ..
next
  case (ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev a1 u1 a2 u2)
  from ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.prems(1, 2)
  have * : ‹a1 ∉ S› ‹a2 ∉ S› ‹set u1 ∩ ev ` S = {}› ‹set u2 ∩ ev ` S = {}› by auto
  from ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.prems(3)
  consider (mvL) t' where ‹t = ev a1 # t'› ‹t' setinterleaves⇩_✓⇘tj⇙ ((u1 @ v1, (ev a2 # u2) @ v2), S)›
    | (mvR) t' where ‹t = ev a2 # t'› ‹t' setinterleaves⇩_✓⇘tj⇙ (((ev a1 # u1) @ v1, u2 @ v2), S)›
    by (auto simp add: "*"(1, 2))
  thus ?case
  proof cases
    case mvL
    from ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.hyps(4)
      [OF "*"(1, 2) "*"(3) ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.prems(2) mvL(2)] obtain u v
      where ** : ‹t' = u @ v› ‹u setinterleaves⇩_✓⇘tj⇙ ((u1, ev a2 # u2), S)›
        ‹v setinterleaves⇩_✓⇘tj⇙ ((v1, v2), S)› by blast
    have ‹t = (ev a1 # u) @ v› ‹ev a1 # u setinterleaves⇩_✓⇘tj⇙ ((ev a1 # u1, ev a2 # u2), S)›
      by (simp_all add: mvL(1) "**"(1, 2) "*"(1))
    with "**"(3) show ?thesis by blast
  next
    case mvR
    from ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.hyps(5)
      [OF "*"(1, 2) ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.prems(1) "*"(4) mvR(2)] obtain u v
      where ** : ‹t' = u @ v› ‹u setinterleaves⇩_✓⇘tj⇙ ((ev a1 # u1, u2), S)›
        ‹v setinterleaves⇩_✓⇘tj⇙ ((v1, v2), S)› by blast
    have ‹t = (ev a2 # u) @ v› ‹ev a2 # u setinterleaves⇩_✓⇘tj⇙ ((ev a1 # u1, ev a2 # u2), S)›
      by (simp_all add: mvR(1) "**"(1, 2) "*"(2))
    with "**"(3) show ?thesis by blast
  qed
next
  case (ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick a1 u1 r2 u2)
  from ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick.prems(1) have ‹a1 ∉ S› by (simp add: image_iff)
  with ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick.prems(1, 3) obtain t'
    where ‹t = ev a1 # t'› ‹t' setinterleaves⇩_✓⇘tj⇙ ((u1 @ v1, (✓(r2) # u2) @ v2), S)› ‹set u1 ∩ ev ` S = {}›
    by (cases v2) (auto simp add: setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps)
  from ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick.hyps[OF ‹a1 ∉ S› this(3)
      ev_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick.prems(2) this(2)] obtain u v
    where * : ‹t' = u @ v› ‹u setinterleaves⇩_✓⇘tj⇙ ((u1, ✓(r2) # u2), S)›
      ‹v setinterleaves⇩_✓⇘tj⇙ ((v1, v2), S)› by blast
  from "*"(1, 2) have ‹t = (ev a1 # u) @ v› ‹ev a1 # u setinterleaves⇩_✓⇘tj⇙ ((ev a1 # u1, ✓(r2) # u2), S)›
    by (simp_all add: ‹t = ev a1 # t'› ‹a1 ∉ S›)
  with "*"(3) show ?case by blast
next
  case (tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev r1 u1 a2 u2)
  from tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.prems(2) have ‹a2 ∉ S› by (simp add: image_iff)
  with tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.prems(2, 3) obtain t'
    where ‹t = ev a2 # t'› ‹t' setinterleaves⇩_✓⇘tj⇙ (((✓(r1) # u1) @ v1, u2 @ v2), S)› ‹set u2 ∩ ev ` S = {}›
    by (cases v1) (auto simp add: setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps)
  from tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.hyps[OF ‹a2 ∉ S› tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_ev.prems(1) this(3, 2)] obtain u v
    where * : ‹t' = u @ v› ‹u setinterleaves⇩_✓⇘tj⇙ ((✓(r1) # u1, u2), S)›
      ‹v setinterleaves⇩_✓⇘tj⇙ ((v1, v2), S)› by blast
  from "*"(1, 2) have ‹t = (ev a2 # u) @ v› ‹ev a2 # u setinterleaves⇩_✓⇘tj⇙ ((✓(r1) # u1, ev a2 # u2), S)›
    by (simp_all add: ‹t = ev a2 # t'› ‹a2 ∉ S›)
  with "*"(3) show ?case by blast
next
  case (tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick r1 u1 r2 u2)
  from tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick.prems obtain t' r 
    where * : ‹t = ✓(r) # t'› ‹set u1 ∩ ev ` S = {}› ‹set u2 ∩ ev ` S = {}›
      ‹tj r1 r2 = Some r› ‹t' setinterleaves⇩_✓⇘tj⇙ ((u1 @ v1, u2 @ v2), S)›
    by (auto split: option.split_asm)
  from tick_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_tick.hyps[OF "*"(4, 2, 3, 5)] obtain u v
    where ** : ‹t' = u @ v› ‹u setinterleaves⇩_✓⇘tj⇙ ((u1, u2), S)›
      ‹v setinterleaves⇩_✓⇘tj⇙ ((v1, v2), S)› by blast
  have ‹t = (✓(r) # u) @ v› ‹✓(r) # u setinterleaves⇩_✓⇘tj⇙ ((✓(r1) # u1, ✓(r2) # u2), S)›
    by (simp_all add: "*"(1, 4) "**"(1, 2))
  with "**"(3) show ?case by blast
qed




subsection ‹Specific Lemmas›

lemma indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma1 :
  fixes tj :: ‹'r ⇒ 's ⇒ 't option› (infixl ‹⊗✓› 100)
  fixes P1 :: ‹('a, 'r') process⇩_p⇩_t⇩_i⇩_c⇩_k› and P2 :: ‹('a, 's') process⇩_p⇩_t⇩_i⇩_c⇩_k›
  assumes ‹α(P1) ∩ S = {}› ‹α(P2) ∩ S = {}›
    ‹⋀r1. r1 ∈ ❙✓❙s(P1) ⟹ (Q1 r1)⇧⁰ ⊆ ev ` S›
    ‹⋀r2. r2 ∈ ❙✓❙s(P2) ⟹ (Q2 r2)⇧⁰ ⊆ ev ` S›
    ‹tF t› ‹t setinterleaves⇩_✓⇘(⊗✓)⇙ ((t1, t2), S)›
    ‹t1 ∈ 𝒟 (P1 ❙;⇩_✓ Q1)› ‹t2 ∈ 𝒯 (P2 ❙;⇩_✓ Q2)›
    ‹Synchro⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓)›
  shows ‹t ∈ 𝒟 ((P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ❙;⇩_✓ (λ(r1, r2). Synchro⇩_p⇩_t⇩_i⇩_c⇩_k.Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) (Q1 r1) S (Q2 r2)))› (is ‹t ∈ 𝒟 ?rhs›)
proof -
  interpret Synchro⇩_p⇩_t⇩_i⇩_c⇩_k ‹(⊗✓)› by (fact assms(9))

  let ?map = ‹map (ev ∘ of_ev)›
  have $ : ‹t setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((t1, t2), {})›
    if ‹tF t› ‹tF t1› ‹tF t2› ‹t1 ∈ 𝒯 P1› ‹t2 ∈ 𝒯 P2›
      ‹?map t setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map t1, ?map t2), S)› for t t1 t2
  proof -
    from that(4, 5) ‹α(P1) ∩ S = {}› ‹α(P2) ∩ S = {}›
    have ‹{a. ev a ∈ set t1 ∨ ev a ∈ set t2} ⊆ - S›
      by (auto intro: events_of_memI)
    with that(2, 3)[THEN tF_map_ev_of_ev_eq_imp_ev_mem_iff]
    have ‹{a. ev a ∈ set (?map t1) ∨ ev a ∈ set (?map t2)} ⊆ - S› by blast
    from setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_is_restrictable_on_superset_events_of
      [OF this, of _ _ S, unfolded Compl_disjoint, THEN iffD1, OF that(6)]
    have ‹?map t setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map t1, ?map t2), {})› .
    thus ‹t setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((t1, t2), {})›
      by (fact tF_imp_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_map_ev_of_ev_iff[OF that(1-3), THEN iffD1])
  qed

  from assms(7) consider (D_P1) u1 v1 where ‹t1 = ?map u1 @ v1› ‹u1 ∈ 𝒟 P1› ‹tF u1› ‹ftF v1›
    | (D_Q1) u1 r1 v1 where ‹t1 = ?map u1 @ v1› ‹u1 @ [✓(r1)] ∈ 𝒯 P1› ‹u1 @ [✓(r1)] ∉ 𝒟 P1› ‹tF u1› ‹v1 ∈ 𝒟 (Q1 r1)›
    by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis D_imp_ftF is_processT9)
  thus ‹t ∈ 𝒟 ?rhs›
  proof cases
    case D_P1
    from assms(8) consider (T_P2) u2 where ‹t2 = ?map u2› ‹u2 ∈ 𝒯 P2› ‹tF u2›
      | (T_Q2) u2 r2 v2 where ‹t2 = ?map u2 @ v2› ‹u2 @ [✓(r2)] ∈ 𝒯 P2› ‹u2 @ [✓(r2)] ∉ 𝒟 P2› ‹tF u2› ‹v2 ∈ 𝒯 (Q2 r2)›
      | (D_P2) u2 v2 where ‹t2 = ?map u2 @ v2› ‹u2 ∈ 𝒟 P2› ‹tF u2› ‹ftF v2›
      by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis (no_types) T_imp_ftF is_processT9)
    thus ‹t ∈ 𝒟 ?rhs›
    proof cases
      case T_P2
      from assms(6)[unfolded D_P1(1) T_P2(1), THEN setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendL]
      obtain u v u2' u2''
        where * : ‹t = u @ v› ‹u2 = u2' @ u2''›
          ‹u setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1, ?map u2'), S)›
          ‹v setinterleaves⇩_✓⇘(⊗✓)⇙ ((v1, ?map u2''), S)›
        by (auto simp add: map_eq_append_conv)
      have ‹tF u› by (metis assms(5) "*"(1) tF_append_iff)
      then obtain u' :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF u'› ‹u = ?map u'›
        using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
      from T_P2(2, 3) have ‹tF u1› ‹tF u2'› ‹u1 ∈ 𝒯 P1› ‹u2' ∈ 𝒯 P2›
        by (auto simp add: D_P1(2, 3) "*"(2) intro: D_T is_processT3_TR_append) 
      from "$"[OF ‹tF u'› this "*"(3)[unfolded ‹u = ?map u'›]]
      have ‹u' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2'), {})› .
      with D_P1(2) ‹tF u'› ‹u2' ∈ 𝒯 P2› have ‹u' ∈ 𝒟 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
        by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs intro: ftF_Nil)
      with ‹tF u'› assms(5) ‹tF u'› show ‹t ∈ 𝒟 ?rhs›
        by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs "*"(1) ‹u = ?map u'› intro: tF_imp_ftF)
    next
      case T_Q2
      from assms(6)[unfolded D_P1(1) T_Q2(1)]
      consider (waitL) t' t'' t''' u1' u1'' v2' v2''
        where ‹t = t' @ t'' @ t'''› ‹u1 = u1' @ u1''› ‹v2 = v2' @ v2''›
          ‹t' setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1', ?map u2), S)›
          ‹t'' setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1'', v2'), S)›
        | (waitR) t' t'' t''' v1' v1'' u2' u2''
        where ‹t = t' @ t'' @ t'''› ‹v1 = v1' @ v1''› ‹u2 = u2' @ u2''›
          ‹t' setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1, ?map u2'), S)›
        by (auto simp add: append_eq_append_conv2 map_eq_append_conv
            dest!: setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendL setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendR)
          (use waitL in blast, use waitR in blast)
      thus ‹t ∈ 𝒟 ?rhs›
      proof cases
        case waitL
        have ‹tF t'› by (metis assms(5) waitL(1) tF_append_iff)
        then obtain t''' :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF t'''› ‹t' = ?map t'''›
          using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
        have ‹u1' ∈ 𝒯 P1› by (metis D_P1(2) waitL(2) is_processT3_TR_append D_T)
        have ‹tF u1'› by (metis D_P1(3) waitL(2) tF_append_iff)
        from "$"[OF ‹tF t'''› ‹tF u1'› T_Q2(4) ‹u1' ∈ 𝒯 P1›
            T_Q2(2)[THEN is_processT3_TR_append] waitL(4)[unfolded ‹t' = ?map t'''›]]
        have * : ‹t''' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1', u2), {})› .
        have ‹r2 ∈ ❙✓❙s(P2)› by (meson T_Q2(2, 3) strict_ticks_of_memI)
        from assms(1) assms(4)[OF ‹r2 ∈ ❙✓❙s(P2)›] T_Q2(5) D_P1(2)[THEN D_T] D_P1(3)
        have ‹v2' = [] ∨ hd v2' ∈ ev ` S› ‹set (?map u1'') ⊆ ev ` (- S)›
          by (simp_all add: waitL(2, 3) subset_iff image_iff disjoint_iff events_of_def)
            (metis initials_memI is_processT3_TR_append list.exhaust list.sel(1),
              metis (no_types) ComplI append.assoc event⇩_p⇩_t⇩_i⇩_c⇩_k.collapse(1)
              in_set_conv_decomp tF_Cons_iff tF_append_iff)
        from setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendL_waitingD[OF this, of _ _ ‹[]›, simplified, OF waitL(5)] this(1)
        have ‹t'' = ?map u1''›
          by (cases v2') (simp_all add: image_iff setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps split: event⇩_p⇩_t⇩_i⇩_c⇩_k.split_asm)
        have ‹tF (t''' @ ?map u1'')› by (simp add: ‹tF t'''›)
        have ‹t''' @ ?map u1'' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2), {})›
          by (unfold waitL(2), rule tF_disjoint_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_append_tailL)
            (metis D_P1(3) waitL(2) tF_append_iff, simp, fact "*")
        with D_P1(2) T_Q2(2)[THEN is_processT3_TR_append] ‹tF (t''' @ ?map u1'')›
        have ‹t''' @ ?map u1'' ∈ 𝒟 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
          by (simp (no_asm) add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (use ftF_Nil in blast)
        moreover have ‹t' @ t'' = ?map (t''' @ ?map u1'')›
          by (simp add: ‹t' = ?map t'''› ‹t'' = ?map u1''›)
        ultimately have ‹t' @ t'' ∈ 𝒟 ?rhs›
          by (simp (no_asm) add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
            (metis Nil_is_map_conv ‹tF (t''' @ ?map u1'')› append_Nil2 ftF_map_tick_comp_iff)
        with assms(5) is_processT7 waitL(1) show ‹t ∈ 𝒟 ?rhs› by fastforce
      next
        case waitR
        have ‹tF t'› by (metis assms(5) waitR(1) tF_append_iff)
        then obtain t'' :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF t''› ‹t' = ?map t''›
          using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
        have ‹tF u2'› by (metis T_Q2(4) waitR(3) tF_append_iff)
        have ‹u2' ∈ 𝒯 P2› by (metis waitR(3) T_Q2(2) is_processT3_TR_append)
        from "$"[OF ‹tF t''› D_P1(3) ‹tF u2'› D_P1(2)[THEN D_T] ‹u2' ∈ 𝒯 P2›
            waitR(4)[unfolded ‹t' = ?map t''›]]
        have ‹t'' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2'), {})› .
        with D_P1(2) ‹u2' ∈ 𝒯 P2› ‹tF t''› have ‹t'' ∈ 𝒟 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
          by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs intro: ftF_Nil)
        thus ‹t ∈ 𝒟 ?rhs›
          by (simp add: waitR(1) ‹t' = ?map t''› Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs )
            (metis ‹tF t''› assms(5) tF_append_iff tF_imp_ftF waitR(1))
      qed
    next
      case D_P2
      from setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_le_prefixLR
        [OF assms(6)[unfolded D_P1(1) D_P2(1)] prefixI[OF refl] prefixI[OF refl]]
      consider (leR) t' u2' where ‹t' ≤ t› ‹u2' ≤ u2› ‹t' setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1, ?map u2'), S)›
        |      (leL) t' u1' where ‹t' ≤ t› ‹u1' ≤ u1› ‹t' setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1', ?map u2), S)›
        by (simp add: less_eq_list_def prefix_def map_eq_append_conv) blast
      thus ‹t ∈ 𝒟 ?rhs›
      proof cases
        case leR
        have ‹tF t'› by (metis Prefix_Order.prefixE assms(5) leR(1) tF_append_iff)
        then obtain t'' :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF t''› ‹t' = ?map t''›
          using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
        from "$"[OF ‹tF t''› _ _ _ _ leR(3)[unfolded ‹t' = ?map t''›]] D_P1(2,3) D_P2(2,3) leR(2)
        have ‹t'' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2'), {})›
          by (metis D_T Prefix_Order.prefixE is_processT3_TR tF_append_iff)
        moreover have ‹u2' ∈ 𝒯 P2›
          by (metis leR(2) D_P2(2) is_processT3_TR D_T)
        ultimately have ‹t'' ∈ 𝒟 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
          using D_P1(2) ‹tF t''› by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs intro: ftF_Nil)
        with leR(1) assms(5) show ‹t ∈ 𝒟 ?rhs›
          by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs less_eq_list_def prefix_def ‹t' = ?map t''›)
            (metis ‹t' = map (ev ∘ of_ev) t''› ‹tF t''› tF_imp_ftF)
      next
        case leL
        have ‹tF t'› by (metis Prefix_Order.prefixE assms(5) leL(1) tF_append_iff)
        then obtain t'' :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF t''› ‹t' = ?map t''›
          using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
        from "$"[OF ‹tF t''› _ _ _ _ leL(3)[unfolded ‹t' = ?map t''›]] D_P1(2,3) D_P2(2,3) leL(2)
        have ‹t'' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1', u2), {})› 
          by (metis D_T Prefix_Order.prefixE is_processT3_TR tF_append_iff)
        moreover have ‹u1' ∈ 𝒯 P1›
          by (metis leL(2) D_P1(2) is_processT3_TR D_T)
        ultimately have ‹t'' ∈ 𝒟 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
          using D_P2(2) ‹tF t''› by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs intro: ftF_Nil)
        with leL(1) assms(5) show ‹t ∈ 𝒟 ?rhs›
          by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs less_eq_list_def prefix_def ‹t' = ?map t''›)
            (metis ‹t' = map (ev ∘ of_ev) t''› ‹tF t''› tF_imp_ftF)
      qed
    qed
  next
    case D_Q1
    have ‹r1 ∈ ❙✓❙s(P1)› by (metis D_Q1(2, 3) strict_ticks_of_memI)
    from assms(3)[OF this] D_Q1(5)[THEN D_T]
    have ‹v1 = [] ∨ hd v1 ∈ ev ` S›
      by (cases v1) (auto simp add: initials_def_bis)
    from assms(1) D_Q1(2)[THEN is_processT3_TR_append] D_Q1(4)
    have ‹set (?map u1) ∩ ev ` S = {}›
      by (auto simp add: events_of_def disjoint_iff)
        (metis event⇩_p⇩_t⇩_i⇩_c⇩_k.collapse(1) split_list tF_Cons_iff tF_append_iff)
    from assms(8) consider (T_P2) u2 where ‹t2 = ?map u2› ‹u2 ∈ 𝒯 P2› ‹tF u2›
      | (T_Q2) u2 r2 v2 where ‹t2 = ?map u2 @ v2› ‹u2 @ [✓(r2)] ∈ 𝒯 P2› ‹u2 @ [✓(r2)] ∉ 𝒟 P2› ‹tF u2› ‹v2 ∈ 𝒯 (Q2 r2)›
      | (D_P2) u2 v2 where ‹t2 = ?map u2 @ v2› ‹u2 ∈ 𝒟 P2› ‹tF u2› ‹ftF v2›
      by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis (no_types) T_imp_ftF is_processT9)
    thus ‹t ∈ 𝒟 ?rhs›
    proof cases
      case T_P2
      from D_Q1(4) assms(2) T_P2(2, 3)
      have ‹set (?map u2) ∩ ev ` S = {}›
        by (auto simp add: events_of_def disjoint_iff)
          (metis event⇩_p⇩_t⇩_i⇩_c⇩_k.collapse(1) split_list tF_Cons_iff tF_append_iff)
      from setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendLR_waitingD
        [OF ‹v1 = [] ∨ hd v1 ∈ ev ` S› _ ‹set (?map u1) ∩ ev ` S = {}› this,
          of ‹[]›, simplified, OF assms(6)[unfolded D_Q1(1) T_P2(1)]]
      obtain v where ‹v setinterleaves⇩_✓⇘(⊗✓)⇙ ((v1, []), S)› by blast
      with ‹v1 = [] ∨ hd v1 ∈ ev ` S› have ‹v1 = []› by (cases v1) auto
      with D_Q1(5) have ‹Q1 r1 = ⊥› by (simp add: BOT_iff_Nil_D)
      with assms(3)[OF ‹r1 ∈ ❙✓❙s(P1)›] have False by auto
      thus ‹t ∈ 𝒟 ?rhs› ..
    next
      case T_Q2
      have ‹r2 ∈ ❙✓❙s(P2)› by (meson T_Q2(2,3) strict_ticks_of_memI)
      from assms(4)[OF this] T_Q2(5) have ‹v2 = [] ∨ hd v2 ∈ ev ` S›
        by (cases v2) (auto simp add: initials_def_bis)
      from assms(2) T_Q2(2)[THEN is_processT3_TR_append] T_Q2(4)
      have ‹set (?map u2) ∩ ev ` S = {}›
        by (auto simp add: events_of_def disjoint_iff)
          (metis event⇩_p⇩_t⇩_i⇩_c⇩_k.collapse(1) split_list tF_Cons_iff tF_append_iff)+
      from setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendLR_waitingD
        [OF ‹v1 = [] ∨ hd v1 ∈ ev ` S› ‹v2 = [] ∨ hd v2 ∈ ev ` S›
          ‹set (?map u1) ∩ ev ` S = {}› this assms(6)[unfolded D_Q1(1) T_Q2(1)]]
      obtain u v where * : ‹t = u @ v› ‹u setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1, ?map u2), S)›
        ‹v setinterleaves⇩_✓⇘(⊗✓)⇙ ((v1, v2), S)› by blast
      have ‹tF u› by (metis assms(5) "*"(1) tF_append_iff)
      then obtain u' :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF u'› ‹u = ?map u'›
        using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
      from "$"[OF ‹tF u'› D_Q1(4) T_Q2(4) D_Q1(2)[THEN is_processT3_TR_append]
          T_Q2(2)[THEN is_processT3_TR_append] "*"(2)[unfolded ‹u = ?map u'›]]
      have ‹u' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2), {})› .
      hence ‹u' @ [✓((r1, r2))] setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1 @ [✓(r1)], u2 @ [✓(r2)]), {})›
        by (auto intro: setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_snoc_tick simp add: Sync⇩_P⇩_a⇩_i⇩_r_tj_def)
      with D_Q1(2) T_Q2(2) have ‹u' @ [✓((r1, r2))] ∈ 𝒯 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
        by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
      moreover have ‹v ∈ 𝒟 (Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
        by (simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
          (metis "*"(1, 3) D_Q1(5) T_Q2(5) append.right_neutral
            assms(5) tF_append_iff tF_imp_ftF)
      ultimately show ‹t ∈ 𝒟 ?rhs›
        using ‹tF u'› by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs "*"(1) ‹u = ?map u'›)
    next
      case D_P2
      have ‹α(P2) = UNIV›
        by (metis D_P2(2) empty_iff events_of_is_strict_events_of_or_UNIV)
      with assms(2) have ‹S = {}› by simp
      with ‹v1 = [] ∨ hd v1 ∈ ev ` S› have ‹v1 = []› by simp
      with D_Q1(5) have ‹Q1 r1 = ⊥› by (simp add: BOT_iff_Nil_D)
      with assms(3)[OF ‹r1 ∈ ❙✓❙s(P1)›] have False by auto
      thus ‹t ∈ 𝒟 ?rhs› ..
    qed
  qed
qed




lemma indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma2 :
  fixes P1 :: ‹('a, 'r') process⇩_p⇩_t⇩_i⇩_c⇩_k› and P2 :: ‹('a, 's') process⇩_p⇩_t⇩_i⇩_c⇩_k›
  assumes common_assms : ‹α(P1) ∩ S = {}› ‹α(P2) ∩ S = {}›
    ‹⋀r2. r2 ∈ ❙✓❙s(P2) ⟹ (Q2 r2)⇧⁰ ⊆ ev ` S›
    ‹t setinterleaves⇩_✓⇘tj⇙ ((t1, t2), S)›
    ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tj X1 S X2›
    and t1_assms : ‹t1 = map (ev ∘ of_ev) u1› ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1) ∈ ℱ P1› ‹tF u1›
    and t2_assms : ‹t2 = map (ev ∘ of_ev) u2 @ v2› ‹u2 @ [✓(r2)] ∈ 𝒯 P2› ‹u2 @ [✓(r2)] ∉ 𝒟 P2› ‹(v2, X2) ∈ ℱ (Q2 r2)›
  obtains u where ‹tF u› ‹t = map (ev ∘ of_ev) u› ‹(u, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
proof -
  let ?map = ‹map (ev ∘ of_ev)›
  have * : ‹t setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((t1, t2), {})›
    if ‹tF t› ‹tF t1› ‹tF t2› ‹t1 ∈ 𝒯 P1› ‹t2 ∈ 𝒯 P2›
      ‹?map t setinterleaves⇩_✓⇘tj⇙ ((?map t1, ?map t2), S)› for t t1 t2
  proof -
    from that(4, 5) ‹α(P1) ∩ S = {}› ‹α(P2) ∩ S = {}›
    have ‹{a. ev a ∈ set t1 ∨ ev a ∈ set t2} ⊆ - S›
      by (auto intro: events_of_memI)
    with that(2, 3)[THEN tF_map_ev_of_ev_eq_imp_ev_mem_iff]
    have ‹{a. ev a ∈ set (?map t1) ∨ ev a ∈ set (?map t2)} ⊆ - S› by blast
    from setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_is_restrictable_on_superset_events_of
      [OF this, of _ _ S, unfolded Compl_disjoint, THEN iffD1, OF that(6)]
    have ‹?map t setinterleaves⇩_✓⇘tj⇙ ((?map t1, ?map t2), {})› .
    thus ‹t setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((t1, t2), {})›
      by (fact tF_imp_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_map_ev_of_ev_iff[OF that(1-3), THEN iffD1])
  qed
  from t2_assms(2, 3) have ‹r2 ∈ ❙✓❙s(P2)› by (auto intro: strict_ticks_of_memI)
  have ‹v2 = []›
  proof (rule ccontr)
    assume ‹v2 ≠ []›
    with t2_assms(4)[THEN F_T] common_assms(3)[OF ‹r2 ∈ ❙✓❙s(P2)›]
    obtain a v2' where ‹a ∈ S› ‹v2 = ev a # v2'›
      by (cases v2) (auto simp add: initials_def_bis)
    have ‹ev a ∉ set t1›
      by (metis ‹a ∈ S› common_assms(1) t1_assms(1-3) F_T disjoint_iff
          events_of_memI tF_map_ev_of_ev_eq_imp_ev_mem_iff)
    moreover have ‹ev a ∈ set t2›
      by (simp add: t2_assms(1) ‹v2 = ev a # v2'›)
    ultimately have ‹setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k (tj, t1, S, t2) = {}›
      by (meson ‹a ∈ S› ev_notin_both_sets_imp_empty_setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k)
    with common_assms(4) show False by simp
  qed
  with common_assms(4) t2_assms(1) have ‹tF t›
    using setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_tF_imp tF_map_ev_comp by force
  then obtain u :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF u› ‹t = map (ev ∘ of_ev) u›
    using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
  from "*"[OF this(1) t1_assms(3) t2_assms(2)[THEN append_T_imp_tF]
      t1_assms(2)[THEN F_T] t2_assms(2)[THEN is_processT3_TR_append]
      common_assms(4)[unfolded this(2) t1_assms(1) t2_assms(1) ‹v2 = []›, simplified]]
  have ‹u setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2), {})› by simp
  moreover from common_assms(1) t1_assms(2) have ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1 ∪ ev ` S) ∈ ℱ P1›
    by (auto intro!: is_processT5 dest: F_T simp add: events_of_def disjoint_iff in_set_conv_decomp)
  moreover have ‹(u2, UNIV - {✓(r2)}) ∈ ℱ P2›
    by (simp add: t2_assms(2) is_processT6_TR)
  moreover have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k Sync⇩_P⇩_a⇩_i⇩_r_tj
                                 (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1 ∪ ev ` S) {} (UNIV - {✓(r2)})›
    (is ‹?lhs_ref ⊆ ?rhs_ref›)
  proof (rule subsetI)
    show ‹e ∈ ?lhs_ref ⟹ e ∈ ?rhs_ref› for e
      using common_assms(5)[THEN set_mp, of ‹(ev ∘ of_ev) e›]
      by (cases e) (force simp add: super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_def ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def image_iff)+
  qed
  ultimately have ‹(u, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
    by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs simp add: )
  with ‹tF u› ‹t = map (ev ∘ of_ev) u› that show thesis by blast
qed



subsection ‹The Theorem›

theorem (in Synchro⇩_p⇩_t⇩_i⇩_c⇩_k) indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2 = (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ❙;⇩_✓ (λ(r1, r2). Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
  (is ‹?lhs = ?rhs›) if ‹α(P1) ∩ S = {}› ‹α(P2) ∩ S = {}›
  ‹⋀r1. r1 ∈ ❙✓❙s(P1) ⟹ (Q1 r1)⇧⁰ ⊆ ev ` S›
  ‹⋀r2. r2 ∈ ❙✓❙s(P2) ⟹ (Q2 r2)⇧⁰ ⊆ ev ` S›
for P1 :: ‹('a, 'r') process⇩_p⇩_t⇩_i⇩_c⇩_k› and P2 :: ‹('a, 's') process⇩_p⇩_t⇩_i⇩_c⇩_k›
proof -
  let ?map = ‹map (ev ∘ of_ev)›

  have ‹(P2 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P1) ❙;⇩_✓ (λ(r1, r2). Q2 r1 ⟦S⟧⇩_✓⇩_d⇩_u⇩_a⇩_l Q1 r2) =
        RenamingTick (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2) prod.swap ❙;⇩_✓ (λ(r2, r1). Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
    by (simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_commute Sync⇩_p⇩_t⇩_i⇩_c⇩_k_dual)
  also have ‹… =  RenamingTick (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2) prod.swap ❙;⇩_✓
                   (λg_r. case THE r. r ∈ ❙✓❙s(P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ∧ g_r = prod.swap r of (r1, r2) ⇒ Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
    by (auto intro!: mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq simp add: strict_ticks_of_RenamingTick)
      (metis (mono_tags, lifting) case_prod_conv swap_simp swap_swap the_equality)
  also have ‹… = ?rhs›
    by (subst inj_on_Renaming_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[of prod.swap ‹P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2› _ id id, simplified])
      (auto intro: mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq)
  finally have $ : ‹(P2 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P1) ❙;⇩_✓ (λ(r1, r2). Q2 r1 ⟦S⟧⇩_✓⇩_d⇩_u⇩_a⇩_l Q1 r2) = ?rhs› .

  have $$ : ‹?map t setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map t1, ?map t2), S)›
    if ‹tF t1› ‹tF t2› ‹t1 ∈ 𝒯 P1› ‹t2 ∈ 𝒯 P2›
      ‹t setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((t1, t2), {})› for t t1 t2
  proof -
    from that(3, 4) ‹α(P1) ∩ S = {}› ‹α(P2) ∩ S = {}›
    have ‹{a. ev a ∈ set t1 ∨ ev a ∈ set t2} ⊆ - S›
      by (auto intro: events_of_memI)
    from setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_is_restrictable_on_superset_events_of
      [OF this, of _ _ S, unfolded Compl_disjoint, THEN iffD2, OF that(5)]
    have ‹t setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((t1, t2), S)› .
    thus ‹?map t setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map t1, ?map t2), S)›
      by (blast intro: tF_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_map_ev_of_ev that(1, 2))
  qed

  have $$$ : ‹t setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((t1, t2), {})›
    if ‹tF t› ‹tF t1› ‹tF t2› ‹t1 ∈ 𝒯 P1› ‹t2 ∈ 𝒯 P2›
      ‹?map t setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map t1, ?map t2), S)› for t t1 t2
  proof -
    from that(4, 5) ‹α(P1) ∩ S = {}› ‹α(P2) ∩ S = {}›
    have ‹{a. ev a ∈ set t1 ∨ ev a ∈ set t2} ⊆ - S›
      by (auto intro: events_of_memI)
    with that(2, 3)[THEN tF_map_ev_of_ev_eq_imp_ev_mem_iff]
    have ‹{a. ev a ∈ set (?map t1) ∨ ev a ∈ set (?map t2)} ⊆ - S› by blast
    from setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_is_restrictable_on_superset_events_of
      [OF this, of _ _ S, unfolded Compl_disjoint, THEN iffD1, OF that(6)]
    have ‹?map t setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map t1, ?map t2), {})› .
    thus ‹t setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((t1, t2), {})›
      by (fact tF_imp_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_map_ev_of_ev_iff[OF that(1-3), THEN iffD1])
  qed


  show ‹?lhs = ?rhs›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    then obtain u v t1 t2 where * : ‹t = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves⇩_✓⇘(⊗✓)⇙ ((t1, t2), S)›
      ‹t1 ∈ 𝒟 (P1 ❙;⇩_✓ Q1) ∧ t2 ∈ 𝒯 (P2 ❙;⇩_✓ Q2) ∨ t1 ∈ 𝒯 (P1 ❙;⇩_✓ Q1) ∧ t2 ∈ 𝒟 (P2 ❙;⇩_✓ Q2)›
      unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
    from "*"(5) show ‹t ∈ 𝒟 ?rhs›
    proof (elim disjE conjE)
      assume ‹t1 ∈ 𝒟 (P1 ❙;⇩_✓ Q1)› ‹t2 ∈ 𝒯 (P2 ❙;⇩_✓ Q2)›
      from indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma1
        [OF that "*"(2, 4) this Synchro⇩_p⇩_t⇩_i⇩_c⇩_k_axioms]
      have ‹u ∈ 𝒟 ?rhs› .
      thus ‹t ∈ 𝒟 ?rhs› by (simp add: "*"(1-3) is_processT7)
    next
      assume ‹t1 ∈ 𝒯 (P1 ❙;⇩_✓ Q1)› ‹t2 ∈ 𝒟 (P2 ❙;⇩_✓ Q2)›
      from indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma1
        [OF that(2, 1, 4, 3) "*"(2) setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_dual
          [THEN iffD1, OF "*"(4)] this(2, 1) Synchro⇩_p⇩_t⇩_i⇩_c⇩_k_dual.Synchro⇩_p⇩_t⇩_i⇩_c⇩_k_axioms]
      have ‹u ∈ 𝒟 ?rhs› unfolding "$" .
      thus ‹t ∈ 𝒟 ?rhs› by (simp add: "*"(1-3) is_processT7)
    qed
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then consider (D_P) u v where ‹t = ?map u @ v› ‹u ∈ 𝒟 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)› ‹tF u› ‹ftF v›
      | (D_Q) u v r1 r2 where ‹t = ?map u @ v› ‹u @ [✓((r1, r2))] ∈ 𝒯 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
        ‹u @ [✓((r1, r2))] ∉ 𝒟 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)› ‹tF u› ‹v ∈ 𝒟 (Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
      by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis D_imp_ftF is_processT9)
    thus ‹t ∈ 𝒟 ?lhs›
    proof cases
      case D_P
      from D_P(2) obtain w x w1 w2 where * : ‹u = w @ x› ‹tF w› ‹ftF x›
        ‹w setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((w1, w2), {})›
        ‹w1 ∈ 𝒟 P1 ∧ w2 ∈ 𝒯 P2 ∨ w1 ∈ 𝒯 P1 ∧ w2 ∈ 𝒟 P2›
        unfolding Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
      from tF_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_iff[THEN iffD1, OF "*"(4)]
      have ‹tF w1› ‹tF w2› by (simp_all add: "*"(2))
      from "*"(5) have ‹?map w ∈ 𝒟 ?lhs›
      proof (elim disjE conjE)
        assume ** : ‹w1 ∈ 𝒟 P1› ‹w2 ∈ 𝒯 P2›
        have ‹?map w setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map w1, ?map w2), S)›
          by (simp add: "$$" "*"(4) "**"(1, 2) D_T ‹tF w1› ‹tF w2›)
        moreover have ‹?map w1 ∈ 𝒟 (P1 ❙;⇩_✓ Q1)›
          by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (use "**"(1) ‹tF w1› ftF_Nil in blast)
        moreover have ‹?map w2 ∈ 𝒯 (P2 ❙;⇩_✓ Q2)›
          by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis "**"(2) ‹tF w2›)
        ultimately show ‹?map w ∈ 𝒟 ?lhs›
          by (simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
            (meson ftF_Nil self_append_conv tF_map_ev_comp)
      next
        assume ** : ‹w1 ∈ 𝒯 P1› ‹w2 ∈ 𝒟 P2›
        have ‹?map w setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map w1, ?map w2), S)›
          by (simp add: "$$" "*"(4) "**"(1, 2) D_T ‹tF w1› ‹tF w2›)
        moreover have ‹?map w1 ∈ 𝒯 (P1 ❙;⇩_✓ Q1)›
          by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis "**"(1) ‹tF w1›)
        moreover have ‹?map w2 ∈ 𝒟 (P2 ❙;⇩_✓ Q2)›
          by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (use "**"(2) ‹tF w2› ftF_Nil in blast)
        ultimately show ‹?map w ∈ 𝒟 ?lhs›
          by (simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
            (meson ftF_Nil self_append_conv tF_map_ev_comp)
      qed
      thus ‹t ∈ 𝒟 ?lhs›
        by (simp add: D_P(1, 4) "*"(1) ftF_append is_processT7)
    next
      case D_Q
      from D_Q(2, 3) obtain u1 u2
        where * : ‹u1 @ [✓(r1)] ∈ 𝒯 P1› ‹u2 @ [✓(r2)] ∈ 𝒯 P2›
          ‹u setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2), {})›
        by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs Sync⇩_P⇩_a⇩_i⇩_r_tj_def elim: snoc_tick_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE)
      from D_Q(5) obtain w x w1 w2 where ** : ‹v = w @ x› ‹tF w› ‹ftF x›
        ‹w setinterleaves⇩_✓⇘(⊗✓)⇙ ((w1, w2), S)›
        ‹w1 ∈ 𝒟 (Q1 r1) ∧ w2 ∈ 𝒯 (Q2 r2) ∨ w1 ∈ 𝒯 (Q1 r1) ∧ w2 ∈ 𝒟 (Q2 r2)›
        by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
      have ‹?map u setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1, ?map u2), S)›
        by (metis "$$" "*" append_T_imp_tF is_processT3_TR_append list.distinct(1))
      from setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_append_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k[OF this "**"(4)]
      have ‹?map u @ w setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1 @ w1, ?map u2 @ w2), S)› .
      moreover from "*"(1, 2) "**"(5)
      have ‹?map u1 @ w1 ∈ 𝒟 (P1 ❙;⇩_✓ Q1) ∧ ?map u2 @ w2 ∈ 𝒯 (P2 ❙;⇩_✓ Q2) ∨
            ?map u1 @ w1 ∈ 𝒯 (P1 ❙;⇩_✓ Q1) ∧ ?map u2 @ w2 ∈ 𝒟 (P2 ❙;⇩_✓ Q2)›
        by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis append_T_imp_tF list.discI)
      ultimately have ‹?map u @ w ∈ 𝒟 ?lhs›
        by (simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
          (metis "**"(2) append.right_neutral ftF_Nil
            tF_append_iff tF_map_ev_comp)
      with D_Q(1) "**"(1-3) is_processT7 show ‹t ∈ 𝒟 ?lhs› by force
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
    then obtain t1 t2 X1 X2
      where * : ‹(t1, X1) ∈ ℱ (P1 ❙;⇩_✓ Q1)› ‹(t2, X2) ∈ ℱ (P2 ❙;⇩_✓ Q2)›
        ‹t setinterleaves⇩_✓⇘(⊗✓)⇙ ((t1, t2), S)› ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) X1 S X2›
      by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
    with ‹t ∉ 𝒟 ?lhs› have ‹t1 ∉ 𝒟 (P1 ❙;⇩_✓ Q1)› ‹t2 ∉ 𝒟 (P2 ❙;⇩_✓ Q2)›
      by (auto simp add: D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k' dest!: F_T intro: ftF_Nil)
    note * = "*"(1) this(1) "*"(2) this(2) "*"(3, 4)
    from "*"(1, 2) consider (F_P1) u1 where ‹t1 = ?map u1› ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1) ∈ ℱ P1› ‹u1 ∉ 𝒟 P1› ‹tF u1›
      | (F_Q1) u1 r1 v1 where ‹t1 = ?map u1 @ v1› ‹u1 @ [✓(r1)] ∈ 𝒯 P1› ‹u1 @ [✓(r1)] ∉ 𝒟 P1› ‹tF u1› ‹(v1, X1) ∈ ℱ (Q1 r1)›
      by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis F_imp_ftF is_processT9)
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      case F_P1
      from "*"(3, 4) consider (F_P2) u2 where ‹t2 = ?map u2› ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2) ∈ ℱ P2› ‹u2 ∉ 𝒟 P2› ‹tF u2›
        | (F_Q2) u2 r2 v2 where ‹t2 = ?map u2 @ v2› ‹u2 @ [✓(r2)] ∈ 𝒯 P2› ‹u2 @ [✓(r2)] ∉ 𝒟 P2› ‹tF u2› ‹(v2, X2) ∈ ℱ (Q2 r2)›
        by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis F_imp_ftF is_processT9)
      thus ‹(t, X) ∈ ℱ ?rhs›
      proof cases
        case F_P2
        from "*"(5) F_P2(1) have ‹tF t›
          using setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_tF_imp tF_map_ev_comp by blast
        then obtain u :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF u› ‹t = ?map u›
          using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
        from "$$$"[OF this(1) F_P1(4) F_P2(4) F_P1(2)[THEN F_T] F_P2(2)[THEN F_T]
            "*"(5)[unfolded this(2) F_P1(1) F_P2(1)]]
        have ‹u setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2), {})› .
        moreover from that(1) F_P1(2) have ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1 ∪ ev ` S) ∈ ℱ P1›
          by (auto intro!: is_processT5 dest: F_T simp add: events_of_def disjoint_iff in_set_conv_decomp)
        moreover from that(2) F_P2(2) have ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2 ∪ ev ` S) ∈ ℱ P2›
          by (auto intro!: is_processT5 dest: F_T simp add: events_of_def disjoint_iff in_set_conv_decomp)
        moreover have ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (Sync⇩_P⇩_a⇩_i⇩_r_tj)
                                       (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1 ∪ ev ` S) {} (ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2 ∪ ev ` S)›
          (is ‹?lhs_ref ⊆ ?rhs_ref›)
        proof (rule subsetI)
          show ‹e ∈ ?lhs_ref ⟹ e ∈ ?rhs_ref› for e
            using "*"(6)[THEN set_mp, of ‹(ev ∘ of_ev) e›]
            by (cases e) (force simp add: super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_def ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def image_iff)+
        qed
        ultimately have ‹(u, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
          by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
        with ‹tF u› ‹t = ?map u› show ‹(t, X) ∈ ℱ ?rhs›
          by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
      next
        case F_Q2
        from indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma2
          [of P1 S P2 Q2, OF that(1, 2, 4) "*"(5, 6) F_P1(1, 2, 4) F_Q2(1-3, 5)]
        obtain u where ‹tF u› ‹t = ?map u› ‹(u, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)› by blast
        thus ‹(t, X) ∈ ℱ ?rhs› by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
      qed
    next
      case F_Q1
      from "*"(3, 4) consider (F_P2) u2 where ‹t2 = ?map u2› ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2) ∈ ℱ P2› ‹u2 ∉ 𝒟 P2› ‹tF u2›
        | (F_Q2) u2 r2 v2 where ‹t2 = ?map u2 @ v2› ‹u2 @ [✓(r2)] ∈ 𝒯 P2› ‹u2 @ [✓(r2)] ∉ 𝒟 P2› ‹tF u2› ‹(v2, X2) ∈ ℱ (Q2 r2)›
        by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (metis F_imp_ftF is_processT9)
      thus ‹(t, X) ∈ ℱ ?rhs›
      proof cases
        case F_P2
        have ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (λs r. r ⊗✓ s) X2 S X1›
          by (metis "*"(6) super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_dual)
        from indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma2
          [of P2 S P1 Q1, OF that(2, 1, 3) setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_dual[THEN iffD1, OF "*"(5)]
            this F_P2(1, 2, 4) F_Q1(1, 2, 3, 5)]
        obtain u where ‹tF u› ‹t = ?map u› ‹(u, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ (P2 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P1)› by blast
        hence ‹(t, X) ∈ ℱ ((P2 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P1) ❙;⇩_✓ (λ(r1, r2). Q2 r1 ⟦S⟧⇩_✓⇩_d⇩_u⇩_a⇩_l Q1 r2))›
          by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
        with "$" show ‹(t, X) ∈ ℱ ?rhs› by simp
      next
        case F_Q2
        from F_Q1(2, 3) F_Q2(2, 3) have ‹r1 ∈ ❙✓❙s(P1)› ‹r2 ∈ ❙✓❙s(P2)›
          by (simp_all add: strict_ticks_of_memI)
        from "*"(5)[unfolded F_Q1(1) F_Q2(1)]
        consider (waitL) t' t'' t''' u1' u1'' v2' v2''
          where ‹t = t' @ t'' @ t'''› ‹u1 = u1' @ u1''› ‹v2 = v2' @ v2''›
            ‹t' setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1', ?map u2), S)›
            ‹t'' setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1'', v2'), S)›
            ‹t''' setinterleaves⇩_✓⇘(⊗✓)⇙ ((v1, v2''), S)›
          | (waitR) t' t'' t''' v1' v1'' u2' u2''
          where ‹t = t' @ t'' @ t'''› ‹v1 = v1' @ v1''› ‹u2 = u2' @ u2''›
            ‹t' setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1, ?map u2'), S)›
            ‹t'' setinterleaves⇩_✓⇘(⊗✓)⇙ ((v1', ?map u2''), S)›
            ‹t''' setinterleaves⇩_✓⇘(⊗✓)⇙ ((v1'', v2), S)›
          by (auto simp add: append_eq_append_conv2 map_eq_append_conv
              dest!: setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendL setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendR)
            (use waitL in blast, use waitR in blast)
        thus ‹(t, X) ∈ ℱ ?rhs›
        proof cases
          case waitL
          have ‹tF t'› using setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_tF_imp tF_map_ev_comp waitL(4) by blast
          then obtain t'''' :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF t''''› ‹t' = ?map t''''›
            using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
          have ‹u1' ∈ 𝒯 P1› using F_Q1(2) is_processT3_TR_append waitL(2) by blast
          have ‹tF u1'› by (metis F_Q1(4) waitL(2) tF_append_iff)
          from "$$$"[OF ‹tF t''''› ‹tF u1'› F_Q2(4) ‹u1' ∈ 𝒯 P1›
              F_Q2(2)[THEN is_processT3_TR_append] waitL(4)[unfolded ‹t' = ?map t''''›]]
          have ** : ‹t'''' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1', u2), {})› .
          from that(1) F_Q1(2)[THEN is_processT3_TR_append] F_Q1(4)
          have ‹set (?map u1'') ⊆ ev ` (- S)›
            by (auto simp add: waitL(2) disjoint_iff image_iff events_of_def)
              (metis Un_iff event⇩_p⇩_t⇩_i⇩_c⇩_k.collapse(1) set_append split_list
                tF_Cons_iff tF_append_iff)
          from that(4)[OF ‹r2 ∈ ❙✓❙s(P2)›] F_Q2(5)[THEN F_T]
          have ‹v2' = [] ∨ hd v2' ∈ ev ` S›
            by (cases v2') (auto simp add: waitL(3) initials_def_bis)
          from this waitL(3) setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendL_waitingD
            [OF this ‹set (?map u1'') ⊆ ev ` (- S)›, of _ _ ‹[]›, simplified, OF waitL(5)]
          have *** : ‹t'' = ?map u1'' ∧ v2' = [] ∧ v2'' = v2›
            by (cases v2') (simp_all add: setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps image_iff
                split: event⇩_p⇩_t⇩_i⇩_c⇩_k.split_asm if_split_asm)
          have ‹tF (t'''' @ ?map u1'')› by (simp add: ‹tF t''''›)
          have ‹t'''' @ ?map u1'' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2), {})›
            by (unfold waitL(2), rule tF_disjoint_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_append_tailL)
              (metis F_Q1(4) waitL(2) tF_append_iff, simp, fact "**")
          hence ‹(t'''' @ ?map u1'') @ [✓((r1, r2))] setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1 @ [✓(r1)], u2 @ [✓(r2)]), {})›
            by (rule setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_snoc_tick) (simp add: Sync⇩_P⇩_a⇩_i⇩_r_tj_def)
          with F_Q1(2) F_Q2(2) have ‹(t'''' @ ?map u1'') @ [✓((r1, r2))] ∈ 𝒯 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
            by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
          moreover have ‹t = ?map (t'''' @ ?map u1'') @ t'''›
            by (simp add: waitL(1) ‹t' = ?map t''''› "***")
          moreover from F_Q1(5) F_Q2(5) waitL(6) "*"(6)
          have ‹(t''', X) ∈ ℱ (Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
            by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs "***")
          ultimately show ‹(t, X) ∈ ℱ ?rhs›
            by (simp (no_asm) add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (use ‹tF (t'''' @ ?map u1'')› in blast)
        next
          case waitR
          have ‹tF t'› using setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_tF_imp tF_map_ev_comp waitR(4) by blast
          then obtain t'''' :: ‹('a, 'r' × 's') trace⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹tF t''''› ‹t' = ?map t''''›
            using tF_map_ev_comp tF_map_ev_of_ev_eq_iff by blast
          have ‹u2' ∈ 𝒯 P2› using F_Q2(2) is_processT3_TR_append waitR(3) by blast
          have ‹tF u2'› by (metis F_Q2(4) waitR(3) tF_append_iff)
          from "$$$"[OF ‹tF t''''› F_Q1(4) ‹tF u2'› F_Q1(2)[THEN is_processT3_TR_append]
              ‹u2' ∈ 𝒯 P2› waitR(4)[unfolded ‹t' = ?map t''''›]]
          have ** : ‹t'''' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2'), {})› .
          from that(2) F_Q2(2)[THEN is_processT3_TR_append] F_Q2(4)
          have ‹set (?map u2'') ⊆ ev ` (- S)›
            by (auto simp add: waitR(3) disjoint_iff image_iff events_of_def)
              (metis Un_iff event⇩_p⇩_t⇩_i⇩_c⇩_k.collapse(1) set_append split_list
                tF_Cons_iff tF_append_iff)
          from that(3)[OF ‹r1 ∈ ❙✓❙s(P1)›] F_Q1(5)[THEN F_T]
          have ‹v1' = [] ∨ hd v1' ∈ ev ` S›
            by (cases v1') (auto simp add: waitR(2) initials_def_bis)
          from this waitR(2) setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_appendR_waitingD
            [OF this ‹set (?map u2'') ⊆ ev ` (- S)›, of _ _ ‹[]›, simplified, OF waitR(5)]
          have *** : ‹t'' = ?map u2'' ∧ v1' = [] ∧ v1'' = v1›
            by (cases v1') (simp_all add: setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps image_iff
                split: event⇩_p⇩_t⇩_i⇩_c⇩_k.split_asm if_split_asm)
          have ‹tF (t'''' @ ?map u2'')› by (simp add: ‹tF t''''›)
          have ‹t'''' @ ?map u2'' setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2), {})›
            by (unfold waitR(3), rule tF_disjoint_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_append_tailR)
              (metis F_Q2(4) waitR(3) tF_append_iff, simp, fact "**")
          hence ‹(t'''' @ ?map u2'') @ [✓((r1, r2))] setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1 @ [✓(r1)], u2 @ [✓(r2)]), {})›
            by (rule setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_snoc_tick) (simp add: Sync⇩_P⇩_a⇩_i⇩_r_tj_def)
          with F_Q1(2) F_Q2(2) have ‹(t'''' @ ?map u2'') @ [✓((r1, r2))] ∈ 𝒯 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
            by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
          moreover have ‹t = ?map (t'''' @ ?map u2'') @ t'''›
            by (simp add: waitR(1) ‹t' = ?map t''''› "***")
          moreover from F_Q1(5) F_Q2(5) waitR(6) "*"(6)
          have ‹(t''', X) ∈ ℱ (Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
            by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs "***")
          ultimately show ‹(t, X) ∈ ℱ ?rhs›
            by (simp (no_asm) add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) (use ‹tF (t'''' @ ?map u2'')› in blast)
        qed
      qed
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs› ‹t ∉ 𝒟 ?lhs›
    from this(1, 2) consider (F_1) u where ‹t = ?map u› ‹(u, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
      ‹u ∉ 𝒟 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)› ‹tF u›
    | (F_2) u r1 r2 v where ‹t = ?map u @ v› ‹u @ [✓((r1, r2))] ∈ 𝒯 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
      ‹u @ [✓((r1, r2))] ∉ 𝒟 (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2)›
      ‹tF u› ‹(v, X) ∈ ℱ (Q1 r1 ⟦S⟧⇩_✓ Q2 r2)› ‹v ∉ 𝒟 (Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
      by (simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
        (metis (no_types) F_imp_ftF append_Nil2 ftF_Nil is_processT9)
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      case F_1
      have ‹tF t› by (simp add: F_1(1))
      from F_1(2, 3) obtain u1 u2 X1 X2
        where * : ‹(u1, X1) ∈ ℱ P1› ‹u1 ∉ 𝒟 P1› ‹(u2, X2) ∈ ℱ P2› ‹u2 ∉ 𝒟 P2›
          ‹u setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2), {})›
          ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k Sync⇩_P⇩_a⇩_i⇩_r_tj X1 {} X2›
        by (simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
          (metis (no_types, lifting) F_1(4) F_T append_self_conv ftF_Nil)
      from F_1(4) tF_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_iff[OF "*"(5)] have ‹tF u1› ‹tF u2› by simp_all
      have ** : ‹t setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1, ?map u2), S)›
        by (unfold F_1(1)) (fact "$$"[OF ‹tF u1› ‹tF u2› "*"(1, 3)[THEN F_T] "*"(5)])
      have ‹t @ [✓(r_s)] ∉ 𝒯 ?lhs› for r_s
      proof (rule notI)
        assume ‹t @ [✓(r_s)] ∈ 𝒯 ?lhs›
        from ‹t ∉ 𝒟 ?lhs› have ‹t @ [✓(r_s)] ∉ 𝒟 ?lhs› by (meson is_processT9)
        with ‹tF t› ‹t @ [✓(r_s)] ∈ 𝒯 ?lhs› obtain u1' u2' r1 r2
          where "€" : ‹r1 ⊗✓ r2 = Some r_s› ‹u1' @ [✓(r1)] ∈ 𝒯 (P1 ❙;⇩_✓ Q1)›
            ‹u1' @ [✓(r1)] ∉ 𝒟 (P1 ❙;⇩_✓ Q1)› ‹u2' @ [✓(r2)] ∈ 𝒯 (P2 ❙;⇩_✓ Q2)›
            ‹u2' @ [✓(r2)] ∉ 𝒟 (P2 ❙;⇩_✓ Q2)› ‹t setinterleaves⇩_✓⇘(⊗✓)⇙ ((u1', u2'), S)›
          by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs elim!: snoc_tick_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE)
            (metis (no_types, lifting) ftF_append_iff
              ftF_charn is_processT3_TR_append is_processT9)
        from "€"(2, 3) obtain u1'' r1' v1'
          where "€€" : ‹u1' @ [✓(r1)] = ?map u1'' @ v1'› ‹u1'' @ [✓(r1')] ∈ 𝒯 P1›
            ‹u1'' @ [✓(r1')] ∉ 𝒟 P1› ‹tF u1''› ‹v1' ∈ 𝒯 (Q1 r1')›
          by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs append_eq_map_conv)
            (metis T_imp_ftF is_processT9)
        from "€€"(2, 3) have ‹r1' ∈ ❙✓❙s(P1)› by (metis strict_ticks_of_memI)
        from that(1, 2) "*"(1, 3)[THEN F_T] setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_empty[OF "*"(5)]
        have ‹set u ∩ ev ` S = {}› unfolding events_of_def by blast
        with tF_map_ev_of_ev_eq_imp_ev_mem_iff[OF F_1(4, 1)]
        have ‹set t ∩ ev ` S = {}› by blast
        with setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_ev_in_set_iff[OF "€"(6)]
        have ‹set u1' ∩ ev ` S = {}› by blast
        moreover from that(3)[OF ‹r1' ∈ ❙✓❙s(P1)›] "€€"(5)
        have ‹v1' = [] ∨ hd v1' ∈ ev ` S›
          by (metis in_mono initials_memI list.sel(1) neq_Nil_conv)
        moreover from that(1) "€€"(2)[THEN is_processT3_TR_append] "€€"(4)
        have ‹set (?map u1'') ∩ ev ` S = {}›
          by (auto simp add: events_of_def disjoint_iff)
            (metis event⇩_p⇩_t⇩_i⇩_c⇩_k.collapse(1) split_list_first tF_Cons_iff tF_append_iff)
        ultimately show False
          using "€€"(1) by (cases v1')
            (auto simp add: append_eq_map_conv image_iff
              append_eq_append_conv2 append_eq_Cons_conv Cons_eq_append_conv)
      qed
      moreover have ‹(t, X ∩ range ev) ∈ ℱ ?lhs›
      proof -
        define X1' :: ‹('a, 'r) refusal⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹X1' ≡ {ev a| a. ev a ∈ X1}›
        define X2' :: ‹('a, 's) refusal⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹X2' ≡ {ev a| a. ev a ∈ X2}›
        have "€" : ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1' = X1 ∪ range tick›
        proof (rule set_eqI)
          show ‹e ∈ ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1' ⟷ e ∈ X1 ∪ range tick› for e
            by (cases e) (force simp add: X1'_def ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def image_iff)+
        qed
        have "€€" : ‹ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2' = X2 ∪ range tick›
        proof (rule set_eqI)
          show ‹e ∈ ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2' ⟷ e ∈ X2 ∪ range tick› for e
            by (cases e) (force simp add: X2'_def ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def image_iff)+
        qed
        from "*"(6)[THEN set_mp, of ‹✓(_)›]
        have ‹range tick ⊆ X1 ∨ range tick ⊆ X2›
          by (auto simp add: ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_def Sync⇩_P⇩_a⇩_i⇩_r_tj_def)
        hence ‹X1 = ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1' ∨ X2 = ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2'›
          unfolding "€" "€€" by blast
        with "*"(1, 3) consider ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1') ∈ ℱ P1› ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2') ∈ ℱ P2›
          | ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1') ∉ ℱ P1› ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2') ∈ ℱ P2›
          | ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1') ∈ ℱ P1› ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2') ∉ ℱ P2› by blast
        thus ‹(t, X ∩ range ev) ∈ ℱ ?lhs›
        proof cases
          assume ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1') ∈ ℱ P1› ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2') ∈ ℱ P2›
          with ‹tF u1› ‹tF u2›
          have ‹(?map u1, X1') ∈ ℱ (P1 ❙;⇩_✓ Q1)› ‹(?map u2, X2') ∈ ℱ (P2 ❙;⇩_✓ Q2)›
            by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
          moreover have ‹X ∩ range ev ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) X1' S X2'›
          proof (rule subsetI)
            show ‹e ∈ X ∩ range ev ⟹ e ∈ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) X1' S X2'› for e
              using set_mp[OF "*"(6), of ‹(ev ∘ of_ev) e›]
              by (cases e) (force simp add: super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_def ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def X1'_def X2'_def)+
          qed
          ultimately show ‹(t, X ∩ range ev) ∈ ℱ ?lhs›
            using "**" by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
        next
          assume ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1') ∉ ℱ P1› ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2') ∈ ℱ P2›
          from is_processT5_S7'[OF "*"(1) this(1)[unfolded "€"]]
          obtain r1 where ‹u1 @ [✓(r1)] ∈ 𝒯 P1› by blast
          have ‹r1 ∈ ❙✓❙s(P1)›
            by (meson "*"(2) ‹u1 @ [✓(r1)] ∈ 𝒯 P1› is_processT9 strict_ticks_of_memI)
          with add_Compl_initials_in_R[of ‹{}› ‹Q1 r1›]
          have ‹- ev ` S ∈ ℛ (Q1 r1)›
            by (simp add: Refusals_iff is_processT1) (meson compl_mono is_processT4 that(3))
          with ‹tF u1› ‹tF u2› ‹u1 @ [✓(r1)] ∈ 𝒯 P1› ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2') ∈ ℱ P2›
          have ‹(?map u1, - ev ` S) ∈ ℱ (P1 ❙;⇩_✓ Q1)› ‹(?map u2, X2') ∈ ℱ (P2 ❙;⇩_✓ Q2)›
            by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs Refusals_def_bis)
          moreover have ‹X ∩ range ev ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) (- ev ` S) S X2'›
          proof (rule subsetI)
            show ‹e ∈ X ∩ range ev ⟹ e ∈ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) (- ev ` S) S X2'› for e
              using set_mp[OF "*"(6), of ‹(ev ∘ of_ev) e›]
              by (cases e) (force simp add: super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_def ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def X1'_def X2'_def)+
          qed
          ultimately show ‹(t, X ∩ range ev) ∈ ℱ ?lhs›
            using "**" by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
        next
          fix r2 assume ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1') ∈ ℱ P1› ‹(u2, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X2') ∉ ℱ P2›
          from is_processT5_S7'[OF "*"(3) this(2)[unfolded "€€"]]
          obtain r2 where ‹u2 @ [✓(r2)] ∈ 𝒯 P2› by blast
          have ‹r2 ∈ ❙✓❙s(P2)›
            by (meson "*"(4) ‹u2 @ [✓(r2)] ∈ 𝒯 P2› is_processT9 strict_ticks_of_memI)
          with add_Compl_initials_in_R[of ‹{}› ‹Q2 r2›]
          have ‹- ev ` S ∈ ℛ (Q2 r2)›
            by (simp add: Refusals_iff is_processT1) (meson compl_mono is_processT4 that(4))
          with ‹tF u1› ‹tF u2› ‹(u1, ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X1') ∈ ℱ P1› ‹u2 @ [✓(r2)] ∈ 𝒯 P2›
          have ‹(?map u1, X1') ∈ ℱ (P1 ❙;⇩_✓ Q1)› ‹(?map u2, - ev ` S) ∈ ℱ (P2 ❙;⇩_✓ Q2)›
            by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs Refusals_def_bis)
          moreover have ‹X ∩ range ev ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) X1' S (- ev ` S)›
          proof (rule subsetI)
            show ‹e ∈ X ∩ range ev ⟹ e ∈ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) X1' S (- ev ` S)› for e
              using set_mp[OF "*"(6), of ‹(ev ∘ of_ev) e›]
              by (cases e) (force simp add: super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_def ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_def X1'_def X2'_def)+
          qed
          ultimately show ‹(t, X ∩ range ev) ∈ ℱ ?lhs›
            using "**" by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
        qed
      qed
      ultimately have ‹(t, X ∩ range ev ∪ range tick) ∈ ℱ ?lhs›
        by (auto intro: is_processT5 F_T)
      moreover have ‹X ⊆ X ∩ range ev ∪ range tick›
        by (simp add: subset_iff image_iff) (metis event⇩_p⇩_t⇩_i⇩_c⇩_k.exhaust)
      ultimately show ‹(t, X) ∈ ℱ ?lhs› by (fact is_processT4)
    next
      case F_2
      from F_2(2, 3) obtain u1 u2
        where * : ‹u1 @ [✓(r1)] ∈ 𝒯 P1› ‹u2 @ [✓(r2)] ∈ 𝒯 P2›
          ‹u setinterleaves⇩_✓⇘Sync⇩_P⇩_a⇩_i⇩_r_tj⇙ ((u1, u2), {})›
        by (auto simp add: Sync⇩_P⇩_a⇩_i⇩_r.Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs Sync⇩_P⇩_a⇩_i⇩_r_tj_def
            elim: snoc_tick_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE)
      from F_2(5, 6) obtain v1 v2 X1 X2
        where ** : ‹(v1, X1) ∈ ℱ (Q1 r1)› ‹(v2, X2) ∈ ℱ (Q2 r2)›
          ‹v setinterleaves⇩_✓⇘(⊗✓)⇙ ((v1, v2), S)›
          ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k (⊗✓) X1 S X2›
        unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
      from F_2(4) tF_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_iff[OF "*"(3)] have ‹tF u1› ‹tF u2› by simp_all
      have ‹?map u setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1, ?map u2), S)›
        by (fact "$$"[OF ‹tF u1› ‹tF u2› "*"(1, 2)[THEN is_processT3_TR_append] "*"(3)])
      with "**"(3) have ‹t setinterleaves⇩_✓⇘(⊗✓)⇙ ((?map u1 @ v1, ?map u2 @ v2), S)›
        by (auto simp add: F_2(1) intro: setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_append_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k)
      moreover from "*"(1) "**"(1) ‹tF u1›
      have ‹(?map u1 @ v1, X1) ∈ ℱ (P1 ❙;⇩_✓ Q1)›
        by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
      moreover from "*"(2) "**"(2) ‹tF u2›
      have ‹(?map u2 @ v2, X2) ∈ ℱ (P2 ❙;⇩_✓ Q2)› by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
      ultimately show ‹(t, X) ∈ ℱ ?lhs›
        using "**"(4) by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
    qed
  qed
qed


hide_fact indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma1
  indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_lemma2




corollary (in Synchro⇩_p⇩_t⇩_i⇩_c⇩_k) indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_through_Inter⇩_R⇩_l⇩_i⇩_s⇩_t :
  ‹P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2 = (P1 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t P2) ❙;⇩_✓ (λR. Q1 (hd R) ⟦S⟧⇩_✓ Q2 (tl R))›
  (is ‹?lhs = ?rhs›) if ‹α(P1) ∩ S = {}› ‹α(P2) ∩ S = {}›
  ‹⋀r1. r1 ∈ ❙✓❙s(P1) ⟹ (Q1 r1)⇧⁰ ⊆ ev ` S›
  ‹⋀r2. r2 ∈ ❙✓❙s(P2) ⟹ (Q2 r2)⇧⁰ ⊆ ev ` S›
proof -
  from indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[OF that]
  have ‹P1 ❙;⇩_✓ Q1 ⟦S⟧⇩_✓ P2 ❙;⇩_✓ Q2 = (P1 |||⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ❙;⇩_✓ (λ(r1, r2). Q1 r1 ⟦S⟧⇩_✓ Q2 r2)› .
  also have ‹… = RenamingTick (P1 ⟦{}⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) (λ(x, y). x # y) ❙;⇩_✓
                  (λR. case THE r. r ∈ ❙✓❙s(P1 ⟦{}⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ∧ R = (case r of (r1, r2) ⇒ r1 # r2) of (r1, r2) ⇒ Q1 r1 ⟦S⟧⇩_✓ Q2 r2)›
    by (auto intro: inj_on_Renaming_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[of ‹λ(r1, r2). r1 # r2› _ _ id id, simplified] inj_onI)
  also have ‹… = (P1 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t P2) ❙;⇩_✓ (λR. Q1 (hd R) ⟦S⟧⇩_✓ Q2 (tl R))›
  proof (unfold Sync⇩_P⇩_a⇩_i⇩_r_to_Sync⇩_R⇩_l⇩_i⇩_s⇩_t, rule mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq[OF refl])
    fix R assume ‹R ∈ ❙✓❙s(P1 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t P2)›
    with Sync⇩_R⇩_l⇩_i⇩_s⇩_t.strict_ticks_of_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_subset[of P1 ‹{}› P2]
    obtain r R' where ‹R = r # R'› by (auto simp add: Sync⇩_R⇩_l⇩_i⇩_s⇩_t_tj_def)
    with ‹R ∈ ❙✓❙s(P1 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t P2)›
    have ‹(THE r. r ∈ ❙✓❙s(P1 ⟦{}⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ∧ R = (case r of (r1, r2) ⇒ r1 # r2)) = (r, R')›
      by (auto simp flip: Sync⇩_P⇩_a⇩_i⇩_r_to_Sync⇩_R⇩_l⇩_i⇩_s⇩_t simp add: strict_ticks_of_RenamingTick)
    thus ‹(case THE r. r ∈ ❙✓❙s(P1 ⟦{}⟧⇩_✓⇩_P⇩_a⇩_i⇩_r P2) ∧ R = (case r of (r1, r2) ⇒ r1 # r2)
                of (r1, r2) ⇒ Q1 r1 ⟦S⟧⇩_✓ Q2 r2) =
          Q1 (hd R) ⟦S⟧⇩_✓ Q2 (tl R)› by (simp add: ‹R = r # R'›)
  qed
  finally show ?thesis .
qed



theorem indep_lhs_waiting_rhs_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹❙⟦S❙⟧⇩_✓ l ∈@ L. (P l ❙;⇩_✓ Q l) = (❙|❙|❙|⇩_✓ l ∈@ L. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip L R. Q l r)›
  if ‹⋀l. l ∈ set L ⟹ α(P l) ∩ S = {}›
    and ‹⋀l r. l ∈ set L ⟹ r ∈ ❙✓❙s(P l) ⟹ (Q l r)⇧⁰ ⊆ ev ` S›
proof -
  from that have
    ‹(R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ L. P l) ⟶ (❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip L R. Q l r)⇧⁰ ⊆ ev ` S) ∧
   ❙⟦S❙⟧⇩_✓ l ∈@ L. (P l ❙;⇩_✓ Q l) = (❙|❙|❙|⇩_✓ l ∈@ L. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip L R. Q l r)› for R
  proof (induct L arbitrary: R rule: induct_list012)
    case 1 show ?case by simp
  next
    case (2 l0)
    show ?case
    proof (intro conjI impI)
      show ‹R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ [l0]. P l) ⟹ (❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip [l0] R. Q l r)⇧⁰ ⊆ ev ` S›
        by (auto simp add: strict_ticks_of_RenamingTick initials_Renaming
            dest!: "2.prems"(2)[of l0, simplified] split: if_split_asm)+
    next
      have ‹❙⟦S❙⟧⇩_✓ l ∈@ [l0]. (P l ❙;⇩_✓ Q l) = RenamingTick (P l0 ❙;⇩_✓ Q l0) (λr. [r])› by simp
      also have ‹… = RenamingTick (P l0) (λr. [r]) ❙;⇩_✓ (λg_r. RenamingTick (Q l0 (THE r. r ∈ ❙✓❙s(P l0) ∧ g_r = [r])) (λr. [r]))›
        by (auto intro: inj_on_Renaming_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[of ‹λr. [r]›] inj_onI)
      also have ‹… = (❙|❙|❙|⇩_✓ l ∈@ [l0]. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip [l0] R. Q l r)›
        by (auto intro!: mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq simp add: strict_ticks_of_RenamingTick the_equality)
      finally show ‹❙⟦S❙⟧⇩_✓ l ∈@ [l0]. (P l ❙;⇩_✓ Q l) = …› by simp
    qed
  next
    case (3 l0 l1 L)
    show ?case
    proof (intro conjI impI)
      fix R assume ‹R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ (l0 # l1 # L). P l)›
      from is_ticks_length_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k[THEN is_ticks_lengthD, OF this]
      obtain r0 r1 R' where ‹R = r0 # r1 # R'› by (metis Suc_length_conv)
      have * : ‹r1 # R' ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ⟹
      (❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l1 # L) (r1 # R'). Q l r)⇧⁰ ⊆ ev ` S›
        by (rule "3.hyps"(2)[THEN conjunct1, rule_format]) (simp_all add: "3.prems")
      from ‹R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ (l0 # l1 # L). P l)›
      show ‹(❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l0 # l1 # L) R. Q l r)⇧⁰ ⊆ ev ` S›
        by (auto simp add: ‹R = r0 # r1 # R'› Sync⇩_R⇩_l⇩_i⇩_s⇩_t.initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k Sync⇩_R⇩_l⇩_i⇩_s⇩_t_tj_def
            dest!: Sync⇩_R⇩_l⇩_i⇩_s⇩_t.strict_ticks_of_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_subset[THEN set_mp]
            "*" "3.prems"(2)[of l0 r0, simplified])+
    next
      have ‹❙⟦S❙⟧⇩_✓ l ∈@ (l0 # l1 # L). (P l ❙;⇩_✓ Q l) =
        P l0 ❙;⇩_✓ Q l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). (P l ❙;⇩_✓ Q l)› by simp
      also have ‹❙⟦S❙⟧⇩_✓ l ∈@ (l1 # L). (P l ❙;⇩_✓ Q l) =
                 (❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip(l1 # L) R. Q l r)›
        by (rule "3.hyps"(2)[THEN conjunct2]) (simp_all add: "3.prems")
      finally have ‹❙⟦S❙⟧⇩_✓ l ∈@ (l0 # l1 # L). (P l ❙;⇩_✓ Q l) =
                    P l0 ❙;⇩_✓ Q l0 ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t (❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip(l1 # L) R. Q l r)› .
      also have ‹… = (P l0 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ❙;⇩_✓
                  (λR. Q l0 (hd R) ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l1 # L) (tl R). Q l r)›
      proof (rule Sync⇩_R⇩_l⇩_i⇩_s⇩_t.indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_through_Inter⇩_R⇩_l⇩_i⇩_s⇩_t)
        show ‹α(P l0) ∩ S = {}› by (simp add: "3.prems"(1))
      next
        show ‹α(❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ∩ S = {}›
          by (auto dest!: events_of_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k_subset[THEN set_mp]) (use "3.prems"(1) in auto)
      next
        show ‹r0 ∈ ❙✓❙s(P l0) ⟹ (Q l0 r0)⇧⁰ ⊆ ev ` S› for r0 by (simp add: "3.prems"(2))
      next
        show ‹R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ⟹ (❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l1 # L) R. Q l r)⇧⁰ ⊆ ev ` S› for R
          using "3.hyps"(2) "3.prems"(1, 2) by auto
      qed
      also have ‹… = (❙|❙|❙|⇩_✓ l ∈@ (l0 # l1 # L). P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l0 # l1 # L) R. Q l r)›
      proof (rule mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq)
        show ‹P l0 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l = ❙|❙|❙|⇩_✓ l ∈@ (l0 # l1 # L). P l› by simp
      next
        fix R assume ‹R ∈ ❙✓❙s(P l0 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l)›
        from is_ticks_length_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k
          [THEN is_ticks_lengthD, of _ _ ‹l0 # l1 # L›, simplified, OF this]
        obtain r0 r1 R' where ‹R = r0 # r1 # R'› by (metis Suc_length_conv)
        thus ‹Q l0 (hd R) ⟦S⟧⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l1 # L) (tl R). Q l r =
          ❙⟦S❙⟧⇩_✓ (l, r) ∈@ zip (l0 # l1 # L) R. Q l r› by simp
      qed
      finally show ‹❙⟦S❙⟧⇩_✓ l ∈@ (l0 # l1 # L). (P l ❙;⇩_✓ Q l) = …› .
    qed
  qed
  thus ?thesis ..
qed



theorem indep_lhs_waiting_rhs_MultiSync_Seq⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹❙⟦S❙⟧ l ∈# (mset L). (P l ❙;⇩_✓ Q l) = (❙|❙|❙|⇩_✓ l ∈@ L. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r) ∈# mset (zip L R). Q l r)›
  if ‹⋀l. l ∈ set L ⟹ α(P l) ∩ S = {}›
    and ‹⋀l r. l ∈ set L ⟹ r ∈ ❙✓❙s(P l) ⟹ (Q l r)⇧⁰ ⊆ ev ` S›
proof -
  from that have
    ‹(R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ L. P l) ⟶ (❙⟦S❙⟧ (l, r) ∈# mset (zip L R). Q l r)⇧⁰ ⊆ ev ` S) ∧
   ❙⟦S❙⟧ l ∈# (mset L). (P l ❙;⇩_✓ Q l) = (❙|❙|❙|⇩_✓ l ∈@ L. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r) ∈# mset (zip L R). Q l r)› for R
  proof (induct L arbitrary: R rule: induct_list012)
    case 1 show ?case by simp
  next
    case (2 l0)
    show ?case
    proof (intro conjI impI)
      show ‹R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ [l0]. P l) ⟹ (❙⟦S❙⟧ (l, r) ∈# mset (zip [l0] R). Q l r)⇧⁰ ⊆ ev ` S›
        by (auto simp add: strict_ticks_of_RenamingTick initials_Renaming
            dest!: "2.prems"(2)[of l0, simplified] split: if_split_asm)+
    next
      have ‹❙⟦S❙⟧ l ∈# mset [l0]. (P l ❙;⇩_✓ Q l) = P l0 ❙;⇩_✓ Q l0› by simp
      also have ‹… = RenamingTick (P l0) (λr. [r]) ❙;⇩_✓ (λg_r. Q l0 (THE r. r ∈ ❙✓❙s(P l0) ∧ g_r = [r]))›
        by (auto intro: inj_on_Renaming_Seq⇩_p⇩_t⇩_i⇩_c⇩_k[of ‹λr. [r]› _ _ id id, simplified] inj_onI)
      also have ‹… = (❙|❙|❙|⇩_✓ l ∈@ [l0]. P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r) ∈# mset (zip [l0] R). Q l r)›
        by (auto intro!: mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq simp add: strict_ticks_of_RenamingTick the_equality)
      finally show ‹❙⟦S❙⟧ l ∈# mset [l0]. (P l ❙;⇩_✓ Q l) = …› by simp
    qed
  next
    case (3 l0 l1 L)
    show ?case
    proof (intro conjI impI)
      fix R assume ‹R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ (l0 # l1 # L). P l)›
      from is_ticks_length_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k[THEN is_ticks_lengthD, OF this]
      obtain r0 r1 R' where ‹R = r0 # r1 # R'› by (metis Suc_length_conv)
      have * : ‹r1 # R' ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ⟹
      (❙⟦S❙⟧ (l, r) ∈# mset (zip (l1 # L) (r1 # R')). Q l r)⇧⁰ ⊆ ev ` S›
        by (rule "3.hyps"(2)[THEN conjunct1, rule_format]) (simp_all add: "3.prems")
      from ‹R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ (l0 # l1 # L). P l)›
      show ‹(❙⟦S❙⟧ (l, r) ∈# mset (zip (l0 # l1 # L) R). Q l r)⇧⁰ ⊆ ev ` S›
        by (auto simp add: ‹R = r0 # r1 # R'› initials_Sync Sync⇩_R⇩_l⇩_i⇩_s⇩_t_tj_def
            dest!: Sync⇩_R⇩_l⇩_i⇩_s⇩_t.strict_ticks_of_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_subset[THEN set_mp]
            "*" "3.prems"(2)[of l0 r0, simplified])+
    next
      have ‹❙⟦S❙⟧ l∈#mset (l0 # l1 # L). (P l ❙;⇩_✓ Q l) =
        P l0 ❙;⇩_✓ Q l0 ⟦S⟧ ❙⟦S❙⟧ l∈#mset (l1 # L). (P l ❙;⇩_✓ Q l)› by simp
      also have ‹❙⟦S❙⟧ l∈#mset (l1 # L). (P l ❙;⇩_✓ Q l) =
        ❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r)∈#mset (zip (l1 # L) R). Q l r)›
        by (rule "3.hyps"(2)[THEN conjunct2]) (simp_all add: "3.prems")
      finally have ‹❙⟦S❙⟧ l∈#mset (l0 # l1 # L). (P l ❙;⇩_✓ Q l) =
                    P l0 ❙;⇩_✓ Q l0 ⟦S⟧ ❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r)∈#mset (zip (l1 # L) R). Q l r)› .
      also have ‹… = (P l0 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ❙;⇩_✓
                      (λR. Q l0 (hd R) ⟦S⟧ ❙⟦S❙⟧ (l, r)∈#mset (zip (l1 # L) (tl R)). Q l r)›
      proof (fold Sync⇩_C⇩_l⇩_a⇩_s⇩_s⇩_i⇩_c_is_Sync,
          rule Sync⇩_C⇩_l⇩_a⇩_s⇩_s⇩_i⇩_c.indep_lhs_waiting_rhs_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_through_Inter⇩_R⇩_l⇩_i⇩_s⇩_t)
        show ‹α(P l0) ∩ S = {}› by (simp add: "3.prems"(1))
      next
        show ‹α(❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ∩ S = {}›
          by (auto dest!: events_of_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k_subset[THEN set_mp]) (use "3.prems"(1) in auto)
      next
        show ‹r0 ∈ ❙✓❙s(P l0) ⟹ (Q l0 r0)⇧⁰ ⊆ ev ` S› for r0 by (simp add: "3.prems"(2))
      next
        show ‹R ∈ ❙✓❙s(❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l) ⟹ (❙⟦S❙⟧ (l, r)∈#mset (zip (l1 # L) R). Q l r)⇧⁰ ⊆ ev ` S› for R
          using "3.hyps"(2) "3.prems"(1, 2) by auto
      qed
      also have ‹… = (❙|❙|❙|⇩_✓ l ∈@ (l0 # l1 # L). P l) ❙;⇩_✓ (λR. ❙⟦S❙⟧ (l, r) ∈# mset (zip (l0 # l1 # L) R). Q l r)›
      proof (rule mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_eq)
        show ‹P l0 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l = ❙|❙|❙|⇩_✓ l ∈@ (l0 # l1 # L). P l› by simp
      next
        fix R assume ‹R ∈ ❙✓❙s(P l0 |||⇩_✓⇩_R⇩_l⇩_i⇩_s⇩_t ❙|❙|❙|⇩_✓ l ∈@ (l1 # L). P l)›
        from is_ticks_length_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k
          [THEN is_ticks_lengthD, of _ _ ‹l0 # l1 # L›, simplified, OF this]
        obtain r0 r1 R' where ‹R = r0 # r1 # R'› by (metis Suc_length_conv)
        thus ‹Q l0 (hd R) ⟦S⟧ ❙⟦S❙⟧ (l, r)∈#mset (zip (l1 # L) (tl R)). Q l r =
              ❙⟦S❙⟧ (l, r)∈#mset (zip (l0 # l1 # L) R). Q l r› by simp
      qed
      finally show ‹❙⟦S❙⟧ l∈#mset (l0 # l1 # L). (P l ❙;⇩_✓ Q l) = …› .
    qed
  qed
  thus ?thesis ..
qed


(*<*)
end
  (*>*)