Theory After_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 ‹Operational Semantics Laws›

(*<*)
theory After_CSP_PTick_Laws
  imports Basic_CSP_PTick_Laws
    "HOL-CSP_OpSem"
begin
  (*>*)



section ‹Behaviour of \<^const>‹initials››

subsection ‹\<^const>‹TickSwap››

lemma initials_TickSwap :
  ‹(TickSwap P)⇧⁰ = (  if P = ⊥ then UNIV
                    else {ev a |a. ev a ∈ P⇧⁰} ∪ {✓((s, r)) |r s. ✓((r, s)) ∈ P⇧⁰})›
  by (auto simp add: TickSwap_is_Renaming initials_Renaming image_iff
      map_event⇩_p⇩_t⇩_i⇩_c⇩_k_eq_tick_iff map_event⇩_p⇩_t⇩_i⇩_c⇩_k_eq_ev_iff 
      tick_eq_map_event⇩_p⇩_t⇩_i⇩_c⇩_k_iff ev_eq_map_event⇩_p⇩_t⇩_i⇩_c⇩_k_iff)
    (metis tick_swap.elims)



subsection ‹Sequential Composition›

lemma initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k : 
  ‹(P ❙;⇩_✓ Q)⇧⁰ = (  if P = ⊥ then UNIV
                else {ev a |a. ev a ∈ P⇧⁰} ∪ (⋃r∈{r. ✓(r) ∈ P⇧⁰}. (Q r)⇧⁰))›
  (is ‹_ = (if _ then _ else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ⟹ (P ❙;⇩_✓ Q)⇧⁰ = UNIV› by simp
next
  show ‹(P ❙;⇩_✓ Q)⇧⁰ = {ev a |a. ev a ∈ P⇧⁰} ∪ (⋃r∈{r. ✓(r) ∈ P⇧⁰}. (Q r)⇧⁰)› if ‹P ≠ ⊥›
  proof (intro subset_antisym subsetI)
    fix e assume ‹e ∈ (P ❙;⇩_✓ Q)⇧⁰›
    from event⇩_p⇩_t⇩_i⇩_c⇩_k.exhaust consider a where ‹e = ev a› | r where ‹e = ✓(r)› by blast
    thus ‹e ∈ ?rhs›
    proof cases
      from ‹e ∈ (P ❙;⇩_✓ Q)⇧⁰› ‹P ≠ ⊥› show ‹e = ev a ⟹ e ∈ ?rhs› for a
        by (auto simp add: image_iff initials_def Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs Cons_eq_append_conv BOT_iff_Nil_D intro: D_T dest: initials_memD)
          (use initials_memI in ‹blast dest: initials_memD›)
    next
      from ‹e ∈ (P ❙;⇩_✓ Q)⇧⁰› ‹P ≠ ⊥› show ‹e = ✓(r) ⟹ e ∈ ?rhs› for r
        by (auto simp add: image_iff initials_def Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs BOT_iff_Nil_D Cons_eq_append_conv)
    qed
  next
    show ‹e ∈ ?rhs ⟹ e ∈ (P ❙;⇩_✓ Q)⇧⁰› for e
      by (simp add: initials_def Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs, elim disjE exE conjE)
        (fastforce, metis list.simps(8) self_append_conv2 tickFree_Nil)
  qed
qed



subsection ‹Synchronization Product›

lemma (in Sync⇩_p⇩_t⇩_i⇩_c⇩_k_locale) initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹(P ⟦S⟧⇩_✓ Q)⇧⁰ =
   (if P = ⊥ ∨ Q = ⊥ then UNIV else
    {ev a |a. a ∈ S ∧ ev a ∈ P⇧⁰ ∧ ev a ∈ Q⇧⁰ ∨ a ∉ S ∧ (ev a ∈ P⇧⁰ ∨ ev a ∈ Q⇧⁰)} ∪
    {✓(r_s) |r_s r s. tick_join r s = Some r_s ∧ ✓(r) ∈ P⇧⁰ ∧ ✓(s) ∈ Q⇧⁰})›
  (is ‹(P ⟦S⟧⇩_✓ Q)⇧⁰ = (if P = ⊥ ∨ Q = ⊥ then UNIV else ?rhs_ev ∪ ?rhs_tick)›)
proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ∨ Q = ⊥ ⟹ (P ⟦S⟧⇩_✓ Q)⇧⁰ = UNIV›
    by (metis Sync⇩_p⇩_t⇩_i⇩_c⇩_k_is_BOT_iff initials_BOT)
next
  show ‹(P ⟦S⟧⇩_✓ Q)⇧⁰ = ?rhs_ev ∪ ?rhs_tick› if non_BOT : ‹¬ (P = ⊥ ∨ Q = ⊥)›
  proof (intro subset_antisym subsetI)
    show ‹e ∈ ?rhs_ev ∪ ?rhs_tick ⟹ e ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰› for e
    proof (elim UnE)
      assume ‹e ∈ ?rhs_ev›
      then consider a where ‹e = ev a› ‹a ∈ S› ‹ev a ∈ P⇧⁰› ‹ev a ∈ Q⇧⁰›
        | a where ‹e = ev a› ‹a ∉ S› ‹ev a ∈ P⇧⁰ ∨ ev a ∈ Q⇧⁰› by blast
      thus ‹e ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
      proof cases
        fix a assume ‹e = ev a› ‹a ∈ S› ‹ev a ∈ P⇧⁰› ‹ev a ∈ Q⇧⁰›
        have * : ‹[ev a] setinterleaves⇩_✓⇘tick_join⇙ (([ev a], [ev a]), S)›
          by (simp add: ‹a ∈ S›)
        from ‹ev a ∈ P⇧⁰› ‹ev a ∈ Q⇧⁰› show ‹e ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
          by (simp add: ‹e = ev a› initials_def T_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) (use "*" in blast)
      next
        fix a assume ‹e = ev a› ‹a ∉ S› ‹ev a ∈ P⇧⁰ ∨ ev a ∈ Q⇧⁰›
        from ‹ev a ∈ P⇧⁰ ∨ ev a ∈ Q⇧⁰› show ‹e ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
        proof (elim disjE)
          assume ‹ev a ∈ P⇧⁰›
          have * : ‹[ev a] setinterleaves⇩_✓⇘tick_join⇙ (([ev a], []), S)›
            by (simp add: ‹a ∉ S›)
          from ‹ev a ∈ P⇧⁰› show ‹e ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
            by (simp add: ‹e = ev a› initials_def T_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) (meson "*" is_processT1_TR)
        next
          assume ‹ev a ∈ Q⇧⁰›
          have * : ‹[ev a] setinterleaves⇩_✓⇘tick_join⇙ (([], [ev a]), S)›
            by (simp add: ‹a ∉ S›)
          from ‹ev a ∈ Q⇧⁰› show ‹e ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
            by (simp add: ‹e = ev a› initials_def T_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) (meson "*" is_processT1_TR)
        qed
      qed
    next
      assume ‹e ∈ ?rhs_tick›
      then obtain r_s r s where ‹tick_join r s = Some r_s›
        ‹e = ✓(r_s)› ‹✓(r) ∈ P⇧⁰› ‹✓(s) ∈ Q⇧⁰› by blast
      have * : ‹[✓(r_s)] setinterleaves⇩_✓⇘tick_join⇙ (([✓(r)], [✓(s)]), S)›
        by (simp add: ‹tick_join r s = Some r_s›)
      from ‹✓(r) ∈ P⇧⁰› ‹✓(s) ∈ Q⇧⁰› show ‹e ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
        by (simp add: ‹e = ✓(r_s)› initials_def T_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) (use "*" in blast)
    qed
  next
    fix e assume ‹e ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
    then consider t_P t_Q where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
      ‹[e] setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)› 
    | (div) t u t_P t_Q
    where ‹[e] = t @ u› ‹ftF u› ‹tF t ∨ u = []›
      ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      unfolding initials_def T_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
    thus ‹e ∈ ?rhs_ev ∪ ?rhs_tick›
    proof cases
      show ‹t_P ∈ 𝒯 P ⟹ t_Q ∈ 𝒯 Q ⟹
            [e] setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S) ⟹
            e ∈ ?rhs_ev ∪ ?rhs_tick› for t_P t_Q
        by (cases e; cases t_P; cases t_Q)
          (auto simp add: initials_def setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps
            split: if_split_asm option.split_asm event⇩_p⇩_t⇩_i⇩_c⇩_k.splits
            dest!: Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k)
    next
      case div
      have ‹t ≠ []› by (metis BOT_iff_Nil_D Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k div(4,5) non_BOT)
      hence ‹t = [e] ∧ u = []›
        by (metis append_Cons append_Nil div(1) list.inject neq_Nil_conv)
      with div(4, 5) non_BOT show ‹e ∈ ?rhs_ev ∪ ?rhs_tick›
        by (cases e; cases t_P; cases t_Q)
          (auto simp add: initials_def setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps BOT_iff_Nil_D
            split: if_split_asm event⇩_p⇩_t⇩_i⇩_c⇩_k.splits option.split_asm 
            dest!: Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k intro: D_T)
    qed
  qed
qed



section ‹Laws of After›

subsection ‹Sequential Composition›

locale AfterDuplicated_same_events = AfterDuplicated Ψ⇩_α Ψ⇩_β
  for Ψ⇩_α :: ‹('a, 'r ) process⇩_p⇩_t⇩_i⇩_c⇩_k ⇒ 'a ⇒ ('a, 'r ) process⇩_p⇩_t⇩_i⇩_c⇩_k›
    and Ψ⇩_β :: ‹('a, 's) process⇩_p⇩_t⇩_i⇩_c⇩_k ⇒ 'a ⇒ ('a, 's) process⇩_p⇩_t⇩_i⇩_c⇩_k›
begin

notation After⇩_α.After (infixl ‹after⇩_α› 86)
notation After⇩_β.After (infixl ‹after⇩_β› 86)


lemma not_skippable_or_not_initialR_After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹(P ❙;⇩_✓ Q) after⇩_β a = (if ev a ∈ P⇧⁰ then P  after⇩_α a ❙;⇩_✓ Q else Ψ⇩_β (P ❙;⇩_✓ Q) a)›
  if ‹range tick ∩ P⇧⁰ = {} ∨ (∀r. ✓(r) ∈ P⇧⁰ ⟶ ev a ∉ (Q r)⇧⁰)›
proof (cases ‹P = ⊥›)
  show ‹P = ⊥ ⟹ (P ❙;⇩_✓ Q) after⇩_β a =
        (if ev a ∈ P⇧⁰ then P after⇩_α a ❙;⇩_✓ Q else Ψ⇩_β (P ❙;⇩_✓ Q) a)›
    by (simp add: After.After_BOT)
next
  note denot_projs = After.After_projs Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs
  assume non_BOT: ‹P ≠ ⊥›
  with that have $ : ‹ev a ∈ (P ❙;⇩_✓ Q)⇧⁰ ⟷ ev a ∈ P⇧⁰›
    by (auto simp add: initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k)
  show ‹(P ❙;⇩_✓ Q) after⇩_β a = (if ev a ∈ P⇧⁰ then P after⇩_α a ❙;⇩_✓ Q else Ψ⇩_β (P ❙;⇩_✓ Q) a)›
  proof (split if_split, intro conjI impI)
    from "$" show ‹ev a ∉ P⇧⁰ ⟹ (P ❙;⇩_✓ Q) after⇩_β a = Ψ⇩_β (P ❙;⇩_✓ Q) a›
      by (simp add: After⇩_β.not_initial_After)
  next
    assume initial_P : ‹ev a ∈ P⇧⁰›
    show ‹(P ❙;⇩_✓ Q) after⇩_β a = P after⇩_α a ❙;⇩_✓ Q›
    proof (rule Process_eq_optimizedI)
      fix t assume ‹t ∈ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)›
      then consider (D_P) t' u where ‹ev a # t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
        | (D_Q) t' r u where ‹ev a # t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹u ∈ 𝒟 (Q r)›
        by (auto simp add: denot_projs "$" initial_P)
      thus ‹t ∈ 𝒟 (P after⇩_α a ❙;⇩_✓ Q)›
      proof cases
        case D_P with non_BOT initial_P show ‹t ∈ 𝒟 (P after⇩_α a ❙;⇩_✓ Q)›
          by (cases t') (auto simp add: BOT_iff_Nil_D denot_projs)
      next
        case D_Q with initial_P show ‹t ∈ 𝒟 (P after⇩_α a ❙;⇩_✓ Q)›
          by (cases t', simp_all add: BOT_iff_Nil_D denot_projs)
            (metis D_T disjoint_iff initials_memI rangeI that, blast)
      qed
    next
      fix t assume ‹t ∈ 𝒟 (P after⇩_α a ❙;⇩_✓ Q)›
      then consider (D_P) t' u where ‹t = map (ev ∘ of_ev) t' @ u› ‹ev a # t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
        | (D_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹ev a # t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹u ∈ 𝒟 (Q r)›
        by (auto simp add: denot_projs initial_P)
      thus ‹t ∈ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)›
      proof cases
        case D_P thus ‹t ∈ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)›
          by (simp add: denot_projs "$" initial_P Cons_eq_append_conv Cons_eq_map_conv)
            (metis event⇩_p⇩_t⇩_i⇩_c⇩_k.disc(1) event⇩_p⇩_t⇩_i⇩_c⇩_k.sel(1) tickFree_Cons_iff)
      next
        case D_Q thus ‹t ∈ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)›
          by (simp add: denot_projs "$" initial_P Cons_eq_append_conv Cons_eq_map_conv)
            (metis append_Cons event⇩_p⇩_t⇩_i⇩_c⇩_k.sel(1) is_ev_def tickFree_Cons_iff)
      qed
    next
      fix t X assume ‹(t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)› ‹t ∉ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)›
      then consider (F_P) t' where ‹ev a # t = map (ev ∘ of_ev) t'›
        ‹(t', ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ P› ‹tF t'›
      | (F_Q) t' r u where ‹ev a # t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P›
        ‹tF t'› ‹(u, X) ∈ ℱ (Q r)›
        by (auto simp add: denot_projs "$" initial_P)
          (metis (mono_tags, lifting) comp_apply list.simps(9) tickFree_Cons_iff)
      thus ‹(t, X) ∈ ℱ (P after⇩_α a ❙;⇩_✓ Q)›
      proof cases
        case F_P thus ‹(t, X) ∈ ℱ (P after⇩_α a ❙;⇩_✓ Q)›
          by (auto simp add: denot_projs initial_P)
      next
        case F_Q thus ‹(t, X) ∈ ℱ (P after⇩_α a ❙;⇩_✓ Q)›
          by (cases t', auto simp add:denot_projs initial_P intro: initials_memI)
            (metis F_T Int_iff empty_iff initials_memI rangeI that)
      qed
    next
      fix t X assume ‹(t, X) ∈ ℱ (P after⇩_α a ❙;⇩_✓ Q)› ‹t ∉ 𝒟 (P after⇩_α a ❙;⇩_✓ Q)›
      then consider (F_P) t' where ‹t = map (ev ∘ of_ev) t'›
        ‹(ev a # t', ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ P› ‹tF t'›
      | (F_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹ev a # t' @ [✓(r)] ∈ 𝒯 P›
        ‹tF t'› ‹(u, X) ∈ ℱ (Q r)›
        by (auto simp add: denot_projs initial_P)
      thus ‹(t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)›
      proof cases
        case F_P thus ‹(t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)›
          by (simp add: denot_projs "$" initial_P Cons_eq_map_conv)
            (metis event⇩_p⇩_t⇩_i⇩_c⇩_k.disc(1) event⇩_p⇩_t⇩_i⇩_c⇩_k.sel(1) tickFree_Cons_iff)
      next
        case F_Q thus ‹(t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)›
          by (simp add: denot_projs "$" initial_P Cons_eq_append_conv Cons_eq_map_conv)
            (metis append_Cons event⇩_p⇩_t⇩_i⇩_c⇩_k.disc(1) event⇩_p⇩_t⇩_i⇩_c⇩_k.sel(1) tickFree_Cons_iff)
      qed
    qed
  qed
qed


lemma skippable_not_initialL_After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹(P ❙;⇩_✓ Q) after⇩_β a = (  if (∃r. ✓(r) ∈ P⇧⁰ ∧ ev a ∈ (Q r)⇧⁰)
                       then ⊓r∈{r. ✓(r) ∈ P⇧⁰ ∧ ev a ∈ (Q r)⇧⁰}. Q r after⇩_β a
                       else Ψ⇩_β (P ❙;⇩_✓ Q) a)›
  (is ‹(P ❙;⇩_✓ Q) after⇩_β a = (if ?prem then ?rhs else _)›) if ‹ev a ∉ P⇧⁰›
proof -
  note denot_projs = After.After_projs Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs GlobalNdet_projs
  from initials_BOT ‹ev a ∉ P⇧⁰› have non_BOT : ‹P ≠ ⊥› by blast
  with ‹ev a ∉ P⇧⁰› have $ : ‹ev a ∈ (P ❙;⇩_✓ Q)⇧⁰ ⟷ ?prem›
    by (auto simp add: initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k)
  show ‹(P ❙;⇩_✓ Q) after⇩_β a = (if ?prem then ?rhs else Ψ⇩_β (P ❙;⇩_✓ Q) a)›
  proof (split if_split, intro conjI impI)
    show ‹¬ ?prem ⟹ (P ❙;⇩_✓ Q) after⇩_β a = Ψ⇩_β (P ❙;⇩_✓ Q) a›
      by (rule After⇩_β.not_initial_After, use "$" in blast)
  next
    show ‹(P ❙;⇩_✓ Q) after⇩_β a = ?rhs› if ?prem
    proof (rule Process_eq_optimizedI)
      fix t assume ‹t ∈ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)›
      then consider (D_P) t' u where ‹ev a # t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
        | (D_Q) t' r u where ‹ev a # t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹u ∈ 𝒟 (Q r)›
        by (auto simp add: denot_projs ‹?prem› "$" ‹ev a ∉ P⇧⁰›)
      thus ‹t ∈ 𝒟 ?rhs›
      proof cases
        case D_P with non_BOT ‹ev a ∉ P⇧⁰› show ‹t ∈ 𝒟 ?rhs›
          by (simp add: denot_projs Cons_eq_append_conv Cons_eq_map_conv BOT_iff_Nil_D)
            (metis D_T event⇩_p⇩_t⇩_i⇩_c⇩_k.collapse(1) initials_memI tickFree_Cons_iff)
      next
        case D_Q with ‹ev a ∉ P⇧⁰› show ‹t ∈ 𝒟 ?rhs›
          by (simp add: denot_projs Cons_eq_append_conv Cons_eq_map_conv)
            (metis D_T append_Nil event⇩_p⇩_t⇩_i⇩_c⇩_k.collapse(1) initials_memI
              is_processT3_TR_append tickFree_Cons_iff)
      qed
    next
      from ‹?prem› show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)› for t
        by (simp add: denot_projs "$" Cons_eq_append_conv)
          (metis append_Nil initials_memD tickFree_Nil)
    next
      fix t X assume ‹(t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)› ‹t ∉ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)›
      then consider (F_P) t' where ‹ev a # t = map (ev ∘ of_ev) t'›
        ‹(t', ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ P› ‹tF t'›
      | (F_Q) t' r u where ‹ev a # t = map (ev ∘ of_ev) t' @ u›
        ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹(u, X) ∈ ℱ (Q r)›
        by (simp add: denot_projs "$" ‹?prem›) metis
      thus ‹(t, X) ∈ ℱ ?rhs›
      proof cases
        case F_P with ‹ev a ∉ P⇧⁰› show ‹(t, X) ∈ ℱ ?rhs›
          by (cases t', simp_all add: denot_projs ‹?prem›)
            (use F_T initials_memI in blast)
      next
        case F_Q with ‹ev a ∉ P⇧⁰› ‹?prem› show ‹(t, X) ∈ ℱ ?rhs›
          by (cases t', auto simp add: denot_projs intro: initials_memI)
            (metis F_T initials_memI)
      qed
    next
      from ‹?prem› show ‹(t, X) ∈ ℱ ?rhs ⟹ t ∉ 𝒟 ?rhs ⟹
                         (t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)› for t X
        by (simp add: denot_projs "$" Cons_eq_append_conv Cons_eq_map_conv split: if_split_asm)
          (metis initials_memD self_append_conv2 tickFree_Nil)
    qed
  qed
qed



lemma skippable_initialL_initialR_After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹(P ❙;⇩_✓ Q) after⇩_β a = (P after⇩_α a ❙;⇩_✓ Q) ⊓ (⊓r∈{r. ✓(r) ∈ P⇧⁰ ∧ ev a ∈ (Q r)⇧⁰}. Q r after⇩_β a)›
  (is ‹(P ❙;⇩_✓ Q) after⇩_β a = (P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs›)
  if assms : ‹∃r. ✓(r) ∈ P⇧⁰ ∧ ev a ∈ (Q r)⇧⁰› ‹ev a ∈ P⇧⁰›
proof (cases ‹P = ⊥›)
  show ‹P = ⊥ ⟹ (P ❙;⇩_✓ Q) after⇩_β a = (P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs›
    by (simp add: After.After_BOT)
next
  note denot_projs = After.After_projs Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs GlobalNdet_projs Ndet_projs
  show ‹(P ❙;⇩_✓ Q) after⇩_β a = (P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs› if ‹P ≠ ⊥›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)›
    then consider (D_P) t' u where ‹ev a # t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
      | (D_Q) t' r u where ‹ev a # t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹u ∈ 𝒟 (Q r)›
      by (auto simp add: denot_projs initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k assms split: if_split_asm)
    thus ‹t ∈ 𝒟 ((P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs)›
    proof cases
      case D_P with ‹P ≠ ⊥› show ‹t ∈ 𝒟 ((P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs)›
        by (auto simp add: denot_projs assms Cons_eq_append_conv BOT_iff_Nil_D)
    next
      case D_Q thus ‹t ∈ 𝒟 ((P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs)›
        by (auto simp add: denot_projs assms Cons_eq_append_conv)
          (meson D_T initials_memI, blast)
    qed
  next
    from ‹P ≠ ⊥› show ‹t ∈ 𝒟 ((P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs) ⟹ t ∈ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)› for t
      by (auto simp add: denot_projs assms initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k Cons_eq_append_conv Cons_eq_map_conv)
        (metis event⇩_p⇩_t⇩_i⇩_c⇩_k.disc(1) event⇩_p⇩_t⇩_i⇩_c⇩_k.sel(1) tickFree_Cons_iff,
          metis Cons_eq_appendI append_T_imp_tickFree event⇩_p⇩_t⇩_i⇩_c⇩_k.sel(1) list.distinct(1),
          metis append_Nil initials_memD tickFree_Nil)
  next
    fix t X assume ‹(t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)› ‹t ∉ 𝒟 ((P ❙;⇩_✓ Q) after⇩_β a)›
    then consider (F_P) t' where ‹ev a # t = map (ev ∘ of_ev) t'›
      ‹(t', ref_Seq⇩_p⇩_t⇩_i⇩_c⇩_k X) ∈ ℱ P› ‹tF t'›
    | (F_Q) t' r u where ‹ev a # t = map (ev ∘ of_ev) t' @ u›
      ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹(u, X) ∈ ℱ (Q r)›
      by (simp add: denot_projs assms initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k split: if_split_asm) meson+
    thus ‹(t, X) ∈ ℱ ((P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs)›
    proof cases
      case F_P thus ‹(t, X) ∈ ℱ ((P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs)›
        by (auto simp add: denot_projs assms)
    next
      case F_Q with assms show ‹(t, X) ∈ ℱ ((P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs)›
        by (cases t', simp_all add: denot_projs)
          (meson F_T initials_memI, blast)
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ((P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs)› ‹t ∉ 𝒟 ((P after⇩_α a ❙;⇩_✓ Q) ⊓ ?rhs)›
    hence ‹(t, X) ∈ ℱ (P after⇩_α a ❙;⇩_✓ Q) ∧ t ∉ 𝒟 (P after⇩_α a ❙;⇩_✓ Q) ∨
           (t, X) ∈ ℱ ?rhs ∧ t ∉ 𝒟 ?rhs› by (simp add: Ndet_projs)
    thus ‹(t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)›
    proof (elim disjE conjE)
      show ‹(t, X) ∈ ℱ (P after⇩_α a ❙;⇩_✓ Q) ⟹ t ∉ 𝒟 (P after⇩_α a ❙;⇩_✓ Q) ⟹
            (t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)›
        by (simp add: denot_projs assms initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k ‹P ≠ ⊥› Cons_eq_append_conv Cons_eq_map_conv)
          (metis (no_types, lifting) Cons_eq_appendI event⇩_p⇩_t⇩_i⇩_c⇩_k.sel(1) is_ev_def tickFree_Cons_iff)
    next
      from assms show ‹(t, X) ∈ ℱ ?rhs ⟹ t ∉ 𝒟 ?rhs ⟹ (t, X) ∈ ℱ ((P ❙;⇩_✓ Q) after⇩_β a)›
        by (simp add: denot_projs initials_Seq⇩_p⇩_t⇩_i⇩_c⇩_k ‹P ≠ ⊥›
            Cons_eq_append_conv Cons_eq_map_conv split: if_split_asm)
          (metis append_Nil initials_memD tickFree_Nil)
    qed
  qed
qed


lemma not_initialL_not_initialR_After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹ev a ∉ P⇧⁰ ⟹ (⋀r. ✓(r) ∈ P⇧⁰ ⟹ ev a ∉ (Q r)⇧⁰) ⟹ 
   (P ❙;⇩_✓ Q) after⇩_β a = Ψ⇩_β (P ❙;⇩_✓ Q) a›
  by (meson skippable_not_initialL_After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k)


lemma After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹(P ❙;⇩_✓ Q) after⇩_β a =
   (  if ∀r. ✓(r) ∈ P⇧⁰ ⟶ ev a ∉ (Q r)⇧⁰
    then   if ev a ∈ P⇧⁰ then P after⇩_α a ❙;⇩_✓ Q else Ψ⇩_β (P ❙;⇩_✓ Q) a
    else   if ev a ∈ P⇧⁰
         then (P after⇩_α a ❙;⇩_✓ Q) ⊓ (⊓r∈{r. ✓(r) ∈ P⇧⁰ ∧ ev a ∈ (Q r)⇧⁰}. Q r after⇩_β a)
         else ⊓r∈{r. ✓(r) ∈ P⇧⁰ ∧ ev a ∈ (Q r)⇧⁰}. Q r after⇩_β a)›
  by (simp add: not_skippable_or_not_initialR_After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k
      skippable_initialL_initialR_After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k skippable_not_initialL_After_Seq⇩_p⇩_t⇩_i⇩_c⇩_k)

end



subsection ‹Synchronization Product›

text ‹Because of the types, we have to extend the ⬚‹locale›.›

locale After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_locale = Sync⇩_p⇩_t⇩_i⇩_c⇩_k_locale tick_join +
  After⇩_l⇩_h⇩_s : After Ψ⇩_l⇩_h⇩_s + After⇩_r⇩_h⇩_s : After Ψ⇩_r⇩_h⇩_s + After⇩_p⇩_t⇩_i⇩_c⇩_k : After Ψ⇩_p⇩_t⇩_i⇩_c⇩_k
  for tick_join :: ‹'r ⇒ 's ⇒ 't option›
    and Ψ⇩_l⇩_h⇩_s :: ‹[('a, 'r) process⇩_p⇩_t⇩_i⇩_c⇩_k, 'a] ⇒ ('a, 'r) process⇩_p⇩_t⇩_i⇩_c⇩_k›
    and Ψ⇩_r⇩_h⇩_s :: ‹[('a, 's) process⇩_p⇩_t⇩_i⇩_c⇩_k, 'a] ⇒ ('a, 's) process⇩_p⇩_t⇩_i⇩_c⇩_k›
    and Ψ⇩_p⇩_t⇩_i⇩_c⇩_k :: ‹[('a, 't) process⇩_p⇩_t⇩_i⇩_c⇩_k, 'a] ⇒ ('a, 't) process⇩_p⇩_t⇩_i⇩_c⇩_k›
begin

notation After⇩_l⇩_h⇩_s.After (infixl ‹after⇩_l⇩_h⇩_s› 86)
notation After⇩_r⇩_h⇩_s.After (infixl ‹after⇩_r⇩_h⇩_s› 86)
notation After⇩_p⇩_t⇩_i⇩_c⇩_k.After (infixl ‹after⇩_p⇩_t⇩_i⇩_c⇩_k› 86)

sublocale After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_locale_sym :
  After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_locale ‹λs r. tick_join r s› Ψ⇩_r⇩_h⇩_s Ψ⇩_l⇩_h⇩_s Ψ⇩_p⇩_t⇩_i⇩_c⇩_k
  by unfold_locales



lemma initialL_not_initialR_not_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹(P ⟦S⟧⇩_✓ Q) after⇩_p⇩_t⇩_i⇩_c⇩_k a = P after⇩_l⇩_h⇩_s a ⟦S⟧⇩_✓ Q› (is ‹?lhs = ?rhs›)
  if initial_hyps: ‹ev a ∈ P⇧⁰› ‹ev a ∉ Q⇧⁰› and notin: ‹a ∉ S›
proof (cases ‹P = ⊥ ∨ Q = ⊥›)
  show ‹P = ⊥ ∨ Q = ⊥ ⟹ ?lhs = ?rhs›
    by (elim disjE) (simp_all add: After⇩_p⇩_t⇩_i⇩_c⇩_k.After_BOT After⇩_l⇩_h⇩_s.After_BOT)
next
  from initial_hyps and notin have init : ‹ev a ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
    by (simp add: initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
  show ‹?lhs = ?rhs› if non_BOT : ‹¬ (P = ⊥ ∨ Q = ⊥)›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    with init have ‹ev a # t ∈ 𝒟 (P ⟦S⟧⇩_✓ Q)› by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.D_After)
    then obtain u v t_P t_Q
      where * : ‹ev a # t = u @ v› ‹tF u› ‹ftF v›
        ‹u setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
    from "*"(4, 5) non_BOT have ‹u ≠ []›
      by (auto simp add: BOT_iff_Nil_D dest: Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k)
    with "*"(1) obtain u' where ‹u = ev a # u'› ‹t = u' @ v›
      by (cases u) simp_all
    from "*"(4, 5) initial_hyps(2) obtain t_P'
      where ‹t_P = ev a # t_P'› ‹u' setinterleaves⇩_✓⇘tick_join⇙ ((t_P', t_Q), S)›
      by (cases t_P; cases t_Q)
        (auto simp add: setinterleaving⇩_p⇩_t⇩_i⇩_c⇩_k_simps ‹u = ev a # u'›
          split: event⇩_p⇩_t⇩_i⇩_c⇩_k.splits if_split_asm option.split_asm
          intro: D_T initials_memI)
    moreover from ‹t_P = ev a # t_P'› "*"(2, 5)
    have ‹t_P' ∈ 𝒟 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒯 Q ∨
          t_P' ∈ 𝒯 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒟 Q›
      by (simp add: After⇩_l⇩_h⇩_s.After_projs initial_hyps(1))
    moreover from "*"(2) have ‹tF u'› by (simp add: ‹u = ev a # u'›)
    ultimately show ‹t ∈ 𝒟 ?rhs›
      using "*"(3) by (auto simp add: ‹t = u' @ v› D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then obtain u v t_P t_Q
      where * : ‹t = u @ v› ‹tF u› ‹ftF v›
        ‹u setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹t_P ∈ 𝒟 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒯 Q ∨
         t_P ∈ 𝒯 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒟 Q›
      unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
    have ‹ev a # t = (ev a # u) @ v› by (simp add: "*"(1))
    moreover from "*"(2) have ‹tF (ev a # u)› by simp
    moreover from "*"(4)
    have ‹ev a # u setinterleaves⇩_✓⇘tick_join⇙ ((ev a # t_P, t_Q), S)›
      by (metis notin rev.simps(2) rev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_rev_rev_iff
          setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_snoc_notinL)
    moreover from "*"(5) have ‹ev a # t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨
                               ev a # t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      by (simp add: After⇩_l⇩_h⇩_s.After_projs initial_hyps(1))
    ultimately have ‹ev a # t ∈ 𝒟 (P ⟦S⟧⇩_✓ Q)›
      using "*"(3) unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
    thus ‹t ∈ 𝒟 ?lhs›
      by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.D_After init)
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs›
      ‹t ∉ 𝒟 ?lhs›
    hence ‹(ev a # t, X) ∈ ℱ (P ⟦S⟧⇩_✓ Q)› ‹ev a # t ∉ 𝒟 (P ⟦S⟧⇩_✓ Q)›
      by (simp_all add: After⇩_p⇩_t⇩_i⇩_c⇩_k.After_projs init)
    then obtain t_P t_Q X_P X_Q
      where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹ev a # t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P S X_Q›
      unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
    from "*"(2, 3) initial_hyps(2) obtain t_P'
      where ‹t_P = ev a # t_P'› ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P', t_Q), S)›
      by (metis Cons_ev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE F_T initials_memI)
    moreover from "*"(1) have ‹(t_P', X_P) ∈ ℱ (P after⇩_l⇩_h⇩_s a)›
      by (simp add: ‹t_P = ev a # t_P'› After⇩_l⇩_h⇩_s.F_After initial_hyps(1))
    ultimately show ‹(t, X) ∈ ℱ ?rhs›
      using "*"(2, 4) by (auto simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
  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 after⇩_l⇩_h⇩_s a)› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P S X_Q›
      unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
    from "*"(1) have ‹(ev a # t_P, X_P) ∈ ℱ P›
      by (simp add: After⇩_l⇩_h⇩_s.F_After initial_hyps(1))
    moreover from "*"(3)
    have ‹ev a # t setinterleaves⇩_✓⇘tick_join⇙ ((ev a # t_P, t_Q), S)›
      by (metis notin rev.simps(2) rev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_rev_rev_iff
          setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_snoc_notinL)
    ultimately have ‹(ev a # t, X) ∈ ℱ (P ⟦S⟧⇩_✓ Q)›
      using "*"(2, 4) by (auto simp add: F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
    thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.F_After init)
  qed
qed


lemma (in After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_locale) not_initialL_initialR_not_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹(P ⟦S⟧⇩_✓ Q) after⇩_p⇩_t⇩_i⇩_c⇩_k a = P ⟦S⟧⇩_✓ Q after⇩_r⇩_h⇩_s a› (is ‹?lhs = ?rhs›)
  if initial_hyps: ‹ev a ∉ P⇧⁰› ‹ev a ∈ Q⇧⁰› and notin: ‹a ∉ S›
  using After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_locale_sym.initialL_not_initialR_not_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k
    [OF ‹ev a ∈ Q⇧⁰› ‹ev a ∉ P⇧⁰› ‹a ∉ S›]
  by (simp add: Sync⇩_p⇩_t⇩_i⇩_c⇩_k_sym)


lemma not_initialL_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹ev a ∉ P⇧⁰ ⟹ a ∈ S ⟹ 
   (P ⟦S⟧⇩_✓ Q) after⇩_p⇩_t⇩_i⇩_c⇩_k a = (if Q = ⊥ then ⊥ else Ψ⇩_p⇩_t⇩_i⇩_c⇩_k (P ⟦S⟧⇩_✓ Q) a)›
  by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.After_BOT, rule impI)
    (subst After⇩_p⇩_t⇩_i⇩_c⇩_k.not_initial_After, auto simp add: initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)

lemma not_initialR_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹ev a ∉ Q⇧⁰ ⟹ a ∈ S ⟹ 
   (P ⟦S⟧⇩_✓ Q) after⇩_p⇩_t⇩_i⇩_c⇩_k a = (if P = ⊥ then ⊥ else Ψ⇩_p⇩_t⇩_i⇩_c⇩_k (P ⟦S⟧⇩_✓ Q) a)›
  by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.After_BOT, rule impI)
    (subst After⇩_p⇩_t⇩_i⇩_c⇩_k.not_initial_After, auto simp add: initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)


lemma initialL_initialR_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k:
  ‹(P ⟦S⟧⇩_✓ Q) after⇩_p⇩_t⇩_i⇩_c⇩_k a = P after⇩_l⇩_h⇩_s a ⟦S⟧⇩_✓ Q after⇩_r⇩_h⇩_s a› (is ‹?lhs = ?rhs›)
  if initial_hyps: ‹ev a ∈ P⇧⁰› ‹ev a ∈ Q⇧⁰› and inside: ‹a ∈ S›
proof (cases ‹P = ⊥ ∨ Q = ⊥›)
  show ‹P = ⊥ ∨ Q = ⊥ ⟹ ?lhs = ?rhs›
    by (elim disjE) (simp_all add: After.After_BOT)
next
  from initial_hyps inside have init : ‹ev a ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
    by (simp add: initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
  show ‹?lhs = ?rhs› if non_BOT : ‹¬ (P = ⊥ ∨ Q = ⊥)›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ((P ⟦S⟧⇩_✓ Q) after⇩_p⇩_t⇩_i⇩_c⇩_k a)›
    hence ‹ev a # t ∈ 𝒟 (P ⟦S⟧⇩_✓ Q)› by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.D_After init)
    then obtain u v t_P t_Q
      where * : ‹ev a # t = u @ v› ‹tF u› ‹ftF v›
        ‹u setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
    from "*"(4, 5) non_BOT have ‹u ≠ []›
      by (auto simp add: BOT_iff_Nil_D dest: Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k)
    with "*"(1) obtain u' where ‹u = ev a # u'› ‹t = u' @ v›
      by (cases u) simp_all
    from "*"(4) inside initial_hyps(1, 2) ‹u = ev a # u'›
    obtain t_P' t_Q' where ‹t_P = ev a # t_P'› ‹t_Q = ev a # t_Q'›
      ‹u' setinterleaves⇩_✓⇘tick_join⇙ ((t_P', t_Q'), S)›
      by (metis (no_types, opaque_lifting) Cons_ev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE)
    moreover from "*"(2) have ‹tF u'› by (simp add: ‹u = ev a # u'›)
    moreover from "*"(5)
    have ‹t_P' ∈ 𝒟 (P after⇩_l⇩_h⇩_s a) ∧ t_Q' ∈ 𝒯 (Q after⇩_r⇩_h⇩_s a) ∨
          t_P' ∈ 𝒯 (P after⇩_l⇩_h⇩_s a) ∧ t_Q' ∈ 𝒟 (Q after⇩_r⇩_h⇩_s a)›
      by (simp add: ‹t_P = ev a # t_P'› ‹t_Q = ev a # t_Q'›
          After.After_projs initial_hyps)
    ultimately show ‹t ∈ 𝒟 ?rhs›
      using "*"(3) by (auto simp add: ‹t = u' @ v› D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then obtain u v t_P t_Q
      where * : ‹t = u @ v› ‹tF u› ‹ftF v›
        ‹u setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹t_P ∈ 𝒟 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒯 (Q after⇩_r⇩_h⇩_s a) ∨
                 t_P ∈ 𝒯 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒟 (Q after⇩_r⇩_h⇩_s a)›
      unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
    from "*"(1) have ‹ev a # t = (ev a # u) @ v› by simp
    moreover from "*"(2) have ‹tF (ev a # u)› by simp
    moreover from "*"(4) have ‹ev a # u setinterleaves⇩_✓⇘tick_join⇙
                               ((ev a # t_P, ev a # t_Q), S)›
      by (simp add: inside)
    moreover from "*"(5) have ‹ev a # t_P ∈ 𝒟 P ∧ ev a # t_Q ∈ 𝒯 Q ∨
                               ev a # t_P ∈ 𝒯 P ∧ ev a # t_Q ∈ 𝒟 Q›
      by (simp add: After.After_projs initial_hyps)
    ultimately have ‹ev a # t ∈ 𝒟 (P ⟦S⟧⇩_✓ Q)›
      unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k using "*"(3) by blast
    thus ‹t ∈ 𝒟 ?lhs› by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.D_After init)
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
    hence ‹(ev a # t, X) ∈ ℱ (P ⟦S⟧⇩_✓ Q)› ‹ev a # t ∉ 𝒟 (P ⟦S⟧⇩_✓ Q)›
      by (simp_all add: After.After_projs init)
    then obtain t_P t_Q X_P X_Q
      where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹ev a # t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P S X_Q›
      unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
    from "*"(3) obtain t_P' t_Q'
      where ‹t_P = ev a # t_P'› ‹t_Q = ev a # t_Q'›
        ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P', t_Q'), S)›
      by (metis (no_types) Cons_ev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE inside)
    moreover from "*"(1, 2) have ‹(t_P', X_P) ∈ ℱ (P after⇩_l⇩_h⇩_s a)›
      ‹(t_Q', X_Q) ∈ ℱ (Q after⇩_r⇩_h⇩_s a)›
      by (simp_all add: ‹t_P = ev a # t_P'› ‹t_Q = ev a # t_Q'› 
          After.F_After initial_hyps)
    ultimately show ‹(t, X) ∈ ℱ ?rhs›
      by (auto simp add: F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k intro!: "*"(4))
  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 after⇩_l⇩_h⇩_s a)›
        ‹(t_Q, X_Q) ∈ ℱ (Q after⇩_r⇩_h⇩_s a)›
        ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P S X_Q›
      unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
    from "*"(1, 2) have ‹(ev a # t_P, X_P) ∈ ℱ P›
      ‹(ev a # t_Q, X_Q) ∈ ℱ Q›
      by (simp_all add: After.F_After initial_hyps)
    moreover from "*"(3) have ‹ev a # t setinterleaves⇩_✓⇘tick_join⇙
                               ((ev a # t_P, ev a # t_Q), S)›
      by (simp add: inside)
    ultimately have ‹(ev a # t, X) ∈ ℱ (P ⟦S⟧⇩_✓ Q)›
      using "*"(4) by (simp (no_asm) add: F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) blast
    thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.F_After init)
  qed
qed



lemma initialL_initialR_not_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k: 
  ‹(P ⟦S⟧⇩_✓ Q) after⇩_p⇩_t⇩_i⇩_c⇩_k a = (P after⇩_l⇩_h⇩_s a ⟦S⟧⇩_✓ Q) ⊓ (P ⟦S⟧⇩_✓ Q after⇩_r⇩_h⇩_s a)›
  (is ‹?lhs = ?rhs1 ⊓ ?rhs2›)
  if initial_hyps: ‹ev a ∈ P⇧⁰› ‹ev a ∈ Q⇧⁰› and notin: ‹a ∉ S›
proof (cases ‹P = ⊥ ∨ Q = ⊥›)
  show ‹P = ⊥ ∨ Q = ⊥ ⟹ ?lhs = ?rhs1 ⊓ ?rhs2›
    by (elim disjE) (simp_all add: After.After_BOT)
next
  from initial_hyps(1) notin have init : ‹ev a ∈ (P ⟦S⟧⇩_✓ Q)⇧⁰›
    by (simp add: initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
  show ‹?lhs = ?rhs1 ⊓ ?rhs2› if non_BOT : ‹¬ (P = ⊥ ∨ Q = ⊥)›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    hence ‹ev a # t ∈ 𝒟 (P ⟦S⟧⇩_✓ Q)›
      by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.D_After init)
    then obtain u v t_P t_Q
      where * : ‹ev a # t = u @ v› ‹tF u› ‹ftF v›
        ‹u setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
    from "*"(4, 5) non_BOT have ‹u ≠ []›
      by (auto simp add: BOT_iff_Nil_D dest: Nil_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k)
    with "*"(1) obtain u' where ‹u = ev a # u'› ‹t = u' @ v›
      by (cases u) simp_all
    from "*"(2) have ‹tF u'› by (simp add: ‹u = ev a # u'›)
    from "*"(4) notin ‹u = ev a # u'›
    consider t_P' where ‹t_P = ev a # t_P'›
      ‹u' setinterleaves⇩_✓⇘tick_join⇙ ((t_P', t_Q), S)›
    | t_Q' where ‹t_Q = ev a # t_Q'›
      ‹u' setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q'), S)›
      by (metis (no_types) Cons_ev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE)
    thus ‹t ∈ 𝒟 (?rhs1 ⊓ ?rhs2)›
    proof cases
      fix t_P' assume $ : ‹t_P = ev a # t_P'›
        ‹u' setinterleaves⇩_✓⇘tick_join⇙ ((t_P', t_Q), S)›
      from "*"(5) have ‹t_P' ∈ 𝒟 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒯 Q ∨
                        t_P' ∈ 𝒯 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒟 Q›
        by (simp add: "$"(1) After⇩_l⇩_h⇩_s.After_projs initial_hyps(1))
      with "$"(2) "*"(3) ‹tF u'› have ‹t ∈ 𝒟 ?rhs1›
        by (auto simp add: ‹t = u' @ v› D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
      thus ‹t ∈ 𝒟 (?rhs1 ⊓ ?rhs2)› by (simp add: D_Ndet)
    next
      fix t_Q' assume $ : ‹t_Q = ev a # t_Q'›
        ‹u' setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q'), S)›
      from "*"(5) have ‹t_P ∈ 𝒟 P ∧ t_Q' ∈ 𝒯 (Q after⇩_r⇩_h⇩_s a) ∨
                        t_P ∈ 𝒯 P ∧ t_Q' ∈ 𝒟 (Q after⇩_r⇩_h⇩_s a)›
        by (simp add: "$"(1) After⇩_r⇩_h⇩_s.After_projs initial_hyps(2))
      with "$"(2) "*"(3) ‹tF u'› have ‹t ∈ 𝒟 ?rhs2›
        by (auto simp add: ‹t = u' @ v› D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
      thus ‹t ∈ 𝒟 (?rhs1 ⊓ ?rhs2)› by (simp add: D_Ndet)
    qed
  next
    fix t assume ‹t ∈ 𝒟 (?rhs1 ⊓ ?rhs2)›
    then consider ‹t ∈ 𝒟 ?rhs1› | ‹t ∈ 𝒟 ?rhs2›
      by (auto simp add: D_Ndet)
    hence ‹ev a # t ∈ 𝒟 (P ⟦S⟧⇩_✓ Q)›
    proof cases
      assume ‹t ∈ 𝒟 ?rhs1›
      then obtain u v t_P t_Q
        where * : ‹t = u @ v› ‹tF u› ‹ftF v›
          ‹u setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
          ‹t_P ∈ 𝒟 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒯 Q ∨
                   t_P ∈ 𝒯 (P after⇩_l⇩_h⇩_s a) ∧ t_Q ∈ 𝒟 Q›
        unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
      from "*"(1) have ‹ev a # t = (ev a # u) @ v› by simp
      moreover from "*"(2) have ‹tF (ev a # u)› by simp
      moreover from "*"(4)
      have ‹ev a # u setinterleaves⇩_✓⇘tick_join⇙ ((ev a # t_P, t_Q), S)›
        by (metis notin rev.simps(2) rev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_rev_rev_iff
            setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_snoc_notinL)
      moreover from "*"(5) have ‹ev a # t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨
                                 ev a # t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
        by (simp add: After⇩_l⇩_h⇩_s.After_projs initial_hyps(1))
      ultimately show ‹ev a # t ∈ 𝒟 (P ⟦S⟧⇩_✓ Q)›
        using "*"(3) unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
    next
      assume ‹t ∈ 𝒟 ?rhs2›
      then obtain u v t_P t_Q
        where * : ‹t = u @ v› ‹tF u› ‹ftF v›
          ‹u setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
          ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 (Q after⇩_r⇩_h⇩_s a) ∨
                   t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 (Q after⇩_r⇩_h⇩_s a)›
        unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
      from "*"(1) have ‹ev a # t = (ev a # u) @ v› by simp
      moreover from "*"(2) have ‹tF (ev a # u)› by simp
      moreover from "*"(4) have ‹ev a # u setinterleaves⇩_✓⇘tick_join⇙ ((t_P, ev a # t_Q), S)›
        by (metis notin rev.simps(2) rev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_rev_rev_iff
            setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_snoc_notinR)
      moreover from "*"(5) have ‹t_P ∈ 𝒟 P ∧ ev a # t_Q ∈ 𝒯 Q ∨
                                 t_P ∈ 𝒯 P ∧ ev a # t_Q ∈ 𝒟 Q›
        by (simp add: After⇩_r⇩_h⇩_s.After_projs initial_hyps(2))
      ultimately show ‹ev a # t ∈ 𝒟 (P ⟦S⟧⇩_✓ Q)›
        using "*"(3) unfolding D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k by blast
    qed
    thus ‹t ∈ 𝒟 ?lhs› by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.D_After init)
  next  
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
    hence ‹(ev a # t, X) ∈ ℱ (P ⟦S⟧⇩_✓ Q)› ‹ev a # t ∉ 𝒟 (P ⟦S⟧⇩_✓ Q)›
      by (simp_all add: After⇩_p⇩_t⇩_i⇩_c⇩_k.After_projs init)
    then obtain t_P t_Q X_P X_Q
      where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹ev a # t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P S X_Q›
      unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
    from "*"(3) notin
    consider t_P' where ‹t_P = ev a # t_P'›
      ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P', t_Q), S)›
    | t_Q' where ‹t_Q = ev a # t_Q'›
      ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q'), S)›
      by (metis (no_types) Cons_ev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_kE)
    thus ‹(t, X) ∈ ℱ (?rhs1 ⊓ ?rhs2)›
    proof cases
      fix t_P' assume $ : ‹t_P = ev a # t_P'›
        ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P', t_Q), S)›
      from "*"(1) have ‹(t_P', X_P) ∈ ℱ (P after⇩_l⇩_h⇩_s a)›
        by (simp add: "$"(1) After⇩_l⇩_h⇩_s.F_After initial_hyps(1))
      with "$"(2) "*"(2, 4) have ‹(t, X) ∈ ℱ ?rhs1›
        by (auto simp add: F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
      thus ‹(t, X) ∈ ℱ (?rhs1 ⊓ ?rhs2)› by (simp add: F_Ndet)
    next
      fix t_Q' assume $ : ‹t_Q = ev a # t_Q'›
        ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q'), S)›
      from "*"(2) have ‹(t_Q', X_Q) ∈ ℱ (Q after⇩_r⇩_h⇩_s a)›
        by (simp add: "$"(1) After⇩_r⇩_h⇩_s.F_After initial_hyps(2))
      with "$"(2) "*"(1, 4) have ‹(t, X) ∈ ℱ ?rhs2›
        by (auto simp add: F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
      thus ‹(t, X) ∈ ℱ (?rhs1 ⊓ ?rhs2)› by (simp add: F_Ndet)
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ (?rhs1 ⊓ ?rhs2)› ‹t ∉ 𝒟 (?rhs1 ⊓ ?rhs2)›
    then consider ‹(t, X) ∈ ℱ ?rhs1› ‹t ∉ 𝒟 ?rhs1›
      | ‹(t, X) ∈ ℱ ?rhs2› ‹t ∉ 𝒟 ?rhs2›
      by (auto simp add: Ndet_projs)
    hence ‹(ev a # t, X) ∈ ℱ (P ⟦S⟧⇩_✓ Q)›
    proof cases
      assume ‹(t, X) ∈ ℱ ?rhs1› ‹t ∉ 𝒟 ?rhs1›
      then obtain t_P t_Q X_P X_Q
        where * : ‹(t_P, X_P) ∈ ℱ (P after⇩_l⇩_h⇩_s a)› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
          ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P S X_Q›
        unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
      from "*"(1) have ‹(ev a # t_P, X_P) ∈ ℱ P›
        by (simp add: After⇩_l⇩_h⇩_s.F_After initial_hyps(1))
      moreover from "*"(3)
      have ‹ev a # t setinterleaves⇩_✓⇘tick_join⇙ ((ev a # t_P, t_Q), S)›
        by (metis notin rev.simps(2) rev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_rev_rev_iff
            setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_snoc_notinL)
      ultimately show ‹(ev a # t, X) ∈ ℱ (P ⟦S⟧⇩_✓ Q)›
        by (auto simp add: F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k intro!: "*"(2, 4))
    next
      assume ‹(t, X) ∈ ℱ ?rhs2› ‹t ∉ 𝒟 ?rhs2›
      then obtain t_P t_Q X_P X_Q
        where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ (Q after⇩_r⇩_h⇩_s a)›
          ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
          ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P S X_Q›
        unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
      from "*"(2) have ‹(ev a # t_Q, X_Q) ∈ ℱ Q›
        by (simp add: After⇩_r⇩_h⇩_s.F_After initial_hyps(2))
      moreover from "*"(3)
      have ‹ev a # t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, ev a # t_Q), S)›
        by (metis notin rev.simps(2) rev_setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_rev_rev_iff
            setinterleaves⇩_p⇩_t⇩_i⇩_c⇩_k_snoc_notinR)
      ultimately show ‹(ev a # t, X) ∈ ℱ (P ⟦S⟧⇩_✓ Q)›
        by (auto simp add: F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k intro!: "*"(1, 4))
    qed
    thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.F_After init)
  qed
qed



lemma not_initialL_not_initialR_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹ev a ∉ P⇧⁰ ⟹ ev a ∉ Q⇧⁰ ⟹ (P ⟦S⟧⇩_✓ Q) after⇩_p⇩_t⇩_i⇩_c⇩_k a = Ψ⇩_p⇩_t⇩_i⇩_c⇩_k (P ⟦S⟧⇩_✓ Q) a›
  by (subst After⇩_p⇩_t⇩_i⇩_c⇩_k.not_initial_After) (auto simp add: initials_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)



text ‹Finally, the monster theorem !›

theorem After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k: 
  ‹(P ⟦S⟧⇩_✓ Q) after⇩_p⇩_t⇩_i⇩_c⇩_k a =
   (  if P = ⊥ ∨ Q = ⊥ then ⊥
    else   if ev a ∈ P⇧⁰ ∧ ev a ∈ Q⇧⁰
         then   if a ∈ S then P after⇩_l⇩_h⇩_s a ⟦S⟧⇩_✓ Q after⇩_r⇩_h⇩_s a
              else (P after⇩_l⇩_h⇩_s a ⟦S⟧⇩_✓ Q) ⊓ (P ⟦S⟧⇩_✓ Q after⇩_r⇩_h⇩_s a)
         else   if ev a ∈ P⇧⁰ ∧ a ∉ S then P after⇩_l⇩_h⇩_s a ⟦S⟧⇩_✓ Q
              else   if ev a ∈ Q⇧⁰ ∧ a ∉ S then P ⟦S⟧⇩_✓ Q after⇩_r⇩_h⇩_s a
                   else Ψ⇩_p⇩_t⇩_i⇩_c⇩_k (P ⟦S⟧⇩_✓ Q) a)›
  by (auto simp add: After⇩_p⇩_t⇩_i⇩_c⇩_k.After_BOT initialL_not_initialR_not_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k
      initialL_initialR_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k initialL_initialR_not_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k
      not_initialL_initialR_not_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k not_initialL_not_initialR_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k
      not_initialR_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k not_initialL_in_After_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)


end


(*<*)
end
  (*>*)