Theory Multi_Synchronization_Product_Generalized

(***********************************************************************************
 * 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
 ***********************************************************************************)

(*<*)
theory Multi_Synchronization_Product_Generalized
  imports Synchronization_Product_Generalized_Interpretations
    "HOL-Combinatorics.List_Permutation"
begin
  (*>*)


unbundle no funcset_syntax
  ― ‹Inherited from theory‹HOL-Combinatorics.List_Permutation›.›


section ‹Synchronization Product›

subsection ‹Definition›

text (in Syncptick_comm_locale) ‹
The generalized synchronization product is not
really commutative (see @{thm Syncptick_commute[no_vars]}).
We therefore define the architectural version on a list.›

fun MultiSyncptick ::
  ‹['a set, 'b list, 'b ⇒ ('a, 'r) processptick] ⇒ ('a, 'r list) processptick›
  where ‹MultiSyncptick S [] P = STOP›
  |     ‹MultiSyncptick S [l] P = RenamingTick (P l) (λr. [r])›
  |     ‹MultiSyncptick S (l # m # L) P = P l ⟦S⟧✓Rlist MultiSyncptick S (m # L) P›


syntax "_MultiSyncptick" ::
  ‹[pttrn, 'a set, 'b list, ('a, 'r) processptick] ⇒ ('a, 'r) processptick›
  (‹(3⟦_⟧✓ _ ∈@ _./ _)› [78,78,78,77] 77)
syntax_consts "_MultiSyncptick" ⇌ MultiSyncptick
translations "⟦S⟧✓ l ∈@ L. P" ⇌ "CONST MultiSyncptick S L (λl. P)"



text ‹Special case of term‹MultiSyncptick S P› when term‹S = {}›.›

abbreviation MultiInterptick ::
  ‹['b list, 'b ⇒ ('a, 'r) processptick] ⇒ ('a, 'r list) processptick›
  where ‹MultiInterptick L P ≡ MultiSyncptick {} L P› 

syntax "_MultiInterptick" ::
  ‹[pttrn, 'b list, ('a, 'r) processptick] ⇒ ('a, 'r) processptick›
  (‹(3|||✓ _∈@_./ _)› [78,78,77] 77)
syntax_consts "_MultiInterptick" ⇌ MultiInterptick
translations "|||✓ l ∈@ L. P" ⇌ "CONST MultiInterptick L (λl. P)"



text ‹Special case of term‹MultiSyncptick S P› when term‹S = UNIV›.›

abbreviation MultiParptick ::
  ‹['b list, 'b ⇒ ('a, 'r) processptick] ⇒ ('a, 'r list) processptick›
  where ‹MultiParptick L P ≡ MultiSyncptick UNIV L P› 

syntax "_MultiParptick" ::
  ‹[pttrn, 'b list, ('a, 'r) processptick] ⇒ ('a, 'r) processptick›
  (‹(3||✓ _∈@_./ _)› [78,78,77] 77)
syntax_consts "_MultiParptick" ⇌ MultiParptick
translations "||✓ l ∈@ L. P" ⇌ "CONST MultiParptick L (λl. P)"



subsection ‹First properties›

lemma is_ticks_length_MultiSyncptick [is_ticks_length_intro] :
  ‹length✓⇘length L⇙(⟦S⟧✓ l ∈@ L. P l)›
  by (induct L rule: induct_list012)
    (simp_all add: is_ticks_length_STOP is_ticks_length_Renaming
      is_ticks_length_Suc_SyncRlist)


lemma MultiSyncptick_Cons :
  ‹⟦S⟧✓ m ∈@ (l # L). P m =
   (  if L = [] then RenamingTick (P l) (λr. [r])
    else P l ⟦S⟧✓Rlist ⟦S⟧✓ m ∈@ L. P m)›
  by (cases L) simp_all



lemma mono_MultiSyncptick_eq :
  ‹(⋀l. l ∈ set L ⟹ P l = Q l) ⟹ ⟦S⟧✓ l ∈@ L. P l = ⟦S⟧✓ l ∈@ L. Q l›
  by (induct L rule: induct_list012) simp_all

lemma mono_MultiSyncptick_eq2:
  ‹(⋀l. l ∈ set L ⟹ P (f l) = Q l) ⟹ ⟦S⟧✓ l ∈@ map f L. P l = ⟦S⟧✓ l ∈@ L. Q l›
  by (induct L rule: induct_list012) simp_all



― ‹Some tests›
lemma ‹(⟦S⟧✓ l ∈@ []. P l) = STOP› 
  and ‹(⟦S⟧✓ l ∈@ [a]. P l) = RenamingTick (P a) (λr. [r])› 
  and ‹(⟦S⟧✓ l ∈@ [a, b]. P l) = P a ⟦S⟧✓Rlist RenamingTick (P b) (λr. [r])›  
  and ‹(⟦S⟧✓ l ∈@ [a, b, c]. P l) = P a ⟦S⟧✓Rlist (P b ⟦S⟧✓Rlist RenamingTick (P c) (λr. [r]))›    
  by simp_all



subsection ‹Properties›

lemma MultiSyncptick_is_BOT_iff:
  ‹⟦S⟧✓ l ∈@ L. P l = ⊥ ⟷ (∃l ∈ set L. P l = ⊥)›
  by (induct L rule: induct_list012)
    (simp_all add: Renaming_is_BOT_iff SyncRlist.Syncptick_is_BOT_iff)


lemma MultiSyncptick_BOT_absorb:
  ‹l ∈ set L ⟹ P l = ⊥ ⟹ ⟦S⟧✓ l ∈@ L. P l = ⊥›
  using MultiSyncptick_is_BOT_iff by blast


lemma MultiSyncptick_SKIP_id :
  ‹⟦S⟧✓ r ∈@ L. SKIP r = (if L = [] then STOP else SKIP L)›
  by (induct L rule: induct_list012) simp_all



subsection ‹Behaviour with binary version›

lemma MultiSyncptick_append :
  ‹L1 ≠ [] ⟹ L2 ≠ [] ⟹
   ⟦S⟧✓ l ∈@ (L1 @ L2). P l =
   ⟦S⟧✓ l ∈@ L1. P l ⇘length L1⇙⟦S⟧✓⇘length L2⇙ ⟦S⟧✓ l ∈@ L2. P l›
proof (induct L1 rule: list_nonempty_induct)
  case (single l) thus ?case
    by (simp add: is_ticks_length_MultiSyncptick MultiSyncptick_Cons flip: SyncRlist_to_SyncLists)
next
  let ?RT = ‹λP. RenamingTick P (λr. [r])›
  case (cons l L1)
  have ‹⟦S⟧✓ l ∈@ ((l # L1) @ L2). P l = P l ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (L1 @ L2). P l›
    by (simp add: MultiSyncptick_Cons ‹L1 ≠ []›)
  also have ‹… = ?RT (P l) ⇘Suc 0⇙⟦S⟧✓⇘length (L1 @ L2)⇙ ⟦S⟧✓ l ∈@ (L1 @ L2). P l›
    by (intro SyncRlist_to_SyncLists is_ticks_length_MultiSyncptick)
  also have ‹… = ?RT (P l) ⇘Suc 0⇙⟦S⟧✓⇘length L1 + length L2⇙
                  (⟦S⟧✓ l ∈@ L1. P l ⇘length L1⇙⟦S⟧✓⇘length L2⇙ ⟦S⟧✓ l ∈@ L2. P l)›
    using cons.hyps(2) cons.prems by simp
  also have ‹… = ?RT (P l) ⇘Suc 0⇙⟦S⟧✓⇘length L1⇙ ⟦S⟧✓ l ∈@ L1. P l
                  ⇘Suc 0 + length L1⇙⟦S⟧✓⇘length L2⇙ ⟦S⟧✓ l ∈@ L2. P l›
    by (simp add: SyncLists_assoc)
  also have ‹?RT (P l) ⇘Suc 0⇙⟦S⟧✓⇘length L1⇙ ⟦S⟧✓ l ∈@ L1. P l =
             P l ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ L1. P l›
    by (intro SyncRlist_to_SyncLists[symmetric] is_ticks_length_MultiSyncptick)
  also have ‹… = ⟦S⟧✓ l ∈@ (l # L1). P l›
    by (simp add: MultiSyncptick_Cons ‹L1 ≠ []›)
  finally show ?case by simp
qed



subsection ‹Behaviour with injectivity›

lemma inj_on_mapping_over_MultiSyncptick:
  ‹inj_on f (set L) ⟹ 
   ⟦S⟧✓ l ∈@ L. P l = ⟦S⟧✓ l ∈@ map f L. P (inv_into (set L) f l)›
proof (induct L rule: induct_list012)
  case (3 l' l'' L)
  have ‹⟦S⟧✓ l ∈@ (l' # l'' # L). P l =
        P l' ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l'' # L). P l› by simp
  also have ‹⟦S⟧✓ l ∈@ (l'' # L). P l =
             ⟦S⟧✓ l ∈@ map f (l'' # L). P (inv_into (set (l'' # L)) f l)›
    by (metis "3.hyps"(2) "3.prems" inj_on_insert list.simps(15))
  also have ‹… = ⟦S⟧✓ l ∈@ map f (l'' # L). P (inv_into (set (l' # l'' # L)) f l)›
    using "3.prems" by (auto intro!: mono_MultiSyncptick_eq)
  also have ‹P l' = P (inv_into (set (l' # l'' # L)) f (f l'))›
    using "3.prems" by auto
  finally show ?case by simp
qed simp_all



subsection ‹Permuting the Sequence›

subsubsection ‹A particular Case›

lemma MultiSyncptick_snoc :
  ‹⟦S⟧✓ m ∈@ (L @ [l]). P m =
   (  if L = [] then RenamingTick (P l) (λr. [r])
    else ⟦S⟧✓ m ∈@ L. P m ⟦S⟧✓Llist P l)›
  by (simp add: MultiSyncptick_append)
    (metis (lifting) ext SyncLlist_to_SyncLists is_ticks_length_MultiSyncptick)


text ‹
At the beginning, we wanted to prove the following property.
›

theorem MultiSyncptick_rev :
  ‹⟦S⟧✓ l ∈@ (rev L). P l = RenamingTick (⟦S⟧✓ l ∈@ L. P l) rev›
proof (induct L)
  case Nil show ?case by simp
next
  let ?RT = ‹RenamingTick›
  case (Cons l L)
  show ?case
  proof (cases ‹L = []›)
    show ‹L = [] ⟹ ?case› by (simp add: comp_def flip: Renaming_comp id_def)
  next
    assume ‹L ≠ []›
    have ‹⟦S⟧✓ m ∈@ (rev (l # L)). P m = ⟦S⟧✓ m ∈@ (rev L). P m ⟦S⟧✓Llist P l›
      by (simp add: MultiSyncptick_snoc ‹L ≠ []›)
    also have ‹… = ?RT (⟦S⟧✓ m ∈@ L. P m) rev ⟦S⟧✓Llist P l›
      by (simp only: Cons.hyps)
    also have ‹… = ?RT (⟦S⟧✓ m ∈@ L. P m) rev ⟦S⟧✓Llist ?RT (P l) id› by simp
    also have ‹… = Syncptick_locale.Syncptick (λr s. Some (rev r @ [s]))
                    (⟦S⟧✓ m ∈@ L. P m) S (P l)›
      by (subst SyncRlist.Syncptick_comm_locale_sym.inj_RenamingTick_Syncptick_inj_RenamingTick)
        simp_all
    also have ‹… = ?RT (P l ⟦S⟧✓Rlist ⟦S⟧✓ m ∈@ L. P m) rev›
    proof (subst SyncRlist.inj_on_RenamingTick_Syncptick)
      show ‹inj_on rev SyncRlist.range_tick_join› by simp
    next
      show ‹Syncptick_locale.Syncptick (λr s. Some (rev r @ [s])) (⟦S⟧✓ m ∈@ L. P m) S (P l) =
            Syncptick_locale.Syncptick
            (λr s. case Some (r # s) of None ⇒ None | Some r_s ⇒ Some (rev r_s))
            (P l) S (MultiSyncptick S L P)›
        by (subst Syncptick_locale.Syncptick_sym, simp_all)
          (unfold_locales, blast)
    qed
    also have ‹P l ⟦S⟧✓Rlist ⟦S⟧✓ m ∈@ L. P m = ⟦S⟧✓ m ∈@ (l # L). P m›
      by (simp add: MultiSyncptick_Cons ‹L ≠ []›)
    finally show ?case .
  qed
qed


text ‹
This has just been established for term‹rev L›,
which is a particular permutation of the list term‹L›.
It turns out that it actually holds for any permutation.
The rest of this file constitutes the proof.
›


subsubsection ‹Arbitrary Permutation›

paragraph ‹Some preliminary results›

lemma permute_list_transpose_eq_list_update :
  ‹i < length xs ⟹ j < length xs ⟹
   permute_list (Transposition.transpose i j) xs = xs[i := xs!j, j := xs!i]›
  by (auto simp add: permute_list_def transpose_def intro: nth_equalityI)

lemma inj_on_permute_list_transpose :
  ‹i < n ⟹ j < n ⟹ inj_on (permute_list (Transposition.transpose i j)) {xs. n ≤ length xs}›
  by (auto intro!: inj_onI simp add: permute_list_transpose_eq_list_update)
    (metis length_list_update nth_equalityI nth_list_update_eq nth_list_update_neq order_less_le_trans)

lemma rev_permute_list_transpose :
  ‹i < length L ⟹ j < length L ⟹
   rev (permute_list (Transposition.transpose i j) L) =
   permute_list (Transposition.transpose (length L - Suc i) (length L - Suc j)) (rev L)›
  by (simp add: permute_list_transpose_eq_list_update rev_nth rev_update)

lemma permute_list_transpose_rev :
  ‹i < length L ⟹ j < length L ⟹
   permute_list (Transposition.transpose i j) (rev L) =
   rev (permute_list (Transposition.transpose (length L - Suc i) (length L - Suc j)) L)›
  by (simp add: permute_list_transpose_eq_list_update rev_nth rev_update)


lemma tickFree_map_map_eventptick_id_eq :
  ‹tF t ⟹ map (map_eventptick id g) t = t›
  and tickFree_mem_T_RenamingTick_iff_mem_T :
  ‹tF t ⟹ t ∈ 𝒯 (RenamingTick P g) ⟷ t ∈ 𝒯 P›
  and tickFree_mem_D_RenamingTick_iff_mem_D :
  ‹tF t ⟹ t ∈ 𝒟 (RenamingTick P g) ⟷ t ∈ 𝒟 P›
  for P :: ‹('a, 'r) processptick› and g :: ‹'r ⇒ 'r›
    ― ‹Necessarily here, antecedents and images for term‹g› share the same type.›
proof -
  show * : ‹tF t ⟹ map (map_eventptick id g) t = t› for t :: ‹('a, 'r) traceptick›
    by (induct t) (auto simp add: is_ev_def)
  show ‹tF t ⟹ t ∈ 𝒯 (RenamingTick P g) ⟷ t ∈ 𝒯 P›
    by (auto simp add: T_Renaming "*" map_eventptick_tickFree D_T is_processT7)
  show ‹tF t ⟹ t ∈ 𝒟 (RenamingTick P g) ⟷ t ∈ 𝒟 P›
    by (auto simp add: D_Renaming "*" is_processT7)
      (metis "*" front_tickFree_Nil self_append_conv)
qed



paragraph ‹The proof›

text ‹
We start by proving that the const‹RenamingTick› of the right-hand side
process term‹Q› by a transposition can be ``taken to the outside''
of the synchronization term‹P ⟦S⟧✓Rlist Q›.
›

lemma SyncRlist_RenamingTick_permute_list_transpose :
  ‹P ⟦S⟧✓Rlist RenamingTick Q (permute_list (Transposition.transpose i j)) =
   RenamingTick (P ⟦S⟧✓Rlist Q) (permute_list (Transposition.transpose (Suc i) (Suc j)))›
  (is ‹?lhs = ?rhs›) if ‹i < n› ‹j < n› ‹⋀rs. rs ∈ ✓s(Q) ⟹ n ≤ length rs›
proof -
  let ?τ = Transposition.transpose
  let ?pl_τ = ‹λi j. permute_list (?τ i j)›
  let ?fun_evt = ‹λi j. map_eventptick id (?pl_τ i j)›
  let ?map_evt = ‹λi j. map (?fun_evt i j)›
  let ?RT = ‹λi j P. RenamingTick P (?pl_τ i j)›
  let ?tj = ‹λr s. ⌊r # s⌋›
  note map_eventptick_eq_iffs [simp] =
    ev_eq_map_eventptick_iff tick_eq_map_eventptick_iff
    map_eventptick_eq_ev_iff map_eventptick_eq_tick_iff
  have length_ge_eq_pl_τ_imp_eq : ‹r = r'›
    if ‹n ≤ length r› and ‹?pl_τ i j r = ?pl_τ i j r'› for r r' :: ‹'r list›
  proof -
    from ‹n ≤ length r› have ‹n ≤ length (?pl_τ i j r)› by simp
    with ‹?pl_τ i j r = ?pl_τ i j r'› have ‹n ≤ length r'› by simp
    have ‹inj_on (?pl_τ i j) {r. n ≤ length r}›
      by (simp add: ‹i < n› ‹j < n› inj_on_permute_list_transpose)
    with ‹n ≤ length r› ‹n ≤ length r'› ‹?pl_τ i j r = ?pl_τ i j r'›
    show ‹r = r'› by (auto dest: inj_onD)
  qed
  have pl_τ_pl_τ : ‹n ≤ length r ⟹ ?pl_τ i j (?pl_τ i j r) = r› for r :: ‹'r list›
    by (subst permute_list_compose[symmetric])
      (metis lessThan_iff order_less_le_trans permutes_swap_id ‹i < n› ‹j < n›, simp)
  have fun_evt_fun_evt :
    ‹(case e of ev a ⇒ True | ✓(r) ⇒ n ≤ length r) ⟹ ?fun_evt i j (?fun_evt i j e) = e›
    for e :: ‹('a, 'r list) eventptick›
    by (cases e) (simp_all add: pl_τ_pl_τ)
  have map_evt_map_evt :
    ‹(⋀e. e ∈ set t ⟹ case e of ev a ⇒ True | ✓(r) ⇒ n ≤ length r)
     ⟹ ?map_evt i j (?map_evt i j t) = t› for t :: ‹('a, 'r list) traceptick›
    by (induct t) (simp_all add: fun_evt_fun_evt)
  from ‹i < n› ‹j < n› have pl_τ_Cons :
    ‹n ≤ length s ⟹ ?pl_τ (Suc i) (Suc j) (r # s) = r # ?pl_τ i j s› for r and s :: ‹'r list›
    by (simp add: list_update_append1 nth_append_left permute_list_transpose_eq_list_update)
  show ‹?lhs = ?rhs›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    then obtain u v t_P t_Q where * : ‹t = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 (?RT i j Q) ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 (?RT i j Q)›
      unfolding SyncRlist.D_Syncptick by blast
    from tickFree_setinterleavesptick_iff[THEN iffD1, OF "*"(4, 2)] have ‹tF t_Q› ..
    with "*"(5) have ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      by (simp add: tickFree_mem_T_RenamingTick_iff_mem_T tickFree_mem_D_RenamingTick_iff_mem_D)
    with "*"(1-4) have ‹t ∈ 𝒟 (P ⟦S⟧✓Rlist Q)›
      by (auto simp add: SyncRlist.D_Syncptick)
    thus ‹t ∈ 𝒟 ?rhs›
      by (meson D_imp_front_tickFree div_butlast_when_non_tickFree_iff
          front_tickFree_iff_tickFree_butlast tickFree_mem_D_RenamingTick_iff_mem_D)
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then obtain t1 t2
      where * : ‹t = ?map_evt (Suc i) (Suc j) t1 @ t2› ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 (P ⟦S⟧✓Rlist Q)›
      by (auto simp add: D_Renaming)
    from "*"(1, 2) have ‹t = t1 @ t2›
      by (simp add: tickFree_map_map_eventptick_id_eq)
    from "*"(4) obtain u1 u2 t_P t_Q where ** : ‹t1 = u1 @ u2› ‹tF u1› ‹ftF u2›
      ‹u1 setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      unfolding SyncRlist.D_Syncptick by blast
    from tickFree_setinterleavesptick_iff[THEN iffD1, OF "**"(4, 2)] have ‹tF t_Q› ..
    with "**"(5) have ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 (?RT i j Q) ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 (?RT i j Q)›
      by (simp_all add: tickFree_mem_T_RenamingTick_iff_mem_T tickFree_mem_D_RenamingTick_iff_mem_D)
    with "**"(1-4) "*"(2, 3) ‹t = t1 @ t2› show ‹t ∈ 𝒟 ?lhs›
      by (auto simp add: SyncRlist.D_Syncptick intro: front_tickFree_append)
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs› ‹t ∉ 𝒟 ?lhs›
    then obtain t' where * : ‹t = ?map_evt (Suc i) (Suc j) t'›
      ‹(t', ?fun_evt (Suc i) (Suc j) -` X) ∈ ℱ (P ⟦S⟧✓Rlist Q)›
      unfolding Renaming_projs by blast
    from "*"(2) ‹t ∉ 𝒟 ?rhs› have ‹t' ∉ 𝒟 (P ⟦S⟧✓Rlist Q)›
      by (metis (no_types, lifting) "*"(1) D_imp_front_tickFree div_butlast_when_non_tickFree_iff
          front_tickFree_iff_tickFree_butlast map_butlast map_eventptick_tickFree
          tickFree_map_map_eventptick_id_eq tickFree_mem_D_RenamingTick_iff_mem_D)
    with "*"(2) obtain t_P t_Q X_P X_Q
      where ** : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t' setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)›
        ‹?fun_evt (Suc i) (Suc j) -` X ⊆ super_ref_Syncptick ?tj X_P S X_Q›
      unfolding SyncRlist.Syncptick_projs by force
    from "*"(2) consider ‹tF t'› | t'' rs where ‹tF t''› ‹t' = t'' @ [✓(rs)]›
      by (metis (lifting) F_T F_imp_front_tickFree T_nonTickFree_imp_decomp
          butlast_snoc front_tickFree_iff_tickFree_butlast)
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹tF t'›
      have ‹?map_evt (Suc i) (Suc j) t' = t'›
        by (simp add: ‹tF t'› tickFree_map_map_eventptick_id_eq)
      have ‹?map_evt i j t_Q = t_Q›
        using "**"(3) ‹tF t'› tickFree_map_map_eventptick_id_eq tickFree_setinterleavesptick_iff by blast
      define X_Q' where ‹X_Q' ≡ X_Q ∩ (range ev ∪ {✓(r) |r. n ≤ length r})›
      define X' where ‹X' ≡ X ∩ (range ev ∪ {✓(rs) |rs. Suc n ≤ length rs})›
      have ‹X_Q' ⊆ X_Q› unfolding X_Q'_def by blast
      with "**"(2) is_processT4 have ‹(t_Q, X_Q') ∈ ℱ Q› by blast
      moreover have ‹?fun_evt i j -` (?fun_evt i j ` X_Q') = X_Q'›
        by (auto simp add: X_Q'_def)
          (use length_ge_eq_pl_τ_imp_eq in blast)+
      moreover have ‹?map_evt i j t_Q = t_Q› by fact
      ultimately have ‹(t_Q, ?fun_evt i j ` X_Q') ∈ ℱ (?RT i j Q)›
        by (auto simp add: F_Renaming)
      moreover have ‹e ∈ X' ⟹ e ∈ super_ref_Syncptick ?tj X_P S (?fun_evt i j ` X_Q')› for e
        using "**"(4)[THEN set_mp, of ‹?fun_evt (Suc i) (Suc j) e›]
        unfolding X'_def X_Q'_def super_ref_Syncptick_def
        by (auto simp add: image_iff pl_τ_Cons) (use pl_τ_pl_τ in force)
      ultimately have ‹(t, X') ∈ ℱ ?lhs›
        by (simp add: SyncRlist.F_Syncptick)
          (metis "*"(1) "**"(1, 3) ‹?map_evt (Suc i) (Suc j) t' = t'› subsetI)
      moreover have ‹Suc n ≤ length (rs)› if ‹t @ [✓(rs)] ∈ 𝒯 ?lhs› for rs
      proof -
        from ‹t ∉ 𝒟 ?lhs› have ‹t @ [✓(rs)] ∉ 𝒟 ?lhs›
          by (meson is_processT9)
        with ‹t @ [✓(rs)] ∈ 𝒯 ?lhs›
        obtain t_P'' t_Q'' where "£" : ‹t_P'' ∈ 𝒯 P› ‹t_Q'' ∈ 𝒯 (?RT i j Q)›
          ‹t @ [✓(rs)] setinterleaves✓⇘λr s. ⌊r # s⌋⇙ ((t_P'', t_Q''), S)›
          unfolding SyncRlist.Syncptick_projs by blast
        from "£" obtain t_P''' t_Q''' r s
          where "££" : ‹rs = r # s› ‹t_P'' = t_P''' @ [✓(r)]› ‹t_Q'' = t_Q''' @ [✓(s)]›
            ‹t setinterleaves✓⇘λr s. ⌊r # s⌋⇙ ((t_P''', t_Q'''), S)›
          by (auto elim: snoc_tick_setinterleavesptickE)
        have ‹tF t_Q'''› using "£"(2) "££"(3) append_T_imp_tickFree by blast
        from ‹t ∉ 𝒟 ?lhs› "£"(1) "££"(2, 4) have ‹t_Q''' ∉ 𝒟 (?RT i j Q)›
          by (simp add: SyncRlist.D_Syncptick')
            (use front_tickFree_Nil is_processT3_TR_append in blast)
        with "£"(2) obtain t_Q''''
          where ‹?map_evt i j t_Q'''' = t_Q''' @ [✓(s)]› ‹t_Q'''' ∈ 𝒯 Q›
          by (simp add: Renaming_projs)
            (metis "££"(3) ‹t_Q''' ∉ 𝒟 (?RT i j Q)› is_processT7 is_processT9
              tickFree_map_map_eventptick_id_eq tickFree_mem_D_RenamingTick_iff_mem_D)
        then obtain s' where "£££" : ‹s = ?pl_τ i j s'› ‹t_Q''' @ [✓(s')] ∈ 𝒯 Q›
          by (auto simp add: map_eq_append_conv Cons_eq_map_conv
              append_T_imp_tickFree tickFree_map_map_eventptick_id_eq)
        have ‹s' ∈ ✓s(Q)›
          by (meson "£££"(2) ‹tF t_Q'''› ‹t_Q''' ∉ 𝒟 (?RT i j Q)› is_processT9
              strict_ticks_of_memI tickFree_mem_D_RenamingTick_iff_mem_D)
        with ‹⋀rs. rs ∈ ✓s(Q) ⟹ n ≤ length rs› have ‹n ≤ length s'› .
        with ‹s = ?pl_τ i j s'› have ‹n ≤ length s› by simp
        with ‹rs = r # s› show ‹Suc n ≤ length rs› by simp
      qed
      ultimately have ‹(t, X' ∪ (X ∩ {✓(rs) |rs. ¬ Suc n ≤ length rs})) ∈ ℱ ?lhs›
        using is_processT5_S7' by blast
      also have ‹X' ∪ (X ∩ {✓(rs) |rs. ¬ Suc n ≤ length rs}) = X›
        by (simp add: set_eq_iff X'_def image_iff) (meson eventptick.exhaust)
      finally show ‹(t, X) ∈ ℱ ?lhs› .
    next
      fix t'' rs assume ‹tF t''› ‹t' = t'' @ [✓(rs)]›
      from "**"(3) obtain t_P' t_Q' r s
        where *** : ‹r # s = rs›
          ‹t'' setinterleaves✓⇘?tj⇙ ((t_P', t_Q'), S)›
          ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
        by (auto elim: snoc_tick_setinterleavesptickE
            simp add: ‹t' = t'' @ [✓(rs)]› split: if_split_asm)
      have ‹n ≤ length s›
      proof -
        from "**"(1)[THEN F_T] "**"(3) ‹t' ∉ 𝒟 (P ⟦S⟧✓Rlist Q)› have ‹t_Q ∉ 𝒟 Q›
          by (simp add: SyncRlist.Syncptick_projs')
            (use front_tickFree_Nil in blast)
        with ‹(t_Q, X_Q) ∈ ℱ Q›[THEN F_T] have ‹s ∈ ✓s(Q)›
          by (simp add: "***"(4) strict_ticks_of_memI)
        with ‹⋀rs. rs ∈ ✓s(Q) ⟹ n ≤ length rs› show ‹n ≤ length s› .
      qed
      from ‹t'' setinterleaves✓⇘?tj⇙ ((t_P', t_Q'), S)›
      have ‹?map_evt (Suc i) (Suc j) t'' setinterleaves✓⇘?tj⇙ ((t_P', ?map_evt i j t_Q'), S)›
        by (metis (no_types, lifting) ‹tF t''› tickFree_map_map_eventptick_id_eq
            tickFree_setinterleavesptick_iff)
      from setinterleavesptick_snoc_tick
        [OF this, of r ‹?pl_τ i j s› ‹?pl_τ (Suc i) (Suc j) rs›] ‹n ≤ length s›
      have ‹?map_evt (Suc i) (Suc j) t' setinterleaves✓⇘?tj⇙ ((t_P, ?map_evt i j t_Q), S)›
        by (simp add: "***"(1, 3, 4) ‹t' = t'' @ [✓(rs)]›) (metis "***"(1) pl_τ_Cons)
      moreover from "**"(2)[THEN F_T] have ‹(?map_evt i j t_Q, UNIV) ∈ ℱ (?RT i j Q)›
        by (simp add: "***"(4), intro tick_T_F) (auto simp add: T_Renaming)
      moreover have ‹(t_P, UNIV) ∈ ℱ P›
        by (metis "**"(1) "***"(3) F_T tick_T_F)
      moreover have ‹e ∈ X ⟹ e ∈ super_ref_Syncptick ?tj UNIV S UNIV› for e
        using "**"(4)[THEN set_mp, of ‹?fun_evt (Suc i) (Suc j) e›]
        by (cases e) (auto simp add: super_ref_Syncptick_def)
      ultimately show ‹(t, X) ∈ ℱ ?lhs›
        using "*"(1) by (simp add: SyncRlist.F_Syncptick) blast
    qed
  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› ‹(t_Q, X_Q) ∈ ℱ (?RT i j Q)›
        ‹t setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Syncptick ?tj X_P S X_Q›
      unfolding SyncRlist.Syncptick_projs by force
    from "*"(1, 3) ‹t ∉ 𝒟 ?lhs› F_T front_tickFree_Nil
    have ‹t_Q ∉ 𝒟 (?RT i j Q)› unfolding SyncRlist.D_Syncptick' by blast
    with "*"(2) obtain t_Q' where ** : ‹t_Q = ?map_evt i j t_Q'› ‹(t_Q', ?fun_evt i j -` X_Q) ∈ ℱ Q›
      unfolding Renaming_projs by blast
    define X_Q' where ‹X_Q' ≡ X_Q ∩ (range ev ∪ {✓(rs) |rs. n ≤ length rs})›
    define X' where ‹X' ≡ X ∩ (range ev ∪ {✓(rs) |rs. Suc n ≤ length rs})›

    from ‹(t, X) ∈ ℱ ?lhs›[THEN F_T] consider ‹tF t› | t' rs where ‹tF t'› ‹t = t' @ [✓(rs)]›
      using T_nonTickFree_imp_decomp append_T_imp_tickFree by blast
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      assume ‹tF t›
      hence ‹?map_evt (Suc i) (Suc j) t = t›
        by (simp add: tickFree_map_map_eventptick_id_eq)
      have ‹?map_evt i j t_Q' = t_Q'›
        using "*"(3) "**"(1) ‹tF t› map_eventptick_tickFree tickFree_map_map_eventptick_id_eq
          tickFree_setinterleavesptick_iff by blast
      have ‹(t_Q, ?fun_evt i j -` X_Q) ∈ ℱ Q›
        by (simp add: "**"(1, 2) ‹?map_evt i j t_Q' = t_Q'›)
      hence ‹(t_Q, ?fun_evt i j -` X_Q') ∈ ℱ Q›
        by (simp add: X_Q'_def is_processT4)
      moreover have ‹(t_P, X_P) ∈ ℱ P› by (fact "*"(1))
      moreover have ‹t setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)› by (fact "*"(3))
      moreover have ‹e ∈ ?fun_evt (Suc i) (Suc j) -` X' ⟹
                     e ∈ super_ref_Syncptick ?tj X_P S (?fun_evt i j -` X_Q)› for e
        using set_mp[OF "*"(4), of ‹?fun_evt (Suc i) (Suc j) e›]
        by (auto simp add: super_ref_Syncptick_def X'_def pl_τ_Cons)
      ultimately have ‹(t, ?fun_evt (Suc i) (Suc j) -` X') ∈ ℱ (P ⟦S⟧✓Rlist Q)›
        by (unfold SyncRlist.F_Syncptick, clarify)
          (metis "**"(1, 2) ‹?map_evt i j t_Q' = t_Q'› subsetI)
      moreover have ‹Suc n ≤ length (rs)› if ‹t @ [✓(rs)] ∈ 𝒯 (P ⟦S⟧✓Rlist Q)› for rs
      proof -
        from ‹t ∉ 𝒟 ?lhs› have ‹t ∉ 𝒟 (P ⟦S⟧✓Rlist Q)›
          by (simp add: SyncRlist.D_Syncptick)
            (metis tickFree_mem_D_RenamingTick_iff_mem_D
              tickFree_mem_T_RenamingTick_iff_mem_T tickFree_setinterleavesptick_iff)
        hence ‹t @ [✓(rs)] ∉ 𝒟 (P ⟦S⟧✓Rlist Q)›
          by (meson is_processT9)
        with ‹t @ [✓(rs)] ∈ 𝒯 (P ⟦S⟧✓Rlist Q)›
        obtain t_P'' t_Q'' where "£" : ‹t_P'' ∈ 𝒯 P› ‹t_Q'' ∈ 𝒯 Q›
          ‹t @ [✓(rs)] setinterleaves✓⇘λr s. ⌊r # s⌋⇙ ((t_P'', t_Q''), S)›
          unfolding SyncRlist.Syncptick_projs by blast
        from "£" obtain t_P''' t_Q''' r s
          where "££" : ‹rs = r # s› ‹t_P'' = t_P''' @ [✓(r)]› ‹t_Q'' = t_Q''' @ [✓(s)]›
            ‹t setinterleaves✓⇘λr s. ⌊r # s⌋⇙ ((t_P''', t_Q'''), S)›
          by (auto elim: snoc_tick_setinterleavesptickE)
        from ‹t ∉ 𝒟 (P ⟦S⟧✓Rlist Q)› have ‹t_Q'' ∉ 𝒟 Q›
          by (simp add: SyncRlist.D_Syncptick')
            (metis "£"(1) "££"(2-4) append.right_neutral
              front_tickFree_Nil is_processT3_TR_append is_processT9)
        have ‹s ∈ ✓s(Q)›
          by (metis "£"(2) "££"(3) ‹t_Q'' ∉ 𝒟 Q› strict_ticks_of_memI)
        with ‹⋀rs. rs ∈ ✓s(Q) ⟹ n ≤ length rs› have ‹n ≤ length s› .
        thus ‹Suc n ≤ length rs› by (simp add: ‹rs = r # s›)
      qed
      ultimately have ‹(t, ?fun_evt (Suc i) (Suc j) -` X' ∪
                           ?fun_evt (Suc i) (Suc j) -`
                           (X ∩ {✓(rs) |rs. ¬ Suc n ≤ length rs})) ∈ ℱ (P ⟦S⟧✓Rlist Q)›
        using is_processT5_S7' by force
      also have ‹?fun_evt (Suc i) (Suc j) -` X' ∪
                 ?fun_evt (Suc i) (Suc j) -` (X ∩ {✓(rs) |rs. ¬ Suc n ≤ length rs}) =
                 ?fun_evt (Suc i) (Suc j) -` X›
        by (auto simp add: X'_def image_iff) (metis eventptick.exhaust)
      finally show ‹(t, X) ∈ ℱ ?rhs›
        using ‹?map_evt (Suc i) (Suc j) t = t› by (auto simp add: F_Renaming)
    next
      fix t' rs assume ‹tF t'› ‹t = t' @ [✓(rs)]›
      from "*"(3) obtain t_P'' t_Q'' r s
        where *** : ‹rs = r # s›
          ‹t' setinterleaves✓⇘?tj⇙ ((t_P'', t_Q''), S)›
          ‹t_P = t_P'' @ [✓(r)]› ‹t_Q = t_Q'' @ [✓(s)]›
          ‹tF t_P''› ‹tF t_Q''›
        by (auto elim!: snoc_tick_setinterleavesptickE
            simp add: ‹t = t' @ [✓(rs)]› split: if_split_asm)
          (metis ‹tF t'› tickFree_setinterleavesptick_iff)
      have ‹t_Q'' ∉ 𝒟 Q›
        by (metis "*"(2) "***"(4) F_imp_front_tickFree ‹t_Q ∉ 𝒟 (?RT i j Q)›
            front_tickFree_append_iff is_processT7 non_tickFree_tick
            tickFree_Nil tickFree_mem_D_RenamingTick_iff_mem_D)
      from "**"(1) "***"(4) obtain s' where ‹s = ?pl_τ i j s'›
        by (auto simp add: "**"(2) append_eq_map_conv Cons_eq_map_conv)
      with "**"(1) "**"(2)[THEN F_T] "***"(4) have ‹t_Q'' @ [✓(s')] ∈ 𝒯 Q›
        by (simp add: "***"(4) append_eq_map_conv Cons_eq_map_conv)
          (metis "***"(6) ‹t_Q'' ∉ 𝒟 Q› is_processT9 length_permute_list map_eventptick_tickFree
            pl_τ_pl_τ strict_ticks_of_memI that(3) tickFree_map_map_eventptick_id_eq)
      with ‹t_Q'' ∉ 𝒟 Q› have ‹s' ∈ ✓s(Q)›
        by (metis is_processT9 strict_ticks_of_memI)
      with ‹⋀rs. rs ∈ ✓s(Q) ⟹ n ≤ length rs› have ‹n ≤ length s'› .
      with ‹s = ?pl_τ i j s'› have ‹n ≤ length s› by simp
      hence ‹Suc n ≤ length rs› by (simp add: ‹rs = r # s›)

      have ‹?map_evt (Suc i) (Suc j) t setinterleaves✓⇘?tj⇙ ((t_P, ?map_evt i j t_Q), S)›
        by (simp add: "***"(1-3, 4, 6) ‹t = t' @ [✓(rs)]› ‹n ≤ length s› ‹tF t'› pl_τ_Cons
            setinterleavesptick_snoc_tick tickFree_map_map_eventptick_id_eq)
      moreover have ‹t_P ∈ 𝒯 P› using "*"(1) F_T by blast
      moreover from "*"(2)[THEN F_T] ‹n ≤ length s› have ‹?map_evt i j t_Q ∈ 𝒯 Q›
        by (auto simp add: T_Renaming "***"(4, 6) append_eq_map_conv Cons_eq_map_conv
            tickFree_map_map_eventptick_id_eq pl_τ_pl_τ)
          (metis append_T_imp_tickFree not_Cons_self2 tickFree_map_map_eventptick_id_eq,
            metis ‹t_Q'' ∉ 𝒟 Q› is_processT7 is_processT9)
      ultimately have ‹?map_evt (Suc i) (Suc j) t ∈ 𝒯 (P ⟦S⟧✓Rlist Q)›
        by (auto simp add: SyncRlist.T_Syncptick)
      with ‹n ≤ length s› have ‹t ∈ 𝒯 ?rhs›
        by (auto simp add: T_Renaming ‹t = t' @ [✓(rs)]› append_eq_map_conv Cons_eq_map_conv)
          (metis "***"(1) ‹tF t'› length_permute_list pl_τ_Cons pl_τ_pl_τ tickFree_map_map_eventptick_id_eq)
      thus ‹(t, X) ∈ ℱ ?rhs› by (simp add: ‹t = t' @ [✓(rs)]› tick_T_F)
    qed
  qed
qed



lemma RenamingTick_permute_list_transpose_SyncListslenL :
  ‹RenamingTick P (permute_list (Transposition.transpose i j)) ⇘n⇙⟦S⟧✓ListslenL Q =
   RenamingTick (P ⇘n⇙⟦S⟧✓ListslenL Q) (permute_list (Transposition.transpose i j))›
  (is ‹?lhs = ?rhs›) if ‹i < n› ‹j < n› for P :: ‹('a, 'r list) processptick›
proof -
  let ?pl = ‹permute_list (Transposition.transpose i j)›
  let ?fun_evt = ‹map_eventptick id (permute_list (Transposition.transpose i j))›
  let ?map_evt = ‹map ?fun_evt›
    and ?RT = ‹λP. RenamingTick P (permute_list (Transposition.transpose i j))›
    and ?tj = ‹λr s. if length r = n then ⌊r @ s⌋ else ◇›
  note map_eventptick_eq_iffs [simp] =
    ev_eq_map_eventptick_iff tick_eq_map_eventptick_iff map_eventptick_eq_ev_iff map_eventptick_eq_tick_iff
  have length_eq_pl_imp : ‹r = r'› if ‹n ≤ length r› and ‹?pl r = ?pl r'› for r r' :: ‹'r list›
  proof -
    from ‹n ≤ length r› have ‹n ≤ length (?pl r)› by simp
    with ‹?pl r = ?pl r'› have ‹n ≤ length r'› by simp
    have ‹inj_on ?pl {r. n ≤ length r}›
      by (simp add: ‹i < n› ‹j < n› inj_on_permute_list_transpose)
    with ‹n ≤ length r› ‹n ≤ length r'› ‹?pl r = ?pl r'›
    show ‹r = r'› by (auto dest: inj_onD)
  qed
  have pl_pl : ‹n ≤ length r ⟹ ?pl (?pl r) = r› for r :: ‹'r list›
    by (subst permute_list_compose[symmetric])
      (metis lessThan_iff order_less_le_trans permutes_swap_id ‹i < n› ‹j < n›, simp)
  have fun_evt_fun_evt :
    ‹(case e of ev a ⇒ True | ✓(r) ⇒ n ≤ length r) ⟹ ?fun_evt (?fun_evt e) = e›
    for e :: ‹('a, 'r list) eventptick›
    by (cases e) (simp_all add: pl_pl)
  have map_evt_map_evt :
    ‹(⋀e. e ∈ set t ⟹ case e of ev a ⇒ True | ✓(r) ⇒ n ≤ length r)
     ⟹ ?map_evt (?map_evt t) = t› for t :: ‹('a, 'r list) traceptick›
    by (induct t) (simp_all add: fun_evt_fun_evt)
  from ‹i < n› ‹j < n› have pl_append :
    ‹n ≤ length r ⟹ ?pl (r @ r') = ?pl r @ r'› for r r' :: ‹'r list›
    by (simp add: list_update_append1 nth_append_left permute_list_transpose_eq_list_update)

  show ‹?lhs = ?rhs›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    then obtain u v t_P t_Q where * : ‹t = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 (?RT P) ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 (?RT P) ∧ t_Q ∈ 𝒟 Q›
      unfolding SyncListslenL.D_Syncptick by blast
    from tickFree_setinterleavesptick_iff[THEN iffD1, OF "*"(4, 2)] have ‹tF t_P› ..
    with "*"(5) have ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      by (simp_all add: tickFree_mem_T_RenamingTick_iff_mem_T tickFree_mem_D_RenamingTick_iff_mem_D)
    with "*"(1-4) have ‹t ∈ 𝒟 (P ⇘n⇙⟦S⟧✓ListslenL Q)›
      by (auto simp add: SyncListslenL.D_Syncptick)
    thus ‹t ∈ 𝒟 ?rhs›
      by (meson D_imp_front_tickFree div_butlast_when_non_tickFree_iff
          front_tickFree_iff_tickFree_butlast tickFree_mem_D_RenamingTick_iff_mem_D)
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then obtain t1 t2
      where * : ‹t = ?map_evt t1 @ t2› ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 (P ⇘n⇙⟦S⟧✓ListslenL Q)›
      by (auto simp add: D_Renaming)
    from "*"(1, 2) have ‹t = t1 @ t2›
      by (simp add: tickFree_map_map_eventptick_id_eq)
    from "*"(4) obtain u1 u2 t_P t_Q where ** : ‹t1 = u1 @ u2› ‹tF u1› ‹ftF u2›
      ‹u1 setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      unfolding SyncListslenL.D_Syncptick by blast
    from tickFree_setinterleavesptick_iff[THEN iffD1, OF "**"(4, 2)] have ‹tF t_P› ..
    with "**"(5) have ‹t_P ∈ 𝒟 (?RT P) ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 (?RT P) ∧ t_Q ∈ 𝒟 Q›
      by (simp_all add: tickFree_mem_T_RenamingTick_iff_mem_T tickFree_mem_D_RenamingTick_iff_mem_D)
    with "**"(1-4) "*"(2, 3) ‹t = t1 @ t2› show ‹t ∈ 𝒟 ?lhs›
      by (auto simp add: SyncListslenL.D_Syncptick intro: front_tickFree_append)
  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) ∈ ℱ (?RT P)› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Syncptick ?tj X_P S X_Q›
      unfolding SyncListslenL.Syncptick_projs by force
    from "*"(2, 3) ‹t ∉ 𝒟 ?lhs› F_T front_tickFree_Nil
    have ‹t_P ∉ 𝒟 (?RT P)› unfolding SyncListslenL.D_Syncptick' by blast
    with "*"(1) obtain t_P' where ** : ‹t_P = ?map_evt t_P'› ‹(t_P', ?fun_evt -` X_P) ∈ ℱ P›
      unfolding Renaming_projs by blast
    from ‹(t, X) ∈ ℱ ?lhs›[THEN F_T] consider ‹tF t› | t' rs where ‹tF t'› ‹t = t' @ [✓(rs)]›
      using T_nonTickFree_imp_decomp append_T_imp_tickFree by blast
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      assume ‹tF t›
      hence ‹?map_evt t = t›
        by (simp add: tickFree_map_map_eventptick_id_eq)
      have ‹?map_evt t_P' = t_P'›
        using "*"(3) "**"(1) ‹tF t› map_eventptick_tickFree tickFree_map_map_eventptick_id_eq
          tickFree_setinterleavesptick_iff by blast
      have ‹(t_P, ?fun_evt -` X_P) ∈ ℱ P›
        by (simp add: "**"(1,2) ‹?map_evt t_P' = t_P'›)
      moreover have ‹(t_Q, X_Q) ∈ ℱ Q› by (fact "*"(2))
      moreover have ‹t setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)› by (fact "*"(3))
      moreover have ‹e ∈ ?fun_evt -` X ⟹ e ∈ super_ref_Syncptick ?tj (?fun_evt -` X_P) S X_Q› for e
        using "*"(4)[THEN set_mp, of ‹?fun_evt e›]
        by (cases e, auto simp add: super_ref_Syncptick_def split: if_split_asm)
          (metis append_eq_append_conv dual_order.refl length_permute_list pl_append,
            metis append_eq_append_conv dual_order.refl length_permute_list pl_append,
            metis dual_order.refl length_permute_list pl_append)
      ultimately have ‹(t, ?fun_evt -` X) ∈ ℱ (P ⇘n⇙⟦S⟧✓ListslenL Q)›
        by (simp add: SyncListslenL.F_Syncptick) blast
      with ‹?map_evt t = t› show ‹(t, X) ∈ ℱ ?rhs›
        by (auto simp add: F_Renaming)
    next
      fix t' rs assume ‹tF t'› ‹t = t' @ [✓(rs)]›
      from "*"(3) obtain t_P'' t_Q'' r s
        where *** : ‹length r = n› ‹r @ s = rs›
          ‹t' setinterleaves✓⇘?tj⇙ ((t_P'', t_Q''), S)›
          ‹t_P = t_P'' @ [✓(r)]› ‹t_Q = t_Q'' @ [✓(s)]›
        by (auto elim: snoc_tick_setinterleavesptickE
            simp add: ‹t = t' @ [✓(rs)]› split: if_split_asm)
      have ‹?pl r @ s = ?pl rs› using "***"(1, 2) pl_append by force
      from ‹t' setinterleaves✓⇘?tj⇙ ((t_P'', t_Q''), S)›
      have ‹?map_evt t' setinterleaves✓⇘?tj⇙ ((?map_evt t_P'', t_Q''), S)›
        by (metis (no_types, lifting) ‹tF t'› tickFree_map_map_eventptick_id_eq
            tickFree_setinterleavesptick_iff)
      have ‹case e of ev a ⇒ True | ✓(r) ⇒ n ≤ length r› if ‹e ∈ set t_P'› for e
      proof -
        have ‹tF t_P''›
          using "***"(3) ‹tF t'› tickFree_setinterleavesptick_iff by blast
        hence ‹e ∈ set t_P'' ⟹ is_ev e› for e
          by (metis in_set_conv_decomp tickFree_Cons_iff tickFree_append_iff)
        moreover from ‹e ∈ set t_P'› have ‹?fun_evt e ∈ set t_P›
          by (simp add: "**"(1))
        ultimately show ‹case e of ev a ⇒ True | ✓(r) ⇒ n ≤ length r›
          using "***"(1) by (cases e, auto simp add: "***"(4)) (metis eventptick.disc(2))
      qed
      with arg_cong[OF "**"(1), where f = ?map_evt] map_evt_map_evt
      have ‹?map_evt t_P = t_P'› by presburger
      with "**" have ‹?map_evt t_P ∈ 𝒯 P› by (simp add: F_T)
      moreover have ‹t_Q ∈ 𝒯 Q› using "*"(2) F_T by blast
      moreover from ‹?map_evt t' setinterleaves✓⇘?tj⇙ ((?map_evt t_P'', t_Q''), S)›
      have ‹?map_evt t setinterleaves✓⇘?tj⇙ ((?map_evt t_P, t_Q), S)›
        by (simp add: ‹t = t' @ [✓(rs)]› "***"(1, 4, 5)
            ‹?pl r @ s = ?pl rs› setinterleavesptick_snoc_tick)
      ultimately have ‹?map_evt t ∈ 𝒯 (P ⇘n⇙⟦S⟧✓ListslenL Q)›
        unfolding SyncListslenL.T_Syncptick by blast
      hence ‹?map_evt (?map_evt t) ∈ 𝒯 ?rhs›
        by (auto simp add: T_Renaming)
      also have ‹?map_evt (?map_evt t) = t›
        by (simp add: ‹t = t' @ [✓(rs)]› )
          (metis "***"(1, 2) ‹tF t'› dual_order.refl length_permute_list
            list.map_comp pl_append pl_pl tickFree_map_map_eventptick_id_eq)
      finally show ‹(t, X) ∈ ℱ ?rhs› by (simp add: ‹t = t' @ [✓(rs)]› tick_T_F)
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs› ‹t ∉ 𝒟 ?lhs›
    then obtain t' where * : ‹t = ?map_evt t'›
      ‹(t', ?fun_evt -` X) ∈ ℱ (P ⇘n⇙⟦S⟧✓ListslenL Q)›
      unfolding Renaming_projs by blast
    from "*"(2) ‹t ∉ 𝒟 ?rhs› have ‹t' ∉ 𝒟 (P ⇘n⇙⟦S⟧✓ListslenL Q)›
      by (metis (no_types, lifting) "*"(1) D_imp_front_tickFree div_butlast_when_non_tickFree_iff
          front_tickFree_iff_tickFree_butlast map_butlast map_eventptick_tickFree
          tickFree_map_map_eventptick_id_eq tickFree_mem_D_RenamingTick_iff_mem_D)
    with "*"(2) obtain t_P t_Q X_P X_Q
      where ** : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t' setinterleaves✓⇘?tj⇙ ((t_P, t_Q), S)›
        ‹?fun_evt -` X ⊆ super_ref_Syncptick ?tj X_P S X_Q›
      unfolding SyncListslenL.Syncptick_projs by force
    from "*"(2) consider ‹tF t'› | t'' rs where ‹tF t''› ‹t' = t'' @ [✓(rs)]›
      by (metis (lifting) F_T F_imp_front_tickFree T_nonTickFree_imp_decomp
          butlast_snoc front_tickFree_iff_tickFree_butlast)
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹tF t'›
      have ‹?map_evt t' setinterleaves✓⇘?tj⇙ ((?map_evt t_P, t_Q), S)›
        by (metis (lifting) "**"(3) ‹tF t'› tickFree_map_map_eventptick_id_eq
            tickFree_setinterleavesptick_iff)

      define X_P' where ‹X_P' ≡ X_P ∩ (range ev ∪ {✓(r) |r. length r = n})›
      define X' where ‹X' ≡ X ∩ (range ev ∪ {✓(rs) |rs. n ≤ length rs})›
      have ‹X_P' ⊆ X_P› unfolding X_P'_def by blast
      with "**"(1) is_processT4 have ‹(t_P, X_P') ∈ ℱ P› by blast
      moreover have ‹?fun_evt -` (?fun_evt ` X_P') = X_P'›
        by (auto simp add: X_P'_def) (use length_eq_pl_imp in blast)+
      moreover have ‹?map_evt t_P = t_P›
        using "**"(3) ‹tF t'› tickFree_map_map_eventptick_id_eq tickFree_setinterleavesptick_iff by blast
      ultimately have ‹(t_P, ?fun_evt ` X_P') ∈ ℱ (?RT P)›
        by (auto simp add: F_Renaming)
      moreover have ‹e ∈ X' ⟹ e ∈ super_ref_Syncptick ?tj (?fun_evt ` X_P') S X_Q› if ‹e ∈ X'› for e
        using "**"(4)[THEN set_mp, of ‹?fun_evt e›] fun_evt_fun_evt[of e]
        unfolding X'_def X_P'_def super_ref_Syncptick_def
        by (auto simp add: image_iff pl_append split: if_split_asm)
          (metis (mono_tags, lifting) Int_iff Un_iff length_permute_list mem_Collect_eq,
            blast, metis length_permute_list)
      ultimately have ‹(t, X') ∈ ℱ ?lhs›
        by (simp add: SyncListslenL.F_Syncptick)
          (metis (lifting) "*"(1) "**"(2, 3) ‹tF t'› subsetI tickFree_map_map_eventptick_id_eq)
      moreover from ‹t ∉ 𝒟 ?lhs› have ‹t @ [✓(rs)] ∈ 𝒯 ?lhs ⟹ n ≤ length (rs)› for rs
        by (auto simp add: SyncListslenL.Syncptick_projs
            elim!: snoc_tick_setinterleavesptickE split: if_split_asm)
          (metis (no_types, lifting) append.assoc butlast_snoc front_tickFree_charn 
            non_tickFree_tick tickFree_Nil tickFree_append_iff tickFree_imp_front_tickFree)+
      ultimately have ‹(t, X' ∪ (X ∩ {✓(rs) |rs. ¬ n ≤ length rs})) ∈ ℱ ?lhs›
        using is_processT5_S7' by fastforce
      also have ‹X' ∪ (X ∩ {✓(rs) |rs. ¬ n ≤ length rs}) = X›
        by (simp add: set_eq_iff X'_def image_iff) (meson eventptick.exhaust)
      finally show ‹(t, X) ∈ ℱ ?lhs› .
    next
      fix t'' rs assume ‹tF t''› ‹t' = t'' @ [✓(rs)]›
      from "**"(3) obtain t_P' t_Q' r s
        where *** : ‹length r = n› ‹r @ s = rs›
          ‹t'' setinterleaves✓⇘?tj⇙ ((t_P', t_Q'), S)›
          ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
        by (auto elim: snoc_tick_setinterleavesptickE
            simp add: ‹t' = t'' @ [✓(rs)]› split: if_split_asm)
      have ‹?pl r @ s = ?pl rs›
        using "***"(1, 2) pl_append by force
      from ‹t'' setinterleaves✓⇘?tj⇙ ((t_P', t_Q'), S)›
      have ‹?map_evt t'' setinterleaves✓⇘?tj⇙ ((?map_evt t_P', t_Q'), S)›
        by (metis (no_types, lifting) ‹tF t''› tickFree_map_map_eventptick_id_eq
            tickFree_setinterleavesptick_iff)
      from setinterleavesptick_snoc_tick[OF this, of ‹?pl r› s ‹?pl rs›]
      have ‹?map_evt t' setinterleaves✓⇘?tj⇙ ((?map_evt t_P, t_Q), S)›
        by (simp add: "***"(1, 4, 5) ‹t' = t'' @ [✓(rs)]› ‹?pl r @ s = ?pl rs›)
      moreover from "**"(1)[THEN F_T] have ‹(?map_evt t_P, UNIV) ∈ ℱ (?RT P)›
        by (simp add: "***"(4), intro tick_T_F) (auto simp add: T_Renaming)
      moreover have ‹(t_Q, UNIV) ∈ ℱ Q›
        by (metis "**"(2) "***"(5) F_T tick_T_F)
      moreover have ‹e ∈ X ⟹ e ∈ super_ref_Syncptick ?tj UNIV S UNIV› for e
        using "**"(4)[THEN set_mp, of ‹?fun_evt e›]
        by (cases e) (auto simp add: super_ref_Syncptick_def)
      ultimately show ‹(t, X) ∈ ℱ ?lhs›
        using "*"(1) by (simp add: SyncListslenL.F_Syncptick) blast
    qed
  qed
qed




text ‹Then, we establish the result when the permutation is only a transposition.›

lemma MultiSyncptick_permute_list_transpose :
  ‹i < length L ⟹ j < length L ⟹
   ⟦S⟧✓ l ∈@ permute_list (Transposition.transpose i j) L. P l =
   RenamingTick (⟦S⟧✓ l ∈@ L. P l) (permute_list (Transposition.transpose i j))›
  for L :: ‹'b list›
proof -
  let ?RT = RenamingTick and ?MS = ‹λL. ⟦S⟧✓ l ∈@ L. P l›
  let ?RS = ‹λL. ⟦S⟧✓ l ∈@ L. P l›
  let ?τ = ‹Transposition.transpose›
  let ?pl_τ = ‹λi j. permute_list (?τ i j)›
  have custom_nat_induct [case_names 0 1 2 Suc] :
    ‹thesis 0 ⟹ thesis 1 ⟹ thesis 2 ⟹
     (⋀n. 2 ≤ n ⟹ (⋀k. k ≤ n ⟹ thesis k) ⟹ thesis (Suc n)) ⟹ thesis n› for thesis n
    by (metis One_nat_def Suc_1 less_2_cases linorder_not_le strong_nat_induct)
  have * : ‹i ≤ j ⟹ i < length L ⟹ j < length L ⟹
            ?RS (?pl_τ i j L) = ?RT (?RS L) (?pl_τ i j)› for i j
  proof (induct ‹length L› arbitrary: i j L rule: custom_nat_induct)
    case 0 thus ?case by simp
  next
    case 1 thus ?case by (cases L) simp_all
  next
    case 2
    from "2.hyps" "2.prems"(1, 3) consider ‹i = j› | ‹i = 0› ‹j = 1› by linarith
    thus ?case
    proof cases
      show ‹i = j ⟹ ?case› by simp
    next
      let ?g = ‹λrs. if rs = [] then [] else last rs # butlast rs›
      assume ‹i = 0› ‹j = 1›
      moreover obtain l1 l2 where ‹L = [l1, l2]›
        by (metis "2.hyps" One_nat_def Suc_1 diff_Suc_1' length_tl lessI
            list.exhaust_sel nat_less_le order.refl take0 take_all_iff)
      ultimately have ‹?MS (?pl_τ i j L) = P l2 ⟦S⟧✓Rlist ?RT (P l1) (λr. [r])›
        by (simp add: permute_list_transpose_eq_list_update)
      also have ‹… = ?RT (?RT (P l1) (λr. [r]) ⟦S⟧✓Llist P l2) ?g›
        by (simp add: SyncRlist.Syncptick_comm_locale_sym.Syncptick_commute)
      also have ‹... = ?RT (?MS L) ?g›
        by (simp add: ‹L = [l1, l2]› MultiSyncptick_snoc[of _ ‹[l1]›, simplified])
      also have ‹… = ?RT (?MS L) (?pl_τ i j)›
      proof (rule RenamingTick_is_restrictable_on_strict_ticks_of)
        fix rs assume ‹rs ∈ ✓s(?MS L)›
        from is_ticks_lengthD is_ticks_length_MultiSyncptick this
        have ‹length rs = length L› .
        thus ‹?g rs = ?pl_τ i j rs›
          by (cases rs; cases ‹tl rs›)
            (simp_all add: ‹L = [l1, l2]› ‹i = 0› ‹j = 1›
              permute_list_transpose_eq_list_update)
      qed
      finally show ?case .
    qed
  next
    case (Suc n)
    show ?case
    proof (cases ‹i = j›)
      show ‹i = j ⟹ ?case›
        by simp (metis RenamingTick_id eq_id_iff permute_list_id)
    next
      assume ‹i ≠ j› hence ‹i < j›
        by (simp add: Suc.prems(1) nat_less_le)

      { fix i j L l0 l1 and L' :: ‹'b list›
        assume ‹i ≠ 0› ‹i < j› ‹i < length L› ‹j < length L› ‹Suc n = length L› ‹L = l0 # l1 # L'›
        with ‹i < length L› ‹j < length L› ‹i < j› ‹i ≠ 0›
        have * : ‹i - 1 < j - 1› ‹i - 1 < length (l1 # L')›
          ‹j - 1 < length (l1 # L')› by auto
        have ‹?pl_τ i j L = l0 # ?pl_τ (i - 1) (j - 1) (l1 # L')›
        proof (subst (1 2) permute_list_transpose_eq_list_update)
          show ‹i - 1 < length (l1 # L')› ‹j - 1 < length (l1 # L')›
            ‹i < length L› ‹j < length L›
            by (fact "*"(2, 3) ‹i < length L› ‹j < length L›)+
        next
          from "*" ‹i ≠ 0›
          show ‹L[i := L ! j, j := L ! i] =
                l0 # (l1 # L')[i - 1 := (l1 # L') ! (j - 1), j - 1 := (l1 # L') ! (i - 1)]›
            by (cases i; cases j) (simp_all add: ‹L = l0 # l1 # L'› nat.case_eq_if)
        qed
        hence ‹?MS (?pl_τ i j L) = P l0 ⟦S⟧✓Rlist ?MS (?pl_τ (i - 1) (j - 1) (l1 # L'))›
          by (simp add: MultiSyncptick_Cons)
            (metis Zero_not_Suc length_Cons length_permute_list list.size(3))
        also have ‹?MS (?pl_τ (i - 1) (j - 1) (l1 # L')) =
                   ?RT (?MS (l1 # L')) (?pl_τ (i - 1) (j - 1))›
          by (subst "Suc.hyps") 
            (use "*" ‹Suc n = length L› ‹L = l0 # l1 # L'› in simp_all)
        also have ‹P l0 ⟦S⟧✓Rlist ?RT (?MS (l1 # L')) (?pl_τ (i - 1) (j - 1)) =
                 ?RT (P l0 ⟦S⟧✓Rlist ?MS (l1 # L')) (?pl_τ (Suc (i - 1)) (Suc (j - 1)))›
          by (rule SyncRlist_RenamingTick_permute_list_transpose[OF "*"(2, 3)])
            (metis is_ticks_lengthD is_ticks_length_MultiSyncptick order_le_less)
        also have ‹(Suc (i - 1)) = i› using ‹i ≠ 0› by simp
        also have ‹(Suc (j - 1)) = j› using "*"(1) by linarith
        also have ‹P l0 ⟦S⟧✓Rlist ?MS (l1 # L') = ?MS L›
          by (simp add: ‹L = l0 # l1 # L'›)
        finally have ‹?MS (?pl_τ i j L) = ?RT (?MS L) (?pl_τ i j)› .
      } note £ = this

      consider ‹i ≠ 0› | ‹j ≠ n› | ‹i = 0› ‹j = n› by argo
      thus ?case
      proof cases
        assume ‹i ≠ 0›
        from Suc.hyps(1, 3) obtain l0 l1 L' where ‹L = l0 # l1 # L'›
          by (cases L; cases ‹tl L›) simp_all
        from "£" ‹i ≠ 0› ‹i < j› Suc.prems(2, 3) Suc.hyps(3) this show ?case .
      next
        assume ‹j ≠ n›
        from Suc.hyps(1, 3) obtain l0 l1 L' where ‹L = L' @ [l1] @ [l0]›
          by (cases L rule: rev_cases; cases ‹butlast L› rule: rev_cases) simp_all
        hence ‹rev L = l0 # l1 # rev L'› by simp
        have ‹Suc n = length (rev L)› by (simp add: Suc.hyps(3))

        have ‹?MS (?pl_τ i j L) = ?MS (rev (?pl_τ (length L - Suc i) (length L - Suc j) (rev L)))›
          by (subst rev_rev_ident[of L, symmetric], subst permute_list_transpose_rev)
            (simp_all add: Suc.prems(2, 3))
        also have ‹… = ?RT (?MS (?pl_τ (length L - Suc i) (length L - Suc j) (rev L))) rev›
          by (fact MultiSyncptick_rev)
        also have ‹?pl_τ (length L - Suc i) (length L - Suc j) =
                   ?pl_τ (length L - Suc j) (length L - Suc i)›
          by (simp add: transpose_commute)
        also have ‹?MS (?pl_τ (length L - Suc j) (length L - Suc i) (rev L)) =
                   ?RT (?MS (rev L)) (?pl_τ (length L - Suc j) (length L - Suc i))›
          by (rule "£") (use Suc.hyps(3) Suc.prems(3) ‹j ≠ n› ‹i < j›
              ‹rev L = l0 # l1 # rev L'› in auto)
        also have ‹?MS (rev L) = ?RT (?MS L) rev›
          by (fact MultiSyncptick_rev)
        also have ‹?RT (?RT (?RT (?MS L) rev) (?pl_τ (length L - Suc j) (length L - Suc i))) rev =
                   ?RT (?MS L) (rev ∘ (?pl_τ (length L - Suc j) (length L - Suc i)) ∘ rev)›
          by (simp add: RenamingTick_comp)
        also have ‹… = ?RT (?MS L) (?pl_τ j i)›
        proof (rule RenamingTick_is_restrictable_on_strict_ticks_of)
          fix rs assume ‹rs ∈ ✓s(?MS L)›
          hence ‹length rs = length L›
            using is_ticks_lengthD is_ticks_length_MultiSyncptick by blast
          thus ‹(rev ∘ (?pl_τ (length L - Suc j) (length L - Suc i)) ∘ rev) rs = ?pl_τ j i rs›
            by (unfold comp_def, subst rev_permute_list_transpose)
              (use Suc.prems(2, 3) in auto)
        qed
        also have ‹… = ?RT (?MS L) (?pl_τ i j)›
          by (simp add: transpose_commute)
        finally show ?case .
      next
        let ?g1 = ‹λrs. if rs = [] then [] else last rs # butlast rs›
        let ?g2 = ‹λrs. drop (Suc (Suc 0)) rs @ take (Suc (Suc 0)) rs›
        let ?g3 = ‹λrs. case rs of r # s ⇒ r # (if s = [] then [] else last s # butlast s)›
        let ?tj = ‹λr s. ⌊id r # (if s = [] then [] else last s # butlast s)⌋›
        assume ‹i = 0› ‹j = n›
        from Suc.hyps(1, 3) obtain l0 l1 L'
          where ‹L = l0 # L' @ [l1]› ‹L' ≠ []›
          by (cases L; cases ‹tl L› rule: rev_cases; force)
        have ‹?pl_τ i j L = l1 # L' @ [l0]›
          by (subst permute_list_transpose_eq_list_update)
            (use Suc.prems(3) Suc.hyps(3) ‹L = l0 # L' @ [l1]›
              in ‹auto simp add: ‹i = 0› ‹j = n››)
        hence ‹?MS (?pl_τ i j L) = P l1 ⟦S⟧✓Rlist (?MS L' ⟦S⟧✓Llist P l0)›
          by (simp add: MultiSyncptick_Cons MultiSyncptick_snoc ‹L' ≠ []›)
        also have ‹… = ?RT (?MS L' ⟦S⟧✓Llist P l0 ⟦S⟧✓Llist P l1) ?g1›
          by (simp only: SyncRlist.Syncptick_comm_locale_sym.Syncptick_commute)
        also have ‹?MS L' ⟦S⟧✓Llist P l0 ⟦S⟧✓Llist P l1 =
                   (?MS L' ⇘Suc (Suc 0)⇙⟦S⟧✓ListslenR (P l0 ⟦S⟧✓Pairlist P l1))›
          by (simp only: SyncListslenR_SyncPairlist_assoc)
        also have ‹… = ?RT (P l0 ⟦S⟧✓Pairlist P l1 ⇘Suc (Suc 0)⇙⟦S⟧✓ListslenL ?MS L') ?g2›
          by (simp only: SyncListslenL.Syncptick_commute)
        also have ‹P l0 ⟦S⟧✓Pairlist P l1 ⇘Suc (Suc 0)⇙⟦S⟧✓ListslenL ?MS L' =
                   P l0 ⟦S⟧✓Rlist (P l1 ⟦S⟧✓Rlist ?MS L')›
          by (simp only: SyncRlist_SyncRlist_assoc)
        also have ‹… = P l0 ⟦S⟧✓Rlist ?RT (?MS L' ⟦S⟧✓Llist P l1) ?g1›
          by (simp only: SyncRlist.Syncptick_comm_locale_sym.Syncptick_commute)
        also have ‹… = ?RT (P l0) id ⟦S⟧✓Rlist ?RT (?MS L' ⟦S⟧✓Llist P l1) ?g1› by simp
        also have ‹… = Syncptick_locale.Syncptick ?tj (P l0) S (?MS L' ⟦S⟧✓Llist P l1)›
        proof (rule SyncRlist.inj_RenamingTick_Syncptick_inj_RenamingTick)
          show ‹inj id› ‹inj (λrs. if rs = [] then [] else last rs # butlast rs)›
            by (auto intro!: injI split: if_split_asm)
              (metis append_butlast_last_id)
        qed
        also have ‹… = ?RT (P l0 ⟦S⟧✓Rlist (?MS L' ⟦S⟧✓Llist P l1)) ?g3›
          by (subst SyncRlist.inj_on_RenamingTick_Syncptick)
            (auto intro!: inj_onI split: if_split_asm, metis append_butlast_last_id)
        also have ‹P l0 ⟦S⟧✓Rlist (?MS L' ⟦S⟧✓Llist P l1) = ?MS L›
          by (simp add: ‹L = l0 # L' @ [l1]› MultiSyncptick_Cons MultiSyncptick_snoc ‹L' ≠ []›)
        also have ‹?RT (?RT (?RT (?MS L) ?g3) ?g2) ?g1 = ?RT (?MS L) (?g1 ∘ ?g2 ∘ ?g3)›
          by (simp only: RenamingTick_comp)
        also have ‹… = ?RT (?MS L) (?pl_τ i j)›
        proof (rule RenamingTick_is_restrictable_on_strict_ticks_of)
          fix rs assume ‹rs ∈ ✓s(?MS L)›
          hence ‹length rs = length L›
            using is_ticks_lengthD is_ticks_length_MultiSyncptick by blast
          obtain n' where ‹n = Suc (Suc n')›
            by (metis One_nat_def Suc.hyps(1) Suc_1 Suc_n_not_le_n ‹i = 0› ‹i ≠ j› ‹j = n› nat.exhaust_sel)
          with Suc.hyps(1, 3) ‹length rs = length L›
          obtain r0 r1 r2 rs' where ‹rs = r0 # r1 # r2 # rs'› ‹n' = length rs'›
            by (cases rs; cases ‹tl rs›; cases ‹tl (tl rs)›) simp_all
          show ‹(?g1 ∘ ?g2 ∘ ?g3) rs = ?pl_τ i j rs›
          proof (subst permute_list_transpose_eq_list_update)
            show ‹i < length rs› ‹j < length rs›
              by (simp_all add: Suc.prems(2, 3) ‹length rs = length L›)
          next
            show ‹(?g1 ∘ ?g2 ∘ ?g3) rs = rs[i := rs ! j, j := rs ! i]›
              by (simp add: ‹i = 0› ‹j = n› ‹rs = r0 # r1 # r2 # rs'› ‹n' = length rs'›
                  ‹n = Suc (Suc n')› butlast_append nat.case_eq_if)
                (metis One_nat_def append_butlast_last_id diff_Suc_1' last_conv_nth
                  length_0_conv length_butlast list_update_length nat.collapse)
          qed
        qed
        finally show ?case .
      qed
    qed
  qed

  consider ‹i ≤ j› | ‹j ≤ i› by linarith
  thus ‹?RS (?pl_τ i j L) = ?RT (?RS L) (?pl_τ i j)› if ‹i < length L› ‹j < length L›
  proof cases
    from that show ‹i ≤ j ⟹ ?RS (?pl_τ i j L) = ?RT (?RS L) (?pl_τ i j)› by (fact "*")
  next
    from that show ‹j ≤ i ⟹ ?RS (?pl_τ i j L) = ?RT (?RS L) (?pl_τ i j)›
      by (subst (1 2) transpose_commute) (rule "*")
  qed
qed


text ‹
Finally, the proof of the general version relies on the fact that
a permutation can be written as finite product of transpositions.
›


theorem MultiSyncptick_permute_list :
  ‹⟦S⟧✓ l ∈@ permute_list f L. P l =
   RenamingTick (⟦S⟧✓ l ∈@ L. P l) (permute_list f)›
  if f_permutes : ‹f permutes {..<length L}›
  using finite_lessThan f_permutes
proof (induct f rule: permutes_rev_induct)
  case id show ?case by (simp flip: id_def)
next
  let ?RT = RenamingTick and ?pl = permute_list and ?τ = Transposition.transpose
  case (swap i j f)  
  have ‹?τ i j permutes {..<length L}›
    by (meson permutes_swap_id swap.hyps(1, 2))
  hence ‹⟦S⟧✓ l ∈@ ?pl (f ∘ ?τ i j) L. P l =
         ⟦S⟧✓ l ∈@ (?pl (?τ i j) (?pl f L)). P l›
    by (simp add: permute_list_compose)

  also have ‹… = ?RT (⟦S⟧✓ l ∈@ (?pl f L). P l) (?pl (?τ i j))›
    by (metis MultiSyncptick_permute_list_transpose atLeast0LessThan
        atLeastLessThan_iff length_permute_list swap.hyps(1,2))
  also have ‹… = ?RT (?RT (⟦S⟧✓ l ∈@ L. P l) (?pl f)) (?pl (?τ i j))›
    unfolding swap.hyps(4) ..
  also have ‹… = ?RT (⟦S⟧✓ l ∈@ L. P l) (?pl (?τ i j) ∘ ?pl f)›
    by (simp flip: Renaming_comp)
  also have ‹… = ?RT (⟦S⟧✓ l ∈@ L. P l) (?pl (f ∘ (?τ i j)))›
  proof (rule RenamingTick_is_restrictable_on_strict_ticks_of)
    fix rs assume ‹rs ∈ ✓s(⟦S⟧✓ l ∈@ L. P l)›
    from is_ticks_lengthD is_ticks_length_MultiSyncptick this
    have ‹length rs = length L› .
    with ‹?τ i j permutes {..<length L}›
    show ‹(?pl (?τ i j) ∘ ?pl f) rs = ?pl (f ∘ ?τ i j) rs›
      by (simp add: permute_list_compose)
  qed
  finally show ?case .
qed



(*<*)
end
  (*>*)