Theory CSPM_Laws

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Laws for architectural operators
 *
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)

section ‹Results for Throw›
(*<*)
theory CSPM_Laws
  imports Global_Deterministic_Choice Multi_Synchronization_Product
    Multi_Sequential_Composition Interrupt Throw
begin
(*>*)


subsection ‹Laws for Throw›

lemma Throw_GlobalDet :
  ‹(□ a ∈ A. P a) Θ b ∈ B. Q b = □ a ∈ A. P a Θ b ∈ B. Q b› (is ‹?lhs = ?rhs›)
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (simp add: D_Throw GlobalDet_projs split: if_split_asm) blast
next
  show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    by (simp add: D_Throw GlobalDet_projs) (meson empty_iff)
next
  fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
  then consider ‹(t, X) ∈ ℱ (□a ∈ A. P a)› ‹set t ∩ ev ` B = {}›
    | (failR) t1 b t2 where ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (□a ∈ A. P a)›
      ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
    unfolding Throw_projs by blast
  thus ‹(t, X) ∈ ℱ ?rhs›
  proof cases
    show ‹(t, X) ∈ ℱ (□a ∈ A. P a) ⟹ set t ∩ ev ` B = {} ⟹ (t, X) ∈ ℱ ?rhs›
      by (cases t) (auto simp add: F_GlobalDet Throw_projs)
  next
    case failR
    from failR(2) obtain a where ‹a ∈ A› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
      by (auto simp add: T_GlobalDet split: if_split_asm)
    with failR(3-5) show ‹(t, X) ∈ ℱ ?rhs›
      by (simp add: F_GlobalDet F_Throw failR(1)) blast
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
  then consider ‹t = []› ‹∀a∈A. (t, X) ∈ ℱ (P a Θ b ∈ B. Q b)›
    | a where ‹a ∈ A› ‹t ≠ []› ‹(t, X) ∈ ℱ (P a Θ b ∈ B. Q b)›
    | a r where ‹a ∈ A› ‹t = []› ‹✓(r) ∉ X› ‹[✓(r)] ∈ 𝒯 (P a Θ b ∈ B. Q b)›
    by (auto simp add: GlobalDet_projs)
  thus ‹(t, X) ∈ ℱ ?lhs›
  proof cases
    show ‹t = [] ⟹ ∀a∈A. (t, X) ∈ ℱ (P a Θ b ∈ B. Q b) ⟹ (t, X) ∈ ℱ ?lhs›
      by (auto simp add: F_Throw F_GlobalDet)
  next
    show ‹a ∈ A ⟹ t ≠ [] ⟹ (t, X) ∈ ℱ (P a Θ b ∈ B. Q b) ⟹ (t, X) ∈ ℱ ?lhs› for a
      by (simp add: F_Throw GlobalDet_projs) (metis empty_iff)
  next
    show ‹⟦a ∈ A; t = []; ✓(r) ∉ X; [✓(r)] ∈ 𝒯 (P a Θ b ∈ B. Q b)⟧ ⟹ (t, X) ∈ ℱ ?lhs› for a r
      by (simp add: Throw_projs F_GlobalDet Cons_eq_append_conv) (metis is_processT9_tick)
  qed
qed


lemma Throw_GlobalNdetR :
  ‹P Θ a ∈ A. ⊓b ∈ B. Q a b =
   (if B = {} then P Θ a ∈ A. STOP else □b ∈ B. P Θ a ∈ A. Q a b)›
  (is ‹?lhs = (if _ then _ else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹B = {} ⟹ ?lhs = P Θ a ∈ A. STOP› by simp
next
  show ‹?lhs = ?rhs› if ‹B ≠ {}›
  proof (subst Process_eq_spec, safe)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (auto simp add: ‹B ≠ {}› D_Throw D_GlobalNdet D_GlobalDet)
  next
    show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
      by (auto simp add: ‹B ≠ {}› D_Throw D_GlobalNdet D_GlobalDet)
  next
    show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
      by (cases t) (auto simp add: ‹B ≠ {}› F_Throw F_GlobalNdet F_GlobalDet)
  next
    show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
      by (auto simp add: ‹B ≠ {}› Throw_projs F_GlobalNdet F_GlobalDet D_T
          is_processT7 Cons_eq_append_conv intro!: is_processT6_TR_notin)
  qed
qed


corollary Throw_Det : ‹P □ P' Θ a ∈ A. Q a = (P Θ a ∈ A. Q a) □ (P' Θ a ∈ A. Q a)›
proof -
  have ‹P □ P' Θ a ∈ A. Q a = (□a∈{0 :: nat, 1}. (if a = 0 then P else P')) Θ a ∈ A. Q a›
    by (simp add: GlobalDet_distrib_unit)
  also have ‹… = □a∈{0 :: nat, 1}. (if a = 0 then P else P') Θ a ∈ A. Q a›
    by (fact Throw_GlobalDet)
  also have ‹… = (P Θ a ∈ A. Q a) □ (P' Θ a ∈ A. Q a)›
    by (simp add: GlobalDet_distrib_unit)
  finally show ?thesis .
qed

corollary Throw_NdetR : ‹P Θ a ∈ A. Q a ⊓ Q' a = (P Θ a ∈ A. Q a) □ (P Θ a ∈ A. Q' a)›
proof -
  have ‹P Θ a ∈ A. Q a ⊓ Q' a = P Θ a ∈ A. ⊓b ∈ {0 :: nat, 1}. (if b = 0 then Q a else Q' a)›
    by (simp add: GlobalNdet_distrib_unit)
  also have ‹… = □b ∈ {0 :: nat, 1}. P Θ a ∈ A. (if b = 0 then Q a else Q' a)›
    by (simp add: Throw_GlobalNdetR)
  also have ‹… = (P Θ a ∈ A. Q a) □ (P Θ a ∈ A. Q' a)›
    by (simp add: GlobalDet_distrib_unit)
  finally show ?thesis .
qed



subsection ‹Laws for Sync›

lemma Sync_GlobalNdet_cartprod:
  ‹(⊓ (a, b) ∈ A × B. (P a ⟦S⟧ Q b)) = 
   (if A = {} ∨ B = {} then STOP else (⊓a ∈ A. P a) ⟦S⟧ (⊓b ∈ B. Q b))›  
  by (simp add: GlobalNdet_cartprod Sync_distrib_GlobalNdet_left
      Sync_distrib_GlobalNdet_right GlobalNdet_sets_commute[of A])


lemmas Inter_GlobalNdet_cartprod = Sync_GlobalNdet_cartprod[where S = ‹{}›]
  and   Par_GlobalNdet_cartprod = Sync_GlobalNdet_cartprod[where S = UNIV]



lemma MultiSync_Hiding_pseudo_distrib:
  ‹finite A ⟹ A ∩ S = {} ⟹ (❙⟦S❙⟧ p ∈# M. (P p \ A)) = (❙⟦S❙⟧ p ∈# M. P p) \ A›
  by (induct M, simp) (metis MultiSync_add MultiSync_rec1 Hiding_Sync)


lemma MultiSync_prefix_pseudo_distrib:
  ‹M ≠ {#} ⟹ a ∈ S ⟹ (❙⟦S❙⟧ p ∈# M. (a → P p)) = (a → (❙⟦S❙⟧ p ∈# M. P p))›
  by (induct M rule: mset_induct_nonempty) 
    (simp_all add: write0_Sync_write0_subset)

lemmas MultiInter_Hiding_pseudo_distrib =
  MultiSync_Hiding_pseudo_distrib[where S = ‹{}›, simplified]
  and MultiPar_prefix_pseudo_distrib =
  MultiSync_prefix_pseudo_distrib[where S = ‹UNIV›, simplified]


text ‹A result on Mndetprefix and Sync.›

lemma Mndetprefix_Sync_distr: ‹A ≠ {} ⟹ B ≠ {} ⟹ 
       (⊓ a ∈ A → P a) ⟦S⟧ (⊓ b ∈ B → Q b) =
        ⊓ a∈A. ⊓ b∈B. (□c ∈ ({a} - S) → (P a ⟦S⟧ (b → Q b))) □ 
                       (□d ∈ ({b} - S) → ((a → P a) ⟦S⟧ Q b)) □
                       (□c∈({a} ∩ {b} ∩ S) → (P a ⟦S⟧ Q b))›
  apply (subst (1 2) Mndetprefix_GlobalNdet) 
  apply (subst Sync_distrib_GlobalNdet_right, simp)
  apply (subst Sync_commute)
  apply (subst Sync_distrib_GlobalNdet_right, simp)
  apply (subst Sync_commute)
  apply (unfold write0_def)
  apply (subst Mprefix_Sync_Mprefix)
  by (fold write0_def, rule refl)

lemma ‹A ≠ {} ⟹ B ≠ {} ⟹ (⊓ a ∈ A → P a) ⟦S⟧ (⊓ b ∈ B → Q b) =
        ⊓ a∈A. ⊓ b∈B. (if a ∈ S then STOP else (a → (P a ⟦S⟧ (b → Q b)))) □ 
                       (if b ∈ S then STOP else (b → ((a → P a) ⟦S⟧ Q b))) □
                       (if a = b ∧ a ∈ S then (a → (P a ⟦S⟧ Q a)) else STOP)›
  apply (subst Mndetprefix_Sync_distr, assumption+)
  apply (intro mono_GlobalNdet_eq)
  apply (intro arg_cong2[where f = ‹(□)›])
  by (simp_all add: Mprefix_singl insert_Diff_if Int_insert_left)





subsection ‹GlobalDet, GlobalNdet and write0›

lemma GlobalDet_write0_is_GlobalNdet_write0:
  ‹(□ p ∈ A. (a → P p)) = ⊓ p ∈ A. (a → P p)› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (simp_all add: D_GlobalDet write0_def D_Mprefix D_GlobalNdet)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs›
    and ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (auto simp add: F_GlobalDet write0_def F_Mprefix F_GlobalNdet split: if_split_asm)
qed    

lemma write0_GlobalNdet_bis:
  ‹A ≠ {} ⟹ (a → (⊓ p ∈ A. P p) = □ p ∈ A. (a → P p))›
  by (simp add: GlobalDet_write0_is_GlobalNdet_write0 write0_GlobalNdet)






section ‹Some Results on Renaming›

(* TODO: useful ? and rename *)
lemma Renaming_GlobalNdet:
  ‹Renaming (⊓ a ∈ A. P (f a)) f g = ⊓ b ∈ f ` A. Renaming (P b) f g›
  by (metis Renaming_distrib_GlobalNdet mono_GlobalNdet_eq2)

lemma Renaming_GlobalNdet_inj_on:
  ‹Renaming (⊓ a ∈ A. P a) f g =
   ⊓ b ∈ f ` A. Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
  if inj_on_f: ‹inj_on f A›
  by (smt (verit, ccfv_SIG) Renaming_distrib_GlobalNdet inj_on_def mono_GlobalNdet_eq2 that the_equality)

corollary Renaming_GlobalNdet_inj:
  ‹Renaming (⊓ a ∈ A. P a) f g =
   ⊓ b ∈ f ` A. Renaming (P (THE a. f a = b)) f g› if inj_f: ‹inj f›
  apply (subst Renaming_GlobalNdet_inj_on, metis inj_eq inj_onI inj_f)
  apply (rule mono_GlobalNdet_eq[rule_format])
  by (metis imageE inj_eq[OF inj_f])


lemma Renaming_distrib_GlobalDet :
  ‹Renaming (□a ∈ A. P a) f g = □a ∈ A. Renaming (P a) f g› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Renaming D_GlobalDet)
next
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  fix s X assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | t where ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t› ‹(t, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (□a ∈ A. P a)›
    unfolding Renaming_projs by blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  next
    show ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t ⟹ (t, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (□a ∈ A. P a)
          ⟹ (s, X) ∈ ℱ ?rhs› for t
      by (cases t; simp add: F_GlobalDet Renaming_projs)
        (force, metis list.simps(9))
  qed
next
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  fix s X assume ‹(s, X) ∈ ℱ ?rhs›
  then consider ‹s = []› ‹∀a∈A. (s, X) ∈ ℱ (Renaming (P a) f g)›
    | a where ‹a ∈ A› ‹s ≠ []› ‹(s, X) ∈ ℱ (Renaming (P a) f g)›
    | a where ‹a ∈ A› ‹s = []› ‹s ∈ 𝒟 (Renaming (P a) f g)›
    | a r where ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› ‹[✓(r)] ∈ 𝒯 (Renaming (P a) f g)›
    unfolding F_GlobalDet by blast
  thus ‹(s, X) ∈ ℱ ?lhs›
  proof cases
    show ‹s = [] ⟹ ∀a∈A. (s, X) ∈ ℱ (Renaming (P a) f g) ⟹ (s, X) ∈ ℱ ?lhs›
      by (auto simp add: F_Renaming F_GlobalDet)
  next
    show ‹a ∈ A ⟹ s ≠ [] ⟹ (s, X) ∈ ℱ (Renaming (P a) f g) ⟹ (s, X) ∈ ℱ ?lhs› for a
      by (simp add: F_Renaming GlobalDet_projs) (metis list.simps(8))
  next
    show ‹a ∈ A ⟹ s = [] ⟹ s ∈ 𝒟 (Renaming (P a) f g) ⟹ (s, X) ∈ ℱ ?lhs› for a
      by (auto simp add: Renaming_projs D_GlobalDet)
  next
    fix a r assume * : ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› ‹[✓(r)] ∈ 𝒯 (Renaming (P a) f g)›
    from "*"(4) consider s1 where ‹[✓(r)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1› ‹s1 ∈ 𝒯 (P a)›
      | s1 s2 where ‹[✓(r)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2›
        ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ 𝒟 (P a)›
      by (simp add: T_Renaming) meson
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      fix s1 assume ‹[✓(r)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1› ‹s1 ∈ 𝒯 (P a)›
      from ‹[✓(r)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1› obtain r' where ‹r = g r'› ‹s1 = [✓(r')]›
        by (metis map_map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff)
      with "*"(1, 2, 3) ‹s1 ∈ 𝒯 (P a)›
      show ‹(s, X) ∈ ℱ ?lhs› by (auto simp add: F_Renaming F_GlobalDet)
    next
      fix s1 s2 assume ‹[✓(r)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2›
        ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ 𝒟 (P a)›
      from ‹[✓(r)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹tickFree s1›
      have ‹s1 = [] ∧ s2 = [✓(r)]›
        by (cases s1; simp) (metis event⇩p⇩t⇩i⇩c⇩k.disc(2) event⇩p⇩t⇩i⇩c⇩k.map_disc_iff(1))
      with "*"(1, 2) ‹s1 ∈ 𝒟 (P a)› show ‹(s, X) ∈ ℱ ?lhs›
        by (auto simp add: F_Renaming F_GlobalDet)
    qed
  qed
qed

lemma Renaming_Mprefix_bis :
  ‹Renaming (□a ∈ A → P a) f g = □a ∈ A. (f a → Renaming (P a) f g)›
  by (simp add: Mprefix_GlobalDet Renaming_distrib_GlobalDet Renaming_write0)


(* TODO : useful ? *)
lemma Renaming_GlobalDet_alt:
  ‹Renaming (□ a ∈ A. P (f a)) f g = □ b ∈ f ` A. Renaming (P b) f g›
  (is ‹?lhs = ?rhs›)
  by (simp add: Renaming_distrib_GlobalDet mono_GlobalDet_eq2)


lemma Renaming_GlobalDet_inj_on:
  ‹inj_on f A ⟹ Renaming (□ a ∈ A. P a) f g =
   □ b ∈ f ` A. Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
  by (simp add: Renaming_distrib_GlobalDet inj_on_def mono_GlobalDet_eq2 the_equality)


corollary Renaming_GlobalDet_inj:
  ‹inj f ⟹ Renaming (□ a ∈ A. P a) f g = □ b ∈ f ` A. Renaming (P (THE a. f a = b)) f g›
  by (subst Renaming_GlobalDet_inj_on, metis inj_eq inj_onI)
    (rule mono_GlobalDet_eq, metis imageE inj_eq)


lemma Renaming_Interrupt :
  ‹Renaming (P △ Q) f g = Renaming P f g △ Renaming Q f g› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  fix t assume ‹t ∈ 𝒟 ?lhs›
  then obtain t1 t2
    where * : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1 @ t2› ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 (P △ Q)›
    unfolding D_Renaming by blast
  from "*"(4) consider ‹t1 ∈ 𝒟 P›
    | u1 u2 where ‹t1 = u1 @ u2› ‹u1 ∈ 𝒯 P› ‹tF u1› ‹u2 ∈ 𝒟 Q›
    unfolding D_Interrupt by blast
  thus ‹t ∈ 𝒟 ?rhs›
  proof cases
    from "*"(1-3) show ‹t1 ∈ 𝒟 P ⟹ t ∈ 𝒟 ?rhs›
      by (auto simp add: D_Interrupt D_Renaming)
  next
    show ‹t1 = u1 @ u2 ⟹ u1 ∈ 𝒯 P ⟹ tF u1 ⟹ u2 ∈ 𝒟 Q ⟹ t ∈ 𝒟 ?rhs› for u1 u2
      by (simp add: D_Interrupt Renaming_projs "*"(1))
        (metis "*"(2, 3) map_event⇩p⇩t⇩i⇩c⇩k_tickFree tickFree_append_iff)
  qed
next
  fix t assume ‹t ∈ 𝒟 ?rhs›
  then consider ‹t ∈ 𝒟 (Renaming P f g)›
    | t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒯 (Renaming P f g)› ‹tF t1› ‹t2 ∈ 𝒟 (Renaming Q f g)›
    unfolding D_Interrupt by blast
  thus ‹t ∈ 𝒟 ?lhs›
  proof cases
    show ‹t ∈ 𝒟 (Renaming P f g) ⟹ t ∈ 𝒟 ?lhs›
      by (auto simp add: D_Renaming D_Interrupt)
  next
    show ‹t = t1 @ t2 ⟹ t1 ∈ 𝒯 (Renaming P f g) ⟹ tF t1 ⟹ t2 ∈ 𝒟 (Renaming Q f g) ⟹ t ∈ 𝒟 ?lhs› for t1 t2
      by (auto simp add: Renaming_projs D_Interrupt append.assoc map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
        (metis (no_types, opaque_lifting) append.assoc map_append tickFree_append_iff,
          metis front_tickFree_append map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
  qed
next
  fix t X assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(t, X) ∈ ℱ ?lhs›
  then consider ‹t ∈ 𝒟 ?lhs›
    | u where ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P △ Q)›
    unfolding Renaming_projs by blast
  thus ‹(t, X) ∈ ℱ ?rhs›
  proof cases
    from same_div D_F show ‹t ∈ 𝒟 ?lhs ⟹ (t, X) ∈ ℱ ?rhs› by blast
  next
    fix u assume * : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P △ Q)›
    from "*"(2) consider ‹u ∈ 𝒟 (P △ Q)›
      | u' r  where ‹u = u' @ [✓(r)]› ‹u' @ [✓(r)] ∈ 𝒯 P›
      | X' r  where ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X = X' - {✓(r)}› ‹u @ [✓(r)] ∈ 𝒯 P›
      | ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ P› ‹tF u› ‹([], map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q›
      | u1 u2 where ‹u = u1 @ u2› ‹u1 ∈ 𝒯 P› ‹tF u1› ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q› ‹u2 ≠ []›
      | X' r  where ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X = X' - {✓(r)}› ‹u ∈ 𝒯 P› ‹tF u› ‹[✓(r)] ∈ 𝒯 Q›
      unfolding Interrupt_projs by safe auto
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      assume ‹u ∈ 𝒟 (P △ Q)›
      hence ‹t ∈ 𝒟 ?lhs›
        by (simp add: "*"(1) D_Renaming)
          (metis (no_types, opaque_lifting) D_imp_front_tickFree append_Nil2 snoc_eq_iff_butlast
            butlast.simps(1) div_butlast_when_non_tickFree_iff front_tickFree_Nil
            front_tickFree_iff_tickFree_butlast front_tickFree_single map_butlast)
      with same_div D_F show ‹(t, X) ∈ ℱ ?rhs› by blast
    next
      show ‹u = u' @ [✓(r)] ⟹ u' @ [✓(r)] ∈ 𝒯 P ⟹ (t, X) ∈ ℱ ?rhs› for u' r
        by (auto simp add: "*"(1) F_Interrupt T_Renaming)
    next
      fix X' r assume ** : ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X = X' - {✓(r)}› ‹u @ [✓(r)] ∈ 𝒯 P›
      from "**" obtain X'' where ‹X = X'' - {✓(g r)}›
        by (metis DiffD2 Diff_insert_absorb event⇩p⇩t⇩i⇩c⇩k.simps(10) insertI1 vimage_eq)
      moreover from "**"(2) have ‹t @ [✓(g r)] ∈ 𝒯 (Renaming P f g)›
        by (auto simp add: "*"(1) T_Renaming)
      ultimately show ‹(t, X) ∈ ℱ ?rhs› by (auto simp add: F_Interrupt)
    next
      show ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ P ⟹ tF u ⟹
            ([], map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q ⟹ (t, X) ∈ ℱ ?rhs›
        using map_event⇩p⇩t⇩i⇩c⇩k_tickFree by (auto simp add: "*"(1) F_Interrupt F_Renaming)
    next
      fix u1 u2 assume ‹u = u1 @ u2› ‹u1 ∈ 𝒯 P› ‹tF u1›
        ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q› ‹u2 ≠ []›
      hence ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2›
        ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 ∈ 𝒯 (Renaming P f g)›
        ‹tF (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1)›
        ‹(map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2, X) ∈ ℱ (Renaming Q f g)›
        ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 ≠ []›
        by (auto simp add: "*"(1) Renaming_projs map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
      thus ‹(t, X) ∈ ℱ ?rhs› by (simp add: F_Interrupt) blast
    next
      fix X' r assume ** : ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X = X' - {✓(r)}› ‹u ∈ 𝒯 P› ‹tF u› ‹[✓(r)] ∈ 𝒯 Q›
      from "**"(1, 2) obtain X'' where ‹X = X'' - {✓(g r)}›
        by (metis DiffD2 Diff_insert_absorb event⇩p⇩t⇩i⇩c⇩k.simps(10) insertI1 vimage_eq)
      moreover from "**"(2-4) have ‹t ∈ 𝒯 (Renaming P f g)› ‹tF t›
        ‹[✓(g r)] ∈ 𝒯 (Renaming Q f g)›
        by (auto simp add: "*"(1) T_Renaming map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
      ultimately show ‹(t, X) ∈ ℱ ?rhs› by (simp add: F_Interrupt) blast
    qed
  qed
next
  fix t X assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(t, X) ∈ ℱ ?rhs›
  then consider ‹t ∈ 𝒟 ?rhs›
    | t' s  where ‹t = t' @ [✓(s)]› ‹t' @ [✓(s)] ∈ 𝒯 (Renaming P f g)›
    | X' s  where ‹X = X' - {✓(s)}› ‹t  @ [✓(s)] ∈ 𝒯 (Renaming P f g)›
    | ‹(t, X) ∈ ℱ (Renaming P f g)› ‹tF t› ‹([], X) ∈ ℱ (Renaming Q f g)›
    | t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒯 (Renaming P f g)› ‹tF t1›
      ‹(t2, X) ∈ ℱ (Renaming Q f g)› ‹t2 ≠ []›
    | X' s where ‹X = X' - {✓(s)}› ‹t ∈ 𝒯 (Renaming P f g)› ‹tF t› ‹[✓(s)] ∈ 𝒯 (Renaming Q f g)›
    by (simp add: Interrupt_projs) blast
  thus ‹(t, X) ∈ ℱ ?lhs›
  proof cases
    from same_div D_F show ‹t ∈ 𝒟 ?rhs ⟹ (t, X) ∈ ℱ ?lhs› by blast
  next
    show ‹⟦t = t' @ [✓(s)]; t' @ [✓(s)] ∈ 𝒯 (Renaming P f g)⟧ ⟹ (t, X) ∈ ℱ ?lhs› for t' s
      by (simp add: Renaming_projs Interrupt_projs)
        (metis T_nonTickFree_imp_decomp map_event⇩p⇩t⇩i⇩c⇩k_tickFree non_tickFree_tick tickFree_append_iff)
  next
    fix X' s assume * : ‹X = X' - {✓(s)}› ‹t @ [✓(s)] ∈ 𝒯 (Renaming P f g)›
    from "*"(2) consider u1 u2 where
      ‹t @ [✓(s)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
    | u r where ‹s = g r› ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹u @ [✓(r)] ∈ 𝒯 P›
      by (simp add: T_Renaming)
        (metis (no_types, opaque_lifting) T_nonTickFree_imp_decomp event⇩p⇩t⇩i⇩c⇩k.disc(4)
          event⇩p⇩t⇩i⇩c⇩k.map_sel(2) event⇩p⇩t⇩i⇩c⇩k.sel(2) last_map map_butlast map_event⇩p⇩t⇩i⇩c⇩k_tickFree
          non_tickFree_tick snoc_eq_iff_butlast tickFree_append_iff)
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      fix u1 u2 assume ‹t @ [✓(s)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
      hence ‹t ∈ 𝒟 ?lhs›
        by (cases u2 rule: rev_cases)
          (auto simp add: D_Interrupt D_Renaming intro: front_tickFree_dw_closed,
            metis map_event⇩p⇩t⇩i⇩c⇩k_tickFree non_tickFree_tick tickFree_append_iff)
      with D_F show ‹(t, X) ∈ ℱ ?lhs› by blast
    next
      fix u r assume ‹s = g r› ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹u @ [✓(r)] ∈ 𝒯 P›
      moreover from "*"(1) ‹s = g r› obtain X'' where ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X = X'' - {✓(r)}›
        by (metis Diff_iff Diff_insert_absorb event⇩p⇩t⇩i⇩c⇩k.simps(10) vimage_eq vimage_singleton_eq)
      ultimately show ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_Renaming F_Interrupt) metis
    qed
  next
    show ‹⟦(t, X) ∈ ℱ (Renaming P f g); tF t; ([], X) ∈ ℱ (Renaming Q f g)⟧ ⟹ (t, X) ∈ ℱ ?lhs›
      by (simp add: Renaming_projs Interrupt_projs)
        (metis is_processT8 map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
  next
    fix t1 t2 assume * : ‹t = t1 @ t2› ‹t1 ∈ 𝒯 (Renaming P f g)› ‹tF t1›
      ‹(t2, X) ∈ ℱ (Renaming Q f g)› ‹t2 ≠ []›
    from "*"(2) consider u1 u2 where
      ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
    | u1 where ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1› ‹u1 ∈ 𝒯 P›
      unfolding T_Renaming by blast
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      fix u1 u2 assume ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
      hence ‹t1 ∈ 𝒟 ?lhs› by (auto simp add: D_Interrupt D_Renaming)
      with "*"(1, 3, 4) F_imp_front_tickFree is_processT7 have ‹t ∈ 𝒟 ?lhs› by blast
      with D_F show ‹(t, X) ∈ ℱ ?lhs› by blast
    next
      fix u1 assume ** : ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1› ‹u1 ∈ 𝒯 P›
      from "*"(4) consider u2 u3 where
        ‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 @ u3› ‹tF u2› ‹ftF u3› ‹u2 ∈ 𝒟 Q›
      | u2 where ‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2› ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q›
        unfolding F_Renaming by blast
      thus ‹(t, X) ∈ ℱ ?lhs›
      proof cases
        fix u2 u3 assume ‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 @ u3› ‹tF u2› ‹ftF u3› ‹u2 ∈ 𝒟 Q›
        hence ‹t ∈ 𝒟 ?lhs›
          by (simp add: "*"(1) "**"(1) D_Renaming D_Interrupt flip: map_append append.assoc)
            (metis "*"(3) "**"(1, 2) map_event⇩p⇩t⇩i⇩c⇩k_tickFree tickFree_append_iff)
        with D_F show ‹(t, X) ∈ ℱ ?lhs› by blast
      next
        show ‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 ⟹ (u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q
              ⟹ (t, X) ∈ ℱ ?lhs› for u2
          by (simp add: F_Renaming F_Interrupt "*"(1) "**"(1) flip: map_append)
            (metis "*"(3, 5) "**"(1, 2) list.map_disc_iff map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
      qed
    qed
  next
    fix X' s assume * : ‹X = X' - {✓(s)}› ‹t ∈ 𝒯 (Renaming P f g)›
      ‹tF t› ‹[✓(s)] ∈ 𝒯 (Renaming Q f g)›
    from "*"(2) consider u1 u2 where
      ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
    | u where ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹u ∈ 𝒯 P›
      by (auto simp add: T_Renaming)
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      fix u1 u2 assume ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
      hence ‹t ∈ 𝒟 ?lhs› by (auto simp add: D_Interrupt D_Renaming)
      with D_F show ‹(t, X) ∈ ℱ ?lhs› by blast
    next
      fix u assume ** : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹u ∈ 𝒯 P›
      from "*"(4) consider ‹Renaming Q f g = ⊥› | r where ‹s = g r› ‹[✓(r)] ∈ 𝒯 Q›
        by (simp add: Renaming_projs BOT_iff_tick_D)
          (metis map_map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff)
      thus ‹(t, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹Renaming Q f g = ⊥›
        hence ‹Q = ⊥› by (simp add: Renaming_is_BOT_iff)
        hence ‹Renaming (P △ Q) f g = ⊥› by simp
        thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_BOT "*"(3))
      next
        fix r assume ‹s = g r› ‹[✓(r)] ∈ 𝒯 Q›
        moreover from "*"(1) ‹s = g r› obtain X''
          where ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X = X'' - {✓(r)}›
          by (metis DiffD2 Diff_empty Diff_insert0 event⇩p⇩t⇩i⇩c⇩k.simps(10) insertI1 vimage_eq)
        ultimately show ‹(t, X) ∈ ℱ ?lhs›
          by (simp add: "**"(1) F_Renaming F_Interrupt)
            (metis "*"(3) "**"(1, 2) map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
      qed
    qed
  qed
qed


lemma inj_on_Renaming_Throw :
  ‹Renaming (P Θ a ∈ A. Q a) f g =
   Renaming P f g Θ b ∈ f ` A. Renaming (Q (inv_into A f b)) f g›
  (is ‹?lhs = ?rhs›) if inj_on_f : ‹inj_on f (events_of P ∪ A)›
proof -
  have $ : ‹set (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t) ∩ ev ` f ` A = {}
            ⟷ set t ∩ ev ` A = {}› if ‹t ∈ 𝒯 P› for t
  proof -
    from ‹t ∈ 𝒯 P› inj_on_f have ‹inj_on f ({a. ev a ∈ set t} ∪ A)›
      by (auto simp add: inj_on_def events_of_memI)
    thus ‹set (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t) ∩ ev ` f ` A = {}
          ⟷ set t ∩ ev ` A = {}›
      by (auto simp add: disjoint_iff image_iff inj_on_def map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff)
        (metis event⇩p⇩t⇩i⇩c⇩k.simps(9), blast)
  qed
  show ‹?lhs = ?rhs›
  proof (subst Process_eq_spec_optimized, safe)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    then obtain t1 t2 where * : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1 @ t2› ‹tF t1›
      ‹ftF t2› ‹t1 ∈ 𝒟 (P Θ a ∈ A. Q a)›
      unfolding D_Renaming by blast
    from "*"(4) consider u1 u2 where ‹t1 = u1 @ u2› ‹u1 ∈ 𝒟 P› ‹tF u1›
      ‹set u1 ∩ ev ` A = {}› ‹ftF u2›
    | u1 a u2 where ‹t1 = u1 @ ev a # u2› ‹u1 @ [ev a] ∈ 𝒯 P›
      ‹set u1 ∩ ev ` A = {}› ‹a ∈ A› ‹u2 ∈ 𝒟 (Q a)›
      unfolding D_Throw by blast
    thus ‹t ∈ 𝒟 ?rhs›
    proof cases
      fix u1 u2 assume ** : ‹t1 = u1 @ u2› ‹u1 ∈ 𝒟 P› ‹tF u1›
        ‹set u1 ∩ ev ` A = {}› ‹ftF u2›
      from "$" "**"(2) "**"(4) D_T
      have *** : ‹set (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1) ∩ ev ` f ` A = {}› by blast
      have ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 @ t2)›
        by (simp add: "*"(1) "**"(1))
      moreover from "*"(2, 3) "**"(1) have ‹ftF (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 @ t2)›
        by (simp add: front_tickFree_append map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
      moreover have ‹tF (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1)›
        by (simp add: "**"(3) map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
      ultimately show ‹t ∈ 𝒟 ?rhs›
        by (simp add: D_Throw D_Renaming)
          (use "**"(2) "**"(3) "***" front_tickFree_Nil in blast)
    next
      fix u1 a u2 assume ** : ‹t1 = u1 @ ev a # u2› ‹u1 @ [ev a] ∈ 𝒯 P›
        ‹set u1 ∩ ev ` A = {}› ‹a ∈ A› ‹u2 ∈ 𝒟 (Q a)›
      have *** : ‹set (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1) ∩ ev ` f ` A = {}›
        by (meson "$" "**"(2) "**"(3) T_F_spec is_processT3)
      have ‹tF u2› using "*"(2) "**"(1) by auto
      moreover have ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ ev (f a) # map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 @ t2›
        by (simp add: "*"(1) "**"(1))
      moreover from "**"(2) have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ [ev (f a)] ∈ 𝒯 (Renaming P f g)›
        by (auto simp add: T_Renaming )
      moreover have ‹inv_into A f (f a) = a›
        by (meson "**"(4) inj_on_Un inv_into_f_eq inj_on_f)
      ultimately show ‹t ∈ 𝒟 ?rhs›
        by (simp add: D_Throw D_Renaming)
          (metis "*"(3) "**"(4) "**"(5) "***" imageI)
    qed
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then consider t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒟 (Renaming P f g)›
      ‹tF t1› ‹set t1 ∩ ev ` f ` A = {}› ‹ftF t2›
    | t1 b t2 where ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Renaming P f g)›
      ‹set t1 ∩ ev ` f ` A = {}› ‹b ∈ f ` A›
      ‹t2 ∈ 𝒟 (Renaming (Q (inv_into A f b)) f g)›
      unfolding D_Throw by blast
    thus ‹t ∈ 𝒟 ?lhs›
    proof cases
      fix t1 t2 assume * : ‹t = t1 @ t2› ‹t1 ∈ 𝒟 (Renaming P f g)›
        ‹tF t1› ‹set t1 ∩ ev ` f ` A = {}› ‹ftF t2›
      from "*"(2) obtain u1 u2
        where ** : ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
        unfolding D_Renaming by blast
      from "*"(4) "**"(1) have ‹set u1 ∩ ev ` A = {}› by auto
      moreover have ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ (u2 @ t2)›
        by (simp add: "*"(1) "**"(1))
      moreover from "*"(3, 5) "**"(1) front_tickFree_append tickFree_append_iff
      have ‹ftF (u2 @ t2)› by blast
      ultimately show ‹t ∈ 𝒟 ?lhs›
        by (simp add: D_Renaming D_Throw)
          (use "**"(2, 4) front_tickFree_Nil in blast)
    next
      fix t1 b t2 assume * : ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Renaming P f g)›
        ‹set t1 ∩ ev ` f ` A = {}› ‹b ∈ f ` A›
        ‹t2 ∈ 𝒟 (Renaming (Q (inv_into A f b)) f g)›
      from ‹b ∈ f ` A› obtain a where ‹a ∈ A› ‹b = f a› by blast
      hence ‹inv_into A f b = a› by (meson inj_on_Un inv_into_f_f inj_on_f)
      from "*"(2) consider u1 u2 where
        ‹t1 @ [ev b] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹u2 ≠ []› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
      | u1 where ‹t1 @ [ev b] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1› ‹u1 ∈ 𝒯 P›
        by (simp add: D_T T_Renaming)
          (metis (no_types, opaque_lifting) D_T append.right_neutral)
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        fix u1 u2
        assume ** : ‹t1 @ [ev b] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹u2 ≠ []› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
        from "**"(1, 2) obtain u2' where *** : ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2'›
          by (metis butlast_append butlast_snoc)
        from "*"(3) "***" have **** : ‹set u1 ∩ ev ` A = {}› by auto
        have ***** : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ (u2' @ ev b # t2)› ‹ftF (u2' @ ev b # t2)›
          by (simp_all add: "*"(1) "***" "****" front_tickFree_append_iff)
            (metis "*"(2, 5) "***" D_imp_front_tickFree append_T_imp_tickFree
              event⇩p⇩t⇩i⇩c⇩k.disc(1) front_tickFree_Cons_iff not_Cons_self tickFree_append_iff)
        show ‹t ∈ 𝒟 ?lhs›
          by (simp add: D_Renaming D_Throw)
            (metis "**"(3) "**"(5) "****" "*****" append_Nil2 front_tickFree_Nil)
      next
        fix u1 assume ‹t1 @ [ev b] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1› ‹u1 ∈ 𝒯 P›
        then obtain u1' where ** : ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1'› ‹u1' @ [ev a] ∈ 𝒯 P›
          by (cases u1 rule: rev_cases, simp_all add: ‹b = f a› ev_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff)
            (metis Nil_is_append_conv Un_iff ‹a ∈ A› events_of_memI inj_onD
              inj_on_f last_in_set last_snoc list.distinct(1))
        from "*"(3) "**"(1) have *** : ‹set u1' ∩ ev ` A = {}› by auto
        from "*"(5) ‹inv_into A f b = a› obtain u2 u3 where
          **** : ‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 @ u3› ‹tF u2› ‹ftF u3› ‹u2 ∈ 𝒟 (Q a)›
          unfolding Renaming_projs by blast
        have ***** : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) (u1' @ ev a # u2) @ u3› ‹tF (u1' @ ev a # u2)›
          by (simp_all add: "*"(1) "**"(1) ‹b = f a› "****"(1))
            (metis "**"(2) "****"(2) T_imp_front_tickFree butlast_snoc
              front_tickFree_iff_tickFree_butlast)
        show ‹t ∈ 𝒟 ?lhs›
          by (simp add: D_Renaming D_Throw)
            (metis "**"(2) "***" "****"(3, 4) "*****"(1, 2) ‹a ∈ A›)
      qed
    qed
  next
    fix t X assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(t, X) ∈ ℱ ?lhs›
    then consider ‹t ∈ 𝒟 ?lhs›
      | u where ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P Θ a ∈ A. Q a)›
      unfolding Renaming_projs by blast
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      from same_div D_F show ‹t ∈ 𝒟 ?lhs ⟹ (t, X) ∈ ℱ ?rhs› by blast
    next
      fix u assume * : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u›
        ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P Θ a ∈ A. Q a)›
      then consider ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ P› ‹set u ∩ ev ` A = {}›
        | u1 u2   where ‹u = u1 @ u2› ‹u1 ∈ 𝒟 P› ‹tF u1› ‹set u1 ∩ ev ` A = {}› ‹ftF u2›
        | u1 a u2 where ‹u = u1 @ ev a # u2› ‹u1 @ [ev a] ∈ 𝒯 P› ‹set u1 ∩ ev ` A = {}›
          ‹a ∈ A› ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (Q a)›
        unfolding F_Throw by blast
      thus ‹(t, X) ∈ ℱ ?rhs›
      proof cases
        show ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ P ⟹ set u ∩ ev ` A = {} ⟹ (t, X) ∈ ℱ ?rhs›
          by (simp add: F_Throw F_Renaming) (metis "$" "*"(1) F_T)
      next
        fix u1 u2 assume ‹u = u1 @ u2› ‹u1 ∈ 𝒟 P› ‹tF u1› ‹set u1 ∩ ev ` A = {}› ‹ftF u2›
        hence ‹t ∈ 𝒟 ?lhs›
          by (simp add: "*"(1) D_Renaming D_Throw)
            (metis append_Nil2 front_tickFree_Nil map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree)
        with same_div D_F show ‹(t, X) ∈ ℱ ?rhs› by blast
      next
        fix u1 a u2
        assume ** : ‹u = u1 @ ev a # u2› ‹u1 @ [ev a] ∈ 𝒯 P› ‹set u1 ∩ ev ` A = {}›
          ‹a ∈ A› ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (Q a)›
        have *** : ‹set (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1) ∩ ev ` f ` A = {}›
          by (meson "$" "**"(2, 3) T_F_spec is_processT3)
        have ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ ev (f a) # map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2›
          by (simp add: "*"(1) "**"(1))
        moreover from "**"(2) have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ [ev (f a)] ∈ 𝒯 (Renaming P f g)›
          by (auto simp add: T_Renaming)
        moreover have ‹inv_into A f (f a) = a›
          by (meson "**"(4) inj_on_Un inv_into_f_f inj_on_f)
        moreover from "**"(5) have ‹(map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2, X) ∈ ℱ (Renaming (Q a) f g)›
          by (auto simp add: F_Renaming)
        ultimately show ‹(t, X) ∈ ℱ ?rhs›
          by (simp add: F_Throw) (metis "**"(4) "***" image_eqI)
      qed
    qed
  next
    fix t X assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(t, X) ∈ ℱ ?rhs›
    then consider ‹t ∈ 𝒟 ?rhs›
      | ‹(t, X) ∈ ℱ (Renaming P f g)› ‹set t ∩ ev ` f ` A = {}›
      | t1 b t2 where ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Renaming P f g)›
        ‹set t1 ∩ ev ` f ` A = {}› ‹b ∈ f ` A›
        ‹(t2, X) ∈ ℱ (Renaming (Q (inv_into A f b)) f g)›
      unfolding Throw_projs by auto
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      from same_div D_F show ‹t ∈ 𝒟 ?rhs ⟹ (t, X) ∈ ℱ ?lhs› by blast
    next
      assume * : ‹(t, X) ∈ ℱ (Renaming P f g)› ‹set t ∩ ev ` f ` A = {}›
      from "*"(1) consider ‹t ∈ 𝒟 (Renaming P f g)›
        | u where ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ P›
        unfolding Renaming_projs by blast
      thus ‹(t, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹t ∈ 𝒟 (Renaming P f g)›
        hence ‹t ∈ 𝒟 ?lhs›
          by (simp add: D_Renaming D_Throw)
            (metis (no_types, lifting) "$" "*"(2) D_T Un_Int_eq(3) append_Nil2
              front_tickFree_Nil inf_bot_right inf_sup_aci(2) set_append)
        with D_F show ‹(t, X) ∈ ℱ ?lhs› by blast
      next
        show ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u ⟹ (u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ P
              ⟹ (t, X) ∈ ℱ ?lhs› for u
          by (simp add: F_Renaming F_Throw) (metis "$" "*"(2) F_T)
      qed
    next
      fix t1 b t2
      assume * : ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Renaming P f g)›
        ‹set t1 ∩ ev ` f ` A = {}› ‹b ∈ f ` A›
        ‹(t2, X) ∈ ℱ (Renaming (Q (inv_into A f b)) f g)›
      from "*"(4) obtain a where ‹a ∈ A› ‹b = f a› by blast
      hence ‹inv_into A f b = a› by (meson inj_on_Un inv_into_f_f inj_on_f)
      from "*"(2) consider u1 u2 where
        ‹t1 @ [ev b] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹u2 ≠ []› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
      | u1 where ‹t1 @ [ev b] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1› ‹u1 ∈ 𝒯 P›
        by (simp add: D_T T_Renaming)
          (metis (no_types, opaque_lifting) D_T append.right_neutral)
      thus ‹(t, X) ∈ ℱ ?lhs›
      proof cases
        fix u1 u2
        assume ** : ‹t1 @ [ev b] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2› ‹u2 ≠ []› ‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P›
        from "**"(1, 2) obtain u2' where *** : ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ u2'›
          by (metis butlast_append butlast_snoc)
        from "*"(3) "***" have ‹set u1 ∩ ev ` A = {}› by auto
        with "**"(3-5) "***" have ‹t ∈ 𝒟 ?rhs›
          by (simp add: D_Renaming D_Throw)
            (metis "*"(1, 3) F_imp_front_tickFree ‹(t, X) ∈ ℱ ?rhs› front_tickFree_Nil
              front_tickFree_append_iff front_tickFree_dw_closed list.discI)
        with same_div D_F show ‹(t, X) ∈ ℱ ?lhs› by blast
      next
        fix u1 assume ‹t1 @ [ev b] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1› ‹u1 ∈ 𝒯 P›
        then obtain u1' where ** : ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1'› ‹u1' @ [ev a] ∈ 𝒯 P›
          by (cases u1 rule: rev_cases, simp_all add: ‹b = f a› ev_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff)
            (metis Nil_is_append_conv Un_iff ‹a ∈ A› events_of_memI inj_onD
              inj_on_f last_in_set last_snoc list.distinct(1))
        from "*"(3) "**"(1) have *** : ‹set u1' ∩ ev ` A = {}› by auto
        from "*"(5) ‹inv_into A f b = a› consider ‹t2 ∈ 𝒟 (Renaming (Q a) f g)›
          | u2 where ‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2› ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (Q a)›
          unfolding Renaming_projs by blast
        thus ‹(t, X) ∈ ℱ ?lhs›
        proof cases
          assume ‹t2 ∈ 𝒟 (Renaming (Q a) f g)›
          with "*"(1-4) ‹inv_into A f b = a› have ‹t ∈ 𝒟 ?rhs›
            by (auto simp add: D_Throw)
          with same_div D_F show ‹(t, X) ∈ ℱ ?lhs› by blast
        next
          fix u2 assume **** : ‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2›
            ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (Q a)›
          from "****"(1) have ***** : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) (u1' @ ev a # u2)›  
            by (simp add: "*"(1) "**"(1) "****" ‹b = f a›)
          show ‹(t, X) ∈ ℱ ?lhs›
            by (simp add: F_Renaming F_Throw)
              (use "**"(2) "***" "****"(2) "*****" ‹a ∈ A› in blast)
        qed
      qed
    qed
  qed
qed



subsection ‹\<^const>‹Renaming› and \<^const>‹Hiding››

text ‹When \<^term>‹f› is one to one, \<^term>‹Renaming (P \ S) f› will behave like we expect it to do.›

lemma strict_mono_map: ‹strict_mono g ⟹ strict_mono (λi. map f (g i))›
  unfolding strict_mono_def less_eq_list_def less_list_def prefix_def by fastforce



lemma trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k :
  ‹inj_on (map_event⇩p⇩t⇩i⇩c⇩k f g) (set s ∪ ev ` S) ⟹
   trace_hide (map (map_event⇩p⇩t⇩i⇩c⇩k f g) s) (ev ` f ` S) = 
   map (map_event⇩p⇩t⇩i⇩c⇩k f g) (trace_hide s (ev ` S))›
proof (induct s)
  case Nil
  show ?case by simp
next
  case (Cons e s)
  hence * : ‹trace_hide (map (map_event⇩p⇩t⇩i⇩c⇩k f g) s) (ev ` f ` S) = 
             map (map_event⇩p⇩t⇩i⇩c⇩k f g) (trace_hide s (ev ` S))› by fastforce
  from Cons.prems[unfolded inj_on_def, rule_format, of e, simplified] show ?case
    apply (simp add: "*")
    apply (simp add: image_iff)
    by (metis event⇩p⇩t⇩i⇩c⇩k.simps(9))
qed


lemma inj_on_map_event⇩p⇩t⇩i⇩c⇩k_set_T:
  ‹inj_on (map_event⇩p⇩t⇩i⇩c⇩k f g) (set s)› if ‹inj_on f (events_of P)› ‹s ∈ 𝒯 P›
proof (rule inj_onI)
  show ‹e ∈ set s ⟹ e' ∈ set s ⟹ map_event⇩p⇩t⇩i⇩c⇩k f g e = map_event⇩p⇩t⇩i⇩c⇩k f g e' ⟹ e = e'› for e e'
    by (cases e; cases e'; simp)
      (meson events_of_memI inj_onD that(1, 2),
        metis T_imp_front_tickFree event⇩p⇩t⇩i⇩c⇩k.disc(2) event⇩p⇩t⇩i⇩c⇩k.simps(2) front_tickFree_Cons_iff that(2)
        front_tickFree_nonempty_append_imp list.distinct(1) snoc_eq_iff_butlast split_list_last)
qed


theorem bij_Renaming_Hiding: ‹Renaming (P \ S) f g = Renaming P f g \ f ` S›
  (is ‹?lhs = ?rhs›) if bij_f: ‹bij f› and bij_g : ‹bij g›
proof -
  have inj_on_map_event⇩p⇩t⇩i⇩c⇩k : ‹inj_on (map_event⇩p⇩t⇩i⇩c⇩k f g) X› for X
  proof (rule inj_onI)
    show ‹e ∈ X ⟹ e' ∈ X ⟹ map_event⇩p⇩t⇩i⇩c⇩k f g e = map_event⇩p⇩t⇩i⇩c⇩k f g e' ⟹ e = e'› for e e'
      by (cases e; cases e'; simp)
        (metis bij_f bij_pointE, metis bij_g bij_pointE)
  qed
  have inj_on_map_event⇩p⇩t⇩i⇩c⇩k_inv : ‹inj_on (map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g)) X› for X
  proof (rule inj_onI)
    show ‹e ∈ X ⟹ e' ∈ X ⟹ map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g) e = map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g) e'
          ⟹ e = e'› for e e'
      by (cases e; cases e', simp_all)
        (metis bij_f bij_inv_eq_iff, metis bij_g bij_inv_eq_iff)
  qed
  show ‹?lhs = ?rhs›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    then obtain s1 s2 where * : ‹tickFree s1› ‹front_tickFree s2›
      ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹s1 ∈ 𝒟 (P \ S)›
      by (simp add: D_Renaming) blast
    from "*"(4) obtain t u
      where ** : ‹front_tickFree u› ‹tickFree t› ‹s1 = trace_hide t (ev ` S) @ u›
        ‹t ∈ 𝒟 P ∨ (∃h. isInfHiddenRun h P S ∧ t ∈ range h)›
      by (simp add: D_Hiding) blast
    from "**"(4) show ‹s ∈ 𝒟 ?rhs›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 P›
      hence ‹front_tickFree (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u @ s2) ∧ tickFree (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t) ∧
             s = trace_hide (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t) (ev ` f ` S) @ map (map_event⇩p⇩t⇩i⇩c⇩k f g) u @ s2 ∧
             map (map_event⇩p⇩t⇩i⇩c⇩k f g) t ∈ 𝒟 (Renaming P f g)›
        apply (simp add: "*"(3) "**"(2, 3) map_event⇩p⇩t⇩i⇩c⇩k_tickFree, intro conjI)
          apply (metis "*"(1, 2) "**"(1) "**"(3) front_tickFree_append_iff
            map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree map_event⇩p⇩t⇩i⇩c⇩k_tickFree tickFree_append_iff)
         apply (simp add: trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k inj_on_map_event⇩p⇩t⇩i⇩c⇩k)
        by (metis (mono_tags, lifting) "**"(2) CollectI D_Renaming append.right_neutral front_tickFree_Nil)
      thus ‹s ∈ 𝒟 ?rhs› by (simp add: D_Hiding) blast
    next
      assume ‹∃h. isInfHiddenRun h P S ∧ t ∈ range h›
      then obtain h where ‹isInfHiddenRun h P S› ‹t ∈ range h› by blast
      hence ‹front_tickFree (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u @ s2) ∧
             tickFree (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t) ∧
             s = trace_hide (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t) (ev ` f ` S) @ map (map_event⇩p⇩t⇩i⇩c⇩k f g) u @ s2 ∧
             isInfHiddenRun (λi. map (map_event⇩p⇩t⇩i⇩c⇩k f g) (h i)) (Renaming P f g) (f ` S) ∧ 
             map (map_event⇩p⇩t⇩i⇩c⇩k f g) t ∈ range (λi. map (map_event⇩p⇩t⇩i⇩c⇩k f g) (h i))›
        apply (simp add: "*"(3) "**"(2, 3) map_event⇩p⇩t⇩i⇩c⇩k_tickFree, intro conjI)
             apply (metis "*"(1, 2) "**"(3) front_tickFree_append map_event⇩p⇩t⇩i⇩c⇩k_tickFree tickFree_append_iff)
            apply (rule trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k, symmetric])
           apply (solves ‹rule strict_mono_map, simp›)
          apply (solves ‹auto simp add: T_Renaming›)
         apply (subst (1 2) trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k])
        by metis blast
      thus ‹s ∈ 𝒟 ?rhs› by (simp add: D_Hiding) blast
    qed
  next
    fix s
    assume ‹s ∈ 𝒟 ?rhs›
    then obtain t u
      where * : ‹front_tickFree u› ‹tickFree t› ‹s = trace_hide t (ev ` f ` S) @ u›
        ‹t ∈ 𝒟 (Renaming P f g) ∨ 
                 (∃h. isInfHiddenRun h (Renaming P f g) (f ` S) ∧ t ∈ range h)›
      by (simp add: D_Hiding) blast
    from "*"(4) show ‹s ∈ 𝒟 ?lhs›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 (Renaming P f g)›
      then obtain t1 t2 where ** : ‹tickFree t1› ‹front_tickFree t2› 
        ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1 @ t2› ‹t1 ∈ 𝒟 P›
        by (simp add: D_Renaming) blast
      have ‹tickFree (trace_hide t1 (ev ` S)) ∧ 
            front_tickFree (trace_hide t2 (ev ` f ` S) @ u) ∧
            trace_hide (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1) (ev ` f ` S) @ trace_hide t2 (ev ` f ` S) @ u =
            map (map_event⇩p⇩t⇩i⇩c⇩k f g) (trace_hide t1 (ev ` S)) @ trace_hide t2 (ev ` f ` S) @ u ∧
            trace_hide t1 (ev ` S) ∈ 𝒟 (P \ S)›
        apply (simp, intro conjI)
        using "**"(1) Hiding_tickFree apply blast
        using "*"(1, 2) "**"(3) Hiding_tickFree front_tickFree_append tickFree_append_iff apply blast
         apply (rule trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k])
        using "**"(4) mem_D_imp_mem_D_Hiding by blast
      thus ‹s ∈ 𝒟 ?lhs› by (simp add: D_Renaming "*"(3) "**"(3)) blast
    next
      have inv_S: ‹S = inv f ` f ` S› by (simp add: bij_is_inj bij_f)
      have inj_inv_f: ‹inj (inv f)› 
        by (simp add: bij_imp_bij_inv bij_is_inj bij_f)
      have ** : ‹map (map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g) ∘ map_event⇩p⇩t⇩i⇩c⇩k f g) v = v› for v
        by (induct v, simp_all)
          (metis bij_f bij_g bij_inv_eq_iff event⇩p⇩t⇩i⇩c⇩k.exhaust event⇩p⇩t⇩i⇩c⇩k.simps(9) map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff)
      assume ‹∃h. isInfHiddenRun h (Renaming P f g) (f ` S) ∧ t ∈ range h›
      then obtain h
        where *** : ‹isInfHiddenRun h (Renaming P f g) (f ` S)› ‹t ∈ range h› by blast
      then consider t1 where ‹t1 ∈ 𝒯 P› ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1›
        | t1 t2 where ‹tickFree t1› ‹front_tickFree t2› 
          ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1 @ t2› ‹t1 ∈ 𝒟 P›
        by (simp add: T_Renaming) blast
      thus ‹s ∈ 𝒟 ?lhs›
      proof cases
        fix t1 assume **** : ‹t1 ∈ 𝒯 P› ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1›
        have ***** : ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g)) t› by (simp add: "****"(2) "**")
        have ****** : ‹trace_hide t1 (ev ` S) = trace_hide t1 (ev ` S) ∧
                       isInfHiddenRun (λi. map (map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g)) (h i)) P S ∧ 
                       t1 ∈ range (λi. map (map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g)) (h i))›
          apply (simp add: "***"(1) strict_mono_map, intro conjI)
            apply (subst Renaming_inv[where f = f and g = g, symmetric])
              apply (solves ‹simp add: bij_is_inj bij_f›)
             apply (solves ‹simp add: bij_is_inj bij_g›)

          using "***"(1) apply (subst T_Renaming, blast)
           apply (subst (1 2) inv_S, subst (1 2) trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k_inv])
           apply (metis "***"(1))
          using "***"(2) "*****" by blast
        have ‹tickFree (trace_hide t1 (ev ` S)) ∧ front_tickFree t1 ∧
              trace_hide (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1) (ev ` f ` S) @ u = 
              map (map_event⇩p⇩t⇩i⇩c⇩k f g) (trace_hide t1 (ev ` S)) @ u ∧ 
              trace_hide t1 (ev ` S) ∈ 𝒟 (P \ S)›
          apply (simp, intro conjI)
          using "*"(2) "****"(2) map_event⇩p⇩t⇩i⇩c⇩k_tickFree Hiding_tickFree apply blast
          using "****"(1) is_processT2_TR apply blast
           apply (rule trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k])
          apply (simp add: D_Renaming D_Hiding)
          using "*"(2) "*****" "******" map_event⇩p⇩t⇩i⇩c⇩k_tickFree front_tickFree_Nil by blast
        with "*"(1) show ‹s ∈ 𝒟 ?lhs› by (simp add: D_Renaming "*"(3) "****"(2)) blast
      next
        fix t1 t2 assume **** : ‹tickFree t1› ‹front_tickFree t2›
          ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1 @ t2› ‹t1 ∈ 𝒟 P›
        have ‹tickFree (trace_hide t1 (ev ` S)) ∧
              front_tickFree (trace_hide t2 (ev ` f ` S) @ u) ∧
              trace_hide (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1) (ev ` f ` S) @ trace_hide t2 (ev ` f ` S) @ u =
              map (map_event⇩p⇩t⇩i⇩c⇩k f g) (trace_hide t1 (ev ` S)) @ trace_hide t2 (ev ` f ` S) @ u ∧
              trace_hide t1 (ev ` S) ∈ 𝒟 (P \ S)›
          apply (simp, intro conjI)
          using "****"(1) Hiding_tickFree apply blast
          using "*"(1, 2) "****"(3) Hiding_tickFree front_tickFree_append tickFree_append_iff apply blast
           apply (rule trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k])
          using "****"(4) mem_D_imp_mem_D_Hiding by blast
        thus ‹s ∈ 𝒟 ?lhs› by (simp add: D_Renaming "*"(3) "****"(3)) blast
      qed
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?lhs›
    then consider ‹s ∈ 𝒟 ?lhs›
      | s1 where ‹(s1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P \ S)› ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1›
      by (simp add: F_Renaming D_Renaming) blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      from D_F same_div show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
    next
      fix s1 assume * : ‹(s1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P \ S)›
        ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1›
      from this(1) consider ‹s1 ∈ 𝒟 (P \ S)›
        | t where ‹s1 = trace_hide t (ev ` S)› ‹(t, map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ ev ` S) ∈ ℱ P›
        by (simp add: F_Hiding D_Hiding) blast
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        assume ‹s1 ∈ 𝒟 (P \ S)›
        then obtain t u
          where ** : ‹front_tickFree u› ‹tickFree t› ‹s1 = trace_hide t (ev ` S) @ u›
            ‹t ∈ 𝒟 P ∨ (∃g. isInfHiddenRun g P S ∧ t ∈ range g)›
          by (simp add: D_Hiding) blast
        have *** : ‹front_tickFree (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u) ∧ tickFree (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t) ∧
                    map (map_event⇩p⇩t⇩i⇩c⇩k f g) (trace_hide t (ev ` S)) @ map (map_event⇩p⇩t⇩i⇩c⇩k f g) u = 
                    trace_hide (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t) (ev ` f ` S) @ (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u)›
          by (simp add: map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree map_event⇩p⇩t⇩i⇩c⇩k_tickFree "**"(1, 2))
            (rule trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k, symmetric])
        from "**"(4) show ‹(s, X) ∈ ℱ ?rhs›
        proof (elim disjE exE)
          assume ‹t ∈ 𝒟 P›
          hence $ : ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) t ∈ 𝒟 (Renaming P f g)›
            apply (simp add: D_Renaming)
            using "**"(2) front_tickFree_Nil by blast
          show ‹(s, X) ∈ ℱ ?rhs›
            by (simp add: F_Hiding) (metis "$" "*"(2) "**"(3) "***" map_append)
        next
          fix h assume ‹isInfHiddenRun h P S ∧ t ∈ range h›
          hence $ : ‹isInfHiddenRun (λi. map (map_event⇩p⇩t⇩i⇩c⇩k f g) (h i)) (Renaming P f g) (f ` S) ∧ 
                     map (map_event⇩p⇩t⇩i⇩c⇩k f g) t ∈ range (λi. map (map_event⇩p⇩t⇩i⇩c⇩k f g) (h i))›
            apply (subst (1 2) trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k])
            by (simp add: strict_mono_map T_Renaming image_iff) (metis (mono_tags, lifting))
          show ‹(s, X) ∈ ℱ ?rhs›
            apply (simp add: F_Hiding)
              (* TODO: break this smt *)
            by (smt (verit, del_insts) "$" "*"(2) "**"(3) "***" map_append)
        qed
      next
        fix t assume ** : ‹s1 = trace_hide t (ev ` S)› 
          ‹(t, map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ ev ` S) ∈ ℱ P›
        have *** : ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ map_event⇩p⇩t⇩i⇩c⇩k f g -` ev ` f ` S = map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ ev ` S›
          by (auto simp add: image_iff map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff) (metis bij_f bij_pointE)
        have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) (trace_hide t (ev ` S)) = 
              trace_hide (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t) (ev ` f ` S) ∧
              (map (map_event⇩p⇩t⇩i⇩c⇩k f g) t, X ∪ ev ` f ` S) ∈ ℱ (Renaming P f g)›
          apply (intro conjI)
           apply (rule trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k, symmetric])
          apply (simp add: F_Renaming)
          using "**"(2) "***" by auto
        show ‹(s, X) ∈ ℱ ?rhs›
          apply (simp add: F_Hiding "*"(2) "**"(1))
          using ‹?this› by blast
      qed
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?rhs›
    then consider ‹s ∈ 𝒟 ?rhs›
      | t where ‹s = trace_hide t (ev ` f ` S)› ‹(t, X ∪ ev ` f ` S) ∈ ℱ (Renaming P f g)›
      by (simp add: F_Hiding D_Hiding) blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      from D_F same_div show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
    next
      fix t assume ‹s = trace_hide t (ev ` f ` S)› ‹(t, X ∪ ev ` f ` S) ∈ ℱ (Renaming P f g)›
      then obtain t
        where * : ‹s = trace_hide t (ev ` f ` S)›
          ‹(t, X ∪ ev ` f ` S) ∈ ℱ (Renaming P f g)› by blast
      have ** : ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ map_event⇩p⇩t⇩i⇩c⇩k f g -` ev ` f ` S = map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ ev ` S›
        by (auto simp add: image_iff map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff) (metis bij_f bij_pointE)
      have ‹(∃s1. (s1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ map_event⇩p⇩t⇩i⇩c⇩k f g -` ev ` f ` S) ∈ ℱ P ∧ t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1) ∨ 
            (∃s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2 ∧ s1 ∈ 𝒟 P)›
        using "*"(2) by (auto simp add: F_Renaming)
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof (elim disjE exE conjE)
        fix s1
        assume ‹(s1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ map_event⇩p⇩t⇩i⇩c⇩k f g -` ev ` f ` S) ∈ ℱ P› ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1›
        hence ‹(trace_hide s1 (ev ` S), map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P \ S) ∧
               s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) (trace_hide s1 (ev ` S))›
          apply (simp add: "*"(1) F_Hiding "**", intro conjI)
          by blast (rule trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k])
        show ‹(s, X) ∈ ℱ ?lhs›
          apply (simp add: F_Renaming)
          using ‹?this› by blast
      next
        fix s1 s2
        assume ‹tickFree s1› ‹front_tickFree s2› ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹s1 ∈ 𝒟 P›
        hence ‹tickFree (trace_hide s1 (ev ` S)) ∧ 
               front_tickFree (trace_hide s2 (ev ` f ` S)) ∧ 
               s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) (trace_hide s1 (ev ` S)) @ trace_hide s2 (ev ` f ` S) ∧ 
               trace_hide s1 (ev ` S) ∈ 𝒟 (P \ S)›
          apply (simp add: F_Renaming "*"(1), intro conjI)
          using Hiding_tickFree apply blast
          using Hiding_front_tickFree apply blast
           apply (rule trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[OF inj_on_map_event⇩p⇩t⇩i⇩c⇩k])
          using mem_D_imp_mem_D_Hiding by blast
        show ‹(s, X) ∈ ℱ ?lhs›
          apply (simp add: F_Renaming)
          using ‹?this› by blast
      qed
    qed
  qed
qed



subsection ‹\<^const>‹Renaming› and \<^const>‹Sync››

text ‹Idem for the synchronization: when \<^term>‹f› is one to one, 
      \<^term>‹Renaming (P ⟦S⟧ Q)› will behave as expected.›

lemma bij_map_setinterleaving_iff_setinterleaving :
  ‹map f r setinterleaves ((map f t, map f u), f ` S) ⟷
   r setinterleaves ((t, u), S)› if bij_f : ‹bij f›
proof (induct ‹(t, S, u)› arbitrary: t u r rule: setinterleaving.induct)
  case 1
  thus ?case by simp
next
  case (2 y u)
  show ?case
  proof (cases ‹y ∈ S›)
    show ‹y ∈ S ⟹ ?case› by simp
  next
    assume ‹y ∉ S›
    hence ‹f y ∉ f ` S› by (metis bij_betw_imp_inj_on inj_image_mem_iff bij_f)
    with "2.hyps"[OF ‹y ∉ S›, of ‹tl r›] show ?case
      by (cases r; simp add: ‹y ∉ S›) (metis bij_pointE bij_f)
  qed
next
  case (3 x t)
  show ?case
  proof (cases ‹x ∈ S›)
    show ‹x ∈ S ⟹ ?case› by simp
  next
    assume ‹x ∉ S›
    hence ‹f x ∉ f ` S› by (metis bij_betw_imp_inj_on inj_image_mem_iff bij_f)
    with "3.hyps"[OF ‹x ∉ S›, of ‹tl r›] show ?case
      by (cases r; simp add: ‹x ∉ S›) (metis bij_pointE bij_f)
  qed
next
  case (4 x t y u)
  have  * : ‹x ≠ y ⟹ f x ≠ f y› by (metis bij_pointE bij_f)
  have ** : ‹f z ∈ f ` S ⟷ z ∈ S› for z
    by (meson bij_betw_def inj_image_mem_iff bij_f)
  show ?case
  proof (cases ‹x ∈ S›; cases ‹y ∈ S›)
    from "4.hyps"(1)[of ‹tl r›] show ‹x ∈ S ⟹ y ∈ S ⟹ ?case›
      by (cases r; simp add: "*") (metis bij_pointE bij_f)
  next
    from "4.hyps"(2)[of ‹tl r›] show ‹x ∈ S ⟹ y ∉ S ⟹ ?case›
      by (cases r; simp add: "**") (metis bij_pointE bij_f)
  next
    from "4.hyps"(5)[of ‹tl r›] show ‹x ∉ S ⟹ y ∈ S ⟹ ?case›
      by (cases r; simp add: "**") (metis bij_pointE bij_f)
  next
    from "4.hyps"(3, 4)[of ‹tl r›] show ‹x ∉ S ⟹ y ∉ S ⟹ ?case›
      by (cases r; simp add: "**") (metis bij_pointE bij_f)
  qed
qed


theorem bij_Renaming_Sync:
  ‹Renaming (P ⟦S⟧ Q) f g = Renaming P f g ⟦f ` S⟧ Renaming Q f g›
  (is ‹?lhs P Q = ?rhs P Q›) if bij_f: ‹bij f› and bij_g : ‹bij g›
proof -
  ― ‹Four intermediate results.›
  have bij_map_event⇩p⇩t⇩i⇩c⇩k : ‹bij (map_event⇩p⇩t⇩i⇩c⇩k f g)›
  proof (rule bijI)
    show ‹inj (map_event⇩p⇩t⇩i⇩c⇩k f g)›
    proof (rule injI)
      show ‹map_event⇩p⇩t⇩i⇩c⇩k f g e = map_event⇩p⇩t⇩i⇩c⇩k f g e' ⟹ e = e'› for e e'
        by (cases e; cases e'; simp)
          (metis bij_f bij_pointE, metis bij_g bij_pointE)
    qed
  next
    show ‹surj (map_event⇩p⇩t⇩i⇩c⇩k f g)›
    proof (rule surjI)
      show ‹map_event⇩p⇩t⇩i⇩c⇩k f g (map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g) e) = e› for e
        by (cases e, simp_all)
          (meson bij_f bij_inv_eq_iff, meson bij_g bij_inv_eq_iff)
    qed
  qed
  moreover have ‹map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g) ∘ map_event⇩p⇩t⇩i⇩c⇩k f g = id›
  proof (rule ext)
    show ‹(map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g) ∘ map_event⇩p⇩t⇩i⇩c⇩k f g) e = id e› for e
      by (cases e, simp_all)
        (meson bij_betw_def bij_f inv_f_eq, meson bij_betw_def bij_g inv_f_eq)
  qed
  ultimately have inv_map_event⇩p⇩t⇩i⇩c⇩k_is_map_event⇩p⇩t⇩i⇩c⇩k_inv :
    ‹inv (map_event⇩p⇩t⇩i⇩c⇩k f g) = map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g)›
    by (metis bij_betw_imp_inj_on bij_betw_imp_surj_on inv_o_cancel surj_fun_eq)
  have sets_S_eq : ‹map_event⇩p⇩t⇩i⇩c⇩k f g ` (range tick ∪ ev ` S) = range tick ∪ ev ` f ` S›
    by (auto simp add: image_iff)
      (metis Un_iff bij_g bij_pointE event⇩p⇩t⇩i⇩c⇩k.simps(10) rangeI,
        metis Un_iff event⇩p⇩t⇩i⇩c⇩k.simps(9) imageI)
  have inj_map_event⇩p⇩t⇩i⇩c⇩k : ‹inj (map_event⇩p⇩t⇩i⇩c⇩k f g)›
    and inj_inv_map_event⇩p⇩t⇩i⇩c⇩k : ‹inj (inv (map_event⇩p⇩t⇩i⇩c⇩k f g))›
    by (use bij_betw_imp_inj_on bij_map_event⇩p⇩t⇩i⇩c⇩k in blast)
      (meson bij_betw_imp_inj_on bij_betw_inv_into bij_map_event⇩p⇩t⇩i⇩c⇩k)
  show ‹?lhs P Q = ?rhs P Q›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 (?lhs P Q)›
    then obtain s1 s2 where * : ‹tickFree s1› ‹front_tickFree s2›
      ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹s1 ∈ 𝒟 (P ⟦S⟧ Q)›
      by (simp add: D_Renaming) blast
    from "*"(4) obtain t u r v 
      where ** : ‹front_tickFree v› ‹tickFree r ∨ v = []› 
        ‹s1 = r @ v› ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
        ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P› 
      by (simp add: D_Sync) blast
    { fix t u P Q
      assume assms : ‹r setinterleaves ((t, u), range tick ∪ ev ` S)› 
        ‹t ∈ 𝒟 P› ‹u ∈ 𝒯 Q›
      have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) r setinterleaves 
            ((map (map_event⇩p⇩t⇩i⇩c⇩k f g) t, map (map_event⇩p⇩t⇩i⇩c⇩k f g) u), range tick ∪ ev ` f ` S)›
        by (metis assms(1) bij_map_setinterleaving_iff_setinterleaving bij_map_event⇩p⇩t⇩i⇩c⇩k sets_S_eq)
      moreover have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) t ∈ 𝒟 (Renaming P f g)›
        apply (cases ‹tickFree t›; simp add: D_Renaming)
        using assms(2) front_tickFree_Nil apply blast
        by (metis D_T D_imp_front_tickFree append_T_imp_tickFree assms(2) front_tickFree_Cons_iff
            is_processT9 list.simps(3) map_append nonTickFree_n_frontTickFree map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree)
      moreover have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u ∈ 𝒯 (Renaming Q f g)›
        using assms(3) by (simp add: T_Renaming) blast
      ultimately have ‹s ∈ 𝒟 (?rhs P Q)›
        by (simp add: D_Sync "*"(3) "**"(3))
          (metis "*"(1, 2) "**"(3) map_event⇩p⇩t⇩i⇩c⇩k_tickFree front_tickFree_append tickFree_append_iff)
    } note *** = this

    from "**"(4, 5) "***" show ‹s ∈ 𝒟 (?rhs P Q)›
      apply (elim disjE)
      using "**"(4) "***" apply blast
      using "**"(4) "***" by (subst Sync_commute) blast
  next
    fix s
    assume ‹s ∈ 𝒟 (?rhs P Q)›
    then obtain t u r v
      where * : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹s = r @ v› 
        ‹r setinterleaves ((t, u), range tick ∪ ev ` f ` S)›
        ‹t ∈ 𝒟 (Renaming P f g) ∧ u ∈ 𝒯 (Renaming Q f g) ∨
                 t ∈ 𝒟 (Renaming Q f g) ∧ u ∈ 𝒯 (Renaming P f g)›
      by (simp add: D_Sync) blast

    { fix t u P Q
      assume assms : ‹r setinterleaves ((t, u), range tick ∪ ev ` f ` S)›
        ‹t ∈ 𝒟 (Renaming P f g)› ‹u ∈ 𝒯 (Renaming Q f g)›
      have ‹inv (map_event⇩p⇩t⇩i⇩c⇩k f g) ` (range tick ∪ ev ` f ` S) =
            inv (map_event⇩p⇩t⇩i⇩c⇩k f g) ` map_event⇩p⇩t⇩i⇩c⇩k f g ` (range tick ∪ ev ` S)›
        using sets_S_eq by presburger
      from bij_map_setinterleaving_iff_setinterleaving
        [THEN iffD2, OF _ assms(1), of ‹inv (map_event⇩p⇩t⇩i⇩c⇩k f g)›,
          simplified this image_inv_f_f[OF inj_map_event⇩p⇩t⇩i⇩c⇩k]]
      have ** : ‹(map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) r) setinterleaves
                 ((map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) t, map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) u), range tick ∪ ev ` S)›
        using bij_betw_inv_into bij_map_event⇩p⇩t⇩i⇩c⇩k by blast
      from assms(2) obtain s1 s2
        where ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ 𝒟 P›
        by (auto simp add: D_Renaming)
      hence ‹map (map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g)) t ∈ 𝒟 (Renaming (Renaming P f g) (inv f) (inv g))›
        apply (simp add: D_Renaming)
        apply (rule_tac x = ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1› in exI)
        apply (rule_tac x = ‹map (map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g)) s2› in exI)
        by simp (metis append_Nil2 front_tickFree_Nil map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
      hence *** : ‹map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) t ∈ 𝒟 P›
        by (metis Renaming_inv bij_def bij_f bij_g inv_map_event⇩p⇩t⇩i⇩c⇩k_is_map_event⇩p⇩t⇩i⇩c⇩k_inv)
      have ‹map (map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g)) u ∈ 𝒯 (Renaming (Renaming Q f g) (inv f) (inv g))›
        using assms(3) by (subst T_Renaming, simp) blast
      hence **** : ‹map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) u ∈ 𝒯 Q›
        by (simp add: Renaming_inv bij_f bij_g bij_is_inj inv_map_event⇩p⇩t⇩i⇩c⇩k_is_map_event⇩p⇩t⇩i⇩c⇩k_inv)
      have ***** : ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g ∘ inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) r = r›
        by (metis (no_types, lifting) bij_betw_imp_inj_on bij_betw_inv_into bij_map_event⇩p⇩t⇩i⇩c⇩k inj_iff list.map_comp list.map_id)
      have ‹s ∈ 𝒟 (?lhs P Q)›
      proof (cases ‹tickFree r›)
        assume ‹tickFree r›
        have $ : ‹r @ v = map (map_event⇩p⇩t⇩i⇩c⇩k f g) (map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) r) @ v›
          by (simp add: "*****")
        show ‹s ∈ 𝒟 (?lhs P Q)›
          apply (simp add: D_Renaming D_Sync "*"(3))
          by (metis "$" "*"(1) "**" "***" "****" map_event⇩p⇩t⇩i⇩c⇩k_tickFree ‹tickFree r› 
              append.right_neutral append_same_eq front_tickFree_Nil)
      next
        assume ‹¬ tickFree r›
        then obtain r' res where $ : ‹r = r' @ [✓(res)]› ‹tickFree r'›
          by (metis D_imp_front_tickFree assms butlast_snoc front_tickFree_charn
              front_tickFree_single ftf_Sync is_processT2_TR list.distinct(1)
              nonTickFree_n_frontTickFree self_append_conv2)
        then obtain t' u'
          where $$ : ‹t = t' @ [✓(res)]› ‹u = u' @ [✓(res)]›
          by (metis D_imp_front_tickFree SyncWithTick_imp_NTF T_imp_front_tickFree assms)
        hence $$$ : ‹(map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) r') setinterleaves
                     ((map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) t', map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) u'),
                      range tick ∪ ev ` S)›
          by (metis "$"(1) append_same_eq assms(1) bij_betw_imp_surj_on
              bij_map_setinterleaving_iff_setinterleaving bij_map_event⇩p⇩t⇩i⇩c⇩k
              ftf_Sync32 inj_imp_bij_betw_inv inj_map_event⇩p⇩t⇩i⇩c⇩k sets_S_eq)
        from "***" $$(1) have *** : ‹map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) t' ∈ 𝒟 P› 
          by simp (use inv_map_event⇩p⇩t⇩i⇩c⇩k_is_map_event⇩p⇩t⇩i⇩c⇩k_inv is_processT9 in force)
        from "****" $$(2) have **** : ‹map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) u' ∈ 𝒯 Q›
          using is_processT3_TR prefixI by simp blast
        have $$$$ : ‹r = map (map_event⇩p⇩t⇩i⇩c⇩k f g) (map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) r') @ [✓(res)]›
          using "$" "*****" by auto
        show ‹s ∈ 𝒟 (?lhs P Q)›
          by (simp add: D_Renaming D_Sync "*"(3) "$$$")
            (metis "$"(1) "$"(2) "$$$" "$$$$" "*"(2) "***" "****" map_event⇩p⇩t⇩i⇩c⇩k_tickFree ‹¬ tickFree r›
              append.right_neutral append_same_eq front_tickFree_Nil front_tickFree_single)
      qed
    } note ** = this
    show ‹s ∈ 𝒟 (?lhs P Q)› by (metis "*"(4, 5) "**" Sync_commute)
  next
    fix s X
    assume same_div : ‹𝒟 (?lhs P Q) = 𝒟 (?rhs P Q)›
    assume ‹(s, X) ∈ ℱ (?lhs P Q)›
    then consider ‹s ∈ 𝒟 (?lhs P Q)›
      | s1 where ‹(s1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P ⟦S⟧ Q)› ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1›
      by (simp add: F_Renaming D_Renaming) blast
    thus ‹(s, X) ∈ ℱ (?rhs P Q)›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 (?lhs P Q) ⟹ (s, X) ∈ ℱ (?rhs P Q)› by blast
    next
      fix s1 assume * : ‹(s1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P ⟦S⟧ Q)› 
        ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1›
      from "*"(1) consider ‹s1 ∈ 𝒟 (P ⟦S⟧ Q)›
        | t_P t_Q X_P X_Q 
        where ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q› 
          ‹s1 setinterleaves ((t_P, t_Q), range tick ∪ ev ` S)›
          ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
        by (auto simp add: F_Sync D_Sync)
      thus ‹(s, X) ∈ ℱ (?rhs P Q)›
      proof cases
        assume ‹s1 ∈ 𝒟 (P ⟦S⟧ Q)›
        hence ‹s ∈ 𝒟 (?lhs P Q)›
          apply (cases ‹tickFree s1›; simp add: D_Renaming "*"(2)) 
          using front_tickFree_Nil apply blast
          by (metis (no_types, lifting) map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree butlast_snoc front_tickFree_iff_tickFree_butlast
              front_tickFree_single map_butlast nonTickFree_n_frontTickFree process_charn)
        with same_div D_F show ‹(s, X) ∈ ℱ (?rhs P Q)› by blast
      next
        fix t_P t_Q X_P X_Q
        assume ** : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹s1 setinterleaves ((t_P, t_Q), range tick ∪ ev ` S)›
          ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
        have ‹(map (map_event⇩p⇩t⇩i⇩c⇩k f g) t_P, (map_event⇩p⇩t⇩i⇩c⇩k f g) ` X_P) ∈ ℱ (Renaming P f g)›
          by (simp add: F_Renaming)
            (metis "**"(1) bij_betw_def bij_map_event⇩p⇩t⇩i⇩c⇩k inj_vimage_image_eq)  
        moreover have ‹(map (map_event⇩p⇩t⇩i⇩c⇩k f g) t_Q, (map_event⇩p⇩t⇩i⇩c⇩k f g) ` X_Q) ∈ ℱ (Renaming Q f g)›
          by (simp add: F_Renaming)
            (metis "**"(2) bij_betw_imp_inj_on bij_map_event⇩p⇩t⇩i⇩c⇩k inj_vimage_image_eq)
        moreover have ‹s setinterleaves ((map (map_event⇩p⇩t⇩i⇩c⇩k f g) t_P, map (map_event⇩p⇩t⇩i⇩c⇩k f g) t_Q),
                                         range tick ∪ ev ` f ` S)›
          by (metis "*"(2) "**"(3) bij_map_event⇩p⇩t⇩i⇩c⇩k sets_S_eq
              bij_map_setinterleaving_iff_setinterleaving)
        moreover have ‹X = ((map_event⇩p⇩t⇩i⇩c⇩k f g) ` X_P ∪ (map_event⇩p⇩t⇩i⇩c⇩k f g) ` X_Q) ∩ (range tick ∪ ev ` f ` S) ∪
                  (map_event⇩p⇩t⇩i⇩c⇩k f g) ` X_P ∩ (map_event⇩p⇩t⇩i⇩c⇩k f g) ` X_Q›
          apply (rule inj_image_eq_iff[THEN iffD1, OF inj_inv_map_event⇩p⇩t⇩i⇩c⇩k])
          apply (subst bij_vimage_eq_inv_image[OF bij_map_event⇩p⇩t⇩i⇩c⇩k, symmetric])
          apply (subst "**"(4), fold image_Un sets_S_eq)
          apply (subst (1 2) image_Int[OF inj_map_event⇩p⇩t⇩i⇩c⇩k, symmetric])
          apply (fold image_Un)
          apply (subst image_inv_f_f[OF inj_map_event⇩p⇩t⇩i⇩c⇩k])
          by simp
        ultimately show ‹(s, X) ∈ ℱ (?rhs P Q)›
          by (simp add: F_Sync) blast
      qed
    qed
  next
    fix s X
    assume same_div : ‹𝒟 (?lhs P Q) = 𝒟 (?rhs P Q)›
    assume ‹(s, X) ∈ ℱ (?rhs P Q)›
    then consider ‹s ∈ 𝒟 (?rhs P Q)›
      | t_P t_Q X_P X_Q where
        ‹(t_P, X_P) ∈ ℱ (Renaming P f g)› ‹(t_Q, X_Q) ∈ ℱ (Renaming Q f g)›
        ‹s setinterleaves ((t_P, t_Q), range tick ∪ ev ` f ` S)›
        ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` f ` S) ∪ X_P ∩ X_Q›
      by (simp add: F_Sync D_Sync) blast
    thus ‹(s, X) ∈ ℱ (?lhs P Q)›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 (?rhs P Q) ⟹ (s, X) ∈ ℱ (?lhs P Q)› by blast
    next
      fix t_P t_Q X_P X_Q
      assume * : ‹(t_P, X_P) ∈ ℱ (Renaming P f g)› ‹(t_Q, X_Q) ∈ ℱ (Renaming Q f g)›
        ‹s setinterleaves ((t_P, t_Q), range tick ∪ ev ` f ` S)›
        ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` f ` S) ∪ X_P ∩ X_Q›
      from "*"(1, 2) consider ‹t_P ∈ 𝒟 (Renaming P f g) ∨ t_Q ∈ 𝒟 (Renaming Q f g)›
        | t_P1 t_Q1 where ‹(t_P1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X_P) ∈ ℱ P› ‹t_P = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t_P1›
          ‹(t_Q1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X_Q) ∈ ℱ Q› ‹t_Q = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t_Q1›
        by (simp add: F_Renaming D_Renaming) blast
      thus ‹(s, X) ∈ ℱ (?lhs P Q)›
      proof cases
        assume ‹t_P ∈ 𝒟 (Renaming P f g) ∨ t_Q ∈ 𝒟 (Renaming Q f g)›
        hence ‹s ∈ 𝒟 (?rhs P Q)›
          apply (simp add: D_Sync)
          using "*"(1, 2, 3) F_T setinterleaving_sym front_tickFree_Nil by blast
        with same_div D_F show ‹(s, X) ∈ ℱ (?lhs P Q)› by blast
      next
        fix t_P1 t_Q1
        assume ** : ‹(t_P1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X_P) ∈ ℱ P› ‹t_P = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t_P1›
          ‹(t_Q1, map_event⇩p⇩t⇩i⇩c⇩k f g -` X_Q) ∈ ℱ Q› ‹t_Q = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t_Q1›
        from "**"(2, 4) have *** : ‹t_P1 = map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) t_P›
          ‹t_Q1 = map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) t_Q›
          by (simp_all add: inj_map_event⇩p⇩t⇩i⇩c⇩k)
        have **** : ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) (map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) s) = s›
          by (metis bij_betw_imp_surj bij_map_event⇩p⇩t⇩i⇩c⇩k list.map_comp list.map_id surj_iff)
        from bij_map_setinterleaving_iff_setinterleaving
          [of ‹inv (map_event⇩p⇩t⇩i⇩c⇩k f g)› s t_P ‹range tick ∪ ev ` f ` S› t_Q, simplified "*"(3)]
        have ‹map (inv (map_event⇩p⇩t⇩i⇩c⇩k f g)) s setinterleaves ((t_P1, t_Q1), range tick ∪ ev ` S)›
          by (metis "***" bij_betw_def bij_map_event⇩p⇩t⇩i⇩c⇩k inj_imp_bij_betw_inv sets_S_eq)
        moreover have ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X = (map_event⇩p⇩t⇩i⇩c⇩k f g -` X_P ∪ map_event⇩p⇩t⇩i⇩c⇩k f g -` X_Q) ∩ (range tick ∪ ev ` S) ∪ 
                      map_event⇩p⇩t⇩i⇩c⇩k f g -` X_P ∩ map_event⇩p⇩t⇩i⇩c⇩k f g -` X_Q›
          by (metis (no_types, lifting) "*"(4) inj_map_event⇩p⇩t⇩i⇩c⇩k inj_vimage_image_eq sets_S_eq vimage_Int vimage_Un)
        ultimately show ‹(s, X) ∈ ℱ (?lhs P Q)›
          by (simp add: F_Renaming F_Sync) (metis "**"(1, 3) "****")
      qed
    qed
  qed
qed

(*<*)
end 
(*>*)