Theory CSP_PTick_Laws

(***********************************************************************************
 * Copyright (c) 2025 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 ‹Other Laws›


(*<*)
theory CSP_PTick_Laws
  imports Multi_Sequential_Composition_Generalized
    Multi_Synchronization_Product_Generalized
    "HOL-CSP_RS" Step_CSP_PTick_Laws_Extended CSP_PTick_Monotonicities
begin
  (*>*)


unbundle option_type_syntax


section ‹Laws of Renaming›

subsection ‹Renaming and Sequential Composition›

lemma FD_Renaming_Seqptick :
  ‹Renaming P f g ;✓ (λg_r. ⊓r ∈ {r ∈ ✓s(P). g_r = g r}. Renaming (Q r) f g')
   ⊑FD Renaming (P ;✓ Q) f g'› (is ‹?lhs ⊑FD ?rhs›)
proof (rule failure_divergence_refine_optimizedI)
  fix s assume ‹s ∈ 𝒟 ?rhs›
  then obtain s1 s2 where * : ‹s = map (map_eventptick f g') s1 @ s2› ‹tF s1›
    ‹ftF s2› ‹s1 ∈ 𝒟 (P ;✓ Q)›
    unfolding D_Renaming by blast
  from "*"(4) consider (D_P) t1 t2 where ‹s1 = map (ev ∘ of_ev) t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1› ‹ftF t2›
    | (D_Q) t1 r t2 where ‹s1 = map (ev ∘ of_ev) t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹t1 ∉ 𝒟 P› ‹tF t1› ‹t2 ∈ 𝒟 (Q r)›
    by (simp add: Seqptick_projs) (metis D_imp_ftF)
  thus ‹s ∈ 𝒟 ?lhs›
  proof cases
    case D_P
    from D_P(2, 3) have ‹map (map_eventptick f g) t1 ∈ 𝒟 (Renaming P f g)›
      by (auto simp add: D_Renaming intro: ftF_Nil)
    hence ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) ∈ 𝒟 ?lhs›
      unfolding Seqptick_projs
      by (metis (mono_tags, lifting) ftF_Nil D_P(3)
          tF_map_eventptick_iff append.right_neutral mem_Collect_eq Un_iff)
    also have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) =
               map (map_eventptick f g') (map (ev ∘ of_ev) t1)›
      by (simp add: ‹tF t1› tF_map_map_eventptick_is)
    finally show ‹s ∈ 𝒟 ?lhs›
      by (auto simp add: "*"(1) D_P(1) intro!: is_processT7)
        (metis list.map_comp tF_map_eventptick_iff tF_map_ev_comp,
          use "*"(2, 3) D_P(1) ftF_append tF_map_eventptick_iff tF_append_iff in blast)
  next
    case D_Q
    from "*"(2) D_Q(1, 5) have ‹map (map_eventptick f g') t2 ∈ 𝒟 (Renaming (Q r) f g')›
      by (auto simp add: D_Renaming intro: ftF_Nil)
    hence ‹map (map_eventptick f g') t2 ∈ 𝒟 (⊓r' ∈ {r' ∈ ✓s(P). g r = g r'}. Renaming (Q r') f g')›
      by (simp add: D_GlobalNdet)
        (metis D_Q(2, 3) is_processT9 strict_ticks_of_memI)
    moreover from D_Q(2) have ‹map (map_eventptick f g) t1 @ [✓(g r)] ∈ 𝒯 (Renaming P f g)›
      by (auto simp add: T_Renaming)
    moreover have ‹tF (map (map_eventptick f g) t1)›
      by (simp add: D_Q(4) tF_map_eventptick_iff)
    ultimately have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) @
                     map (map_eventptick f g') t2 ∈ 𝒟 ?lhs›
      unfolding Seqptick_projs by blast
    with "*"(2, 3) have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) @
                         map (map_eventptick f g') t2 @ s2 ∈ 𝒟 ?lhs›
      by (auto simp add: D_Q(1) comp_assoc tF_map_eventptick_iff
          intro!: is_processT7[of ‹_ @ _›, simplified])
    also from D_Q(4) have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) @
                           map (map_eventptick f g') t2 @ s2 = s›
      by (simp add: "*"(1) D_Q(1))
        (metis eventptick.map_sel(1) in_set_conv_decomp tF_Cons_iff tF_append_iff)
    finally show ‹s ∈ 𝒟 ?lhs› .
  qed
next
  assume subset_div : ‹𝒟 ?rhs ⊆ 𝒟 ?lhs›
  fix s X assume ‹(s, X) ∈ ℱ ?rhs›
  then consider ‹s ∈ 𝒟 ?rhs›
    | (fail) s1 where ‹s = map (map_eventptick f g') s1›
      ‹(s1, map_eventptick f g' -` X) ∈ ℱ (P ;✓ Q)› ‹s1 ∉ 𝒟 (P ;✓ Q)›
    by (simp add: Renaming_projs)
      (metis (no_types, opaque_lifting) ftF_Nil ftF_iff_tF_butlast
        ftF_Cons_iff[of ‹last s› ‹[]›] map_butlast[of ‹map_eventptick f g'›]
        map_is_Nil_conv[of ‹map_eventptick f g'› ‹[]›] map_is_Nil_conv[of ‹map_eventptick f g'›]
        append_self_conv[of ‹map (map_eventptick f g') _› ‹[]›] F_imp_ftF
        snoc_eq_iff_butlast[of ‹butlast s› ‹last s› s]
        div_butlast_when_non_tF_iff not_tF_imp_not_Nil)
  thus ‹(s, X) ∈ ℱ ?lhs›
  proof cases
    from subset_div D_F show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
  next
    case fail
    from fail(2, 3)
    consider (F_P) t1 where ‹s1 = map (ev ∘ of_ev) t1› ‹(t1, ref_Seqptick (map_eventptick f g' -` X)) ∈ ℱ P› ‹tF t1›
      | (F_Q) t1 r t2 where ‹s1 = map (ev ∘ of_ev) t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹tF t1› ‹t1 ∉ 𝒟 P› ‹(t2, map_eventptick f g' -` X) ∈ ℱ (Q r)›
      by (simp add: Seqptick_projs) (metis F_imp_ftF)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      case F_P
      have ‹map_eventptick f g -` (ref_Seqptick X) = ref_Seqptick (map_eventptick f g' -` X)› for X
      proof (rule set_eqI)
        show ‹e ∈ map_eventptick f g -` (ref_Seqptick X) ⟷
                  e ∈ ref_Seqptick (map_eventptick f g' -` X)› for e
          by (cases e, auto simp add: ref_Seqptick_def image_iff)
            (metis Int_iff eventptick.sel(1) eventptick.simps(9) rangeI vimage_eq,
              metis IntI UNIV_I eventptick.sel(1) image_eqI)
      qed
      with F_P(2) have ‹(map (map_eventptick f g) t1, ref_Seqptick X) ∈ ℱ (Renaming P f g)›
        by (auto simp add: F_Renaming)
      with F_P(3) have ‹(map (ev ∘ of_ev) (map (map_eventptick f g) t1), X) ∈ ℱ ?lhs›
        by (fastforce simp add: Seqptick_projs tF_map_eventptick_iff)
      also have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) = s›
        by (simp add: fail(1) F_P(1))
          (metis F_P(3) eventptick.map_sel(1) in_set_conv_decomp tF_Cons_iff tF_append_iff)
      finally show ‹(s, X) ∈ ℱ ?lhs› .
    next
      case F_Q
      with F_Q(4) have ‹(map (map_eventptick f g') t2, X) ∈ ℱ (Renaming (Q r) f g')›
        by (auto simp add: F_Renaming)
      hence ‹(map (map_eventptick f g') t2, X) ∈
             ℱ (⊓r' ∈ {r' ∈ ✓s(P). g r = g r'}. Renaming (Q r') f g')›
        by (simp add: F_GlobalNdet)
          (metis F_Q(2, 4) is_processT9 strict_ticks_of_memI)
      moreover from F_Q(2) have ‹map (map_eventptick f g) t1 @ [✓(g r)] ∈ 𝒯 (Renaming P f g)›
        by (auto simp add: T_Renaming)
      moreover have ‹tF (map (map_eventptick f g) t1)›
        by (simp add: F_Q(3) tF_map_eventptick_iff)
      ultimately have ‹(map (ev ∘ of_ev) (map (map_eventptick f g) t1) @
                        map (map_eventptick f g') t2, X) ∈ ℱ ?lhs›
        unfolding Seqptick_projs by fast
      also have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) @ map (map_eventptick f g') t2 = s›
        by (simp add: fail(1) F_Q(1))
          (metis F_Q(3) eventptick.map_sel(1) in_set_conv_decomp
            tF_Cons_iff tF_append_iff)
      finally show ‹(s, X) ∈ ℱ ?lhs› .
    qed
  qed
qed



lemma inj_on_Renaming_Seqptick :
  ‹Renaming (P ;✓ Q) f g' =
   Renaming P f g ;✓ (λg_r. Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g')›
  (is ‹?lhs = ?rhs›) if ‹inj_on g ✓s(P)›
  ―‹This assumption is necessary, otherwise we cannot know which tick triggered term‹Q›.›
proof (rule FD_antisym)
  show ‹?lhs ⊑FD ?rhs›
  proof (rule failure_divergence_refine_optimizedI)
    fix s assume ‹s ∈ 𝒟 ?rhs›
    then consider (D_P) s1 s2 where ‹s = map (ev ∘ of_ev) s1 @ s2› ‹s1 ∈ 𝒟 (Renaming P f g)› ‹tF s1› ‹ftF s2›
      | (D_Q) s1 g_r s2 where ‹s = map (ev ∘ of_ev) s1 @ s2› ‹s1 @ [✓(g_r)] ∈ 𝒯 (Renaming P f g)›
        ‹s1 ∉ 𝒟 (Renaming P f g)› ‹tF s1› ‹s2 ∈ 𝒟 (Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g')›
      by (simp add: Seqptick_projs) (use D_imp_ftF in blast)
    thus ‹s ∈ 𝒟 ?lhs›
    proof cases
      case D_P
      from D_P(2) obtain t1 t2
        where * : ‹s1 = map (map_eventptick f g) t1 @ t2› ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 P›
        unfolding D_Renaming by blast
      from "*"(2, 4) have ‹map (ev ∘ of_ev) t1 ∈ 𝒟 (P ;✓ Q)›
        by (auto simp add: Seqptick_projs intro: ftF_Nil)
      hence ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1) ∈ 𝒟 ?lhs›
        unfolding D_Renaming mem_Collect_eq
        by (metis (mono_tags, lifting) ftF_Nil tF_map_ev_comp append.right_neutral)
      also have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1) =
                 map (ev ∘ of_ev) (map (map_eventptick f g) t1)›
        by simp (metis "*"(2) eventptick.map_sel(1) in_set_conv_decomp tF_Cons_iff tF_append_iff)
      finally show ‹s ∈ 𝒟 ?lhs›
        by (auto simp add: D_P(1, 4) "*"(1) ftF_append comp_assoc intro!: is_processT7)
    next
      case D_Q
      have ‹s1 @ [✓(g_r)] ∉ 𝒟 (Renaming P f g)› by (meson D_Q(3) is_processT9)
      with D_Q(2-4) obtain t1 r
        where * : ‹g_r = g r› ‹r ∈ ✓s(P)› ‹s1 = map (map_eventptick f g) t1› ‹t1 @ [✓(r)] ∈ 𝒯 P›
        by (auto simp add: Renaming_projs append_eq_map_conv tick_eq_map_eventptick_iff)
          (metis append_Nil2 ftF_Nil is_processT9 tF_map_eventptick_iff strict_ticks_of_memI)
      from "*"(1, 2) ‹inj_on g ✓s(P)› have ‹(THE r. r ∈ ✓s(P) ∧ g_r = g r) = r›
        by (auto dest: inj_onD)
      with D_Q(5) have ‹s2 ∈ 𝒟 (Renaming (Q r) f g')› by simp
      then obtain t2 t3
        where ** : ‹s2 = map (map_eventptick f g') t2 @ t3› ‹tF t2› ‹ftF t3› ‹t2 ∈ 𝒟 (Q r)›
        unfolding D_Renaming by blast
      from "*"(4) "**"(4) have ‹map (ev ∘ of_ev) t1 @ t2 ∈ 𝒟 (P ;✓ Q)›
        by (simp add: Seqptick_projs) (metis append_T_imp_tF not_Cons_self)
      with "**"(2) have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1 @ t2) ∈ 𝒟 ?lhs›
        unfolding D_Renaming mem_Collect_eq
        by (metis append.right_neutral ftF_Nil tF_append_iff tF_map_ev_comp)
      moreover have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1 @ t2) @ t3 = s›
        by (simp add: D_Q(1) "*"(3) "**"(1))
          (metis "*"(3) D_Q(4) eventptick.map_sel(1) in_set_conv_decomp
            tF_map_eventptick_iff tF_Cons_iff tF_append_iff)
      ultimately show ‹s ∈ 𝒟 ?lhs›
        by (auto simp add: "**"(3) intro!: is_processT7[of ‹_ @ _›, simplified])
          (use "**"(1) D_Q(1) in force, use "**"(2) tF_map_eventptick_iff in blast)
    qed
  next
    assume subset_div : ‹𝒟 ?rhs ⊆ 𝒟 ?lhs›
    fix s X assume ‹(s, X) ∈ ℱ ?rhs›
    then consider ‹s ∈ 𝒟 ?rhs›
      | (F_P) s1 where ‹s = map (ev ∘ of_ev) s1› ‹(s1, ref_Seqptick X) ∈ ℱ (Renaming P f g)› ‹s1 ∉ 𝒟 (Renaming P f g)› ‹tF s1›
      | (F_Q) s1 g_r s2 where ‹s = map (ev ∘ of_ev) s1 @ s2› ‹s1 @ [✓(g_r)] ∈ 𝒯 (Renaming P f g)›
        ‹s1 ∉ 𝒟 (Renaming P f g)› ‹tF s1› ‹(s2, X) ∈ ℱ (Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g')›
        ‹s2 ∉ 𝒟 (Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g')›
      by (simp add: Seqptick_projs)
        (metis (no_types, lifting) F_imp_ftF ftF_charn self_append_conv)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      from subset_div D_F show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
    next
      case F_P
      from F_P(2, 3) obtain t1
        where * : ‹s1 = map (map_eventptick f g) t1› ‹(t1, map_eventptick f g -` ref_Seqptick X) ∈ ℱ P›
        unfolding Renaming_projs by blast
      have ‹map_eventptick f g -` (ref_Seqptick X) = ref_Seqptick (map_eventptick f g' -` X)› for X
      proof (rule set_eqI)
        show ‹e ∈ map_eventptick f g -` (ref_Seqptick X) ⟷
              e ∈ ref_Seqptick (map_eventptick f g' -` X)› for e
          by (cases e, auto simp add: ref_Seqptick_def image_iff)
            (metis Int_iff eventptick.sel(1) eventptick.simps(9) rangeI vimage_eq,
              metis IntI UNIV_I eventptick.sel(1) image_eqI)
      qed
      with "*"(2) have ‹(t1, ref_Seqptick (map_eventptick f g' -` X)) ∈ ℱ P› by simp
      hence ‹(map (ev ∘ of_ev) t1, map_eventptick f g' -` X) ∈ ℱ (P ;✓ Q)›
        by (simp add: Seqptick_projs)
          (metis "*"(1) F_P(4) tF_map_eventptick_iff)
      hence ‹(map (map_eventptick f g') (map (ev ∘ of_ev) t1), X) ∈ ℱ ?lhs›
        unfolding F_Renaming by blast
      also have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1) = s›
        by (simp add: F_P(1) "*"(1))
          (metis "*"(1) F_P(4) eventptick.map_sel(1) in_set_conv_decomp
            tF_map_eventptick_iff tF_Cons_iff tF_append_iff)
      finally show ‹(s, X) ∈ ℱ ?lhs› .
    next
      case F_Q
      have ‹s1 @ [✓(g_r)] ∉ 𝒟 (Renaming P f g)› by (meson F_Q(3) is_processT9)
      with F_Q(2-4) obtain t1 r
        where * : ‹g_r = g r› ‹r ∈ ✓s(P)› ‹s1 = map (map_eventptick f g) t1› ‹t1 @ [✓(r)] ∈ 𝒯 P›
        by (auto simp add: Renaming_projs append_eq_map_conv tick_eq_map_eventptick_iff)
          (metis append_Nil2 ftF_Nil is_processT9 tF_map_eventptick_iff strict_ticks_of_memI)
      from "*"(1, 2) ‹inj_on g ✓s(P)› have ‹(THE r. r ∈ ✓s(P) ∧ g_r = g r) = r›
        by (auto dest: inj_onD)
      with F_Q(5, 6) have ‹(s2, X) ∈ ℱ (Renaming (Q r) f g')›
        ‹s2 ∉ 𝒟 (Renaming (Q r) f g')› by simp_all
      then obtain t2 where ** : ‹s2 = map (map_eventptick f g') t2› ‹(t2, map_eventptick f g' -` X) ∈ ℱ (Q r)›
        unfolding Renaming_projs by blast
      from "*"(4) "**"(2) have ‹(map (ev ∘ of_ev) t1 @ t2, map_eventptick f g' -` X) ∈ ℱ (P ;✓ Q)›
        by (simp add: Seqptick_projs) (metis append_T_imp_tF not_Cons_self2)
      hence ‹(map (map_eventptick f g') (map (ev ∘ of_ev) t1 @ t2), X) ∈ ℱ ?lhs›
        unfolding F_Renaming by blast
      also have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1 @ t2) = s›
        by (simp add: F_Q(1) "*"(3) "**"(1))
          (metis "*"(3) F_Q(4) eventptick.map_sel(1) in_set_conv_decomp
            tF_map_eventptick_iff tF_Cons_iff tF_append_iff)
      finally show ‹(s, X) ∈ ℱ ?lhs› .
    qed
  qed
next

  have ‹?rhs = Renaming P f g ;✓ (λg_r. ⊓r ∈ {r ∈ ✓s(P). g_r = g r}. Renaming (Q r) f g')›
  proof (rule mono_Seqptick_eq)
    show ‹Renaming P f g = Renaming P f g› ..
  next
    fix g_r assume ‹g_r ∈ ✓s(Renaming P f g)›
    then obtain s s1 where ‹s @ [✓(g_r)] = map (map_eventptick f g) s1› ‹s1 ∈ 𝒯 P› ‹s1 ∉ 𝒟 P›
      by (simp add: strict_ticks_of_def Renaming_projs)
        (metis (no_types, opaque_lifting) T_imp_ftF append_Nil2 butlast_snoc
          div_butlast_when_non_tF_iff ftF_Nil
          ftF_iff_tF_butlast ftF_single map_butlast)
    from this(1) obtain s1' r where ‹g_r = g r› ‹s1 = s1' @ [✓(r)]›
      by (cases s1 rule: rev_cases) (auto simp add: tick_eq_map_eventptick_iff)
    with ‹s1 ∈ 𝒯 P› ‹s1 ∉ 𝒟 P› have ‹s1' @ [✓(r)] ∈ 𝒯 P› ‹s1' @ [✓(r)] ∉ 𝒟 P› by simp_all
    hence ‹r ∈ ✓s(P)› unfolding strict_ticks_of_def by blast
    have ‹{r ∈ ✓s(P). g_r = g r} = {r}›
      by (auto simp add: ‹r ∈ ✓s(P)› ‹g_r = g r› intro: inj_onD[OF ‹inj_on g ✓s(P)›])
    moreover have ‹(THE r. r ∈ ✓s(P) ∧ g_r = g r) = r›
      using calculation by blast
    ultimately have ‹Q (THE r. r ∈ ✓s(P) ∧ g_r = g r) =
                     GlobalNdet {r ∈ ✓s(P). g_r = g r} Q› by simp
    thus ‹Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g' =
          (⊓r ∈ {r ∈ ✓s(P). g_r = g r}. Renaming (Q r) f g')›
      by (simp flip: Renaming_distrib_GlobalNdet)
  qed
  thus ‹?rhs ⊑FD ?lhs› by (simp add: FD_Renaming_Seqptick)
qed


text ‹When typ‹'r› is set on typ‹unit›, we recover the version that we had before the generalization.›
lemma ‹Renaming (P ;✓ Q) f g = Renaming P f g ;✓ (λr. Renaming (Q ()) f g)›
  by (subst inj_on_Renaming_Seqptick[where g = g]) (auto intro: inj_onI)


―‹New in Isabelle26.›
corollary Seqptick_inj_on_RenamingTick :
  ‹RenamingTick P g ;✓ Q = P ;✓ (λr. Q (g r))› if ‹inj_on g ✓s(P)›
proof -
  from inj_on_Renaming_Seqptick[OF that, where g' = id and f = id and Q = ‹λr. Q (g r)›]
  have ‹P ;✓ (λr. Q (g r)) = RenamingTick P g ;✓ (λg_r. Q (g (THE r. r ∈ ✓s(P) ∧ g_r = g r)))› by simp
  also have ‹… = RenamingTick P g ;✓ Q›
  proof (rule mono_Seqptick_eq[OF refl arg_cong[where f = Q]])
    show ‹g_r ∈ ✓s(RenamingTick P g) ⟹ g (THE r. r ∈ ✓s(P) ∧ g_r = g r) = g_r› for g_r
      by (simp add: strict_ticks_of_RenamingTick image_iff)
        (metis (mono_tags, lifting) inj_on_eq_iff that the_equality)
  qed
  finally show ‹RenamingTick P g ;✓ Q = P ;✓ (λr. Q (g r))› ..
qed


―‹New in Isabelle26.›
corollary Seqptick_RenamingTick_permute_list :
  ‹length✓⇘n⇙(P) ⟹ f permutes {..<n} ⟹
   RenamingTick P (permute_list f) ;✓ Q = P ;✓ (λr. Q (permute_list f r))›
  by (intro Seqptick_inj_on_RenamingTick inj_onI)
    (metis is_ticks_lengthD permute_list_compose permute_list_id permutes_inv permutes_inv_o(1))



lemma TickSwap_Seqptick [simp] :
  ‹TickSwap (P ;✓ Q) = TickSwap P ;✓ (λ(s, r). TickSwap (Q (r, s)))› (is ‹?lhs = ?rhs›)
proof -
  have ‹?lhs = Renaming (P ;✓ Q) id prod.swap› by (simp add: TickSwap_is_Renaming)
  also have ‹… = Renaming P id prod.swap ;✓
                  (λs_r. Renaming (Q (THE r_s. r_s ∈ strict_ticks_of P ∧
                                               s_r = prod.swap r_s)) id prod.swap)›
    (is ‹_ = _ ;✓ ?rhs'›) by (simp add: inj_on_Renaming_Seqptick)
  also have ‹… = ?rhs›
  proof (rule mono_Seqptick_eq, unfold TickSwap_is_Renaming)
    show ‹Renaming P id prod.swap = Renaming P id prod.swap› ..
  next
    fix s_r assume ‹s_r ∈ strict_ticks_of (Renaming P id prod.swap)›
    then obtain r s where ‹(r, s) ∈ strict_ticks_of P› ‹s_r = (s, r)›
      by (auto simp flip: TickSwap_is_Renaming)
    hence ‹(THE r_s. r_s ∈ strict_ticks_of P ∧ s_r = prod.swap r_s) = (r, s)› by auto
    thus ‹Renaming (Q (THE r_s. r_s ∈ strict_ticks_of P ∧ s_r = prod.swap r_s)) id prod.swap =
          (case s_r of (s, r) ⇒ Renaming (Q (r, s)) id prod.swap)›
      by (simp add: ‹s_r = (s, r)›)
  qed
  finally show ‹?lhs = ?rhs› .
qed

lemma TickSwap_is_Seqptick_iff [simp] :
  ‹TickSwap P = Q ;✓ R ⟷ P = TickSwap Q ;✓ (λ(r, s). TickSwap (R (s, r)))›
  by (simp add: TickSwap_eq_iff_eq_TickSwap)




subsection ‹Renaming and Synchronization Product›

theorem (in Synchroptick) inj_RenamingEv_Syncptick :
  ‹RenamingEv (P ⟦S⟧✓ Q) f = RenamingEv P f ⟦f ` S⟧✓ RenamingEv Q f›
  (is ‹?lhs = ?rhs›) if ‹inj f›
proof -
  let ?fun = ‹map_eventptick f id›
  let ?map = ‹map ?fun›
  let ?R   = ‹λP. RenamingEv P f›
  show ‹?lhs = ?rhs›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    then obtain t1 t2 where * : ‹t = ?map t1 @ t2›
      ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 (P ⟦S⟧✓ Q)› unfolding D_Renaming by blast
    from "*"(4) obtain u v t_P t_Q where ** : ‹t1 = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      unfolding D_Syncptick by blast
    from setinterleavesptick_inj_map_map_eventptick_iff_weak [THEN iffD2, OF ‹inj f› "**"(4)]
    have ‹?map u setinterleaves✓⇘(⊗✓)⇙ ((?map t_P, ?map t_Q), f ` S)› .
    moreover from "**"(5) have ‹?map t_P ∈ 𝒟 (?R P) ∧ ?map t_Q ∈ 𝒯 (?R Q) ∨
                              ?map t_P ∈ 𝒯 (?R P) ∧ ?map t_Q ∈ 𝒟 (?R Q)›
      by (auto simp add: Renaming_projs dest: D_T)
        (metis "**"(2,4) append_self_conv ftF_map_tick_iff
          list.map_disc_iff tF_setinterleavesptick_iff)+
    moreover have ‹t = ?map u @ (?map v @ t2)› by (simp add: "*"(1) "**"(1))
    moreover have ‹tF (?map u)› by (simp add: "**"(2) tF_map_eventptick_iff)
    moreover from "*"(2,3) "**"(1) have ‹ftF (?map v @ t2)›
      using ftF_append tF_map_eventptick_iff tF_append_iff by blast
    ultimately show ‹t ∈ 𝒟 ?rhs› unfolding D_Syncptick by blast
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then obtain u v t_P t_Q where * : ‹t = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), f ` S)›
      ‹t_P ∈ 𝒟 (?R P) ∧ t_Q ∈ 𝒯 (?R Q) ∨ t_P ∈ 𝒯 (?R P) ∧ t_Q ∈ 𝒟 (?R Q)›
      unfolding D_Syncptick by blast
    from "*"(5) show ‹t ∈ 𝒟 ?lhs›
    proof (elim disjE conjE)
      assume ‹t_P ∈ 𝒟 (?R P)› ‹t_Q ∈ 𝒯 (?R Q)›
      from ‹t_P ∈ 𝒟 (?R P)› obtain t_P1 t_P2
        where ** : ‹t_P = ?map t_P1 @ t_P2› ‹tF t_P1› ‹ftF t_P2› ‹t_P1 ∈ 𝒟 P›
        unfolding D_Renaming by blast
      from ‹t_Q ∈ 𝒯 (?R Q)› consider (T_Q) t_Q1 where ‹t_Q = ?map t_Q1› ‹t_Q1 ∈ 𝒯 Q›
        | (D_Q) t_Q1 t_Q2 where ‹t_Q = ?map t_Q1 @ t_Q2› ‹tF t_Q1› ‹ftF t_Q2› ‹t_Q1 ∈ 𝒟 Q›
        unfolding T_Renaming by blast
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        case T_Q
        from "*"(4)[unfolded "**"(1) T_Q(1), THEN setinterleavesptick_appendL]
        obtain u1 u2 t_Q11 t_Q12 where *** : ‹u = u1 @ u2› ‹?map t_Q1 = t_Q11 @ t_Q12›
          ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((?map t_P1, t_Q11), f ` S)› by blast
        obtain t_Q11' where ‹t_Q11' ≤ t_Q1› ‹t_Q11 = ?map t_Q11'› 
          by (metis "***"(2) map_eq_append_conv Prefix_Order.prefixI)
        from setinterleavesptick_inj_map_map_eventptick_iff_strong
          [THEN iffD1, OF ‹inj f› "***"(3)[unfolded this]]
        obtain u1' where **** : ‹u1 = ?map u1'›
          ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q11'), S)› by blast
        from "*"(2) "***"(1) "****"(1) tF_map_eventptick_iff
          T_Q(2) ‹t_Q11' ≤ t_Q1› is_processT3_TR
        have ‹u1' = u1' @ []› ‹tF u1'› ‹ftF []› ‹t_Q11' ∈ 𝒯 Q› by simp_all blast
        with "****"(2) "**"(4) have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
          unfolding D_Syncptick by blast
        moreover have ‹t = ?map u1' @ (u2 @ v)› by (simp add: "*"(1) "***"(1) "****"(1))
        moreover have ‹ftF (u2 @ v)›
          using "*"(2,3) "***"(1) ftF_append tF_append_iff by blast
        ultimately show ‹t ∈ 𝒟 ?lhs› unfolding D_Renaming using ‹tF u1'› by blast
      next
        case D_Q
        have ‹?map t_P1 ≤ t_P› ‹?map t_Q1 ≤ t_Q›
          by (simp_all add: "**"(1) D_Q(1))
        from setinterleavesptick_le_prefixLR[OF "*"(4) this] show ‹t ∈ 𝒟 ?lhs›
        proof (elim disjE exE conjE)
          fix u1 t_Q1' assume *** : ‹u1 ≤ u› ‹t_Q1' ≤ ?map t_Q1›
            ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((?map t_P1, t_Q1'), f ` S)›
          obtain u2 where ‹u = u1 @ u2› using "***"(1) prefixE by blast
          obtain t_Q1'' where ‹t_Q1' = ?map t_Q1''› ‹t_Q1'' ≤ t_Q1›
            by (metis "***"(2) prefixE prefixI map_eq_append_conv)
          from setinterleavesptick_inj_map_map_eventptick_iff_strong
            [THEN iffD1, OF ‹inj f› "***"(3)[unfolded ‹t_Q1' = ?map t_Q1''›]]
          obtain u1' where **** : ‹u1 = ?map u1'›
            ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› by blast
          have ‹u1' = u1' @ []› ‹ftF []› by simp_all
          moreover from "**"(2) "****"(2) setinterleavesptick_tF_imp
          have ‹tF u1'› by blast
          moreover from D_Q(4) D_T ‹t_Q1'' ≤ t_Q1› is_processT3_TR
          have ‹t_Q1'' ∈ 𝒯 Q› by blast
          ultimately have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
            unfolding D_Syncptick using ‹t_P1 ∈ 𝒟 P› "****"(2) by blast
          moreover from "*"(1-3) "****"(1)
          have ‹t = ?map u1' @ (u2 @ v)› ‹ftF (u2 @ v)›
            by (auto simp add: ‹u = u1 @ u2› ftF_append)
          ultimately show ‹t ∈ 𝒟 ?lhs›
            unfolding D_Renaming using ‹tF u1'› by blast
        next
          fix u1 t_P1' assume *** : ‹u1 ≤ u› ‹t_P1' ≤ ?map t_P1›
            ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((t_P1', ?map t_Q1), f ` S)›
          obtain u2 where ‹u = u1 @ u2› using "***"(1) prefixE by blast
          obtain t_P1'' where ‹t_P1' = ?map t_P1''› ‹t_P1'' ≤ t_P1›
            by (metis "***"(2) prefixE prefixI map_eq_append_conv)
          from setinterleavesptick_inj_map_map_eventptick_iff_strong
            [THEN iffD1, OF ‹inj f› "***"(3)[unfolded ‹t_P1' = ?map t_P1''›]]
          obtain u1' where **** : ‹u1 = ?map u1'›
            ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1'', t_Q1), S)› by blast
          have ‹u1' = u1' @ []› ‹ftF []› by simp_all
          moreover from D_Q(2) "****"(2) setinterleavesptick_tF_imp
          have ‹tF u1'› by blast
          moreover from "**"(4) D_T ‹t_P1'' ≤ t_P1› is_processT3_TR
          have ‹t_P1'' ∈ 𝒯 P› by blast
          ultimately have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
            unfolding D_Syncptick using ‹t_Q1 ∈ 𝒟 Q› "****"(2) by blast
          moreover from "*"(1-3) "****"(1)
          have ‹t = ?map u1' @ (u2 @ v)› ‹ftF (u2 @ v)›
            by (auto simp add: ‹u = u1 @ u2› ftF_append)
          ultimately show ‹t ∈ 𝒟 ?lhs›
            unfolding D_Renaming using ‹tF u1'› by blast
        qed
      qed
    next
      assume ‹t_Q ∈ 𝒟 (?R Q)› ‹t_P ∈ 𝒯 (?R P)›
      from ‹t_Q ∈ 𝒟 (?R Q)› obtain t_Q1 t_Q2
        where ** : ‹t_Q = ?map t_Q1 @ t_Q2› ‹tF t_Q1› ‹ftF t_Q2› ‹t_Q1 ∈ 𝒟 Q›
        unfolding D_Renaming by blast
      from ‹t_P ∈ 𝒯 (?R P)› consider (T_P) t_P1 where ‹t_P = ?map t_P1› ‹t_P1 ∈ 𝒯 P›
        | (D_P) t_P1 t_P2 where ‹t_P = ?map t_P1 @ t_P2› ‹tF t_P1› ‹ftF t_P2› ‹t_P1 ∈ 𝒟 P›
        unfolding T_Renaming by blast
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        case T_P
        from "*"(4)[unfolded "**"(1) T_P(1), THEN setinterleavesptick_appendR]
        obtain u1 u2 t_P11 t_P12 where *** : ‹u = u1 @ u2› ‹?map t_P1 = t_P11 @ t_P12›
          ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((t_P11, ?map t_Q1), f ` S)› by blast
        obtain t_P11' where ‹t_P11' ≤ t_P1› ‹t_P11 = ?map t_P11'› 
          by (metis "***"(2) map_eq_append_conv Prefix_Order.prefixI)
        from setinterleavesptick_inj_map_map_eventptick_iff_strong
          [THEN iffD1, OF ‹inj f› "***"(3)[unfolded this]]
        obtain u1' where **** : ‹u1 = ?map u1'›
          ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P11', t_Q1), S)› by blast
        from "*"(2) "***"(1) "****"(1) tF_map_eventptick_iff
          T_P(2) ‹t_P11' ≤ t_P1› is_processT3_TR
        have ‹u1' = u1' @ []› ‹tF u1'› ‹ftF []› ‹t_P11' ∈ 𝒯 P› by simp_all blast
        with "****"(2) "**"(4) have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
          unfolding D_Syncptick by blast
        moreover have ‹t = ?map u1' @ (u2 @ v)› by (simp add: "*"(1) "***"(1) "****"(1))
        moreover have ‹ftF (u2 @ v)›
          using "*"(2,3) "***"(1) ftF_append tF_append_iff by blast
        ultimately show ‹t ∈ 𝒟 ?lhs› unfolding D_Renaming using ‹tF u1'› by blast
      next
        case D_P
        have ‹?map t_P1 ≤ t_P› ‹?map t_Q1 ≤ t_Q›
          by (simp_all add: "**"(1) D_P(1))
        from setinterleavesptick_le_prefixLR[OF "*"(4) this] show ‹t ∈ 𝒟 ?lhs›
        proof (elim disjE exE conjE)
          fix u1 t_Q1' assume *** : ‹u1 ≤ u› ‹t_Q1' ≤ ?map t_Q1›
            ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((?map t_P1, t_Q1'), f ` S)›
          obtain u2 where ‹u = u1 @ u2› using "***"(1) prefixE by blast
          obtain t_Q1'' where ‹t_Q1' = ?map t_Q1''› ‹t_Q1'' ≤ t_Q1›
            by (metis "***"(2) prefixE prefixI map_eq_append_conv)
          from setinterleavesptick_inj_map_map_eventptick_iff_strong
            [THEN iffD1, OF ‹inj f› "***"(3)[unfolded ‹t_Q1' = ?map t_Q1''›]]
          obtain u1' where **** : ‹u1 = ?map u1'›
            ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› by blast
          have ‹u1' = u1' @ []› ‹ftF []› by simp_all
          moreover from D_P(2) "****"(2) setinterleavesptick_tF_imp
          have ‹tF u1'› by blast
          moreover from "**"(4) D_T ‹t_Q1'' ≤ t_Q1› is_processT3_TR
          have ‹t_Q1'' ∈ 𝒯 Q› by blast
          ultimately have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
            unfolding D_Syncptick using ‹t_P1 ∈ 𝒟 P› "****"(2) by blast
          moreover from "*"(1-3) "****"(1)
          have ‹t = ?map u1' @ (u2 @ v)› ‹ftF (u2 @ v)›
            by (auto simp add: ‹u = u1 @ u2› ftF_append)
          ultimately show ‹t ∈ 𝒟 ?lhs›
            unfolding D_Renaming using ‹tF u1'› by blast
        next
          fix u1 t_P1' assume *** : ‹u1 ≤ u› ‹t_P1' ≤ ?map t_P1›
            ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((t_P1', ?map t_Q1), f ` S)›
          obtain u2 where ‹u = u1 @ u2› using "***"(1) prefixE by blast
          obtain t_P1'' where ‹t_P1' = ?map t_P1''› ‹t_P1'' ≤ t_P1›
            by (metis "***"(2) prefixE prefixI map_eq_append_conv)
          from setinterleavesptick_inj_map_map_eventptick_iff_strong
            [THEN iffD1, OF ‹inj f› "***"(3)[unfolded ‹t_P1' = ?map t_P1''›]]
          obtain u1' where **** : ‹u1 = ?map u1'›
            ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1'', t_Q1), S)› by blast
          have ‹u1' = u1' @ []› ‹ftF []› by simp_all
          moreover from "**"(2) "****"(2) setinterleavesptick_tF_imp
          have ‹tF u1'› by blast
          moreover from D_P(4) D_T ‹t_P1'' ≤ t_P1› is_processT3_TR
          have ‹t_P1'' ∈ 𝒯 P› by blast
          ultimately have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
            unfolding D_Syncptick using ‹t_Q1 ∈ 𝒟 Q› "****"(2) by blast
          moreover from "*"(1-3) "****"(1)
          have ‹t = ?map u1' @ (u2 @ v)› ‹ftF (u2 @ v)›
            by (auto simp add: ‹u = u1 @ u2› ftF_append)
          ultimately show ‹t ∈ 𝒟 ?lhs›
            unfolding D_Renaming using ‹tF u1'› by blast
        qed
      qed
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
    then obtain t' where ‹t = ?map t'›
      and * : ‹(t', ?fun -` X) ∈ ℱ (P ⟦S⟧✓ Q)›
      unfolding Renaming_projs by blast
    have ‹t' ∉ 𝒟 (P ⟦S⟧✓ Q)›
    proof (rule notI)
      assume ‹t' ∈ 𝒟 (P ⟦S⟧✓ Q)›
      hence ‹t ∈ 𝒟 ?lhs›
        by (simp add: ‹t = ?map t'› D_Syncptick D_Renaming)
          (metis (no_types) append_Nil2 ftF_Nil map_append ftF_map_eventptick_iff)
      with ‹t ∉ 𝒟 ?lhs› show False ..
    qed
    with "*" obtain t_P t_Q X_P X_Q
      where ** : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
        ‹?fun -` X ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
      unfolding Syncptick_projs by fast
    from "**"(2, 3) F_T ‹t' ∉ 𝒟 (P ⟦S⟧✓ Q)› append_Nil2 ftF_Nil
    have ‹t_P ∉ 𝒟 P› unfolding D_Syncptick' by blast
    from "**"(1, 3) F_T ‹t' ∉ 𝒟 (P ⟦S⟧✓ Q)› append_Nil2 ftF_Nil
    have ‹t_Q ∉ 𝒟 Q› unfolding D_Syncptick' by blast
    have *** : ‹?fun -` ?fun ` X_P = X_P› ‹?fun -` ?fun ` X_Q = X_Q›
      by (simp add: set_eq_iff image_iff,
          metis (mono_tags, opaque_lifting) eventptick.inj_map_strong id_apply injD ‹inj f›)+
    from "**"(1) have ‹(?map t_P, ?fun ` X_P) ∈ ℱ (?R P)›
      by (subst (asm) "***"(1)[symmetric]) (auto simp add: F_Renaming)
    moreover {
      fix a assume ‹?map t_P @ [ev a] ∈ 𝒯 (?R P)› ‹a ∉ range f›
      then consider t_P1 where ‹?map t_P @ [ev a] = ?map t_P1› ‹t_P1 ∈ 𝒯 P›
        | t_P1 t_P2 where ‹?map t_P @ [ev a] = ?map t_P1 @ t_P2› ‹tF t_P1› ‹t_P1 ∈ 𝒟 P›
        unfolding T_Renaming by blast
      hence False
      proof cases
        from ‹a ∉ range f› show ‹?map t_P @ [ev a] = ?map t_P1 ⟹ False› for t_P1
          by (auto simp add: append_eq_map_conv ev_eq_map_eventptick_iff)
      next
        fix t_P1 t_P2 assume ‹?map t_P @ [ev a] = ?map t_P1 @ t_P2› ‹tF t_P1› ‹t_P1 ∈ 𝒟 P›
        from this(1) ‹a ∉ range f› have ‹t_P1 ≤ t_P›
          by (cases t_P2 rule: rev_cases, auto simp add: append_eq_map_conv ev_eq_map_eventptick_iff)
            (metis prefixI eventptick.inj_map inj_map_eq_map inj_on_id map_eq_append_conv ‹inj f›)
        with ‹t_P1 ∈ 𝒟 P› have ‹t_P ∈ 𝒟 P›
          by (metis "**"(1) F_imp_ftF prefixE ‹tF t_P1› ftF_append_iff
              is_processT7 tF_Nil tF_imp_ftF)
        with ‹t_P ∉ 𝒟 P› show False ..
      qed
    }
    ultimately have $ : ‹(?map t_P, ?fun ` X_P ∪ {ev a | a. a ∉ range f}) ∈ ℱ (?R P)›
      using is_processT5_S7' by blast
    from "**"(2) have ‹(?map t_Q, ?fun ` X_Q) ∈ ℱ (?R Q)›
      by (subst (asm) "***"(2)[symmetric]) (auto simp add: F_Renaming)
    moreover {
      fix a assume ‹?map t_Q @ [ev a] ∈ 𝒯 (?R Q)› ‹a ∉ range f›
      then consider t_Q1 where ‹?map t_Q @ [ev a] = ?map t_Q1› ‹t_Q1 ∈ 𝒯 Q›
        | t_Q1 t_Q2 where ‹?map t_Q @ [ev a] = ?map t_Q1 @ t_Q2› ‹tF t_Q1› ‹t_Q1 ∈ 𝒟 Q›
        unfolding T_Renaming by blast
      hence False
      proof cases
        from ‹a ∉ range f› show ‹?map t_Q @ [ev a] = ?map t_Q1 ⟹ False› for t_Q1
          by (auto simp add: append_eq_map_conv ev_eq_map_eventptick_iff)
      next
        fix t_Q1 t_Q2 assume ‹?map t_Q @ [ev a] = ?map t_Q1 @ t_Q2› ‹tF t_Q1› ‹t_Q1 ∈ 𝒟 Q›
        from this(1) ‹a ∉ range f› have ‹t_Q1 ≤ t_Q›
          by (cases t_Q2 rule: rev_cases, auto simp add: append_eq_map_conv ev_eq_map_eventptick_iff)
            (metis prefixI eventptick.inj_map inj_map_eq_map inj_on_id map_eq_append_conv ‹inj f›)
        with ‹t_Q1 ∈ 𝒟 Q› have ‹t_Q ∈ 𝒟 Q›
          by (metis "**"(2) F_imp_ftF prefixE ‹tF t_Q1› ftF_append_iff
              is_processT7 tF_Nil tF_imp_ftF)
        with ‹t_Q ∉ 𝒟 Q› show False ..
      qed
    }
    ultimately have $$ : ‹(?map t_Q, ?fun ` X_Q ∪ {ev a | a. a ∉ range f}) ∈ ℱ (?R Q)›
      using is_processT5_S7' by blast
    from "**"(3) have $$$ : ‹t setinterleaves✓⇘(⊗✓)⇙ ((?map t_P, ?map t_Q), f ` S)›
      by (simp add: ‹t = ?map t'› setinterleavesptick_inj_map_map_eventptick_iff_weak ‹inj f›)
    have ‹e ∈ X ⟹ e ∈ super_ref_Syncptick (⊗✓) (?fun ` X_P ∪ {ev a | a. a ∉ range f}) (f ` S)
                         (?fun ` X_Q ∪ {ev a | a. a ∉ range f})› for e
      using "**"(4)[THEN set_mp, of ‹map_eventptick (inv f) id e›] ‹inj f›
      unfolding super_ref_Syncptick_def
      by (cases e, simp_all add: image_iff tick_eq_map_eventptick_iff) force
    hence $$$$ : ‹X ⊆ super_ref_Syncptick (⊗✓) (?fun ` X_P ∪ {ev a | a. a ∉ range f}) (f ` S)
                       (?fun ` X_Q ∪ {ev a | a. a ∉ range f})› by blast
    from "$" "$$" "$$$" "$$$$" show ‹(t, X) ∈ ℱ ?rhs› unfolding F_Syncptick by fast
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
    then obtain t_P t_Q X_P X_Q
      where * : ‹(t_P, X_P) ∈ ℱ (?R P)› ‹(t_Q, X_Q) ∈ ℱ (?R Q)›
        ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), f ` S)›
        ‹X ⊆ super_ref_Syncptick (⊗✓) X_P (f ` S) X_Q›
      unfolding Syncptick_projs by blast
    have ‹¬ (t_P ∈ 𝒟 (?R P) ∨ t_Q ∈ 𝒟 (?R Q))›
    proof (rule notI)
      assume ‹t_P ∈ 𝒟 (?R P) ∨ t_Q ∈ 𝒟 (?R Q)›
      hence ‹t ∈ 𝒟 ?rhs›
        by (simp add: D_Syncptick')
          (metis "*"(1-3) F_T append_Nil2 ftF_Nil)
      with ‹t ∉ 𝒟 ?rhs› show False ..
    qed
    with "*"(1, 2) obtain t_P' t_Q'
      where ** : ‹t_P = ?map t_P'› ‹(t_P', ?fun -` X_P) ∈ ℱ P›
        ‹t_Q = ?map t_Q'› ‹(t_Q', ?fun -` X_Q) ∈ ℱ Q›
      unfolding Renaming_projs by blast
    from setinterleavesptick_inj_map_map_eventptick_iff_strong
      [THEN iffD1, OF ‹inj f› "*"(3)[unfolded "**"(1, 3)]] obtain t'
      where *** : ‹t = ?map t'› ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)› by blast
    have ‹e ∈ ?fun -` X ⟹ e ∈ super_ref_Syncptick (⊗✓) (?fun -` X_P) S (?fun -` X_Q)› for e
      using "*"(4)[THEN set_mp, of ‹?fun e›]
      by (cases e) (auto simp add: super_ref_Syncptick_def dest: injD[OF ‹inj f›])
    hence ‹?fun -` X ⊆ super_ref_Syncptick (⊗✓) (?fun -` X_P) S (?fun -` X_Q)› by blast
    with "**"(2, 4) "***"(2) have ‹(t', ?fun -` X) ∈ ℱ (P ⟦S⟧✓ Q)›
      unfolding F_Syncptick by auto
    thus ‹(t, X) ∈ ℱ ?lhs› by (auto simp add: "***"(1) F_Renaming)
  qed
qed




section ‹Laws of Hiding›

section ‹Hiding and Sequential Composition›

text ‹We start by giving a counter example when the assumption term‹𝔽✓(P)› is not satisfied.›

notepad begin
  define Q :: ‹nat ⇒ ('a, 'r) processptick›
    where ‹Q r ≡ (((→) undefined) ^^ r) STOP› for r
  have ‹SKIPS UNIV \ {undefined} = (SKIPS UNIV :: ('a, nat) processptick)›
    by (simp add: Hiding_SKIPS)
  moreover have ‹Q r \ {undefined} = STOP› for r
    by (induct r) (simp_all add: Q_def Hiding_write0_non_disjoint)
  ultimately have * : ‹(SKIPS UNIV \ {undefined}) ;✓ (λr. Q r \ {undefined}) = STOP›
    by (simp only: SKIPS_Seqptick) simp

  have ‹SKIPS UNIV ;✓ Q = ⊓r ∈ UNIV. Q r› by simp
  moreover have ‹[] ∈ 𝒟 (… \ {undefined})›
  proof (rule D_Hiding_seqRunI)
    show ‹ftF []› ‹tF []› ‹[] = trace_hide [] (ev ` {undefined}) @ []› by simp_all
  next
    { fix r
      have ‹replicate r (ev undefined) ∈ 𝒯 (Q r)›
        by (induct r) (simp_all add: Q_def T_write0)
      also have ‹replicate r (ev undefined) = map (λi. ev undefined) [0..<r]›
        by (simp add: map_replicate_trivial)
      finally have ‹map (λi. ev undefined) [0..<r] ∈ 𝒯 (Q r)› .
    }
    hence ‹∃r. map (λi. ev undefined) [0..<i] ∈ 𝒯 (Q r)› for i by blast
    thus ‹[] ∈ 𝒟 (⊓r ∈ UNIV. Q r) ∨ (∃x. isInfHidden_seqRun x (⊓r ∈ UNIV. Q r) {undefined} [])›
      by (auto simp add: T_GlobalNdet)
  qed
  ultimately have ** : ‹(SKIPS UNIV ;✓ Q) \ {undefined} = ⊥›
    by (simp add: BOT_iff_Nil_D)

  have ‹(SKIPS UNIV \ {undefined}) ;✓ (λr. Q r \ {undefined}) ≠ (SKIPS UNIV ;✓ Q) \ {undefined}›
    unfolding "*" "**" by simp

  hence ‹∃P (Q :: nat ⇒ ('a, 'r) processptick) S.
         (P \ S) ;✓ (λr. Q r \ S) ≠ (P ;✓ Q) \ S› by blast

end



text ‹In general, only one refinement is holding.›

theorem Hiding_Seqptick_FD_Seqptick_Hiding :
  ‹(P ;✓ Q) \ S ⊑FD (P \ S) ;✓ (λr. Q r \ S)› (is ‹?lhs ⊑FD ?rhs›)
proof (rule failure_divergence_refine_optimizedI)
  let ?th = ‹λt. trace_hide t (ev ` S)› and ?map = ‹λt. map (ev ∘ of_ev) t›
  fix t assume ‹t ∈ 𝒟 ?rhs›
  with D_imp_ftF is_processT9
  consider (D_P) u v where ‹t = ?map u @ v› ‹u ∈ 𝒟 (P \ S)› ‹tF u› ‹ftF v›
    | (D_Q) u r v where ‹t = ?map u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P \ S)›
      ‹u @ [✓(r)] ∉ 𝒟 (P \ S)› ‹tF u› ‹v ∈ 𝒟 (Q r \ S)›
    by (fastforce simp add: Seqptick_projs)
  thus ‹t ∈ 𝒟 ?lhs›
  proof cases
    case D_P
    from D_P(2) obtain u' v' x where * : ‹u = ?th u' @ v'› ‹tF u'› ‹ftF v'›
      ‹u' ∈ 𝒟 P ∨ isInfHidden_seqRun x P S u'›
      by (blast elim: D_Hiding_seqRunE)
    from "*"(4) have ‹?th (?map u') ∈ 𝒟 ?lhs›
    proof (elim disjE)
      assume ‹u' ∈ 𝒟 P›
      with "*"(2) have ‹?map u' ∈ 𝒟 (P ;✓ Q)›
        by (auto simp add: Seqptick_projs intro: ftF_Nil)
      with mem_D_imp_mem_D_Hiding show ‹?th (?map u') ∈ 𝒟 ?lhs› .
    next
      assume ‹isInfHidden_seqRun x P S u'›
      from this isInfHidden_seqRun_imp_tF_seqRun[OF this]
      have ‹isInfHidden_seqRun (ev ∘ of_ev ∘ x) (P ;✓ Q) S (?map u')›
        by (simp add: Seqptick_projs image_iff)
          (metis eventptick.sel(1) list.map_comp map_append seqRun_def)
      thus ‹?th (?map u') ∈ 𝒟 ?lhs›
        by (simp add: D_Hiding_seqRun)
          (metis (no_types) append.right_neutral comp_apply
            ftF_Nil tF_map_ev_comp)
    qed
    also have ‹?th (?map u') = ?map (?th u')›
      by (fact tF_trace_hide_map_ev_comp_of_ev[OF ‹tF u'›])
    finally show ‹t ∈ 𝒟 ?lhs›
      by (simp add: D_P(1, 4) "*"(1) ftF_append is_processT7)
  next
    case D_Q
    from D_Q(2, 3) obtain u' where ‹u @ [✓(r)] = ?th u'› ‹(u', ev ` S) ∈ ℱ P›
      unfolding T_Hiding D_Hiding by fast
    then obtain u' where ‹u = ?th u'› ‹(u' @ [✓(r)], ev ` S) ∈ ℱ P›
      by (cases u' rule: rev_cases, simp_all split: if_split_asm)
        (metis Hiding_tF eventptick.disc(2) ftF_nonempty_append_imp is_processT2
          not_Cons_self2 tF_Cons_iff tF_append_iff)
    from D_Q(5) obtain v' w' x where * : ‹v = ?th v' @ w'› ‹tF v'› ‹ftF w'›
      ‹v' ∈ 𝒟 (Q r) ∨ isInfHidden_seqRun x (Q r) S v'›
      by (blast elim: D_Hiding_seqRunE)
    from "*"(4) have ‹?th (?map u' @ v') ∈ 𝒟 ?lhs›
    proof (elim disjE)
      assume ‹v' ∈ 𝒟 (Q r)›
      hence ‹?map u' @ v' ∈ 𝒟 (P ;✓ Q)›
        by (simp add: Seqptick_projs)
          (metis F_T ‹(u' @ [✓(r)], ev ` S) ∈ ℱ P› append_T_imp_tF not_Cons_self)
      with mem_D_imp_mem_D_Hiding show ‹?th (?map u' @ v') ∈ 𝒟 ?lhs› .
    next
      assume ‹isInfHidden_seqRun x (Q r) S v'›
      hence ‹isInfHidden_seqRun x (P ;✓ Q) S (?map u' @ v')›
        by (simp add: seqRun_def image_iff Seqptick_projs)
          (metis F_T ‹(u' @ [✓(r)], ev ` S) ∈ ℱ P› append_T_imp_tF list.discI)
      thus ‹?th (?map u' @ v') ∈ 𝒟 ?lhs›
        by (simp add: D_Hiding_seqRun)
          (metis append.right_neutral filter_append
            ftF_Nil isInfHidden_seqRun_imp_tF)
    qed
    also have ‹?th (?map u' @ v') = ?map (?th u') @ ?th v'›
      using D_Q(4) Hiding_tF ‹u = ?th u'› tF_trace_hide_map_ev_comp_of_ev by auto
    finally have ‹?map (?th u') @ ?th v' ∈ 𝒟 ?lhs› .
    moreover have ‹tF (?map (?th u') @ ?th v')›
      by (simp add: "*"(2) Hiding_tF)
    ultimately show ‹t ∈ 𝒟 ?lhs›
      unfolding "*"(1) D_Q(1) ‹u = ?th u'› using ‹ftF w'›
      by (metis append.assoc is_processT7)
  qed
next

  assume subset_div : ‹𝒟 ?rhs ⊆ 𝒟 ?lhs›
  let ?th = ‹λt. trace_hide t (ev ` S)› and ?map = ‹λt. map (ev ∘ of_ev) t›
  fix t X assume ‹(t, X) ∈ ℱ ?rhs›
  then consider (div) ‹t ∈ 𝒟 ?rhs›
    | (F_P) u where ‹t = ?map u› ‹(u, ref_Seqptick X) ∈ ℱ (P \ S)› ‹u ∉ 𝒟 (P \ S)› ‹tF u›
    | (F_Q) u r v where ‹t = ?map u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P \ S)› ‹u @ [✓(r)] ∉ 𝒟 (P \ S)›
      ‹tF u› ‹(v, X) ∈ ℱ (Q r \ S)› ‹v ∉ 𝒟 (Q r \ S)›
    by (simp add: Seqptick_projs)
      (metis F_T T_imp_ftF ftF_Nil is_processT9 self_append_conv)
  thus ‹(t, X) ∈ ℱ ?lhs›
  proof cases
    case div with subset_div show ‹(t, X) ∈ ℱ ?lhs›
      by (simp add: in_mono is_processT8)
  next
    case F_P
    from F_P(2, 3) obtain u' where * : ‹u = ?th u'› ‹(u', ref_Seqptick X ∪ ev ` S) ∈ ℱ P›
      unfolding F_Hiding D_Hiding by fast
    have ‹tF u'› using "*"(1) F_P(4) Hiding_tF by blast
    have $ : ‹ref_Seqptick (X ∪ ev ` S) = ref_Seqptick X ∪ ev ` S›
      by (auto simp add: image_iff ref_Seqptick_def)
        (metis Int_iff Un_iff eventptick.sel(1) image_eqI rangeI)
    from ‹tF u'› "*"(2) have ‹(?map u', X ∪ ev ` S) ∈ ℱ (P ;✓ Q)›
      by (auto simp add: Seqptick_projs "$")
    thus ‹(t, X) ∈ ℱ ?lhs›
      by (simp add: F_Hiding)
        (metis "*"(1) F_P(1) ‹tF u'› tF_trace_hide_map_ev_comp_of_ev)
  next
    case F_Q
    from F_Q(2, 3) obtain u' where ‹u @ [✓(r)] = ?th u'› ‹(u', ev ` S) ∈ ℱ P›
      unfolding T_Hiding D_Hiding by fast
    then obtain u' where * : ‹u = ?th u'› ‹(u' @ [✓(r)], ev ` S) ∈ ℱ P›
      by (cases u' rule: rev_cases, simp_all split: if_split_asm)
        (metis Hiding_tF eventptick.disc(2) ftF_nonempty_append_imp is_processT2
          not_Cons_self2 tF_Cons_iff tF_append_iff)
    from F_Q(5, 6) obtain v' where ** : ‹v = ?th v'› ‹(v', X ∪ ev ` S) ∈ ℱ (Q r)›
      unfolding F_Hiding D_Hiding by blast
    have ‹(?map u' @ v', X ∪ ev ` S) ∈ ℱ (P ;✓ Q)›
      by (simp add: Seqptick_projs)
        (metis "*"(2) "**"(2) F_T append_T_imp_tF list.distinct(1))
    with F_Q(4) show ‹(t, X) ∈ ℱ ?lhs›
      by (simp add: F_Hiding F_Q(1) "*"(1) "**"(1))
        (metis Hiding_tF filter_append tF_trace_hide_map_ev_comp_of_ev)
  qed
qed

(* 
Hiding_Seqptick_FD_Seqptick_Hiding (λr. (SEQ✓ l ∈@ L. P l) r \ S) = SEQ✓ l ∈@ L. (λr. P l r \ S)
 *)
corollary Hiding_MultiSeqptick_FD_MultiSeqptick_Hiding :
  ‹(SEQ✓ l ∈@ L. P l) r \ S ⊑FD (SEQ✓ l ∈@ L. (λr. P l r \ S)) r›
  by (induct L arbitrary: r rule: induct_list012)
    (auto intro: trans_FD[OF Hiding_Seqptick_FD_Seqptick_Hiding] mono_Seqptick_FD)



text ‹If we assume term‹𝔽✓(P)›, we can recover the equality (new in Isabelle26).›

theorem finite_ticks_Hiding_Seqptick :
  ‹(P ;✓ Q) \ S = (P \ S) ;✓ (λr. Q r \ S)› (is ‹?lhs = ?rhs›) if ‹𝔽✓(P)›
for P :: ‹('a, 'r) processptick› and Q :: ‹'r ⇒ ('a, 's) processptick›
proof (rule FD_antisym)
  from Hiding_Seqptick_FD_Seqptick_Hiding show ‹?lhs ⊑FD ?rhs› .
next
  let ?th = ‹λt. trace_hide t (ev ` S)› and ?map = ‹λt. map (ev ∘ of_ev) t›
  show ‹?rhs ⊑FD ?lhs›
  proof (rule failure_divergence_refine_optimizedI)
    assume subset_div : ‹𝒟 ?lhs ⊆ 𝒟 ?rhs›
    fix t X assume ‹(t, X) ∈ ℱ ?lhs›
    then consider (div) ‹t ∈ 𝒟 ?lhs›
      | (not_div) t' where ‹t = ?th t'› ‹(t', X ∪ ev ` S) ∈ ℱ (P ;✓ Q)› ‹t' ∉ 𝒟 (P ;✓ Q)›
      by (simp add: F_Hiding D_Hiding) (use div mem_D_imp_mem_D_Hiding in blast)
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      case div with subset_div show ‹(t, X) ∈ ℱ ?rhs›
        by (simp add: in_mono is_processT8)
    next
      case not_div
      from not_div(2, 3) consider (F_P) u where ‹t' = ?map u› ‹(u, ref_Seqptick (X ∪ ev ` S)) ∈ ℱ P› ‹tF u›
        | (F_Q) u r v where ‹t' = ?map u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹tF u› ‹(v, X ∪ ev ` S) ∈ ℱ (Q r)›
        unfolding Seqptick_projs by fast
      thus ‹(t, X) ∈ ℱ ?rhs›
      proof cases
        case F_P
        from F_P(2) have ‹(?th u, ref_Seqptick X) ∈ ℱ (P \ S)›
          by (auto simp add: F_Hiding ref_Seqptick_union_image_ev)
        hence ‹(?map (?th u), X) ∈ ℱ ?rhs›
          by (simp add: Seqptick_projs) (metis F_P(3) Hiding_tF)
        also have ‹?map (?th u) = t›
          by (metis not_div(1) F_P(1, 3) tF_trace_hide_map_ev_comp_of_ev)
        finally show ‹(t, X) ∈ ℱ ?rhs› .
      next
        case F_Q
        from mem_T_imp_mem_T_Hiding F_Q(2) have ‹?th (u @ [✓(r)]) ∈ 𝒯 (P \ S)› .
        also have ‹?th (u @ [✓(r)]) = ?th u @ [✓(r)]› by (simp add: image_iff)
        finally have ‹?th u @ [✓(r)] ∈ 𝒯 (P \ S)› .
        moreover from F_Q(4) have ‹(?th v, X) ∈ ℱ (Q r \ S)› by (auto simp add: F_Hiding)
        ultimately have ‹(?map (?th u) @ ?th v, X) ∈ ℱ ?rhs›
          by (simp add: Seqptick_projs) (metis append_T_imp_tF not_Cons_self2)
        also have ‹?map (?th u) @ ?th v = t›
          by (simp add: not_div(1) F_Q(1, 3) tF_trace_hide_map_ev_comp_of_ev)
        finally show ‹(t, X) ∈ ℱ ?rhs› .
      qed
    qed
  next
    fix t assume ‹t ∈ 𝒟 ?lhs›
    then obtain u v x where * : ‹t = ?th u @ v› ‹tF u› ‹ftF v›
      ‹u ∈ 𝒟 (P ;✓ Q) ∨ isInfHidden_seqRun_strong x (P ;✓ Q) S u›
      by (blast elim: D_Hiding_seqRunE)
    from "*"(4) have ‹?th u ∈ 𝒟 ?rhs›
    proof (elim disjE)
      assume ‹u ∈ 𝒟 (P ;✓ Q)›
      then consider (D_P) u' v' where ‹u = ?map u' @ v'› ‹u' ∈ 𝒟 P› ‹tF u'› ‹ftF v'›
        | (D_Q) u' r v' where ‹u = ?map u' @ v'› ‹u' @ [✓(r)] ∈ 𝒯 P› ‹tF u'› ‹v' ∈ 𝒟 (Q r)›
        unfolding Seqptick_projs by blast
      thus ‹?th u ∈ 𝒟 ?rhs›
      proof cases
        case D_P
        from mem_D_imp_mem_D_Hiding D_P(2) have ‹?th u' ∈ 𝒟 (P \ S)› .
        with D_P(3) have ‹?map (?th u') ∈ 𝒟 ?rhs›
          by (simp add: Seqptick_projs)
            (metis Hiding_tF append.right_neutral ftF_Nil)
        also have ‹?map (?th u') = ?th (?map u')›
          by (simp add: D_P(3) tF_trace_hide_map_ev_comp_of_ev)
        finally have ‹?th (?map u') ∈ 𝒟 ?rhs› .
        thus ‹?th u ∈ 𝒟 ?rhs›
          by (simp add: D_P(1))
            (metis (lifting) "*"(2) D_P(1) filter_map is_processT7 tF_append_iff
              tF_iff_is_map_ev tF_imp_ftF)
      next
        case D_Q
        from mem_T_imp_mem_T_Hiding D_Q(2) have ‹?th (u' @ [✓(r)]) ∈ 𝒯 (P \ S)› .
        also have ‹?th (u' @ [✓(r)]) = ?th u' @ [✓(r)]› by (simp add: image_iff)
        finally have ‹?th u' @ [✓(r)] ∈ 𝒯 (P \ S)› .
        moreover from mem_D_imp_mem_D_Hiding D_Q(4) have ‹?th v' ∈ 𝒟 (Q r \ S)› .
        ultimately have ‹?map (?th u') @ ?th v' ∈ 𝒟 ?rhs›
          by (simp add: Seqptick_projs) (metis append_T_imp_tF not_Cons_self2)
        also have ‹?map (?th u') @ ?th v' = ?th u›
          by (simp add: D_Q(1, 3) tF_trace_hide_map_ev_comp_of_ev)
        finally show ‹?th u ∈ 𝒟 ?rhs› .
      qed
    next
      assume assm : ‹isInfHidden_seqRun_strong x (P ;✓ Q) S u›
      hence € : ‹x i ∈ ev ` S› for i by blast
      define U2 :: ‹('a, 'r) traceptick set›
        where ‹U2 ≡ {u' |u'. u' ∈ 𝒯 P ∧ u' ∉ 𝒟 P ∧ tF u'}›
      define U3 :: ‹('a, 's) traceptick set›
        where ‹U3 ≡ {?map u' @ v' | u' r v'. u' @ [✓(r)] ∈ 𝒯 P ∧ u' ∉ 𝒟 P ∧ tF u' ∧ v' ∈ 𝒯 (Q r) ∧ v' ∉ 𝒟 (Q r)}›
      have ‹seqRun u x i ∈ ?map ` U2 ∪ U3› for i
        using assm[rule_format, of i]
        by (simp add: U2_def U3_def Seqptick_projs image_iff, safe, simp_all)
          ((auto)[1], metis T_imp_ftF)
      then consider ‹infinite {i. seqRun u x i ∈ ?map ` U2}›
        | j where ‹finite {i. seqRun u x i ∈ ?map ` U2}› ‹⋀i. j ≤ i ⟹ seqRun u x i ∈ U3›
        by (metis (no_types, lifting) Un_iff ex_least_nat_le finite_nat_set_iff_bounded mem_Collect_eq order_class.order_eq_iff)
      thus ‹?th u ∈ 𝒟 ?rhs›
      proof cases
        assume ‹infinite {i. seqRun u x i ∈ ?map ` U2}›
        hence ‹∃∞i. seqRun u x i ∈ ?map ` U2›
          by (simp add: frequently_cofinite)
        then obtain f :: ‹nat ⇒ nat›
          where $ : ‹strict_mono f› ‹⋀i. seqRun u x (f i) ∈ ?map ` U2›
          by (blast dest: extraction_subseqD[where σ = id, simplified])
        define g :: ‹nat ⇒ ('a, 'r) eventptick list›
          where ‹g i ≡ ?map (seqRun u x (f i))› for i
        from "$"(1) have ‹strict_mono g›
          by (auto intro!: strict_monoI simp add: g_def)
            (metis strict_mono_less strict_mono_map strict_mono_seqRun)
        moreover from "$"(2) have ‹g i ∈ 𝒯 P› for i
          by (simp add: g_def U2_def image_iff)
            (metis tF_map_ev_of_ev_eq_iff)
        moreover have ‹?th (g i) = ?th (g 0)› for i
        proof -
          have ‹g i = ?map (seqRun u x (f i))› by (simp only: g_def)
          also from assm have ‹?th … = ?th (?map u)›
            by (simp add: seqRun_def image_iff filter_empty_conv) (metis eventptick.sel(1))
          also from assm have ‹… = ?th (?map (seqRun u x (f 0)))›
            by (simp add: seqRun_def image_iff filter_empty_conv) (metis eventptick.sel(1))
          also have ‹?map (seqRun u x (f 0)) = g 0› by (simp only: g_def)
          finally show ‹?th (g i) = ?th (g 0)› .
        qed
        ultimately have ‹isInfHiddenRun g P S› by blast
        moreover from assm have ‹?map (?th u) = ?th (g 0) @ []›
          by (fold tF_trace_hide_map_ev_comp_of_ev[OF ‹tF u›],
              simp add: g_def seqRun_def image_iff filter_empty_conv)
            (metis eventptick.sel(1))
        moreover have ‹tF (g 0)› by (simp add: g_def)
        moreover have ‹ftF []› by simp
        moreover have ‹g 0 ∈ range g› by simp
        ultimately have ‹?map (?th u) ∈ 𝒟 (P \ S)›
          unfolding D_Hiding by blast
        thus ‹?th u ∈ 𝒟 ?rhs›
          by (simp add: Seqptick_projs)
            (metis "*"(2) ‹ftF []› append.right_neutral filter_map
              tF_map_ev_comp tF_map_ev_of_ev_eq_iff)
      next
        fix j assume $ : ‹finite {i. seqRun u x i ∈ ?map ` U2}› ‹⋀i. j ≤ i ⟹ seqRun u x i ∈ U3›
        let ?pred = ‹λi u' r' v'. seqRun u x (i + j) = ?map u' @ v' ∧ u' @ [✓(r')] ∈ 𝒯 P ∧
                                     u' ∉ 𝒟 P ∧ tF u' ∧ v' ∈ 𝒯 (Q r') ∧ v' ∉ 𝒟 (Q r')›
        define u'_r'_v' where "£" : ‹u'_r'_v' i ≡ SOME u'_r'_v'. ?pred i (fst u'_r'_v')
                                                  (fst (snd u'_r'_v')) (snd (snd u'_r'_v'))› for i
        define u' r' v'
          where "££" : ‹u' i ≡ fst (u'_r'_v' i)› ‹r' i ≡ fst (snd (u'_r'_v' i))›
            ‹v' i ≡ snd (snd (u'_r'_v' i))› for i
        from "$"(2) have ‹∃u'_r'_v'. ?pred i (fst u'_r'_v') (fst (snd u'_r'_v')) (snd (snd u'_r'_v'))› for i
          by (simp add: U3_def)
        from someI_ex[OF this, folded "£"]
        have $$ : ‹?pred i (u' i) (r' i) (v' i)› for i by (simp_all add: "££")
        show ‹?th u ∈ 𝒟 ?rhs›
        proof (cases ‹finite (range u')›)
          assume ‹infinite (range u')›
          hence ‹∃f :: nat ⇒ _. strict_mono f ∧ range f ⊆ {t. ∃t'∈range u'. t ≤ t'}›
          proof (intro KoenigLemma allI)
            fix i
            have ‹{t. ∃t'∈range u'. t = take i t'} ⊆ ?map ` {t. t ≤ seqRun u x (i + j)}›
            proof (rule subsetI)
              fix t' assume ‹t' ∈ {t. ∃t'∈range u'. t = take i t'}›
              then obtain i' where ‹t' = take i (u' i')› by blast
              from "$$"[of i'] have ‹seqRun u x (i' + j) = ?map (u' i') @ v' i'› by argo
              hence ‹?map (u' i') ≤ seqRun u x (i' + j)› by auto
              from this[THEN mono_take, of i]
              have ‹?map (take i (u' i')) ≤ seqRun u x (min (i - length u) (i' + j))›
                by (simp add: min.commute take_map split: if_split_asm)
                  (metis prefix_prefix append_take_drop_id take_map)
              also have ‹… ≤ seqRun u x (i + j)› by simp
              finally have ‹?map (take i (u' i')) ≤ seqRun u x (i + j)› .
              with "$$" ‹t' = take i (u' i')› show ‹t' ∈ ?map ` {t. t ≤ seqRun u x (i + j)}›
                by (simp add: image_iff)
                  (metis append_take_drop_id map_ev_of_ev_map_ev_of_ev
                    tF_append_iff tF_map_ev_of_ev_same_type_is)
            qed
            moreover have ‹finite …› by (simp add: prefixes_fin)
            ultimately show ‹finite {t. ∃t'∈range u'. t = take i t'}›
              by (meson finite_subset)
          qed
          then obtain f :: ‹nat ⇒ _›
            where $$$ : ‹strict_mono f› ‹range f ⊆ {t. ∃t'∈range u'. t ≤ t'}› by blast
          define g :: ‹nat ⇒ ('a, 'r) traceptick› where ‹g ≡ ?map ∘ f ∘ ((+) (length u))›
          have $$$$ : ‹length u ≤ length (g i)› for i
            by (simp add: g_def)
              (metis "$$$"(1) add_leE length_strict_mono)
          have ‹?th (g i) = ?th (?map u)› for i
          proof -
            from "$$$"(2) "$$" obtain i' where ‹g i ≤ u' i'›
              by (simp add: g_def subset_iff)
                (metis prefixE range_eqI tF_append_iff tF_map_ev_of_ev_same_type_is)
            also from "$$" have ‹… ≤ ?map (seqRun u x (i' + j))›
              by (simp add: tF_map_ev_of_ev_same_type_is)
            finally have ‹g i ≤ ?map (seqRun u x (i' + j))› .
            with "$$$$" obtain i'' where ‹g i = ?map u @ seqRun [] ((ev ∘ of_ev) ∘ x) i''›
              by (auto simp add: less_eq_list_def less_list_def prefix_def map_eq_append_conv seqRun_def append_eq_append_conv2)
                (metis append.right_neutral append_eq_append_conv le_add1 length_append length_map order_antisym_conv,
                  metis (no_types, lifting) add.left_neutral append_eq_conv_conj le_add1 le_add_diff_inverse length_append length_upt take_upt)
            with "€" show ‹?th (g i) = ?th (?map u)›
              by (simp add: trace_hide_is_Nil_iff, simp add: image_iff subset_iff)
                (metis eventptick.sel(1))
          qed
          moreover have ‹strict_mono g›
            by (simp add: g_def "$$$"(1) comp_def strict_mono_map strict_monoD strict_monoI)
          moreover from "$$" "$$$"(2) have ‹g i ∈ 𝒯 P› for i
            by (simp add: g_def subset_iff image_iff)
              (metis tF_append_iff map_ev_of_ev_map_ev_of_ev
                is_processT3_TR_append prefixE tF_map_ev_of_ev_eq_iff)
          ultimately have ‹?th (?map u) ∈ 𝒟 (P \ S)›
            by (simp add: D_Hiding)
              (metis (lifting) ext Hiding_tF append_Nil2 ftF_Nil
                rangeI tF_map_ev_comp)
          thus ‹?th u ∈ 𝒟 ?rhs›
            by (simp add: Seqptick_projs)
              (metis (lifting) ext "*"(2) tF_trace_hide_map_ev_comp_of_ev[of u S] append_Nil2
                ftF_Nil map_ev_of_ev_map_ev_of_ev tF_map_ev_comp tF_map_ev_of_ev_same_type_is)
        next
          assume ‹finite (range u')›
          have ‹range r' ⊆ (⋃u''∈ range u'. {r''. u'' @ [✓(r'')] ∈ 𝒯 P ∧ u'' ∉ 𝒟 P})›
            using "$$" by fast
          moreover have ‹finite …›
            by (rule finite_UN_I[OF ‹finite (range u')›])
              (simp add: finite_ticksD ‹𝔽✓(P)›)
          ultimately have ‹finite (range r')›
            using finite_subset by blast
          have ‹infinite (range v')›
          proof (rule notI)
            assume ‹finite (range v')›
            from "$$" have ‹range (λi. seqRun u x (i + j)) ⊆
                            (λ(u'', v''). u'' @ v'') ` ((?map ` (range u')) × range v')› by auto
            moreover have ‹finite …›
              by (simp add: ‹finite (range u')› ‹finite (range v')›)
            ultimately have ‹finite (range (λi. seqRun u x (i + j)))›
              by (meson finite_subset)
            moreover have ‹range (seqRun u x) = range (λi. seqRun u x (i + j)) ∪ seqRun u x ` {..j}›
              by (auto simp add: image_iff) presburger
            ultimately have ‹finite (range (seqRun u x))› by simp
            with infinite_range_seqRun show False ..
          qed
          { assume hyp : ‹∀u'' ∈ range u'. ∀r'' ∈ range r'. finite {i. ?pred i u'' r'' (v' i)}›
            from "$$" have ‹range v' = (⋃u'' ∈ range u'. ⋃r'' ∈ range r'. v' ` {i. ?pred i u'' r'' (v' i)})›
              by (auto simp add: image_iff)
            also from hyp ‹finite (range u')› ‹finite (range r')› have ‹finite …› by blast
            finally have ‹finite (range v')› .
            with ‹infinite (range v')› have False ..
          }
          then obtain u'' r'' where ‹infinite {i. ?pred i u'' r'' (v' i)}› by blast
          hence ‹∃∞i. ?pred i u'' r'' (v' i)›
            by (simp add: frequently_cofinite)
          then obtain f :: ‹nat ⇒ nat›
            where $$$ : ‹strict_mono f› ‹⋀i. ?pred (f i) u'' r'' (v' (f i))›
            by (blast dest: extraction_subseqD[where σ = id, simplified])
          have ‹?th (u'' @ [✓(r'')]) ∈ 𝒯 (P \ S)›
            by (rule mem_T_imp_mem_T_Hiding) (simp add: "$$$"(2))
          also have ‹?th (u'' @ [✓(r'')]) = ?th u'' @ [✓(r'')]›
            by (simp add: image_iff)
          finally have ‹?th u'' @ [✓(r'')] ∈ 𝒯 (P \ S)› .
          moreover have ‹?th (v' (f 0)) ∈ 𝒟 (Q r'' \ S)›
          proof -
            have ‹ftF []› by simp
            moreover from "$$$"(2)[of 0, THEN conjunct1, THEN arg_cong[where f = tF]] assm "*"(2)
            have ‹tF (v' (f 0))›
              by (simp add: tF_seqRun_iff image_iff) (metis eventptick.disc(1))
            moreover have ‹strict_mono (v' ∘ f)›
            proof (rule strict_monoI)
              fix i1 i2 :: nat assume ‹i1 < i2›
              hence ‹f i1 + j < f i2 + j› by (simp add: "$$$"(1) strict_mono_less)                                                                       
              hence ‹seqRun u x (f i1 + j) < seqRun u x (f i2 + j)› by simp
              with "$$$"(2)[of i1] "$$$"(2)[of i2]
              show ‹(v' ∘ f) i1 < (v' ∘ f) i2› by simp                                                                                                   
            qed                                                                     
            moreover have ‹(v' ∘ f) i ∈ 𝒯 (Q r'')› for i by (simp add: "$$$"(2))
            moreover have ‹?th ((v' ∘ f) i) = ?th ((v' ∘ f) 0)› for i
              using "$$$"(2)[of i, THEN conjunct1, THEN arg_cong[where f = ?th]]
                "$$$"(2)[of 0, THEN conjunct1, THEN arg_cong[where f = ?th]]
              by (simp add: trace_hide_seqRun_eq_iff[THEN iffD2, rule_format, OF "€"])
            moreover have ‹v' (f 0) ∈ range (v' ∘ f)› by simp
            ultimately show ‹?th (v' (f 0)) ∈ 𝒟 (Q r'' \ S)›
              unfolding D_Hiding by blast
          qed
          ultimately have ‹?map (?th u'') @ ?th (v' (f 0)) ∈ 𝒟 ?rhs›
            by (simp add: Seqptick_projs)
              (metis append_T_imp_tF not_Cons_self2)
          also from "$$$"(2)[of 0, THEN conjunct1, THEN arg_cong[where f = ?th, symmetric]] assm
          have ‹?map (?th u'') @ ?th (v' (f 0)) = ?th u›
            by (simp, subst (asm) tF_trace_hide_map_ev_comp_of_ev, solves ‹simp add: "$$$"(2)›)
              (simp, use trace_hide_seqRun_eq_iff in blast)
          finally show ‹?th u ∈ 𝒟 ?rhs› .
        qed
      qed
    qed
    moreover from "*"(2) Hiding_tF have ‹tF (?th u)› by blast
    ultimately show ‹t ∈ 𝒟 ?rhs›
      unfolding "*"(1) using "*"(3) by (fact is_processT7)
  qed
qed


corollary Hiding_Seq_unit : ‹P ; Q \ S = (P \ S) ; (Q \ S)› for P :: ‹'a process›
  by (simp flip: Seqptick_const add: finite_ticks_Hiding_Seqptick finite_ticks_simps)


corollary finite_ticks_Hiding_MultiSeqptick :
  ‹(⋀l r. l ∈ set (butlast L) ⟹ 𝔽✓(P l r)) ⟹
   (λr. (SEQ✓ l ∈@ L. P l) r \ S) = SEQ✓ l ∈@ L. (λr. P l r \ S)›
proof (induct L rule: induct_list012)
  case 1 show ?case by simp
next
  case 2 show ?case by simp
next
  case (3 l0 l1 L)
  have ‹(λr. (SEQ✓ l ∈@ (l0 # l1 # L). P l) r \ S) =
        (λr. (P l0 r \ S) ;✓ (λr. (SEQ✓ l ∈@ (l1 # L). P l) r \ S))›
    by (subst MultiSeqptick_Cons, subst finite_ticks_Hiding_Seqptick)
      (simp_all add: "3.prems")
  also have ‹(λr. (SEQ✓ l ∈@ (l1 # L). P l) r \ S) = SEQ✓ l ∈@ (l1 # L). (λr. P l r \ S)›
    by (rule "3.hyps"(2)) (simp add: "3.prems")
  finally show ?case by simp
qed

corollary Hiding_MultiSeq_unit :
  ‹(SEQ l ∈@ L. P l) \ S = SEQ l ∈@ L. (P l \ S)›
  (is ‹?lhs = ?rhs›) for P :: ‹'b ⇒ 'a process›
using  finite_ticks_Hiding_MultiSeqptick[of L ‹λl r. P l›, simplified]
proof (cases ‹L = []›)
  show ‹L = [] ⟹ ?lhs = ?rhs› by simp
next
  assume ‹L ≠ []›
  hence ‹?lhs = (SEQ✓ l ∈@ L. (λr. P l)) () \ S› by simp
  also have ‹… = (SEQ✓ l ∈@ L. (λr. P l \ S)) ()›
    by (rule finite_ticks_Hiding_MultiSeqptick[THEN fun_cong]) (simp add: finite_ticks_simps)
  also have ‹… = ?rhs› by simp
  finally show ‹?lhs = ?rhs› .
qed


section ‹Hiding and Synchronization Product›

lemma setinterleavesptick_imp_superset_ev :
  ‹t setinterleaves✓⇘tj⇙ ((u, v), A) ⟹
   {ev a |a. ev a ∈ set u} ∪ {ev a |a. ev a ∈ set v} ⊆ {ev a |a. ev a ∈ set t}›
proof (induct t arbitrary: u v)
  case Nil thus ?case by (auto dest: Nil_setinterleavesptick)
next
  case (Cons e t)
  from Cons.prems consider (mv_left) a u' where ‹e = ev a› ‹u = ev a # u'›
    ‹t setinterleaves✓⇘tj⇙ ((u', v), A)›
  | (mv_right) a v' where ‹e = ev a› ‹v = ev a # v'›
    ‹t setinterleaves✓⇘tj⇙ ((u, v'), A)›
  | (mv_both_ev) a u' v' where ‹e = ev a› ‹u = ev a # u'› ‹v = ev a # v'›
    ‹t setinterleaves✓⇘tj⇙ ((u', v'), A)›
  | (mv_both_tick) r s u' v' where ‹u = ✓(r) # u'› ‹v = ✓(s) # v'›
    ‹t setinterleaves✓⇘tj⇙ ((u', v'), A)›
    by (cases e) (auto elim: Cons_ev_setinterleavesptickE Cons_tick_setinterleavesptickE)
  thus ?case by cases (auto dest!: Cons.hyps)
qed


lemma (in Synchroptick) disjoint_isInfHidden_seqRunL_to_Syncptick :
  assumes ‹A ∩ S = {}› and ‹isInfHidden_seqRun x P A t_P›
    and ‹t_Q ∈ 𝒯 Q› and ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
  shows ‹isInfHidden_seqRun (ev ∘ of_ev ∘ x) (P ⟦S⟧✓ Q) A t›
proof -
  have tF_x : ‹tF (map x [0..<i])› for i
    by (metis assms(2) imageE is_ev_def seqRun_def tF_append_iff
        tF_map_tick_comp_iff tF_seqRun_iff)
  define t' where ‹t' i ≡ t @ map (ev ∘ of_ev) (map x [0..<i])› for i
  from assms(1, 2) have ‹{a. ev a ∈ set (map x [0..<i])} ∩ S = {}› for i
    by (simp add: disjoint_iff image_iff) (metis eventptick.inject(1))
  from tF_disjoint_setinterleavesptick_append_tailL[OF tF_x this assms(4)]
  have ‹seqRun t (ev ∘ of_ev ∘ x) i setinterleaves✓⇘(⊗✓)⇙ ((seqRun t_P x i, t_Q), S)› for i
    by (simp add: seqRun_def)
  moreover have ‹of_ev (x i) ∈ A› for i
    by (metis assms(2) eventptick.sel(1) image_iff)
  ultimately show ‹isInfHidden_seqRun (ev ∘ of_ev ∘ x) (P ⟦S⟧✓ Q) A t›
    using assms(2, 3) by (auto simp add: T_Syncptick)
qed

lemma (in Synchroptick) disjoint_isInfHidden_seqRunR_to_Syncptick :
  ‹⟦A ∩ S = {}; isInfHidden_seqRun x Q A t_Q; t_P ∈ 𝒯 P;
    t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)⟧ ⟹
   isInfHidden_seqRun (ev ∘ of_ev ∘ x) (P ⟦S⟧✓ Q) A t›
  by (fold Syncptick_dual, rule Synchroptick.disjoint_isInfHidden_seqRunL_to_Syncptick)
    (use setinterleavesptick_dual in ‹blast intro: Synchroptick_dual.Synchroptick_axioms›)+



lemma (in Synchroptick) disjoint_Hiding_Syncptick_FD_Syncptick_Hiding_aux :
  ― ‹This lemma avoids duplication of the proof work.›
  assumes ‹A ∩ S = {}› ‹tF u› ‹ftF v› ‹t_P ∈ 𝒟 (P \ A)› ‹t_Q ∈ 𝒯 (Q \ A)›
    and * : ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
  shows ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
proof -
  let ?th_A = ‹λt. trace_hide t (ev ` A)›
  from ‹t_P ∈ 𝒟 (P \ A)› obtain t_P1 t_P2 
    where D_P : ‹tF t_P1› ‹ftF t_P2› ‹t_P = ?th_A t_P1 @ t_P2›
      ‹t_P1 ∈ 𝒟 P ∨ (∃t_P_x. isInfHidden_seqRun_strong t_P_x P A t_P1)›
    by (blast elim: D_Hiding_seqRunE)
  from setinterleavesptick_appendL[OF "*"[unfolded D_P(3)]] obtain u1 u2 t_Q1 t_Q2
    where ** : ‹u = u1 @ u2› ‹t_Q = t_Q1 @ t_Q2›
      ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P1, t_Q1), S)›
      ‹u2 setinterleaves✓⇘(⊗✓)⇙ ((t_P2, t_Q2), S)› by blast
  from ‹t_Q ∈ 𝒯 (Q \ A)› consider t_Q1' where ‹t_Q = ?th_A t_Q1'› ‹(t_Q1', ev ` A) ∈ ℱ Q›
    | (D_Q) t_Q1' t_Q2' where ‹tF t_Q1'› ‹ftF t_Q2'› ‹t_Q = ?th_A t_Q1' @ t_Q2'›
      ‹t_Q1' ∈ 𝒟 Q ∨ (∃t_Q_x. isInfHidden_seqRun_strong t_Q_x Q A t_Q1')›
    by (elim T_Hiding_seqRunE)
  thus ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
  proof cases
    fix t_Q1' assume ‹t_Q = ?th_A t_Q1'› ‹(t_Q1', ev ` A) ∈ ℱ Q›
    from ‹t_Q = ?th_A t_Q1'› "**"(2) obtain t_Q1''
      where ‹t_Q1 = ?th_A t_Q1''› ‹t_Q1'' ≤ t_Q1'›
      by (metis Prefix_Order.prefixI le_trace_hide)
    from F_T ‹(t_Q1', ev ` A) ∈ ℱ Q› ‹t_Q1'' ≤ t_Q1'› is_processT3_TR
    have ‹t_Q1'' ∈ 𝒯 Q› by blast
    from "**"(3)[unfolded ‹t_Q1 = ?th_A t_Q1''›,
        THEN disjoint_trace_hide_setinterleavesptick[OF ‹A ∩ S = {}›]]
    obtain u1' where ‹u1 = ?th_A u1'› ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› by blast
    from D_P(4) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
    proof (elim disjE exE)
      assume ‹t_P1 ∈ 𝒟 P›
      with ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› D_P(1) setinterleavesptick_tF_imp
      have ‹u1' = u1' @ []› ‹tF u1'› ‹ftF []›
        ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› ‹t_P1 ∈ 𝒟 P›
        by simp_all (blast intro: is_processT3_TR)+
      with ‹t_Q1'' ∈ 𝒯 Q› have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)› unfolding D_Syncptick by blast
      moreover have ‹u @ v = ?th_A u1' @ (u2 @ v)›
        by (simp add: "*"(1) "**"(1) ‹u1 = ?th_A u1'›)
      ultimately show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
        unfolding D_Hiding using ‹tF u› ‹ftF v› "**"(1) ‹tF u1'›
        by (auto intro: ftF_append)
    next
      fix t_P_x assume ‹isInfHidden_seqRun_strong t_P_x P A t_P1›
      hence ‹isInfHidden_seqRun (ev ∘ of_ev ∘ t_P_x) (P ⟦S⟧✓ Q) A u1'›
        by (intro disjoint_isInfHidden_seqRunL_to_Syncptick
            [OF ‹A ∩ S = {}› _ ‹t_Q1'' ∈ 𝒯 Q› ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)›]) simp
      with "**"(1) ‹u1 = ?th_A u1'› assms(2, 3) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
        unfolding D_Hiding_seqRun by clarify
          (metis append_eq_append_conv2[of u1 ‹u2 @ v› ‹u1 @ u2› v]
            isInfHidden_seqRun_imp_tF[of u1' ‹ev ∘ of_ev ∘ t_P_x› ‹P ⟦S⟧✓ Q› A]
            ftF_append[of u2 v] tF_append_iff[of u1 u2])
    qed
  next
    case D_Q
    from setinterleavesptick_le_prefixLR
      [OF "*"[unfolded D_P(3) D_Q(3)], of ‹?th_A t_P1› ‹?th_A t_Q1'›]
    consider (left) u' t_Q1'' where ‹u' ≤ u› ‹t_Q1'' ≤ t_Q1'›
      ‹u' setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P1, ?th_A t_Q1''), S)›
    | (right) u' t_P1' where ‹u' ≤ u› ‹t_P1' ≤ t_P1›
      ‹u' setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P1', ?th_A t_Q1'), S)›
      by (auto dest!: le_trace_hide)
    thus ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
    proof cases
      case left
      have ‹t_Q1'' ∈ 𝒯 Q› by (meson D_Q(4) D_T is_processT3_TR left(2) t_le_seqRun)
      from disjoint_trace_hide_setinterleavesptick[OF ‹A ∩ S = {}› left(3)]
      obtain u'' where $ : ‹u' = ?th_A u''›
        ‹u'' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› by blast
      from D_P(4) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
      proof (elim disjE exE)
        assume ‹t_P1 ∈ 𝒟 P›
        hence ‹u'' ∈ 𝒟 (P ⟦S⟧✓ Q)›
          by (simp add: D_Syncptick)
            (metis "$"(2) D_P(1) ‹t_Q1'' ∈ 𝒯 Q› append.right_neutral
              ftF_Nil setinterleavesptick_tF_imp)
        with left(1) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (elim Prefix_Order.prefixE, simp add: D_Hiding "$"(1))
            (metis Hiding_tF assms(2, 3) ftF_append tF_append_iff)
      next
        fix t_P_x assume ‹isInfHidden_seqRun_strong t_P_x P A t_P1›
        hence ‹isInfHidden_seqRun (ev ∘ of_ev ∘ t_P_x) (P ⟦S⟧✓ Q) A u''›
          by (intro disjoint_isInfHidden_seqRunL_to_Syncptick
              [OF ‹A ∩ S = {}› _ ‹t_Q1'' ∈ 𝒯 Q› "$"(2)]) simp
        from left(1) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (elim Prefix_Order.prefixE, simp add: D_Hiding_seqRun "$"(1))
            (metis ‹?this› assms(2, 3) ftF_append
              isInfHidden_seqRun_imp_tF tF_append_iff)
      qed
    next
      case right
      have ‹t_P1' ∈ 𝒯 P› by (meson D_P(4) D_T is_processT3_TR right(2) t_le_seqRun)
      from disjoint_trace_hide_setinterleavesptick[OF ‹A ∩ S = {}› right(3)]
      obtain u'' where $ : ‹u' = ?th_A u''›
        ‹u'' setinterleaves✓⇘(⊗✓)⇙ ((t_P1', t_Q1'), S)› by blast
      from D_Q(4) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
      proof (elim disjE exE)
        assume ‹t_Q1' ∈ 𝒟 Q›
        hence ‹u'' ∈ 𝒟 (P ⟦S⟧✓ Q)›
          by (simp add: D_Syncptick)
            (metis "$"(2) D_Q(1) ‹t_P1' ∈ 𝒯 P› append.right_neutral
              ftF_Nil setinterleavesptick_tF_imp)
        with right(1) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (elim Prefix_Order.prefixE, simp add: D_Hiding "$"(1))
            (metis Hiding_tF assms(2, 3) ftF_append tF_append_iff)
      next
        fix t_Q_x assume ‹isInfHidden_seqRun_strong t_Q_x Q A t_Q1'›
        hence ‹isInfHidden_seqRun (ev ∘ of_ev ∘ t_Q_x) (P ⟦S⟧✓ Q) A u''›
          by (intro disjoint_isInfHidden_seqRunR_to_Syncptick
              [OF ‹A ∩ S = {}› _ ‹t_P1' ∈ 𝒯 P› "$"(2)]) simp
        from right(1) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (elim Prefix_Order.prefixE, simp add: D_Hiding_seqRun "$"(1))
            (metis ‹?this› assms(2, 3) ftF_append
              isInfHidden_seqRun_imp_tF tF_append_iff)
      qed
    qed
  qed
qed



theorem (in Synchroptick) disjoint_Hiding_Syncptick_FD_Syncptick_Hiding :
  ‹P ⟦S⟧✓ Q \ A ⊑FD (P \ A) ⟦S⟧✓ (Q \ A)› if ‹A ∩ S = {}›
proof (rule failure_divergence_refine_optimizedI)
  let ?th_A = ‹λt. trace_hide t (ev ` A)›
  fix t assume ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
  from this obtain u v t_P t_Q
    where * : ‹t = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 (P \ A) ∧ t_Q ∈ 𝒯 (Q \ A) ∨ t_P ∈ 𝒯 (P \ A) ∧ t_Q ∈ 𝒟 (Q \ A)›
    unfolding D_Syncptick by blast
  from "*"(5) show ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
  proof (elim disjE conjE)
    show ‹t_P ∈ 𝒟 (P \ A) ⟹ t_Q ∈ 𝒯 (Q \ A) ⟹ t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
      by (simp add: "*"(1-4) disjoint_Hiding_Syncptick_FD_Syncptick_Hiding_aux ‹A ∩ S = {}›)
  next
    assume ‹t_P ∈ 𝒯 (P \ A)› ‹t_Q ∈ 𝒟 (Q \ A)›
    have ‹u setinterleaves✓⇘λs r. r ⊗✓ s⇙ ((t_Q, t_P), S)›
      using "*"(4) setinterleavesptick_dual by blast
    from Synchroptick_dual.disjoint_Hiding_Syncptick_FD_Syncptick_Hiding_aux
      [OF ‹A ∩ S = {}› "*"(2, 3) ‹t_Q ∈ 𝒟 (Q \ A)› ‹t_P ∈ 𝒯 (P \ A)› this]
    have ‹u @ v ∈ 𝒟 (Synchroptick_dual.Syncptick Q S P \ A)› .
    also have ‹Synchroptick_dual.Syncptick Q S P = P ⟦S⟧✓ Q› by (fact Syncptick_dual)
    finally show ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)› unfolding "*"(1) .
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
    and subset_div : ‹𝒟 ((P \ A) ⟦S⟧✓ (Q \ A)) ⊆ 𝒟 (P ⟦S⟧✓ Q \ A)›
  from this(1) consider ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
    | (fail_Sync) t_P t_Q X_P X_Q where ‹(t_P, X_P) ∈ ℱ (P \ A)› ‹(t_Q, X_Q) ∈ ℱ (Q \ A)›
      ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› ‹X ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
    unfolding Syncptick_projs by blast
  thus ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
  proof cases
    from subset_div show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A)) ⟹ (t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
      by (simp add: in_mono is_processT8)
  next
    case fail_Sync
    from fail_Sync(1, 2) consider ‹t_P ∈ 𝒟 (P \ A) ∨ t_Q ∈ 𝒟 (Q \ A)›
      | (fail_Hiding) t_P' t_Q' where
        ‹t_P = trace_hide t_P' (ev ` A)› ‹(t_P', X_P ∪ ev ` A) ∈ ℱ P›
        ‹t_Q = trace_hide t_Q' (ev ` A)› ‹(t_Q', X_Q ∪ ev ` A) ∈ ℱ Q›
      unfolding F_Hiding D_Hiding by blast
    thus ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
    proof cases
      assume ‹t_P ∈ 𝒟 (P \ A) ∨ t_Q ∈ 𝒟 (Q \ A)›
      with fail_Sync(1-3) have ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
        by (simp add: D_Syncptick')
          (metis F_T append_self_conv ftF_Nil)
      with subset_div show ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
        by (simp add: in_mono is_processT8)
    next
      case fail_Hiding
      from disjoint_trace_hide_setinterleavesptick
        [OF ‹A ∩ S = {}› fail_Sync(3)[unfolded fail_Hiding(1, 3)]]
      obtain t' where * : ‹t = trace_hide t' (ev ` A)›
        ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)› by blast
      from fail_Sync(4) have ‹X ∪ ev ` A ⊆ super_ref_Syncptick (⊗✓) (X_P ∪ ev ` A) S (X_Q ∪ ev ` A)›
        by (auto simp add: super_ref_Syncptick_def image_iff)
      with "*"(2) fail_Hiding(2, 4) have ‹(t', X ∪ ev ` A) ∈ ℱ (P ⟦S⟧✓ Q)›
        by (auto simp add: F_Syncptick)
      with "*"(1) show ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)› unfolding F_Hiding by blast
    qed
  qed
qed



theorem (in Synchroptick) disjoint_finite_Hiding_Syncptick :
  ‹P ⟦S⟧✓ Q \ A = (P \ A) ⟦S⟧✓ (Q \ A)› if ‹A ∩ S = {}› and ‹finite A›
  ― ‹Monster theorem!›
proof (rule FD_antisym)
  from disjoint_Hiding_Syncptick_FD_Syncptick_Hiding[OF ‹A ∩ S = {}›]
  show ‹P ⟦S⟧✓ Q \ A ⊑FD (P \ A) ⟦S⟧✓ (Q \ A)› .
next
  let ?th_A = ‹λt. trace_hide t (ev ` A)›
  show ‹(P \ A) ⟦S⟧✓ (Q \ A) ⊑FD P ⟦S⟧✓ Q \ A›
  proof (rule failure_divergence_refine_optimizedI)
    fix t X assume ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
      and subset_div : ‹𝒟 (P ⟦S⟧✓ Q \ A) ⊆ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
    from this(1) consider ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
      | t' where ‹t = ?th_A t'› ‹(t', X ∪ ev ` A) ∈ ℱ (P ⟦S⟧✓ Q)›
      unfolding F_Hiding D_Hiding by blast
    thus ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
    proof cases
      show ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A) ⟹ (t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
        using subset_div is_processT8 by blast
    next
      fix t' assume ‹t = ?th_A t'› ‹(t', X ∪ ev ` A) ∈ ℱ (P ⟦S⟧✓ Q)›
      from this(2) consider ‹t' ∈ 𝒟 (P ⟦S⟧✓ Q)›
        | (fail) t_P X_P t_Q X_Q where ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
          ‹X ∪ ev ` A ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
        unfolding Syncptick_projs by auto
      thus ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
      proof cases
        assume ‹t' ∈ 𝒟 (P ⟦S⟧✓ Q)›
        with ‹t = ?th_A t'› have ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (metis mem_D_imp_mem_D_Hiding)
        with subset_div is_processT8 show ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))› by blast
      next
        case fail
        from ‹A ∩ S = {}› fail(4) have ‹X_P = X_P ∪ ev ` A› ‹X_Q = X_Q ∪ ev ` A›
          ― ‹i.e. term‹ev ` A ⊆ X_P› and term‹ev ` A ⊆ X_Q››
          by (auto simp add: super_ref_Syncptick_def)
        with fail(1, 2) have ‹(?th_A t_P, X_P) ∈ ℱ (P \ A)›
          ‹(?th_A t_Q, X_Q) ∈ ℱ (Q \ A)›
          by (auto simp add: F_Hiding)
        moreover from fail(3) have ‹t setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P, ?th_A t_Q), S)›
          unfolding ‹t = ?th_A t'› by (fact setinterleavesptick_trace_hide)
        ultimately show ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
          using fail(4) unfolding F_Syncptick by fast
      qed
    qed
  next
    fix t assume ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
    then obtain u v where * : ‹ftF v› ‹tF u› ‹t = ?th_A u @ v›
      ‹u ∈ 𝒟 (P ⟦S⟧✓ Q) ∨ (∃x. isInfHidden_seqRun_strong x (P ⟦S⟧✓ Q) A u)›
      by (blast elim: D_Hiding_seqRunE)
    from "*"(4) show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
    proof (elim disjE exE)
      assume ‹u ∈ 𝒟 (P ⟦S⟧✓ Q)›
      then obtain u1 u2 t_P t_Q where ** : ‹u = u1 @ u2› ‹tF u1› ‹ftF u2›
        ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
        ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
        unfolding D_Syncptick by blast
      have ‹t = ?th_A u1 @ (?th_A u2 @ v)›
        by (simp add: "*"(3) "**"(1))
      moreover from "**"(2) have ‹tF (?th_A u1)› using Hiding_tF by blast
      moreover have ‹ftF (?th_A u2 @ v)›
        by (metis D_imp_ftF ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)› calculation(1)
            ftF_append_iff ftF_charn)
      moreover from "**"(4) have ‹?th_A u1 setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P, ?th_A t_Q), S)›
        by (fact setinterleavesptick_trace_hide)
      moreover from "**"(5) have ‹?th_A t_P ∈ 𝒟 (P \ A) ∧ ?th_A t_Q ∈ 𝒯 (Q \ A) ∨
                                  ?th_A t_P ∈ 𝒯 (P \ A) ∧ ?th_A t_Q ∈ 𝒟 (Q \ A)›
        by (metis mem_D_imp_mem_D_Hiding mem_T_imp_mem_T_Hiding)
      ultimately show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
        unfolding D_Syncptick by blast
    next
      fix x assume ** : ‹isInfHidden_seqRun_strong x (P ⟦S⟧✓ Q) A u›
      from "**" have *** : ‹∃t_P t_Q. t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒯 Q ∧
        seqRun u x i setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› for i
        unfolding Syncptick_projs by blast

      define t_P_t_Q where ‹t_P_t_Q i ≡ SOME (t_P, t_Q). t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒯 Q ∧
      seqRun u x i setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› for i
      define t_P where ‹t_P ≡ fst ∘ t_P_t_Q›
      define t_Q where ‹t_Q ≡ snd ∘ t_P_t_Q›
      have **** : ‹t_P i ∈ 𝒯 P› ‹t_Q i ∈ 𝒯 Q›
        ‹seqRun u x i setinterleaves✓⇘(⊗✓)⇙ ((t_P i, t_Q i), S)› for i
        by (use "***"[of i] in ‹simp add: t_P_def t_Q_def,
                              cases ‹t_P_t_Q i›, simp add: t_P_t_Q_def,
                              metis (mono_tags, lifting) case_prod_conv someI_ex›)+
      from "*"(2) "**" have ‹set (seqRun u x i) ⊆ {ev a |a. ev a ∈ set u} ∪ ev ` A› for i
        by (simp add: seqRun_def subset_iff)
          (metis image_iff list.set_map tF_iff_is_map_ev)
      have ***** : ‹{ev a |a. ev a ∈ set (t_P i)} ∪ {ev a |a. ev a ∈ set (t_Q i)} ⊆
                      {ev a |a. ev a ∈ set u} ∪ ev ` A› for i
        by (rule subset_trans[OF setinterleavesptick_imp_superset_ev[OF "****"(3)]])
          (use ‹set (seqRun u x i) ⊆ {ev a |a. ev a ∈ set u} ∪ ev ` A› in blast)
      have ****** : ‹tF (t_P i)› ‹tF (t_Q i)› for i
        using tF_setinterleavesptick_iff[OF "****"(3)[of i]]
        by (metis "*"(2) "**" eventptick.disc(1) imageE tF_seqRun_iff)+

      { fix i
        have ‹{w. tF w ∧ {ev a |a. ev a ∈ set w} ⊆ set u ∪ ev ` A ∧ length w ≤ i} ⊆
                  map (ev ∘ of_ev) ` {w. set w ⊆ set u ∪ ev ` A ∧ length w ≤ i}›
          (is ‹?S1 ⊆ map (ev ∘ of_ev) ` ?S2›)
        proof (rule subsetI)
          fix w assume ‹w ∈ ?S1›
          hence ‹map (ev ∘ of_ev) (map (ev ∘ of_ev) w) = w›
            by (induct w) (auto simp add: subset_iff)
          moreover from ‹w ∈ ?S1› have ‹map (ev ∘ of_ev) w ∈ ?S2›
            by (induct w) (auto simp add: subset_iff)
          ultimately show ‹w ∈ map (ev ∘ of_ev) ` ?S2›
            by (metis (lifting) image_eqI)
        qed
        moreover have ‹finite {w. set w ⊆ set u ∪ ev ` A ∧ length w ≤ i}›
          by (rule finite_lists_length_le) (simp add: ‹finite A›)
        ultimately have ‹finite {w. tF w ∧ {ev a |a. ev a ∈ set w} ⊆ set u ∪ ev ` A ∧ length w ≤ i}›
          using finite_subset[OF _ finite_imageI] by blast
      } note £ = this

      have ‹inj t_P_t_Q›
      proof (rule injI)
        fix i j assume ‹t_P_t_Q i = t_P_t_Q j›
        with "****"(3) have ‹seqRun u x i setinterleaves✓⇘tj⇙ ((t_P i, t_Q i), S) ∧
        seqRun u x j setinterleaves✓⇘tj⇙ ((t_P i, t_Q i), S)›
          unfolding t_P_t_Q_def t_P_def t_Q_def by fastforce
        with setinterleavesptick_eq_length
        have ‹length (seqRun u x i) = length (seqRun u x j)› by blast
        thus ‹i = j› by simp
      qed
      hence ‹infinite (range t_P_t_Q)› using finite_imageD by blast
      moreover have ‹range t_P_t_Q ⊆ range t_P × range t_Q›
        by (simp add: t_P_def t_Q_def subset_iff image_iff) (metis fst_conv snd_conv)
      ultimately have ‹infinite (range t_P) ∨ infinite (range t_Q)› 
        by (meson finite_SigmaI infinite_super)

      thus ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
      proof (elim disjE)
        assume ‹infinite (range t_P)›
        have ‹finite {w. ∃t'∈range t_P. w = take i t'}› for i
          using "******"(1) "*****"
          by (auto intro!: finite_subset[OF _ "£"[of i]] simp add: image_iff subset_iff)
            (metis append_take_drop_id tF_append_iff, metis eventptick.inject(1) in_set_takeD)
        with ‹infinite (range t_P)› obtain t_P' :: ‹nat ⇒ _›
          where $ : ‹strict_mono t_P'› ‹range t_P' ⊆ {w. ∃t'∈range t_P. w ≤ t'}›
          using KoenigLemma by blast
        from "$"(2) "****"(1) is_processT3_TR have ‹range t_P' ⊆ 𝒯 P› by blast
        define t_P'' where ‹t_P'' i ≡ t_P' (i + length u)› for i
        from ‹range t_P' ⊆ 𝒯 P› have ‹range t_P'' ⊆ 𝒯 P› and ‹strict_mono t_P''›
          by (auto simp add: t_P''_def "$"(1) strict_monoD strict_monoI)
        have $$ : ‹?th_A (t_P'' i) = ?th_A (t_P'' 0)› for i
        proof -
          have ‹length u ≤ length (t_P'' 0)›
            by (metis "$"(1) add_0 add_leD1 t_P''_def length_strict_mono)
          obtain t' where ‹t_P'' i = t_P'' 0 @ t'›
            by (meson prefixE ‹strict_mono t_P''› strict_mono_less_eq zero_order(1))
          moreover from "$"(2) obtain j where ‹t_P'' i ≤ t_P j› by (auto simp add: t_P''_def)
          ultimately obtain t'' where ‹t_P j = t_P'' 0 @ t' @ t''› by (metis prefixE append.assoc)

          have ‹tF (t' @ t'')›
            by (metis "******"(1) ‹t_P j = t_P'' 0 @ t' @ t''› tF_append_iff)
          with setinterleavesptick_set_subsetL
            [OF "****"(3)[of j], where n = ‹length (t_P'' 0)›, unfolded ‹t_P j = t_P'' 0 @ t' @ t''›]
          have ‹e ∈ set (t' @ t'') ⟹ e ∈ {ev a |a. ev a ∈ set (drop (length (t_P'' 0)) (seqRun u x j))}› for e
            by (cases e) (auto simp add: tickFree_def)
          moreover have ‹{a. ev a ∈ set (drop (length (t_P'' 0)) (seqRun u x j))} ⊆
                       {a. ev a ∈ set (drop (length u) (seqRun u x j))}›
            by (simp add: subset_iff)
              (meson ‹length u ≤ length (t_P'' 0)› in_mono set_drop_subset_set_drop)
          moreover from "**" have ‹set (drop (length u) (seqRun u x j)) ⊆ ev ` A›
            by (auto simp add: seqRun_def)
          ultimately have ‹set (t' @ t'') ⊆ ev ` A› by blast
          thus ‹?th_A (t_P'' i) = ?th_A (t_P'' 0)›
            by (simp add: ‹t_P'' i = t_P'' 0 @ t'› subset_iff)
        qed
        from "$"(2) obtain i where ‹t_P'' 0 ≤ t_P i› by (auto simp add: t_P''_def)
        with prefixE obtain w where ‹t_P i = t_P'' 0 @ w› by blast
        have ‹ftF v› by (fact "*"(1))
        moreover have ‹tF (?th_A (seqRun u x i))›
          by (metis "*"(2) "**" Hiding_tF trace_hide_seqRun_eq_iff)
        moreover have ‹t = ?th_A (seqRun u x i) @ v›
          by (metis "*"(3) "**" trace_hide_seqRun_eq_iff)
        moreover have ‹?th_A (seqRun u x i) setinterleaves✓⇘(⊗✓)⇙ ((?th_A (t_P i), ?th_A (t_Q i)), S)›
          by (intro setinterleavesptick_trace_hide "****"(3))
        moreover have ‹?th_A (t_P i) ∈ 𝒟 (P \ A)›
        proof (unfold D_Hiding, clarify, intro exI conjI)
          show ‹ftF (?th_A w)›
            by (metis "******"(1) Hiding_ftF ‹t_P i = t_P'' 0 @ w›
                tF_append_iff tF_imp_ftF)
        next
          show ‹tF (t_P'' 0)›
            by (metis "******"(1) ‹t_P i = t_P'' 0 @ w› tF_append_iff)
        next
          show ‹?th_A (t_P i) = ?th_A (t_P'' 0) @ ?th_A w›
            by (simp add: ‹t_P i = t_P'' 0 @ w›)
        next
          show ‹t_P'' 0 ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P A ∧ t_P'' 0 ∈ range f)›
            using "$$" ‹range t_P'' ⊆ 𝒯 P› ‹strict_mono t_P''› by blast
        qed
        moreover have ‹?th_A (t_Q i) ∈ 𝒯 (Q \ A)›
        proof (cases ‹∃t'. ?th_A t' = ?th_A (t_Q i) ∧ (t', ev ` A) ∈ ℱ Q›)
          assume ‹∃t'. ?th_A t' = ?th_A (t_Q i) ∧ (t', ev ` A) ∈ ℱ Q›
          then obtain t' where ‹?th_A (t_Q i) = ?th_A t'› ‹(t', ev ` A) ∈ ℱ Q› by metis
          thus ‹?th_A (t_Q i) ∈ 𝒯 (Q \ A)› unfolding T_Hiding by blast
        next
          assume ‹∄t'. ?th_A t' = ?th_A (t_Q i) ∧ (t', ev ` A) ∈ ℱ Q›
          with inf_hidden[OF _ "****"(2)] obtain t_Q' j
            where ‹isInfHiddenRun t_Q' Q A› ‹t_Q i = t_Q' j› by blast
          thus ‹?th_A (t_Q i) ∈ 𝒯 (Q \ A)›
            unfolding T_Hiding using "******"(2) ftF_Nil by blast
        qed
        ultimately show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))› unfolding D_Syncptick by blast
      next
        assume ‹infinite (range t_Q)›
        have ‹finite {w. ∃t'∈range t_Q. w = take i t'}› for i
          using "******"(2) "*****"
          by (auto intro!: finite_subset[OF _ "£"[of i]] simp add: image_iff subset_iff)
            (metis append_take_drop_id tF_append_iff, metis eventptick.inject(1) in_set_takeD)
        with ‹infinite (range t_Q)› obtain t_Q' :: ‹nat ⇒ _›
          where $ : ‹strict_mono t_Q'› ‹range t_Q' ⊆ {w. ∃t'∈range t_Q. w ≤ t'}›
          using KoenigLemma by blast
        from "$"(2) "****"(2) is_processT3_TR have ‹range t_Q' ⊆ 𝒯 Q› by blast
        define t_Q'' where ‹t_Q'' i ≡ t_Q' (i + length u)› for i
        from ‹range t_Q' ⊆ 𝒯 Q› have ‹range t_Q'' ⊆ 𝒯 Q› and ‹strict_mono t_Q''›
          by (auto simp add: t_Q''_def "$"(1) strict_monoD strict_monoI)
        have $$ : ‹?th_A (t_Q'' i) = ?th_A (t_Q'' 0)› for i
        proof -
          have ‹length u ≤ length (t_Q'' 0)›
            by (metis "$"(1) add_0 add_leD1 t_Q''_def length_strict_mono)
          obtain t' where ‹t_Q'' i = t_Q'' 0 @ t'›
            by (meson prefixE ‹strict_mono t_Q''› strict_mono_less_eq zero_order(1))
          moreover from "$"(2) obtain j where ‹t_Q'' i ≤ t_Q j› by (auto simp add: t_Q''_def)
          ultimately obtain t'' where ‹t_Q j = t_Q'' 0 @ t' @ t''› by (metis prefixE append.assoc)
          have ‹tF (t' @ t'')›
            by (metis "******"(2) ‹t_Q j = t_Q'' 0 @ t' @ t''› tF_append_iff)
          with setinterleavesptick_set_subsetR
            [OF "****"(3)[of j], where n = ‹length (t_Q'' 0)›, unfolded ‹t_Q j = t_Q'' 0 @ t' @ t''›]
          have ‹e ∈ set (t' @ t'') ⟹ e ∈ {ev a |a. ev a ∈ set (drop (length (t_Q'' 0)) (seqRun u x j))}› for e
            by (cases e) (auto simp add: tickFree_def)
          moreover have ‹{a. ev a ∈ set (drop (length (t_Q'' 0)) (seqRun u x j))} ⊆
                         {a. ev a ∈ set (drop (length u) (seqRun u x j))}›
            by (simp add: subset_iff)
              (meson ‹length u ≤ length (t_Q'' 0)› in_mono set_drop_subset_set_drop)
          moreover from "**" have ‹set (drop (length u) (seqRun u x j)) ⊆ ev ` A›
            by (auto simp add: seqRun_def)
          ultimately have ‹set (t' @ t'') ⊆ ev ` A› by blast
          thus ‹?th_A (t_Q'' i) = ?th_A (t_Q'' 0)›
            by (simp add: ‹t_Q'' i = t_Q'' 0 @ t'› subset_iff)
        qed
        from "$"(2) obtain i where ‹t_Q'' 0 ≤ t_Q i› by (auto simp add: t_Q''_def)
        with prefixE obtain w where ‹t_Q i = t_Q'' 0 @ w› by blast
        have ‹ftF v› by (fact "*"(1))
        moreover have ‹tF (?th_A (seqRun u x i))›
          by (metis "*"(2) "**" Hiding_tF trace_hide_seqRun_eq_iff)
        moreover have ‹t = ?th_A (seqRun u x i) @ v›
          by (metis "*"(3) "**" trace_hide_seqRun_eq_iff)
        moreover have ‹?th_A (seqRun u x i) setinterleaves✓⇘(⊗✓)⇙ ((?th_A (t_P i), ?th_A (t_Q i)), S)›
          by (intro setinterleavesptick_trace_hide "****"(3))
        moreover have ‹?th_A (t_Q i) ∈ 𝒟 (Q \ A)›
        proof (unfold D_Hiding, clarify, intro exI conjI)
          show ‹ftF (?th_A w)›
            by (metis "******"(2) Hiding_ftF ‹t_Q i = t_Q'' 0 @ w›
                tF_append_iff tF_imp_ftF)
        next
          show ‹tF (t_Q'' 0)›
            by (metis "******"(2) ‹t_Q i = t_Q'' 0 @ w› tF_append_iff)
        next
          show ‹?th_A (t_Q i) = ?th_A (t_Q'' 0) @ ?th_A w›
            by (simp add: ‹t_Q i = t_Q'' 0 @ w›)
        next
          show ‹t_Q'' 0 ∈ 𝒟 Q ∨ (∃f. isInfHiddenRun f Q A ∧ t_Q'' 0 ∈ range f)›
            using "$$" ‹range t_Q'' ⊆ 𝒯 Q› ‹strict_mono t_Q''› by blast
        qed
        moreover have ‹?th_A (t_P i) ∈ 𝒯 (P \ A)›
        proof (cases ‹∃t'. ?th_A t' = ?th_A (t_P i) ∧ (t', ev ` A) ∈ ℱ P›)
          assume ‹∃t'. ?th_A t' = ?th_A (t_P i) ∧ (t', ev ` A) ∈ ℱ P›
          then obtain t' where ‹?th_A (t_P i) = ?th_A t'› ‹(t', ev ` A) ∈ ℱ P› by metis
          thus ‹?th_A (t_P i) ∈ 𝒯 (P \ A)› unfolding T_Hiding by blast
        next
          assume ‹∄t'. ?th_A t' = ?th_A (t_P i) ∧ (t', ev ` A) ∈ ℱ P›
          with inf_hidden[OF _ "****"(1)] obtain t_P' j
            where ‹isInfHiddenRun t_P' P A› ‹t_P i = t_P' j› by blast
          thus ‹?th_A (t_P i) ∈ 𝒯 (P \ A)›
            unfolding T_Hiding using "******"(1) ftF_Nil by blast
        qed
        ultimately show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))› unfolding D_Syncptick by blast
      qed
    qed
  qed
qed



lemma disjoint_Hiding_MultiSyncptick_FD_MultiSyncptick_Hiding :
  ‹⟦S⟧✓ l ∈@ L. P l \ A ⊑FD ⟦S⟧✓ l ∈@ L. (P l \ A)› if ‹A ∩ S = {}›
proof (induct L rule: induct_list012)
  case 1 show ?case by simp
next
  case (2 l0)
  show ?case by (simp add: RenamingTick_Hiding)
next
  case (3 l0 l1 L)
  have ‹⟦S⟧✓ l ∈@ (l0 # l1 # L). P l \ A =
        P l0 ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l1 # L). P l \ A› by simp
  also have ‹… ⊑FD (P l0 \ A) ⟦S⟧✓Rlist (⟦S⟧✓ l ∈@ (l1 # L). P l \ A)›
    by (simp add: SyncRlist.disjoint_Hiding_Syncptick_FD_Syncptick_Hiding ‹A ∩ S = {}›)
  also have ‹… ⊑FD (P l0 \ A) ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l1 # L). (P l \ A)›
    by (simp add: "3.hyps"(2) SyncRlist.mono_Syncptick_FD)
  also have ‹… = ⟦S⟧✓ l ∈@ (l0 # l1 # L). (P l \ A)› by simp
  finally show ?case .
qed


lemma disjoint_finite_Hiding_MultiSyncptick :
  ‹⟦S⟧✓ l ∈@ L. P l \ A = ⟦S⟧✓ l ∈@ L. (P l \ A)› if ‹A ∩ S = {}› and ‹finite A›
proof (induct L rule: induct_list012)
  case 1 show ?case by simp
next
  case (2 l0)
  show ?case by (simp add: RenamingTick_Hiding)
next
  case (3 l0 l1 L)
  have ‹⟦S⟧✓ l ∈@ (l0 # l1 # L). P l \ A =
        P l0 ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l1 # L). P l \ A› by simp
  also have ‹… = (P l0 \ A) ⟦S⟧✓Rlist (⟦S⟧✓ l ∈@ (l1 # L). P l \ A)›
    by (simp add: SyncRlist.disjoint_finite_Hiding_Syncptick ‹A ∩ S = {}› ‹finite A›)
  also have ‹… = (P l0 \ A) ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l1 # L). (P l \ A)›
    by (simp add: "3.hyps"(2) SyncRlist.mono_Syncptick_FD)
  also have ‹… = ⟦S⟧✓ l ∈@ (l0 # l1 # L). (P l \ A)› by simp
  finally show ?case .
qed



section ‹Other Laws of Synchronization Product›

subsection ‹Some Refinements›

context Synchroptick begin

lemma Mndetprefix_Syncptick_Det_distr_FD :
  ‹(⊓ a ∈ A → (P a ⟦ C ⟧✓ (⊓ b ∈ B → Q b))) □
   (⊓ b ∈ B → ((⊓ a ∈ A → P a) ⟦ C ⟧✓ Q b))
   ⊑FD (⊓ a ∈ A → P a) ⟦ C ⟧✓ (⊓ b ∈ B → Q b)›
  (is ‹?lhs1 □ ?lhs2 ⊑FD ?rhs›)
  if ‹A ≠ {}› ‹B ≠ {}› ‹A ∩ C = {}› ‹B ∩ C = {}›
proof -
  have ‹?lhs1 = ⊓ b∈B. ⊓ a∈A. (a → (P a ⟦C⟧✓ (b → Q b)))› (is ‹_ = ?lhs1'›)
    by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
        Syncptick_distrib_GlobalNdet_left Syncptick_distrib_GlobalNdet_right
        write0_def GlobalNdet_Mprefix_distr[OF ‹B ≠ {}›, symmetric])
      (subst GlobalNdet_sets_commute, simp)
  moreover have ‹?lhs2 = ⊓ b∈B. ⊓ a∈A. (b → (a → P a ⟦C⟧✓ Q b))› (is ‹_ = ?lhs2'›)
    by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
        Syncptick_distrib_GlobalNdet_left Syncptick_distrib_GlobalNdet_right
        write0_def GlobalNdet_Mprefix_distr[OF ‹A ≠ {}›, symmetric])
  ultimately have ‹?lhs1 □ ?lhs2 = ?lhs1' □ ?lhs2'› by simp
  moreover have ‹?lhs1' □ ?lhs2' ⊑FD ⊓ b∈B. ⊓ a∈A.   (a → (P a ⟦C⟧✓ (b → Q b)))
                                                    □ (b → ((a → P a) ⟦C⟧✓ Q b))›
    by (auto simp add: ‹A ≠ {}› ‹B ≠ {}› refine_defs GlobalNdet_projs Det_projs write0_def)
  moreover have ‹… = ⊓ b∈B. ⊓ a∈A. ((a → P a) ⟦C⟧✓ (b → Q b))›
    by (rule mono_GlobalNdet_eq, rule mono_GlobalNdet_eq,
        simp add: write0_def, subst Mprefix_Syncptick_Mprefix_indep)
      (use ‹A ∩ C = {}› ‹B ∩ C = {}› in auto)
  moreover have ‹… = ?rhs›
    by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
        Syncptick_distrib_GlobalNdet_left Syncptick_distrib_GlobalNdet_right)
  ultimately show ‹?lhs1 □ ?lhs2 ⊑FD ?rhs› by argo
qed


lemmas Mndetprefix_Syncptick_Det_distr_F =
  Mndetprefix_Syncptick_Det_distr_FD[THEN leFD_imp_leF]

lemmas Mndetprefix_Syncptick_Det_distr_D =
  Mndetprefix_Syncptick_Det_distr_FD[THEN leFD_imp_leD]

lemmas Mndetprefix_Syncptick_Det_distr_T =
  Mndetprefix_Syncptick_Det_distr_F[THEN leF_imp_leT]

lemma Mndetprefix_Syncptick_Det_distr_DT :
  ‹⟦A ≠ {}; B ≠ {}; A ∩ C = {}; B ∩ C = {}⟧ ⟹
   (⊓ a ∈ A → (P a ⟦ C ⟧✓ (⊓ b ∈ B → Q b))) □
   (⊓ b ∈ B → ((⊓ a ∈ A → P a) ⟦ C ⟧✓ Q b))
   ⊑DT (⊓ a ∈ A → P a) ⟦ C ⟧✓ (⊓ b ∈ B → Q b)›
  by (simp add: Mndetprefix_Syncptick_Det_distr_D
      Mndetprefix_Syncptick_Det_distr_T leD_leT_imp_leDT)


end



subsection ‹Sequential Composition with STOP›

text ‹New in Isabelle26.›

lemma (in Synchroptick) Seq_STOP_Parptick_Seq_STOP :
  ‹P ; STOP ||✓ (Q ; STOP) = P ||✓ Q ; STOP› (is ‹?lhs = ?rhs›)
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (simp add: Syncptick_projs Seq_projs STOP_projs)
      (metis D_T is_processT3_TR_append)
next
  show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    by (simp add: Syncptick_projs Seq_projs STOP_projs)
      (metis tF_setinterleavesptick_iff)
next
  fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
  then obtain t_P t_Q X_P X_Q where * : ‹(t_P, X_P) ∈ ℱ (P ; STOP)› ‹t_P ∉ 𝒟 (P ; STOP)›
    ‹(t_Q, X_Q) ∈ ℱ (Q ; STOP)› ‹t_Q ∉ 𝒟 (Q ; STOP)›
    ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), UNIV)› ‹X ⊆ super_ref_Syncptick (⊗✓) X_P UNIV X_Q›
    by (simp add: F_Syncptick D_Syncptick')
      (metis (no_types) F_T append.right_neutral ftF_Nil)
  from "*"(1-4) have ‹tF t_P ∧ ((t_P, X_P ∪ range tick) ∈ ℱ P ∨ (∃r. t_P @ [✓(r)] ∈ 𝒯 P))›
    ‹tF t_Q ∧ ((t_Q, X_Q ∪ range tick) ∈ ℱ Q ∨ (∃s. t_Q @ [✓(s)] ∈ 𝒯 Q))›
    by (auto simp add: Syncptick_projs Seq_projs STOP_projs append_T_imp_tF)
  thus ‹(t, X) ∈ ℱ ?rhs›
  proof (elim disjE conjE exE)
    assume ** : ‹tF t_P› ‹(t_P, X_P ∪ range tick) ∈ ℱ P› ‹tF t_Q› ‹(t_Q, X_Q ∪ range tick) ∈ ℱ Q›
    from "*"(6) have ‹X ∪ range tick ⊆ super_ref_Syncptick (⊗✓) (X_P ∪ range tick) UNIV (X_Q ∪ range tick)›
      by (auto simp add: super_ref_Syncptick_def)
    with "*"(5) "**"(2, 4) have ‹(t, X ∪ range tick) ∈ ℱ (P ||✓ Q)›
      by (auto simp add: Syncptick_projs)
    thus ‹(t, X) ∈ ℱ ?rhs›
      by (simp add: F_Seq F_STOP)
        (use "*"(5) "**"(1, 3) tF_setinterleavesptick_iff in blast)
  next
    fix s assume ** : ‹tF t_P› ‹(t_P, X_P ∪ range tick) ∈ ℱ P› ‹tF t_Q› ‹t_Q @ [✓(s)] ∈ 𝒯 Q›
    have ‹(t_Q, UNIV - {✓(s)}) ∈ ℱ Q› by (simp add: "**"(4) is_processT6_TR)
    moreover from "*"(6) have ‹X ∪ range tick ⊆ super_ref_Syncptick (⊗✓) (X_P ∪ range tick) UNIV (UNIV - {✓(s)})›
      by (auto simp add: super_ref_Syncptick_def)
    ultimately have ‹(t, X ∪ range tick) ∈ ℱ (P ||✓ Q)›
      using "*"(5) "**"(2) by (auto simp add: Syncptick_projs)
    thus ‹(t, X) ∈ ℱ ?rhs›
      by (simp add: F_Seq F_STOP)
        (use "*"(5) "**"(1, 3) tF_setinterleavesptick_iff in blast)
  next
    fix r assume ** : ‹tF t_P› ‹t_P @ [✓(r)] ∈ 𝒯 P› ‹tF t_Q› ‹(t_Q, X_Q ∪ range tick) ∈ ℱ Q›
    have ‹(t_P, UNIV - {✓(r)}) ∈ ℱ P› by (simp add: "**"(2) is_processT6_TR)
    moreover from "*"(6) have ‹X ∪ range tick ⊆ super_ref_Syncptick (⊗✓) (UNIV - {✓(r)}) UNIV (X_Q ∪ range tick)›
      by (auto simp add: super_ref_Syncptick_def)
    ultimately have ‹(t, X ∪ range tick) ∈ ℱ (P ||✓ Q)›
      using "*"(5) "**"(4) by (auto simp add: Syncptick_projs)
    thus ‹(t, X) ∈ ℱ ?rhs›
      by (simp add: F_Seq F_STOP)
        (use "*"(5) "**"(1, 3) tF_setinterleavesptick_iff in blast)
  next
    fix r s assume ** : ‹tF t_P› ‹t_P @ [✓(r)] ∈ 𝒯 P› ‹tF t_Q› ‹t_Q @ [✓(s)] ∈ 𝒯 Q›
    show ‹(t, X) ∈ ℱ ?rhs›
    proof (cases ‹∃r_s. r ⊗✓ s = ⌊r_s⌋›)
      assume ‹∃r_s. r ⊗✓ s = ⌊r_s⌋›
      then obtain r_s where ‹r ⊗✓ s = ⌊r_s⌋› ..
      with "*"(5) have ‹t @ [✓(r_s)] setinterleaves✓⇘(⊗✓)⇙ ((t_P @ [✓(r)], t_Q @ [✓(s)]), UNIV)›
        by (simp add: setinterleavesptick_snoc_tick)
      with "**"(2, 4) have ‹t @ [✓(r_s)] ∈ 𝒯 (P ||✓ Q)›
        by (auto simp add: T_Syncptick)
      thus ‹(t, X) ∈ ℱ ?rhs› by (auto simp add: F_Seq F_STOP)
    next
      assume ‹∄r_s. r ⊗✓ s = ⌊r_s⌋›
      with "*"(6) have ‹X ∪ range tick ⊆ super_ref_Syncptick (⊗✓) (UNIV - {✓(r)}) UNIV (UNIV - {✓(s)})›
        by (auto simp add: super_ref_Syncptick_def)
      moreover from "**"(2, 4) have ‹(t_P, UNIV - {✓(r)}) ∈ ℱ P› ‹(t_Q, UNIV - {✓(s)}) ∈ ℱ Q›
        by (simp_all add: is_processT6_TR)
      ultimately have ‹(t, X ∪ range tick) ∈ ℱ (P ||✓ Q)›
        using "*"(5) by (auto simp add: F_Syncptick)
      thus ‹(t, X) ∈ ℱ ?rhs›
        by (simp add: F_Seq F_STOP)
          (use "*"(5) "**"(1, 3) tF_setinterleavesptick_iff in blast)
    qed
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
  then consider (F) ‹tF t› ‹(t, X ∪ range tick) ∈ ℱ (P ||✓ Q)› ‹t ∉ 𝒟 (P ||✓ Q)›
    | (T) r_s where ‹tF t› ‹t @ [✓(r_s)] ∈ 𝒯 (P ||✓ Q)› ‹t @ [✓(r_s)] ∉ 𝒟 (P ||✓ Q)›
    by (simp add: Seq_projs STOP_projs) (metis append_T_imp_tF is_processT9 not_Cons_self2)
  thus ‹(t, X) ∈ ℱ ?lhs›
  proof cases
    case F
    from F(2, 3) obtain t_P t_Q X_P X_Q
      where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), UNIV)›
        ‹X ∪ range tick ⊆ super_ref_Syncptick (⊗✓) X_P UNIV X_Q›
      unfolding Syncptick_projs by force
    from "*"(1, 2)[THEN is_processT5_S7'[where A = ‹range tick›]] obtain r s where
      ‹(t_P, X_P ∪ range tick) ∈ ℱ P ∧ (t_Q, X_Q ∪ range tick) ∈ ℱ Q ∨ 
       (t_P, X_P ∪ range tick) ∈ ℱ P ∧ t_Q @ [✓(s)] ∈ 𝒯 Q ∨
       t_P @ [✓(r)] ∈ 𝒯 P ∧ (t_Q, X_Q ∪ range tick) ∈ ℱ Q ∨
       t_P @ [✓(r)] ∈ 𝒯 P ∧ t_Q @ [✓(s)] ∈ 𝒯 Q› by auto
    moreover from "*"(3) F(1) tF_setinterleavesptick_iff have ‹tF t_P› ‹tF t_Q› by blast+
    ultimately show ‹(t, X) ∈ ℱ ?lhs›
      using "*"(3, 4) by (simp add: Syncptick_projs Seq_projs STOP_projs) blast
  next
    case T
    from T(2, 3) obtain t_P t_Q where ** : ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
      ‹t @ [✓(r_s)] setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), UNIV)›
      unfolding Syncptick_projs by blast
    from "**"(3) obtain t_P' t_Q' r s
      where *** : ‹r ⊗✓ s = ⌊r_s⌋› ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
        ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), UNIV)›
      by (auto elim: snoc_tick_setinterleavesptickE)
    from "**"(1) "***"(2) have ‹(t_P', UNIV) ∈ ℱ (P ; STOP)›
      by (auto simp add: F_Seq F_STOP)
    moreover from "**"(2) "***"(3) have ‹(t_Q', UNIV) ∈ ℱ (Q ; STOP)›
      by (auto simp add: F_Seq F_STOP)
    moreover have ‹X ⊆ super_ref_Syncptick (⊗✓) UNIV UNIV UNIV›
      by (simp add: super_ref_Syncptick_def subset_iff) (metis eventptick.exhaust)
    ultimately show ‹(t, X) ∈ ℱ ?lhs›
      using "***"(4) by (auto simp add: Syncptick_projs)
  qed
qed




subsection ‹The Particular Case of Runit›

text ‹New in Isabelle26.
The study of this particular interpretation is motivated by the fact that
it is involved in the definition of the alphabetized synchronization product.›

subsubsection ‹First Properties›

text ‹
Note that when both processes term‹P› and term‹Q› are of type typ‹'a process›,
we have term‹P ⟦A⟧✓Runit Q = P ⟦A⟧✓Lunit Q›.
We further have the equality with term‹P ⟦A⟧✓Classic Q› (and consequently with term‹P ⟦A⟧ Q›).›

lemma SyncRunit_is_SyncLunit_unit : ‹P ⟦A⟧✓Runit Q = P ⟦A⟧✓Lunit Q›
  by (metis (full_types) SyncRunit.inj_tj SyncRunit_tj_def SyncRunit_tj_dual_def ext)

lemma SyncClassic_is_SyncRunit_unit : ‹P ⟦A⟧✓Classic Q = P ⟦A⟧✓Runit Q›
  by (metis (full_types, lifting) ext SyncClassic_tj_def SyncRunit.inj_tj SyncRunit_tj_def)

lemma SyncClassic_is_SyncLunit_unit : ‹P ⟦A⟧✓Classic Q = P ⟦A⟧✓Lunit Q›
  by (metis SyncClassic_is_SyncRunit_unit SyncRunit_is_SyncLunit_unit)

lemma SKIPS_SyncRunit_SKIP : ‹SKIPS R ⟦A⟧✓Runit SKIP s = SKIPS R›
  by (simp add: SKIPS_def SyncRunit.Syncptick_distrib_GlobalNdet_right)

lemma SKIP_SyncLunit_SKIPS : ‹SKIP r ⟦A⟧✓Lunit SKIPS S = SKIPS S›
  by (simp add: SKIPS_def SyncRunit.Synchroptick_comm_dual.Syncptick_distrib_GlobalNdet_left)



subsubsection ‹Projections›

lemma D_SyncRunit_Skip :
  ‹𝒟 (P ⟦A⟧✓Runit Skip) = {t @ u |t u. tF t ∧ ftF u ∧ t ∈ 𝒟 P ∧ set t ∩ ev ` A = {}}›
  (is ‹?lhs = ?rhs›)
proof (intro set_eqI iffI)
  fix t assume ‹t ∈ ?lhs›
  then obtain u v t_P t_Skip where * : ‹t = u @ v› ‹tF u› ‹ftF v›
    ‹u setinterleaves✓⇘SyncRunit_tj⇙ ((t_P, t_Skip), A)› ‹t_P ∈ 𝒟 P› ‹t_Skip ∈ 𝒯 Skip›
    by (auto simp add: SyncRunit.Syncptick_projs D_SKIP)
  from "*"(2, 4, 6) have ‹u = t_P ∧ set u ∩ ev ` A = {}›
    by (fastforce simp add: T_SKIP setinterleavesptick_NilR_iff
        tF_map_ev_of_ev_same_type_is tF_setinterleavesptick_iff)
  with "*"(1-3, 5) show ‹t ∈ ?rhs› by fast
next
  fix t assume ‹t ∈ ?rhs›
  then obtain u v
    where * : ‹t = u @ v› ‹tF u› ‹ftF v› ‹u ∈ 𝒟 P› ‹set u ∩ ev ` A = {}› by blast
  from "*"(2, 5) have ‹u setinterleaves✓⇘SyncRunit_tj⇙ ((u, []), A)›
    by (simp add: setinterleavesptick_NilR_iff tF_map_ev_of_ev_same_type_is)
  with "*"(1-4) show ‹t ∈ ?lhs›
    by (simp add: SyncRunit.Syncptick_projs D_SKIP) (blast intro: Nil_elem_T)
qed

corollary D_Skip_SyncLunit :
  ‹𝒟 (Skip ⟦A⟧✓Lunit Q) = {t @ u |t u. tF t ∧ ftF u ∧ t ∈ 𝒟 Q ∧ set t ∩ ev ` A = {}}›
  by (simp flip: SyncRunit.Syncptick_commute add: D_SyncRunit_Skip)



corollary Dmin_SyncRunit_Skip :
  ‹𝒟min (P ⟦A⟧✓Runit Skip) = {t ∈ 𝒟min P. set t ∩ ev ` A = {}}› (is ‹𝒟min ?P = ?rhs›)
proof (intro set_eqI iffI)
  fix t assume ‹t ∈ 𝒟min ?P›
  then obtain u v where * : ‹t = u @ v› ‹tF u› ‹ftF v› ‹u ∈ 𝒟 P› ‹set u ∩ ev ` A = {}›
    by (auto simp add: D_SyncRunit_Skip dest!: Dmin_D)
  from "*"(2, 4, 5) have ‹u ∈ 𝒟 ?P›
    by (auto simp add: D_SyncRunit_Skip intro: ftF_Nil)
  with ‹t ∈ 𝒟min ?P› have ‹v = []›
    by (simp add: "*"(1) Divergencesmin_def)
      (metis Prefix_Order.prefixI min_elems_no_list_set_list_set self_append_conv)
  moreover have ‹u ∈ 𝒟min P›
  proof (rule ccontr)
    assume ‹u ∉ 𝒟min P›
    with "*"(4) obtain u' where ‹u' < u› ‹u' ∈ 𝒟 P›
      by (metis Dmin_D Divergencesmin_def antisym_conv2 ex_le_mem_min_elems_list_set)
    with "*"(1, 2, 5) have ‹u' ∈ 𝒟 ?P›
      by (auto simp add: less_list_def less_eq_list_def prefix_def D_SyncRunit_Skip)
        (blast intro: ftF_Nil)
    with ‹u' < u› ‹t ∈ 𝒟min ?P› show False
      by (simp add: "*"(1) ‹v = []› Divergencesmin_def min_elems_def)
  qed
  ultimately show ‹t ∈ ?rhs› by (simp add: "*"(1, 5))
next
  fix t assume ‹t ∈ ?rhs›
  hence * : ‹t ∈ 𝒟min P› ‹set t ∩ ev ` A = {}› by simp_all
  show ‹t ∈ 𝒟min ?P›
  proof (rule ccontr)
    assume ‹¬ t ∈ 𝒟min ?P›
    moreover from "*" have ‹t ∈ 𝒟 ?P›
      by (auto simp add: D_SyncRunit_Skip intro: Dmin_D ftF_Nil tF_mem_Dmin)
    ultimately obtain t' where ‹t' < t› ‹t' ∈ 𝒟 ?P›
      by (metis Dmin_D antisym_conv2 mem_D_imp_ex_le_mem_Dmin)
    then obtain u v where ‹t' = u @ v› ‹u ∈ 𝒟 P› by (auto simp add: D_SyncRunit_Skip)
    from ‹t' = u @ v› ‹t' < t› have ‹u < t›
      by (meson Prefix_Order.prefixI order_le_less_trans)
    with ‹u ∈ 𝒟 P› ‹t ∈ 𝒟min P› show False
      by (simp add: Divergencesmin_def min_elems_def)
  qed
qed

corollary Dmin_Skip_SyncLunit :
  ‹𝒟min (Skip ⟦A⟧✓Lunit Q) = {t ∈ 𝒟min Q. set t ∩ ev ` A = {}}›
  by (metis Dmin_SyncRunit_Skip Renaming_id SyncRunit.Syncptick_commute)



lemma T_SyncRunit_Skip :
  ‹𝒯 (P ⟦A⟧✓Runit Skip) = {t @ u |t u. tF t ∧ ftF u ∧ t ∈ 𝒟 P ∧ set t ∩ ev ` A = {}} ∪
                         {t ∈ 𝒯 P. set t ∩ ev ` A = {}}›
  (is ‹_ = ?div ∪ ?tr›)
proof (intro set_eqI iffI)
  fix t assume ‹t ∈ 𝒯 (P ⟦A⟧✓Runit Skip)›
  then consider ‹t ∈ 𝒟 (P ⟦A⟧✓Runit Skip)›
    | (tr) t_P t_Skip where ‹t_P ∈ 𝒯 P› ‹t_Skip ∈ 𝒯 Skip›
      ‹t setinterleaves✓⇘SyncRunit_tj⇙ ((t_P, t_Skip), A)›
    by (auto simp add: SyncRunit.Syncptick_projs)
  thus ‹t ∈ ?div ∪ ?tr›
  proof cases
    assume ‹t ∈ 𝒟 (P ⟦A⟧✓Runit Skip)›
    hence ‹t ∈ ?div› by (simp add: D_SyncRunit_Skip)
    thus ‹t ∈ ?div ∪ ?tr› ..
  next
    case tr
    from tr(2, 3) have ‹t = t_P› ‹set t ∩ ev ` A = {}›
      by (auto simp add: T_SKIP setinterleavesptick_NilR_iff tF_map_ev_of_ev_same_type_is
          SyncRunit_tj_def ftF_setinterleavesptick_snoc_tickR_iff
          [OF ‹t ∈ 𝒯 (P ⟦A⟧✓Runit Skip)›[THEN T_imp_ftF], where v = ‹[]›, simplified])+
    with tr(1) have ‹t ∈ ?tr› by simp
    thus ‹t ∈ ?div ∪ ?tr› ..
  qed
next
  show ‹t ∈ ?div ∪ ?tr ⟹ t ∈ 𝒯 (P ⟦A⟧✓Runit Skip)› for t 
  proof (elim UnE)
    fix t assume ‹t ∈ ?div›
    hence ‹t ∈ 𝒟 (P ⟦A⟧✓Runit Skip)› by (simp add: D_SyncRunit_Skip)
    thus ‹t ∈ 𝒯 (P ⟦A⟧✓Runit Skip)› by (fact D_T)
  next
    fix t assume ‹t ∈ ?tr›
    hence * : ‹t ∈ 𝒯 P› ‹set t ∩ ev ` A = {}› by simp_all
    define t_Skip :: ‹'a trace› where ‹t_Skip ≡ (if tF t then [] else [✓])›
    from "*" ‹t ∈ 𝒯 P›[THEN T_imp_ftF]
    have ‹t setinterleaves✓⇘SyncRunit_tj⇙ ((t, t_Skip), A)›
      by (simp add: t_Skip_def setinterleavesptick_NilR_iff SyncRunit_tj_def
          ftF_setinterleavesptick_snoc_tickR_iff[where v = ‹[]›, simplified])
        (metis (no_types) Int_assoc ftF_E inf_bot_right inf_sup_absorb
          set_append tF_map_ev_of_ev_same_type_is)
    moreover have ‹t_Skip ∈ 𝒯 Skip› by (simp add: T_SKIP t_Skip_def)
    ultimately show ‹t ∈ 𝒯 (P ⟦A⟧✓Runit Skip)›
      using "*"(1) by (auto simp add: SyncRunit.Syncptick_projs)
  qed
qed


corollary T_Skip_SyncLunit :
  ‹𝒯 (Skip ⟦A⟧✓Lunit Q) = {t @ u |t u. tF t ∧ ftF u ∧ t ∈ 𝒟 Q ∧ set t ∩ ev ` A = {}} ∪
                         {t ∈ 𝒯 Q. set t ∩ ev ` A = {}}›
  by (simp flip: SyncRunit.Syncptick_commute add: T_SyncRunit_Skip)




lemma F_SyncRunit_Skip :
  ‹ℱ (P ⟦A⟧✓Runit Skip) =
   {(t, X). ∃X_P. (t, X_P) ∈ ℱ P ∧ set t ∩ ev ` A = {} ∧ X ⊆ X_P ∪ ev ` A} ∪
   {(t @ u, X) |t u X. tF t ∧ ftF u ∧ t ∈ 𝒟 P ∧ set t ∩ ev ` A = {}}›
  (is ‹ℱ ?lhs = ?rhs1 ∪ ?rhs2›)
proof (rule subset_antisym)
  { fix t X assume ‹(t, X) ∈ ℱ ?lhs›
    then consider ‹t ∈ 𝒟 ?lhs›
      | (fail) t_P X_P t_Skip X_Skip where ‹t ∉ 𝒟 ?lhs›
        ‹(t_P, X_P) ∈ ℱ P› ‹(t_Skip, X_Skip) ∈ ℱ Skip›
        ‹t setinterleaves✓⇘SyncRunit_tj⇙ ((t_P, t_Skip), A)›
        ‹X ⊆ super_ref_Syncptick SyncRunit_tj X_P A X_Skip›
      unfolding SyncRunit.Syncptick_projs by blast
    hence ‹(t, X) ∈ ?rhs1 ∪ ?rhs2›
    proof cases
      assume ‹t ∈ 𝒟 ?lhs›
      hence ‹(t, X) ∈ ?rhs2› by (simp add: D_SyncRunit_Skip)
      thus ‹(t, X) ∈ ?rhs1 ∪ ?rhs2› ..
    next
      case fail
      from ‹(t, X) ∈ ℱ ?lhs›[THEN F_imp_ftF]
      show ‹(t, X) ∈ ?rhs1 ∪ ?rhs2›
      proof (elim ftF_E)
        fix t' r assume ‹t = t' @ [✓(r)]›
        with ‹(t, X) ∈ ℱ ?lhs›[THEN F_T] ‹t ∉ 𝒟 ?lhs›
        have ‹t ∈ 𝒯 P› ‹set t ∩ ev ` A = {}›
          by (auto simp add: T_SyncRunit_Skip D_SyncRunit_Skip)
        with ‹t = t' @ [✓(r)]› have ‹(t, X) ∈ ?rhs1›
          by simp (meson Un_iff subsetI tick_T_F)
        thus ‹(t, X) ∈ ?rhs1 ∪ ?rhs2› ..
      next
        assume ‹tF t›
        with fail(3, 4) have * : ‹t = t_P ∧ t_Skip = [] ∧ set t ∩ ev ` A = {}›
          by (auto simp add: ftF_setinterleavesptick_snoc_tickR_iff[where v = ‹[]›, simplified]
              setinterleavesptick_NilR_iff F_SKIP tF_map_ev_of_ev_same_type_is) blast+
        with fail(3, 5) have ‹X ⊆ X_P ∪ ev ` A›
          by (auto simp add: F_SKIP super_ref_Syncptick_def subset_iff SyncRunit_tj_def)
        with "*" fail(2) have ‹(t, X) ∈ ?rhs1› by blast
        thus ‹(t, X) ∈ ?rhs1 ∪ ?rhs2› ..
      qed
    qed
  } 
  thus ‹ℱ ?lhs ⊆ ?rhs1 ∪ ?rhs2› by safe blast
next
  have ‹?rhs1 ⊆ ℱ ?lhs›
  proof safe
    fix t X X_P assume ‹(t, X_P) ∈ ℱ P› ‹set t ∩ ev ` A = {}› ‹X ⊆ X_P ∪ ev ` A›
    from F_imp_ftF this(1) have ‹ftF t› .
    define t_Skip :: ‹'a trace› where ‹t_Skip ≡ if tF t then [] else [✓]›
    define X_Skip :: ‹'a refusal› where ‹X_Skip ≡ if tF t then range ev else UNIV›
    have ‹(t_Skip, X_Skip) ∈ ℱ Skip›
      by (simp add: F_SKIP t_Skip_def X_Skip_def image_iff)
    moreover from ‹set t ∩ ev ` A = {}› ‹ftF t› have ‹t setinterleaves✓⇘SyncRunit_tj⇙ ((t, t_Skip), A)›
      by (auto simp add: t_Skip_def setinterleavesptick_NilR_iff tF_map_ev_of_ev_same_type_is
          ftF_setinterleavesptick_snoc_tickR_iff[where v = ‹[]›, simplified] SyncRunit_tj_def)
        (metis Int_assoc ftF_E inf_bot_right inf_sup_absorb set_append tF_map_ev_of_ev_same_type_is)
    moreover from ‹X ⊆ X_P ∪ ev ` A› have ‹X ⊆ super_ref_Syncptick SyncRunit_tj X_P A X_Skip›
      by (simp add: super_ref_Syncptick_def subset_iff X_Skip_def image_iff SyncRunit_tj_def) (metis eventptick.exhaust)
    ultimately show ‹(t, X) ∈ ℱ (P ⟦A⟧✓Runit Skip)›
      using ‹(t, X_P) ∈ ℱ P› by (auto simp add: SyncRunit.Syncptick_projs)
  qed
  moreover have ‹?rhs2 ⊆ ℱ ?lhs›
    by (rule subset_trans[of _ ‹{(t, X). t ∈ 𝒟 (P ⟦A⟧✓Runit Skip)}›], simp add: D_SyncRunit_Skip)
      (auto intro: is_processT8)
  ultimately show ‹?rhs1 ∪ ?rhs2 ⊆ ℱ ?lhs› by simp
qed


corollary F_Skip_SyncLunit :
  ‹ℱ (Skip ⟦A⟧✓Lunit Q) =
   {(t, X). ∃X_P. (t, X_P) ∈ ℱ Q ∧ set t ∩ ev ` A = {} ∧ X ⊆ X_P ∪ ev ` A} ∪
   {(t @ u, X) |t u X. tF t ∧ ftF u ∧ t ∈ 𝒟 Q ∧ set t ∩ ev ` A = {}}›
  by (simp flip: SyncRunit.Syncptick_commute add: F_SyncRunit_Skip)



lemmas SyncRunit_Skip_projs = F_SyncRunit_Skip D_SyncRunit_Skip Dmin_SyncRunit_Skip T_SyncRunit_Skip
  and Skip_SyncLunit_projs = F_Skip_SyncLunit D_Skip_SyncLunit Dmin_Skip_SyncLunit T_Skip_SyncLunit





subsubsection ‹Laws›

theorem RenamingTick_SyncRunit :
  ‹RenamingTick (P ⟦A⟧✓Runit Q) g = RenamingTick P g ⟦A⟧✓Runit Q›
  (is ‹?lhs = ?rhs›) for g :: ‹'r ⇒ 's›
proof -
  let ?map = ‹map (map_eventptick id g)›
  let ?RT  = ‹λP. RenamingTick P g›
  let ?map_ev = ‹map (ev ∘ of_ev)›
  let ?map_vim = ‹λX. map_eventptick id g -` X›

  have $ : ‹⋀t. tF t ⟹ ?map t = ?map_ev t›
    by (simp add: tF_map_map_eventptick_is)

  have $$ : ‹t setinterleaves✓⇘SyncRunit_tj⇙ ((u, v), A) ⟹
    ?map t setinterleaves✓⇘SyncRunit_tj⇙ ((?map u, v), A)› for t u v
    by (induct ‹(SyncRunit_tj :: 'r ⇒ unit ⇒ 'r option, u, A, v)› arbitrary: t u v)
      (auto simp add: SyncRunit_tj_def)

  show ‹?lhs = ?rhs›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    then obtain t1 t2 where * : ‹t = ?map t1 @ t2› ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 (P ⟦A⟧✓Runit Q)›
      unfolding Renaming_projs by blast
    from "*"(4) obtain t11 t12 t_P t_Q
      where ** : ‹t1 = t11 @ t12› ‹tF t11› ‹ftF t12›
        ‹t11 setinterleaves✓⇘SyncRunit_tj⇙ ((t_P, t_Q), A)›
        ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      unfolding SyncRunit.Syncptick_projs by blast
    from "**"(4) have ‹?map t11 setinterleaves✓⇘SyncRunit_tj⇙ ((?map t_P, t_Q), A)› by (fact "$$")
    moreover from "**"(5)
    have ‹?map t_P ∈ 𝒟 (?RT P) ∧ t_Q ∈ 𝒯 Q ∨ ?map t_P ∈ 𝒯 (?RT P) ∧ t_Q ∈ 𝒟 Q›
      by (simp add: Renaming_projs)
        (metis "**"(2, 4) append_self_conv ftF_Nil tF_setinterleavesptick_iff)
    ultimately have ‹?map t11 ∈ 𝒟 ?rhs›
      unfolding SyncRunit.Syncptick_projs
      using "**"(2) ftF_Nil tF_map_eventptick_iff by blast
    thus ‹t ∈ 𝒟 ?rhs›
      by (simp add: "*"(1) "**"(1))
        (metis "*"(2, 3) "**"(1) ftF_append is_processT7
          tF_map_eventptick_iff tF_append_iff)
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    with D_T obtain t1 t2 t_P t_Q where * : ‹t = t1 @ t2› ‹tF t1› ‹ftF t2›
      ‹t1 setinterleaves✓⇘SyncRunit_tj⇙ ((t_P, t_Q), A)›
      ‹t_P ∈ 𝒟 (?RT P) ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 (?RT P) ∧ t_P ∉ 𝒟 (?RT P) ∧ t_Q ∈ 𝒟 Q›
      by (simp add: SyncRunit.Syncptick_projs) blast
    from tF_setinterleavesptick_iff[OF "*"(4)]
    have ‹tF t_P› ‹tF t_Q› by (simp_all add: "*"(2))
    from "*"(5) show ‹t ∈ 𝒟 ?lhs›
    proof (elim disjE conjE)
      assume ‹t_P ∈ 𝒟 (?RT P)› ‹t_Q ∈ 𝒯 Q›
      from ‹t_P ∈ 𝒟 (?RT P)›
      obtain t_P1 t_P2 where ** : ‹t_P = ?map t_P1 @ t_P2› ‹tF t_P1› ‹ftF t_P2› ‹t_P1 ∈ 𝒟 P›
        unfolding Renaming_projs by blast
      from "*"(4)[unfolded "**"(1), THEN setinterleavesptick_appendL]
      obtain t11 t12 t_Q1 t_Q2 where *** : ‹t1 = t11 @ t12› ‹t_Q = t_Q1 @ t_Q2›
        ‹t11 setinterleaves✓⇘SyncRunit_tj⇙ ((?map t_P1, t_Q1), A)› by blast
      from "*"(2) ‹tF t_Q› have ‹tF t11› ‹tF t_Q1› by (simp_all add: "***"(1, 2))
      then obtain t11' :: ‹('a, 'r) traceptick› and t_Q1' :: ‹'a trace›
        where ‹tF t11'› ‹tF t_Q1'› ‹t11 = ?map_ev t11'› ‹t_Q1 = ?map_ev t_Q1'› ‹t_Q1 = t_Q1'›
        by (metis tF_map_ev_comp tF_map_ev_of_ev_eq_iff tF_map_ev_of_ev_same_type_is)
      from tF_imp_setinterleavesptick_map_ev_of_ev_iff
        [THEN iffD1, OF this(1) "**"(2) this(2) "***"(3)[unfolded this(3, 4) "$"[OF "**"(2)]]]
      have ‹t11' setinterleaves✓⇘SyncRunit_tj⇙ ((t_P1, t_Q1'), A)› .
      moreover have ‹t_Q1' ∈ 𝒯 Q›
        using "***"(2) ‹t_Q ∈ 𝒯 Q› ‹t_Q1 = t_Q1'› is_processT3_TR_append by blast
      ultimately have ‹t11' ∈ 𝒟 (P ⟦A⟧✓Runit Q)›
        by (simp add: SyncRunit.Syncptick_projs)
          (use "**"(4) ‹tF t11'› ftF_Nil in blast)
      hence ‹?map t11' ∈ 𝒟 ?lhs›
        by (simp add: Renaming_projs)
          (metis ftF_Nil ‹tF t11'› append.right_neutral)
      thus ‹t ∈ 𝒟 ?lhs›
        by (simp add: "*"(1) "***"(1))
          (metis "$" "*"(2, 3) "***"(1) ‹t11 = ?map_ev t11'› ‹tF t11'›
            ftF_append is_processT7 tF_append_iff)
    next
      assume ‹t_P ∈ 𝒯 (?RT P)› ‹t_P ∉ 𝒟 (?RT P)› ‹t_Q ∈ 𝒟 Q›
      from this(1, 2) obtain t_P' where ‹t_P = ?map t_P'› ‹t_P' ∈ 𝒯 P›
        unfolding Renaming_projs by blast
      from ‹tF t_P› ‹t_P = ?map t_P'› have ‹tF t_P'› ‹t_P = ?map_ev t_P'›
        by (simp_all add: tF_map_eventptick_iff "$")
      from "*"(2) ‹tF t_Q› obtain t1' :: ‹('a, 'r) traceptick› and t_Q' :: ‹'a trace›
        where ‹tF t1'› ‹tF t_Q'› ‹t1 = ?map_ev t1'› ‹t_Q = ?map_ev t_Q'› ‹t_Q = t_Q'›
        by (metis tF_map_ev_comp tF_map_ev_of_ev_eq_iff tF_map_ev_of_ev_same_type_is)
      from tF_imp_setinterleavesptick_map_ev_of_ev_iff
        [THEN iffD1, OF this(1) ‹tF t_P'› this(2) "*"(4)[unfolded this(3, 4) ‹t_P = ?map_ev t_P'›]]
      have ‹t1' setinterleaves✓⇘SyncRunit_tj⇙ ((t_P', t_Q'), A)› .
      with ‹t_P' ∈ 𝒯 P› ‹t_Q ∈ 𝒟 Q› have ‹t1' ∈ 𝒟 (P ⟦A⟧✓Runit Q)›
        by (simp add: SyncRunit.Syncptick_projs ‹t_Q = t_Q'›)
          (metis ‹tF t1'› ftF_Nil append.right_neutral)
      hence ‹?map t1' ∈ 𝒟 ?lhs›
        by (simp add: Renaming_projs)
          (metis ftF_Nil ‹tF t1'› append.right_neutral)
      thus ‹t ∈ 𝒟 ?lhs›
        by (simp add: "*"(1) ‹t1 = ?map_ev t1'› "$" "*"(3) ‹tF t1'› is_processT7)
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs› ‹t ∉ 𝒟 ?rhs›
    define X' where ‹X' ≡ X ∩ (range ev ∪ tick ` (range g))›
    { fix g_r assume ‹t @ [✓(g_r)] ∈ 𝒯 ?rhs›
      moreover from ‹t ∉ 𝒟 ?rhs› have ‹t @ [✓(g_r)] ∉ 𝒟 ?rhs› by (meson is_processT9)
      ultimately obtain t_P t_Q where * : ‹t_P ∈ 𝒯 (?RT P)›
        ‹t_Q ∈ 𝒯 Q› ‹t @ [✓(g_r)] setinterleaves✓⇘SyncRunit_tj⇙ ((t_P, t_Q), A)›
        unfolding SyncRunit.Syncptick_projs by blast
      with ‹t @ [✓(g_r)] ∉ 𝒟 ?rhs› have ‹t_P ∉ 𝒟 (?RT P)›
        by (auto simp add: SyncRunit.Syncptick_projs' intro: ftF_Nil)
      with "*"(1) obtain t_P' where ‹t_P = ?map t_P'› ‹t_P' ∈ 𝒯 P›
        unfolding Renaming_projs by blast
      with "*"(3) have ‹g_r ∈ range g›
        by (auto simp add: map_eq_append_conv tick_eq_map_eventptick_iff SyncRunit_tj_def
            elim!: snoc_tick_setinterleavesptickE)
    }
    moreover have ‹(t, X') ∈ ℱ ?rhs›
    proof -
      from ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
      obtain t' where ‹t = ?map t'› ‹(t', ?map_vim X) ∈ ℱ (P ⟦A⟧✓Runit Q)›
        unfolding Renaming_projs by blast
      with ‹t ∉ 𝒟 ?lhs› have ‹t' ∉ 𝒟 (P ⟦A⟧✓Runit Q)›
        by (simp add: Renaming_projs SyncRunit.Syncptick_projs)
          (metis (no_types) append.right_neutral ftF_Nil map_append ftF_map_eventptick_iff)
      with ‹(t', map_eventptick id g -` X) ∈ ℱ (P ⟦A⟧✓Runit Q)› obtain t_P t_Q X_P X_Q
        where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹t' setinterleaves✓⇘SyncRunit_tj⇙ ((t_P, t_Q), A)›
          ‹?map_vim X ⊆ super_ref_Syncptick SyncRunit_tj X_P A X_Q›
        unfolding SyncRunit.Syncptick_projs by force
      from ‹(t', ?map_vim X) ∈ ℱ (P ⟦A⟧✓Runit Q)›[THEN F_imp_ftF] show ‹(t, X') ∈ ℱ ?rhs›
      proof (elim ftF_E)
        fix t'' r assume ‹t' = t'' @ [✓(r)]›
        with "*"(3) obtain t_P' t_Q'
          where ** : ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓]›
            ‹t'' setinterleaves✓⇘SyncRunit_tj⇙ ((t_P', t_Q'), A)›
          by (auto simp add: SyncRunit_tj_def elim!: snoc_tick_setinterleavesptickE)
        from "$$"[OF "**"(3)] have ‹t setinterleaves✓⇘SyncRunit_tj⇙ ((?map t_P, t_Q), A)›
          by (simp add: ‹t = ?map t'› ‹t' = t'' @ [✓(r)]› "**"(1, 2) setinterleavesptick_snoc_tick SyncRunit_tj_def)
        moreover from "*"(1) have ‹?map t_P ∈ 𝒯 (?RT P)›
          by (auto simp add: T_Renaming dest: F_T)
        ultimately have ‹t ∈ 𝒯 ?rhs›
          by (simp add: SyncRunit.Syncptick_projs) (meson "*"(2) F_T)
        thus ‹(t, X') ∈ ℱ ?rhs›
          by (simp add: ‹t = ?map t'› ‹t' = t'' @ [✓(r)]› tick_T_F)
      next
        assume ‹tF t'›
        with tF_setinterleavesptick_iff[OF "*"(3)] have ‹tF t_P› ‹tF t_Q› by simp_all
        define X_P' where ‹X_P' ≡ {ev a |a. ev a ∈ X_P} ∪
          (if ✓ ∈ X_Q then {} else {✓(g r) |r. ✓(r) ∈ X_P ∧ ✓(g r) ∈ X})›
        have ‹?map_vim X_P' ⊆ X_P›
        proof (rule subsetI)
          show ‹e ∈ ?map_vim X_P' ⟹ e ∈ X_P› for e
            using "*"(4)[THEN set_mp, of ‹✓(of_tick e)›]
            by (cases e) (auto simp add: X_P'_def super_ref_Syncptick_def SyncRunit_tj_def split: if_split_asm)
        qed
        hence ‹(t_P, ?map_vim X_P') ∈ ℱ P› by (meson "*"(1) is_processT4)
        hence ‹(?map_ev t_P, X_P') ∈ ℱ (?RT P)›
          by (simp add: F_Renaming) (metis ‹tF t_P› "$")
        moreover have ‹X' ⊆ super_ref_Syncptick SyncRunit_tj X_P' A X_Q›
        proof (rule subsetI)
          show ‹e ∈ X' ⟹ e ∈ super_ref_Syncptick SyncRunit_tj X_P' A X_Q› for e
            using "*"(4)[THEN set_mp, of ‹ev (of_ev e)›] "*"(4)[THEN set_mp, of ‹✓(_)›]
            by (cases e) (auto simp add: super_ref_Syncptick_def X'_def X_P'_def SyncRunit_tj_def)
        qed
        ultimately show ‹(t, X') ∈ ℱ ?rhs›
          by (simp add: SyncRunit.Syncptick_projs)
            (metis (mono_tags, lifting) "$" "*"(2, 3) ‹t = ?map t'› ‹tF t_P› "$$")
      qed
    qed
    ultimately have ‹(t, X' ∪ tick ` (-  range g)) ∈ ℱ ?rhs›
      by (blast intro: is_processT5 F_T)
    also have ‹X ⊆ X' ∪ tick ` (-  range g)›
      by (simp add: X'_def subset_iff image_iff) (metis eventptick.exhaust ComplI image_iff)
    finally (is_processT4) show ‹(t, X) ∈ ℱ ?rhs› .
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?lhs› ‹t ∉ 𝒟 ?rhs›
    define X' where ‹X' ≡ X ∩ (range ev ∪ tick ` (range g))›
    { fix g_r assume ‹t @ [✓(g_r)] ∈ 𝒯 ?lhs›
      moreover from ‹t ∉ 𝒟 ?lhs› have ‹t @ [✓(g_r)] ∉ 𝒟 ?lhs› by (meson is_processT9)
      ultimately have ‹g_r ∈ range g›
        by (auto simp add: Renaming_projs append_eq_map_conv tick_eq_map_eventptick_iff)
    }
    moreover have ‹(t, X') ∈ ℱ ?lhs›
    proof -
      from ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs› obtain t_P t_Q X_P X_Q
        where * : ‹(t_P, X_P) ∈ ℱ (?RT P)› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹t setinterleaves✓⇘SyncRunit_tj⇙ ((t_P, t_Q), A)›
          ‹X ⊆ super_ref_Syncptick SyncRunit_tj X_P A X_Q›
        unfolding SyncRunit.Syncptick_projs by blast
      with ‹t ∉ 𝒟 ?rhs› have ‹t_P ∉ 𝒟 (?RT P)›
        unfolding SyncRunit.Syncptick_projs' by (blast intro: F_T ftF_Nil)
      with "*"(1) obtain t_P' where ** : ‹t_P = ?map t_P'› ‹(t_P', ?map_vim X_P) ∈ ℱ P›
        unfolding Renaming_projs by blast
      from ‹(t_P', ?map_vim X_P) ∈ ℱ P›[THEN F_imp_ftF] show ‹(t, X') ∈ ℱ ?lhs›
      proof (elim ftF_E)
        fix t_P'' r assume ‹t_P' = t_P'' @ [✓(r)]› ‹tF t_P''›
        with "*"(3) obtain t' t_Q' where *** : ‹t = t' @ [✓(g r)]› ‹t_Q = t_Q' @ [✓]›
          ‹t' setinterleaves✓⇘SyncRunit_tj⇙ ((?map t_P'', t_Q'), A)›
          by (auto simp add: "**"(1) ftF_setinterleavesptick_snoc_tickL_iff
              [OF ‹(t, X) ∈ ℱ ?rhs›[THEN F_imp_ftF]] SyncRunit_tj_def)
        from ‹(t, X) ∈ ℱ ?rhs› "***"(1) have ‹tF t'›
          by (metis  F_imp_ftF ftF_append_iff list.discI)
        have ‹tF (?map t_P'')› by (simp add: ‹tF t_P''› tF_map_eventptick_iff)
        from "*"(2) "***"(2) have ‹tF t_Q'›
          by (metis F_imp_ftF ftF_append_iff not_Cons_self)
        from tF_imp_setinterleavesptick_map_ev_of_ev_iff[THEN iffD2]
          ‹tF t'› ‹tF (?map t_P'')› ‹tF t_Q'› "***"(3)
        have ‹?map_ev t' setinterleaves✓⇘SyncRunit_tj⇙ ((?map_ev (?map t_P''), ?map_ev t_Q'), A)› .
        also have ‹?map_ev (?map t_P'') = t_P''›
          by (metis "$" ‹tF t_P''› tF_map_ev_of_ev_eq_iff)
        also have ‹?map_ev t_Q' = t_Q'›
          by (simp add: ‹tF t_Q'› tF_map_ev_of_ev_same_type_is)
        finally have ‹?map_ev t' setinterleaves✓⇘SyncRunit_tj⇙ ((t_P'', t_Q'), A)› .
        hence ‹?map_ev t' @ [✓(r)] setinterleaves✓⇘SyncRunit_tj⇙ ((t_P', t_Q), A)›
          by (simp add: ‹t_P' = t_P'' @ [✓(r)]› "***"(2) setinterleavesptick_snoc_tick SyncRunit_tj_def)
        hence ‹?map_ev t' @ [✓(r)] ∈ 𝒯 (P ⟦A⟧✓Runit Q)›
          by (simp add: SyncRunit.Syncptick_projs) (meson "*"(2) "**"(2) F_T)
        hence ‹?map (?map_ev t' @ [✓(r)]) ∈ 𝒯 ?lhs› by (auto simp add: T_Renaming)
        also from ‹tF t'› have ‹?map (?map_ev t' @ [✓(r)]) = t›
          by (simp add: "***"(1) list.map_comp)
            (metis "$" list.map_comp tF_map_ev_comp tF_map_ev_of_ev_eq_iff)
        finally have ‹t ∈ 𝒯 ?lhs› .
        with "***"(1) show ‹(t, X') ∈ ℱ ?lhs› by (simp add: tick_T_F)
      next
        assume ‹tF t_P'›
        hence ‹tF t_P› by (simp add: "**"(1) tF_map_eventptick_iff)
        with setinterleavesptick_tF_imp[OF _ "*"(3)]
        have ‹tF t› ‹tF t_Q› by simp_all
        from tF_imp_setinterleavesptick_map_ev_of_ev_iff[THEN iffD2]
          ‹tF t› ‹tF t_P› ‹tF t_Q› "*"(3)
        have ‹?map_ev t setinterleaves✓⇘SyncRunit_tj⇙ ((?map_ev t_P, ?map_ev t_Q), A)› .
        also have ‹?map_ev t_Q = t_Q›
          by (simp add: ‹tF t_Q› tF_map_ev_of_ev_same_type_is)
        also have ‹?map_ev t_P = t_P'›
          by (metis "$" "**"(1) ‹tF t_P'› tF_map_ev_of_ev_eq_iff)
        finally have ‹?map_ev t setinterleaves✓⇘SyncRunit_tj⇙ ((t_P', t_Q), A)› .
        moreover have ‹?map_vim X' ⊆ super_ref_Syncptick SyncRunit_tj (?map_vim X_P) A X_Q›
        proof (rule subsetI)
          from "*"(4) show ‹e ∈ ?map_vim X' ⟹ e ∈ super_ref_Syncptick SyncRunit_tj (?map_vim X_P) A X_Q› for e
            by (cases e) (auto simp add: super_ref_Syncptick_def X'_def SyncRunit_tj_def)
        qed
        ultimately have ‹(?map_ev t, map_eventptick id g -` X') ∈ ℱ (P ⟦A⟧✓Runit Q)›
          by (simp add: SyncRunit.Syncptick_projs) (metis "*"(2) "**"(2))
        hence ‹(?map (?map_ev t), X') ∈ ℱ ?lhs› by (auto simp add: F_Renaming)
        also have ‹?map (?map_ev t) = t›
          by (metis "$" ‹tF t› tF_map_ev_comp tF_map_ev_of_ev_eq_iff)
        finally show ‹(t, X') ∈ ℱ ?lhs› .
      qed
    qed
    ultimately have ‹(t, X' ∪ tick ` (-  range g)) ∈ ℱ ?lhs›
      by (blast intro: is_processT5 F_T)
    also have ‹X ⊆ X' ∪ tick ` (-  range g)›
      by (simp add: X'_def subset_iff image_iff) (metis eventptick.exhaust ComplI image_iff)
    finally (is_processT4) show ‹(t, X) ∈ ℱ ?lhs› .
  qed
qed


corollary RenamingTick_SyncLunit :
  ‹RenamingTick (P ⟦A⟧✓Lunit Q) g = P ⟦A⟧✓Lunit RenamingTick Q g›
  by (metis RenamingTick_SyncRunit RenamingTick_id SyncRunit.Syncptick_commute)





(* TODO: are the following results useful ? *)

lemma GlobalNdet_SyncRunit_Skip :
  ‹⊓x ∈ S. P x ⟦A⟧✓Runit Skip = ⊓x ∈ S. (P x ⟦A⟧✓Runit Skip)›
  by (simp add: SyncRunit.Syncptick_distrib_GlobalNdet_right)

lemma Skip_SyncLunit_GlobalNdet :
  ‹Skip ⟦A⟧✓Lunit ⊓x ∈ S. P x = ⊓x ∈ S. (Skip ⟦A⟧✓Lunit P x)›
  by (simp add: SyncRunit.Synchroptick_comm_dual.Syncptick_distrib_GlobalNdet_left)


lemma Ndet_SyncRunit_Skip :
  ‹P ⊓ Q ⟦A⟧✓Runit Skip = (P ⟦A⟧✓Runit Skip) ⊓ (Q ⟦A⟧✓Runit Skip)›
  by (fact SyncRunit.Syncptick_distrib_Ndet_right)

lemma Skip_SyncLunit_Ndet :
  ‹Skip ⟦A⟧✓Lunit P ⊓ Q = (Skip ⟦A⟧✓Lunit P) ⊓ (Skip ⟦A⟧✓Lunit Q)›
  by (fact SyncRunit.Synchroptick_comm_dual.Syncptick_distrib_Ndet_left)





theorem (in Synchroptick) SyncRunit_Skip_distrib_Syncptick_left :
  ‹P ⟦S⟧✓ Q ⟦A⟧✓Runit Skip = ((P ⟦A⟧✓Runit Skip) ⟦S⟧✓ (Skip ⟦A⟧✓Lunit Q))› (is ‹?lhs = ?rhs›)
proof (rule Process_eqI_Dmin_version)
  fix t assume ‹t ∈ 𝒟min ?lhs›
  hence ‹t ∈ 𝒟min (P ⟦S⟧✓ Q)› ‹set t ∩ ev ` A = {}› by (simp_all add: Dmin_SyncRunit_Skip)
  from this(1) obtain t_P t_Q
    where * : ‹tF t› ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟min P ∧ t_Q ∈ 𝒟min Q ∨ t_P ∈ 𝒟min P ∧ t_Q ∈ 𝒯 Q ∨ t_Q ∈ 𝒟min Q ∧ t_P ∈ 𝒯 P›
    by (auto dest: Dmin_Syncptick_subset[THEN set_mp])
  from "*"(2)[THEN setinterleavesptick_ev_in_set_iff] ‹set t ∩ ev ` A = {}›
  have ** : ‹set t_P ∩ ev ` A = {}› ‹set t_Q ∩ ev ` A = {}› by auto
  from "*"(3) show ‹t ∈ 𝒟 ?rhs›
  proof (elim disjE conjE)
    assume ‹t_P ∈ 𝒟min P› ‹t_Q ∈ 𝒟min Q›
    with "**" have ‹t_P ∈ 𝒟min (P ⟦A⟧✓Runit Skip)› ‹t_Q ∈ 𝒟min (Skip ⟦A⟧✓Lunit Q)›
      by (simp_all add: Dmin_SyncRunit_Skip Dmin_Skip_SyncLunit)
    with "*"(1, 2) show ‹t ∈ 𝒟 ?rhs›
      by (simp add: D_Syncptick)
        (meson Dmin_subset_D D_T ftF_Nil self_append_conv subset_iff)
  next
    assume ‹t_P ∈ 𝒟min P› ‹t_Q ∈ 𝒯 Q›
    from ‹t_P ∈ 𝒟min P› "**"(1) have ‹t_P ∈ 𝒟min (P ⟦A⟧✓Runit Skip)›
      by (simp add: Dmin_SyncRunit_Skip)
    moreover from ‹t_Q ∈ 𝒯 Q› "**"(2) have ‹t_Q ∈ 𝒯 (Skip ⟦A⟧✓Lunit Q)›
      by (simp add: T_Skip_SyncLunit)
    ultimately show ‹t ∈ 𝒟 ?rhs›
      using "*"(1, 2) by (simp add: D_Syncptick)
        (meson Dmin_subset_D D_T ftF_Nil self_append_conv subset_iff)
  next
    assume ‹t_Q ∈ 𝒟min Q› ‹t_P ∈ 𝒯 P›
    from ‹t_Q ∈ 𝒟min Q› "**"(2) have ‹t_Q ∈ 𝒟min (Skip ⟦A⟧✓Lunit Q)›
      by (simp add: Dmin_Skip_SyncLunit)
    moreover from ‹t_P ∈ 𝒯 P› "**"(1) have ‹t_P ∈ 𝒯 (P ⟦A⟧✓Runit Skip)›
      by (simp add: T_SyncRunit_Skip)
    ultimately show ‹t ∈ 𝒟 ?rhs›
      using "*"(1, 2) by (simp add: D_Syncptick)
        (meson Dmin_subset_D D_T ftF_Nil self_append_conv subset_iff)
  qed
next
  fix t assume ‹t ∈ 𝒟min ?rhs›
  from Dmin_Syncptick_subset[THEN set_mp, OF this]
  obtain t_P t_Q where * : ‹tF t› ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
    ‹set t_P ∩ ev ` A = {}› ‹set t_Q ∩ ev ` A = {}›
    ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
    by (auto simp add: SyncRunit_Skip_projs Skip_SyncLunit_projs dest!: Dmin_D dest: D_T)
  from "*"(2)[THEN setinterleavesptick_ev_in_set_iff] "*"(3, 4)
  have ‹set t ∩ ev ` A = {}› by auto
  moreover from "*"(1, 2, 5) have ‹t ∈ 𝒟 (P ⟦S⟧✓ Q)›
    by (auto simp add: D_Syncptick intro: ftF_Nil)
  ultimately show ‹t ∈ 𝒟 ?lhs›
    using "*"(1) by (auto simp add: D_SyncRunit_Skip intro: ftF_Nil)
next
  fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
  from this(1, 2) obtain X'
    where * : ‹(t, X') ∈ ℱ (P ⟦S⟧✓ Q)› ‹set t ∩ ev ` A = {}› ‹X ⊆ X' ∪ ev ` A›
    by (auto simp add: SyncRunit_Skip_projs)
  from "*"(1) consider ‹t ∈ 𝒟 (P ⟦S⟧✓ Q)›
    | (fail) t_P t_Q X_P X_Q where ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
      ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› ‹X' ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
    unfolding Syncptick_projs by blast
  thus ‹(t, X) ∈ ℱ ?rhs›
  proof cases
    assume ‹t ∈ 𝒟 (P ⟦S⟧✓ Q)›
    from this this[THEN D_imp_ftF] "*"(2) have ‹t ∈ 𝒟 ?lhs›
      by (auto elim!: ftF_E simp add: SyncRunit_Skip_projs intro: ftF_Nil)
        (metis ftF_single is_processT9)
    with ‹t ∉ 𝒟 ?lhs› have False ..
    thus ‹(t, X) ∈ ℱ ?rhs› ..
  next
    case fail
    from "*"(2) fail(3)[THEN setinterleavesptick_ev_in_set_iff]
    have ** : ‹set t_P ∩ ev ` A = {}› ‹set t_Q ∩ ev ` A = {}› by auto
    from "**"(1) fail(1) have ‹(t_P, X_P ∪ ev ` A) ∈ ℱ (P ⟦A⟧✓Runit Skip)›
      by (auto simp add: F_SyncRunit_Skip)
    moreover from "**"(2) fail(2) have ‹(t_Q, X_Q ∪ ev ` A) ∈ ℱ (Skip ⟦A⟧✓Lunit Q)›
      by (auto simp add: F_Skip_SyncLunit)
    moreover from "*"(3) fail(4) have ‹X ⊆ super_ref_Syncptick (⊗✓) (X_P ∪ ev ` A) S (X_Q ∪ ev ` A)›
      by (fastforce simp add: super_ref_Syncptick_def subset_iff)
    ultimately show ‹(t, X) ∈ ℱ ?rhs›
      using fail(3) by (auto simp add: F_Syncptick)
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
  then obtain t_P t_Q X_P X_Q
    where * : ‹(t_P, X_P) ∈ ℱ (P ⟦A⟧✓Runit Skip)› ‹t_P ∉ 𝒟 (P ⟦A⟧✓Runit Skip)›
      ‹(t_Q, X_Q) ∈ ℱ (Skip ⟦A⟧✓Lunit Q)› ‹t_Q ∉ 𝒟 (Skip ⟦A⟧✓Lunit Q)›
      ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› ‹X ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
    by (simp add: Syncptick_projs') (metis F_T append_Nil2 ftF_Nil)
  from "*"(1, 2) obtain X_P'
    where ** : ‹(t_P, X_P') ∈ ℱ P› ‹set t_P ∩ ev ` A = {}› ‹X_P ⊆ X_P' ∪ ev ` A›
    unfolding SyncRunit_Skip_projs by blast
  from "*"(3, 4) obtain X_Q'
    where *** : ‹(t_Q, X_Q') ∈ ℱ Q› ‹set t_Q ∩ ev ` A = {}› ‹X_Q ⊆ X_Q' ∪ ev ` A›
    unfolding Skip_SyncLunit_projs by blast
  have ‹(t, super_ref_Syncptick (⊗✓) X_P' S X_Q') ∈ ℱ (P ⟦S⟧✓ Q)›
    using "*"(5) "**"(1) "***"(1) by (auto simp add: F_Syncptick)
  moreover from "*"(5)[THEN setinterleavesptick_ev_in_set_iff] "**"(2) "***"(2)
  have ‹set t ∩ ev ` A = {}› by blast
  moreover from "*"(6) "**"(3) "***"(3)
  have ‹X ⊆ super_ref_Syncptick (⊗✓) X_P' S X_Q' ∪ ev ` A›
    by (fastforce simp add: super_ref_Syncptick_def subset_iff)
  ultimately show ‹(t, X) ∈ ℱ ?lhs›
    by (auto simp add: F_SyncRunit_Skip)
qed


corollary (in Synchroptick) Skip_SyncLunit_distrib_Syncptick_right :
  ‹Skip ⟦A⟧✓Lunit (P ⟦S⟧✓ Q) = ((P ⟦A⟧✓Runit Skip) ⟦S⟧✓ (Skip ⟦A⟧✓Lunit Q))›
  by (metis SyncRunit_Skip_distrib_Syncptick_left RenamingTick_id SyncRunit.Syncptick_commute)



unbundle no option_type_syntax


(*<*)
end
  (*>*)