Theory CSP_New_Laws

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff.
 *
 * This file       : New laws
 *
 * 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.
 ******************************************************************************›
(*>*)

chapter‹ Bonus: powerful new Laws ›

(*<*)
theory  CSP_New_Laws
  imports Initials
begin
(*>*)

section ‹Powerful Results about \<^const>‹Sync››

lemma add_complementary_events_of_in_failure:
  ‹(t, X) ∈ ℱ P ⟹ (t, X ∪ ev ` (- α(P))) ∈ ℱ P›
  by (erule is_processT5) (auto simp add: events_of_def, metis F_T in_set_conv_decomp)

lemma add_complementary_initials_in_refusal: ‹X ∈ ℛ P ⟹ X ∪ - P⇧0 ∈ ℛ P›
  unfolding Refusals_iff by (erule is_processT5) (auto simp add: initials_def F_T)

lemma TickRightSync: 
  ‹✓(r) ∈ S ⟹ ftF u ⟹ t setinterleaves ((u, [✓(r)]), S) ⟹ t = u ∧ last u = ✓(r)›
  by (simp add: TickLeftSync setinterleaving_sym)

  

theorem Sync_is_Sync_restricted_superset_events:
  fixes S A :: ‹'a set› and P Q :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  assumes superset : ‹α(P) ∪ α(Q) ⊆ A›
  defines ‹S' ≡ S ∩ A›
  shows ‹P ⟦S⟧ Q = P ⟦S'⟧ Q›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 (P ⟦S⟧ Q) ⟹ s ∈ 𝒟 (P ⟦S'⟧ Q)› for s
    by (simp add: D_Sync S'_def)
       (metis Un_UNIV_left Un_commute equals0D events_of_is_strict_events_of_or_UNIV
              inf_top.right_neutral sup.orderE superset)
next
  show ‹s ∈ 𝒟 (P ⟦S'⟧ Q) ⟹ s ∈ 𝒟 (P ⟦S⟧ Q)› for s
    by (simp add: D_Sync S'_def)
       (metis Un_UNIV_left Un_commute equals0D events_of_is_strict_events_of_or_UNIV
              inf_top.right_neutral sup.orderE superset)
next
  let ?S  = ‹range tick ∪ ev ` S  :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
  and ?S' = ‹range tick ∪ ev ` S' :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
  fix s X
  assume same_div : ‹𝒟 (P ⟦S⟧ Q) = 𝒟 (P ⟦S'⟧ Q)›
  assume ‹(s, X) ∈ ℱ (P ⟦S'⟧ Q)›
  then consider ‹s ∈ 𝒟 (P ⟦S'⟧ Q)›
    | s_P X_P s_Q X_Q where ‹(rev s_P, X_P) ∈ ℱ P› ‹(rev s_Q, X_Q) ∈ ℱ Q›
                            ‹s setinterleaves ((rev s_P, rev s_Q), ?S')›
                            ‹X = (X_P ∪ X_Q) ∩ ?S' ∪ X_P ∩ X_Q›
    by (simp add: F_Sync D_Sync) (metis rev_rev_ident)
  thus ‹(s, X) ∈ ℱ (P ⟦S⟧ Q)›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 (P ⟦S'⟧ Q) ⟹ (s, X) ∈ ℱ (P ⟦S⟧ Q)› by blast
  next
    fix s_P s_Q and X_P X_Q :: ‹('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
    let ?X_P' = ‹X_P ∪ ev ` (- α(P))› and ?X_Q' = ‹X_Q ∪ ev ` (- α(Q))›
    assume assms : ‹(rev s_P, X_P) ∈ ℱ P› ‹(rev s_Q, X_Q) ∈ ℱ Q›
                   ‹s setinterleaves ((rev s_P, rev s_Q), ?S')›
                   ‹X = (X_P ∪ X_Q) ∩ ?S' ∪ X_P ∩ X_Q›
    
    from assms(1, 2)[THEN F_T] and assms(3)
    have assms_3_bis : ‹s setinterleaves ((rev s_P, rev s_Q), ?S)›
    proof (induct ‹(s_P, ?S, s_Q)› arbitrary: s_P s_Q s rule: setinterleaving.induct)
      case 1
      thus ‹s setinterleaves ((rev [], rev []), ?S)› by simp
    next
      case (2 y s_Q)
      from "2.prems"(3)[THEN doubleReverse] obtain s' b 
        where * : ‹y = ev b› ‹b ∉ S'› ‹s = rev (y # s')›
                  ‹s' setinterleaves (([], s_Q), ?S')›
        by (simp add: image_iff split: if_split_asm) (metis event⇩p⇩t⇩i⇩c⇩k.exhaust)
      from "2.prems"(2)[unfolded ‹y = ev b›]
      have ‹b ∈ α(Q)› by (force simp add: events_of_def)
      with ‹b ∉ S'› superset have ‹b ∉ S› by (simp add: S'_def subset_iff)
      from "2.prems"(2)[simplified, THEN is_processT3_TR] have ‹rev s_Q ∈ 𝒯 Q› by auto
      have ‹y ∉ ?S› by (simp add: "*"(1) ‹b ∉ S› image_iff)
      have ‹rev s' setinterleaves ((rev [], rev s_Q), ?S)›
        by (fact "2.hyps"[OF ‹y ∉ ?S› "2.prems"(1) ‹rev s_Q ∈ 𝒯 Q› "*"(4)[THEN doubleReverse]])
      from this[THEN addNonSync, OF ‹y ∉ ?S›]
      show ‹s setinterleaves ((rev [], rev (y # s_Q)), ?S)›
        by (simp add: ‹s = rev (y # s')›)
    next
      case (3 x s_P)
      from "3.prems"(3)[THEN doubleReverse] obtain s' a 
        where * : ‹x = ev a› ‹a ∉ S'› ‹s = rev (x # s')›
                  ‹s' setinterleaves ((s_P, []), ?S')›
        by (simp add: image_iff split: if_split_asm) (metis event⇩p⇩t⇩i⇩c⇩k.exhaust)
      from "3.prems"(1)[unfolded ‹x = ev a›]
      have ‹a ∈ α(P)› by (force simp add: events_of_def)
      with ‹a ∉ S'› superset have ‹a ∉ S› by (simp add: S'_def subset_iff)
      from "3.prems"(1)[simplified, THEN is_processT3_TR] have ‹rev s_P ∈ 𝒯 P› by auto
      have ‹x ∉ ?S› by (simp add: "*"(1) ‹a ∉ S› image_iff)
      have ‹rev s' setinterleaves ((rev s_P, rev []), ?S)›
        by (fact "3.hyps"[OF ‹x ∉ ?S› ‹rev s_P ∈ 𝒯 P› "3.prems"(2) "*"(4)[THEN doubleReverse]])
      from this[THEN addNonSync, OF ‹x ∉ ?S›]
      show ‹s setinterleaves ((rev (x # s_P), rev []), ?S)›
        by (simp add: ‹s = rev (x # s')›)
    next
      case (4 x s_P y s_Q)
      from "4.prems"(1)[simplified, THEN is_processT3_TR] have ‹rev s_P ∈ 𝒯 P› by auto
      from "4.prems"(2)[simplified, THEN is_processT3_TR] have ‹rev s_Q ∈ 𝒯 Q› by auto
      from "4.prems"(1) have ‹x ∈ range tick ∪ ev ` α(P)›
        by (cases x; force simp add: events_of_def image_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
      from "4.prems"(2) have ‹y ∈ range tick ∪ ev ` α(Q)›
        by (cases y; force simp add: events_of_def image_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
      consider ‹x ∈ ?S› and ‹y ∈ ?S› | ‹x ∈ ?S› and ‹y ∉ ?S›
        | ‹x ∉ ?S› and ‹y ∈ ?S› | ‹x ∉ ?S› and ‹y ∉ ?S› by blast
      thus ‹s setinterleaves ((rev (x # s_P), rev (y # s_Q)), ?S)›
      proof cases
        assume ‹x ∈ ?S› and ‹y ∈ ?S›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∈ ?S'› and ‹y ∈ ?S'› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse] obtain s'
        where * : ‹x = y› ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, s_Q), ?S')›
          by (simp split: if_split_asm) blast

        from "4.hyps"(1)[OF ‹x ∈ ?S› ‹y ∈ ?S› ‹x = y› ‹rev s_P ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                            ‹s' setinterleaves ((s_P, s_Q), ?S')›[THEN doubleReverse]]
        have ‹rev s' setinterleaves ((rev s_P, rev s_Q), ?S)› .
        from this[THEN doubleReverse] ‹x ∈ ?S›
        have ‹(x # s') setinterleaves ((x # s_P, x # s_Q), ?S)› by simp
        from this[THEN doubleReverse] show ?case by (simp add: "*"(1, 2))
      next
        assume ‹x ∈ ?S› and ‹y ∉ ?S›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∈ ?S'› and ‹y ∉ ?S'› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse, simplified] obtain s'
        where * : ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S')›
          by (simp split: if_split_asm) blast
        from "4.hyps"(2)[OF ‹x ∈ ?S› ‹y ∉ ?S› ‹rev (x # s_P) ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                            ‹s' setinterleaves ((x # s_P, s_Q), ?S')›[THEN doubleReverse]]
        have ‹rev s' setinterleaves ((rev (x # s_P), rev s_Q), ?S)› .
        from this[THEN doubleReverse] ‹x ∈ ?S› ‹y ∉ ?S›
        have ‹(y # s') setinterleaves ((x # s_P, y # s_Q), ?S)› by simp
        from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (y # s')›)
      next
        assume ‹x ∉ ?S› and ‹y ∈ ?S›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∉ ?S'› and ‹y ∈ ?S'› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse] obtain s'
        where * : ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S')›
          by (simp split: if_split_asm) blast
        from "4.hyps"(5)[OF ‹x ∉ ?S› _ ‹rev s_P ∈ 𝒯 P› ‹rev (y # s_Q) ∈ 𝒯 Q›
                            ‹s' setinterleaves ((s_P, y # s_Q), ?S')›[THEN doubleReverse]] ‹y ∈ ?S›
        have ‹rev s' setinterleaves ((rev s_P, rev (y # s_Q)), ?S)› by simp
        from this[THEN doubleReverse] ‹x ∉ ?S› ‹y ∈ ?S›
        have ‹(x # s') setinterleaves ((x # s_P, y # s_Q), ?S)› by simp
        from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (x # s')›)
      next
        assume ‹x ∉ ?S› and ‹y ∉ ?S›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)›
        have ‹x ∉ ?S'› and ‹y ∉ ?S'› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse, simplified] consider
          s' where ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S')›
        | s' where ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S')›
          by (simp split: if_split_asm) blast
        thus ?case
        proof cases
          fix s' assume ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S')›
          from "4.hyps"(3)[OF ‹x ∉ ?S› ‹y ∉ ?S› ‹rev s_P ∈ 𝒯 P› ‹rev (y # s_Q) ∈ 𝒯 Q›
                              ‹s' setinterleaves ((s_P, y # s_Q), ?S')›[THEN doubleReverse]]
          have ‹rev s' setinterleaves ((rev s_P, rev (y # s_Q)), ?S)› .
          from this[THEN doubleReverse] ‹x ∉ ?S› ‹y ∉ ?S›
          have ‹(x # s') setinterleaves ((x # s_P, y # s_Q), ?S)› by simp
          from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (x # s')›)
        next
          fix s' assume ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S')›
          from "4.hyps"(4)[OF ‹x ∉ ?S› ‹y ∉ ?S› ‹rev (x # s_P) ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                              ‹s' setinterleaves ((x # s_P, s_Q), ?S')›[THEN doubleReverse]]
          have ‹rev s' setinterleaves ((rev (x # s_P), rev s_Q), ?S)› .
          from this[THEN doubleReverse] ‹x ∉ ?S› ‹y ∉ ?S›
          have ‹(y # s') setinterleaves ((x # s_P, y # s_Q), ?S)› by simp
          from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (y # s')›)
        qed
      qed
    qed
  
    from add_complementary_events_of_in_failure[OF assms(1)]
    have ‹(rev s_P, ?X_P') ∈ ℱ P› .
    moreover from add_complementary_events_of_in_failure[OF assms(2)]
    have ‹(rev s_Q, ?X_Q') ∈ ℱ Q› .
    ultimately have ‹(s, (?X_P' ∪ ?X_Q') ∩ ?S ∪ ?X_P' ∩ ?X_Q') ∈ ℱ (P ⟦S⟧ Q)›
      using assms_3_bis by (simp add: F_Sync) blast
    moreover have ‹X ⊆ (?X_P' ∪ ?X_Q') ∩ ?S ∪ ?X_P' ∩ ?X_Q'›
      by (auto simp add: assms(4) S'_def image_iff)
    ultimately show ‹(s, X) ∈ ℱ (P ⟦S⟧ Q)› by (rule is_processT4)
  qed
next
  let ?S  = ‹range tick ∪ ev ` S  :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
  and ?S' = ‹range tick ∪ ev ` S' :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
  fix s X
  assume same_div : ‹𝒟 (P ⟦S⟧ Q) = 𝒟 (P ⟦S'⟧ Q)›
  assume ‹(s, X) ∈ ℱ (P ⟦S⟧ Q)›
  then consider ‹s ∈ 𝒟 (P ⟦S⟧ Q)›
    | s_P X_P s_Q X_Q where ‹(rev s_P, X_P) ∈ ℱ P› ‹(rev s_Q, X_Q) ∈ ℱ Q›
                            ‹s setinterleaves ((rev s_P, rev s_Q), ?S)›
                            ‹X = (X_P ∪ X_Q) ∩ ?S ∪ X_P ∩ X_Q›
    by (simp add: F_Sync D_Sync) (metis rev_rev_ident)
  thus ‹(s, X) ∈ ℱ (P ⟦S'⟧ Q)›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 (P ⟦S⟧ Q) ⟹ (s, X) ∈ ℱ (P ⟦S'⟧ Q)› by blast
  next
    fix s_P s_Q and X_P X_Q :: ‹('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
    let ?X_P' = ‹X_P ∪ ev ` (- α(P))› and ?X_Q' = ‹X_Q ∪ ev ` (- α(Q))›
    assume assms : ‹(rev s_P, X_P) ∈ ℱ P› ‹(rev s_Q, X_Q) ∈ ℱ Q›
                   ‹s setinterleaves ((rev s_P, rev s_Q), ?S)›
                   ‹X = (X_P ∪ X_Q) ∩ ?S ∪ X_P ∩ X_Q›
    
    from assms(1, 2)[THEN F_T] and assms(3)
    have assms_3_bis : ‹s setinterleaves ((rev s_P, rev s_Q), ?S')›
    proof (induct ‹(s_P, ?S', s_Q)› arbitrary: s_P s_Q s rule: setinterleaving.induct)
      case 1
      thus ‹s setinterleaves ((rev [], rev []), ?S')› by simp
    next
      case (2 y s_Q)
      from "2.prems"(3)[THEN doubleReverse] obtain s' b 
        where * : ‹y = ev b› ‹b ∉ S› ‹s = rev (y # s')›
                  ‹s' setinterleaves (([], s_Q), ?S)›
        by (simp add: image_iff split: if_split_asm) (metis event⇩p⇩t⇩i⇩c⇩k.exhaust)
      from "2.prems"(2)[unfolded ‹y = ev b›]
      have ‹b ∈ α(Q)› by (force simp add: events_of_def)
      with ‹b ∉ S› have ‹b ∉ S'› by (simp add: S'_def)
      from "2.prems"(2)[simplified, THEN is_processT3_TR] have ‹rev s_Q ∈ 𝒯 Q› by auto
      have ‹y ∉ ?S'› by (simp add: "*"(1) ‹b ∉ S'› image_iff)
      have ‹rev s' setinterleaves ((rev [], rev s_Q), ?S')›
        by (fact "2.hyps"[OF ‹y ∉ ?S'› "2.prems"(1) ‹rev s_Q ∈ 𝒯 Q› "*"(4)[THEN doubleReverse]])
      from this[THEN addNonSync, OF ‹y ∉ ?S'›]
      show ‹s setinterleaves ((rev [], rev (y # s_Q)), ?S')›
        by (simp add: ‹s = rev (y # s')›)
    next
      case (3 x s_P)
      from "3.prems"(3)[THEN doubleReverse] obtain s' a 
        where * : ‹x = ev a› ‹a ∉ S› ‹s = rev (x # s')›
                  ‹s' setinterleaves ((s_P, []), ?S)›
        by (simp add: image_iff split: if_split_asm) (metis event⇩p⇩t⇩i⇩c⇩k.exhaust)
      from "3.prems"(1)[unfolded ‹x = ev a›]
      have ‹a ∈ α(P)› by (force simp add: events_of_def)
      with ‹a ∉ S› have ‹a ∉ S'› by (simp add: S'_def)
      from "3.prems"(1)[simplified, THEN is_processT3_TR] have ‹rev s_P ∈ 𝒯 P› by auto
      have ‹x ∉ ?S'› by (simp add: "*"(1) ‹a ∉ S'› image_iff)
      have ‹rev s' setinterleaves ((rev s_P, rev []), ?S')›
        by (fact "3.hyps"[OF ‹x ∉ ?S'› ‹rev s_P ∈ 𝒯 P› "3.prems"(2) "*"(4)[THEN doubleReverse]])
      from this[THEN addNonSync, OF ‹x ∉ ?S'›]
      show ‹s setinterleaves ((rev (x # s_P), rev []), ?S')›
        by (simp add: ‹s = rev (x # s')›)
    next
      case (4 x s_P y s_Q)
      from "4.prems"(1)[simplified, THEN is_processT3_TR] have ‹rev s_P ∈ 𝒯 P› by auto
      from "4.prems"(2)[simplified, THEN is_processT3_TR] have ‹rev s_Q ∈ 𝒯 Q› by auto
      from "4.prems"(1) have ‹x ∈ range tick ∪ ev ` α(P)›
        by (cases x; force simp add: events_of_def image_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
      from "4.prems"(2) have ‹y ∈ range tick ∪ ev ` α(Q)›
        by (cases y; force simp add: events_of_def image_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
      consider ‹x ∈ ?S'› and ‹y ∈ ?S'› | ‹x ∈ ?S'› and ‹y ∉ ?S'›
        | ‹x ∉ ?S'› and ‹y ∈ ?S'› | ‹x ∉ ?S'› and ‹y ∉ ?S'› by blast
      thus ‹s setinterleaves ((rev (x # s_P), rev (y # s_Q)), ?S')›
      proof cases
        assume ‹x ∈ ?S'› and ‹y ∈ ?S'›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)›
        have ‹x ∈ ?S› and ‹y ∈ ?S› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse] obtain s'
        where * : ‹x = y› ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, s_Q), ?S)›
          by (simp split: if_split_asm) blast

        from "4.hyps"(1)[OF ‹x ∈ ?S'› ‹y ∈ ?S'› ‹x = y› ‹rev s_P ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                            ‹s' setinterleaves ((s_P, s_Q), ?S)›[THEN doubleReverse]]
        have ‹rev s' setinterleaves ((rev s_P, rev s_Q), ?S')› .
        from this[THEN doubleReverse] ‹x ∈ ?S'›
        have ‹(x # s') setinterleaves ((x # s_P, x # s_Q), ?S')› by simp
        from this[THEN doubleReverse] show ?case by (simp add: "*"(1, 2))
      next
        assume ‹x ∈ ?S'› and ‹y ∉ ?S'›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∈ ?S› and ‹y ∉ ?S› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse, simplified] obtain s'
        where * : ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S)›
          by (simp split: if_split_asm) blast
        from "4.hyps"(2)[OF ‹x ∈ ?S'› ‹y ∉ ?S'› ‹rev (x # s_P) ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                            ‹s' setinterleaves ((x # s_P, s_Q), ?S)›[THEN doubleReverse]]
        have ‹rev s' setinterleaves ((rev (x # s_P), rev s_Q), ?S')› .
        from this[THEN doubleReverse] ‹x ∈ ?S'› ‹y ∉ ?S'›
        have ‹(y # s') setinterleaves ((x # s_P, y # s_Q), ?S')› by simp
        from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (y # s')›)
      next
        assume ‹x ∉ ?S'› and ‹y ∈ ?S'›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∉ ?S› and ‹y ∈ ?S› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse] obtain s'
        where * : ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S)›
          by (simp split: if_split_asm) blast
        from "4.hyps"(5)[OF ‹x ∉ ?S'› _ ‹rev s_P ∈ 𝒯 P› ‹rev (y # s_Q) ∈ 𝒯 Q›
                            ‹s' setinterleaves ((s_P, y # s_Q), ?S)›[THEN doubleReverse]] ‹y ∈ ?S'›
        have ‹rev s' setinterleaves ((rev s_P, rev (y # s_Q)), ?S')› by simp
        from this[THEN doubleReverse] ‹x ∉ ?S'› ‹y ∈ ?S'›
        have ‹(x # s') setinterleaves ((x # s_P, y # s_Q), ?S')› by simp
        from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (x # s')›)
      next
        assume ‹x ∉ ?S'› and ‹y ∉ ?S'›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∉ ?S› and ‹y ∉ ?S› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse, simplified] consider
          s' where ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S)›
        | s' where ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S)›
          by (simp split: if_split_asm) blast
        thus ?case
        proof cases
          fix s' assume ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S)›
          from "4.hyps"(3)[OF ‹x ∉ ?S'› ‹y ∉ ?S'› ‹rev s_P ∈ 𝒯 P› ‹rev (y # s_Q) ∈ 𝒯 Q›
                              ‹s' setinterleaves ((s_P, y # s_Q), ?S)›[THEN doubleReverse]]
          have ‹rev s' setinterleaves ((rev s_P, rev (y # s_Q)), ?S')› .
          from this[THEN doubleReverse] ‹x ∉ ?S'› ‹y ∉ ?S'›
          have ‹(x # s') setinterleaves ((x # s_P, y # s_Q), ?S')› by simp
          from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (x # s')›)
        next
          fix s' assume ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S)›
          from "4.hyps"(4)[OF ‹x ∉ ?S'› ‹y ∉ ?S'› ‹rev (x # s_P) ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                              ‹s' setinterleaves ((x # s_P, s_Q), ?S)›[THEN doubleReverse]]
          have ‹rev s' setinterleaves ((rev (x # s_P), rev s_Q), ?S')› .
          from this[THEN doubleReverse] ‹x ∉ ?S'› ‹y ∉ ?S'›
          have ‹(y # s') setinterleaves ((x # s_P, y # s_Q), ?S')› by simp
          from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (y # s')›)
        qed
      qed
    qed
  
    from add_complementary_events_of_in_failure[OF assms(1)]
    have ‹(rev s_P, ?X_P') ∈ ℱ P› .
    moreover from add_complementary_events_of_in_failure[OF assms(2)]
    have ‹(rev s_Q, ?X_Q') ∈ ℱ Q› .
    ultimately have ‹(s, (?X_P' ∪ ?X_Q') ∩ ?S' ∪ ?X_P' ∩ ?X_Q') ∈ ℱ (P ⟦S'⟧ Q)›
      using assms_3_bis by (simp add: F_Sync) blast
    moreover from superset have ‹X ⊆ (?X_P' ∪ ?X_Q') ∩ ?S' ∪ ?X_P' ∩ ?X_Q'›
      by (auto simp add: assms(4) S'_def image_iff)
    ultimately show ‹(s, X) ∈ ℱ (P ⟦S'⟧ Q)› by (rule is_processT4)
  qed
qed

corollary Sync_is_Sync_restricted_events : ‹P ⟦S⟧ Q = P ⟦S ∩ (α(P) ∪ α(Q))⟧ Q›
  by (simp add: Sync_is_Sync_restricted_superset_events)

text ‹This version is closer to the intuition that we may have, but the first one would be more
useful if we don't want to compute the events of a process but know a superset approximation.›


(* lemma Sync_with_SKIP_eq_itself_if_disjoint_events:
  ‹α(P) ∩ S = {} ⟹ P ⟦S⟧ SKIP r = P›
  oops
  by (metis Int_commute Inter_SKIP Sync_is_Sync_restricted_events events_Inter)

lemma Sync_with_STOP_eq_itself_Seq_STOP_if_disjoint_events:
  ‹α(P) ∩ S = {} ⟹ P ⟦S⟧ STOP = P ❙; (λr. STOP)›
  oops
  by (metis Int_Un_eq(3) Int_commute Inter_STOP_Seq_STOP Sync_is_Sync_restricted_events events_STOP) *)


corollary ‹deadlock_free P ⟹ deadlock_free Q ⟹
           S ∩ (α(P) ∪ α(Q)) = {} ⟹ deadlock_free (P ⟦S⟧ Q)›
  by (subst Sync_is_Sync_restricted_events) (simp add: Inter_deadlock_free)
    (* but we already had this with data_independence_deadlock_free_Sync *)






section ‹Powerful Results about \<^const>‹Renaming››

text ‹In this section we will provide laws about the \<^const>‹Renaming› operator.
      In the first subsection we will give slight generalizations of previous results,
      but in the other we prove some very powerful theorems.›

subsection ‹Some Generalizations›

text ‹For \<^const>‹Renaming›, we can obtain generalizations of the following results:

      @{thm Renaming_Mprefix[no_vars] Renaming_Mndetprefix[no_vars]}›



lemma Renaming_Mprefix_Sliding:
  ‹Renaming ((□a ∈ A → P a) ⊳ Q) f g = 
   (□y ∈ f ` A → ⊓a ∈ {x ∈ A. y = f x}. Renaming (P a) f g) ⊳ Renaming Q f g›
  unfolding Sliding_def
  by (simp add: Renaming_Det Renaming_distrib_Ndet Renaming_Mprefix)





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
    by (simp add: "*", simp add: image_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
       (metis event⇩p⇩t⇩i⇩c⇩k.simps(9))
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
    by (metis bij_betw_imp_inj_on bij_f bij_g event⇩p⇩t⇩i⇩c⇩k.inj_map inj_eq inj_onI)
  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
    by (metis bij_betw_def bij_f bij_g event⇩p⇩t⇩i⇩c⇩k.inj_map inj_on_inverseI inv_f_eq surj_imp_inj_inv)
  show ‹?lhs = ?rhs›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    then obtain s1 s2 where * : ‹tF s1› ‹ftF 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 ** : ‹ftF u› ‹tF t› ‹s1 = trace_hide t (ev ` S) @ u›
                 ‹t ∈ 𝒟 P ∨ (∃g. isInfHiddenRun g P S ∧ t ∈ range g)›
      by (simp add: D_Hiding) blast
    from "**"(4) show ‹s ∈ 𝒟 ?rhs›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 P›
      hence ‹ftF (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u @ s2) ∧ tF (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 (rule trace_hide_map_map_event⇩p⇩t⇩i⇩c⇩k[symmetric])
         apply (meson inj_def inj_onCI inj_on_map_event⇩p⇩t⇩i⇩c⇩k)
        apply (simp add: D_Renaming)
        using "**"(2) front_tickFree_Nil by blast
      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 ‹ftF (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u @ s2) ∧
             tF (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 * : ‹ftF u› ‹tF 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 ** : ‹tF t1› ‹ftF t2› 
                                   ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1 @ t2› ‹t1 ∈ 𝒟 P›
        by (simp add: D_Renaming) blast
      have ‹tF (trace_hide t1 (ev ` S)) ∧ 
            ftF (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 UNIV_I bij_betw_inv_into_left bij_f bij_g event⇩p⇩t⇩i⇩c⇩k.exhaust event⇩p⇩t⇩i⇩c⇩k.map(2) event⇩p⇩t⇩i⇩c⇩k.simps(9))
      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 ‹tF t1› ‹ftF 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 ‹tF (trace_hide t1 (ev ` S)) ∧ ftF 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 **** : ‹tF t1› ‹ftF t2›
                                ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t1 @ t2› ‹t1 ∈ 𝒟 P›
        have ‹tF (trace_hide t1 (ev ` S)) ∧
              ftF (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 ** : ‹ftF u› ‹tF 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 *** : ‹ftF (map (map_event⇩p⇩t⇩i⇩c⇩k f g) u) ∧ tF (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 (simp add: set_eq_iff map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff image_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 (simp add: set_eq_iff map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff image_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. tF s1 ∧ ftF 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 ‹tF s1› ‹ftF s2› ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹s1 ∈ 𝒟 P›
        hence ‹tF (trace_hide s1 (ev ` S)) ∧ 
               ftF (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 map_antecedent_if_subset_rangeE :
  assumes ‹set u ⊆ range f›
  obtains t where ‹u = map f t›
  ― ‹In particular, when \<^term>‹f› is surjective or bijective.›
proof -
  from ‹set u ⊆ range f› have ‹∃t. u = map f t›
  proof (induct u)
    show ‹∃t. [] = map f t› by simp
  next
    fix a u
    assume prem : ‹set (a # u) ⊆ range f›
       and  hyp : ‹set u ⊆ range f ⟹ ∃t. u = map f t›
    then obtain t where * : ‹u = map f t› 
      by (meson set_subset_Cons subset_trans)
    from prem obtain x where ** : ‹f x = a› by auto
    show ‹∃t. a # u = map f t›
    proof (intro exI)
      show ‹a # u = map f (x # t)› by (simp add: "*" "**")
    qed
  qed
  with that show thesis by blast
qed


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 -
  ― ‹Some intermediate results.›
  have map_event⇩p⇩t⇩i⇩c⇩k_inv_comp_map_event⇩p⇩t⇩i⇩c⇩k : ‹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_comp_map_event⇩p⇩t⇩i⇩c⇩k :
      ‹(map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g) ∘ map_event⇩p⇩t⇩i⇩c⇩k f g) t = id t› for t
      by (induct t, simp_all) (metis bij_f bij_inv_eq_iff, metis bij_g bij_inv_eq_iff)
  qed
  have map_event⇩p⇩t⇩i⇩c⇩k_comp_map_event⇩p⇩t⇩i⇩c⇩k_inv : ‹map_event⇩p⇩t⇩i⇩c⇩k f g ∘ map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g) = id›
    proof (rule ext)
    show map_event⇩p⇩t⇩i⇩c⇩k_inv_comp_map_event⇩p⇩t⇩i⇩c⇩k :
      ‹(map_event⇩p⇩t⇩i⇩c⇩k f g ∘ map_event⇩p⇩t⇩i⇩c⇩k (inv f) (inv g)) t = id t› for t
      by (induct t, simp_all) (metis bij_f bij_inv_eq_iff, metis bij_g bij_inv_eq_iff)
  qed
  from map_event⇩p⇩t⇩i⇩c⇩k_inv_comp_map_event⇩p⇩t⇩i⇩c⇩k map_event⇩p⇩t⇩i⇩c⇩k_comp_map_event⇩p⇩t⇩i⇩c⇩k_inv o_bij
  have bij_map_event⇩p⇩t⇩i⇩c⇩k : ‹bij (map_event⇩p⇩t⇩i⇩c⇩k f g)› by blast
  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 (simp add: inv_equality map_event⇩p⇩t⇩i⇩c⇩k_comp_map_event⇩p⇩t⇩i⇩c⇩k_inv map_event⇩p⇩t⇩i⇩c⇩k_inv_comp_map_event⇩p⇩t⇩i⇩c⇩k pointfree_idE)
  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: set_eq_iff image_iff tick_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff ev_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
       (metis UNIV_I Un_iff bij_betw_def bij_g image_iff, blast)
  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 * : ‹tF s1› ‹ftF 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 ** : ‹ftF v› ‹tF 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 ‹tF 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 * : ‹ftF v› ‹tF 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› ‹tF s1› ‹ftF 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 ‹tF r›)
        assume ‹tF 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 ‹tF r› 
                    append.right_neutral append_same_eq front_tickFree_Nil)
      next
        assume ‹¬ tF r›
        then obtain r' res where $ : ‹r = r' @ [✓(res)]› ‹tF 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 (no_types) "$"(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 ‹¬ tF 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 ‹tF 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


section ‹\<^const>‹Hiding› and \<^const>‹Mprefix››

text ‹We already have a way to distribute the \<^const>‹Hiding› operator on the
      \<^const>‹Mprefix› operator with @{thm Hiding_Mprefix_disjoint[of S A]}.
      But this is only usable when \<^term>‹A ∩ S = {}›. With the \<^const>‹Sliding›
      operator, we can now handle the case \<^term>‹A ∩ S ≠ {}›.›

subsection ‹\<^const>‹Hiding› and \<^const>‹Mprefix› for disjoint Sets›

text ‹This is a result similar to @{thm Hiding_Mprefix_disjoint}
      when we add a \<^const>‹Sliding› in the expression.›

theorem Hiding_Mprefix_Sliding_disjoint:
  ‹((□a ∈ A → P a) ⊳ Q) \ S = (□a ∈ A → (P a \ S)) ⊳ (Q \ S)›
  if disjoint: ‹A ∩ S = {}›
proof (subst Hiding_Mprefix_disjoint[OF disjoint, symmetric])
  show ‹((□a ∈ A → P a) ⊳ Q) \ S = (□a ∈ A → P a \ S) ⊳ (Q \ S)›
   (is ‹?lhs = ?rhs›)
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    hence ‹s ∈ 𝒟 (Mprefix A P ⊓ Q \ S)›
      by (simp add: D_Hiding D_Sliding D_Ndet T_Sliding T_Ndet)
    thus ‹s ∈ 𝒟 ?rhs›
      by (rule set_rev_mp) (simp add: D_Ndet D_Sliding Hiding_distrib_Ndet)
  next
    fix s
    assume ‹s ∈ 𝒟 ?rhs›
    hence ‹s ∈ 𝒟 (Q \ S) ∨ s ∈ 𝒟 (□a ∈ A → P a \ S)›
      by (simp add: Hiding_Mprefix_disjoint[OF disjoint]
                    D_Ndet D_Sliding) blast
    thus ‹s ∈ 𝒟 ?lhs›
      by (auto simp add: D_Hiding D_Sliding T_Sliding)
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?lhs›
    then consider ‹s ∈ 𝒟 ?lhs›
      |‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)›
      by (simp add: F_Hiding D_Hiding) blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
    next
      assume ‹∃t. s = trace_hide t (ev ` S) ∧
                  (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)›
      then obtain t
        where * : ‹s = trace_hide t (ev ` S)›
                  ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)› by blast
      from "*"(2) consider ‹(t, X ∪ ev ` S) ∈ ℱ Q›
        | ‹t ≠ []› ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        by (simp add: F_Sliding D_Mprefix) blast
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        have ‹(t, X ∪ ev ` S) ∈ ℱ Q ⟹ (s, X) ∈ ℱ (Q \ S)›
          by (auto simp add: F_Hiding "*"(1))
        thus ‹(t, X ∪ ev ` S) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?rhs›
          by (simp add: F_Ndet F_Sliding "*"(1))
      next
        assume assms : ‹t ≠ []› ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        with disjoint have ‹trace_hide t (ev ` S) ≠ []›
          by (cases t, auto simp add: F_Mprefix)
        also have ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
          using assms by (auto simp: F_Hiding "*"(1))
        ultimately show ‹(s, X) ∈ ℱ ?rhs›
          by (simp add: F_Sliding "*"(1))
      qed
    qed
  next
    have * : ‹t ∈ 𝒯 (Mprefix A P) ⟹ trace_hide t (ev ` S) = [] ⟷ t = []› for t
      using disjoint by (cases t, auto simp add: T_Mprefix)
    have ** : ‹[] ∉ 𝒟 (Mprefix A P \ S)›
      apply (rule ccontr, simp add: D_Hiding, elim exE conjE disjE)
      by (use "*" D_T Nil_notin_D_Mprefix in blast)
         (metis (no_types, lifting) "*" UNIV_I f_inv_into_f old.nat.distinct(2) strict_mono_on_eqD)
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?rhs›
    with ** consider ‹(s, X) ∈ ℱ (Q \ S)›
      | ‹s ≠ []› ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
      by (simp add: Hiding_Mprefix_disjoint[OF disjoint] F_Sliding D_Mprefix) blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹(s, X) ∈ ℱ (Q \ S)›
      then consider ‹s ∈ 𝒟 (Q \ S)›
        | ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ Q›
        by (simp add: F_Hiding D_Hiding) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (Q \ S)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Ndet D_Sliding)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ Q›
        thus ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Hiding F_Sliding) blast
      qed
    next
      assume assms : ‹s ≠ []› ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
      then consider ‹s ∈ 𝒟 (Mprefix A P \ S)›
        | ‹∃t. t ≠ [] ∧ s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        by (simp add: F_Hiding D_Hiding) (metis filter.simps(1))
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (Mprefix A P \ S)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Ndet D_Sliding)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        show ‹∃t. t ≠ [] ∧ s = trace_hide t (ev ` S) ∧
                  (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P) ⟹ (s, X) ∈ ℱ ?lhs›
          by (auto simp add: F_Sliding F_Hiding)
      qed
    qed
  qed
qed




subsection ‹\<^const>‹Hiding› and \<^const>‹Mprefix› for non-disjoint Sets›

text ‹Finally the new version, when \<^term>‹A ∩ S ≠ {}›.›

― ‹Just a small lemma to understand why the nonempty hypothesis is necessary.›
lemma ‹∃A :: nat set. ∃P S.
       A ∩ S = {} ∧ □a ∈ A → P a \ S ≠ 
       (□a ∈ (A - S) → (P a \ S)) ⊳ (⊓a ∈ (A ∩ S). (P a \ S))›
proof (intro exI)
  show ‹{0} ∩ {Suc 0} = {} ∧ 
        □a ∈ {0} → SKIP undefined \ {Suc 0} ≠ 
        (□a ∈ ({0} - {Suc 0}) → (SKIP undefined \ {Suc 0})) ⊳ (⊓a ∈ ({0} ∩ {Suc 0}). (SKIP undefined \ {Suc 0}))›
    apply (simp add: write0_def[symmetric] Hiding_write0_disjoint)
    using UNIV_I list.discI by (auto simp add: Process_eq_spec write0_def F_Ndet
                                               F_Mprefix F_Sliding F_STOP set_eq_iff)
qed


text ‹This is a result similar to @{thm Hiding_Mprefix_non_disjoint}
      when we add a \<^const>‹Sliding› in the expression.›

lemma Hiding_Mprefix_Sliding_non_disjoint:
  ‹(□a ∈ A → P a) ⊳ Q \ S = (□a ∈ (A - S) → (P a \ S)) ⊳ 
                              (Q \ S) ⊓ (⊓a ∈ (A ∩ S). (P a \ S))›
  if non_disjoint: ‹A ∩ S ≠ {}›
proof (subst Sliding_distrib_Ndet_left,
       subst Hiding_Mprefix_non_disjoint[OF non_disjoint, symmetric])
  show ‹Mprefix A P ⊳ Q \ S =
        ((□a ∈ (A - S) → (P a \ S)) ⊳ (Q \ S)) ⊓ (□a ∈ A → P a \ S)›
   (is ‹?lhs = ?rhs›)
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    hence ‹s ∈ 𝒟 (Mprefix A P ⊓ Q \ S)›
      by (simp add: D_Hiding D_Sliding D_Ndet T_Sliding T_Ndet)
    thus ‹s ∈ 𝒟 ?rhs›
      by (rule set_rev_mp)
         (simp add: D_Ndet D_Sliding Hiding_distrib_Ndet subsetI)
  next
    fix s
    assume ‹s ∈ 𝒟 ?rhs›
    hence ‹s ∈ 𝒟 (Q \ S) ∨ s ∈ 𝒟 (□a ∈ A → P a \ S)›
      by (simp add: Hiding_Mprefix_non_disjoint[OF non_disjoint]
                    D_Ndet D_Sliding) blast
    thus ‹s ∈ 𝒟 ?lhs›
      by (auto simp add: D_Hiding D_Sliding T_Sliding)
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?lhs›
    then consider ‹s ∈ 𝒟 ?lhs›
      |‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)›
      by (simp add: F_Hiding D_Hiding) blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
    next
      assume ‹∃t. s = trace_hide t (ev ` S) ∧
                  (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)›
      then obtain t
        where * : ‹s = trace_hide t (ev ` S)›
                  ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)› by blast
      from "*"(2) consider ‹(t, X ∪ ev ` S) ∈ ℱ Q›
        | ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        by (simp add: F_Sliding D_Mprefix) blast
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        have ‹(t, X ∪ ev ` S) ∈ ℱ Q ⟹ (s, X) ∈ ℱ (Q \ S)›
          by (auto simp add: F_Hiding "*"(1))
        thus ‹(t, X ∪ ev ` S) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?rhs›
          by (simp add: F_Ndet F_Sliding "*"(1))
      next
        assume ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        hence ‹(s, X) ∈ ℱ (Mprefix A P \ S)› by (auto simp: F_Hiding "*"(1))
        thus ‹(s, X) ∈ ℱ ?rhs› by (simp add: F_Ndet "*"(1))
      qed
    qed
  next
    fix s X
    have * : ‹s ≠ [] ⟹ (s, X) ∈ ℱ (□a ∈ (A - S) → (P a \ S)) ⟹ 
                          (s, X) ∈ ℱ (□a ∈ A → P a \ S)›
      by (simp add: Hiding_Mprefix_non_disjoint[OF non_disjoint] F_Sliding)
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?rhs›
    with "*" consider ‹(s, X) ∈ ℱ (Q \ S)› | ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
      by (auto simp add: F_Ndet F_Sliding)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹(s, X) ∈ ℱ (Q \ S)›
      then consider ‹s ∈ 𝒟 (Q \ S)›
        | ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ Q›
        by (simp add: F_Hiding D_Hiding) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (Q \ S)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Ndet D_Sliding)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ Q›
        thus ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Hiding F_Sliding) blast
      qed
    next
      assume ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
      then consider ‹s ∈ 𝒟 (Mprefix A P \ S)›
        | ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        by (simp add: F_Hiding D_Hiding) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (Mprefix A P \ S)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Ndet D_Sliding)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        then obtain t where * : ‹s = trace_hide t (ev ` S)›
                                ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)› by blast
        from "*"(2) non_disjoint have ‹t ≠ []› by (simp add: F_Mprefix) blast
        with "*" show ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Hiding F_Sliding) blast
      qed
    qed
  qed
qed
       


section ‹\<^const>‹Sliding› behaviour›

text ‹We already proved several laws for the \<^const>‹Sliding› operator.
      Here we give other results in the same spirit as
      @{thm [source] Hiding_Mprefix_Sliding_disjoint} and
      @{thm [source] Hiding_Mprefix_Sliding_non_disjoint}.›

lemma Mprefix_Sliding_Mprefix_Sliding:
  ‹(□a ∈ A → P a) ⊳ (□b ∈ B → Q b) ⊳ R =
   (□ x ∈ (A ∪ B) → (if x ∈ A ∩ B then P x ⊓ Q x else if x ∈ A then P x else Q x)) ⊳ R›
  (is ‹(□a ∈ A → P a) ⊳ (□b ∈ B → Q b) ⊳ R = ?term ⊳ R›)
proof (subst Sliding_def, subst Mprefix_Det_Mprefix)
  have ‹Mprefix B Q ⊓ (Mprefix A P □ Mprefix B Q) ⊳ R = Mprefix A P □ Mprefix B Q ⊳ R›
    by (metis (no_types, opaque_lifting) Det_assoc Det_commute Ndet_commute
              Ndet_distrib_Det_left Ndet_id Sliding_Det Sliding_assoc Sliding_def)
  thus ‹?term ⊓ Mprefix B Q ⊳ R = ?term ⊳ R›
    by (simp add: Mprefix_Det_Mprefix Ndet_commute)
qed


lemma Mprefix_Sliding_Seq: 
  ‹(□a ∈ A → P a) ⊳ P' ❙; Q = (□a ∈ A → (P a ❙; Q)) ⊳ (P' ❙; Q)›
proof (subst Mprefix_Seq[symmetric])
  show ‹((□a ∈ A → P a) ⊳ P') ❙; Q = 
        ((□a ∈ A → P a) ❙; Q) ⊳ (P' ❙; Q)› (is ‹?lhs = ?rhs›)
  proof (subst Process_eq_spec, safe)
    show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
      by (simp add: D_Sliding D_Seq T_Sliding) blast
  next
    show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
      by (auto simp add: D_Sliding D_Seq T_Sliding)
  next
    show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
      by (cases s; simp add: F_Sliding D_Sliding T_Sliding F_Seq) metis
  next
    show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
      by (cases s; simp add: F_Sliding D_Sliding T_Sliding
                             F_Seq D_Seq T_Seq D_Mprefix T_Mprefix)
         (metis event⇩p⇩t⇩i⇩c⇩k.simps(4) hd_append list.sel(1), blast)
  qed
qed



lemma Throw_Sliding :
  ‹(□a ∈ A → P a) ⊳ P' Θ b ∈ B. Q b = 
   (□a ∈ A → (if a ∈ B then Q a else P a Θ b ∈ B. Q b)) ⊳ (P' Θ b ∈ B. Q b)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then consider t1 t2 where ‹s = t1 @ t2› ‹t1 ∈ 𝒟 (Mprefix A P ⊳ P')›
                            ‹tF t1› ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
    | t1 b t2 where ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P')›
                    ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
    by (simp add: D_Throw) blast
  thus ‹s ∈ 𝒟 ?rhs›
  proof cases
    fix t1 t2 assume * : ‹s = t1 @ t2› ‹t1 ∈ 𝒟 (Mprefix A P ⊳ P')› ‹tF t1›
                         ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
    from "*"(2) consider ‹t1 ∈ 𝒟 (Mprefix A P)› | ‹t1 ∈ 𝒟 P'›
      by (simp add: D_Sliding) blast
    thus ‹s ∈ 𝒟 ?rhs›
    proof cases
      assume ‹t1 ∈ 𝒟 (Mprefix A P)›
      then obtain a t1' where ‹t1 = ev a # t1'› ‹a ∈ A› ‹t1' ∈ 𝒟 (P a)›
        by (auto simp add: D_Mprefix image_iff)
      with "*"(1, 3, 4, 5) show ‹s ∈ 𝒟 ?rhs›
        by (simp add: D_Sliding D_Mprefix D_Throw) (metis image_eqI)
    next
      from "*"(1, 3, 4, 5)  show ‹t1 ∈ 𝒟 P' ⟹ s ∈ 𝒟 ?rhs›
        by (simp add: D_Sliding D_Throw) blast
    qed
  next
    fix t1 b t2 assume * : ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P')›
                           ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
    from "*"(2) consider ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P)› | ‹t1 @ [ev b] ∈ 𝒯 P'›
      by (simp add: T_Sliding) blast
    thus ‹s ∈ 𝒟 ?rhs›
    proof cases
      assume ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P)›
      then obtain a t1'
        where ‹t1 @ [ev b] = ev a # t1'› ‹a ∈ A› ‹t1' ∈ 𝒯 (P a)›
        by (auto simp add: T_Mprefix)
      with "*"(1, 3, 4, 5) show ‹s ∈ 𝒟 ?rhs›
        by (cases t1; simp add: "*"(1) D_Sliding D_Mprefix D_Throw)
           (metis image_eqI)
    next
      from "*"(1, 3, 4, 5) show ‹t1 @ [ev b] ∈ 𝒯 P' ⟹ s ∈ 𝒟 ?rhs›
        by (simp add: D_Sliding D_Mprefix D_Throw) blast
    qed
  qed
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then consider ‹s ∈ 𝒟 (Throw P' B Q)›
    | ‹s ∈ 𝒟 (□a∈A → (if a ∈ B then Q a else Throw (P a) B Q))›
    by (simp add: D_Sliding) blast
  thus ‹s ∈ 𝒟 ?lhs›
  proof cases
    show ‹s ∈ 𝒟 (Throw P' B Q) ⟹ s ∈ 𝒟 ?lhs›
      by (simp add: D_Throw D_Sliding T_Sliding) blast
  next
    assume ‹s ∈ 𝒟 (□a∈A → (if a ∈ B then Q a else Throw (P a) B Q))›
    then obtain a s' 
      where * : ‹s = ev a # s'› ‹a ∈ A›
                ‹s' ∈ 𝒟 (if a ∈ B then Q a else Throw (P a) B Q)›
      by (cases s; simp add: D_Mprefix) blast
    show ‹s ∈ 𝒟 ?lhs›
    proof (cases ‹a ∈ B›)
      from "*" show ‹a ∈ B ⟹ s ∈ 𝒟 ?lhs›
        by (simp add: D_Throw T_Sliding T_Mprefix disjoint_iff)
           (metis Nil_elem_T emptyE empty_set self_append_conv2)
    next
      assume ‹a ∉ B›
      with "*"(3) consider 
        t1 t2 where ‹s' = t1 @ t2› ‹t1 ∈ 𝒟 (P a)› ‹tF t1›
                    ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
        | t1 b t2 where ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
                        ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
        by (simp add: D_Throw) blast
      thus ‹s ∈ 𝒟 ?lhs›
      proof cases
        fix t1 t2 assume ** : ‹s' = t1 @ t2› ‹t1 ∈ 𝒟 (P a)› ‹tF t1›
                              ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
        have *** : ‹s = (ev a # t1) @ t2 ∧ set (ev a # t1) ∩ ev ` B = {}›
          by (simp add: "*"(1) "**"(1, 4) image_iff ‹a ∉ B›)
        from "*" "**"(1, 2, 3, 5) show ‹s ∈ 𝒟 ?lhs›
          by (simp add: D_Throw D_Sliding D_Mprefix image_iff)
             (metis "***" event⇩p⇩t⇩i⇩c⇩k.disc(1) tickFree_Cons_iff)
      next
        fix t1 b t2 assume ** : ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
                                ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
        have *** : ‹s = (ev a # t1 @ [ev b]) @ t2 ∧ set (ev a # t1) ∩ ev ` B = {}›
          by (simp add: "*"(1) "**"(1, 3) image_iff ‹a ∉ B›)
        from "*" "**"(1, 2, 4, 5) show ‹s ∈ 𝒟 ?lhs›
          by (simp add: D_Throw T_Sliding T_Mprefix) (metis "***" Cons_eq_appendI)
      qed
    qed
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | ‹(s, X) ∈ ℱ (Mprefix A P ⊳ P')› ‹set s ∩ ev ` B = {}›
    | t1 b t2 where ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P')›
                    ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
    by (auto simp add: F_Throw D_Throw)
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  next
    show ‹(s, X) ∈ ℱ (Mprefix A P ⊳ P') ⟹ set s ∩ ev ` B = {} ⟹ (s, X) ∈ ℱ ?rhs›
      by (cases s; simp add: F_Sliding F_Mprefix F_Throw) blast
  next
    fix t1 b t2 assume * : ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P')›
                           ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
    from "*"(2) consider ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P)› | ‹t1 @ [ev b] ∈ 𝒯 P'›
      by (simp add: T_Sliding) blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      assume ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P)›
      then obtain a t1'
        where ‹t1 @ [ev b] = ev a # t1'› ‹a ∈ A› ‹t1' ∈ 𝒯 (P a)›
        by (auto simp add: T_Mprefix)
      with "*"(1, 3, 4, 5) show ‹(s, X) ∈ ℱ ?rhs›
        by (cases t1; simp add: "*"(1) F_Sliding F_Mprefix F_Throw) blast
    next
      from "*"(1, 3, 4, 5) show ‹t1 @ [ev b] ∈ 𝒯 P' ⟹ (s, X) ∈ ℱ ?rhs›
        by (simp add: F_Sliding F_Mprefix F_Throw) blast
    qed
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?rhs›
  then consider ‹s ∈ 𝒟 ?rhs› | ‹(s, X) ∈ ℱ (Throw P' B Q)›
    | ‹s ≠ []› ‹(s, X) ∈ ℱ (□a ∈ A → (if a ∈ B then Q a else Throw (P a) B Q))›
    by (simp add: F_Sliding D_Sliding) blast
  thus ‹(s, X) ∈ ℱ ?lhs›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
  next
    show ‹(s, X) ∈ ℱ (Throw P' B Q) ⟹ (s, X) ∈ ℱ ?lhs›
      by (simp add: F_Throw F_Sliding D_Sliding T_Sliding) blast
  next
    assume ‹s ≠ []› ‹(s, X) ∈ ℱ (□a ∈ A → (if a ∈ B then Q a else Throw (P a) B Q))›
    then obtain a s'
      where * : ‹s = ev a # s'› ‹a ∈ A› 
                ‹(s', X) ∈ ℱ (if a ∈ B then Q a else Throw (P a) B Q)›
      by (auto simp add: F_Mprefix image_iff)
    show ‹(s, X) ∈ ℱ ?lhs›
    proof (cases ‹a ∈ B›)
      assume ‹a ∈ B›
      have ‹[ev a] ∈ 𝒯 (Mprefix A P ⊳ P')›
        by (simp add: T_Sliding T_Mprefix "*"(2))
      with "*"(1, 3) ‹a ∈ B› show ‹(s, X) ∈ ℱ ?lhs›
        by (simp add: F_Throw) (metis append_Nil empty_set inf_bot_left)
    next
      assume ‹a ∉ B›
      with "*"(3) consider ‹s' ∈ 𝒟 (Throw (P a) B Q)›
        | ‹(s', X) ∈ ℱ (P a)› ‹set s' ∩ ev ` B = {}›
        | t1 b t2 where ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
                        ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
        by (auto simp add: F_Throw D_Throw)
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s' ∈ 𝒟 (Throw (P a) B Q)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: "*"(1, 2) D_Sliding D_Mprefix ‹a ∉ B›)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        show ‹(s', X) ∈ ℱ (P a) ⟹ set s' ∩ ev ` B = {} ⟹ (s, X) ∈ ℱ ?lhs›
          using "*"(1, 2) ‹a ∉ B› by (simp add: F_Throw F_Sliding F_Mprefix) blast
      next
        fix t1 b t2 assume ** : ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
                                ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
        from "**" have *** : ‹(ev a # t1) @ [ev b] ∈ 𝒯 (Mprefix A P) ∧ 
                              set (ev a # t1) ∩ ev ` B = {}›
          by (simp add: T_Mprefix "*"(2) image_iff ‹a ∉ B›)
        from "*"(1) "**"(1, 4, 5) "**"(5) show ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Throw T_Sliding) (metis "***" Cons_eq_appendI)
      qed
    qed
  qed
qed



section ‹Dealing with \<^const>‹SKIP››

lemma Renaming_Mprefix_Det_SKIP:
  ‹Renaming ((□ a ∈ A → P a) □ SKIP r) f g =
   (□y∈f ` A → ⊓ a ∈ {x ∈ A. y = f x}. Renaming (P a) f g) □ SKIP (g r)›
  (* TODO: remove Renaming_Mprefix from CSP_Laws, or change the name *)
  by (simp add: Renaming_Det Renaming_Mprefix)


lemma Mprefix_Sliding_SKIP_Seq: ‹((□ a ∈ A → P a) ⊳ SKIP r) ❙; Q = (□ a ∈ A → (P a ❙; Q)) ⊳ Q›
  (* TODO: see if we leave Sliding_SKIP in simp *)
  by (simp del: Sliding_SKIP add: Mprefix_Sliding_Seq)

lemma Mprefix_Det_SKIP_Seq: ‹((□ a ∈ A → P a) □ SKIP r) ❙; Q = (□ a ∈ A → (P a ❙; Q)) ⊳ Q›
  by (fold Sliding_SKIP) (fact Mprefix_Sliding_SKIP_Seq)


lemma Sliding_Ndet_pseudo_assoc : ‹(P ⊳ Q) ⊓ R = P ⊳ Q ⊓ R›
  by (metis Ndet_assoc Ndet_distrib_Det_right Ndet_id Sliding_def)

lemma Hiding_Mprefix_Det_SKIP:
  ‹(□ a ∈ A → P a) □ SKIP r \ S =
   (if A ∩ S = {} then (□ a ∈ A → (P a \ S)) □ SKIP r
    else ((□ a ∈ (A - S) → (P a \ S)) □ SKIP r) ⊓ (⊓ a ∈ (A ∩ S). (P a \ S)))›
  by (fold Sliding_SKIP)
     (simp del: Sliding_SKIP add: Hiding_Mprefix_Sliding_disjoint
           Hiding_Mprefix_Sliding_non_disjoint Sliding_Ndet_pseudo_assoc)


lemma ‹s ≠ [] ⟹ (s, X) ∈ ℱ (P □ Q) ⟷ (s, X) ∈ ℱ (P ⊓ Q)›
  by (simp add: F_Det F_Ndet)



lemma Mprefix_Det_SKIP_Sync_SKIP :
  ‹((□ a ∈ A → P a) □ SKIP res) ⟦S⟧ SKIP res' = 
   (if res = res' then (□ a ∈ (A - S) → (P a ⟦S⟧ SKIP res')) □ SKIP res'
    else (□ a ∈ (A - S) → (P a ⟦S⟧ SKIP res')) ⊓ STOP)›
  (is ‹?lhs = (if res = res' then ?rhs1 else ?rhs2)›)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then obtain a t u r v
    where * : ‹ftF v› ‹tF r ∨ v = []› ‹s = r @ v›
              ‹r setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
              ‹a ∈ A› ‹t ∈ 𝒟 (P a)› ‹u ∈ 𝒯 (SKIP res')›
    by (simp add: D_Sync D_SKIP D_Det D_Mprefix T_SKIP image_iff) blast
  from "*"(3, 4, 5, 7) have ** : ‹a ∈ A - S› ‹s = ev a # tl r @ v›
                                 ‹tl r setinterleaves ((t, u), range tick ∪ ev ` S)›
    by (auto simp add: image_iff T_SKIP split: if_split_asm)
  have ‹tl s ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
    by (simp add: D_Sync)
       (metis "*"(1, 2, 6, 7) "**"(2, 3) list.sel(3) tickFree_tl)
  with "**"(1) show ‹s ∈ 𝒟 (if res = res' then ?rhs1 else ?rhs2)›
    by (simp add: D_Det D_Ndet D_Mprefix "**"(2))
next
  fix s
  assume ‹s ∈ 𝒟 (if res = res' then ?rhs1 else ?rhs2)›
  then obtain a s' where * : ‹s = ev a # s'› ‹a ∈ A - S› ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
    by (auto simp add: D_Det D_Ndet D_SKIP D_STOP D_Mprefix image_iff split: if_split_asm)
  then obtain t u r v
    where ** : ‹ftF v› ‹tF r ∨ v = []› ‹s' = r @ v›
               ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
               ‹t ∈ 𝒟 (P a)› ‹u ∈ 𝒯 (SKIP res')›
    by (simp add: D_Sync D_SKIP) blast
  have ‹(ev a # r) setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
    using "*"(2) "**"(4, 6) by (auto simp add: T_SKIP)
  with "*"(2) "**"(1, 2, 3, 5, 6) show ‹s ∈ 𝒟 ?lhs›
    by (simp add: D_Sync D_SKIP D_Det D_Mprefix T_SKIP image_iff)
       (metis (no_types, opaque_lifting) "*"(1) Cons_eq_appendI event⇩p⇩t⇩i⇩c⇩k.disc(1) tickFree_Cons_iff)
next
  fix s Z
  assume same_div : ‹𝒟 ?lhs = 𝒟 (if res = res' then ?rhs1 else ?rhs2)›
  assume ‹(s, Z) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | t u X Y where ‹(t, X) ∈ ℱ (Mprefix A P □ SKIP res)› ‹(u, Y) ∈ ℱ (SKIP res')›
                    ‹s setinterleaves ((t, u), range tick ∪ ev ` S)›
                    ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
    by (simp add: F_Sync D_Sync) blast
  thus ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)› by blast
  next
    fix t u X Y
    assume * : ‹(t, X) ∈ ℱ (Mprefix A P □ SKIP res)› ‹(u, Y) ∈ ℱ (SKIP res')›
               ‹s setinterleaves ((t, u), range tick ∪ ev ` S)›
               ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›    
    from "*"(1) consider ‹t = []› | ‹t = [✓(res)]› | a t' where ‹t = ev a # t'›
      by (auto simp add: F_Det F_SKIP F_Mprefix)
    thus ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
    proof cases
      assume ‹t = []›
      with "*"(2, 3) have ‹s = []› by (auto simp add: F_SKIP)
      with ‹t = []› "*"(3)[simplified ‹t = []›, THEN emptyLeftProperty] "*"(1, 2, 3, 4)
      show ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
        by (auto simp add: F_Det F_Ndet F_Mprefix F_STOP F_SKIP D_SKIP T_SKIP)
    next
      assume ‹t = [✓(res)]›
      with "*"(2, 3) have ‹res' = res ∧ s = [✓(res)]›
        by (cases u; auto simp add: F_SKIP split: if_split_asm)
      with ‹t = [✓(res)]› show ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
        by (simp add: F_Det F_Ndet F_STOP F_SKIP)      
    next
      fix a t' assume ‹t = ev a # t'›
      with "*"(1, 2, 3) empty_setinterleaving obtain s'
        where ** : ‹s' setinterleaves ((t', u), range tick ∪ ev ` S)›
                   ‹s = ev a # s'› ‹(t', X) ∈ ℱ (P a)› ‹a ∈ A - S›
        by (auto simp add: F_SKIP F_Det F_Mprefix image_iff split: if_split_asm)
      from "*"(2, 4) "**"(1, 3) have ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res')›
        by (simp add: F_Sync) blast  
      with "**"(4) show ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
        by (simp add: F_Det F_Ndet ‹s = ev a # s'› F_SKIP F_Mprefix)
    qed
  qed
next
  fix s Z
  assume same_div : ‹𝒟 ?lhs = 𝒟 (if res = res' then ?rhs1 else ?rhs2)›
  assume ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
  then consider ‹res = res'› ‹(s, Z) ∈ ℱ ?rhs1›
    | ‹res ≠ res'› ‹(s, Z) ∈ ℱ ?rhs2› by presburger
  thus ‹(s, Z) ∈ ℱ ?lhs›
  proof cases
    assume ‹res = res'› ‹(s, Z) ∈ ℱ ?rhs1›
    then consider ‹s = []› | ‹s = [✓(res')]› | a s' where ‹s = ev a # s'›
      by (auto simp add: F_Det F_SKIP F_Mprefix)
    thus ‹(s, Z) ∈ ℱ ?lhs›
    proof cases
      assume ‹s = []›
      with ‹(s, Z) ∈ ℱ ?rhs1› have ‹tick res' ∉ Z›
        by (auto simp add: F_Det F_Mprefix F_SKIP D_SKIP T_SKIP)
      with ‹s = []› show ‹(s, Z) ∈ ℱ ?lhs›
        by (simp add: F_Sync F_Det T_SKIP F_SKIP ‹res = res'›)
           (metis Int_Un_eq(3) si_empty1 Un_Int_eq(4) Un_commute insertI1)
    next
      assume ‹s = [✓(res')]›
      hence * : ‹([✓(res')], Z) ∈ ℱ (Mprefix A P □ SKIP res') ∧ 
                 s setinterleaves (([✓(res')], [✓(res')]), range tick ∪ ev ` S) ∧ 
                 ([✓(res')], Z) ∈ ℱ (SKIP res') ∧ Z = (Z ∪ Z) ∩ (range tick ∪ ev ` S) ∪ Z ∩ Z›
        by (simp add: F_Det F_SKIP)
      show ‹(s, Z) ∈ ℱ ?lhs› by (simp add: F_Sync ‹res = res'›) (meson "*")
    next
      fix a s' assume ‹s = ev a # s'›
      with ‹(s, Z) ∈ ℱ ?rhs1› have * : ‹a ∈ A› ‹a ∉ S› ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res')›
        by (simp_all add: F_Det F_SKIP F_Mprefix image_iff)
      from "*"(3) consider ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
        | t u X Y where ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res')›
                        ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
                        ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
        by (simp add: F_Sync D_Sync) blast
      thus ‹(s, Z) ∈ ℱ ?lhs›
      proof cases
        assume ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
        hence ‹s ∈ 𝒟 ?rhs1›
          by (simp add: D_Det D_Mprefix image_iff "*"(1, 2) ‹s = ev a # s'›)
        with same_div show ‹(s, Z) ∈ ℱ ?lhs› by (simp add: ‹res = res'› is_processT8)
      next
        fix t u X Y assume ** : ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res')›
                                ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
                                ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
        from "**"(2, 3) have ‹(ev a # s') setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
          by (auto simp add: "*"(1, 2) F_SKIP image_iff)
        thus ‹(s, Z) ∈ ℱ ?lhs›
          by (simp add: F_Sync F_Det F_Mprefix image_iff)
             (metis "*"(1) "**"(1, 2, 4) ‹s = ev a # s'› list.distinct(1))
      qed
    qed
  next
    assume ‹res ≠ res'› ‹(s, Z) ∈ ℱ ?rhs2›
    then consider ‹s = []›
      | a s' where ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res')›
      by (auto simp add: F_Ndet F_STOP F_Mprefix)
    thus ‹(s, Z) ∈ ℱ ?lhs›
    proof cases
      have ‹([], UNIV) ∈ ℱ ?lhs›
        apply (simp add: F_Sync, rule disjI1)
        apply (rule_tac x = ‹[]› in exI, simp add: F_Det F_Mprefix F_SKIP T_SKIP D_SKIP)
        apply (rule_tac x = ‹[]› in exI, rule_tac x = ‹UNIV - {✓(res)}› in exI)
        apply (simp, rule_tac x = ‹UNIV - {✓(res')}› in exI)
        using ‹res ≠ res'› by auto
      thus ‹s = [] ⟹ (s, Z) ∈ ℱ ?lhs› by (auto intro: is_processT4)
    next
      fix a s' assume * : ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res')›
      from "*"(4) consider ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
        | t u X Y where ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res')›
                        ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
                        ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
        by (auto simp add: F_Sync D_Sync)
      thus ‹(s, Z) ∈ ℱ ?lhs›
      proof cases
        assume ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
        hence ‹s ∈ 𝒟 ?rhs2› by (simp add: "*"(1, 2, 3) D_Ndet D_Mprefix)
        with same_div show ‹(s, Z) ∈ ℱ ?lhs› by (simp add: ‹res ≠ res'› is_processT8)
      next
        fix t u X Y assume ** : ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res')›
                                ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
                                ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
        show ‹(s, Z) ∈ ℱ ?lhs›
          apply (simp add: F_Sync, rule disjI1)
          apply (rule_tac x = ‹ev a # t› in exI)
          apply (rule_tac x = u in exI)
          apply (rule_tac x = X in exI)
          apply (rule conjI, solves ‹simp add: F_Det F_Mprefix "*"(1) "**"(1)›)
          apply (rule_tac x = Y in exI)
          apply (simp add: "**"(2, 4))
          using "**"(2, 3) by (auto simp add: "*"(1, 2, 3) F_SKIP)
      qed
    qed
  qed
qed


lemma Sliding_def_bis : ‹P ⊳ Q = (P ⊓ Q) □ Q›
  by (simp add: Det_distrib_Ndet_right Sliding_def)





  
(* 
lemma Sliding_Sync : ‹P ⊳ Q ⟦S⟧ R = (P ⟦S⟧ R) ⊳ (Q ⟦S⟧ R) ⊓ (P ⊳ Q ⟦S⟧ R)›
  
  sorry

lemma Sync_Sliding : ‹P ⟦S⟧ Q ⊳ R = (P ⟦S⟧ Q) ⊳ (P ⟦S⟧ R) ⊓ (P ⟦S⟧ Q ⊳ R)›
  by (metis Sliding_Sync Sync_commute) *)


(* lemma Sliding_Sync_Sliding :
  ‹P ⊳ Q ⟦B⟧ R ⊳ S = (P ⟦B⟧ R) ⊳ ((Q ⟦B⟧ R ⊳ S) ⊓ (P ⊳ Q ⟦B⟧ S))›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (simp add: D_Sync, elim exE conjE disjE)
       (simp add: D_Sync D_Sliding D_Ndet T_Sliding, use front_tickFree_Nil in blast)+
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (simp add: D_Sliding D_Ndet, elim disjE)
       (simp add: D_Sync D_Sliding T_Sliding, blast)+
next
  fix s Z
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, Z) ∈ ℱ ?lhs›
  with F_T setinterleaving_sym front_tickFree_Nil consider ‹s ∈ 𝒟 ?lhs›
    | ‹∃t u X Y. (t, X) ∈ ℱ (P ⊳ Q) ∧ t ∉ 𝒟 P ∧ (u, Y) ∈ ℱ (R ⊳ S) ∧ u ∉ 𝒟 R ∧
                 s setinterleaves ((t, u), insert tick (ev ` B)) ∧
                 Z = (X ∪ Y) ∩ insert tick (ev ` B) ∪ X ∩ Y›
    by (simp add: F_Sync D_Sync D_Sliding, blast)
  thus ‹(s, Z) ∈ ℱ ?rhs›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, Z) ∈ ℱ ?rhs› by blast
  next
    assume ‹∃t u X Y. (t, X) ∈ ℱ (P ⊳ Q) ∧ t ∉ 𝒟 P ∧ (u, Y) ∈ ℱ (R ⊳ S) ∧ u ∉ 𝒟 R ∧
                      s setinterleaves ((t, u), insert tick (ev ` B)) ∧
                      Z = (X ∪ Y) ∩ insert tick (ev ` B) ∪ X ∩ Y›
    then obtain t u X Y
      where * : ‹(t, X) ∈ ℱ (P ⊳ Q)› ‹t ∉ 𝒟 P› ‹(u, Y) ∈ ℱ (R ⊳ S)› ‹u ∉ 𝒟 R›
                ‹s setinterleaves ((t, u), insert tick (ev ` B))›
                ‹Z = (X ∪ Y) ∩ insert tick (ev ` B) ∪ X ∩ Y› by blast
    from "*"(1, 2, 3, 4)
    have ‹(t, X) ∈ ℱ Q ∨ t ≠ [] ∧ (t, X) ∈ ℱ P ∨ t = [] ∧ tick ∉ X ∧ [tick] ∈ 𝒯 P›
     and ‹(u, Y) ∈ ℱ S ∨ u ≠ [] ∧ (u, Y) ∈ ℱ R ∨ u = [] ∧ tick ∉ Y ∧ [tick] ∈ 𝒯 R›
      by (auto simp add: F_Sliding)
    with "*"(5, 6) show ‹(s, Z) ∈ ℱ ?rhs›
      apply (elim disjE; simp add: F_Sliding F_Ndet F_Sync )
              apply (metis+)[5]
         apply (metis empty_setinterleaving)
        apply (metis empty_setinterleaving is_processT6_S2)
      apply (metis emptyLeftProperty is_processT6_S2)
      by (simp add: T_Sync) (metis "*"(5) addSync insertCI self_append_conv2)
  qed
next
  fix s Z
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, Z) ∈ ℱ ?rhs› 
  then consider ‹s ∈ 𝒟 ?rhs› | ‹(s, Z) ∈ ℱ ?rhs› ‹s ∉ 𝒟 ?rhs› by fast
  thus ‹(s, Z) ∈ ℱ ?lhs›
  proof cases
    oops *)
  
  
  (* 
  
  oops


  show ‹(s, Z) ∈ ℱ ?rhs ⟹ (s, Z) ∈ ℱ ?lhs›
    apply (rule ccontr)
    apply (auto simp add: F_Sync F_Sliding F_Ndet D_Sliding D_Ndet T_Sliding)
                        apply metis+
                        apply (metis append.right_neutral front_tickFree_Nil)+
     defer apply 
    apply (metis append.right_neutral front_tickFree_Nil)+ 
    apply (metis BOT_iff_D Nil_elem_T Sync.si_empty1 Sync_is_BOT_iff insertCI)+

    apply (auto simp add: T_Sync)

    sledgehammer defer sledgehammer defer sledgehammer
    apply (metis T_Sliding Un_iff) defer sledgehammer defer sledgehammer
  then consider ‹(s, Z) ∈ ℱ (Q ⟦B⟧ R ⊳ S)› | ‹(s, Z) ∈ ℱ (P ⊳ Q ⟦B⟧ S)›
    | ‹s ≠ []› ‹(s, Z) ∈ ℱ (P ⟦B⟧ R)› ‹(s, Z) ∉ ℱ (Q ⟦B⟧ R ⊳ S)› ‹(s, Z) ∉ ℱ (P ⊳ Q ⟦B⟧ S)›
    | ‹s = []› ‹(s ∈ 𝒟 (P ⟦B⟧ R) ∨ tick ∉ Z ∧ [tick] ∈ 𝒯 (P ⟦B⟧ R))›
    by (simp add: F_Sliding F_Ndet) blast
  thus ‹(s, Z) ∈ ℱ ?lhs›
  proof cases
    show ‹(s, Z) ∈ ℱ (Q ⟦B⟧ R ⊳ S) ⟹ (s, Z) ∈ ℱ ?lhs›
      by (simp add: F_Sync F_Sliding T_Sliding D_Sliding; elim disjE; metis)
  next
    show ‹(s, Z) ∈ ℱ (P ⊳ Q ⟦B⟧ S) ⟹ (s, Z) ∈ ℱ ?lhs›
      by (simp add: F_Sync F_Sliding T_Sliding D_Sliding; elim disjE; metis)
  next
    assume assms : ‹s ≠ []› ‹(s, Z) ∈ ℱ (P ⟦B⟧ R)›
      ‹(s, Z) ∉ ℱ (Q ⟦B⟧ R ⊳ S)› ‹(s, Z) ∉ ℱ (P ⊳ Q ⟦B⟧ S)›
    from assms(2) consider ‹s ∈ 𝒟 (P ⟦B⟧ R)›
      | ‹∃t u X Y. (t, X) ∈ ℱ P ∧ (u, Y) ∈ ℱ R ∧
                   s setinterleaves ((t, u), insert tick (ev ` B)) ∧
                   Z = (X ∪ Y) ∩ insert tick (ev ` B) ∪ X ∩ Y›
      by (simp add: F_Sync D_Sync) blast
    thus ‹(s, Z) ∈ ℱ ?lhs›
    proof cases
      assume ‹s ∈ 𝒟 (P ⟦B⟧ R)›
      hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Sliding)
      with same_div D_F show ‹(s, Z) ∈ ℱ ?lhs› by blast
    next
      assume ‹∃t u X Y. (t, X) ∈ ℱ P ∧ (u, Y) ∈ ℱ R ∧
                        s setinterleaves ((t, u), insert tick (ev ` B)) ∧
                        Z = (X ∪ Y) ∩ insert tick (ev ` B) ∪ X ∩ Y›
      then obtain t u X Y
        where * : ‹(t, X) ∈ ℱ P› ‹(u, Y) ∈ ℱ R›
                  ‹s setinterleaves ((t, u), insert tick (ev ` B))›
                  ‹Z = (X ∪ Y) ∩ insert tick (ev ` B) ∪ X ∩ Y› by blast
    (*   from "*"(1, 2) have ‹(t, X) ∈ ℱ (P ⊳ Q)› and ‹(u, Y) ∈ ℱ (R ⊳ S)›
        apply (auto simp add: F_Sliding) *)
      
      from "*"(3) ‹s ≠ []›
      consider ‹t ≠ []› ‹u ≠ []› | ‹t = []› ‹u = s› | ‹t = s› ‹u = []›
        by (metis setinterleaving_sym emptyLeftProperty)
      thus ‹(s, Z) ∈ ℱ ?lhs›
      proof cases
        assume ‹t ≠ []› and ‹u ≠ []›
        with "*"(1, 2) have ‹(t, X) ∈ ℱ (P ⊳ Q)› and ‹(u, Y) ∈ ℱ (R ⊳ S)› 
          by (simp_all add: F_Sliding)
        with "*"(3, 4) show ‹(s, Z) ∈ ℱ ?lhs› by (simp add: F_Sync) blast
      next
        assume ‹t = []› and ‹u = s›
        with "*"(2) ‹s ≠ []› have ‹(u, Y) ∈ ℱ (R ⊳ S)› by (simp add: F_Sliding)
        have ‹(t, X) ∉ ℱ Q›
        proof (rule ccontr)
          assume ‹¬ (t, X) ∉ ℱ Q›
          with "*"(3, 4) ‹(u, Y) ∈ ℱ (R ⊳ S)› have ‹(s, Z) ∈ ℱ (Q ⟦B⟧ R ⊳ S)›
            by (simp add: F_Sync) blast
          with assms(3) show False by simp
        qed
        from assms(4) "*"(3, 4) consider ‹(t, X) ∉ ℱ (P ⊳ Q)› | ‹(u, Y) ∉ ℱ S›
          by (simp add: F_Sync) blast
        thus ‹(s, Z) ∈ ℱ ?lhs›
        proof cases
          assume ‹(t, X) ∉ ℱ (P ⊳ Q)›
          hence ** : ‹([], X) ∉ ℱ Q› ‹[] ∉ 𝒟 P› ‹tick ∈ X ∨ [tick] ∉ 𝒯 P›
            by (simp_all add: F_Sliding ‹(t, X) ∉ ℱ Q› ‹t = []›)
          thus ‹(s, Z) ∈ ℱ ?lhs›
            apply (simp add: F_Sync)
            apply (rule disjI1)
            apply (auto simp add: F_Sliding) sledgehammer
            sorry
        next
          show ‹(u, Y) ∉ ℱ S ⟹ (s, Z) ∈ ℱ (P ⊳ Q ⟦B⟧ R ⊳ S)›
            apply (simp add: F_Sync)
          thm this[simplified F_Sliding, simplified, simplified ]

          oops
          apply (simp add: F_Sync)
          apply (rule disjI1)
          apply (rule_tac x = ‹[]› in exI, rule_tac x = u in exI, rule_tac x = ‹{}› in exI)
          apply (simp add: is_processT1)
          apply (rule_tac x = ‹Z ∪ insert tick (ev ` B)› in exI, intro conjI)
            apply (intro conjI)
          sledgehammer
          apply (meson ‹(u, Y) ∈ ℱ (R ⊳ S)› inf_sup_ord(1) is_processT4)
            apply (meson ‹(u, Y) ∈ ℱ (R ⊳ S)› inf_sup_ord(1) is_processT4)
defer sledgehammer defer 
          sledgehammer
          using "*"(3) ‹t = []› apply blast
          using is_processT1 apply blast


          thm F_Sliding


        oops
          using  by blast
      from "*"(3) ‹s ≠ []› have ‹t ≠ [] ∧ u ≠ []›
        apply (cases t; cases u; simp split: if_split_asm) sledgehammer
      thus ‹(s, Z) ∈ ℱ ?lhs›
        
        apply (simp add: F_Sync)
        apply (rule disjI1)
    thm this[simplified F_Sync, simplified]


     apply (simp add: F_Sync F_Sliding, elim conjE disjE, rule disjI1) sledgehammer


    oops
    apply (simp add: F_Sync D_Sliding T_Sliding F_Sliding, elim conjE disjE exE) sledgehammer
    sorry
qed


      oops

  then consider ‹s ∈ 𝒟 (P ⟦B⟧ R)› | ‹s ∈ 𝒟 (Q ⟦B⟧ R ⊳ S)› | ‹s ∈ 𝒟 (P ⊳ Q ⟦B⟧ S)›
    by (simp add: D_Sliding D_Ndet) blast
  thus ‹s ∈ 𝒟 (?lhs P Q R S)›
  proof cases
    show ‹s ∈ 𝒟 (P ⟦B⟧ R) ⟹ s ∈ 𝒟 (P ⊳ Q ⟦B⟧ R ⊳ S)›
      by (simp add: D_Sync D_Sliding T_Sliding) blast
  next
    show ‹s ∈ 𝒟 (Q ⟦B⟧ R ⊳ S) ⟹ s ∈ 𝒟 (P ⊳ Q ⟦B⟧ R ⊳ S)›
      by (simp add: D_Sync D_Sliding T_Sliding) blast
  next
    
  thm this[simplified D_Sliding, simplified]
  

    thm "**"[of u t]

    oops
    sledgehammer
    sorry
 *)
 

(* 
lemma Sliding_Sync_Mprefix :
  ‹P ⊳ Q ⟦S⟧ (□a ∈ A → R a) =
   □ a ∈ A - S → ((P ⊳ Q) ⟦S⟧ R a) □ ((P ⟦S⟧ (□a ∈ A → R a)) ⊳ (Q ⟦S⟧ (□a ∈ A → R a)))›
  (is ‹?lhs = ?rhs›)
  oops
   

 *)

(* 

section ‹Global Non-Deterministic Choice›

lemma GlobalNdet_Mprefix_distr:
  ‹A ≠ {} ⟹ (⊓ a ∈ A. □ b ∈ B → P a b) = □ b ∈ B → (⊓ a ∈ A. P a b)›
  by (auto simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet F_Mprefix D_Mprefix)

lemma GlobalNdet_Mprefix :
  ‹(⊓ a∈A. □ b ∈ B a → P a b) = (if A = {} then STOP else
   (⊓ a∈A. □ b ∈ B a - (⋃a'∈{a'∈A. a' ≠ a}. B a') → P a b)
   □ (□ b ∈ (⋂a∈A. B a) → ⊓a∈A. P a b))›
  (is ‹?lhs = (if A = {} then STOP else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹A = {} ⟹ ?lhs = STOP› by (simp add: GlobalNdet.abs_eq STOP.abs_eq)
next
  show ‹?lhs = ?rhs› if ‹A ≠ {}›
  proof (subst Process_eq_spec, safe)
    show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
      apply (auto simp add: ‹A ≠ {}› D_Det D_GlobalNdet D_Mprefix)
      sledgehammer

  apply (auto simp add: Process_eq_spec F_GlobalNdet F_Det)
 *)

(*<*)
end 
(*>*)