Theory Basic_CSP_Laws

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : Basic laws
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * 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 list of conditions and the following disclaimer.
 *
 *     * 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.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * 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
 * OWNER 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.
 ******************************************************************************›
(*>*)

section‹ The Basic Laws ›

(*<*)
theory Basic_CSP_Laws                                               
  imports Constant_Processes Deterministic_Choice Non_Deterministic_Choice
    Global_Non_Deterministic_Choice Sliding_Choice
    Multi_Deterministic_Prefix_Choice Multi_Non_Deterministic_Prefix_Choice
    Sequential_Composition Synchronization_Product Hiding Renaming CSP_Monotonies
begin
  (*>*)

text ‹By ``basic'' laws we mean the behaviour of \<^term>‹⊥›, \<^const>‹STOP› and \<^const>‹SKIP›,
      plus the associativity of some concerned operators.›


subsection ‹The Laws of \<^term>‹⊥››

text ‹From the characterization @{thm BOT_iff_Nil_D}, we can easily derive the behaviour
      of \<^term>‹⊥› wrt. \<^const>‹STOP›, \<^const>‹SKIP›, and the operators.›

lemma BOT_less1 [simp]: ‹(⊥ :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ≤ X›
  by (simp add: le_approx_imp_le_ref)

lemma STOP_neq_BOT [simp] : ‹STOP   ≠ ⊥›
  and SKIP_neq_BOT [simp] : ‹SKIP r ≠ ⊥›
  by (simp_all add: BOT_iff_Nil_D D_STOP D_SKIP)


lemma Det_is_BOT_iff : ‹P □ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (simp add: BOT_iff_Nil_D D_Det D_BOT)

lemma Det_BOT [simp] : ‹P □ ⊥ = ⊥› and BOT_Det [simp] : ‹⊥ □ P = ⊥›
  by (simp_all add: Det_is_BOT_iff)


lemma Ndet_is_BOT_iff : ‹P ⊓ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (simp add: BOT_iff_Nil_D D_Ndet D_BOT)

lemma Ndet_BOT [simp] : ‹P ⊓ ⊥ = ⊥› and BOT_Ndet [simp] : ‹⊥ ⊓ P = ⊥›
  by (simp_all add: Ndet_is_BOT_iff)


lemma Sliding_is_BOT_iff: ‹P ⊳ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (simp add: Sliding_def Ndet_is_BOT_iff Det_is_BOT_iff)

lemma Sliding_BOT [simp] : ‹P ⊳ ⊥ = ⊥› and BOT_Sliding [simp] : ‹⊥ ⊳ P = ⊥›
  by (simp_all add: Sliding_is_BOT_iff)


lemma Mprefix_neq_BOT [simp] : ‹□ a ∈ A → P a ≠ ⊥›
  by (simp add: BOT_iff_Nil_D D_Mprefix)

lemma Mndetprefix_neq_BOT [simp] : ‹⊓ a ∈ A → P a ≠ ⊥›
  by (simp add: BOT_iff_Nil_D D_Mndetprefix write0_def D_Mprefix)


lemma Seq_is_BOT_iff : ‹P ❙; Q = ⊥ ⟷ P = ⊥ ∨ (∃r. [✓(r)] ∈ 𝒯 P ∧ Q = ⊥)›
  by (simp add: BOT_iff_Nil_D D_Seq)

lemma BOT_Seq [simp] : ‹⊥ ❙; P = ⊥› by (simp add: Seq_is_BOT_iff)


lemma Hiding_BOT [simp] : ‹⊥ \ A = ⊥›
  by (simp add: BOT_iff_Nil_D D_Hiding BOT_projs)
    (meson filter.simps(1) tickFree_Nil tickFree_imp_front_tickFree)


lemma Sync_is_BOT_iff : ‹P ⟦S⟧ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (simp add: BOT_iff_Nil_D D_Sync)
    (metis si_empty1 empty_setinterleaving insertI1 is_processT1_TR)

lemma Sync_BOT [simp] : ‹P ⟦ S ⟧ ⊥ = ⊥› and BOT_Sync [simp] : ‹⊥ ⟦ S ⟧ P = ⊥›
  by (simp_all add: Sync_is_BOT_iff)


lemma Renaming_is_BOT_iff : ‹Renaming P f g = ⊥ ⟷ P = ⊥›
  by (simp add: BOT_iff_Nil_D D_Renaming)

lemma Renaming_BOT [simp] : ‹Renaming ⊥ f g = ⊥›
  by (simp add: Renaming_is_BOT_iff)


lemma GlobalNdet_is_BOT_iff : ‹(⊓a∈A. P a) = ⊥ ⟷ (∃a∈A. P a = ⊥)›
  by (simp add: BOT_iff_Nil_D D_GlobalNdet)

lemma GlobalNdet_BOT [simp] : ‹a ∈ A ⟹ P a = ⊥ ⟹ (⊓a∈A. P a) = ⊥›
  by (auto simp add: GlobalNdet_is_BOT_iff)



subsection ‹The Laws of \<^const>‹STOP››

text ‹From the characterization @{thm STOP_iff_T}, we can easily derive the behaviour
      of \<^const>‹STOP› wrt. \<^const>‹SKIP› and the operators.›

lemma SKIP_Neq_STOP : ‹SKIP r ≠ STOP›
  by (simp add: STOP_iff_T T_SKIP)


lemma Det_is_STOP_iff : ‹P □ Q = STOP ⟷ P = STOP ∧ Q = STOP›
  by (simp add: STOP_iff_T T_Det) (use Nil_elem_T in blast)

lemma Det_STOP [simp] : ‹P □ STOP = P› and STOP_Det [simp] : ‹STOP □ P = P›
  by (auto simp add: Process_eq_spec F_Det F_STOP D_Det D_STOP T_STOP
      intro: is_processT8 is_processT6_TR_notin)


lemma Ndet_is_STOP_iff : ‹P ⊓ Q = STOP ⟷ P = STOP ∧ Q = STOP›
  by (simp add: STOP_iff_T T_Ndet) (use Nil_elem_T in blast)


lemma Sliding_is_STOP_iff: ‹P ⊳ Q = STOP ⟷ P = STOP ∧ Q = STOP›
  by (simp add: Sliding_def Ndet_is_STOP_iff Det_is_STOP_iff)

lemma Sliding_STOP [simp] : ‹P ⊳ STOP = P ⊓ STOP› and STOP_Sliding [simp] : ‹STOP ⊳ P = P›
  by (simp_all add: Sliding_def)


lemma Mprefix_is_STOP_iff : ‹□ a ∈ A → P a = STOP ⟷ A = {}›
  by (simp add: STOP_iff_T T_Mprefix) (use Nil_elem_T in blast)

lemma Mprefix_empty [simp] : ‹□ a ∈ {} → P a = STOP›
  by (simp add: Mprefix_is_STOP_iff)

lemma Mndetprefix_is_STOP_iff : ‹⊓ a ∈ A → P a = STOP ⟷ A = {}›
  by (simp add: STOP_iff_T T_Mndetprefix') (use Nil_elem_T in blast)

lemma Mndetprefix_empty [simp] : ‹⊓ a ∈ {} → P a = STOP›
  by (simp add: Mndetprefix_is_STOP_iff)


lemma Seq_is_STOP_iff :
  ‹P ❙; Q = STOP ⟷ 𝒯 P ⊆ insert [] {[✓(r)]| r. True} ∧ (P ≠ STOP ⟶ Q = STOP)›
proof (intro iffI conjI subsetI)
  show ‹P ❙; Q = STOP ⟹ t ∈ 𝒯 P ⟹ t ∈ insert [] {[✓(r)] |r. True}› for t
    by (simp add: STOP_iff_T T_Seq set_eq_iff)
      (metis T_nonTickFree_imp_decomp append.right_neutral append_Nil is_processT1_TR)
next
  show ‹P ❙; Q = STOP ⟹ P ≠ STOP ⟶ Q = STOP›
    by (simp add: STOP_iff_T T_Seq set_eq_iff)
      (metis T_nonTickFree_imp_decomp append_is_Nil_conv is_processT1_TR)
next
  show ‹𝒯 P ⊆ insert [] {[✓(r)] |r. True} ∧ (P ≠ STOP ⟶ Q = STOP) ⟹ P ❙; Q = STOP›
    by (simp add: STOP_iff_T T_Seq subset_iff, safe, simp_all)
      (((use D_T in fastforce)+)[3],
        metis D_T event⇩p⇩t⇩i⇩c⇩k.distinct(1) front_tickFree_single is_processT9_tick list.sel(1) not_Cons_self)
qed

lemma STOP_Seq [simp] : ‹STOP ❙; P = STOP› by (simp add: Seq_is_STOP_iff T_STOP)


lemma Hiding_STOP [simp] : ‹STOP \ A = STOP›
  by (auto simp add: STOP_iff_T T_Hiding F_STOP D_STOP T_STOP strict_mono_def) blast


lemma STOP_Sync_STOP [simp] : ‹STOP ⟦S⟧ STOP = STOP›
  by (simp add: STOP_iff_T T_Sync T_STOP D_STOP)


lemma Renaming_is_STOP_iff : ‹Renaming P f g = STOP ⟷ P = STOP›
proof (rule iffI)
  show ‹P = STOP ⟹ Renaming P f g = STOP›
    by (simp add: STOP_iff_T T_Renaming subset_iff)
      (metis D_STOP STOP_iff_T empty_iff)
next
  assume ‹Renaming P f g = STOP›
  hence ‹P ≠ ⊥› by force
  with ‹Renaming P f g = STOP› show ‹P = STOP›
    by (simp add: BOT_iff_Nil_D STOP_iff_T T_Renaming set_eq_iff) blast
qed

lemma Renaming_STOP [simp] : ‹Renaming STOP f g = STOP›
  by (simp add: Renaming_is_STOP_iff)


lemma GlobalNdet_is_STOP_iff : ‹(⊓a∈A. P a) = STOP ⟷ (∀a∈A. P a = STOP)›
  by (simp add: STOP_iff_T T_GlobalNdet) (use Nil_elem_T in blast)

lemma GlobalNdet_empty [simp] : ‹(⊓a∈{}. P a) = STOP›
  by (simp add: GlobalNdet_is_STOP_iff)

lemma GlobalNdet_id [simp] : ‹(⊓a∈A. P) = (if A = {} then STOP else P)›
  by simp 

lemma ‹(⊓a∈A. STOP) = STOP› by simp



subsubsection ‹More powerful Laws›

lemma Inter_STOP [simp] : ‹P ||| STOP = P ❙; STOP›
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 (P ||| STOP) ⟹ t ∈ 𝒟 (P ❙; STOP)› for t
    by (simp add: D_Sync D_Seq D_STOP T_STOP)
      (metis emptyRightProperty is_processT7 self_append_conv)
next
  show ‹t ∈ 𝒟 (P ❙; STOP) ⟹ t ∈ 𝒟 (P ||| STOP)› for t
    apply (simp add: D_Sync D_Seq D_STOP T_STOP)
    apply (frule D_imp_front_tickFree)
    apply (rule exI[of _ ‹if tF t then t else butlast t›],
        rule exI[of _ ‹if tF t then t else butlast t›])
    apply (simp split: if_split_asm)
    by (metis butlast_snoc disjoint_iff emptyLeftSelf front_tickFree_iff_tickFree_butlast
        front_tickFree_single is_processT9 nonTickFree_n_frontTickFree setinterleaving_sym tickFree_def)
next
  fix t X assume ‹(t, X) ∈ ℱ (P ||| STOP)› ‹t ∉ 𝒟 (P ||| STOP)›
  then obtain t_P X_P X_Q where ‹(t_P, X_P) ∈ ℱ P› ‹t setinterleaves ((t_P, []), range tick)›
    ‹X = (X_P ∪ X_Q) ∩ range tick ∪ X_P ∩ X_Q›
    by (simp add: F_Sync D_Sync F_STOP) blast
  from ‹t setinterleaves ((t_P, []), range tick)› EmptyLeftSync
  have ‹tF t ∧ t = t_P› by (metis inf_commute setinterleaving_sym tickFree_def)
  show ‹(t, X) ∈ ℱ (P ❙; STOP)›
  proof (cases ‹∃r. t_P @ [✓(r)] ∈ 𝒯 P›)
    show ‹∃r. t_P @ [✓(r)] ∈ 𝒯 P ⟹ (t, X) ∈ ℱ (P ❙; STOP)›
      using ‹tF t ∧ t = t_P› by (simp add: F_Seq F_STOP)
  next
    assume ‹∄r. t_P @ [✓(r)] ∈ 𝒯 P›
    with ‹(t_P, X_P) ∈ ℱ P› have ‹(t_P, X_P ∪ range tick) ∈ ℱ P›
      by (metis is_processT5_S7' rangeE)
    moreover from ‹X = (X_P ∪ X_Q) ∩ range tick ∪ X_P ∩ X_Q›
    have ‹X ∪ range tick ⊆ X_P ∪ range tick› by auto
    ultimately have ‹(t_P, X ∪ range tick) ∈ ℱ P› by (fact is_processT4)
    with ‹tF t ∧ t = t_P› show ‹(t, X) ∈ ℱ (P ❙; STOP)› by (auto simp add: F_Seq)
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ (P ❙; STOP)› ‹t ∉ 𝒟 (P ❙; STOP)›
  then consider ‹(t, X ∪ range tick) ∈ ℱ P› ‹tF t› | r where ‹t @ [✓(r)] ∈ 𝒯 P›
    by (simp add: Seq_projs F_STOP) blast
  thus ‹(t, X) ∈ ℱ (P ||| STOP)›
  proof cases
    assume ‹(t, X ∪ range tick) ∈ ℱ P› and ‹tF t›
    from ‹tF t› have ‹t setinterleaves ((t, []), range tick)›
      by (metis disjoint_iff emptyLeftSelf setinterleaving_sym tickFree_def)
    with ‹(t, X ∪ range tick) ∈ ℱ P› show ‹(t, X) ∈ ℱ (P ||| STOP)›
      apply (simp add: F_Sync F_STOP)
      by (metis Int_Un_eq(1) Un_Int_eq(3) is_processT4 sup_ge1)
  next
    fix r assume ‹t @ [✓(r)] ∈ 𝒯 P›
    hence * : ‹(t, X - {✓(r)}) ∈ ℱ P› and ‹tF t›
      by (auto simp add: T_F_spec is_processT6 intro: append_T_imp_tickFree)
    from ‹tF t› have ‹t setinterleaves ((t, []), range tick)›
      by (metis disjoint_iff emptyLeftSelf setinterleaving_sym tickFree_def)
    hence ‹(t, (X - {✓(r)} ∪ UNIV) ∩ range tick ∪ (X - {✓(r)}) ∩ UNIV) ∈ ℱ (P ||| STOP)›
      by (simp add: F_Sync F_STOP) (use "*" in blast)
    moreover have ‹X ⊆ (X - {✓(r)} ∪ UNIV) ∩ range tick ∪ (X - {✓(r)}) ∩ UNIV› by auto
    ultimately show ‹(t, X) ∈ ℱ (P ||| STOP)› by (fact is_processT4)
  qed
qed

corollary STOP_Inter [simp] : ‹STOP ||| P = P ❙; STOP›
  by (metis Inter_STOP Sync_commute)


lemma Par_STOP [simp] : ‹P || STOP = (if P = ⊥ then ⊥ else STOP)›
proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ⟹ P || STOP = ⊥› by simp
next
  assume ‹P ≠ ⊥›
  from ‹P ≠ ⊥› show ‹P || STOP = STOP›
    by (simp add: STOP_iff_T T_Sync STOP_projs set_eq_iff BOT_iff_Nil_D)
      (metis EmptyLeftSync si_empty1 inf_top.right_neutral insertI1
        is_processT1_TR set_empty2 setinterleaving_sym)
qed

lemma STOP_Par [simp] : ‹STOP || P = (if P = ⊥ then ⊥ else STOP)›
  by (metis Par_STOP Sync_commute)




subsection ‹The Laws of \<^const>‹SKIP››

subsubsection ‹The definition of SKIPS›

definition SKIPS :: ‹'r set ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  where ‹SKIPS R ≡ ⊓r ∈ R. SKIP r›

lemma SKIPS_empty [simp]         : ‹SKIPS {} = STOP›
  and SKIPS_singl_is_SKIP [simp] : ‹SKIPS {r} = SKIP r› by (simp_all add: SKIPS_def)


lemma F_SKIPS :
  ‹ℱ (SKIPS R) = (  if R = {} then {(s, X). s = []}
                  else {([], X) |X. ∃r ∈ R. tick r ∉ X} ∪
                       {(s, X). ∃r ∈ R. s = [tick r]})›
  by (auto simp add: SKIPS_def F_GlobalNdet F_SKIP)

lemma D_SKIPS : ‹𝒟 (SKIPS R) = {}›
  by (auto simp add: SKIPS_def D_GlobalNdet D_SKIP)

lemma T_SKIPS : ‹𝒯 (SKIPS R) = insert [] {[tick r]| r. r ∈ R}›
  by (auto simp add: SKIPS_def T_GlobalNdet T_SKIP)

lemmas SKIPS_projs = F_SKIPS D_SKIPS T_SKIPS



subsubsection ‹Laws›

lemma SKIP_Sliding [simp] : ‹SKIP r ⊳ P = P ⊓ SKIP r›
  by (auto simp add: Process_eq_spec F_Sliding D_Sliding F_Ndet D_Ndet SKIP_projs)

lemma Sliding_SKIP [simp] : ‹P ⊳ SKIP r = P □ SKIP r› 
  by (auto simp add: Process_eq_spec F_Sliding D_Sliding F_Det D_Det SKIP_projs)


lemma Mprefix_neq_SKIP [simp] : ‹□ a ∈ A → P a ≠ SKIP r›
  by (auto simp add: Process_eq_spec F_Mprefix F_SKIP)

lemma Mndetprefix_neq_SKIP [simp] : ‹⊓ a ∈ A → P a ≠ SKIP r›
  by (auto simp add: Process_eq_spec F_Mndetprefix write0_def F_Mprefix F_SKIP)


lemma SKIP_Seq [simp] : ‹SKIP r ❙; P = P›
  by (simp add: Process_eq_spec Seq_projs SKIP_projs)

lemma Seq_SKIP [simp] : ‹P ❙; SKIP () = P›
  ―‹This is only true when the type \<^typ>‹'r› of \<^typ>‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k› is set to \<^typ>‹unit›
     (morally, we have ``only one \<^const>‹tick›'').›
  by (auto simp add: Process_eq_spec Seq_projs SKIP_projs tick_T_F intro: is_processT4 is_processT6_TR_notin is_processT8)
    (metis (full_types) append.right_neutral is_processT5_S7' old.unit.exhaust rangeE,
      metis (full_types) F_T T_imp_front_tickFree nonTickFree_n_frontTickFree old.unit.exhaust)


lemma Hiding_SKIP [simp] : ‹SKIP r \ A = SKIP r›
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 (SKIP r \ A) ⟹ s ∈ 𝒟 (SKIP r)› for s
    by (auto simp add: D_Hiding D_SKIP T_SKIP)
      (metis (full_types) Hiding_tickFree non_tickFree_tick not_less_eq_eq strict_mono_eq)
next
  show ‹s ∈ 𝒟 (SKIP r) ⟹ s ∈ 𝒟 (SKIP r \ A)› for s
    by (simp add: D_Hiding D_SKIP T_SKIP)
next
  show ‹(s, X) ∈ ℱ (SKIP r \ A) ⟹ (s, X) ∈ ℱ (SKIP r)› for s X
    by (auto simp add: F_Hiding SKIP_projs image_iff)
      (metis (mono_tags, lifting) filter.simps(1) non_tickFree_tick,
        (metis less_tail list.sel(3) nil_less strict_mono_Suc_iff)+)
next
  show ‹(s, X) ∈ ℱ (SKIP r) ⟹ (s, X) ∈ ℱ (SKIP r \ A)› for s X
    by (simp add: F_Hiding SKIP_projs)
      (metis event⇩p⇩t⇩i⇩c⇩k.distinct(1) filter.simps(1, 2) image_iff)
qed



subsubsection ‹Synchronization›

lemma SKIP_Sync_SKIP [simp] : ‹SKIP r ⟦ S ⟧ SKIP s = (if r = s then SKIP r else STOP)›
  for S :: ‹'a set› and r :: 'r
proof (split if_split, intro conjI impI)
  show ‹SKIP r ⟦S⟧ SKIP s = SKIP r› if ‹r = s›
  proof (fold ‹r = s›, subst Process_eq_spec_optimized, safe)
    show ‹s ∈ 𝒟 (SKIP r ⟦S⟧ SKIP r) ⟹ s ∈ 𝒟 (SKIP r)›
      and ‹s ∈ 𝒟 (SKIP r) ⟹ s ∈ 𝒟 (SKIP r ⟦S⟧ SKIP r)› for s
      by (simp_all add: D_Sync D_SKIP)
  next
    assume same_div : ‹𝒟 (SKIP r ⟦S⟧ SKIP r) = 𝒟 (SKIP r)›
    fix s X assume ‹(s, X) ∈ ℱ (SKIP r ⟦S⟧ SKIP r)›
    then consider ‹s ∈ 𝒟 (SKIP r ⟦S⟧ SKIP r)›
      | s_P s_Q X_P X_Q where
        ‹(s_P, X_P) ∈ ℱ (SKIP r)› ‹(s_Q, X_Q) ∈ ℱ (SKIP r)›
        ‹s setinterleaves ((s_P, s_Q), range tick ∪ ev ` S)›
        ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
      by (simp add: F_Sync D_Sync) blast
    thus ‹(s, X) ∈ ℱ (SKIP r)›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 (SKIP r ⟦S⟧ SKIP r) ⟹ (s, X) ∈ ℱ (SKIP r)› by blast
    next
      fix s_P s_Q X_P X_Q
      assume * : ‹(s_P, X_P) ∈ ℱ (SKIP r)› ‹(s_Q, X_Q) ∈ ℱ (SKIP r)›
        ‹s setinterleaves ((s_P, s_Q), range tick ∪ ev ` S)›
        ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
      from "*"(1, 2, 3) consider ‹s = []› ‹s_P = []› ‹s_Q = []›
        | ‹s = [tick r]› ‹s_P = [tick r]› ‹s_Q = [tick r]›
        by (cases s_P; cases s_Q; simp add: image_iff F_SKIP split: if_split_asm)
      thus ‹(s, X) ∈ ℱ (SKIP r)›
      proof cases
        assume ‹s = []› and ‹s_P = []› and ‹s_Q = []›
        from ‹s_P = []› "*"(1) have ‹tick r ∉ X_P› by (simp add: F_SKIP)
        moreover from ‹s_Q = []› "*"(2) have ‹tick r ∉ X_Q› by (simp add: F_SKIP)
        ultimately have ‹tick r ∉ X› by (simp add: "*"(4))
        with ‹s = []› show ‹(s, X) ∈ ℱ (SKIP r)› by (simp add: F_SKIP)
      next
        show ‹s = [tick r] ⟹ (s, X) ∈ ℱ (SKIP r)› by (simp add: F_SKIP)
      qed
    qed
  next
    fix s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› and X assume ‹(s, X) ∈ ℱ (SKIP r)›
    then consider ‹s = []› ‹tick r ∉ X› | ‹s = [tick r]› by (simp add: F_SKIP) blast
    thus ‹(s, X) ∈ ℱ (SKIP r ⟦S⟧ SKIP r)›
    proof cases
      assume ‹s = []› and ‹tick r ∉ X›
      have ‹([], X) ∈ ℱ (SKIP r)› by (simp add: F_SKIP ‹tick r ∉ X›)
      moreover have ‹[] setinterleaves (([], []), range tick ∪ ev ` S)› by simp
      moreover have ‹X = (X ∪ X) ∩ (range tick ∪ ev ` S) ∪ X ∩ X› by simp
      ultimately show ‹(s, X) ∈ ℱ (SKIP r ⟦S⟧ SKIP r)›
        unfolding F_Sync using ‹s = []› by blast
    next
      assume ‹s = [tick r]›
      have ‹([tick r], X) ∈ ℱ (SKIP r)› by (simp add: F_SKIP)
      moreover have ‹[tick r] setinterleaves (([tick r], [tick r]), range tick ∪ ev ` S)› by simp
      moreover have ‹X = (X ∪ X) ∩ (range tick ∪ ev ` S) ∪ X ∩ X› by simp
      ultimately show ‹(s, X) ∈ ℱ (SKIP r ⟦S⟧ SKIP r)›
        unfolding F_Sync using ‹s = [tick r]› by blast
    qed
  qed
next
  show ‹r ≠ s ⟹ SKIP r ⟦S⟧ SKIP s = STOP›
    by (force simp add: STOP_iff_T T_Sync T_SKIP D_SKIP)
qed


lemma SKIP_Sync_STOP [simp] : ‹SKIP r ⟦S⟧ STOP   = STOP›
  and STOP_Sync_SKIP [simp] : ‹STOP   ⟦S⟧ SKIP r = STOP›
  by (force simp add: STOP_iff_T T_Sync T_SKIP D_SKIP T_STOP D_STOP)+

lemma Mprefix_Sync_SKIP : ‹(□a ∈ A → P a) ⟦S⟧ SKIP res = □a ∈ (A - S) → (P a ⟦S⟧ SKIP res)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then obtain a t u r v
    where * : ‹a ∈ A› ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹s = r @ v›
      ‹r setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
      ‹t ∈ 𝒟 (P a)› ‹u = [] ∨ u = [tick res]›
    by (simp add: D_Sync D_SKIP T_SKIP D_Mprefix image_iff) blast
  from "*"(5, 7) obtain r'
    where ** : ‹a ∉ S› ‹r = ev a # r'› ‹r' setinterleaves ((t, u), range tick ∪ ev ` S)›
    by (elim disjE; simp add: image_iff split: if_split_asm, blast)
  show ‹s ∈ 𝒟 ?rhs›
    by (simp add: D_Mprefix "*"(1, 4) "**"(1, 2) D_Sync T_SKIP D_SKIP)
      (use "*"(2, 3, 6, 7) "**"(2, 3) tickFree_Cons_iff in blast)
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then obtain s' a t u r v
    where * : ‹s = ev a # s'› ‹a ∈ A› ‹a ∉ S› ‹front_tickFree v› ‹t ∈ 𝒟 (P a)›
      ‹tickFree r ∨ v = []› ‹s' = r @ v› ‹u = [] ∨ u = [tick res]›
      ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
    by (simp add: D_Mprefix D_Sync T_SKIP D_SKIP image_iff) blast
  from "*"(8, 9) have ‹(ev a # r) setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
    by (elim disjE; simp add: "*"(3) image_iff)
  moreover have ‹ev a # t ∈ 𝒟 (□a ∈ A → P a)› by (simp add: D_Mprefix "*"(2, 5))
  ultimately show ‹s ∈ 𝒟 ?lhs›
    apply (simp add: D_Sync T_SKIP D_SKIP "*"(1, 7))
    apply (rule exI[of _ ‹ev a # t›], rule exI[of _ u],
        rule exI[of _ ‹ev a # r›], simp)
    using "*"(4) "*"(6) "*"(8) by blast
next
  fix s Z
  assume same_div: ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, Z) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | t u X Y where ‹(t, X) ∈ ℱ (□a ∈ A → P a)› ‹(u, Y) ∈ ℱ (SKIP res)›
      ‹s setinterleaves ((t, u), range tick ∪ ev ` S)›
      ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
    by (simp add: F_Sync D_Sync) blast
  thus ‹(s, Z) ∈ ℱ ?rhs›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, Z) ∈ ℱ ?rhs› by blast
  next
    fix t u X Y
    assume assms : ‹(t, X) ∈ ℱ (□a ∈ A → P a)› ‹(u, Y) ∈ ℱ (SKIP res)›
      ‹s setinterleaves ((t, u), range tick ∪ ev ` S)›
      ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
    from assms(1) have ‹t = [] ∧ X ∩ ev ` A = {} ∨
                        (∃a t'. a ∈ A ∧ t = ev a # t' ∧ (t', X) ∈ ℱ (P a))›
      by (simp add: F_Mprefix image_iff) blast
    thus ‹(s, Z) ∈ ℱ ?rhs›
    proof (elim disjE exE conjE)
      assume ‹t = []› and ‹X ∩ ev ` A = {}›
      from ‹t = []› assms(2, 3) emptyLeftProperty have ‹s = [] ∧ u = []›
        by (cases s; cases u; simp add: F_SKIP split: if_split_asm)
      with ‹X ∩ ev ` A = {}› show ‹(s, Z) ∈ ℱ ?rhs›
        by (auto simp add: F_Mprefix assms(4))
    next
      fix a t'
      assume ‹a ∈ A› ‹t = ev a # t'› ‹(t', X) ∈ ℱ (P a)›
      from assms(2, 3) ‹t = ev a # t'› obtain s'
        where * : ‹a ∉ S› ‹s = ev a # s'› ‹s' setinterleaves ((t', u), range tick ∪ ev ` S)›
        by (simp add: F_SKIP, elim disjE; simp split: if_split_asm, blast)
      show ‹(s, Z) ∈ ℱ ?rhs›
        by (simp add: F_Mprefix ‹s = ev a # s'› ‹a ∈ A› ‹a ∉ S› F_Sync)
          (use "*"(3) ‹(t', X) ∈ ℱ (P a)› assms(2, 4) in blast)
    qed
  qed
next
  fix s Z
  assume same_div: ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, Z) ∈ ℱ ?rhs›
  hence ‹s = [] ∧ Z ∩ ev ` (A - S) = {} ∨ (∃a s'. a ∈ A ∧ a ∉ S ∧ s = ev a # s' ∧ (s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res))›
    by (simp add: F_Mprefix image_iff) blast
  thus ‹(s, Z) ∈ ℱ ?lhs›
  proof (elim disjE exE conjE)
    assume ‹s = []› and ‹Z ∩ ev ` (A - S) = {}›
    hence * : ‹([], Z - ev ` S) ∈ ℱ (□a ∈ A → P a) ∧ ([], Z - {tick res}) ∈ ℱ (SKIP res) ∧
               s setinterleaves (([], []), range tick ∪ ev ` S) ∧
               Z = (Z - ev ` S ∪ (Z - {tick res})) ∩ (range tick ∪ ev ` S) ∪ (Z - ev ` S) ∩ (Z - {tick res})›
      by (auto simp add: F_Mprefix F_SKIP)
    show ‹(s, Z) ∈ ℱ ?lhs› by (simp add: F_Sync) (metis "*")
  next  
    fix a s'
    assume ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res)›
    from ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res)› consider ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res)›
      | t u X Y where ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res)›
        ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
        ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
      by (simp add: F_Sync D_Sync) blast
    thus ‹(s, Z) ∈ ℱ ?lhs›
    proof cases
      assume ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res)›
      with ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› have ‹s ∈ 𝒟 ?rhs› by (simp add: D_Mprefix)
      with same_div D_F show ‹(s, Z) ∈ ℱ ?lhs› by blast
    next
      fix t u X Y
      assume assms: ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res)›
        ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
        ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
      hence ‹(ev a # t, X) ∈ ℱ (□a∈ A → P a) ∧ s setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
        by (simp add: F_SKIP F_Mprefix ‹s = ev a # s'›, elim disjE)
          (simp_all add: ‹a ∈ A› ‹a ∉ S› image_iff)
      with assms(2, 4) show ‹(s, Z) ∈ ℱ ?lhs› by (simp add: F_Sync) blast
    qed
  qed
qed

lemma SKIP_Sync_Mprefix : ‹SKIP res ⟦S⟧ (□b ∈ B → P b) = □b ∈ (B - S) → (SKIP res ⟦S⟧ P b)›
  by (metis (no_types, lifting) Mprefix_Sync_SKIP Sync_commute mono_Mprefix_eq)



(* TODO: probably not true, see if we put SKIPS definition in Assertions again  *)
(* lemma Renaming_is_SKIP_iff : ‹Renaming P f g = SKIP s ⟷ (∃R. P = SKIPS R ∧ g ` R = {s})›
proof (intro iffI exI conjI)
  show ‹∃R. P = SKIPS R ∧ g ` R = {s} ⟹ Renaming P f g = SKIP s›
    apply (elim exE conjE, clarify)
    apply (simp add: Process_eq_spec F_Renaming D_Renaming F_SKIPS D_SKIPS F_SKIP D_SKIP )
    by (safe, auto) (metis imageE map_renaming_fun_eq_tick_iff singletonI)
next
  assume ‹Renaming P f g = SKIP s›
  from this[THEN arg_cong[where f = 𝒟]] have ‹𝒟 P = {}›
    by (simp add: D_SKIP D_Renaming)
       (metis D_imp_front_tickFree equals0I front_tickFree_Nil front_tickFree_append_iff
              is_processT9 list.distinct(1) nonTickFree_n_frontTickFree)
  define R where ‹R ≡ {r. [✓(r)] ∈ 𝒯 P ∧ g r = s}›
  from ‹Renaming P f g = SKIP s›[THEN arg_cong[where f = 𝒯]] have ‹R ≠ {}›
    by (simp add: T_Renaming ‹𝒟 P = {}› T_SKIP R_def set_eq_iff)
       (metis (no_types, opaque_lifting) map_renaming_fun_eq_tick_iff)

  thus ‹g ` R = {s}› by (auto simp add: R_def)

  show ‹P = SKIPS R›
  proof (subst Process_eq_spec, safe)
    show ‹u ∈ 𝒟 P ⟹ u ∈ 𝒟 (SKIPS R)›
     and ‹u ∈ 𝒟 (SKIPS R) ⟹ u ∈ 𝒟 P› for u by (simp_all add: ‹𝒟 P = {}› D_SKIPS)
  next
    show ‹(u, X) ∈ ℱ (SKIPS R) ⟹ (u, X) ∈ ℱ P› for u X
      by (simp add: F_SKIPS ‹R ≠ {}›, simp add: R_def)
         (metis append_Nil is_processT6_TR_notin tick_T_F)
  next
    fix u X assume ‹(u, X) ∈ ℱ P›
    from this[THEN F_T] ‹Renaming P f g = SKIP s›[THEN arg_cong[where f = 𝒯]]
    consider ‹u = []› | r where ‹u = [✓(r)]›
      by (simp add: Process_eq_spec T_Renaming ‹𝒟 P = {}› T_SKIP set_eq_iff)
         (metis Nil_is_map_conv map_renaming_fun_eq_tick_iff)
    thus ‹(u, X) ∈ ℱ (SKIPS R)›
    proof cases
      assume ‹u = []›
      find_theorems ‹?S = ?t ⟹ ?S ⊆ ?t›
      from ‹Renaming P f g = SKIP s›
           [THEN arg_cong[where f = ℱ], THEN equalityD1, THEN set_mp, of ‹([], renaming_fun f g ` X)›]
      have ‹∃r∈R. ✓(r) ∉ X›
        apply (auto simp add: F_Renaming ‹𝒟 P = {}› F_SKIP subset_iff vimage_image_eq)
        apply (auto simp add: renaming_fun_def event⇩p⇩t⇩i⇩c⇩k.case_eq_if image_iff split: if_splits)
        find_theorems image vimage
        sledgehammer
        apply (simp add: F_Renaming ‹𝒟 P = {}› F_SKIP)
      have ‹(u, X) ∈ ℱ (SKIPS R)›
        apply (simp add: F_SKIPS ‹R ≠ {}›)


      oops
      show ‹u = [] ⟹ (u, X) ∈ ℱ (SKIPS R)›
        sledgehammer
  
      oops
    consider ‹u = []› ‹(tick ` R) ∩ X = {}› | r where ‹g r = s› ‹u = [✓(r)]›
      apply (cases u; auto simp add: Process_eq_spec F_Renaming ‹𝒟 P = {}› F_SKIP disjoint_iff set_eq_iff image_iff R_def vimage_def)
      sledgehammer
    from ‹Renaming P f g = SKIP s›[THEN arg_cong[where f = ℱ]] show ‹ℱ P = ℱ (SKIPS R)›
      apply (simp add: F_Renaming ‹𝒟 P = {}› F_SKIPS ‹R ≠ {}› F_SKIP)
      apply (simp add: R_def set_eq_iff, safe)
         apply simp_all
      sledgehammer defer sledgehammer defer sledgehammer defer sledgehammer
    
  proof (rule conjI)
    from ‹Renaming P f g = SKIP s›[THEN arg_cong[where f = 𝒯]]
    show ‹g ` R = {s}›
      apply (simp add: T_Renaming ‹𝒟 P = {}› T_SKIP set_eq_iff image_iff)
      sledgehammer
  
      sledgehammer
  
  from ‹Renaming P f g = SKIP s›[THEN arg_cong[where f = ℱ]]
  have ‹(u, X) ∈ ℱ (Renaming P f g) ⟷ u = [✓(s)] ∨ u = [] ∧ ✓(s) ∉ X› for u X
    by (auto simp add: F_SKIP)
  hence ‹(∃v. u = map (renaming_fun f g) v ∧ (v, renaming_fun f g -` X) ∈ ℱ P) ⟷
         u = [✓(s)] ∨ u = [] ∧ ✓(s) ∉ X› for u X
    by (simp add: F_Renaming ‹𝒟 P = {}›)
  thm this[simplified F_Renaming ‹𝒟 P = {}›, simplified]
    thm F_SKIP
  have ‹∀a b. (∃s1. a = map (renaming_fun f g) s1 ∧
                (∃X. (∀x. (x ∈ b) = (x ∈ X)) ∧ (s1, renaming_fun f g -` X) ∈ ℱ P)) =
          (a = [] ∧ (∃X. (∀x. (x ∈ b) = (x ∈ X)) ∧ ✓(s) ∉ X) ∨ a = [✓(s)])›
    by (simp add: F_Renaming F_SKIP ‹𝒟 P = {}› set_eq_iff)

  oops
  have ‹∃r. P = SKIP r ∧ g r = s›
    apply (simp add: F_Renaming F_SKIP ‹𝒟 P = {}› set_eq_iff)
    apply (subst Process_eq_spec, simp add: Process_eq_spec F_SKIP D_SKIP)
    sledgehammer
  show ‹∃r. P = SKIP r ∧ g r = s› if ‹Renaming P f g = SKIP s›
    apply (simp add: Process_eq_spec F_Renaming D_Renaming F_SKIP D_SKIP)
    apply safe
    apply (meson front_tickFree_Nil)
     defer sledgehammer


    oops
    apply (simp add: set_eq_iff)

    oops
  apply (simp add: Process_eq_spec F_Renaming F_SKIP D_Renaming D_SKIP)
  sledgehammer *)


lemma Renaming_SKIP [simp] : ‹Renaming (SKIP r) f g = SKIP (g r)›
  by (force simp add: Process_eq_spec F_Renaming F_SKIP D_Renaming D_SKIP)



subsubsection ‹Associative Operators›

lemma Det_assoc: ‹P □ (Q □ R) = P □ Q □ R›
  by (auto simp add: Process_eq_spec D_Det F_Det T_Det)


lemma Ndet_assoc: ‹P ⊓ (Q ⊓ R) = P ⊓ Q ⊓ R›
  by (auto simp add: Process_eq_spec D_Ndet F_Ndet)


lemma Sliding_assoc: ‹P ⊳ (Q ⊳ R) = P ⊳ Q ⊳ R›
  by (auto simp add: Process_eq_spec F_Sliding D_Sliding T_Sliding)


lemma Seq_assoc : ‹P ❙; (Q ❙; R) = P ❙; Q ❙; R›
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 (P ❙; (Q ❙; R)) ⟹ t ∈ 𝒟 (P ❙; Q ❙; R)› for t
    by (simp add: D_Seq T_Seq_bis) (metis append.assoc)
next
  fix t assume ‹t ∈ 𝒟 (P ❙; Q ❙; R)›
  then consider ‹t ∈ 𝒟 (P ❙; Q)› 
    | u v r where ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P ❙; Q)› ‹v ∈ 𝒟 R›
    by (simp add: D_Seq) blast
  thus ‹t ∈ 𝒟 (P ❙; (Q ❙; R))›
  proof cases
    show ‹t ∈ 𝒟 (P ❙; Q) ⟹ t ∈ 𝒟 (P ❙; (Q ❙; R))› by (auto simp add: D_Seq)
  next
    fix u v r assume ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P ❙; Q)› ‹v ∈ 𝒟 R›
    from ‹u @ [✓(r)] ∈ 𝒯 (P ❙; Q)› consider ‹u @ [✓(r)] ∈ 𝒟 P›
      | w x s where ‹u @ [✓(r)] = w @ x› ‹w @ [✓(s)] ∈ 𝒯 P› ‹x ∈ 𝒯 Q›
      by (simp add: T_Seq_bis) blast
    thus ‹t ∈ 𝒟 (P ❙; (Q ❙; R))›
    proof cases
      from ‹v ∈ 𝒟 R› show ‹u @ [✓(r)] ∈ 𝒟 P ⟹ t ∈ 𝒟 (P ❙; (Q ❙; R))›
        by (simp add: D_Seq ‹t = u @ v›)
          (metis D_imp_front_tickFree butlast_snoc is_processT7 is_processT9
            front_tickFree_iff_tickFree_butlast)
    next
      from ‹v ∈ 𝒟 R› show ‹⟦u @ [✓(r)] = w @ x; w @ [✓(s)] ∈ 𝒯 P; x ∈ 𝒯 Q⟧ ⟹ t ∈ 𝒟 (P ❙; (Q ❙; R))› for w x s
        by (cases x rule: rev_cases, simp_all add: D_Seq ‹t = u @ v›)
          (meson append_T_imp_tickFree non_tickFree_tick not_Cons_self2 tickFree_append_iff, blast)
    qed
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ (P ❙; (Q ❙; R))› ‹t ∉ 𝒟 (P ❙; Q ❙; R)› ‹t ∉ 𝒟 (P ❙; Q ❙; R)›
  then consider ‹(t, X ∪ range tick) ∈ ℱ P› ‹tF t›
    | u v r where ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹(v, X) ∈ ℱ (Q ❙; R)›
    unfolding Seq_projs by simp metis
  thus ‹(t, X) ∈ ℱ (P ❙; Q ❙; R)›
  proof cases
    show ‹(t, X ∪ range tick) ∈ ℱ P ⟹ tF t ⟹ (t, X) ∈ ℱ (P ❙; Q ❙; R)›
      by (simp add: F_Seq)
  next
    fix u v r assume ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹(v, X) ∈ ℱ (Q ❙; R)›
    with ‹t ∉ 𝒟 (P ❙; Q ❙; R)› consider ‹(v, X ∪ range tick) ∈ ℱ Q› ‹tF v›
      | w x s where ‹v = w @ x› ‹w @ [✓(s)] ∈ 𝒯 Q› ‹(x, X) ∈ ℱ R›
      unfolding Seq_projs by fast
    thus ‹(t, X) ∈ ℱ (P ❙; Q ❙; R)›
    proof cases
      show ‹(v, X ∪ range tick) ∈ ℱ Q ⟹ tF v ⟹ (t, X) ∈ ℱ (P ❙; Q ❙; R)›
        by (simp add: ‹t = u @ v› F_Seq)
          (metis ‹u @ [✓(r)] ∈ 𝒯 P› append_T_imp_tickFree list.discI)
    next
      show ‹v = w @ x ⟹ w @ [✓(s)] ∈ 𝒯 Q ⟹ (x, X) ∈ ℱ R ⟹ (t, X) ∈ ℱ (P ❙; Q ❙; R)› for w x s
        by (simp add: ‹t = u @ v› F_Seq T_Seq_bis) (metis ‹u @ [✓(r)] ∈ 𝒯 P› append_assoc)
    qed
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ (P ❙; Q ❙; R)› ‹t ∉ 𝒟 (P ❙; Q ❙; R)› ‹t ∉ 𝒟 (P ❙; (Q ❙; R))›
  then consider ‹(t, X ∪ range tick) ∈ ℱ (P ❙; Q)› ‹tF t›
    | u v r where ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P ❙; Q)› ‹(v, X) ∈ ℱ R›
    unfolding Seq_projs[of ‹P ❙; Q›] by blast
  thus ‹(t, X) ∈ ℱ (P ❙; (Q ❙; R))›
  proof cases
    show ‹(t, X ∪ range tick) ∈ ℱ (P ❙; Q) ⟹ tF t ⟹ (t, X) ∈ ℱ (P ❙; (Q ❙; R))›
      by (simp add: F_Seq) (metis tickFree_append_iff)
  next
    fix u v r assume ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P ❙; Q)› ‹(v, X) ∈ ℱ R›
    with ‹t ∉ 𝒟 (P ❙; (Q ❙; R))› obtain w x s
      where ‹u @ [✓(r)] = w @ x› ‹w @ [✓(s)] ∈ 𝒯 P› ‹x ∈ 𝒯 Q›
      by (simp add: D_Seq T_Seq)
        (meson F_imp_front_tickFree ‹u @ [✓(r)] ∈ 𝒯 (P ❙; Q)›
          append_T_imp_tickFree is_processT7 is_processT9 not_Cons_self2)
    with ‹(v, X) ∈ ℱ R› show ‹(t, X) ∈ ℱ (P ❙; (Q ❙; R))›
      by (cases x rule: rev_cases, simp_all add: ‹t = u @ v› F_Seq)
        (metis append_T_imp_tickFree non_tickFree_tick
          not_Cons_self2 tickFree_append_iff, blast)
  qed
qed



subsubsection ‹Synchronization›


lemma interleave_set: ‹s setinterleaves ((t, u), C) ⟹ set t ∪ set u ⊆ set s›
  by (induct ‹(t, C, u)› arbitrary: t u s rule: setinterleaving.induct)
    (simp split: if_split_asm; meson dual_order.trans list.set_intros set_subset_Cons)+


lemma interleave_order: ‹s setinterleaves ((t1 @ t2, u), C) ⟹ set t2 ⊆ set (drop (length t1) s)›
proof (induct ‹(t1, C, u)› arbitrary: t1 u s rule: setinterleaving.induct)
  case 1
  with emptyRightProperty show ?case by auto
next
  case (2 y u)
  with interleave_set show ?case by simp blast
next
  case (3 x t1)
  thus ?case by (simp split: if_split_asm) (metis drop_Suc_Cons)
next
  case (4 x t1 y u)
  thus ?case
    apply (simp split: if_split_asm)
       apply (metis drop_Suc_Cons)
      apply (metis (mono_tags, opaque_lifting) drop_Suc_Cons dual_order.refl le_SucI set_drop_subset_set_drop subset_trans)
     apply (metis (no_types, opaque_lifting) drop_Suc_Cons dual_order.trans le_SucI order_refl set_drop_subset_set_drop)
    by (metis drop_Suc_Cons)
qed


lemma interleave_append_left : 
  ‹s setinterleaves ((t1 @ t2, u), C) ⟹
   ∃u1 u2 s1 s2. u = u1 @ u2 ∧ s = s1 @ s2 ∧
                 s1 setinterleaves ((t1, u1), C) ∧ s2 setinterleaves ((t2, u2), C)›
proof (induct ‹(t1, C, u)› arbitrary: t1 u s rule: setinterleaving.induct)
  case 1
  thus ?case by simp
next
  case (2 y u)
  thus ?case by (metis si_empty1 append_Nil singletonI)
next
  case (3 x t1)
  thus ?case by (simp split: if_split_asm) (metis append_Cons)
next
  case (4 x t1 y u)
  from "4.prems" consider v where ‹x ∈ C› ‹y ∈ C› ‹x = y› ‹s = y # v› ‹v setinterleaves ((t1 @ t2, u), C)›
    | v where ‹x ∈ C› ‹y ∉ C› ‹s = y # v› ‹v setinterleaves (((x # t1) @ t2, u), C)›
    | v where ‹x ∉ C› ‹y ∉ C› ‹s = x # v› ‹v setinterleaves ((t1 @ t2, y # u), C)›
    | v where ‹x ∉ C› ‹y ∉ C› ‹s = y # v› ‹v setinterleaves (((x # t1) @ t2, u), C)›
    | v where ‹x ∉ C› ‹y ∈ C› ‹s = x # v› ‹v setinterleaves ((t1 @ t2, y # u), C)›
    by (auto split: if_split_asm)
  thus ?case
  proof cases
    fix v assume * : ‹x ∈ C› ‹y ∈ C› ‹x = y› ‹s = y # v› ‹v setinterleaves ((t1 @ t2, u), C)›
    from "4.hyps"(1)[OF "*"(1, 2, 3, 5)] obtain u1 u2 s1 s2
      where ** : ‹u = u1 @ u2› ‹v = s1 @ s2› ‹s1 setinterleaves ((t1, u1), C)›
        ‹s2 setinterleaves ((t2, u2), C)› by blast
    show ?case
      apply (rule exI[of _ ‹y # u1›], rule exI[of _ u2])
      apply (rule exI[of _ ‹y # s1›], rule exI[of _ s2])
      by (simp add: "*"(2, 3, 4) "**")
  next
    fix v assume * : ‹x ∈ C› ‹y ∉ C› ‹s = y # v› ‹v setinterleaves (((x # t1) @ t2, u), C)›
    from "4.hyps"(2)[OF "*"(1, 2, 4)] obtain u1 u2 s1 s2
      where ** : ‹u = u1 @ u2› ‹v = s1 @ s2› ‹s1 setinterleaves ((x # t1, u1), C)›
        ‹s2 setinterleaves ((t2, u2), C)› by blast
    show ?case
      apply (rule exI[of _ ‹y # u1›], rule exI[of _ u2])
      apply (rule exI[of _ ‹y # s1›], rule exI[of _ s2])
      by (simp add: "*"(1, 2, 3) "**")
  next
    fix v assume * : ‹x ∉ C› ‹y ∉ C› ‹s = x # v› ‹v setinterleaves ((t1 @ t2, y # u), C)›
    from "4.hyps"(3)[OF "*"(1, 2, 4)] obtain u1 u2 s1 s2
      where ** : ‹y # u = u1 @ u2› ‹v = s1 @ s2› ‹s1 setinterleaves ((t1, u1), C)›
        ‹s2 setinterleaves ((t2, u2), C)› by blast
    show ?case
      apply (rule exI[of _ ‹u1›],     rule exI[of _ u2])
      apply (rule exI[of _ ‹x # s1›], rule exI[of _ s2])
      by (cases u1) (use "**" in ‹simp_all add: "*"(1, 2, 3)›)
  next
    fix v assume * : ‹x ∉ C› ‹y ∉ C› ‹s = y # v› ‹v setinterleaves (((x # t1) @ t2, u), C)›
    from "4.hyps"(4)[OF "*"(1, 2, 4)] obtain u1 u2 s1 s2
      where ** : ‹u = u1 @ u2› ‹v = s1 @ s2› ‹s1 setinterleaves ((x # t1, u1), C)›
        ‹s2 setinterleaves ((t2, u2), C)› by blast
    show ?case
      apply (rule exI[of _ ‹y # u1›], rule exI[of _ u2])
      apply (rule exI[of _ ‹y # s1›], rule exI[of _ s2])
      by (simp add: "*"(1, 2, 3) "**")
  next
    fix v assume * : ‹x ∉ C› ‹y ∈ C› ‹s = x # v› ‹v setinterleaves ((t1 @ t2, y # u), C)›
    from "4.hyps"(5)[simplified, OF "*"(1, 2, 4)] obtain u1 u2 s1 s2
      where ** : ‹y # u = u1 @ u2› ‹v = s1 @ s2› ‹s1 setinterleaves ((t1, u1), C)›
        ‹s2 setinterleaves ((t2, u2), C)› by blast
    show ?case
      apply (rule exI[of _ ‹u1›],     rule exI[of _ u2])
      apply (rule exI[of _ ‹x # s1›], rule exI[of _ s2])
      by (cases u1) (use "**" in ‹simp_all add: "*"(1, 2, 3)›)
  qed
qed


lemma interleave_append_right : 
  ‹s setinterleaves ((t, u1 @ u2), C) ⟹
   ∃t1 t2 s1 s2. t = t1 @ t2 ∧ s = s1 @ s2 ∧
                 s1 setinterleaves ((t1, u1), C) ∧ s2 setinterleaves ((t2, u2), C)›
  by (subst (asm) setinterleaving_sym, drule interleave_append_left)
    (simp add: setinterleaving_sym)

lemma interleave_append_tail_left: 
  ‹s setinterleaves ((t1, u), C) ⟹ set t2 ∩ C = {} ⟹ (s @ t2) setinterleaves ((t1 @ t2, u), C)›
  by (induct ‹(t1, C, u)› arbitrary: t1 t2 u s rule: setinterleaving.induct,
      auto split: if_split_asm)
    (metis disjoint_iff emptyLeftSelf setinterleaving_sym,
      metis SyncSingleHeadAdd setinterleaving_sym)


lemma interleave_append_tail_right: 
  ‹s setinterleaves ((t, u1), C) ⟹ set u2 ∩ C = {} ⟹ (s @ u2) setinterleaves ((t, u1 @ u2), C)›
  by (metis (no_types) setinterleaving_sym interleave_append_tail_left)



lemma interleave_assoc_1: 
  ‹⟦tu setinterleaves ((t, u), A); tuv setinterleaves ((tu, v), A)⟧ ⟹
   ∃uv. uv setinterleaves ((u, v), A) ∧ tuv setinterleaves ((t, uv), A)›
proof (induct ‹(tu, A, v)› arbitrary: t u tu v tuv rule: setinterleaving.induct)
  case 1
  with emptyLeftProperty empty_setinterleaving show ?case by blast
next
  case (2 z v)
  from "2.prems"(2) emptyLeftProperty have ‹tuv = z # v› by blast
  with "2.prems" empty_setinterleaving setinterleaving_sym show ?case by blast
next
  case (3 y tu)
  from "3.prems"(2) emptyRightProperty have ‹tuv = y # tu› by blast
  with "3.prems" show ?case
    by (metis (no_types) EmptyLeftSync Un_iff disjoint_iff
        emptyLeftSelf interleave_set setinterleaving_sym subsetD)
next
  case (4 y tu z v)
  consider ‹y ∈ A› ‹z ∈ A› | ‹y ∈ A› ‹z ∉ A› | ‹y ∉ A› ‹z ∈ A› | ‹y ∉ A› ‹z ∉ A› by blast
  thus ?case
  proof cases
    assume ‹y ∈ A› and ‹z ∈ A›
    with "4.prems"(2) obtain tuv'
      where ‹y = z› ‹tuv = y # tuv'› ‹tuv' setinterleaves ((tu, v), A)›
      by (simp split: if_split_asm) blast
    from ‹tuv = y # tuv'› ‹y = z› ‹z ∈ A› "4.prems"(1)
      "4.hyps"(1)[OF ‹y ∈ A› ‹z ∈ A› ‹y = z› _ ‹tuv' setinterleaves ((tu, v), A)›]
    show ?case by (induct ‹(t, A, u)› arbitrary: t u tu rule: setinterleaving.induct;
          fastforce split: if_split_asm)
  next
    assume ‹y ∈ A› and ‹z ∉ A›
    with "4.prems"(2) obtain tuv'
      where ‹tuv = z # tuv'› ‹tuv' setinterleaves ((y # tu, v), A)›
      by (simp split: if_split_asm) blast
    from ‹y ∈ A› and ‹z ∉ A› ‹tuv = z # tuv'› "4.prems"(1)
      "4.hyps"(2)[OF _ _ _ ‹tuv' setinterleaves ((y # tu, v), A)›]
    show ?case
      apply (cases ‹(t, A, u)› rule: setinterleaving.cases; simp split: if_split_asm)
      by (metis "4.prems"(1) SyncHdAdd list.distinct(1) list.sel(1, 3)) fastforce
  next
    assume ‹y ∉ A› and ‹z ∈ A›
    with "4.prems"(2) obtain tuv'
      where ‹tuv = y # tuv'› ‹tuv' setinterleaves ((tu, z # v), A)›
      by (simp split: if_split_asm) blast
    from ‹y ∉ A› ‹z ∈ A› ‹tuv = y # tuv'› "4.prems"(1)
      "4.hyps"(5)[OF _ _ _ ‹tuv' setinterleaves ((tu, z # v), A)›]
    show ?case by (cases ‹(t, A, u)› rule: setinterleaving.cases; fastforce split: if_split_asm)
  next
    assume ‹y ∉ A› and ‹z ∉ A›
    with "4.prems"(2) obtain tuv'
      where ‹tuv = y # tuv' ∧ tuv' setinterleaves ((tu, z # v), A) ∨
             tuv = z # tuv' ∧ tuv' setinterleaves ((y # tu, v), A)› by auto
    thus ?case
    proof (elim disjE conjE)      
      assume ‹tuv = y # tuv'› ‹tuv' setinterleaves ((tu, z # v), A)›
      show ?case
      proof (cases ‹(t, A, u)› rule: setinterleaving.cases)
        from "4.prems"(1) show ‹(t, A, u) = ([], X, []) ⟹ ?case› for X by simp
      next
        show ‹(t, A, u) = ([], X, y' # u') ⟹ ?case› for X y' u'
          by (metis "4.prems"(1) "4.prems"(2) Pair_inject emptyLeftProperty
              emptyLeftSelf empty_iff empty_set ftf_Sync1 ftf_Sync21)
      next
        show ‹(t, A, u) = (x' # t', X, []) ⟹ ?case› for X x' t'
          by (metis (no_types, lifting) "4.prems" Nil_in_shufflesI Pair_inject si_empty1
              emptyLeftNonSync emptyLeftSelf emptyRightProperty ftf_Sync21 shuffles.simps(1))
      next
        fix X x' t' y' u'
        assume ‹(t, A, u) = (x' # t', X, y' # u')›
        hence ‹t = x' # t'› ‹u = y' # u'› ‹X = A› by simp_all
        consider ‹x' ∈ A› ‹y' ∈ A› | ‹x' ∈ A› ‹y' ∉ A›
          | ‹x' ∉ A› ‹y' ∈ A› | ‹x' ∉ A› ‹y' ∉ A› by blast
        thus ?case
        proof cases
          assume ‹x' ∈ A› ‹y' ∈ A›
          with "4.prems"(1) ‹t = x' # t'› ‹u = y' # u'› ‹y ∉ A› have False
            by (metis SyncSameHdTl list.sel(1))
          thus ?case by simp
        next
          assume ‹x' ∈ A› ‹y' ∉ A›
          with "4.prems"(1) ‹t = x' # t'› ‹u = y' # u'›
          have ‹y' = y› ‹tu setinterleaves ((x' # t', u'), A)› by simp_all
          from "4.hyps"(3)[OF ‹y ∉ A› ‹z ∉ A› this(2) ‹tuv' setinterleaves ((tu, z # v), A)›]
          obtain uv where ‹uv setinterleaves ((u', z # v), A) ∧
                           tuv' setinterleaves ((x' # t', uv), A)› ..
          hence ‹(y # uv) setinterleaves ((u, z # v), A) ∧ tuv setinterleaves ((t, y # uv), A)›
            by (simp add: ‹u = y' # u'› ‹z ∉ A› ‹y' = y› ‹y ∉ A› ‹t = x' # t'› ‹tuv = y # tuv'›)
          thus ?case by blast
        next
          assume ‹x' ∉ A› ‹y' ∈ A›
          with "4.prems"(1) ‹t = x' # t'› ‹u = y' # u'›
          have ‹x' = y› ‹tu setinterleaves ((t', y' # u'), A)› by simp_all
          from "4.hyps"(3)[OF ‹y ∉ A› ‹z ∉ A› this(2) ‹tuv' setinterleaves ((tu, z # v), A)›]
          obtain uv where ‹uv setinterleaves ((y' # u', z # v), A) ∧
                           tuv' setinterleaves ((t', uv), A)› ..
          hence ‹uv setinterleaves ((u, z # v), A) ∧ tuv setinterleaves ((t, uv), A)›
            by (simp add: ‹tuv = y # tuv'› ‹u = y' # u'› ‹z ∉ A›
                ‹t = x' # t'› ‹x' = y› ‹y ∉ A› SyncSingleHeadAdd)
          thus ?case by blast
        next
          assume ‹x' ∉ A› ‹y' ∉ A›
          with "4.prems"(1) ‹t = x' # t'› ‹u = y' # u'›
          have ‹x' = y ∧ tu setinterleaves ((t', y' # u'), A) ∨
                y' = y ∧ tu setinterleaves ((x' # t', u'), A)› by auto
          thus ?case
          proof (elim disjE conjE)
            assume ‹x' = y› ‹tu setinterleaves ((t', y' # u'), A)›
            from "4.hyps"(3)[OF ‹y ∉ A› ‹z ∉ A› this(2) ‹tuv' setinterleaves ((tu, z # v), A)›]
            obtain uv where ‹uv setinterleaves ((y' # u', z # v), A) ∧
                             tuv' setinterleaves ((t', uv), A)› ..
            hence ‹uv setinterleaves ((u, z # v), A) ∧ tuv setinterleaves ((t, uv), A)›
              by (simp add: ‹x' = y› ‹y ∉ A› ‹t = x' # t'›
                  ‹tuv = y # tuv'› ‹u = y' # u'› SyncSingleHeadAdd)
            thus ?case by blast
          next
            assume ‹y' = y› ‹tu setinterleaves ((x' # t', u'), A)›
            from "4.hyps"(3)[OF ‹y ∉ A› ‹z ∉ A› this(2) ‹tuv' setinterleaves ((tu, z # v), A)›]
            obtain uv where ‹uv setinterleaves ((u', z # v), A) ∧
                             tuv' setinterleaves ((x' # t', uv), A)› ..
            hence ‹(y # uv) setinterleaves ((u, z # v), A) ∧ tuv setinterleaves ((t, y # uv), A)›
              by (simp add: ‹u = y' # u'› ‹y' = y› ‹y ∉ A› ‹z ∉ A› ‹t = x' # t'› ‹tuv = y # tuv'›)
            thus ?case by blast
          qed
        qed
      qed
    next
      assume ‹tuv = z # tuv'› ‹tuv' setinterleaves ((y # tu, v), A)›
      from "4.hyps"(4)[OF ‹y ∉ A› ‹z ∉ A› "4.prems"(1) ‹tuv' setinterleaves ((y # tu, v), A)›]
      obtain uv where ‹uv setinterleaves ((u, v), A) ∧ tuv' setinterleaves ((t, uv), A)› ..
      hence ‹(z # uv) setinterleaves ((u, z # v), A) ∧ tuv setinterleaves ((t, z # uv), A)›
        by (cases u; cases t) (simp_all add: ‹z ∉ A› ‹tuv = z # tuv'›)
      thus ?case by blast
    qed
  qed
qed 


lemma interleave_assoc_2:
  assumes  *:‹uv setinterleaves ((u, v), A)› and 
    **:‹tuv setinterleaves ((t, uv), A)›
  shows ‹∃tu. tu setinterleaves ((t, u), A) ∧ tuv setinterleaves ((tu, v), A)›
  using "*" "**" setinterleaving_sym interleave_assoc_1 by blast



theorem Sync_assoc: ‹P ⟦S⟧ (Q ⟦S⟧ R) = P ⟦S⟧ Q ⟦S⟧ R› for P Q R :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof (rule FD_antisym)
  show ‹P ⟦S⟧ (Q ⟦S⟧ R) ⊑⇩F⇩D P ⟦S⟧ Q ⟦S⟧ R› for P Q R :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  proof (rule failure_divergence_refine_optimizedI)
    fix s assume ‹s ∈ 𝒟 (P ⟦S⟧ Q ⟦S⟧ R)›
    from this[simplified D_Sync[of ‹P ⟦S⟧ Q›]] obtain t u r v
      where * : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹s = r @ v› 
        ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
        ‹t ∈ 𝒟 (P ⟦S⟧ Q) ∧ u ∈ 𝒯 R ∨ t ∈ 𝒟 R ∧ u ∈ 𝒯 (P ⟦S⟧ Q) - 𝒟 (P ⟦S⟧ Q)›
      by simp (metis D_T setinterleaving_sym)
    from "*"(5) show ‹s ∈ 𝒟 (P ⟦S⟧ (Q ⟦S⟧ R))›
    proof (elim disjE conjE)
      assume ‹t ∈ 𝒟 R› and ‹u ∈ 𝒯 (P ⟦S⟧ Q) - 𝒟 (P ⟦S⟧ Q)›
      from ‹u ∈ 𝒯 (P ⟦S⟧ Q) - 𝒟 (P ⟦S⟧ Q)› obtain t1 u1
        where ** : ‹u setinterleaves ((t1, u1), range tick ∪ ev ` S)›
          ‹t1 ∈ 𝒯 P› ‹u1 ∈ 𝒯 Q› by (simp add: D_Sync T_Sync) blast
      from interleave_assoc_1[OF "**"(1)] obtain uv
        where *** : ‹uv setinterleaves ((u1, t), range tick ∪ ev ` S)›
          ‹r setinterleaves ((t1, uv), range tick ∪ ev ` S)›
        using "*"(4) setinterleaving_sym by blast
      from "***"(1) setinterleaving_sym ‹t ∈ 𝒟 R› ‹u1 ∈ 𝒯 Q› front_tickFree_Nil
      have ‹uv ∈ 𝒟 (Q ⟦S⟧ R)› unfolding D_Sync by blast
      with "*"(1, 2, 3) "**"(2) "***"(2) setinterleaving_sym
      show ‹s ∈ 𝒟 (P ⟦S⟧ (Q ⟦S⟧ R))› by (subst D_Sync) blast
    next
      assume ‹t ∈ 𝒟 (P ⟦S⟧ Q)› and ‹u ∈ 𝒯 R›
      from ‹t ∈ 𝒟 (P ⟦S⟧ Q)› obtain t1 u1 r1 v1
        where ** : ‹front_tickFree v1› ‹tickFree r1 ∨ v1 = []› ‹t = r1 @ v1›
          ‹r1 setinterleaves ((t1, u1), range tick ∪ ev ` S)›
          ‹t1 ∈ 𝒟 P ∧ u1 ∈ 𝒯 Q ∨ t1 ∈ 𝒟 Q ∧ u1 ∈ 𝒯 P›
        by (simp add: D_Sync) blast
      from interleave_append_left[OF "*"(4)[unfolded "**"(3)]] obtain r' r'' u' u''
        where *** : ‹r' setinterleaves ((r1, u'), range tick ∪ ev ` S)›
          ‹r = r' @ r''› ‹u = u' @ u''› by blast
      have ‹u' ∈ 𝒯 R› by (metis "***"(3) prefixI ‹u ∈ 𝒯 R› is_processT3_TR)
      have $ : ‹front_tickFree (r'' @ v)›
        by (metis "*"(3) "***"(2) D_imp_front_tickFree ‹s ∈ 𝒟 (P ⟦S⟧ Q ⟦S⟧ R)›
            front_tickFree_append_iff front_tickFree_charn tickFree_append_iff)
      have $$ : ‹tickFree r' ∨ r'' @ v = []›
        by (metis "*"(3) "***"(2) D_imp_front_tickFree ‹s ∈ 𝒟 (P ⟦S⟧ Q ⟦S⟧ R)›
            append.right_neutral front_tickFree_append_iff tickFree_append_iff)
      have $$$ : ‹s = r' @ r'' @ v› by (simp add: "*"(3) "***"(2))

      from "**"(5) show ‹s ∈ 𝒟 (P ⟦S⟧ (Q ⟦S⟧ R))›
      proof (elim disjE conjE)
        assume ‹t1 ∈ 𝒟 P› and ‹u1 ∈ 𝒯 Q›
        from interleave_assoc_1[OF "**"(4) "***"(1)] obtain uv
          where **** : ‹uv setinterleaves ((u1, u'), range tick ∪ ev ` S)›
            ‹r' setinterleaves ((t1, uv), range tick ∪ ev ` S)› by blast
        from ‹u' ∈ 𝒯 R› "****"(1) ‹u1 ∈ 𝒯 Q› have ‹uv ∈ 𝒯 (Q ⟦S⟧ R)›
          unfolding T_Sync by blast
        with "$" "$$" "$$$" "****"(2) ‹t1 ∈ 𝒟 P›
        show ‹s ∈ 𝒟 (P ⟦S⟧ (Q ⟦S⟧ R))› unfolding D_Sync by blast
      next
        assume ‹t1 ∈ 𝒟 Q› ‹u1 ∈ 𝒯 P›
        from interleave_assoc_2[OF "**"(4)] "***"(1) setinterleaving_sym obtain tu
          where "****" : ‹tu setinterleaves ((u', t1), range tick ∪ ev ` S)›
            ‹r' setinterleaves ((tu, u1), range tick ∪ ev ` S)› by blast
        from ‹u' ∈ 𝒯 R› "****"(1)[unfolded setinterleaving_sym] front_tickFree_Nil ‹t1 ∈ 𝒟 Q›
        have ‹tu ∈ 𝒟 (Q ⟦S⟧ R)› unfolding D_Sync by blast
        with "$" "$$" "$$$" "****"(2) ‹u1 ∈ 𝒯 P›
        show ‹s ∈ 𝒟 (P ⟦S⟧ (Q ⟦S⟧ R))› unfolding D_Sync by blast
      qed
    qed
  next
    let ?Sync_set = ‹λX Y. (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
    assume subset_div : ‹𝒟 (P ⟦S⟧ Q ⟦S⟧ R) ⊆ 𝒟 (P ⟦S⟧ (Q ⟦S⟧ R))›
    fix s Z assume ‹(s, Z) ∈ ℱ (P ⟦S⟧ Q ⟦S⟧ R)›
    then consider (D) ‹s ∈ 𝒟 (P ⟦S⟧ Q ⟦S⟧ R)›
      | (F) t X u Y where ‹(t, X) ∈ ℱ (P ⟦S⟧ Q)› ‹(u, Y) ∈ ℱ R› ‹Z = ?Sync_set X Y›
        ‹s setinterleaves ((t, u), range tick ∪ ev ` S)›
      unfolding F_Sync D_Sync by blast
    thus ‹(s, Z) ∈ ℱ (P ⟦S⟧ (Q ⟦S⟧ R))›
    proof cases
      from subset_div D_F show ‹s ∈ 𝒟 (P ⟦S⟧ Q ⟦S⟧ R) ⟹ (s, Z) ∈ ℱ (P ⟦S⟧ (Q ⟦S⟧ R))› by blast
    next
      case F
      from "F"(1) consider (D1) ‹t ∈ 𝒟 (P ⟦S⟧ Q)›
        | (F1) t1 X1 u1 Y1 where ‹(t1, X1) ∈ ℱ P› ‹(u1, Y1) ∈ ℱ Q› ‹X = ?Sync_set X1 Y1›
          ‹t setinterleaves ((t1, u1), range tick ∪ ev ` S)›
        unfolding F_Sync D_Sync by blast
      thus ‹(s, Z) ∈ ℱ (P ⟦S⟧ (Q ⟦S⟧ R))›
      proof cases
        assume ‹t ∈ 𝒟 (P ⟦S⟧ Q)›
        with F(2) F(4) F_T front_tickFree_Nil
        have ‹s ∈ 𝒟 (P ⟦S⟧ Q ⟦S⟧ R)› unfolding D_Sync by blast
        with subset_div D_F show ‹(s, Z) ∈ ℱ (P ⟦S⟧ (Q ⟦S⟧ R))› by blast
      next
        case F1
        from interleave_assoc_1[OF F1(4) F(4)] obtain uv
          where * : ‹uv setinterleaves ((u1, u), range tick ∪ ev ` S)›
            ‹s setinterleaves ((t1, uv), range tick ∪ ev ` S)› by blast
        from "*"(1) F(2) F1(2) have ‹(uv, ?Sync_set Y1 Y) ∈ ℱ (Q ⟦S⟧ R)›
          unfolding F_Sync by blast
        with "*"(2) F1(1) have ‹(s, ?Sync_set X1 (?Sync_set Y1 Y)) ∈ ℱ (P ⟦S⟧ (Q ⟦S⟧ R))›
          by (subst F_Sync) blast
        also from F(3) F1(3) have ‹?Sync_set X1 (?Sync_set Y1 Y) = Z› by blast
        finally show ‹(s, Z) ∈ ℱ (P ⟦S⟧ (Q ⟦S⟧ R))› .
      qed
    qed
  qed
  thus ‹P ⟦S⟧ Q ⟦S⟧ R ⊑⇩F⇩D P ⟦S⟧ (Q ⟦S⟧ R)› by (metis Sync_commute)
qed


(*<*)
end
  (*>*)