(*<*)
―‹ ********************************************************************
 * Project : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version : 2.0
 *
 * Author : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 * (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file : Algebraic laws
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * 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 ‹ Powerful Laws of CSP ›

(*<*)
theory CSP_Laws                                               
  imports Basic_CSP_Laws Step_CSP_Laws_Extended
begin
  (*>*)

subsection‹ Laws for Mndetprefix and Sync›

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


lemmas Mndetprefix_Sync_Det_distr_F = Mndetprefix_Sync_Det_distr_FD[THEN leFD_imp_leF]
  and Mndetprefix_Sync_Det_distr_D = Mndetprefix_Sync_Det_distr_FD[THEN leFD_imp_leD]

lemmas Mndetprefix_Sync_Det_distr_T = Mndetprefix_Sync_Det_distr_F[THEN leF_imp_leT]

lemma Mndetprefix_Sync_Det_distr_DT :
  ‹[A ≠ {}; B ≠ {}; A ∩ C = {}; B ∩ C = {}] ==>
 (⊓ a ∈ A → (P a [ C ] (⊓ b ∈ B → Q b))) ◻
 (⊓ b ∈ B → ((⊓ a ∈ A → P a) [ C ] Q b))
 ⊑_DT (⊓ a ∈ A → P a) [ C ] (⊓ b ∈ B → Q b)›
  by (simp add: Mndetprefix_Sync_Det_distr_D Mndetprefix_Sync_Det_distr_T leD_leT_imp_leDT)


subsection ‹Hiding Operator Laws›

theorem Hiding_Hiding_less_eq_process_Hiding_Un : ‹P \ A \ B ⊑_FD P \ (A ∪ B)›
proof (rule failure_divergence_refine_optimizedI)
  fix s assume ‹s ∈ D (P \ (A ∪ B))›
  then obtain t u
    where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` (A ∪ B)) @ u›
      ‹t ∈ D P ∨ (∃f. isInfHiddenRun f P (A ∪ B) ∧ t ∈ range f)›
    unfolding D_Hiding by blast
  have ** : ‹trace_hide t (ev ` (A ∪ B)) = trace_hide (trace_hide t (ev ` A)) (ev ` B)›
    using trace_hide_ev_union by blast
  from "*"(4) show ‹s ∈ D (P \ A \ B)›
  proof (elim disjE exE)
    assume ‹t ∈ D P›
    with mem_D_imp_mem_D_Hiding have ‹trace_hide t (ev ` A) ∈ D (P \ A)› by blast
    thus ‹s ∈ D (P \ A \ B)›
      by (subst D_Hiding) (use"*"(1, 2, 3) "**" Hiding_tickFree in blast)
  next
    fix f assume ** : ‹isInfHiddenRun f P (A ∪ B) ∧ t ∈ range f›
    hence ‹strict_mono f› by simp
    define ff where ‹ff i ≡ take (i + length (f 0)) (f i)› for i
    have *** : ‹isInfHiddenRun ff P (A ∪ B) ∧ t ∈ range ff›
    proof (intro conjI allI)
      show ‹strict_mono ff›
      proof (unfold strict_mono_Suc_iff, rule allI, unfold ff_def)
        fix i nat
        from length_strict_mono[of f ‹Suc i›, OF ‹strict_mono f›]
        have $ : ‹take (i + length (f 0)) (f (Suc i)) < take ((Suc i) + length (f 0)) (f (Suc i))›
          by (simp add: take_Suc_conv_app_nth)
        from ‹strict_mono f›[THEN strict_monoD, of i ‹Suc i›, simplified] 
        obtain t where ‹f (Suc i) = f i @ t› by (meson strict_prefixE')
        with length_strict_mono[of f i, OF ‹strict_mono f›]
        have ‹take (i + length (f 0)) (f i) = take (i + length (f 0)) (f (Suc i))› by simp
        with "$" show ‹take (i + length (f 0)) (f i) < take (Suc i + length (f 0)) (f (Suc i))› by simp
      qed
    next
      show ‹ff i ∈ T P› for i
        by (unfold ff_def) (metis "**" prefixI append_take_drop_id is_processT3_TR)
    next
      show ‹trace_hide (ff i) (ev ` (A ∪ B)) = trace_hide (ff 0) (ev ` (A ∪ B))› for i
      proof (rule order_antisym)
        have ‹f 0 ≤ f i› by (simp add: "**" strict_mono_less_eq)
        hence ‹f 0 ≤ take (i + length (f 0)) (f i)›
          by (metis prefixE Prefix_Order.prefixI le_add2 take_all_iff take_append)
        from mono_trace_hide[OF this]
        show ‹trace_hide (ff 0) (ev ` (A ∪ B)) ≤ trace_hide (ff i) (ev ` (A ∪ B))›
          by (unfold ff_def) (metis le_add2 take_all_iff)
      next
        have ‹take (i + length (f 0)) (f i) ≤ f i›
          by (metis prefixI append_take_drop_id)
        from mono_trace_hide[OF this]
        show ‹trace_hide (ff i) (ev ` (A ∪ B)) ≤ trace_hide (ff 0) (ev ` (A ∪ B))›
          by (unfold ff_def) (metis "**" le_add2 take_all_iff)
      qed
    next
      from "**" obtain i where ‹t = f i› by blast
      moreover have ‹f 0 ≤ f i› by (simp add: "**" strict_mono_less_eq)
      ultimately have ‹t = ff (max i (length t - length (f 0)))›
        by (simp add: ff_def max_def le_length_mono)
          (metis "**" prefixE append_eq_conv_conj strict_mono_less_eq)
      thus ‹t ∈ range ff› by blast
    qed

    show ‹s ∈ D (P \ A \ B)›
    proof (cases ‹∃m. ∀i>m. last (ff i) ∈ ev ` A›)
      assume ‹∃m. ∀i>m. last (ff i) ∈ ev ` A›
      then obtain m where $ : ‹m < i ==> last (ff i) ∈ ev ` A› for i by blast
      hence ‹tF (ff m)›
        by (metis "***" strict_prefixE' append_T_imp_tickFree list.distinct(1) strict_mono_Suc_iff)
      have $$ : ‹∃t. ff (i + m) = ff m @ t ∧ set t ⊆ ev ` A› for i
      proof (induct i)
        show ‹∃t. ff (0 + m) = ff m @ t ∧ set t ⊆ ev ` A› by simp
      next
        fix i assume ‹∃t. ff (i + m) = ff m @ t ∧ set t ⊆ ev ` A›
        then obtain t where ‹ff (i + m) = ff m @ t› ‹set t ⊆ ev ` A› by blast
        obtain r where ‹ff (Suc i + m) = ff (i + m) @ r›
          by (metis "***" strict_prefixE' add_Suc strict_mono_Suc_iff)
        moreover have ‹length (ff (Suc i + m)) = Suc (length (ff (i + m)))›
          by (simp add: ff_def) (metis "**" add_Suc length_strict_mono min_absorb2)
        ultimately have ‹length r = 1› by (metis Suc_eq_plus1 add_left_cancel length_append)
        with ‹ff (Suc i + m) = ff (i + m) @ r›
        have ‹ff (Suc i + m) = ff (i + m) @ [last (ff (Suc i + m))]› by (cases r) simp_all
        with ‹ff (i + m) = ff m @ t›
        have ‹ff (Suc i + m) = ff m @ t @ [last (ff (Suc i + m))]› by simp
        moreover have ‹last (ff (Suc i + m)) ∈ ev ` A› by (simp add: "$")
        ultimately show ‹∃t. ff (Suc i + m) = ff m @ t ∧ set t ⊆ ev ` A›
          by (intro exI[of _ ‹t @ [last (ff (Suc i + m))]›]) (simp add: ‹set t ⊆ ev ` A›)
      qed
      then obtain fff where $$$$ : ‹ff (i + m) = ff m @ fff i› ‹set (fff i) ⊆ ev ` A› for i by metis
      show ‹s ∈ D (P \ A \ B)›
        apply (simp add: D_Hiding)
        apply (rule exI[of _ ‹trace_hide (ff m) (ev ` A)›], rule exI[of _ u], intro conjI)
        subgoal by (fact ‹ftF u›)
        subgoal using Hiding_tickFree ‹tF (ff m)› by blast
        subgoal by (metis (no_types) "*"(3) "***" rangeE trace_hide_ev_union)
        apply (rule disjI1)
        apply (rule exI[of _ ‹ff m›], rule exI[of _ ‹[]›], simp add: ‹tF (ff m)›)
        apply (rule disjI2)
        apply (rule exI[of _ ‹λi. ff (i + m)›], intro conjI)
        subgoal by (metis (mono_tags, lifting) "***" add_Suc strict_mono_Suc_iff)
        subgoal using "***" by blast
        subgoal using "$$$$" by (simp add: subset_iff)
        by (metis (mono_tags) add_0 rangeI)
    next
      assume ‹∄m. ∀i>m. last (ff i) ∈ ev ` A›
      { fix i :: nat assume ‹0 < i›
        from "***" obtain t where ‹ff i = ff 0 @ t› ‹set t ⊆ ev ` (A ∪ B)›
          unfolding isInfHiddenRun_1 by blast
        with ‹0 < i› have ‹last (ff i) ∈ ev ` (A ∪ B)›
          by (cases t) (auto simp add: "***" strict_mono_eq)
      }
      with ‹∄m. ∀i>m. last (ff i) ∈ ev ` A› have $ : ‹∀i. ∃j>i. last(ff j) ∈ ev ` B - ev ` A›
        by (metis Un_Diff_cancel2 Un_iff gr0I image_Un not_less0)
      define fff where ‹fff = rec_nat t (λi t. ff (SOME j. t < ff j ∧ last (ff j) ∈ ev ` B - ev ` A))›
      hence ‹fff i ∈ range ff› for i
        unfolding fff_def
        by (metis (mono_tags, lifting) "***" gr0_conv_Suc nat.rec(2)
            old.nat.simps(6) rangeI zero_less_iff_neq_zero)
      have $$$ : ‹strict_mono (λi. trace_hide (fff i) (ev ` A))›
      proof (unfold strict_mono_Suc_iff, rule allI)
        fix i
        have "£" : ‹fff (Suc i) = ff (SOME j. fff i < ff j ∧ last (ff j) ∈ ev ` B - ev ` A)›
          by (simp add: fff_def)
        from ‹∧i. fff i ∈ range ff› obtain j where ‹fff i = ff j› by blast
        hence ‹∃j. fff i < ff j ∧ last (ff j) ∈ ev ` B - ev ` A› by (metis "$" "***" monotoneD)
        hence "££" : ‹fff i < fff (Suc i) ∧ last (fff (Suc i)) ∉ ev ` A›
          by (metis (no_types, lifting) Diff_iff "£" someI_ex)
        then obtain r where ‹fff (Suc i) = fff i @ r› ‹last r ∉ ev ` A›
          by (metis append_self_conv last_append less_eq_list_def prefix_def less_list_def)
        thus ‹trace_hide (fff i) (ev ` A) < trace_hide (fff (Suc i)) (ev ` A)›
          by (metis (mono_tags, lifting) prefixI "££" empty_filter_conv
              filter_append last_in_set nless_le self_append_conv)
      qed
      show ‹s ∈ D (P \ A \ B)›
        apply (simp add: D_Hiding)
        apply (rule exI[of _ ‹trace_hide t (ev ` A)›], rule exI[of _ u], intro conjI)
        subgoal by (fact ‹ftF u›)
        subgoal using Hiding_tickFree ‹tF t› by blast
        subgoal by (simp add: "*"(3))
        apply (rule disjI2)
        apply (rule exI[of _ ‹λi. trace_hide (fff i) (ev ` A)›], intro conjI)
        subgoal by (fact "$$$")
        subgoal by (metis "***" ‹∧i. fff i ∈ range ff› mem_T_imp_mem_T_Hiding rangeE)
        subgoal by (metis (no_types) "***" ‹∧i. fff i ∈ range ff› rangeE trace_hide_ev_union)
        by (metis (mono_tags, lifting) fff_def old.nat.simps(6) rangeI)
    qed
  qed
next
  assume subset_div : ‹D (P \ (A ∪ B)) ⊆ D (P \ A \ B)›
  fix s X assume ‹(s, X) ∈ F (P \ (A ∪ B))›
  then consider ‹s ∈ D (P \ (A ∪ B))›
    | t where ‹s = trace_hide t (ev ` (A ∪ B))› ‹(t, X ∪ ev ` (A ∪ B)) ∈ F P›
    unfolding F_Hiding D_Hiding by blast
  thus ‹(s, X) ∈ F (P \ A \ B)›
  proof cases
    from subset_div D_F show ‹s ∈ D (P \ (A ∪ B)) ==> (s, X) ∈ F (P \ A \ B)› by blast
  next
    fix t assume ‹s = trace_hide t (ev ` (A ∪ B))› ‹(t, X ∪ ev ` (A ∪ B)) ∈ F P›
    hence * : ‹s = trace_hide (trace_hide t (ev ` A)) (ev ` B)›
      ‹(t, X ∪ ev ` B ∪ ev ` A) ∈ F P›
      by (simp_all add: image_Un sup_commute sup_left_commute)
    show ‹(s, X) ∈ F (P \ A \ B)›
      by (simp add: F_Hiding) (use "*" in blast)
  qed
qed


theorem Hiding_Un : ‹P \ (A ∪ B) = P \ A \ B›
  if ‹finite A› for P :: ‹('a, 'r) process_ptick›
proof (rule order_antisym)
  show ‹P \ (A ∪ B) ≤ P \ A \ B›
  proof (rule failure_divergence_refine_optimizedI)
    fix s assume ‹s ∈ D (P \ A \ B)›
    then obtain t u
      where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` B) @ u›
        ‹t ∈ D (P \ A) ∨ (∃x. isInfHidden_seqRun_strong x (P \ A) B t)›
      by (elim D_Hiding_seqRunE)
    from "*"(4) show ‹s ∈ D (P \ (A ∪ B))›
    proof (elim disjE exE)
      assume ‹t ∈ D (P \ A)›
      then obtain t' u'
        where ** : ‹ftF u'› ‹tF t'› ‹t = trace_hide t' (ev ` A) @ u'›
          ‹t' ∈ D P ∨ (∃x. isInfHidden_seqRun_strong x P A t')›
        by (elim D_Hiding_seqRunE)
      from "*"(1, 2) "**"(3) have *** : ‹ftF (trace_hide u' (ev ` B) @ u)›
        using Hiding_tickFree front_tickFree_append tickFree_append_iff by blast
      show ‹s ∈ D (P \ (A ∪ B))›
        apply (unfold D_Hiding_seqRun, clarify)
        apply (rule exI[of _ t'], rule exI[of _ ‹trace_hide u' (ev ` B) @ u›])
        apply (intro conjI)
        subgoal by (fact "***")
        subgoal by (fact "**"(2))
        subgoal by (simp add: "*"(3) "**"(3))
        by (metis "**"(4) Un_iff image_Un)
    next
      fix x assume ** : ‹isInfHidden_seqRun_strong x (P \ A) B t›
      have trH_x : ‹trace_hide (seqRun t x i) (ev ` B) = trace_hide t (ev ` B)› for i
        using "**" trace_hide_seqRun_eq_iff by blast
      from "**" have ‹∀i. seqRun t x i ∈ {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ F P}›
        unfolding T_Hiding D_Hiding by blast
      with F_T have ‹∀i. ∃w. seqRun t x i = trace_hide w (ev ` A) ∧ w ∈ T P› by blast
      then obtain f where *** : ‹seqRun t x i = trace_hide (f i) (ev ` A)› ‹f i ∈ T P› for i by metis
      have ‹inj f› by (rule injI) (metis "***"(1) seqRun_eq_iff)
      with finite_imageD have ‹infinite (range f)› by blast
      have $ : ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A› if ‹t' ∈ range f› for i t'
      proof -
        from ‹t' ∈ range f› obtain j where ‹t' = f j› ..
        hence "£" : ‹seqRun t x j = trace_hide t' (ev ` A)› ‹t' ∈ T P› by (simp_all add: "***")
        consider ‹i ≤ j› | ‹j ≤ i› by linarith
        thus ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A›
        proof cases
          assume ‹j ≤ i›
          hence ‹seqRun t x j ≤ seqRun t x i› by simp
          hence ‹set (seqRun t x j) ⊆ set (seqRun t x i)›
            by (metis prefixE Un_iff set_append subsetI)
          moreover have ‹set (take i t') ⊆ set (seqRun t x j) ∪ ev ` A›
            by (rule subsetI, drule in_set_takeD) (simp add: "£"(1))
          ultimately show ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A› by blast
        next
          assume ‹i ≤ j›
          hence ‹seqRun t x i ≤ seqRun t x j› by simp
          hence ‹take i (seqRun t x j) ≤ seqRun t x i› by simp
          have ‹seqRun t x j = trace_hide (take i t') (ev ` A) @ trace_hide (drop i t') (ev ` A)›
            by (metis "£"(1) append_take_drop_id filter_append)
          moreover have ‹length (trace_hide (take i t') (ev ` A)) ≤ i›
            by (metis length_filter_le length_take min.bounded_iff)
          ultimately have ‹trace_hide (take i t') (ev ` A) ≤ take i (seqRun t x j)› by simp
          with ‹take i (seqRun t x j) ≤ seqRun t x i› obtain t''
            where ‹seqRun t x i = trace_hide (take i t') (ev ` A) @ t''›
            by (meson prefixE dual_order.trans)
          thus ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A› by (simp add: subsetI)
        qed
      qed
      have ‹finite {take i w |w. w ∈ range f}› for i
      proof (induct i)
        show ‹finite {take 0 w |w. w ∈ range f}› by simp
      next
        fix i assume hyp : ‹finite {take i w |w. w ∈ range f}›
        show ‹finite {take (Suc i) w |w. w ∈ range f}›
        proof (rule finite_subset)
          show ‹ {take (Suc i) w |w. w ∈ range f}
 ⊆ {take i w |w. w ∈ range f}
 ∪ (∪e∈set (seqRun t x (Suc i)) ∪ ev ` A. {take i w @ [e] |w. w ∈ range f})›
            (is ‹?lhs ⊆ {take i w |w. w ∈ range f} ∪ (∪e∈?S1. ?S2 e)›)
          proof (intro subsetI)
            fix t' assume ‹t' ∈ ?lhs›
            then obtain w where "£" : ‹t' = take (Suc i) w› ‹w ∈ range f› by blast
            show ‹t' ∈ {take i w |w. w ∈ range f} ∪ (∪e∈?S1. ?S2 e)›
            proof (cases ‹i < length t'›)
              assume ‹i < length t'›
              with "£"(1) take_Suc_conv_app_nth
              have ‹take (Suc i) t' = take i w @ [t' ! i]› by auto
              moreover from "£" "$" ‹i < length t'› nth_mem have ‹t' ! i ∈ ?S1› by blast
              ultimately have ‹t' ∈ (∪e∈?S1. ?S2 e)›
                by (intro UN_I[of ‹t' ! i›], simp_all)
                  (metis "£" less_not_refl min.absorb2 not_le_imp_less take_take)
              thus ‹t' ∈ {take i w |w. w ∈ range f} ∪ (∪e∈?S1. ?S2 e)› by simp
            next
              assume ‹¬ i < length t'›
              hence ‹take (Suc i) t' = take i t'› by simp
              with "£" show ‹t' ∈ {take i w |w. w ∈ range f} ∪ (∪e∈?S1. ?S2 e)› by auto
            qed
          qed
        next
          show ‹finite ({take i w |w. w ∈ range f} ∪
 (∪e∈set (seqRun t x (Suc i)) ∪ ev ` A.
 {take i w @ [e] |w. w ∈ range f}))›
          proof (rule finite_UnI)
            show ‹finite {take i w |w. w ∈ range f}› by (fact hyp)
          next
            show ‹finite (∪e∈set (seqRun t x (Suc i)) ∪ ev ` A. {take i w @ [e] |w. w ∈ range f})›
            proof (rule finite_UN_I)
              show ‹finite (set (seqRun t x (Suc i)) ∪ ev ` A)›
                by (simp add: ‹finite A›) ―‹Here we use that term‹A› is const‹finite›.›
            next
              fix e assume ‹e ∈ set (seqRun t x (Suc i)) ∪ ev ` A›
              have ‹ {take i w @ [e] |w. w ∈ range f}
 = (λt'. t' @ [e]) ` {take i w |w. w ∈ range f}› by auto
              also have ‹finite …› by (rule finite_imageI) (fact hyp)
              finally show ‹finite {take i w @ [e] |w. w ∈ range f}› .
            qed
          qed
        qed
      qed
      also have ‹{take i w |w. w ∈ range f} = {w. ∃t'∈range f. w = take i t'}› for i by auto
      finally have ‹∀i. finite {w. ∃t'∈range f. w = take i t'}› ..
      from KoenigLemma[OF ‹infinite (range f)› this]
      obtain ff :: ‹nat → ('a, 'r) trace<sub>ptick</sub>›
        where $$ : ‹strict_mono ff› ‹range ff ⊆ {t. ∃t'∈range f. t ≤ t'}› by blast
      from "$$"(2) have $$$ : ‹∃t'. ff (Suc j) ≤ t' ∧ t' ∈ range f› for j by blast
      hence ‹ftF (ff (Suc j))› for j
        by (metis "***"(2) imageE is_processT2_TR is_processT3_TR)
      hence ‹tF (ff j)› for j
        using strict_monoD[OF "$$"(1), of j ‹Suc j›, simplified]
        by (metis strict_prefixE' front_tickFree_append_iff list.distinct(1))
      from "$$"(2) "***"(2) have ‹ff (j + i) ∈ T P› for i j
        by (simp add: subset_iff) (meson is_processT3_TR rangeI)
      have $$$$ : ‹∃w. trace_hide (ff i) (ev ` A) ≤ t @ w› for i
      proof -
        from "$$"(2) obtain j where ‹ff i ≤ f j› by auto
        moreover from "**" isInfHiddenRun_1 have ‹∃w. seqRun t x j = t @ w›
          by (simp add: seqRun_def) 
        ultimately show ‹∃w. trace_hide (ff i) (ev ` A) ≤ t @ w›
          by (metis "***"(1) mono_trace_hide)
      qed
      have ‹∃i. t ≤ trace_hide (ff i) (ev ` A)›
      proof (rule ccontr)
        define fff where ‹fff i ≡ trace_hide (ff i) (ev ` A)› for i
        assume assm : ‹∄i. t ≤ fff i›
        moreover from "$$$$" have ‹∀i. ∃w. fff i ≤ t @ w› unfolding fff_def ..
        ultimately have assm_bis : ‹∀i. fff i ≤ t›
          by (metis prefixI le_same_imp_eq_or_less order.order_iff_strict)
        have ‹mono fff›
          by (rule monoI, simp add: fff_def)
            (metis "$$"(1) prefixE prefixI filter_append strict_mono_less_eq)
        from mono_constant[OF this assm_bis]
        obtain j where ‹j ≤ i ==> fff i = fff j› for i by blast
        have ‹fff j ∈ D (P \ A)›
          apply (unfold D_Hiding, clarify)
          apply (rule exI[of _ ‹ff j›], rule exI[of _ ‹[]›])
          apply (simp add: fff_def ‹tF (ff j)›)
          apply (rule disjI2)
          apply (rule exI[of _ ‹λi. ff (j + i)›])
          apply (intro conjI)
          subgoal by (simp add: "$$"(1) strict_monoI strict_mono_less)
          subgoal by (simp add: ‹∧i. ff (j + i) ∈ T P›)
          subgoal by (metis ‹∧i. j ≤ i ==> fff i = fff j› fff_def le_add1)
          subgoal by (metis Nat.add_0_right rangeI) .
        thus False
          by (metis (no_types) "**" prefixE T_imp_front_tickFree append.right_neutral assm_bis
              front_tickFree_append_iff is_processT3_TR is_processT7 t_le_seqRun)
      qed
      then obtain j where ‹t ≤ trace_hide (ff j) (ev ` A)› ..
      have "£" : ‹s = trace_hide (ff j) (ev ` (A ∪ B)) @ u›
      proof (unfold "*"(3), rule arg_cong[where f = ‹λx. x @ _›])
        from "$$"(1) "$$$" obtain l where ‹ff j ≤ f l›
          by (metis dual_order.trans order_less_imp_le rangeE strict_mono_Suc_iff)
        from mono_trace_hide[OF this] have ‹trace_hide (ff j) (ev ` A) ≤ seqRun t x l›
          unfolding "***"(1) by presburger
        with mono_trace_hide[OF this] mono_trace_hide[OF ‹t ≤ trace_hide (ff j) (ev ` A)›]
        show ‹trace_hide t (ev ` B) = trace_hide (ff j) (ev ` (A ∪ B))›
          by (metis trH_x dual_order.eq_iff trace_hide_ev_union)
      qed
      have "££" : ‹trace_hide (ff (j + i)) (ev ` (A ∪ B)) = trace_hide (ff (j + 0)) (ev ` (A ∪ B))› for i
      proof -
        from "$$"(1) "$$$" obtain l where ‹ff (j + i) ≤ f l›
          by (metis dual_order.trans order_less_imp_le rangeE strict_mono_Suc_iff)
        from mono_trace_hide[OF this] have ‹trace_hide (ff (j + i)) (ev ` A) ≤ seqRun t x l›
          unfolding "***"(1) by presburger
        from mono_trace_hide[OF this, of B]
          mono_trace_hide[THEN mono_trace_hide, of _ _ B A,
            OF ‹strict_mono ff›[THEN strict_mono_mono, THEN monoD, of j ‹j + i›, simplified]]
          mono_trace_hide[OF ‹t ≤ trace_hide (ff j) (ev ` A)›, of B]
        show ‹trace_hide (ff (j + i)) (ev ` (A ∪ B)) =
 trace_hide (ff (j + 0)) (ev ` (A ∪ B))› by (simp add: trH_x)
      qed
      show ‹s ∈ D (P \ (A ∪ B))›
        apply (unfold D_Hiding, clarify)
        apply (rule exI[of _ ‹ff j›], rule exI[of _ u])
        apply (intro conjI)
        subgoal by (fact ‹ftF u›)
        subgoal by (fact ‹tF (ff j)›)
        subgoal by (fact "£")
        apply (rule disjI2)
        apply (rule exI[of _ ‹λi. ff (j + i)›])
        apply (intro conjI)
        subgoal by (simp add: "$$"(1) strict_monoI strict_mono_less)
        subgoal by (simp add: ‹∧i. ff (j + i) ∈ T P›)
        subgoal by (use "££" in blast)
        by (metis Nat.add_0_right rangeI)
    qed
  next
    assume subset_div : ‹D (P \ A \ B) ⊆ D (P \ (A ∪ B))›
    fix s X assume ‹(s, X) ∈ F (P \ A \ B)›
    from this[simplified F_Hiding[of ‹P \ A› B]] D_Hiding[of ‹P \ A› B]
    consider ‹s ∈ D (P \ A \ B)›
      | t where ‹s = trace_hide t (ev ` B)› ‹(t, X ∪ ev ` B) ∈ F (P \ A)› by blast
    thus ‹(s, X) ∈ F (P \ (A ∪ B))›
    proof cases
      from subset_div D_F show ‹s ∈ D (P \ A \ B) ==> (s, X) ∈ F (P \ (A ∪ B))› by blast
    next
      fix t assume * : ‹s = trace_hide t (ev ` B)› ‹(t, X ∪ ev ` B) ∈ F (P \ A)›
      from "*"(2) consider ‹t ∈ D (P \ A)›
        | u where ‹t = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` B ∪ ev ` A) ∈ F P›
        unfolding F_Hiding D_Hiding by blast
      thus ‹(s, X) ∈ F (P \ (A ∪ B))›
      proof cases
        assume ‹t ∈ D (P \ A)›
        with "*"(1) mem_D_imp_mem_D_Hiding have ‹s ∈ D (P \ A \ B)› by fast
        with subset_div D_F show ‹(s, X) ∈ F (P \ (A ∪ B))› by blast
      next
        fix u assume ** : ‹t = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` B ∪ ev ` A) ∈ F P›
        from "*"(1) "**"(1) have ‹s = trace_hide u (ev ` (A ∪ B))› by simp
        moreover from "**"(2) have ‹(u, X ∪ ev ` (A ∪ B)) ∈ F P›
          by (simp add: image_Un sup_commute sup_left_commute)
        ultimately show ‹(s, X) ∈ F (P \ (A ∪ B))› unfolding F_Hiding by blast
      qed
    qed
  qed
next
  show ‹P \ A \ B ≤ P \ (A ∪ B)› by (fact Hiding_Hiding_less_eq_process_Hiding_Un)
qed




subsection‹ Sync Operator Laws ›  

subsubsection‹ Preliminaries ›

lemma tickFree_isInfHiddenRun : ‹tF s›
  if ‹isInfHiddenRun f P A› and ‹s ∈ range f›
proof -
  from ‹s ∈ range f› obtain i where ‹s = f i› ..
  moreover have ‹f i < f (Suc i)› by (meson ‹isInfHiddenRun f P A› strict_mono_Suc_iff)
  ultimately obtain t where ‹t ≠ []› ‹f (Suc i) = s @ t› by (meson strict_prefixE' list.discI)
  moreover from ‹isInfHiddenRun f P A› is_processT2_TR
  have ‹ftF (f (Suc i))› by blast
  ultimately show ‹tF s› by (simp add: front_tickFree_append_iff)
qed

lemma Hiding_interleave: 
  ‹r setinterleaves ((t, u), C) ==>
 (trace_hide r A) setinterleaves ((trace_hide t A, trace_hide u A), C)›
  (* The hypothesis \<open>A \<inter> C = {}\<close> was useless, see if we can obtain more powerful results *)
proof (induct ‹(t, C, u)› arbitrary: r t u rule: setinterleaving.induct)
  case 1 thus ?case by simp
next
  case (2 x t) thus ?case by auto
next
  case (3 y u) thus ?case by auto
next
  case (4 x t y u)
  thus ?case 
    by (simp split: if_splits)
      (safe, simp_all, (use SyncSingleHeadAdd setinterleaving_sym in blast)+)
qed

lemma non_Sync_interleaving: 
  ‹(set t ∪ set u) ∩ C = {} ==> setinterleaving (t, C, u) ≠ {}› (* FINALLY NON-USED*)
  by (induct ‹(t, C, u)› arbitrary: t u rule: setinterleaving.induct) simp_all


lemma interleave_Hiding: 
  ‹s setinterleaves ((trace_hide t A, trace_hide u A), C)
 ==> ∃r. s = trace_hide r A ∧ r setinterleaves ((t, u), C)› if ‹A ∩ C = {}›
proof (induct ‹(t, C, u)› arbitrary: t u s rule: setinterleaving.induct)
  case 1
  thus ?case by simp
next
  case (2 y u)
  from "2.prems" ‹A ∩ C = {}› show ?case
    by (simp add: disjoint_iff split: if_split_asm)
      (metis "2.hyps" "2.prems" emptyLeftProperty filter.simps(1))+
next
  case (3 x t)
  from "3.prems" ‹A ∩ C = {}› show ?case
    by (simp add: disjoint_iff split: if_split_asm)
      (metis "3.hyps" "3.prems" emptyRightProperty filter.simps(1))+
next
  case (4 x t y u)
  from "4.prems" ‹A ∩ C = {}› show ?case
    apply (cases ‹x = y›, simp_all add: disjoint_iff split: if_split_asm)
    subgoal using "4.hyps"(1) by force
    subgoal by (metis (no_types, lifting) "4.hyps"(3) "4.hyps"(4) filter.simps(2))
    subgoal by (metis (no_types, lifting) "4.hyps"(3) filter.simps(2))
    subgoal using "4.hyps"(2) by force
    subgoal by (metis (no_types, lifting) "4.hyps"(3) "4.hyps"(4) filter.simps(2)) 
    subgoal using "4.hyps"(5) by force 
    subgoal by (metis (no_types, lifting) "4.hyps"(2) "4.hyps"(4) filter.simps(2))
    subgoal by (metis (no_types, lifting) "4.hyps"(3) "4.hyps"(5) filter.simps(2))
    subgoal by (metis (no_types, lifting) "4.hyps"(4) filter.simps(2))
    done
qed


lemma le_trace_hide : ‹u ≤ trace_hide t S ==> ∃u'. u = trace_hide u' S ∧ u' ≤ t›
proof (induct t arbitrary: u)
  show ‹u ≤ trace_hide [] S ==> ∃u'. u = trace_hide u' S ∧ u' ≤ []› for u by simp
next
  fix a t u assume prem: ‹u ≤ trace_hide (a # t) S›
  assume hyp : ‹u ≤ trace_hide t S ==> ∃u'. u = trace_hide u' S ∧ u' ≤ t› for u
  from prem consider ‹u = []› | ‹a ∈ S› ‹u ≤ trace_hide t S›
    | v where ‹a ∉ S› ‹u = a # v› ‹v ≤ trace_hide t S›
    by (cases u) (simp_all split: if_split_asm)
  thus ‹∃u'. u = trace_hide u' S ∧ u' ≤ a # t›
  proof cases
    show ‹u = [] ==> ∃u'. u = trace_hide u' S ∧ u' ≤ a # t›
      by (metis filter.simps(1) nil_le)
  next
    assume ‹a ∈ S› ‹u ≤ trace_hide t S›
    from hyp[OF ‹u ≤ trace_hide t S›] obtain u' where ‹u = trace_hide u' S ∧ u' ≤ t› ..
    with ‹a ∈ S› have ‹u = trace_hide (a # u') S ∧ a # u' ≤ a # t› by simp
    thus ‹∃u'. u = trace_hide u' S ∧ u' ≤ a # t› ..
  next
    fix v assume ‹a ∉ S› ‹u = a # v› ‹v ≤ trace_hide t S›
    from hyp[OF ‹v ≤ trace_hide t S›] obtain v' where ‹v = trace_hide v' S ∧ v' ≤ t› ..
    with ‹a ∉ S› ‹u = a # v› have ‹u = trace_hide (a # v') S ∧ a # v' ≤ a # t› by simp
    thus ‹∃u'. u = trace_hide u' S ∧ u' ≤ a # t› ..
  qed
qed



lemma append_interleave :
  ‹s1 setinterleaves ((t1, u1), S) ==> s2 setinterleaves ((t2, u2), S) ==>
 (s1 @ s2) setinterleaves ((t1 @ t2, u1 @ u2), S)›
proof (induct ‹(t1, S, u1)› arbitrary: s1 t1 u1 rule: setinterleaving.induct)
  case 1 thus ?case by simp
next
  case (2 y u1)
  thus ?case by (auto split: if_split_asm)
      (use SyncSingleHeadAdd setinterleaving_sym in blast)
next
  case (3 x t1)
  thus ?case by (auto split: if_split_asm) (blast intro: SyncSingleHeadAdd)
next
  case (4 x t2 y u2)
  thus ?case by auto
qed


subsubsection ‹The Theorem: Sync and Hiding›

theorem Hiding_Sync : ‹(P [S] Q) \ A = (P \ A) [S] (Q \ A)›
  if ‹finite A› and ‹A ∩ S = {}› for P Q :: ‹('a, 'r) process_ptick›
    ― ‹Monster theorem!›
proof (subst Process_eq_spec_optimized, safe)
  let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
  fix s assume ‹s ∈ D (P [S] Q \ A)›
  then obtain t u
    where * : ‹ftF u› ‹tF t› ‹s = ?trH_A t @ u›
      ‹t ∈ D (P [S] Q) ∨ (∃x. isInfHidden_seqRun_strong x (P [S] Q) A t)›
    by (elim D_Hiding_seqRunE)
  from "*"(4) show ‹s ∈ D ((P \ A) [S] (Q \ A))›
  proof (elim disjE exE)
    assume ‹t ∈ D (P [S] Q)›
    then obtain t' u' r' v'
      where ** : ‹ftF v'› ‹tF r' ∨ v' = []›
        ‹t = r' @ v'› ‹r' setinterleaves ((t', u'), ?tick_S)›
        ‹t' ∈ D P ∧ u' ∈ T Q ∨ t' ∈ D Q ∧ u' ∈ T P›
      unfolding D_Sync by blast
    { fix t' u' and P Q
      assume *** : ‹r' setinterleaves ((t', u'), ?tick_S)›
        ‹t' ∈ D P› ‹u' ∈ T Q›
      have ‹?trH_A r' setinterleaves ((?trH_A t', ?trH_A u'), ?tick_S)›
        using "***"(1) Hiding_interleave by blast
      moreover from "***"(2) mem_D_imp_mem_D_Hiding have ‹?trH_A t' ∈ D (P \ A)› by blast
      moreover from "***"(3) mem_T_imp_mem_T_Hiding have ‹?trH_A u' ∈ T (Q \ A)› by blast
      ultimately have ‹s ∈ D ((P \ A) [S] (Q \ A))›
        apply (simp add: "*"(3) D_Sync)
        apply (rule exI[of _ ‹?trH_A t'›], rule exI[of _ ‹?trH_A u'›],
            rule exI[of _ ‹?trH_A r'›], rule exI[of _ ‹?trH_A v' @ u›])
        apply (simp add: "*"(3) "**"(3) Hiding_tickFree)
        using "*"(1, 2) "**"(3) Hiding_tickFree front_tickFree_append tickFree_append_iff by blast
    } note $ = this
    from "**"(5) show ‹s ∈ D ((P \ A) [S] (Q \ A))›
    proof (elim disjE conjE)
      show ‹t' ∈ D P ==> u' ∈ T Q ==> s ∈ D ((P \ A) [S] (Q \ A))›
        by (metis "$" "**"(4))
      show ‹t' ∈ D Q ==> u' ∈ T P ==> s ∈ D ((P \ A) [S] (Q \ A))›
        by (metis "$" "**"(4) Sync_commute)
    qed
  next
    fix x assume ** : ‹isInfHidden_seqRun_strong x (P [S] Q) A t›
    from "**" have *** : ‹∃t' u'. t' ∈ T P ∧ u' ∈ T Q ∧
 seqRun t x i setinterleaves ((t', u'), ?tick_S)› for i
      unfolding T_Sync D_Sync by blast
    define ftu where ‹ftu i ≡ SOME (t', u'). t' ∈ T P ∧ u' ∈ T Q ∧
 seqRun t x i setinterleaves ((t', u'), ?tick_S)› for i
    define ft fu where ‹ft ≡ λi. fst (ftu i)› and ‹fu ≡ λi. snd (ftu i)›
    have **** : ‹ft i ∈ T P› ‹fu i ∈ T Q›
      ‹seqRun t x i setinterleaves ((ft i, fu i), ?tick_S)› for i
      by (use "***"[of i] in ‹simp add: ft_def fu_def,
 cases ‹ftu i›, simp add: ftu_def,
 metis (mono_tags, lifting) case_prod_conv someI_ex›)+
    from "**" have ‹set (seqRun t x i) ⊆ set t ∪ ev ` A› for i
      by (auto simp add: seqRun_def)

    have ‹set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A› for i
      by (rule subset_trans[OF interleave_set[OF "****"(3)]])
        (fact ‹set (seqRun t x i) ⊆ set t ∪ ev ` A›)
    have ‹inj ftu›
    proof (rule injI)
      fix i j assume ‹ftu i = ftu j›
      obtain t' u' where ‹(t', u') = ftu i› by (metis surj_pair)
      with ‹ftu i = ftu j› have ‹seqRun t x i setinterleaves ((t', u'), ?tick_S)›
        ‹seqRun t x j setinterleaves ((t', u'), ?tick_S)›
        by (metis "****"(3) fst_conv ft_def fu_def snd_conv)+
      from interleave_eq_size[OF this] have ‹length (seqRun t x i) = length (seqRun t x j)› .
      thus ‹i = j› by simp
    qed
    hence ‹infinite (range ftu)› using finite_imageD by blast
    moreover have ‹range ftu ⊆ range ft × range fu›
      by (clarify, metis fst_conv ft_def fu_def rangeI snd_conv)
    ultimately have ‹infinite (range ft) ∨ infinite (range fu)›
      by (meson finite_SigmaI infinite_super)

    { fix ft fu P Q
      assume assms : ‹infinite (range ft)›
        ‹∧i. set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A›
        ‹∧i. ft i ∈ T P› ‹∧i. fu i ∈ T Q›
        ‹∧i. seqRun t x i setinterleaves ((ft i, fu i), ?tick_S)›

      have ‹finite {t. ∃t'∈range ft. t = take i t'}› for i
      proof (rule finite_subset)
        show ‹ {w. ∃t'∈range ft. w = take i t'}
 ⊆ {w. set w ⊆ set t ∪ ev ` A ∧ length w ≤ i}›
          by auto (meson Un_iff assms(2) in_set_takeD subsetD)
      next
        show ‹finite {w. set w ⊆ set t ∪ ev ` A ∧ length w ≤ i}›
          by (rule finite_lists_length_le) (simp add: ‹finite A›)
            ― ‹Here we use the assumption @{thm ‹finite A›}.›
      qed
      with assms(1) obtain ft' :: ‹nat → _›
        where $ : ‹strict_mono ft'› ‹range ft' ⊆ {w. ∃t'∈range ft. w ≤ t'}›
        using KoenigLemma by blast
      from "$"(2) assms(3) is_processT3_TR have ‹range ft' ⊆ T P› by blast
      define ft'' where ‹ft'' i ≡ ft' (i + length t)› for i
      from ‹range ft' ⊆ T P› have ‹range ft'' ⊆ T P› and ‹strict_mono ft''›
        by (auto simp add: ft''_def "$"(1) strict_monoD strict_monoI)
      have $$ : ‹?trH_A (ft'' i) = ?trH_A (ft'' 0)› for i
      proof -
        have ‹length t ≤ length (ft'' 0)›
          by (metis "$"(1) add_0 add_leD1 ft''_def length_strict_mono)
        obtain t' where ‹ft'' i = ft'' 0 @ t'›
          by (meson prefixE ‹strict_mono ft''› strict_mono_less_eq zero_order(1))
        moreover from "$"(2) obtain j where ‹ft'' i ≤ ft j› by (auto simp add: ft''_def)
        ultimately obtain t'' where ‹ft j = ft'' 0 @ t' @ t''› by (metis prefixE append.assoc)
        have ‹set (t' @ t'') ⊆ set (drop (length t) (seqRun t x j))›
        proof (rule subset_trans)
          show ‹set (t' @ t'') ⊆ set (drop (length (ft'' 0)) (seqRun t x j))›
            by (rule interleave_order, fold ‹ft j = ft'' 0 @ t' @ t''›, fact assms(5))
        next
          show ‹set (drop (length (ft'' 0)) (seqRun t x j)) ⊆ set (drop (length t) (seqRun t x j))›
            by (simp add: ‹length t ≤ length (ft'' 0)› set_drop_subset_set_drop)
        qed
        also from "**" have ‹set (drop (length t) (seqRun t x j)) ⊆ ev ` A›
          by (auto simp add: seqRun_def)
        finally show ‹?trH_A (ft'' i) = ?trH_A (ft'' 0)›
          by (simp add: ‹ft'' i = ft'' 0 @ t'› subset_iff)
      qed
      from "$"(2) obtain i where ‹ft'' 0 ≤ ft i› by (auto simp add: ft''_def)
      with prefixE obtain v where ‹ft i = ft'' 0 @ v› by blast

      have ‹ftF u› by (fact "*"(1))
      moreover have ‹tF (?trH_A (seqRun t x i)) ∨ u = []›
        by (metis "*"(2) "**" Hiding_tickFree trace_hide_seqRun_eq_iff)
      moreover have ‹s = ?trH_A (seqRun t x i) @ u›
        by (metis "*"(3) "**" trace_hide_seqRun_eq_iff)
      moreover have ‹?trH_A (seqRun t x i) setinterleaves ((?trH_A (ft i), ?trH_A (fu i)), ?tick_S)›
        using assms(5) Hiding_interleave by blast
      moreover have ‹?trH_A (ft i) ∈ D (P \ A)›
        apply (unfold D_Hiding, clarify)
        apply (rule exI[of _ ‹ft'' 0›])
        apply (rule exI[of _ ‹?trH_A v›])
        apply (intro conjI)
        subgoal by (metis assms(3) Hiding_front_tickFree ‹ft i = ft'' 0 @ v›
              front_tickFree_Nil front_tickFree_nonempty_append_imp is_processT2_TR) 
        subgoal by (metis strict_prefixE' T_imp_front_tickFree ‹range ft'' ⊆ T P› ‹strict_mono ft''›
              front_tickFree_append_iff list.distinct(1) range_subsetD strict_mono_Suc_iff)
        subgoal by (simp add: ‹ft i = ft'' 0 @ v›)
        subgoal using "$$" ‹range ft'' ⊆ T P› ‹strict_mono ft''› by blast .
      moreover have ‹?trH_A (fu i) ∈ T (Q \ A)›
      proof (cases ‹∃t'. ?trH_A t' = ?trH_A (fu i) ∧ (t', ev ` A) ∈ F Q›)
        assume ‹∃t'. ?trH_A t' = ?trH_A (fu i) ∧ (t', ev ` A) ∈ F Q›
        then obtain t' where ‹?trH_A (fu i) = ?trH_A t'› ‹(t', ev ` A) ∈ F Q› by metis
        thus ‹?trH_A (fu i) ∈ T (Q \ A)› unfolding T_Hiding by blast
      next
        assume ‹∄t'. ?trH_A t' = ?trH_A (fu i) ∧ (t', ev ` A) ∈ F Q›
        with assms(4) inf_hidden obtain fu' j
          where $$$ : ‹isInfHiddenRun fu' Q A› ‹fu i = fu' j› by blast
        show ‹?trH_A (fu i) ∈ T (Q \ A)›
          apply (unfold T_Hiding, simp)
          apply (rule disjI2)
          apply (rule exI[of _ ‹fu' j›], rule exI[of _ ‹[]›])
          apply (intro conjI)
          subgoal by simp
          subgoal by (metis "$$$"(1) strict_prefixE' T_imp_front_tickFree neq_Nil_conv
                front_tickFree_nonempty_append_imp strict_mono_Suc_iff)
          subgoal by (simp add: "$$$"(2))
          subgoal using "$$$"(1) by blast .
      qed
      ultimately have ‹s ∈ D ((P \ A) [S] (Q \ A))› unfolding D_Sync by blast
    } note $ = this

    from ‹infinite (range ft) ∨ infinite (range fu)›
    show ‹s ∈ D ((P \ A) [S] (Q \ A))›
    proof (elim disjE)
      from "$" "****" ‹∧i. set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A›
      show ‹infinite (range ft) ==> s ∈ D ((P \ A) [S] (Q \ A))› by blast
    next
      from "$" "****" ‹∧i. set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A›
      show ‹infinite (range fu) ==> s ∈ D ((P \ A) [S] (Q \ A))›
        by (metis Sync_commute setinterleaving_sym sup_commute)
    qed
  qed
next
  let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
  assume same_div : ‹D (P [S] Q \ A) = D ((P \ A) [S] (Q \ A))›
  fix s X assume ‹(s, X) ∈ F (P [S] Q \ A)›
  then consider ‹s ∈ D (P [S] Q \ A)›
    | t where ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ F (P [S] Q)›
    unfolding F_Hiding D_Hiding by blast
  thus ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
  proof cases
    from same_div D_F show ‹s ∈ D (P [S] Q \ A) ==> (s, X) ∈ F ((P \ A) [S] (Q \ A))› by blast
  next
    fix t assume * : ‹s = ?trH_A t› ‹(t, X ∪ ev ` A) ∈ F (P [S] Q)›
    then consider ‹t ∈ D (P [S] Q)›
      | (F) t_P X_P t_Q X_Q
      where ‹(t_P, X_P) ∈ F P› ‹(t_Q, X_Q) ∈ F Q›
        ‹t setinterleaves ((t_P, t_Q), ?tick_S)›
        ‹X ∪ ev ` A = (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q›
      by (auto simp add: F_Sync D_Sync) 
    thus ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
    proof cases
      assume ‹t ∈ D (P [S] Q)›
      with "*"(1) mem_D_imp_mem_D_Hiding have ‹s ∈ D (P [S] Q \ A)› by blast
      with same_div D_F show ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))› by blast
    next
      case F
      from inf_hidden[OF _ F(1)[THEN F_T], of A] inf_hidden[OF _ F(2)[THEN F_T], of A]
      consider (D_P) f_P where ‹isInfHiddenRun f_P P A› ‹t_P ∈ range f_P›
        | (D_Q) f_Q where ‹isInfHiddenRun f_Q Q A› ‹t_Q ∈ range f_Q›
        | (F_both) t_P' t_Q'
        where ‹?trH_A t_P' = ?trH_A t_P› ‹(t_P', ev ` A) ∈ F P›
          ‹?trH_A t_Q' = ?trH_A t_Q› ‹(t_Q', ev ` A) ∈ F Q›
        by blast
      thus ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
      proof cases
        case D_P
        have $ : ‹?trH_A t_P ∈ D (P \ A)›
          apply (unfold D_Hiding, clarify)
          apply (rule exI[of _ ‹t_P›], rule exI[of _ ‹[]›])
          using tickFree_isInfHiddenRun D_P front_tickFree_Nil by blast
        from F(2) F_T mem_T_imp_mem_T_Hiding
        have $$ : ‹?trH_A t_Q ∈ T (Q \ A)› by blast
        show ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
          apply (simp add: F_Sync)
          apply (rule disjI2)
          apply (rule exI[of _ ‹?trH_A t_P›])
          apply (rule exI[of _ ‹?trH_A t_Q›])
          apply (rule exI[of _ ‹?trH_A t›], rule exI[of _ ‹[]›])
          by (simp add: "*"(1) F(3) Hiding_interleave "$" "$$")
      next
        case D_Q
        from F(1) F_T mem_T_imp_mem_T_Hiding
        have $ : ‹?trH_A t_P∈ T (P \ A)› by blast
        have $$ : ‹?trH_A t_Q ∈ D (Q \ A)›
          apply (unfold D_Hiding, clarify)
          apply (rule exI[of _ ‹t_Q›], rule exI[of _ ‹[]›])
          using tickFree_isInfHiddenRun D_Q front_tickFree_Nil by blast
        show ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
          apply (simp add: F_Sync)
          apply (rule disjI2)
          apply (rule exI[of _ ‹?trH_A t_Q›])
          apply (rule exI[of _ ‹?trH_A t_P›])
          apply (rule exI[of _ ‹?trH_A t›], rule exI[of _ ‹[]›])
          by (simp add: "*"(1) F(3) Hiding_interleave setinterleaving_sym "$" "$$")
      next
        case F_both
        from F(4) ‹A ∩ S = {}› have ‹ev ` A ⊆ X_P› and ‹ev ` A ⊆ X_Q› by auto
        have ‹(?trH_A t_P, X_P) ∈ F (P \ A)›
          by (simp add: F_Hiding) (metis F(1) F_both(1) ‹ev ` A ⊆ X_P› sup.orderE)
        moreover have ‹(?trH_A t_Q, X_Q) ∈ F (Q \ A)›
          by (simp add: F_Hiding) (metis F(2) F_both(3) ‹ev ` A ⊆ X_Q› sup.orderE)
        moreover from F(3) Hiding_interleave
        have ‹s setinterleaves ((?trH_A t_P, ?trH_A t_Q), ?tick_S)›
          unfolding "*"(1) by blast
        ultimately have ‹(s, (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q) ∈ F ((P \ A) [S] (Q \ A))›
          unfolding F_Sync by blast
        moreover from F(4) have ‹X ⊆ (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q› by blast
        ultimately show ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))› by (fact is_processT4)
      qed
    qed
  qed
next
  let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
  fix s assume ‹s ∈ D ((P \ A) [S] (Q \ A))›
  then obtain t_P t_Q r v
    where * : ‹ftF v› ‹tF r ∨ v = []› ‹s = r @ v› ‹r setinterleaves ((t_P, t_Q), ?tick_S)›
      ‹t_P ∈ D (P \ A) ∧ t_Q ∈ T (Q \ A) ∨ t_P ∈ D (Q \ A) ∧ t_Q ∈ T (P \ A)›
    unfolding D_Sync by blast
  from ‹s ∈ D ((P \ A) [S] (Q \ A))› have ‹ftF s›
    by (simp add: D_imp_front_tickFree)
  { fix t_P t_Q and P Q
    assume ** : ‹r setinterleaves ((t_P, t_Q), ?tick_S)›
      ‹t_P ∈ D (P \ A)› ‹t_Q ∈ T (Q \ A)›
    from **(2) obtain t u
      where *** : ‹ftF u› ‹tF t› ‹t_P = ?trH_A t @ u›
        ‹t ∈ D P ∨ (∃x. isInfHidden_seqRun_strong x P A t)›
      by (elim D_Hiding_seqRunE)
    from interleave_append_left[OF "**"(1)[unfolded "***"(3)]]
    obtain t_Q1 t_Q2 r1 r2
      where **** : ‹t_Q = t_Q1 @ t_Q2› ‹r = r1 @ r2›
        ‹r1 setinterleaves ((?trH_A t, t_Q1), ?tick_S)›
        ‹r2 setinterleaves ((u, t_Q2), ?tick_S)› by blast
    from "**"(3) consider t_Q' where ‹t_Q = ?trH_A t_Q'› ‹(t_Q', ev ` A) ∈ F Q›
      | (D_Q) t' u' where ‹ftF u'› ‹tF t'› ‹t_Q = ?trH_A t' @ u'›
        ‹t' ∈ D Q ∨ (∃y. isInfHidden_seqRun_strong y Q A t')›
      by (elim T_Hiding_seqRunE)
    hence ‹s ∈ D (P [S] Q \ A)›
    proof cases
      fix t_Q' assume ‹t_Q = ?trH_A t_Q'› ‹(t_Q', ev ` A) ∈ F Q›
      from trace_hide_append[OF this(1)[unfolded "****"(1)]]
      obtain t_Q1' t_Q2' where $ : ‹t_Q' = t_Q1' @ t_Q2'› ‹t_Q1 = ?trH_A t_Q1'›
        ‹t_Q2 = ?trH_A t_Q2'› by blast
      from ‹A ∩ S = {}› have ‹ev ` A ∩ ?tick_S = {}› by blast
      from interleave_Hiding[OF this "****"(3)[unfolded "$"(2)]]
      obtain r1' where $$ : ‹r1 = ?trH_A r1'›
        ‹r1' setinterleaves ((t, t_Q1'), ?tick_S)› by blast

      show ‹s ∈ D (P [S] Q \ A)›
      proof (rule D_Hiding_seqRunI)
        show ‹ftF (r2 @ v)›
          by (metis "*"(1, 3) "****"(2) ‹ftF s›
              front_tickFree_append_iff tickFree_append_iff)
      next
        show ‹tF r1'›
          by (metis "$"(1) "$$"(2) "***"(2) F_imp_front_tickFree SyncWithTick_imp_NTF
              ‹(t_Q', ev ` A) ∈ F Q› front_tickFree_dw_closed nonTickFree_n_frontTickFree
              non_tickFree_tick tickFree_append_iff ftf_Sync tickFree_imp_front_tickFree)
      next
        from "$$"(1) "*"(3) "****"(2) append.assoc
        show ‹s = ?trH_A r1' @ r2 @ v› by blast
      next
        from "***"(4) show ‹r1' ∈ D (P [S] Q) ∨
 (∃x. ∀i. seqRun r1' x i ∈ T (P [S] Q) ∧ x i ∈ ev ` A)›
        proof (elim disjE exE)
          assume ‹t ∈ D P›
          moreover have ‹t_Q1' ∈ T Q›
            by (metis "$"(1) F_T prefixI ‹(t_Q', ev ` A) ∈ F Q› is_processT3_TR)
          ultimately have ‹r1' ∈ D (P [S] Q)›
            unfolding D_Sync using "$$"(2) front_tickFree_Nil by blast
          thus ‹r1' ∈ D (P [S] Q) ∨ (∃x. isInfHidden_seqRun x (P [S] Q) A r1')› ..
        next
          fix x assume "£" : ‹isInfHidden_seqRun_strong x P A t›
          from "£" ‹A ∩ S = {}› have ‹set (map x [0..<i]) ∩ ?tick_S = {}› for i
            by (simp add: disjoint_iff image_iff)
              (metis event<sub>ptick</sub>.distinct(1) event<sub>ptick</sub>.inject(1))
          from "$$"(2)[THEN interleave_append_tail_left, OF this, folded seqRun_def]
          have "££" : ‹seqRun r1' x i setinterleaves ((seqRun t x i, t_Q1'), ?tick_S)› for i .
          have ‹isInfHidden_seqRun x (P [S] Q) A r1'›
          proof (intro allI conjI)
            have ‹t_Q1' ∈ T Q›
              by (metis "$"(1) F_T prefixI ‹(t_Q', ev ` A) ∈ F Q› is_processT3_TR)
            with "£" "££" show ‹seqRun r1' x i ∈ T (P [S] Q)› for i
              unfolding T_Sync by blast
          next
            show ‹x i ∈ ev ` A› for i by (simp add: "£")
          qed
          thus ‹r1' ∈ D (P [S] Q) ∨ (∃x. isInfHidden_seqRun x (P [S] Q) A r1')› by blast
        qed
      qed
    next
      case D_Q
      have ‹t ∈ T P› using "***"(4) D_T by (metis seqRun_0)
      consider ‹?trH_A t' ≤ t_Q1› | ‹t_Q1 ≤ ?trH_A t'›
        by (metis "****"(1) D_Q(3) prefixI dual_order.eq_iff le_same_imp_eq_or_less nless_le)
      thus ‹s ∈ D (P [S] Q \ A)›
      proof cases
        assume ‹?trH_A t' ≤ t_Q1›
        from interleave_le_right[OF "****"(3) this]
        obtain r1_bis t_hidden_bis
          where ‹r1_bis ≤ r1› ‹t_hidden_bis ≤ ?trH_A t›
            ‹r1_bis setinterleaves ((t_hidden_bis, ?trH_A t'), ?tick_S)› by blast
        moreover from le_trace_hide[OF ‹t_hidden_bis ≤ ?trH_A t›]
        obtain t_bis where ‹t_hidden_bis = ?trH_A t_bis ∧ t_bis ≤ t› ..
        ultimately have $ : ‹r1_bis ≤ r1› ‹t_bis ≤ t›
          ‹r1_bis setinterleaves ((?trH_A t_bis, ?trH_A t'), ?tick_S)› by blast+
        from interleave_Hiding[OF _ "$"(3)] ‹A ∩ S = {}›
        obtain r1_bis_unhidden
          where $$ : ‹r1_bis = ?trH_A r1_bis_unhidden›
            ‹r1_bis_unhidden setinterleaves ((t_bis, t'), ?tick_S)› by blast
        from "$"(2) ‹t ∈ T P› is_processT3_TR have ‹t_bis ∈ T P› by blast
        from D_Q(4) have ‹r1_bis ∈ D (P [S] Q \ A)›
        proof (elim disjE exE)
          assume ‹t' ∈ D Q›
          with "$$"(2) ‹t_bis ∈ T P› have ‹r1_bis_unhidden ∈ D (P [S] Q)›
            by (simp add: D_Sync)
              (use front_tickFree_Nil setinterleaving_sym in blast)
          with "$$"(1) mem_D_imp_mem_D_Hiding show ‹r1_bis ∈ D (P [S] Q \ A)› by blast
        next
          fix y assume £ : ‹isInfHidden_seqRun_strong y Q A t'›
            (*  with exists_suff obtain g_suff
          where g_suff_props : \<open>g i = g 0 @ g_suff i\<close> \<open>set (g_suff i) \<subseteq> ev ` A\<close>
                               \<open>set (g_suff i) \<inter> ?tick_S = {}\<close> \<open>strict_mono g_suff\<close> for i by metis *)
          from "£" ‹A ∩ S = {}› have ‹set (map y [0..<i]) ∩ ?tick_S = {}› for i
            by (simp add: disjoint_iff image_iff)
              (metis event_ptick.distinct(1) event_ptick.inject(1))
          from "$$"(2)[THEN interleave_append_tail_right, OF this, folded seqRun_def]
          have $$$ : ‹seqRun r1_bis_unhidden y i setinterleaves ((t_bis, seqRun t' y i), ?tick_S)› for i .
          have $$$$ : ‹isInfHidden_seqRun y (P [S] Q) A r1_bis_unhidden›
          proof (intro allI conjI)
            from "$$$" "£" ‹t_bis ∈ T P›
            show ‹seqRun r1_bis_unhidden y i ∈ T (P [S] Q)› for i
              unfolding T_Sync by blast
          next
            show ‹y i ∈ ev ` A› for i by (simp add: "£")
          qed
          show ‹r1_bis ∈ D (P [S] Q \ A)›
          proof (rule D_Hiding_seqRunI)
            show ‹ftF []› by simp
          next
            show ‹tF r1_bis_unhidden›
              by (metis "$$"(2) D_Q(2) SyncWithTick_imp_NTF T_imp_front_tickFree ‹t_bis ∈ T P›
                  ftf_Sync nonTickFree_n_frontTickFree non_tickFree_tick
                  tickFree_append_iff tickFree_imp_front_tickFree)
          next
            show ‹r1_bis = ?trH_A r1_bis_unhidden @ []› by (simp add: $$(1))
          next
            from "$$$$" show ‹r1_bis_unhidden ∈ D (P [S] Q) ∨
 (∃x. isInfHidden_seqRun x (P [S] Q) A r1_bis_unhidden)› by blast
          qed
        qed
        with "$"(1) show ‹s ∈ D (P [S] Q \ A)›
          unfolding less_eq_list_def prefix_def
          by (metis (no_types, opaque_lifting) "*"(3) "****"(2) ‹ftF s›
              append_Nil2 front_tickFree_append_iff front_tickFree_dw_closed is_processT7)
      next
        assume ‹t_Q1 ≤ ?trH_A t'›
        from le_trace_hide[OF this] obtain t_Q1_unhidden
          where $ : ‹t_Q1 = ?trH_A t_Q1_unhidden› ‹t_Q1_unhidden ≤ t'› by blast
        from ‹A ∩ S = {}› have ‹ev ` A ∩ ?tick_S = {}› by blast
        from "****"(3)[unfolded "$"(1)]
        have ‹r1 setinterleaves ((?trH_A t, ?trH_A t_Q1_unhidden), ?tick_S)› .
        from interleave_Hiding[OF ‹ev ` A ∩ ?tick_S = {}› this]
        obtain r1_unhidden
          where $$ : ‹r1 = ?trH_A r1_unhidden›
            ‹r1_unhidden setinterleaves ((t, t_Q1_unhidden), ?tick_S)› by blast
        from ‹t_Q1_unhidden ≤ t'› have ‹t_Q1_unhidden ∈ T Q›
          by (metis D_Q(4) D_T is_processT3_TR t_le_seqRun)

        from "***"(4) have ‹r1 ∈ D (P [S] Q \ A)›
        proof (elim disjE exE)
          assume ‹t ∈ D P›
          have ‹r1_unhidden ∈ D (P [S] Q)›
          proof (unfold D_Sync, clarify, intro exI conjI)
            show ‹ftF []› ‹tF r1_unhidden ∨ [] = []›
              ‹r1_unhidden = r1_unhidden @ []› by simp_all
          next
            show ‹r1_unhidden setinterleaves ((t, t_Q1_unhidden), ?tick_S)› by (fact "$$"(2))
          next
            show ‹t ∈ D P ∧ t_Q1_unhidden ∈ T Q ∨ t ∈ D Q ∧ t_Q1_unhidden ∈ T P›
              by (simp add: ‹t ∈ D P› ‹t_Q1_unhidden ∈ T Q›)
          qed
          thus ‹r1 ∈ D (P [S] Q \ A)› unfolding "$$"(1) by (fact mem_D_imp_mem_D_Hiding)
        next
          fix x assume £ : ‹isInfHidden_seqRun_strong x P A t›
          from "£" ‹A ∩ S = {}› have ‹set (map x [0..<i]) ∩ ?tick_S = {}› for i
            by (simp add: disjoint_iff image_iff)
              (metis event_ptick.distinct(1) event_ptick.inject(1))
          from "$$"(2)[THEN interleave_append_tail_left, OF this, folded seqRun_def]
          have "££" : ‹seqRun r1_unhidden x i setinterleaves ((seqRun t x i, t_Q1_unhidden), ?tick_S)› for i .
          have "£££" : ‹isInfHidden_seqRun x (P [S] Q) A r1_unhidden›
          proof (intro allI conjI)
            from "£" "££" ‹t_Q1_unhidden ∈ T Q›
            show ‹seqRun r1_unhidden x i ∈ T (P [S] Q)› for i unfolding T_Sync by blast
          next
            from "£" show ‹x i ∈ ev ` A› for i by blast
          qed
          show ‹r1 ∈ D (P [S] Q \ A)›
          proof (unfold D_Hiding_seqRun, clarify, intro exI conjI)
            show ‹ftF []› by simp
          next
            from isInfHidden_seqRun_imp_tickFree[OF "£££"] show ‹tF r1_unhidden› .
          next
            show ‹r1 = ?trH_A r1_unhidden @ []› by (simp add: "$$"(1))
          next
            from "£££" show ‹r1_unhidden ∈ D (P [S] Q) ∨
 (∃x. isInfHidden_seqRun x (P [S] Q) A r1_unhidden)› by blast
          qed
        qed
        thus ‹s ∈ D (P [S] Q \ A)›
          by (metis "*"(3) "****"(2) ‹ftF s› append.right_neutral
              front_tickFree_append_iff front_tickFree_dw_closed is_processT7)
      qed
    qed
  } note $ = this
  from "*"(5) show ‹s ∈ D (P [S] Q \ A)›
    by (elim disjE conjE) (metis "$" "*"(4), metis "$" "*"(4) Sync_commute)
next
  let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
  assume same_div : ‹D (P [S] Q \ A) = D ((P \ A) [S] (Q \ A))›
  fix s X assume ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
  then consider ‹s ∈ D ((P \ A) [S] (Q \ A))›
    | (F) s_P X_P s_Q X_Q
    where ‹(s_P, X_P) ∈ F (P \ A)› ‹(s_Q, X_Q) ∈ F (Q \ A)›
      ‹s setinterleaves ((s_P, s_Q), ?tick_S)›
      ‹X = (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q›
    unfolding F_Sync D_Sync by blast
  thus ‹(s, X) ∈ F (P [S] Q \ A)›
  proof cases
    from same_div D_F show ‹s ∈ D ((P \ A) [S] (Q \ A)) ==> (s, X) ∈ F (P [S] Q \ A)› by blast
  next
    case F
    from F(1, 2) consider ‹s_P ∈ D (P \ A)› | ‹s_Q ∈ D (Q \ A)›
      | (F_both) s_P' s_Q'
      where ‹s_P = ?trH_A s_P'› ‹(s_P', X_P ∪ ev ` A) ∈ F P›
        ‹s_Q = ?trH_A s_Q'› ‹(s_Q', X_Q ∪ ev ` A) ∈ F Q›
      unfolding F_Hiding D_Hiding by blast
    thus ‹(s, X) ∈ F (P [S] Q \ A)›
    proof cases
      assume ‹s_P ∈ D (P \ A)›
      moreover from F(2) F_T have ‹s_Q ∈ T (Q \ A)› by blast
      ultimately have ‹s ∈ D ((P \ A) [S] (Q \ A))›
        using F(3) front_tickFree_Nil unfolding D_Sync by blast
      with same_div D_F show ‹(s, X) ∈ F (P [S] Q \ A)› by blast
    next
      from F(1) F_T have ‹s_P ∈ T (P \ A)› by blast
      moreover assume ‹s_Q ∈ D (Q \ A)›
      moreover have ‹s setinterleaves ((s_Q, s_P), range tick ∪ ev ` S)›
        by (simp add: F(3) setinterleaving_sym)
      ultimately have ‹s ∈ D ((P \ A) [S] (Q \ A))›
        using front_tickFree_Nil unfolding D_Sync by blast
      with same_div D_F show ‹(s, X) ∈ F (P [S] Q \ A)› by blast
    next
      case F_both
      from ‹A ∩ S = {}› have ‹ev ` A ∩ (range tick ∪ ev ` S) = {}› by blast
      from interleave_Hiding[OF this F(3)[unfolded F_both(1, 3)]]
      obtain s' where * : ‹s = ?trH_A s'›
        ‹s' setinterleaves ((s_P', s_Q'), range tick ∪ ev ` S)› by blast
      have ‹X ∪ ev ` A = (X_P ∪ ev ` A ∪ (X_Q ∪ ev ` A)) ∩ (range tick ∪ ev ` S)
 ∪ (X_P ∪ ev ` A) ∩ (X_Q ∪ ev ` A)›
        by (simp add: F(4) Un_Int_distrib2 Un_assoc sup_left_commute)
      thus ‹(s, X) ∈ F (P [S] Q \ A)›
        by (simp add: "*"(1) F_Hiding F_Sync) (use "*"(2) F_both(2, 4) in blast)
    qed
  qed
qed





(* TODO: do we need this ? *)
(* Trivial results have been removed *)
(* 
lemmas Par_SKIP_SKIP = SKIP_Sync_SKIP[where S = \<open>UNIV\<close>]
   and Par_SKIP_STOP = SKIP_Sync_STOP[where S = \<open>UNIV\<close>]
   and Par_commute = Sync_commute[where S = \<open>UNIV\<close>]
   and Par_assoc = Sync_assoc[where S = \<open>UNIV\<close>]
   and Mprefix_Par_SKIP = Mprefix_Sync_SKIP[where S = \<open>UNIV\<close>, simplified]
   and prefix_Par_SKIP = prefix_Sync_SKIP[where S = \<open>UNIV\<close>, simplified]
   and prefix_Par1 = prefix_Sync1[where S = \<open>UNIV\<close>, simplified]
   and prefix_Par2 = prefix_Sync2[where S = \<open>UNIV\<close>, simplified]
   and Mprefix_Par_distr = Mprefix_Sync_Mprefix_subset[where S = \<open>UNIV\<close>, simplified]

   and Inter_SKIP_SKIP = SKIP_Sync_SKIP[where S = \<open>{}\<close>]
   and Inter_SKIP_STOP = SKIP_Sync_STOP[where S = \<open>{}\<close>]
   and Inter_commute = Sync_commute[where S = \<open>{}\<close>]
   and Inter_assoc = Sync_assoc[where S = \<open>{}\<close>]
   and Mprefix_Inter_SKIP = Mprefix_Sync_SKIP[where S = \<open>{}\<close>, simplified]
   and prefix_Inter_SKIP = prefix_Sync_SKIP[where S = \<open>{}\<close>, simplified]
   (* and Hiding_Inter = Hiding_Sync[where S = \<open>{}\<close>, simplified] *)
   and Mprefix_Inter_distr = Mprefix_Sync_Mprefix_indep[where S = ‹{}›, simplified]
   and prefix_Inter = Mprefix_Sync_Mprefix_indep[of ‹{a}› ‹{}› ‹{b}› ‹λx. P› ‹λx. Q›,
                                               simplified, folded write0_def] for a P b Q
 *)




subsection ‹Renaming Operator Laws›

lemma Renaming_Ndet: ‹Renaming (P ⊓ Q) f g = Renaming P f g ⊓ Renaming Q f g›
  by (subst Process_eq_spec) (auto simp add: F_Renaming D_Renaming F_Ndet D_Ndet)


lemma Renaming_Det:  ‹Renaming (P ◻ Q) f g = Renaming P f g ◻ Renaming Q f g›
proof (subst Process_eq_spec, safe)
  show ‹(s, X) ∈ F (Renaming (P ◻ Q) f g) ==>
 (s, X) ∈ F (Renaming P f g ◻ Renaming Q f g)› for s X
    by (cases s) (auto simp add: F_Renaming F_Det D_Renaming D_Det T_Renaming)+
next
  fix s X assume ‹(s, X) ∈ F (Renaming P f g ◻ Renaming Q f g)›
  then consider ‹s = []› ‹(s, X) ∈ F (Renaming P f g)› ‹(s, X) ∈ F (Renaming Q f g)›
    | e s' where ‹s = e # s'› ‹(s, X) ∈ F (Renaming P f g) ∨ (s, X) ∈ F (Renaming Q f g)›
    | ‹s = []› ‹s ∈ D (Renaming P f g) ∨ s ∈ D (Renaming Q f g)›
    | r where ‹s = []› ‹🚫(r) ∉ X› ‹([🚫(r)] ∈ T (Renaming P f g) ∨ [🚫(r)] ∈ T (Renaming Q f g))›
    by (cases s) (auto simp add: F_Det)
  thus ‹(s, X) ∈ F (Renaming (P ◻ Q) f g)›
  proof cases
    show ‹[s = []; (s, X) ∈ F (Renaming P f g); (s, X) ∈ F (Renaming Q f g)]
 ==> (s, X) ∈ F (Renaming (P ◻ Q) f g)›
      by (auto simp add: F_Renaming F_Det)
  next
    show ‹s = e # s' ==> (s, X) ∈ F (Renaming P f g) ∨ (s, X) ∈ F (Renaming Q f g)
 ==> (s, X) ∈ F (Renaming (P ◻ Q) f g)› for s' e
      by (simp add: F_Renaming F_Det D_Det, safe)
        (metis list.distinct(1) list.simps(9), presburger)+
  next
    show ‹s = [] ==> s ∈ D (Renaming P f g) ∨ s ∈ D (Renaming Q f g)
 ==> (s, X) ∈ F (Renaming (P ◻ Q) f g)›
      by (simp add: D_Renaming F_Renaming D_Det)
  next
    show ‹[s = []; 🚫(r) ∉ X; [🚫(r)] ∈ T (Renaming P f g) ∨ [🚫(r)] ∈ T (Renaming Q f g)]
 ==> (s, X) ∈ F (Renaming (P ◻ Q) f g)› for r
      by (auto simp add: T_Renaming F_Renaming D_Det F_Det
          dest: map_event_{ptick_eq_tick_iff}[THEN iffD1, OF sym, of r])
        (metis append_eq_Cons_conv list.map_disc_iff map_event_{ptick_tickFree}
          non_tickFree_tick tickFree_Nil tickFree_append_iff)+
  qed
next
  show ‹s ∈ D (Renaming (P ◻ Q) f g) ==> s ∈ D (Renaming P f g ◻ Renaming Q f g)›
    and ‹s ∈ D (Renaming P f g ◻ Renaming Q f g) ==> s ∈ D (Renaming (P ◻ Q) f g)› for s
    by (auto simp add: D_Renaming D_Det)
qed


lemma Sliding_STOP_Det [simp] : ‹(P ⊳ STOP) ◻ Q = P ⊳ Q›
  by (simp add: Det_commute Det_distrib_Ndet_left Sliding_def)

lemma Sliding_Det: ‹(P ⊳ P') ◻ Q = P ⊳ P' ◻ Q›
  by (metis Det_assoc Sliding_STOP_Det)  


lemma Renaming_Sliding:
  ‹Renaming (P ⊳ Q) f g = Renaming P f g ⊳ Renaming Q f g›
  by (simp add: Renaming_Det Renaming_Ndet Sliding_def)



(* TODO: do we need the following versions ? *)
lemma Renaming_Mprefix_image:
  ‹Renaming (◻ a ∈ A → P (f a)) f g =
 ◻ b ∈ f ` A → Renaming (P b) f g› (is ‹?lhs = ?rhs›)
  by (subst Renaming_Mprefix, rule mono_Mprefix_eq)
    (simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet F_Renaming D_Renaming, safe, auto)

lemma Renaming_Mprefix_image_inj_on:
  ‹Renaming (Mprefix A P) f g = ◻ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
  if inj_on_f: ‹inj_on f A›
  apply (subst Renaming_Mprefix_image[symmetric])
  apply (intro arg_cong[where f = ‹λQ. Renaming Q f g›] mono_Mprefix_eq)
  by (metis that the_inv_into_def the_inv_into_f_f)

corollary Renaming_Mprefix_image_inj:
  ‹Renaming (Mprefix A P) f g = ◻ b ∈ f ` A → Renaming (P (THE a. f a = b)) f g› if inj_f: ‹inj f›
  apply (subst Renaming_Mprefix_image_inj_on, metis inj_eq inj_onI that)
  apply (rule mono_Mprefix_eq[rule_format])
  by (metis imageE inj_eq[OF inj_f])


lemma Renaming_Mndetprefix_image: ‹Renaming (⊓ a ∈ A → P (f a)) f g = ⊓ b ∈ f ` A → Renaming (P b) f g›
  by (auto simp add: Mndetprefix_GlobalNdet Renaming_distrib_GlobalNdet write0_def Renaming_Mprefix
      intro!: mono_Mprefix_eq mono_GlobalNdet_eq2 intro: sym)

corollary Renaming_Mndetprefix_inj_on:
  ‹Renaming (Mndetprefix A P) f g = ⊓ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
  if inj_on_f: ‹inj_on f A›
  apply (subst Renaming_Mndetprefix_image[symmetric])
  apply (intro arg_cong[where f = ‹λQ. Renaming Q f g›] mono_Mndetprefix_eq)
  by (metis that the_inv_into_def the_inv_into_f_f)

corollary Renaming_Mndetprefix_inj:
  ‹Renaming (Mndetprefix A P) f g = ⊓ b ∈ f ` A → Renaming (P (THE a. f a = b)) f g›
  if inj_f: ‹inj f›
  apply (subst Renaming_Mndetprefix_inj_on, metis inj_eq inj_onI that)
  apply (rule mono_Mndetprefix_eq[rule_format])
  by (metis imageE inj_eq[OF inj_f])



lemma Hiding_distrib_FD_GlobalNdet :
  ‹(⊓a ∈ A. P a) \ S ⊑_FD ⊓a ∈ A. (P a \ S)› (is ‹?lhs ⊑_FD ?rhs›)
proof (cases ‹A = {}›)
  show ‹A = {} ==> ?lhs ⊑_FD ?rhs› by simp
next
  show ‹?lhs ⊑_FD ?rhs› if ‹A ≠ {}›
  proof (rule failure_divergence_refine_optimizedI)
    show ‹s ∈ D ?rhs ==> s ∈ D ?lhs› for s
      by (simp add: GlobalNdet_projs D_Hiding_seqRun) blast
  next
    assume subset_div : ‹D ?rhs ⊆ D ?lhs›
    fix s X assume ‹(s, X) ∈ F ?rhs›
    then obtain a where ‹a ∈ A› ‹(s, X) ∈ F (P a \ S)›
      by (auto simp add: F_GlobalNdet ‹A ≠ {}›)
    from ‹(s, X) ∈ F (P a \ S)› consider ‹s ∈ D (P a \ S)›
      | t where ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ F (P a)›
      unfolding D_Hiding F_Hiding by blast
    thus ‹(s, X) ∈ F ?lhs›
    proof cases
      assume ‹s ∈ D (P a \ S)›
      with ‹a ∈ A› have ‹s ∈ D ?rhs› by (auto simp add: D_GlobalNdet)
      with subset_div D_F show ‹(s, X) ∈ F ?lhs› by blast
    next
      from ‹a ∈ A› show ‹s = trace_hide t (ev ` S) ==> (t, X ∪ ev ` S) ∈ F (P a)
 ==> (s, X) ∈ F ?lhs› for t
        by (simp add: F_Hiding_seqRun F_GlobalNdet) blast
    qed
  qed
qed



lemma Renaming_Seq :
  ‹Renaming (P ; Q) f g = Renaming P f g ; Renaming Q f g› (is ‹?lhs = ?rhs›)
proof (rule Process_eq_optimizedI)
  fix t assume ‹t ∈ D ?lhs›
  then obtain u v where ‹t = map (map_event_ptick f g) u @ v› ‹tF u› ‹ftF v› ‹u ∈ D (P ; Q)›
    unfolding D_Renaming by blast
  from ‹u ∈ D (P ; Q)› consider ‹u ∈ D P›
    | u1 u2 r where ‹u = u1 @ u2› ‹u1 @ [🚫(r)] ∈ T P› ‹u2 ∈ D Q›
    unfolding D_Seq by blast
  thus ‹t ∈ D ?rhs›
  proof cases
    from ‹ftF v› ‹t = map (map_event_ptick f g) u @ v› ‹tF u›
    show ‹u ∈ D P ==> t ∈ D ?rhs› by (auto simp add: D_Seq D_Renaming)
  next
    fix u1 u2 r assume ‹u = u1 @ u2› ‹u1 @ [🚫(r)] ∈ T P› ‹u2 ∈ D Q›
    from ‹u1 @ [🚫(r)] ∈ T P› have ‹map (map_event_ptick f g) u1 @ [🚫(g r)] ∈ T (Renaming P f g)›
      by (auto simp add: T_Renaming)
    moreover from ‹u2 ∈ D Q› ‹tF u› ‹u = u1 @ u2›
    have ‹map (map_event_ptick f g) u2 ∈ D (Renaming Q f g)›
      by (simp add: D_Renaming) (use front_tickFree_Nil in blast)
    ultimately have ‹map (map_event_ptick f g) u ∈ D ?rhs› by (auto simp add: ‹u = u1 @ u2› D_Seq)
    thus ‹t ∈ D ?rhs› by (simp add: ‹t = map (map_event_ptick f g) u @ v› ‹ftF v›
          ‹tF u› is_processT7 map_event_{ptick_tickFree})
  qed
next
  fix t assume ‹t ∈ D ?rhs›
  thm this[simplified D_Seq, simplified]
  then consider ‹t ∈ D (Renaming P f g)›
    | t1 t2 s where ‹t = t1 @ t2› ‹t1 @ [🚫(s)] ∈ T (Renaming P f g)›
      ‹t1 @ [🚫(s)] ∉ D (Renaming P f g)› ‹t2 ∈ D (Renaming Q f g)›
    by (simp add: D_Seq) (metis D_imp_front_tickFree append_T_imp_tickFree
        is_processT7 is_processT9 list.distinct(1))
  thus ‹t ∈ D ?lhs›
  proof cases
    show ‹t ∈ D (Renaming P f g) ==> t ∈ D ?lhs›
      by (auto simp add: D_Renaming D_Seq)
  next
    fix t1 t2 s assume ‹t = t1 @ t2› ‹t1 @ [🚫(s)] ∈ T (Renaming P f g)›
      ‹t1 @ [🚫(s)] ∉ D (Renaming P f g)› ‹t2 ∈ D (Renaming Q f g)›
    from this(2, 3) obtain u1' where ‹t1 @ [🚫(s)] = map (map_event_ptick f g) u1'› ‹u1' ∈ T P›
      by (auto simp add: Renaming_projs)
    then obtain u1 r where ‹s = g r› ‹t1 = map (map_event_ptick f g) u1› ‹u1 @ [🚫(r)] ∈ T P›
      by (cases u1' rule: rev_cases) (auto simp add: tick_eq_map_event_{ptick_iff})
    from ‹t2 ∈ D (Renaming Q f g)› obtain u2 u3
      where ‹t2 = map (map_event_ptick f g) u2 @ u3› ‹tF u2› ‹ftF u3› ‹u2 ∈ D Q›
      unfolding D_Renaming by blast
    from ‹u1 @ [🚫(r)] ∈ T P› ‹u2 ∈ D Q› have ‹u1 @ u2 ∈ D (P ; Q)›
      by (auto simp add: D_Seq)
    with ‹ftF u3› ‹tF u2› ‹u1 @ [🚫(r)] ∈ T P› show ‹t ∈ D ?lhs›
      by (simp add: ‹t = t1 @ t2› ‹t1 = map (map_event_ptick f g) u1›
          ‹t2 = map (map_event_ptick f g) u2 @ u3› D_Renaming)
        (metis append_T_imp_tickFree append_eq_appendI map_append not_Cons_self tickFree_append_iff)
  qed
next
  fix t X assume ‹(t, X) ∈ F ?lhs› ‹t ∉ D ?lhs›
  from ‹(t, X) ∈ F ?lhs› ‹t ∉ D ?lhs› obtain u
    where ‹t = map (map_event_ptick f g) u› ‹(u, map_event_ptick f g -` X) ∈ F (P ; Q)›
    unfolding Renaming_projs by blast
  from ‹(u, map_event<sub>ptick</sub> f g -` X) ∈ F (P ; Q)› ‹t ∉ D ?lhs›
  consider ‹(u, map_event_ptick f g -` X ∪ range tick) ∈ F P› ‹tF u›
    | u1 r u2 where ‹u = u1 @ u2› ‹u1 @ [🚫(r)] ∈ T P› ‹(u2, map_event<sub>ptick</sub> f g -` X) ∈ F Q›
    by (auto simp add: ‹t = map (map_event_ptick f g) u› Seq_projs D_Renaming)
      (metis D_imp_front_tickFree butlast_snoc front_tickFree_iff_tickFree_butlast front_tickFree_single
        is_processT8 is_processT9 map_append map_event_{ptick_front_tickFree} nonTickFree_n_frontTickFree)
  thus ‹(t, X) ∈ F ?rhs›
  proof cases
    assume ‹(u, map_event_ptick f g -` X ∪ range tick) ∈ F P› ‹tF u›
    have ‹map_event<sub>ptick</sub> f g -` X ∪ map_event_ptick f g -` range tick ⊆ map_event<sub>ptick</sub> f g -` X ∪ range tick›
      by (auto simp add: map_event_{ptick_eq_tick_iff})
    with ‹(u, map_event_ptick f g -` X ∪ range tick) ∈ F P›
    have ‹(u, map_event<sub>ptick</sub> f g -` X ∪ map_event_ptick f g -` range tick) ∈ F P›
      by (meson is_processT4)
    with ‹tF u› show ‹(t, X) ∈ F ?rhs›
      by (auto simp add: F_Seq ‹t = map (map_event<sub>ptick</sub> f g) u› F_Renaming map_event<sub>ptick_tickFree</sub>)
  next
    fix u1 u2 r assume ‹u = u1 @ u2› ‹u1 @ [🚫(r)] ∈ T P› ‹(u2, map_event<sub>ptick</sub> f g -` X) ∈ F Q›
    from ‹u1 @ [🚫(r)] ∈ T P› have ‹map (map_event_ptick f g) u1 @ [🚫(g r)] ∈ T (Renaming P f g)›
      by (auto simp add: T_Renaming)
    moreover from ‹(u2, map_event_ptick f g -` X) ∈ F Q›
    have ‹(map (map_event<sub>ptick</sub> f g) u2, X) ∈ F (Renaming Q f g)› by (auto simp add: F_Renaming)
    ultimately show ‹(t, X) ∈ F ?rhs›
      by (auto simp add: ‹t = map (map_event<sub>ptick</sub> f g) u› ‹u = u1 @ u2› F_Seq)
  qed
next
  fix t X assume ‹(t, X) ∈ F ?rhs› ‹t ∉ D ?rhs› ‹t ∉ D ?lhs›
  then consider ‹(t, X ∪ range tick) ∈ F (Renaming P f g)› ‹tF t›
    | t1 t2 s where ‹t = t1 @ t2› ‹t1 @ [🚫(s)] ∈ T (Renaming P f g)› ‹(t2, X) ∈ F (Renaming Q f g)›
    unfolding Seq_projs by blast
  thus ‹(t, X) ∈ F ?lhs›
  proof cases
    assume ‹(t, X ∪ range tick) ∈ F (Renaming P f g)› ‹tF t›
    with ‹t ∉ D ?rhs› obtain u
      where ‹t = map (map_event<sub>ptick</sub> f g) u›
        ‹(u, map_event<sub>ptick</sub> f g -` X ∪ map_event_ptick f g -` range tick) ∈ F P›
      by (auto simp add: D_Seq Renaming_projs)
    from this(2) have ‹(u, map_event<sub>ptick</sub> f g -` X ∪ range tick) ∈ F P›
      by (rule is_processT4) auto
    with ‹tF t› show ‹(t, X) ∈ F ?lhs›
      by (auto simp add: F_Renaming F_Seq ‹t = map (map_event_ptick f g) u› map_event_{ptick_tickFree})
  next
    fix t1 t2 s assume ‹t = t1 @ t2› ‹t1 @ [🚫(s)] ∈ T (Renaming P f g)› ‹(t2, X) ∈ F (Renaming Q f g)›
    from ‹t ∉ D ?rhs› have ‹t1 @ [🚫(s)] ∉ D (Renaming P f g)›
      by (simp add: ‹t = t1 @ t2› D_Seq)
        (metis D_imp_front_tickFree F_imp_front_tickFree ‹(t2, X) ∈ F (Renaming Q f g)›
          front_tickFree_append_iff is_processT7 is_processT9 not_Cons_self)
    with ‹t1 @ [🚫(s)] ∈ T (Renaming P f g)› obtain u1'
      where ‹t1 @ [🚫(s)] = map (map_event_ptick f g) u1'› ‹u1' ∈ T P›
      unfolding Renaming_projs by blast
    then obtain u1 r where ‹s = g r› ‹t1 = map (map_event_ptick f g) u1› ‹u1 @ [🚫(r)] ∈ T P›
      by (cases u1' rule: rev_cases) (auto simp add: tick_eq_map_event_{ptick_iff})
    from ‹t ∉ D ?rhs› ‹t1 @ [🚫(s)] ∈ T (Renaming P f g)› have ‹t2 ∉ D (Renaming Q f g)›
      by (auto simp add: ‹t = t1 @ t2› D_Seq)
    with ‹(t2, X) ∈ F (Renaming Q f g)› obtain u2
      where ‹t2 = map (map_event_ptick f g) u2› ‹(u2, map_event_ptick f g -` X) ∈ F Q›
      unfolding Renaming_projs by blast
    from ‹(u2, map_event<sub>ptick</sub> f g -` X) ∈ F Q› ‹u1 @ [🚫(r)] ∈ T P›
    have ‹(u1 @ u2, map_event_ptick f g -` X) ∈ F (P ; Q)› by (auto simp add: F_Seq)
    thus ‹(t, X) ∈ F ?lhs›
      by (auto simp add: ‹t = t1 @ t2› ‹t1 = map (map_event_ptick f g) u1›
          ‹t2 = map (map_event_ptick f g) u2› F_Renaming)
  qed
qed



lemma Renaming_fix :
  ‹Renaming (μ X. φ X) f g = (μ X. ((λP. Renaming P f g) ∘ φ ∘ (λP. Renaming P (inv f) (inv g))) X)›
  (is ‹Renaming (μ X. φ X) f g = (μ X. ?φ' X)›) if ‹cont φ›
  and ‹bij f› and ‹bij g› for φ :: ‹('a, 'r) process_ptick → ('a, 'r) process_ptick›
proof -
  ― ‹Some facts first.›
  have * : ‹φ = (λP. Renaming P (inv f) (inv g)) ∘ ?φ' ∘ (λP. Renaming P f g)›
    by (rule ext) (simp add: Renaming_inv bij_is_inj ‹bij f› ‹bij g›)

  have mono_φ  : ‹P ⊑ Q ==> φ P ⊑ φ Q› for P Q
    by (simp add: cont2monofunE ‹cont φ›)
  have mono_φ' : ‹P ⊑ Q ==> ?φ' P ⊑ ?φ' Q› for P Q
    by (simp add: mono_Renaming mono_φ)

  have finitary_props : ‹finitary f› ‹finitary g› ‹finitary (inv f)› ‹finitary (inv g)›
    by (simp_all add: bij_is_inj bij_is_surj surj_imp_inj_inv ‹bij f› ‹bij g›)
  have ‹cont (λX. Renaming (φ X) f g)› by (simp add: finitary_props(1, 2) ‹cont φ›)
  moreover have ‹cont (λX. Renaming X (inv f) (inv g))› by (simp add: finitary_props(3, 4))
  ultimately have ‹cont ?φ'› unfolding comp_def by (rule cont_compose)

  from ‹cont φ› ‹cont ?φ'› cont_process_rec 
  have ** : ‹(μ X. φ X) = φ (μ X. φ X)› ‹(μ X. ?φ' X) = ?φ' (μ X. ?φ' X)› by blast+

  show ‹Renaming (μ X. φ X) f g = (μ X. ?φ' X)›
  proof (rule below_antisym)
    show ‹Renaming (μ X. φ X) f g ⊑ (μ X. ?φ' X)›
    proof (induct rule: fix_ind[where F = ‹Λ X. φ X›])
      show ‹adm (λa. Renaming a f g ⊑ (μ X. ?φ' X))›
        by (simp add: ‹finitary f› ‹finitary g› monofunI)
    next
      show ‹Renaming ⊥ f g ⊑ (μ X. ?φ' X)› by simp
    next
      fix X assume ‹Renaming X f g ⊑ (μ X. ?φ' X)›
      hence ‹?φ' (Renaming X f g) ⊑ ?φ' (μ X. ?φ' X)› by (fact mono_φ')
      hence ‹Renaming (?φ' (Renaming X f g)) (inv f) (inv g) ⊑
 Renaming (?φ' (μ X. ?φ' X)) (inv f) (inv g)› by (fact mono_Renaming)
      also from "*" have ‹Renaming (?φ' (Renaming X f g)) (inv f) (inv g) = φ X›
        unfolding comp_def by metis
      also from "**"(2) have ‹?φ' (μ X. ?φ' X) = (μ X. ?φ' X)› by argo
      finally have ‹Renaming (φ X) f g ⊑ Renaming (Renaming (μ X. ?φ' X) (inv f) (inv g)) f g›
        by (fact mono_Renaming)
      also have ‹… = (μ X. ?φ' X)› by (simp add: inv_Renaming ‹bij f› ‹bij g›)
      finally show ‹Renaming ((Λ X. φ X)⋅X) f g ⊑ (μ X. ?φ' X)›
        by (subst beta_cfun[OF ‹cont φ›]) (simp add: comp_def)
    qed
  next
    show ‹(μ X. ?φ' X) ⊑ Renaming (μ X. φ X) f g›
    proof (induct rule: fix_ind[where F = ‹Λ X. ?φ' X›])
      show ‹adm (λa. a ⊑ Renaming (μ x. φ x) f g)› by (simp add: monofunI)
    next
      show ‹⊥ ⊑ Renaming (μ x. φ x) f g› by simp
    next
      fix X assume hyp : ‹X ⊑ Renaming (μ X. φ X) f g›
      hence ‹Renaming X (inv f) (inv g) ⊑ Renaming (Renaming (μ X. φ X) f g) (inv f) (inv g)›
        by (fact mono_Renaming)
      also have ‹… = (μ X. φ X)› by (simp add: Renaming_inv bij_is_inj ‹bij f› ‹bij g›)
      finally have ‹φ (Renaming X (inv f) (inv g)) ⊑ φ (μ X. φ X)› by (fact mono_φ)
      hence ‹Renaming (φ (Renaming X (inv f) (inv g))) f g ⊑
 Renaming (φ (μ x. φ x)) f g› by (fact mono_Renaming)
      also from "**"(1) have ‹φ (μ x. φ x) = (μ X. φ X)› by presburger
      finally show ‹(Λ X. ?φ' X)⋅X ⊑ Renaming (μ X. φ X) f g›
        by (subst beta_cfun[OF ‹cont ?φ'›]) (simp add: comp_def)
    qed
  qed
qed



(*<*)
end
  (*>*)