Theory Basic_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 ‹First Laws›

(*<*)
theory Basic_CSP_PTick_Laws
  imports Sequential_Composition_Generalized CSP_PTick_Renaming Finite_Ticks
begin
  (*>*)

unbundle option_type_syntax


section ‹Behaviour with Constant Processes›

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


lemma Seqptick_const [simp] : ‹P ;✓ (λr. Q) = P ; Q›
  ― ‹Very basic law.›
  by (simp add: Process_eq_spec Seqptick_same_type_projs Seq_projs)



subsection ‹The Laws of term‹⊥››

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

lemma BOT_Seqptick [simp] : ‹⊥ ;✓ P = ⊥› by (simp add: Seqptick_is_BOT_iff)


lemma (in Syncptick_locale) Syncptick_is_BOT_iff : ‹P ⟦S⟧✓ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (simp add: BOT_iff_Nil_D D_Syncptick)
    (metis Nil_setinterleavesptick Nil_setinterleavingptick_Nil insertCI is_processT1_TR)

lemma (in Syncptick_locale) Syncptick_BOT [simp] : ‹P ⟦S⟧✓ ⊥ = ⊥› and BOT_Syncptick [simp] : ‹⊥ ⟦S⟧✓ Q = ⊥›
  by (simp_all add: Syncptick_is_BOT_iff)



subsection ‹The Laws of const‹STOP››

lemma Seqptick_is_STOP_iff :
  ‹P ;✓ Q = STOP ⟷ 𝒯 P ⊆ insert [] {[✓(r)]| r. True} ∧
                     (∀r. [✓(r)] ∈ 𝒯 P ⟶ Q r = STOP)› (is ‹?lhs ⟷ ?rhs›)
proof (intro iffI conjI subsetI allI impI)
  show ‹?lhs ⟹ t ∈ 𝒯 P ⟹ t ∈ insert [] {[✓(r)] |r. True}› for t
    by (simp add: STOP_iff_T Seqptick_projs set_eq_iff)
      (metis Prefix_Order.prefixI T_nonTickFree_imp_decomp append_Nil
        append_T_imp_tickFree is_processT3_TR length_0_conv length_map list.distinct(1))
next
  show ‹?lhs ⟹ [✓(r)] ∈ 𝒯 P ⟹ Q r = STOP› for r
    by (force simp add: STOP_iff_T Seqptick_projs set_eq_iff)
next
  show ‹?rhs ⟹ P ;✓ Q = STOP›
    by (auto simp add: STOP_iff_T Seqptick_projs subset_iff)
      (metis D_T non_tickFree_tick,
        metis BOT_iff_Nil_D D_T D_BOT append_Nil eventptick.distinct(1) mem_Collect_eq
        front_tickFree_single is_processT9 list.distinct(1) list.inject)
qed

lemma Seqptick_is_STOP_iff_bis :
  ‹P ;✓ Q = STOP ⟷ SKIPS {r. [✓(r)] ∈ 𝒯 P} ⊑DT P ∧ (∀r. [✓(r)] ∈ 𝒯 P ⟶ Q r = STOP)›
  (is ‹?lhs ⟷ ?rhs›)
proof (rule iffI)
  assume ?lhs
  from this[THEN arg_cong, where f = 𝒟]
  have ‹𝒟 P = {}›
    by (simp add: Seqptick_projs D_STOP)
      (metis front_tickFree_Nil nonempty_divE[of P])
  with ‹?lhs› show ?rhs
    by (subst (asm) Seqptick_is_STOP_iff)
      (auto simp add: refine_defs SKIPS_projs)
next
  show ‹?rhs ⟹ ?lhs›
    unfolding Seqptick_is_STOP_iff by (auto simp add: refine_defs SKIPS_projs)
qed


corollary STOP_Seqptick [simp] : ‹STOP ;✓ P = STOP›
  by (simp add: Seqptick_is_STOP_iff T_STOP)


lemma (in Syncptick_locale) STOP_Syncptick_STOP [simp] : ‹STOP ⟦S⟧✓ STOP = STOP›
  by (simp add: STOP_iff_T T_Syncptick STOP_projs)



paragraph ‹More powerful Laws›

lemma (in Syncptick_locale) Interptick_STOP :
  ― ‹Here, term‹g› is a free parameter.›
  ‹P |||✓ STOP = RenamingTick (P ; STOP)
                 (λr. the (tick_join r (g r)))› (is ‹?lhs = ?rhs›)
proof -
  let ?f = ‹λr. the (tick_join r (g r))›
  have * : ‹tF t ⟹ map (map_eventptick id ?f) t
                     = map ev (map of_ev t)› for t :: ‹('a, 'r) traceptick›
    by (induct t, simp_all)
      (metis (no_types, lifting) eventptick.collapse(1) eventptick.simps(9) id_apply)
  show ‹?lhs = ?rhs›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    then obtain u v t_P
      where ‹t = u @ v› ‹ftF v› ‹tF u ∨ v = []›
        ‹u setinterleaves✓⇘tick_join⇙ ((t_P, []), {})› ‹t_P ∈ 𝒟 P›
      unfolding D_Syncptick STOP_projs by blast
    from this(4) setinterleavesptick_NilR_iff
    have ‹tF t_P› ‹u = map ev (map of_ev t_P)› by auto

    from "*" ‹tF t_P› have ‹u @ v = map (map_eventptick id ?f) t_P @ v›
      by (simp add: ‹u = map ev (map of_ev t_P)›)
    moreover have ‹t_P ∈ 𝒟 (P ; STOP)› by (simp add: D_Seq ‹t_P ∈ 𝒟 P›)
    ultimately show ‹t ∈ 𝒟 ?rhs›
      using ‹ftF v› ‹tF t_P› by (auto simp add: D_Renaming ‹t = u @ v›)
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then obtain u v
      where $ : ‹t = map (map_eventptick id ?f) u @ v›
        and ‹tF u› ‹ftF v› ‹u ∈ 𝒟 P› unfolding D_Renaming D_Seq D_STOP by blast
    have ‹tF (map (map_eventptick id ?f) u)›
      by (simp add: ‹tF u› map_eventptick_tickFree)
    moreover from ‹tF u›
    have ‹map (map_eventptick id ?f) u
          setinterleaves✓⇘tick_join⇙ ((u, []), {})›
    proof (induct u)
      case Nil show ?case by simp
    next
      case (Cons e u)
      obtain a where ‹e = ev a› ‹tF u› by (meson Cons.prems is_ev_def tickFree_Cons_iff)
      from Cons.hyps[OF ‹tF u›] show ?case by (simp add: ‹e = ev a›)
    qed
    ultimately show ‹t ∈ 𝒟 (P |||✓ STOP)›
      using ‹ftF v› ‹u ∈ 𝒟 P› by (auto simp add: D_Syncptick STOP_projs "$")
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
    then obtain t_P X_P X_Q
      where ‹(t_P, X_P) ∈ ℱ P› ‹t setinterleaves✓⇘tick_join⇙ ((t_P, []), {})›
        ‹X ⊆ super_ref_Syncptick tick_join X_P {} X_Q›
      unfolding Syncptick_projs F_STOP by blast

    from ‹X ⊆ super_ref_Syncptick tick_join X_P {} X_Q›
    have $ : ‹e ∈ map_eventptick id ?f -` X ∪ range tick
              ⟹ e ∈ X_P ∪ range tick› for e
      by (cases e) (auto simp add: super_ref_Syncptick_def)
    from setinterleavesptick_NilR_iff
      [THEN iffD1, OF ‹t setinterleaves✓⇘tick_join⇙ ((t_P, []), {})›]
    have ‹tF t_P› ‹t = map ev (map of_ev t_P)› by simp_all
    have $$ : ‹t = map (map_eventptick id ?f) t_P›
      by (simp add: "*" ‹t = map ev (map of_ev t_P)› ‹tF t_P›)
    show ‹(t, X) ∈ ℱ ?rhs›
    proof (cases ‹∃r. t_P @ [✓(r)] ∈ 𝒯 P›)
      show ‹∃r. t_P @ [✓(r)] ∈ 𝒯 P ⟹ (t, X) ∈ ℱ ?rhs›
        by (auto simp add: F_Renaming F_Seq F_STOP "$$")
    next
      assume ‹∄r. t_P @ [✓(r)] ∈ 𝒯 P›
      hence ‹(t_P, X_P ∪ range tick) ∈ ℱ P›
        by (auto intro!: is_processT5 ‹(t_P, X_P) ∈ ℱ P› F_T)
      with "$" have ‹(t_P, map_eventptick id ?f -` X ∪ range tick) ∈ ℱ P›
        by (meson is_processT4 subsetI)
      with ‹tF t_P› show ‹(t, X) ∈ ℱ ?rhs› by (auto simp add: F_Renaming F_Seq "$$")
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
    then obtain u where $ : ‹t = map (map_eventptick id ?f) u›
      ‹(u, map_eventptick id ?f -` X) ∈ ℱ (P ; STOP)›
      unfolding Renaming_projs by blast
    from "$"(2) consider ‹u ∈ 𝒟 P› | r where ‹u @ [✓(r)] ∈ 𝒯 P›
      | ‹(u, map_eventptick id ?f -` X ∪ range tick) ∈ ℱ P› ‹tF u›
      by (auto simp add: Seq_projs F_STOP)
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      let ?u' = ‹if tF u then u else butlast u›
      let ?v' = ‹if tF u then [] else [✓(?f (of_tick (last u)))]›
      assume ‹u ∈ 𝒟 P›
      hence ‹?u' ∈ 𝒟 P› by (simp add: D_imp_front_tickFree div_butlast_when_non_tickFree_iff)
      moreover from D_imp_front_tickFree ‹u ∈ 𝒟 P› front_tickFree_iff_tickFree_butlast
      have ‹tF ?u'› by auto
      moreover have ‹ftF ?v'› by simp
      moreover from ‹tF ?u'› have ‹t = map (map_eventptick id ?f) ?u' @ ?v'›
        by (cases u rule: rev_cases, auto simp add: "$"(1) split: if_split_asm)
          (metis eventptick.collapse(2) eventptick.simps(10))
      ultimately have ‹t ∈ 𝒟 ?rhs› unfolding D_Renaming D_Seq by blast
      with ‹t ∉ 𝒟 ?rhs› show ‹(t, X) ∈ ℱ ?lhs› ..
    next
      fix r assume ‹u @ [✓(r)] ∈ 𝒯 P›
      hence ‹(u, UNIV - {✓(r)}) ∈ ℱ P› by (simp add: is_processT6_TR)
      moreover from "$"(1) "*" ‹u @ [✓(r)] ∈ 𝒯 P› append_T_imp_tickFree
      have ‹t setinterleaves✓⇘tick_join⇙ ((u, []), {})›
        by (auto simp add: setinterleavesptick_NilR_iff)
      moreover have ‹X ⊆ super_ref_Syncptick tick_join (UNIV - {✓(r)}) {} UNIV›
        by (simp add: subset_iff super_ref_Syncptick_def) (metis eventptick.exhaust)
      ultimately show ‹(t, X) ∈ ℱ ?lhs› unfolding F_Syncptick F_STOP by clarify blast
    next
      assume ‹(u, map_eventptick id ?f -` X ∪ range tick) ∈ ℱ P› ‹tF u›
      moreover from "$"(1) "*" ‹tF u› have ‹t setinterleaves✓⇘tick_join⇙ ((u, []), {})›
        by (auto simp add: setinterleavesptick_NilR_iff)
      moreover have ‹X ⊆ super_ref_Syncptick tick_join (map_eventptick id ?f -` X ∪ range tick) {} UNIV›
        by (simp add: subset_iff super_ref_Syncptick_def) (metis eventptick.exhaust)
      ultimately show ‹(t, X) ∈ ℱ ?lhs› unfolding F_Syncptick F_STOP by clarify blast
    qed
  qed
qed



lemma (in Syncptick_locale) STOP_Interptick :
  ‹STOP |||✓ Q = RenamingTick (Q ; STOP)
                 (λs. the (tick_join (g s) s))›
  by (metis Syncptick_locale_sym.Interptick_STOP Syncptick_sym)



lemma (in Syncptick_locale) Parptick_STOP [simp] : ‹P ||✓ STOP = (if P = ⊥ then ⊥ else STOP)›
proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ⟹ P ||✓ STOP = ⊥› by simp
next
  show ‹P ≠ ⊥ ⟹ P ||✓ STOP = STOP›
    by (auto simp add: STOP_iff_T T_Syncptick STOP_projs set_eq_iff
        BOT_iff_Nil_D setinterleavesptick_NilR_iff image_iff)
      (metis eventptick.collapse(1) last_in_set tickFree_butlast)+
qed

lemma (in Syncptick_locale) STOP_Parptick [simp] : ‹STOP ||✓ P = (if P = ⊥ then ⊥ else STOP)›
proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ⟹ STOP ||✓ P = ⊥› by simp
next
  show ‹P ≠ ⊥ ⟹ STOP ||✓ P = STOP›
    by (auto simp add: STOP_iff_T T_Syncptick STOP_projs set_eq_iff
        BOT_iff_Nil_D setinterleavesptick_NilL_iff image_iff)
      (metis eventptick.collapse(1) last_in_set tickFree_butlast)+
qed



subsection ‹The Laws of const‹SKIP››

subsubsection ‹Sequential Composition›

text ‹const‹SKIP› is neutral for @{const [source] Seqptick}!›

lemma SKIP_Seqptick [simp] : ‹SKIP r ;✓ P = P r›
  by (simp add: Process_eq_spec Seqptick_projs ref_Seqptick_def SKIP_projs)

lemma Seqptick_SKIP [simp] : ‹P ;✓ SKIP = P›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 (P ;✓ SKIP) ⟹ s ∈ 𝒟 P›
    and ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 (P ;✓ SKIP)› for s
    by (simp_all add: D_Seqptick_same_type D_SKIP)
next
  show ‹(s, X) ∈ ℱ (P ;✓ SKIP) ⟹ (s, X) ∈ ℱ P› for s X
    by (auto simp add : F_Seqptick_same_type F_SKIP is_processT6_TR_notin tick_T_F
        intro : is_processT4 is_processT8)
next
  show ‹(s, X) ∈ ℱ P ⟹ (s, X) ∈ ℱ (P ;✓ SKIP)› for s X
    by (simp add : F_Seqptick_same_type F_SKIP)
      (metis (mono_tags, opaque_lifting) F_T T_nonTickFree_imp_decomp
        append.right_neutral f_inv_into_f is_processT5_S7')
qed

lemma SKIPS_Seqptick [simp] : ‹SKIPS R ;✓ P = ⊓r ∈ R. P r›
  by (auto simp add: Process_eq_spec GlobalNdet_projs Seqptick_projs
                     STOP_projs SKIPS_projs ref_Seqptick_def)


lemma finite_ticks_Seqptick [finite_ticks_simps] : ‹𝔽✓(P ;✓ Q)›
  if ‹𝔽✓(P)› and ‹(⋀r. r ∈ ✓s(P) ⟹ 𝔽✓(Q r))›
proof (rule finite_ticksI)
  fix t assume ‹t ∈ 𝒯 (P ;✓ Q)› ‹t ∉ 𝒟 (P ;✓ Q)›
  have ‹{r'. t @ [✓(r')] ∈ 𝒯 (P ;✓ Q)} ⊆
        (⋃u ∈ {u. ∃v r. t = map (ev ∘ of_ev) u @ v ∧ u @ [✓(r)] ∈ 𝒯 P ∧ u ∉ 𝒟 P ∧ tF u ∧ ftF v}.
         ⋃r ∈ {r. u @ [✓(r)] ∈ 𝒯 P}. {s. drop (length u) t @ [✓(s)] ∈ 𝒯 (Q r)})› (is ‹?lhs ⊆ ?rhs›)
  proof (rule subsetI)
    fix r' assume ‹r' ∈ ?lhs›
    hence ‹t @ [✓(r')] ∈ 𝒯 (P ;✓ Q)› by simp
    with ‹t ∉ 𝒟 (P ;✓ Q)› obtain t' r u'
      where ‹t @ [✓(r')] = map (ev ∘ of_ev) t' @ u'› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹t' ∉ 𝒟 P› ‹tF t'› ‹u' ∈ 𝒯 (Q r)›
      by (auto simp add: Seqptick_projs)
        (metis non_tickFree_tick tickFree_append_iff tickFree_map_ev_comp,
          metis (no_types, opaque_lifting) T_imp_front_tickFree butlast_append butlast_snoc
                front_tickFree_iff_tickFree_butlast non_tickFree_tick tickFree_append_iff
                tickFree_imp_front_tickFree tickFree_map_ev_comp,
          metis (no_types, opaque_lifting) append.assoc butlast_snoc front_tickFree_charn non_tickFree_tick
                tickFree_Nil tickFree_append_iff tickFree_imp_front_tickFree tickFree_map_ev_comp)
      
      thus ‹r' ∈ ?rhs›
      apply auto
      by (smt (verit, ccfv_SIG) Prefix_Order.same_prefix_nil T_imp_front_tickFree append_eq_append_conv2 append_eq_append_conv_if append_eq_conv_conj
          append_eq_first_pref_spec append_same_eq eventptick.disc(2) front_tickFree_dw_closed length_map tickFree_Cons_iff tickFree_append_iff
          tickFree_map_ev_comp)
  qed
  moreover have ‹finite …›
  proof (rule finite_UN_I)
    show ‹finite {u. ∃v r. t = map (ev ∘ of_ev) u @ v ∧ u @ [✓(r)] ∈ 𝒯 P ∧ u ∉ 𝒟 P ∧ tF u ∧ ftF v}›
      by (rule finite_subset[of _ ‹{u. u ≤ map (ev ∘ of_ev) (if tF t then t else butlast t)}›])
        (auto simp add: append_T_imp_tickFree tickFree_map_ev_of_ev_same_type_is prefixes_fin,
          metis prefixI append_T_imp_tickFree butlast_append map_append
                not_Cons_self2 tickFree_Nil tickFree_map_ev_of_ev_eq_iff)
  next
    fix u assume ‹u ∈ {u. ∃v r. t = map (ev ∘ of_ev) u @ v ∧ u @ [✓(r)] ∈ 𝒯 P ∧ u ∉ 𝒟 P ∧ tF u ∧ ftF v}›
    then obtain r v where ‹t = map (ev ∘ of_ev) u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹u ∉ 𝒟 P› ‹tF u› ‹ftF v› by blast
    show ‹finite (⋃r∈{r. u @ [✓(r)] ∈ 𝒯 P}. {s. drop (length u) t @ [✓(s)] ∈ 𝒯 (Q r)})›
    proof (rule finite_UN_I)
      show ‹finite {r. u @ [✓(r)] ∈ 𝒯 P}›
        by (simp add: ‹𝔽✓(P)› ‹u ∉ 𝒟 P› finite_ticksD)
    next
      fix r assume ‹r ∈ {r. u @ [✓(r)] ∈ 𝒯 P}›
      hence ‹u @ [✓(r)] ∈ 𝒯 P› ..
      with ‹t ∉ 𝒟 (P ;✓ Q)› ‹u @ [✓(r)] ∈ 𝒯 P› ‹tF u› have ‹v ∉ 𝒟 (Q r)›
        by (auto simp add: ‹t = map (ev ∘ of_ev) u @ v› Seqptick_projs)
      show ‹finite {s. drop (length u) t @ [✓(s)] ∈ 𝒯 (Q r)}›
        by (simp add: ‹t = map (ev ∘ of_ev) u @ v›)
          (metis ‹u @ [✓(r)] ∈ 𝒯 P› ‹u ∉ 𝒟 P› ‹v ∉ 𝒟 (Q r)› finite_ticksD
                 is_processT9 strict_ticks_of_memI ‹(⋀r. r ∈ ✓s(P) ⟹ 𝔽✓(Q r))›)
    qed
  qed
  ultimately show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (P ;✓ Q)}› by (fact finite_subset)
qed



lemma finite_ticks_fun_Seqptick_bis :
  ‹𝔽✓⇒(f) ⟹ (⋀x r. r ∈ ✓s(f x) ⟹ 𝔽✓(x) ⟹ 𝔽✓(g x r)) ⟹ 𝔽✓⇒(λx. f x ;✓ g x)›
  by (simp add: finite_ticks_fun_def finite_ticks_Seqptick)

lemma finite_ticks_fun_Seqptick [finite_ticks_fun_simps] :
  ― ‹Big approximation.›
  ‹𝔽✓⇒(f) ⟹ (⋀r. r ∈ (⋃x. ✓s(f x)) ⟹ 𝔽✓⇒(λx. g x r)) ⟹ 𝔽✓⇒(λx. f x ;✓ g x)›
  by (rule finite_ticks_fun_Seqptick_bis)
    (auto simp add: finite_ticks_fun_def)



subsubsection ‹Synchronization Product›

text ‹The generalization of the synchronization product was essentially motivated by
      the following theorem (in comparison to @{thm SKIP_Sync_SKIP[of r A s]}).›

theorem (in Syncptick_locale) SKIP_Syncptick_SKIP [simp] :
  ‹SKIP r ⟦A⟧✓ SKIP s = (case tick_join r s of ⌊r_s⌋ ⇒ SKIP r_s | ◇ ⇒ STOP)›
proof (split option.split, intro conjI impI allI)
  show ‹tick_join r s = ◇ ⟹ SKIP r ⟦A⟧✓ SKIP s = STOP›
    unfolding STOP_iff_T T_Syncptick SKIP_projs set_eq_iff
    by (safe, simp_all, metis Nil_setinterleavingptick_Nil insertCI)
next
  show ‹SKIP r ⟦A⟧✓ SKIP s = SKIP r_s› if ‹tick_join r s = ⌊r_s⌋› for r_s
  proof (rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 (SKIP r ⟦A⟧✓ SKIP s) ⟹ t ∈ 𝒟 (SKIP r_s)› for t
      by (simp add: D_Syncptick SKIP_projs)
  next
    show ‹t ∈ 𝒟 (SKIP r_s) ⟹ t ∈ 𝒟 (SKIP r ⟦A⟧✓ SKIP s)› for t
      by (simp add: D_Syncptick SKIP_projs)
  next
    fix t X assume ‹(t, X) ∈ ℱ (SKIP r ⟦A⟧✓ SKIP s)› ‹t ∉ 𝒟 (SKIP r ⟦A⟧✓ SKIP s)›
    then obtain t_P t_Q X_P X_Q
      where fail: ‹(t_P, X_P) ∈ ℱ (SKIP r)› ‹(t_Q, X_Q) ∈ ℱ (SKIP s)›
        ‹t setinterleaves✓⇘tick_join⇙ ((t_P, t_Q), A)›
        ‹X ⊆ super_ref_Syncptick tick_join X_P A X_Q›
      unfolding Syncptick_projs by blast
    from fail(1-3) consider ‹t = []› ‹✓(r) ∉ X_P› ‹✓(s) ∉ X_Q› | ‹t = [✓(r_s)]›
      by (cases t_P; cases t_Q) (simp_all add: F_SKIP ‹tick_join r s = ⌊r_s⌋›)
    thus ‹(t, X) ∈ ℱ (SKIP r_s)›
    proof cases
      assume ‹t = []› ‹✓(r) ∉ X_P› ‹✓(s) ∉ X_Q›
      from ‹✓(r) ∉ X_P› ‹✓(s) ∉ X_Q› fail(4) ‹tick_join r s = ⌊r_s⌋›
      have ‹✓(r_s) ∉ X›
        by (simp add: super_ref_Syncptick_def subset_iff)
          (metis eventptick.distinct(1) eventptick.inject(2) inj_tick_join)
      with ‹t = []› show ‹(t, X) ∈ ℱ (SKIP r_s)› by (simp add: F_SKIP)
    next
      show ‹t = [✓(r_s)] ⟹ (t, X) ∈ ℱ (SKIP r_s)› by (simp add: F_SKIP)
    qed
  next
    fix t :: ‹('a, _) traceptick› and X assume ‹(t, X) ∈ ℱ (SKIP r_s)›
    then consider ‹t = []› ‹✓(r_s) ∉ X› | ‹t = [✓(r_s)]›
      unfolding F_SKIP by blast
    thus ‹(t, X) ∈ ℱ (SKIP r ⟦A⟧✓ SKIP s)›
    proof cases
      assume ‹t = []› ‹✓(r_s) ∉ X›
      have ‹([], - {✓(r)}) ∈ ℱ (SKIP r)›
        by (simp add: F_SKIP)
      moreover have ‹([], - {✓(s)}) ∈ ℱ (SKIP s)›
        by (simp add: F_SKIP)
      moreover have  ‹t setinterleaves✓⇘tick_join⇙ (([], []), A)›
        by (simp add: ‹t = []›)
      moreover have ‹X ⊆ super_ref_Syncptick tick_join (- {✓(r)}) A (- {✓(s)})›
        using ‹✓(r_s) ∉ X› ‹tick_join r s = ⌊r_s⌋›
        by (simp add: super_ref_Syncptick_def subset_iff)
          (metis eventptick.exhaust option.inject)
      ultimately show ‹(t, X) ∈ ℱ (SKIP r ⟦A⟧✓ SKIP s)›
        by (simp (no_asm) add: F_Syncptick) blast
    next
      assume ‹t = [✓(r_s)]›
      have ‹([✓(r)], UNIV) ∈ ℱ (SKIP r)›
        by (simp add: F_SKIP)
      moreover have ‹([✓(s)], UNIV) ∈ ℱ (SKIP s)›
        by (simp add: F_SKIP)
      moreover have ‹t setinterleaves✓⇘tick_join⇙ (([✓(r)], [✓(s)]), A)›
        by (simp add: ‹t = [✓(r_s)]› ‹tick_join r s = ⌊r_s⌋›)
      moreover have ‹X ⊆ super_ref_Syncptick tick_join UNIV A UNIV›
        by (simp add: super_ref_Syncptick_def subset_iff)
          (metis eventptick.exhaust)
      ultimately show ‹(t, X) ∈ ℱ (SKIP r ⟦A⟧✓ SKIP s)›
        by (simp (no_asm) add: F_Syncptick) blast
    qed
  qed
qed



lemma (in Syncptick_locale) STOP_Syncptick_SKIP [simp] : ‹STOP ⟦A⟧✓ SKIP s = STOP›
  and SKIP_Syncptick_STOP [simp] : ‹SKIP r ⟦A⟧✓ STOP = STOP›
  by (force simp add: STOP_iff_T T_Syncptick STOP_projs SKIP_projs)+


lemma (in Syncptick_locale) Mprefix_Syncptick_SKIP :
  ‹□a ∈ A → P a ⟦S⟧✓ SKIP r =
   □a ∈ (A - S) → (P a ⟦S⟧✓ SKIP r)› (is ‹?lhs = ?rhs›)
proof (rule Process_eq_optimizedI)
  fix t assume ‹t ∈ 𝒟 ?lhs›
  then obtain u v t_P a t_Q
    where * : ‹t = u @ v› ‹tF u› ‹ftF v› ‹a ∈ A› ‹t_P ∈ 𝒟 (P a)›
      ‹u setinterleaves✓⇘(⊗✓)⇙ ((ev a # t_P, t_Q), S)› ‹t_Q = [] ∨ t_Q = [✓(r)]›
    unfolding D_Syncptick SKIP_projs Mprefix_projs by blast
  from "*"(6, 7) obtain u'
    where ‹a ∉ S› ‹u = ev a # u'› ‹u' setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
    by (auto split: if_split_asm)
  from this(2, 3) "*"(2, 5, 7) front_tickFree_charn have ‹u' ∈ 𝒟 (P a ⟦S⟧✓ SKIP r)›
    by (auto simp add: D_Syncptick SKIP_projs)
  with "*"(1-4) ‹a ∉ S› ‹u = ev a # u'› is_processT7 show ‹t ∈ 𝒟 ?rhs›
    by (auto simp add: D_Mprefix)
next
  fix t assume ‹t ∈ 𝒟 ?rhs›
  then obtain a t' where ‹t = ev a # t'› ‹a ∈ A› ‹a ∉ S› ‹t' ∈ 𝒟 (P a ⟦S⟧✓ SKIP r)›
    unfolding D_Mprefix by blast
  then obtain u v t_P t_Q
    where * : ‹t' = u @ v› ‹tF u› ‹ftF v› ‹t_P ∈ 𝒟 (P a)›
      ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› ‹t_Q = [] ∨ t_Q = [✓(r)]›
    unfolding D_Syncptick SKIP_projs by blast
  have ‹t = (ev a # u) @ v› by (simp add: "*"(1) ‹t = ev a # t'›)
  moreover from "*"(2) have ‹tF (ev a # u)› by simp
  moreover from "*"(5, 6) have ‹ev a # u setinterleaves✓⇘(⊗✓)⇙ ((ev a # t_P, t_Q), S)›
    by (cases t_Q) (simp_all add: ‹a ∉ S› Cons_setinterleavingptick_Cons)
  moreover have ‹ev a # t_P ∈ 𝒟 (□a ∈ A → P a)›
    by (simp add: "*"(4) D_Mprefix ‹a ∈ A›)
  ultimately show ‹t ∈ 𝒟 ?lhs›
    unfolding D_Syncptick SKIP_projs using "*"(3, 6) by blast
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) ∈ ℱ (□a ∈ A → P a)› ‹(t_Q, X_Q) ∈ ℱ (SKIP r)›
      ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
      ‹X ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
    unfolding Syncptick_projs by blast
  from "*"(1) consider ‹t_P = []› ‹X_P ∩ ev ` A = {}›
    | a t_P' where ‹t_P = ev a # t_P'› ‹a ∈ A› ‹(t_P', X_P) ∈ ℱ (P a)›
    unfolding F_Mprefix by blast
  thus ‹(t, X) ∈ ℱ ?rhs›
  proof cases
    assume ‹t_P = []› ‹X_P ∩ ev ` A = {}›
    from ‹t_P = []› "*"(2, 3) have ‹t = []› ‹t_Q = []› ‹✓(r) ∉ X_Q›
      by (auto simp add: F_SKIP)
    with "*"(4) show ‹t_P = [] ⟹ X_P ∩ ev ` A = {} ⟹ (t, X) ∈ ℱ ?rhs›
      by (auto simp add: F_Mprefix super_ref_Syncptick_def)
  next
    fix a t_P' assume ‹t_P = ev a # t_P'› ‹a ∈ A› ‹(t_P', X_P) ∈ ℱ (P a)›
    from "*"(2, 3) obtain t'
      where ‹t = ev a # t'› ‹a ∉ S› ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q), S)›
      by (auto simp add: ‹t_P = ev a # t_P'› F_SKIP split: if_split_asm)
    from "*"(2, 4) ‹(t_P', X_P) ∈ ℱ (P a)› this(3)
    have ‹(t', X) ∈ ℱ (P a ⟦S⟧✓ SKIP r)› by (auto simp add: F_Syncptick)
    thus ‹(t, X) ∈ ℱ ?rhs› by (simp add: ‹t = ev a # t'› F_Mprefix ‹a ∈ A› ‹a ∉ S›)
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
  from ‹(t, X) ∈ ℱ ?rhs› consider ‹t = []› ‹X ∩ ev ` (A - S) = {}›
    | a t' where ‹t = ev a # t'› ‹a ∈ A› ‹a ∉ S› ‹(t', X) ∈ ℱ (P a ⟦S⟧✓ SKIP r)›
    unfolding F_Mprefix by blast
  thus ‹(t, X) ∈ ℱ ?lhs›
  proof cases
    assume ‹t = []› ‹X ∩ ev ` (A - S) = {}›
    from ‹X ∩ ev ` (A - S) = {}›
    have ‹([], range tick ∪ {ev a |a. ev a ∈ X ∧ a ∉ S}) ∈ ℱ (□a ∈ A → P a)›
      by (auto simp add: F_Mprefix)
    moreover have ‹([], UNIV - {✓(r)}) ∈ ℱ (SKIP r)› by (simp add: F_SKIP)
    moreover have ‹X ⊆ super_ref_Syncptick (⊗✓) 
                       (range tick ∪ {ev a |a. ev a ∈ X ∧ a ∉ S}) S (UNIV - {✓(r)})›
      by (simp add: subset_iff super_ref_Syncptick_def) (metis eventptick.exhaust)
    moreover have ‹[] setinterleaves✓⇘(⊗✓)⇙ (([], []), S)› by simp
    ultimately show ‹(t, X) ∈ ℱ ?lhs› by (simp (no_asm) add: ‹t = []› F_Syncptick) blast
  next
    fix a t' assume ‹t = ev a # t'› ‹a ∈ A› ‹a ∉ S› ‹(t', X) ∈ ℱ (P a ⟦S⟧✓ SKIP r)›
    from this(1, 4) ‹t ∉ 𝒟 ?rhs› ‹a ∈ A› ‹a ∉ S›
    obtain t_P t_Q X_P X_Q
      where * : ‹(t_P, X_P) ∈ ℱ (P a)› ‹(t_Q, X_Q) ∈ ℱ (SKIP r)›
        ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
      unfolding D_Mprefix Syncptick_projs by force
    have ‹(ev a # t_P, X_P) ∈ ℱ (□a ∈ A → P a)›
      by (simp add: "*"(1) F_Mprefix ‹a ∈ A›)
    moreover from "*"(2, 3) have ‹t setinterleaves✓⇘(⊗✓)⇙ ((ev a # t_P, t_Q), S)›
      by (auto simp add: ‹t = ev a # t'› F_SKIP ‹a ∉ S›)
    ultimately show ‹(t, X) ∈ ℱ ?lhs› unfolding F_Syncptick using "*"(2, 4) by auto
  qed
qed


corollary (in Syncptick_locale) SKIP_Syncptick_Mprefix :
  ‹SKIP r ⟦S⟧✓ □b ∈ B → Q b = □b ∈ (B - S) → (SKIP r ⟦S⟧✓ Q b)› (is ‹?lhs = ?rhs›)
  by (subst (1 2) Syncptick_locale_sym.Syncptick_sym mono_Mprefix_eq)
    (fact Syncptick_locale_sym.Mprefix_Syncptick_SKIP)


lemma (in Syncptick_locale) finite_ticks_Syncptick [finite_ticks_simps] :
  ‹𝔽✓(P ⟦S⟧✓ Q)› if ‹𝔽✓(P)› and ‹𝔽✓(Q)›
proof (rule finite_ticksI)
  fix t assume ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)›
  have ‹{r_s. t @ [✓(r_s)] ∈ 𝒯 (P ⟦S⟧✓ Q)} ⊆
        (⋃(t_P, t_Q)∈{(t_P, t_Q). t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)}.
                      {r_s. ∃r s. r ⊗✓ s = ⌊r_s⌋ ∧
                                  t_P @ [✓(r)] ∈ 𝒯 P ∧ t_P ∉ 𝒟 P ∧
                                  t_Q @ [✓(s)] ∈ 𝒯 Q ∧ t_Q ∉ 𝒟 Q})›
    (is ‹_ ⊆ ?rhs›)
  proof (rule subsetI)
    fix r_s assume ‹r_s ∈ {r_s. t @ [✓(r_s)] ∈ 𝒯 (P ⟦S⟧✓ Q)}›
    hence ‹t @ [✓(r_s)] ∈ 𝒯 (P ⟦S⟧✓ Q)› ..
    moreover from ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)› have ‹t @ [✓(r_s)] ∉ 𝒟 (P ⟦S⟧✓ Q)›
      by (meson is_processT9)
    ultimately obtain t_P t_Q where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› ‹t_P ∉ 𝒟 P› ‹t_Q ∉ 𝒟 Q›
      ‹t @ [✓(r_s)] setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
      by (simp add: T_Syncptick D_Syncptick') (use front_tickFree_Nil in blast)
    from this(5) show ‹r_s ∈ ?rhs›
    proof (elim snoc_tick_setinterleavesptickE)
      fix r s t_P' t_Q'
      assume assms : ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)›
        ‹r ⊗✓ s = ⌊r_s⌋› ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
      from ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› ‹t_P ∉ 𝒟 P› ‹t_Q ∉ 𝒟 Q› assms(3, 4)
      have ‹t_P' ∉ 𝒟 P› ‹t_Q' ∉ 𝒟 Q›
        by (meson T_imp_front_tickFree front_tickFree_append_iff is_processT7 not_Cons_self2)+
      with ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› assms show ‹r_s ∈ ?rhs› by auto
    qed
  qed
  moreover have ‹finite …›
  proof (rule finite_UN_I, safe)
    show ‹finite {(t_P, t_Q). t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)}›
      by (fact finite_setinterleavesptick_tick_join)
  next
    fix t_P t_Q
    let ?S = ‹{r_s. ∃r s. r ⊗✓ s = ⌊r_s⌋ ∧
                          t_P @ [✓(r)] ∈ 𝒯 P ∧ t_P ∉ 𝒟 P ∧
                          t_Q @ [✓(s)] ∈ 𝒯 Q ∧ t_Q ∉ 𝒟 Q}›
    have ‹Some ` ?S ⊆ (λ(r, s). r ⊗✓ s) `
                       ({r. t_P @ [✓(r)] ∈ 𝒯 P ∧ t_P ∉ 𝒟 P} ×
                        {s. t_Q @ [✓(s)] ∈ 𝒯 Q ∧ t_Q ∉ 𝒟 Q})› by force
    moreover have ‹finite …› by (simp add: finite_ticksD ‹𝔽✓(P)› ‹𝔽✓(Q)›)
    ultimately have ‹finite (Some ` ?S)› by (fact finite_subset)
    thus ‹finite ?S› by (simp add: finite_image_iff)
  qed
  ultimately show ‹finite {r_s. t @ [✓(r_s)] ∈ 𝒯 (P ⟦S⟧✓ Q)}› by (fact finite_subset)
qed

lemma (in Syncptick_locale) finite_ticks_fun_Syncptick [finite_ticks_fun_simps] :
  ‹𝔽✓⇒(f) ⟹ 𝔽✓⇒(g) ⟹ 𝔽✓⇒(λx. f x ⟦S⟧✓ g x)›
  by (simp add: finite_ticks_fun_def finite_ticks_Syncptick)



section ‹Associativity of Sequential Composition›

lemma Seqptick_assoc : ‹P ;✓ (λr. Q r ;✓ R) = P ;✓ Q ;✓ R›
  for P :: ‹('a, 'r) processptick›
    and Q :: ‹'r ⇒ ('a, 's) processptick›
    and R :: ‹'s ⇒ ('a, 't) processptick›
proof (rule Process_eq_optimizedI)
  fix t assume ‹t ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
  then consider (D_P) t' u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
    | (D_Q_R) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹u ∈ 𝒟 (Q r ;✓ R)›
    unfolding Seqptick_projs[of P] by fast
  thus ‹t ∈ 𝒟 (P ;✓ Q ;✓ R)›
  proof cases
    case D_P
    define t'' :: ‹('a, 's) traceptick› where ‹t'' = map (ev ∘ of_ev) t'›
    from D_P have ‹t'' ∈ 𝒟 (P ;✓ Q)›
      by (auto simp add: t''_def Seqptick_projs intro: front_tickFree_Nil)
    moreover have ‹tF t''› by (simp add: t''_def)
    ultimately have ‹map (ev ∘ of_ev) t'' ∈ 𝒟 (P ;✓ Q ;✓ R)›
      by (simp add: Seqptick_projs[of ‹P ;✓ Q›])
        (metis append.right_neutral front_tickFree_Nil)
    also have ‹map (ev ∘ of_ev) t'' = map (ev ∘ of_ev) t'›
      by (simp add: t''_def)
    finally have ‹map (ev ∘ of_ev) t' ∈ 𝒟 (P ;✓ Q ;✓ R)› .
    with D_P(1, 3, 4) show ‹t ∈ 𝒟 (P ;✓ Q ;✓ R)› by (simp add: is_processT7)
  next
    case D_Q_R
    from D_Q_R(3) consider (D_Q) u' v where ‹u = map (ev ∘ of_ev) u' @ v› ‹u' ∈ 𝒟 (Q r)› ‹tF u'› ‹ftF v›
      | (D_R) u' s v where ‹u = map (ev ∘ of_ev) u' @ v› ‹u' @ [✓(s)] ∈ 𝒯 (Q r)› ‹tF u'› ‹v ∈ 𝒟 (R s)›
      unfolding Seqptick_projs by blast
    thus ‹t ∈ 𝒟 (P ;✓ Q ;✓ R)›
    proof cases
      case D_Q
      define t'' :: ‹('a, 's) traceptick› where ‹t'' = map (ev ∘ of_ev) t' @ map (ev ∘ of_ev) u'›
      have ‹t'' ∈ 𝒟 (P ;✓ Q)›
        by (simp add: t''_def Seqptick_projs)
          (metis D_Q(2,3) D_Q_R(2) append_T_imp_tickFree list.distinct(1)
                 tickFree_map_ev_of_ev_same_type_is)
      moreover have ‹tF t''› by (simp add: t''_def)
      ultimately have ‹map (ev ∘ of_ev) t'' ∈ 𝒟 (P ;✓ Q ;✓ R)›
        by (simp add: Seqptick_projs[of ‹P ;✓ Q›])
          (metis append.right_neutral front_tickFree_Nil)
      also have ‹map (ev ∘ of_ev) t'' = map (ev ∘ of_ev) t' @ map (ev ∘ of_ev) u'›
        by (simp add: t''_def)
      finally have ‹map (ev ∘ of_ev) t' @ map (ev ∘ of_ev) u' ∈ 𝒟 (P ;✓ Q ;✓ R)› .
      with D_Q(1,4) D_Q_R(1) is_processT7 show ‹t ∈ 𝒟 (P ;✓ Q ;✓ R)› by fastforce
    next
      case D_R
      define t'' :: ‹('a, 's) traceptick› where ‹t'' = map (ev ∘ of_ev) (map (ev ∘ of_ev) t' @ u')›
      have ‹t'' @ [✓(s)] ∈ 𝒯 (P ;✓ Q)›
        by (simp add: t''_def Seqptick_projs[of P] del: map_map)
          (metis D_Q_R(2) D_R(2) append_T_imp_tickFree not_Cons_self2
                 tickFree_map_ev_of_ev_same_type_is)
      moreover have ‹tF t''› unfolding t''_def by (blast intro: tickFree_map_ev_comp)

      ultimately have ‹map (ev ∘ of_ev) t'' @ v ∈ 𝒟 (P ;✓ Q ;✓ R)›
        unfolding Seqptick_projs[of ‹P ;✓ Q›] using D_R(4) by blast
      also have ‹map (ev ∘ of_ev) t'' @ v = t›
        by (simp add: D_Q_R(1) D_R(1) t''_def)
      finally show ‹t ∈ 𝒟 (P ;✓ Q ;✓ R)› .
    qed
  qed
next

  fix t assume ‹t ∈ 𝒟 (P ;✓ Q ;✓ R)›
  then consider (D_P_Q) t' u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 (P ;✓ Q)› ‹tF t'› ‹ftF u›
    | (D_R) t' s u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(s)] ∈ 𝒯 (P ;✓ Q)› ‹u ∈ 𝒟 (R s)›
    unfolding Seqptick_projs[of ‹P ;✓ Q›] by blast
  thus ‹t ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
  proof cases
    case D_P_Q
    from D_P_Q(2) consider (D_P) t'' u' where ‹t' = map (ev ∘ of_ev) t'' @ u'› ‹t'' ∈ 𝒟 P› ‹tF t''› ‹ftF u'›
      | (D_Q) t'' r u' where ‹t' = map (ev ∘ of_ev) t'' @ u'› ‹t'' @ [✓(r)] ∈ 𝒯 P› ‹tF t''› ‹u' ∈ 𝒟 (Q r)›
      unfolding Seqptick_projs by blast
    thus ‹t ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
    proof cases
      case D_P
      from D_P(2, 3) have ‹map (ev ∘ of_ev) t'' ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
        by (auto simp add: Seqptick_projs[of P] intro: front_tickFree_Nil)
      thus ‹t ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
        by (simp add: D_P_Q(1) D_P(1))
          (metis (mono_tags, lifting) D_P_Q(4) front_tickFree_append
            is_processT7 tickFree_map_ev_comp)
    next
      case D_Q
      from D_P_Q(3) D_Q(1, 4) have ‹map (ev ∘ of_ev) u' ∈ 𝒟 (Q r ;✓ R)›
        by (simp add: Seqptick_projs) (metis append.right_neutral front_tickFree_Nil)
      with D_Q(2, 3) have ‹map (ev ∘ of_ev) (map (ev ∘ of_ev) t'' @ u') ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
        by (auto simp add: Seqptick_projs[of P])
      with D_P_Q(4) is_processT7 show ‹t ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
        by (fastforce simp add: D_P_Q(1) D_Q(1))
    qed
  next
    case D_R
    then consider (T_P) t'' r u' where ‹t' = map (ev ∘ of_ev) t'' @ u'›
      ‹t'' @ [✓(r)] ∈ 𝒯 P› ‹tF t''› ‹u' @ [✓(s)] ∈ 𝒯 (Q r)›
    | (D_P) t'' u' where ‹t' = map (ev ∘ of_ev) t'' @ u'› ‹t'' ∈ 𝒟 P› ‹tF t''› ‹tF u'›
      by (auto simp add: Seqptick_projs append_eq_append_conv2 append_eq_map_conv
          Cons_eq_append_conv front_tickFree_append_iff intro: D_P T_P)
    thus ‹t ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
    proof cases
      case T_P
      from D_R(3) T_P(4) have ‹map (ev ∘ of_ev) u' @ u ∈ 𝒟 (Q r ;✓ R)›
        by (simp add: Seqptick_projs) (metis append_T_imp_tickFree not_Cons_self2)
      with T_P(2, 3) have ‹map (ev ∘ of_ev) t'' @ map (ev ∘ of_ev) u' @ u ∈
                           𝒟 (P ;✓ (λr. Q r ;✓ R))›
        by (auto simp add: Seqptick_projs[of P])
      also have ‹map (ev ∘ of_ev) t'' @ map (ev ∘ of_ev) u' @ u = t›
        by (simp add: D_R(1) T_P(1))
      finally show ‹t ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))› .
    next
      case D_P
      from D_P(2, 3) have ‹map (ev ∘ of_ev) t'' ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
        by (auto simp add: Seqptick_projs[of P] intro: front_tickFree_Nil)
      with D_R(3) show ‹t ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
        by (simp add: D_R(1) D_P(1))
          (metis (mono_tags, lifting) D_imp_front_tickFree
            front_tickFree_append is_processT7 tickFree_map_ev_comp)
    qed
  qed
next

  fix t X assume ‹(t, X) ∈ ℱ (P ;✓ (λr. Q r ;✓ R))› ‹t ∉ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
  then consider (F_P) t' where ‹t = map (ev ∘ of_ev) t'› ‹(t', ref_Seqptick X) ∈ ℱ P› ‹tF t'›
    | (F_Q_R) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P›
      ‹tF t'› ‹(u, X) ∈ ℱ (Q r ;✓ R)›
    unfolding Seqptick_projs[of P] by fast
  thus ‹(t, X) ∈ ℱ (P ;✓ Q ;✓ R)›
  proof cases
    case F_P
    from F_P(2) have ‹(t', ref_Seqptick (ref_Seqptick X)) ∈ ℱ P›
      by (simp add: ref_Seqptick_idem)
    with F_P(3) have ‹(map (ev ∘ of_ev) t', ref_Seqptick X) ∈ ℱ (P ;✓ Q)›
      by (auto simp add: Seqptick_projs)
    thus ‹(t, X) ∈ ℱ (P ;✓ Q ;✓ R)›
      by (simp add: Seqptick_projs[of ‹P ;✓ Q›] F_P(1))
        (metis map_ev_of_ev_map_ev_of_ev tickFree_map_ev_comp)
  next
    case F_Q_R
    from F_Q_R(4)
    consider (F_Q) u' where ‹u = map (ev ∘ of_ev) u'›
      ‹(u', ref_Seqptick X) ∈ ℱ (Q r)› ‹tF u'›
    | (F_R) u' s u'' where ‹u = map (ev ∘ of_ev) u' @ u''› ‹u' @ [✓(s)] ∈ 𝒯 (Q r)› ‹tF u'› ‹(u'', X) ∈ ℱ (R s)›
    | (D_Q) u' u'' where ‹u = map (ev ∘ of_ev) u' @ u''› ‹u' ∈ 𝒟 (Q r)› ‹tF u'› ‹ftF u''›
      unfolding Seqptick_projs by blast
    thus ‹(t, X) ∈ ℱ (P ;✓ Q ;✓ R)›
    proof cases
      case F_Q
      from F_Q(2) F_Q_R(2, 3)
      have ‹(map (ev ∘ of_ev) t' @ u',ref_Seqptick X) ∈ ℱ (P ;✓ Q)›
        by (auto simp add: Seqptick_projs)
      with F_Q(1,3) F_Q_R(1) show ‹(t, X) ∈ ℱ (P ;✓ Q ;✓ R)›
        by (simp add: Seqptick_projs[of ‹P ;✓ Q›])
          (metis map_append map_ev_of_ev_map_ev_of_ev tickFree_append_iff tickFree_map_ev_comp)
    next
      case F_R
      from F_Q_R(2, 3) F_R(2) have $ : ‹map (ev ∘ of_ev) t' @ u' @ [✓(s)] ∈ 𝒯 (P ;✓ Q)›
        by (auto simp add: Seqptick_projs)
      have $$ : ‹tF (map (ev ∘ of_ev) t' @ u')› by (simp add: F_R(3))
      show ‹(t, X) ∈ ℱ (P ;✓ Q ;✓ R)›
        by (simp add: Seqptick_projs[of ‹P ;✓ Q›])
          (metis map_append[of ‹ev ∘ of_ev› ‹map (ev ∘ of_ev) t'› u']
            F_Q_R(1) F_R(1, 4) "$" "$$" append_eq_appendI map_ev_of_ev_map_ev_of_ev)
    next
      case D_Q
      from D_Q(2) F_Q_R(2, 3) have $ : ‹map (ev ∘ of_ev) t' @ u' ∈ 𝒟 (P ;✓ Q)›
        by (auto simp add: Seqptick_projs)
      have $$ : ‹tF (map (ev ∘ of_ev) t' @ u')› by (simp add: D_Q(3))
      have ‹t ∈ 𝒟 (P ;✓ Q ;✓ R)›
        by (simp add: Seqptick_projs[of ‹P ;✓ Q›])
          (metis D_Q(1, 4) F_Q_R(1) "$" "$$" append_assoc map_append map_ev_of_ev_map_ev_of_ev)
      thus ‹(t, X) ∈ ℱ (P ;✓ Q ;✓ R)› by (fact is_processT8)
    qed
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ (P ;✓ Q ;✓ R)› ‹t ∉ 𝒟 (P ;✓ Q ;✓ R)›
  then consider (F_P_Q) t' where ‹t = map (ev ∘ of_ev) t'›
    ‹(t', ref_Seqptick X) ∈ ℱ (P ;✓ Q)› ‹tF t'›
  | (F_R) t' s u where ‹t = map (ev ∘ of_ev) t' @ u›
    ‹t' @ [✓(s)] ∈ 𝒯 (P ;✓ Q)› ‹tF t'› ‹(u, X) ∈ ℱ (R s)›
    unfolding Seqptick_projs[of ‹P ;✓ Q›] by fast
  thus ‹(t, X) ∈ ℱ (P ;✓ (λr. Q r ;✓ R))›
  proof cases
    case F_P_Q
    from F_P_Q(1, 3) ‹t ∉ 𝒟 (P ;✓ Q ;✓ R)› have ‹t' ∉ 𝒟 (P ;✓ Q)›
      by (simp add: Seqptick_projs) (metis front_tickFree_Nil self_append_conv)
    with F_P_Q(2) consider (F_P) t'' where ‹t' = map (ev ∘ of_ev) t''›
      ‹(t'', ref_Seqptick (ref_Seqptick X :: ('a, 's) refusalptick)) ∈ ℱ P› ‹tF t''›
    | (F_Q) t'' r u where ‹t' = map (ev ∘ of_ev) t'' @ u› ‹t'' @ [✓(r)] ∈ 𝒯 P› ‹tF t''›
      ‹(u, ref_Seqptick X) ∈ ℱ (Q r)›
      unfolding Seqptick_projs by fast
    thus ‹(t, X) ∈ ℱ (P ;✓ (λr. Q r ;✓ R))›
    proof cases
      case F_P
      from F_P(2, 3) have ‹(t'',ref_Seqptick X) ∈ ℱ P›
        by (simp add: ref_Seqptick_idem)
      moreover have ‹t = map (ev ∘ of_ev) t''›
        by (simp add: F_P_Q(1) F_P(1))
      ultimately show ‹(t, X) ∈ ℱ (P ;✓ (λr. Q r ;✓ R))›
        by (auto simp add: Seqptick_projs[of P] F_P(3))
    next
      case F_Q
      from F_P_Q(3) F_Q(1, 4) have ‹(map (ev ∘ of_ev) u, X) ∈ ℱ (Q r ;✓ R)›
        by (auto simp add: Seqptick_projs)
      with F_Q(2, 3) show ‹(t, X) ∈ ℱ (P ;✓ (λr. Q r ;✓ R))›
        by (auto simp add: Seqptick_projs[of P] F_P_Q(1) F_Q(1))
    qed
  next
    case F_R
    from F_R(2) consider (T_P) t'' r u' where ‹t' = map (ev ∘ of_ev) t'' @ u'›
      ‹t'' @ [✓(r)] ∈ 𝒯 P› ‹tF t''› ‹u' @ [✓(s)] ∈ 𝒯 (Q r)›
    | (D_P) t'' u' where ‹t' = map (ev ∘ of_ev) t'' @ u'› ‹t'' ∈ 𝒟 P› ‹tF t''› ‹tF u'›
      by (auto simp add: Seqptick_projs append_eq_append_conv2 Cons_eq_append_conv)
        (auto simp add: append_eq_map_conv front_tickFree_append_iff intro: D_P T_P)
    thus ‹(t, X) ∈ ℱ (P ;✓ (λr. Q r ;✓ R))›
    proof cases
      case T_P
      with F_R(3, 4) T_P(1, 4) have ‹(map (ev ∘ of_ev) u' @ u, X) ∈ ℱ (Q r ;✓ R)›
        by (auto simp add: Seqptick_projs)
      with T_P(2, 3) show ‹(t, X) ∈ ℱ (P ;✓ (λr. Q r ;✓ R))›
        by (auto simp add: Seqptick_projs[of P] F_R(1) T_P(1))
    next
      case D_P
      with D_P(2,3) F_R(4) have ‹t ∈ 𝒟 (P ;✓ (λr. Q r ;✓ R))›
        by (simp add: Seqptick_projs F_R(1) D_P(1))
          (metis F_imp_front_tickFree front_tickFree_append tickFree_map_ev_comp)
      thus ‹(t, X) ∈ ℱ (P ;✓ (λr. Q r ;✓ R))› by (fact is_processT8)
    qed
  qed
qed



(*<*)
end
  (*>*)