Theory Synchronization_Product_Generalized

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


chapter ‹Generalization of the Synchronization Product›

(*<*)
theory  Synchronization_Product_Generalized
  imports "HOL-CSP"
begin
  (*>*)

section ‹Trace Interleaving›

subsection ‹Motivation›

text ‹
The notion of trace interleaving found in session‹HOL-CSP›
does not allow us to precisely handle termination.
Indeed, as soon as term‹r ≠ s›, we cannot have
term‹t setinterleaves (([✓(r)], [✓(s)]), range tick ∪ ev ` A)›.
›


lemma ‹r ≠ s ⟹ ¬ t setinterleaves (([✓(r)], [✓(s)]), range tick ∪ ev ` A)› by simp

text ‹
The actual issue of this previous definition is that no distinction is done
between the ``regular'' events (like term‹ev a›) and the terminations (like term‹✓(r)›).
Here, while we still want the same behaviour for regular events, we want instead
the interleaving of term‹✓(r)› and term‹✓(s)› to be term‹✓((r, s))›.
But we would also like this interleaving to generalize the old one,
i.e. be able to prevent sometimes two ticks from being combined.
Our solution is therefore to rely on a parameter:
term‹tick_join› of type typ‹'r ⇒ 's ⇒ 't option› whose role is to specify how
two ticks can be combined (or not).
›


bundle option_type_syntax
begin

no_notation floor   (‹(‹open_block notation=‹mixfix floor››⌊_⌋)›)
no_notation ceiling (‹(‹open_block notation=‹mixfix ceiling››⌈_⌉)›)

notation Some       (‹(‹open_block notation=‹mixfix Some››⌊_⌋)›)
notation the        (‹(‹open_block notation=‹mixfix the››⌈_⌉)›)
notation None       (‹◇›)

end

unbundle option_type_syntax



subsection ‹Definition›


type_synonym ('a, 'r, 's, 't) setinterleavingptick_args =
  ‹('r ⇒ 's ⇒ 't option) × ('a, 'r) traceptick × 'a set × ('a, 's) traceptick›

fun setinterleavingptick ::
  ‹('a, 'r, 's, 't) setinterleavingptick_args ⇒ ('a, 't) traceptick set›
  where Nil_setinterleavingptick_Nil :
    ‹setinterleavingptick (tick_join, [], A, []) = {[]}›

|       ev_setinterleavingptick_Nil :
  ‹setinterleavingptick (tick_join, ev a # u, A, []) =
   (  if a ∈ A then {}
    else {ev a # t| t. t ∈ setinterleavingptick (tick_join, u, A, [])})›
|       tick_setinterleavingptick_Nil :
  ‹setinterleavingptick (tick_join, ✓(r) # u, A, []) = {}›

|       Nil_setinterleavingptick_ev :
  ‹setinterleavingptick (tick_join, [], A, ev b # v) =
   (  if b ∈ A then {}
    else {ev b # t| t. t ∈ setinterleavingptick (tick_join, [], A, v)})›
|       Nil_setinterleavingptick_tick  :
  ‹setinterleavingptick (tick_join, [], A, ✓(s) # v) = {}›

|       ev_setinterleavingptick_ev : 
  ‹setinterleavingptick (tick_join, ev a # u, A, ev b # v) =
   (  if a ∈ A
    then    if b ∈ A 
          then   if a = b
               then {ev a # t |t. t ∈ setinterleavingptick (tick_join, u, A, v)}
               else {}
          else {ev b # t |t. t ∈ setinterleavingptick (tick_join, ev a # u, A, v)}
     else   if b ∈ A
          then {ev a # t |t. t ∈ setinterleavingptick (tick_join, u, A, ev b # v)}
          else {ev a # t |t. t ∈ setinterleavingptick (tick_join, u, A, ev b # v)} ∪
               {ev b # t |t. t ∈ setinterleavingptick (tick_join, ev a # u, A, v)})›
|       ev_setinterleavingptick_tick :
  ‹setinterleavingptick (tick_join, ev a # u, A, ✓(s) # v) =
   (  if a ∈ A then {}
    else {ev a # t |t. t ∈ setinterleavingptick (tick_join, u, A, ✓(s) # v)})›
|       tick_setinterleavingptick_ev :
  ‹setinterleavingptick (tick_join, ✓(r) # u, A, ev b # v) =
   (  if b ∈ A then {}
    else {ev b # t |t. t ∈ setinterleavingptick (tick_join, ✓(r) # u, A, v)})›
|       tick_setinterleavingptick_tick :
  ‹setinterleavingptick (tick_join, ✓(r) # u, A, ✓(s) # v) =
  (case tick_join r s
   of ⌊r_s⌋ ⇒ {✓(r_s) # t |t. t ∈ setinterleavingptick (tick_join, u, A, v)}
      |  ◇ ⇒ {})›


lemmas setinterleavingptick_induct
  [case_names Nil_setinterleavingptick_Nil ev_setinterleavingptick_Nil
    tick_setinterleavingptick_Nil Nil_setinterleavingptick_ev
    Nil_setinterleavingptick_tick ev_setinterleavingptick_ev
    ev_setinterleavingptick_tick tick_setinterleavingptick_ev
    tick_setinterleavingptick_tick,
    induct type: setinterleavingptick_args] = setinterleavingptick.induct



lemma Cons_setinterleavingptick_Nil :
  ‹setinterleavingptick (tick_join, e # u, A, []) =
   (case e of ev a ⇒
    (  if a ∈ A then {}
     else {ev a # t |t. t ∈ setinterleavingptick (tick_join, u, A, [])})
            | ✓(r) ⇒ {})›
  by (cases e) simp_all

lemma Nil_setinterleavingptick_Cons :
  ‹setinterleavingptick (tick_join, [], A, e # v) =
   (case e of ev a ⇒
    (  if a ∈ A then {}
     else {ev a # t |t. t ∈ setinterleavingptick (tick_join, [], A, v)})
            | ✓(r) ⇒ {})›
  by (cases e) simp_all

lemma Cons_setinterleavingptick_Cons :
  ‹setinterleavingptick (tick_join, e # u, A, f # v) =
   (case e of ev a ⇒
    (case f of ev b ⇒ 
       if a ∈ A
     then   if b ∈ A 
           then   if a = b
                then {ev a # t |t. t ∈ setinterleavingptick (tick_join, u, A, v)}
                else {}
           else {ev b # t |t. t ∈ setinterleavingptick (tick_join, ev a # u, A, v)}
      else   if b ∈ A
           then {ev a # t |t. t ∈ setinterleavingptick (tick_join, u, A, ev b # v)}
           else {ev a # t |t. t ∈ setinterleavingptick (tick_join, u, A, ev b # v)} ∪
                {ev b # t |t. t ∈ setinterleavingptick (tick_join, ev a # u, A, v)}
             | ✓(s) ⇒   if a ∈ A then {}
                       else {ev a # t |t. t ∈ setinterleavingptick (tick_join, u, A, ✓(s) # v)})
            | ✓(r) ⇒
    (case f of ev b ⇒
         if b ∈ A then {}
       else {ev b # t| t. t ∈ setinterleavingptick (tick_join, ✓(r) # u, A, v)}
             | ✓(s) ⇒
         (case tick_join r s of ⌊r_s⌋ ⇒
            {✓(r_s) # t |t. t ∈ setinterleavingptick (tick_join, u, A, v)}
                                |  ◇ ⇒ {})))›
  by (cases e; cases f) simp_all


lemmas setinterleavingptick_simps =
  Cons_setinterleavingptick_Nil Nil_setinterleavingptick_Cons Cons_setinterleavingptick_Cons 



abbreviation setinterleavesptick ::
  ‹[('a, 't) traceptick, 'r ⇒ 's ⇒ 't option,
    ('a, 'r) traceptick, ('a, 's) traceptick, 'a set] ⇒ bool›
  (‹(_ /(setinterleaves✓)⇘_⇙/ '(()'(_, _')(), _'))› [63,0,0,0,0] 64)
  where ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ≡
         t ∈ setinterleavingptick (tick_join, u, A, v)›



subsection ‹First Properties›

text ‹First of all: this formalization may seem tricky,
      but is actually a generalization of the old setup.›

theorem setinterleaves_is_setinterleavesptick :
  ‹t setinterleaves ((u, v), range tick ∪ ev ` A) ⟷
   t setinterleaves✓⇘λr s. if r = s then ⌊r⌋ else ◇⇙ ((u, v), A)›
  for t :: ‹('a, 'r) traceptick›
  by (induct ‹(λr :: 'r. λs :: 'r. if r = s then ⌊r⌋ else ◇, u, A, v)›
      arbitrary: t u v) (simp_all add: image_iff)

corollary setinterleaves_is_setinterleavesptick_unit :
  ‹t setinterleaves ((u, v), insert ✓ (ev ` A)) ⟷
   t setinterleaves✓⇘λr s. ⌊r⌋⇙ ((u, v), A)› (is ‹?lhs ⟷ ?rhs›)
proof -
  have ‹?lhs ⟷ t setinterleaves ((u, v), range tick ∪ ev ` A)›
    by (simp add: UNIV_unit)
  also have ‹… ⟷ ?rhs›
    by (simp add: setinterleaves_is_setinterleavesptick)
  finally show ‹?lhs ⟷ ?rhs› .
qed




lemma setinterleavesptick_sym :
  ―‹Of course not suitable for simplifier.›
  ‹t setinterleaves✓⇘λs r. tick_join r s⇙ ((v, u), A) ⟷
   t setinterleaves✓⇘λr s. tick_join r s⇙ ((u, v), A)›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v) (auto split: option.split)


lemma setinterleavesPair_UNIV_iff :
  ‹t setinterleaves✓⇘λr s. ⌊(r, s)⌋⇙ ((u, v), UNIV) ⟷
   u = map (map_eventptick id fst) t ∧
   v = map (map_eventptick id snd) t› for t :: ‹('a, 'r × 's) traceptick›
  by (induct ‹(λr :: 'r. λs :: 's. ⌊(r, s)⌋, u, UNIV :: 'a set, v)› arbitrary: t u v)
    (auto simp add: ev_eq_map_eventptick_iff tick_eq_map_eventptick_iff)

lemma setinterleavesptick_empty :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), {}) ⟹
   ev a ∈ set t ⟷ ev a ∈ set u ∨ ev a ∈ set v›
  for u :: ‹('a, 'r) traceptick ›
  by (induct ‹(tick_join, u, {} :: 'a set, v)› arbitrary: t u v)
    (auto split: option.split_asm)




lemma tickFree_setinterleavesptick_any_tick_join :
  ‹t setinterleaves✓⇘tick_join ⇙ ((u, v), A) ⟷
   t setinterleaves✓⇘tick_join'⇙ ((u, v), A)›
  if ‹tF t ∨ tF u ∨ tF v›
proof (rule iffI)
  from ‹tF t ∨ tF u ∨ tF v›
  show ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
        t setinterleaves✓⇘tick_join'⇙ ((u, v), A)›
    for tick_join tick_join'
    by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
      (auto split: if_split_asm option.split_asm)
  thus ‹t setinterleaves✓⇘tick_join'⇙ ((u, v), A) ⟹
        t setinterleaves✓⇘tick_join⇙ ((u, v), A)› .
qed



lemma tickFree_setinterleavesptick_iff :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ tF t ⟷ tF u ∧ tF v›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto split: if_split_asm option.split_asm)

lemma setinterleavesptick_tickFree_imp :
  ‹tF u ∨ tF v ⟹ t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ tF t ∧ tF u ∧ tF v›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto split: if_split_asm)



lemma setinterleavesptick_NilL_iff :
  ‹t setinterleaves✓⇘tick_join⇙ (([], v), A) ⟷
   tF v ∧ set v ∩ ev ` A = {} ∧ t = map ev (map of_ev v)›
  for tick_join :: ‹'r ⇒ 's ⇒ 't option›
  by (induct ‹(tick_join, [] :: ('a, 'r) traceptick, A, v)›
      arbitrary: t v) (auto split: if_split_asm)

lemma setinterleavesptick_NilR_iff :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, []), A) ⟷
   tF u ∧ set u ∩ ev ` A = {} ∧ t = map ev (map of_ev u)›
  for tick_join :: ‹'r ⇒ 's ⇒ 't option›
  by (induct ‹(tick_join, u, A, [] :: ('a, 's) traceptick)›
      arbitrary: t u) (auto split: if_split_asm)

lemma setinterleavesptick_subsetL :
  ‹tF t ⟹ {a. ev a ∈ set u} ⊆ A ⟹
   t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   t = map ev (map of_ev v)›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto simp add: subset_iff split: if_split_asm option.split_asm)

lemma setinterleavesptick_subsetR :
  ‹tF t ⟹ {a. ev a ∈ set v} ⊆ A ⟹
   t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   t = map ev (map of_ev u)›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto simp add: subset_iff split: if_split_asm option.split_asm)

lemma Nil_setinterleavesptick :
  ‹[] setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ u = [] ∧ v = []›
  by (induct ‹(tick_join, u, A, v)› arbitrary: u v)
    (simp_all split: if_split_asm option.split_asm)


lemma front_tickFree_setinterleavesptick_iff :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ ftF t ⟷ ftF u ∧ ftF v›
proof (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
  case Nil_setinterleavingptick_Nil thus ?case by simp
next
  case (ev_setinterleavingptick_Nil a u)
  thus ?case by (simp add: setinterleavesptick_NilR_iff split: if_split_asm)
next
  case (tick_setinterleavingptick_Nil r u) thus ?case by simp
next
  case (Nil_setinterleavingptick_ev b v) 
  thus ?case by (simp add: setinterleavesptick_NilL_iff split: if_split_asm)
next
  case (Nil_setinterleavingptick_tick s v) thus ?case by simp
next
  case (ev_setinterleavingptick_ev a u b v)
  thus ?case by (simp split: if_split_asm)
      (metis eventptick.disc(1) front_tickFree_Cons_iff front_tickFree_Nil)+
next
  case (ev_setinterleavingptick_tick a u s v)
  thus ?case by (simp split: if_split_asm)
      (metis eventptick.disc(1) front_tickFree_Cons_iff front_tickFree_Nil)
next
  case (tick_setinterleavingptick_ev r u b v)
  thus ?case by (simp split: if_split_asm)
      (metis eventptick.disc(1) front_tickFree_Cons_iff front_tickFree_Nil)
next
  case (tick_setinterleavingptick_tick r u s v) thus ?case
    by (simp split: option.split_asm) 
      (metis Nil_setinterleavesptick Nil_setinterleavingptick_Nil
        eventptick.disc(2) front_tickFree_Cons_iff singletonD)
qed





lemma setinterleavesptick_snoc_notinL :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ a ∉ A ⟹
   t @ [ev a] setinterleaves✓⇘tick_join⇙ ((u @ [ev a], v), A)›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto split: if_split_asm option.split_asm)

lemma setinterleavesptick_snoc_notinR :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ a ∉ A ⟹
   t @ [ev a] setinterleaves✓⇘tick_join⇙ ((u, v @ [ev a]), A)›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto split: if_split_asm option.split_asm)

lemma setinterleavesptick_snoc_inside :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ a ∈ A ⟹
   t @ [ev a] setinterleaves✓⇘tick_join⇙ ((u @ [ev a], v @ [ev a]), A)›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto split: if_split_asm option.split_asm)


lemma setinterleavesptick_snoc_tick :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ tick_join r s = ⌊r_s⌋ ⟹
   t @ [✓(r_s)] setinterleaves✓⇘tick_join⇙ ((u @ [✓(r)], v @ [✓(s)]), A)›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto split: if_split_asm option.split_asm)


lemma Cons_tick_setinterleavesptickE :
  ‹✓(r_s) # t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   (⋀u' v' r s. ⟦tick_join r s = ⌊r_s⌋; u = ✓(r) # u'; v = ✓(s) # v';
                 t setinterleaves✓⇘tick_join⇙ ((u', v'), A)⟧ ⟹ thesis) ⟹ thesis›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (simp_all split: if_split_asm option.split_asm)

lemma Cons_ev_setinterleavesptickE :
  ‹ev a # t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   (⋀u'. a ∉ A ⟹ u = ev a # u' ⟹ t setinterleaves✓⇘tick_join⇙ ((u', v), A) ⟹ thesis) ⟹
   (⋀v'. a ∉ A ⟹ v = ev a # v' ⟹ t setinterleaves✓⇘tick_join⇙ ((u, v'), A) ⟹ thesis) ⟹
   (⋀u' v'. a ∈ A ⟹ u = ev a # u' ⟹ v = ev a # v' ⟹
             t setinterleaves✓⇘tick_join⇙ ((u', v'), A) ⟹ thesis) ⟹ thesis›
proof (induct ‹(tick_join, u, A, v)› arbitrary: u v t)
  case Nil_setinterleavingptick_Nil thus ?case by simp
next
  case (ev_setinterleavingptick_Nil b u)
  from ev_setinterleavingptick_Nil.prems(1) show ?case
    by (simp add: ev_setinterleavingptick_Nil.prems(2) split: if_split_asm)
next
  case (tick_setinterleavingptick_Nil r u) thus ?case by simp
next
  case (Nil_setinterleavingptick_ev c v)
  from Nil_setinterleavingptick_ev.prems(1) show ?case
    by (simp add: Nil_setinterleavingptick_ev.prems(3) split: if_split_asm)
next
  case (Nil_setinterleavingptick_tick s v) thus ?case by simp
next
  case (ev_setinterleavingptick_ev b u c v)
  from ev_setinterleavingptick_ev.prems(1) show ?case
    by (simp add: ev_setinterleavingptick_ev.prems(2, 3, 4) split: if_split_asm)
      (use ev_setinterleavingptick_ev.prems(2, 3) in presburger)
next
  case (ev_setinterleavingptick_tick b u s v)
  from ev_setinterleavingptick_tick.prems(1) show ?case
    by (simp add: ev_setinterleavingptick_tick.prems(2) split: if_split_asm)
next
  case (tick_setinterleavingptick_ev r u c v)
  from tick_setinterleavingptick_ev.prems(1) show ?case
    by (simp add: tick_setinterleavingptick_ev.prems(3) split: if_split_asm)
next
  case (tick_setinterleavingptick_tick r u s v)
  thus ?case by (simp split: option.split_asm)
qed


lemma rev_setinterleavesptick_rev_rev_iff :
  ‹rev t setinterleaves✓⇘tick_join⇙ ((rev u, rev v), A)
   ⟷ t setinterleaves✓⇘tick_join⇙ ((u, v), A)›
  for u :: ‹('a, 'r) traceptick› and v :: ‹('a, 's) traceptick›
proof (rule iffI)
  show ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
        rev t setinterleaves✓⇘tick_join⇙ ((rev u, rev v), A)›
    for u :: ‹('a, 'r) traceptick› and v :: ‹('a, 's) traceptick› and t
  proof (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    case Nil_setinterleavingptick_Nil thus ?case by simp
  next
    case (ev_setinterleavingptick_Nil a u)
    thus ?case by (auto simp add: setinterleavesptick_snoc_notinL split: if_split_asm )
  next
    case (tick_setinterleavingptick_Nil r v) thus ?case by simp
  next
    case (Nil_setinterleavingptick_ev b v)
    thus ?case by (auto simp add:  setinterleavesptick_snoc_notinR split: if_split_asm )
  next
    case (Nil_setinterleavingptick_tick s v) thus ?case by simp
  next
    case (ev_setinterleavingptick_ev a u b v)
    from ev_setinterleavingptick_ev.prems
    consider (both_in)   t' where ‹a ∈ A› ‹a = b› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, v), A)›
    |        (inR_mvL)   t' where ‹a ∉ A› ‹b ∈ A› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), A)›
    |        (inL_mvR)   t' where ‹a ∈ A› ‹b ∉ A› ‹t = ev b # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), A)›
    |        (notin_mvL) t' where ‹a ∉ A› ‹b ∉ A› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), A)›
    |        (notin_mvR) t' where ‹a ∉ A› ‹b ∉ A› ‹t = ev b # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), A)›
      by (auto split: if_split_asm)
    thus ?case
    proof cases
      case both_in thus ?thesis
        by (simp add: ev_setinterleavingptick_ev.hyps(1) setinterleavesptick_snoc_inside)
    next
      case inR_mvL thus ?thesis
        by (metis ev_setinterleavingptick_ev.hyps(3) rev.simps(2) setinterleavesptick_snoc_notinL)
    next
      case inL_mvR thus ?thesis
        by (metis ev_setinterleavingptick_ev.hyps(2) rev.simps(2) setinterleavesptick_snoc_notinR)
    next
      case notin_mvL thus ?thesis
        by (metis ev_setinterleavingptick_ev.hyps(4) rev.simps(2) setinterleavesptick_snoc_notinL)
    next
      case notin_mvR thus ?thesis
        by (metis ev_setinterleavingptick_ev.hyps(5) rev.simps(2) setinterleavesptick_snoc_notinR)
    qed
  next
    case (ev_setinterleavingptick_tick a u s v) thus ?case
      by (auto simp add: setinterleavesptick_snoc_notinL split: if_split_asm)
  next
    case (tick_setinterleavingptick_ev r u b v) thus ?case
      by (auto simp add: setinterleavesptick_snoc_notinR split: if_split_asm)
  next
    case (tick_setinterleavingptick_tick r u s v)
    from tick_setinterleavingptick_tick.prems
    obtain t' r_s where ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, v), A)›
      by (auto split: option.split_asm)
    from ‹t' setinterleaves✓⇘tick_join⇙ ((u, v), A)›
    have ‹rev t' setinterleaves✓⇘tick_join⇙ ((rev u, rev v), A)›
      by (simp add: ‹tick_join r s = ⌊r_s⌋› tick_setinterleavingptick_tick.hyps)
    hence ‹rev t' @ [✓(r_s)] setinterleaves✓⇘tick_join⇙ ((rev u @ [✓(r)], rev v @ [✓(s)]), A)›
      by (simp add: ‹tick_join r s = ⌊r_s⌋› setinterleavesptick_snoc_tick)
    thus ?case by (simp add: ‹t = ✓(r_s) # t'› )
  qed
  from this[of ‹rev t› ‹rev u› ‹rev v›, simplified]
  show ‹rev t setinterleaves✓⇘tick_join⇙ ((rev u, rev v), A) ⟹
        t setinterleaves✓⇘tick_join⇙ ((u, v), A)› .
qed


lemma setinterleavesptick_preserves_ev_notin_set :
  ‹⟦ev a ∉ set u; ev a ∉ set v; t setinterleaves✓⇘tick_join⇙ ((u, v), A)⟧ ⟹ ev a ∉ set t›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto split: if_split_asm option.split_asm)

lemma setinterleavesptick_inj_preserves_tick_notin_set :
  ‹⟦tick_join r s = ⌊r_s⌋; ✓(r) ∉ set u ∨ ✓(s) ∉ set v;
    t setinterleaves✓⇘tick_join⇙ ((u, v), A)⟧ ⟹ ✓(r_s) ∉ set t›
  ―‹This is a weakened injectivity property.›
  if inj_tick_join : ‹⋀r' s'. tick_join r' s' = ⌊r_s⌋ ⟹ r' = r ∧ s' = s›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto split: if_split_asm option.split_asm, (metis inj_tick_join)+)

lemma setinterleavesptick_preserves_ev_inside_set :
  ‹⟦ev a ∈ set u; ev a ∈ set v; t setinterleaves✓⇘tick_join⇙ ((u, v), A)⟧ ⟹ ev a ∈ set t›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto split: if_split_asm option.split_asm)

lemma ev_notin_both_sets_imp_empty_setinterleavingptick :
  ‹⟦ev a ∈ set u ∧ ev a ∉ set v ∨ ev a ∉ set u ∧ ev a ∈ set v; a ∈ A⟧ ⟹
   setinterleavingptick (tick_join, u, A, v) = {}›
  by (induct ‹(tick_join, u, A, v)› arbitrary: u v)
    (simp_all, safe, auto split: option.split_asm)



lemma setinterleavesptick_snoc_tick_snoc_tickE:
  ‹(⋀t' r_s. tick_join r s = ⌊r_s⌋ ⟹ t' setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
              t = t' @ [✓(r_s)] ⟹ thesis) ⟹ thesis›
  if ‹t setinterleaves✓⇘tick_join⇙ ((u @ [✓(r)], v @ [✓(s)]), A)›
proof -
  from that have ‹rev t setinterleaves✓⇘tick_join⇙ ((✓(r) # rev u, ✓(s) # rev v), A)›
    by (metis (no_types) rev.simps(2) rev_rev_ident rev_setinterleavesptick_rev_rev_iff)
  then obtain t' r_s where ‹tick_join r s = ⌊r_s⌋› ‹rev t = ✓(r_s) # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((rev u, rev v), A)›
    by (cases t rule: rev_cases) (simp_all split: option.split_asm)
  hence ‹rev t' setinterleaves✓⇘tick_join⇙ ((u, v), A) ∧ t = rev t' @ [✓(r_s)]›
    using rev_setinterleavesptick_rev_rev_iff by force
  with ‹tick_join r s = ⌊r_s⌋›
  show ‹(⋀t' r_s. tick_join r s = ⌊r_s⌋ ⟹ t' setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
                  t = t' @ [✓(r_s)] ⟹ thesis) ⟹ thesis› by blast
qed

lemma snoc_tick_setinterleavesptickE :
  ‹(⋀u' v' r s. ⟦tick_join r s = ⌊r_s⌋; t setinterleaves✓⇘tick_join⇙ ((u', v'), A);
                 u = u' @ [✓(r)]; v = v' @ [✓(s)]⟧ ⟹ thesis) ⟹ thesis›
  if ‹t @ [✓(r_s)] setinterleaves✓⇘tick_join⇙ ((u, v), A)›
proof -
  from that have ‹rev (t @ [✓(r_s)]) setinterleaves✓⇘tick_join⇙ ((rev u, rev v), A)›
    by (metis (no_types) rev.simps(2) rev_rev_ident rev_setinterleavesptick_rev_rev_iff)
  hence ‹✓(r_s) # rev t setinterleaves✓⇘tick_join⇙ ((rev u, rev v), A)› by simp
  then obtain u' v' r s where ‹tick_join r s = ⌊r_s⌋›
    ‹rev t setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
    ‹rev u = ✓(r) # u'› ‹rev v = ✓(s) # v'›
    by (elim Cons_tick_setinterleavesptickE)
  hence ‹t setinterleaves✓⇘tick_join⇙ ((rev u', rev v'), A) ∧
         u = rev u' @ [✓(r)] ∧ v = rev v' @ [✓(s)]›
    using rev_setinterleavesptick_rev_rev_iff by fastforce
  with ‹tick_join r s = ⌊r_s⌋›
  show ‹(⋀u' v' r s. ⟦tick_join r s = ⌊r_s⌋; t setinterleaves✓⇘tick_join⇙ ((u', v'), A);
                      u = u' @ [✓(r)]; v = v' @ [✓(s)]⟧ ⟹ thesis) ⟹ thesis› by blast
qed




subsection ‹Lengths›


lemma length_setinterleavesptick_eq_sum_minus_filterL :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   length t = length u + length v - length (filter (λe. e ∈ range tick ∪ ev ` A) u)›
proof (induct t arbitrary: u v)
  case Nil
  thus ?case by (auto dest: Nil_setinterleavesptick)
next
  note thms = Suc_diff_le le_add1 length_filter_le order_trans
  case (Cons e t)
  from Cons.prems consider (mv_left) a u' where ‹a ∉ A› ‹e = ev a› ‹u = ev a # u'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u', v), A)›
  | (mv_right) a v' where ‹a ∉ A› ‹e = ev a› ‹v = ev a # v'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u, v'), A)›
  | (mv_both_ev) a u' v' where ‹a ∈ A› ‹e = ev a› ‹u = ev a # u'› ‹v = ev a # v'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
  | (mv_both_tick) r s r_s u' v' where ‹tick_join r s = ⌊r_s⌋› ‹e = ✓(r_s)›
    ‹u = ✓(r) # u'› ‹v = ✓(s) # v'› ‹t setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
    by (cases e) (auto elim: Cons_ev_setinterleavesptickE Cons_tick_setinterleavesptickE)
  thus ?case
  proof cases
    case mv_left
    from Cons.hyps[OF mv_left(4)] show ?thesis
      by (simp add: mv_left(1-3) image_iff) (metis (no_types, lifting) thms)
  next
    case mv_right
    from Cons.hyps[OF mv_right(4)] show ?thesis
      by (simp add: mv_right(1-3) image_iff) (metis (no_types, lifting) thms)
  next
    case mv_both_ev
    from Cons.hyps[OF mv_both_ev(5)] show ?thesis
      by (simp add: mv_both_ev(1, 3, 4) image_iff) (metis (no_types, lifting) thms)
  next
    case mv_both_tick
    from Cons.hyps[OF mv_both_tick(5)] show ?thesis
      by (simp add: mv_both_tick(3, 4) image_iff) (metis (no_types, lifting) thms)
  qed
qed

lemma length_setinterleavesptick_eq_sum_minus_filterR :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   length t = length u + length v - length (filter (λe. e ∈ range tick ∪ ev ` A) v)›
  by (subst (asm) setinterleavesptick_sym)
    (auto dest: length_setinterleavesptick_eq_sum_minus_filterL)


lemma setinterleavesptick_eq_length : 
  ‹t  setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   t' setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ length t = length t'›
  by (simp add: length_setinterleavesptick_eq_sum_minus_filterL)


lemma setinterleavesptick_imp_lengthLR_le :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   length u ≤ length t ∧ length v ≤ length t›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (fastforce split: if_split_asm option.split_asm)+



subsection ‹Trace Prefix Interleaving›

text ‹We start with versions involving term‹(@)›
      before giving corollaries about the prefix ordering on traces.›

lemma setinterleavesptick_appendL : 
  ‹t setinterleaves✓⇘tick_join⇙ ((u1 @ u2, v), A) ⟹
   ∃t1 t2 v1 v2. t = t1 @ t2 ∧ v = v1 @ v2 ∧
                 t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A) ∧
                 t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)›
proof (induct ‹(tick_join, u1, A, v)› arbitrary: t u1 v)
  case Nil_setinterleavingptick_Nil
  thus ?case by simp
next
  case (ev_setinterleavingptick_Nil a u1)
  from ev_setinterleavingptick_Nil.prems
  have ‹a ∉ A› ‹t = ev a # map ev (map of_ev (u1 @ u2))›
    ‹map ev (map of_ev (u1 @ u2)) setinterleaves✓⇘tick_join⇙ ((u1 @ u2, []), A)›
    by (simp_all add: setinterleavesptick_NilR_iff split: if_split_asm)
  from ev_setinterleavingptick_Nil.hyps[OF ‹a ∉ A› this(3)]
  obtain t1 t2 v1 v2 where ‹map ev (map of_ev (u1 @ u2)) = t1 @ t2›
    ‹[] = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
    ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
  thus ?case
    by (simp add: ‹a ∉ A› ‹t = ev a # map ev (map of_ev (u1 @ u2))›) 
      (metis append_Cons)
next
  case (tick_setinterleavingptick_Nil r u1)
  from tick_setinterleavingptick_Nil.prems have False by simp
  thus ?case ..
next
  case (Nil_setinterleavingptick_ev b v)
  thus ?case
    by (cases u2, simp_all split: if_split_asm)
      (fastforce, metis Nil_setinterleavingptick_Nil self_append_conv2 singleton_iff)
next
  case (Nil_setinterleavingptick_tick s v)
  thus ?case by (cases u2, simp_all add: setinterleavingptick_simps
        split: eventptick.split_asm) fastforce+
next
  case (ev_setinterleavingptick_ev a u1 b v)
  from ev_setinterleavingptick_ev.prems [simplified]
  consider (mv_both)   t' where ‹a ∈ A› ‹b ∈ A› ‹a = b› ‹t = ev b # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((u1 @ u2, v), A)›
    |    (mvR_inL)   t' where ‹a ∈ A› ‹b ∉ A› ‹t = ev b # t'› ‹t' setinterleaves✓⇘tick_join⇙ (((ev a # u1) @ u2, v), A)›
    |    (mvL_inR)   t' where ‹a ∉ A› ‹b ∈ A› ‹t = ev a # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((u1 @ u2, ev b # v), A)›
    |    (mvR_notin) t' where ‹a ∉ A› ‹b ∉ A› ‹t = ev b # t'› ‹t' setinterleaves✓⇘tick_join⇙ (((ev a # u1) @ u2, v), A)›
    |    (mvL_notin) t' where ‹a ∉ A› ‹b ∉ A› ‹t = ev a # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((u1 @ u2, ev b # v), A)›
    by (auto split: if_split_asm)
  thus ?case
  proof cases 
    case mv_both
    from ev_setinterleavingptick_ev.hyps(1)[OF mv_both(1-3, 5)] obtain t1 t2 v1 v2
      where ‹t' = t1 @ t2› ‹v = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
        ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
    hence ‹t = (ev b # t1) @ t2 ∧ ev b # v = (ev b # v1) @ v2 ∧
           ev b # t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, ev b # v1), A) ∧
           t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by (simp add: mv_both(1-4))
    thus ?thesis by blast
  next
    case mvR_inL
    from ev_setinterleavingptick_ev.hyps(2)[OF mvR_inL(1, 2, 4)] obtain t1 t2 v1 v2
      where ‹t' = t1 @ t2› ‹v = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, v1), A)›
        ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
    hence ‹t = (ev b # t1) @ t2 ∧ ev b # v = (ev b # v1) @ v2 ∧
           ev b # t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, ev b # v1), A) ∧
           t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by (simp add: mvR_inL(1-3))
    thus ?thesis by blast
  next
    case mvL_inR
    from ev_setinterleavingptick_ev.hyps(3)[OF mvL_inR(1, 2, 4)] obtain t1 t2 v1 v2
      where ‹t' = t1 @ t2› ‹ev b # v = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
        ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
    hence ‹t = (ev a # t1) @ t2 ∧ ev b # v = v1 @ v2 ∧
           ev a # t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, v1), A) ∧
           t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)›
      by (cases v1, simp_all add: mvL_inR(1, 3))
    thus ?thesis by blast
  next
    case mvR_notin
    from ev_setinterleavingptick_ev.hyps(5)[OF mvR_notin(1, 2, 4)] obtain t1 t2 v1 v2
      where ‹t' = t1 @ t2› ‹v = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, v1), A)›
        ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
    hence ‹t = (ev b # t1) @ t2 ∧ ev b # v = (ev b # v1) @ v2 ∧
           ev b # t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, ev b # v1), A) ∧
           t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by (simp add: mvR_notin(1-3))
    thus ?thesis by blast
  next
    case mvL_notin
    from ev_setinterleavingptick_ev.hyps(4)[OF mvL_notin(1, 2, 4)] obtain t1 t2 v1 v2
      where ‹t' = t1 @ t2› ‹ev b # v = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
        ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
    hence ‹t = (ev a # t1) @ t2 ∧ ev b # v = v1 @ v2 ∧
           ev a # t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, v1), A) ∧
           t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)›
      by (cases v1, simp_all add: mvL_notin(1, 3))
    thus ?thesis by blast
  qed
next
  case (ev_setinterleavingptick_tick a u1 s v)
  from ev_setinterleavingptick_tick.prems obtain t'
    where ‹a ∉ A› ‹t = ev a # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((u1 @ u2, ✓(s) # v), A)›
    by (auto split: if_split_asm)
  from ev_setinterleavingptick_tick.hyps[OF this(1, 3)] obtain t1 t2 v1 v2
    where ‹t' = t1 @ t2› ‹✓(s) # v = v1 @ v2›
      ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
      ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
  hence ‹t = (ev a # t1) @ t2 ∧ ✓(s) # v = v1 @ v2 ∧
         ev a # t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, v1), A) ∧
         t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)›
    by (cases v1, simp_all add: ‹t = ev a # t'› ‹a ∉ A›)
  thus ?case by blast
next
  case (tick_setinterleavingptick_ev r u1 b v)
  from tick_setinterleavingptick_ev.prems obtain t'
    where ‹b ∉ A› ‹t = ev b # t'› ‹t' setinterleaves✓⇘tick_join⇙ (((✓(r) # u1) @ u2, v), A)›
    by (auto split: if_split_asm)
  from tick_setinterleavingptick_ev.hyps[OF this(1, 3)] obtain t1 t2 v1 v2
    where ‹t' = t1 @ t2› ‹v = v1 @ v2›
      ‹t1 setinterleaves✓⇘tick_join⇙ ((✓(r) # u1, v1), A)›
      ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
  hence ‹t = (ev b # t1) @ t2 ∧ ev b # v = (ev b # v1) @ v2 ∧
         ev b # t1 setinterleaves✓⇘tick_join⇙ ((✓(r) # u1, ev b # v1), A) ∧
         t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)›
    by (simp add: ‹t = ev b # t'› ‹b ∉ A›)
  thus ?case by blast
next
  case (tick_setinterleavingptick_tick r u1 s v)
  from tick_setinterleavingptick_tick.prems obtain r_s t'
    where ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u1 @ u2, v), A)› by (auto split: option.split_asm)
  from tick_setinterleavingptick_tick.hyps[OF this(1, 3)] obtain t1 t2 v1 v2
    where ‹t' = t1 @ t2› ‹v = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
      ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
  hence ‹t = (✓(r_s) # t1) @ t2 ∧ ✓(s) # v = (✓(s) # v1) @ v2 ∧
         ✓(r_s) # t1 setinterleaves✓⇘tick_join⇙ ((✓(r) # u1, ✓(s) # v1), A) ∧
         t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)›
    by (simp add: ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›)
  thus ?case by blast
qed

corollary setinterleavesptick_appendR : 
  ‹∃t1 t2 u1 u2. t = t1 @ t2 ∧ u = u1 @ u2 ∧
                 t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A) ∧
                 t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)›
  if ‹t setinterleaves✓⇘tick_join⇙ ((u, v1 @ v2), A)›
proof -
  from that have ‹t setinterleaves✓⇘λs r. tick_join r s⇙ ((v1 @ v2, u), A)›
    using setinterleavesptick_sym by blast
  from setinterleavesptick_appendL[OF this]
  obtain t1 t2 u1 u2 where ‹t = t1 @ t2› ‹u = u1 @ u2›
    ‹t1 setinterleaves✓⇘λs r. tick_join r s⇙ ((v1, u1), A)›
    ‹t2 setinterleaves✓⇘λs r. tick_join r s⇙ ((v2, u2), A)› by blast
  from this(3, 4) have ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
    ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› 
    using setinterleavesptick_sym by blast+
  with ‹t = t1 @ t2› ‹u = u1 @ u2› show ?thesis by blast
qed



lemma append_setinterleavesptick :
  ‹t1 @ t2 setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   ∃u1 u2 v1 v2. u = u1 @ u2 ∧ v = v1 @ v2 ∧
                 t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A) ∧
                 t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)›
proof (induct t1 arbitrary: u v)
  case Nil
  hence ‹u = [] @ u› ‹v = [] @ v›
    ‹[] setinterleaves✓⇘tick_join⇙ (([], []), A)›
    ‹t2 setinterleaves✓⇘tick_join⇙ ((u, v), A)› by simp_all
  thus ?case by blast
next
  case (Cons e t1)
  from Cons.prems consider (mv_left) a u' where ‹a ∉ A› ‹e = ev a› ‹u = ev a # u'›
    ‹t1 @ t2 setinterleaves✓⇘tick_join⇙ ((u', v), A)›
  | (mv_right) a v' where ‹a ∉ A› ‹e = ev a› ‹v = ev a # v'›
    ‹t1 @ t2 setinterleaves✓⇘tick_join⇙ ((u, v'), A)›
  | (mv_both_ev) a u' v' where ‹a ∈ A› ‹e = ev a› ‹u = ev a # u'› ‹v = ev a # v'›
    ‹t1 @ t2 setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
  | (mv_both_tick) r s r_s u' v' where ‹tick_join r s = ⌊r_s⌋› ‹e = ✓(r_s)›
    ‹u = ✓(r) # u'› ‹v = ✓(s) # v'› ‹t1 @ t2 setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
    by (cases e) (auto elim: Cons_ev_setinterleavesptickE Cons_tick_setinterleavesptickE)
  thus ?case
  proof cases
    case mv_left
    from Cons.hyps[OF mv_left(4)] obtain u1 u2 v1 v2
      where ‹u' = u1 @ u2› ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
        and * : ‹v = v1 @ v2› ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
    from this(2) have ‹e # t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, v1), A)›
      by (cases v1) (auto simp add: ‹a ∉ A› ‹e = ev a› setinterleavingptick_simps
          split: eventptick.split)
    moreover from ‹u' = u1 @ u2› have ‹u = (ev a # u1) @ u2›
      by (simp add: mv_left(3))
    ultimately show ?thesis using "*"(1, 2) by blast
  next
    case mv_right
    from Cons.hyps[OF mv_right(4)] obtain u1 u2 v1 v2
      where ‹v' = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
        and * : ‹u = u1 @ u2› ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
    from this(2) have ‹e # t1 setinterleaves✓⇘tick_join⇙ ((u1, ev a # v1), A)›
      by (cases u1) (auto simp add: ‹a ∉ A› ‹e = ev a› setinterleavingptick_simps
          split: eventptick.split)
    moreover from ‹v' = v1 @ v2› have ‹v = (ev a # v1) @ v2›
      by (simp add: mv_right(3))
    ultimately show ?thesis using "*"(1, 2) by blast
  next
    case mv_both_ev
    from Cons.hyps[OF mv_both_ev(5)] obtain u1 u2 v1 v2
      where ‹u' = u1 @ u2› ‹v' = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
        and * : ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
    from this(3) have ‹e # t1 setinterleaves✓⇘tick_join⇙ ((ev a # u1, ev a # v1), A)›
      by (simp add: ‹a ∈ A› ‹e = ev a›)
    moreover from ‹u' = u1 @ u2› have ‹u = (ev a # u1) @ u2›
      by (simp add: mv_both_ev(3))
    moreover from ‹v' = v1 @ v2› have ‹v = (ev a # v1) @ v2›
      by (simp add: mv_both_ev(4))
    ultimately show ?thesis using "*" by blast
  next
    case mv_both_tick
    from Cons.hyps[OF mv_both_tick(5)] obtain u1 u2 v1 v2
      where ‹u' = u1 @ u2› ‹v' = v1 @ v2› ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
        and * : ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)› by blast
    from this(3) have ‹e # t1 setinterleaves✓⇘tick_join⇙ ((✓(r) # u1, ✓(s) # v1), A)›
      by (simp add: mv_both_tick(1, 2))
    moreover from ‹u' = u1 @ u2› have ‹u = (✓(r) # u1) @ u2›
      by (simp add: mv_both_tick(3))
    moreover from ‹v' = v1 @ v2› have ‹v = (✓(s) # v1) @ v2›
      by (simp add: mv_both_tick(4))
    ultimately show ?thesis using "*" by blast
  qed
qed



corollary setinterleavesptick_le_prefixL :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ u' ≤ u ⟹
   ∃t' ≤ t. ∃v' ≤ v. t' setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
  by (auto elim!: prefixE dest!: setinterleavesptick_appendL intro: prefixI)

corollary setinterleavesptick_le_prefixR :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ v' ≤ v ⟹
   ∃t' ≤ t. ∃u' ≤ u. t' setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
  by (auto elim!: prefixE dest!: setinterleavesptick_appendR intro: prefixI)

corollary le_prefix_setinterleavesptick :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ t' ≤ t ⟹
   ∃u' ≤ u. ∃v' ≤ v. t' setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
  by (auto elim!: prefixE dest!: append_setinterleavesptick intro: prefixI)




lemma setinterleavesptick_less_prefixL :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ u' < u ⟹
   ∃t' v'. t' < t ∧ v' ≤ v ∧ t' setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
proof (induct ‹(tick_join, u, A, v)› arbitrary: t u u' v)
  case Nil_setinterleavingptick_Nil thus ?case by simp
next
  case (ev_setinterleavingptick_Nil a u)
  from ‹u' < ev a # u› consider ‹u' = []› | u'' where ‹u' = ev a # u''› ‹u'' < u›
    by (metis Prefix_Order.prefix_Cons less_list_def)
  thus ?case
  proof cases
    from ev_setinterleavingptick_Nil.prems(1)
    show ‹u' = [] ⟹ ?case› by (auto split: if_split_asm)
  next
    fix u'' assume ‹u' = ev a # u''› ‹u'' < u›
    from ev_setinterleavingptick_Nil.prems(1)
    obtain t' where ‹a ∉ A› ‹t = ev a # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((u, []), A)›
      by (auto split: if_split_asm)
    from ev_setinterleavingptick_Nil.hyps[OF ‹a ∉ A› this(3) ‹u'' < u›]
    obtain t'' v' where ‹t'' < t'› ‹v' ≤ []› ‹t'' setinterleaves✓⇘tick_join⇙ ((u'', v'), A)› by blast
    hence ‹ev a # t'' < t ∧ v' ≤ [] ∧ ev a # t'' setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
      by (simp add: ‹u' = ev a # u''› ‹t = ev a # t'› ‹a ∉ A›)
    thus ?case by blast    
  qed
next
  case (tick_setinterleavingptick_Nil r u) thus ?case by simp
next
  case (Nil_setinterleavingptick_ev b v) thus ?case by simp
next
  case (Nil_setinterleavingptick_tick s v) thus ?case by simp
next
  case (ev_setinterleavingptick_ev a u b v)
  from ‹u' < ev a # u› consider ‹u' = []› | u'' where ‹u' = ev a # u''› ‹u'' < u›
    by (metis Prefix_Order.prefix_Cons less_list_def)
  thus ?case
  proof cases
    from ev_setinterleavingptick_ev.prems(1)
    show ‹u' = [] ⟹ ?case› by (simp split: if_split_asm) force+
  next
    fix u'' assume ‹u' = ev a # u''› ‹u'' < u›
    hence ‹ev a # u'' < ev a # u› by simp
    from ev_setinterleavingptick_ev.prems(1)
    consider (both_in)   t' where ‹a ∈ A› ‹b ∈ A› ‹a = b› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, v), A)›
    |      (inR_mvL)   t' where ‹a ∉ A› ‹b ∈ A› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), A)›
    |      (inL_mvR)   t' where ‹a ∈ A› ‹b ∉ A› ‹t = ev b # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), A)›
    |      (notin_mvL) t' where ‹a ∉ A› ‹b ∉ A› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), A)›
    |      (notin_mvR) t' where ‹a ∉ A› ‹b ∉ A› ‹t = ev b # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), A)›
      by (auto split: if_split_asm)
    thus ?case
    proof cases
      case both_in
      from ev_setinterleavingptick_ev.hyps(1)[OF both_in(1-3, 5) ‹u'' < u›]
      obtain t'' v' where ‹t'' < t' ∧ v' ≤ v ∧ t'' setinterleaves✓⇘tick_join⇙ ((u'', v'), A)› by blast
      hence ‹ev a # t'' < t ∧ ev b # v' ≤ ev b # v ∧
             ev a # t'' setinterleaves✓⇘tick_join⇙ ((u', ev b # v'), A)›
        by (simp add: both_in(2, 3, 4) ‹u' = ev a # u''›)
      thus ?thesis by blast
    next
      case inR_mvL
      from ev_setinterleavingptick_ev.hyps(3)[OF inR_mvL(1, 2, 4) ‹u'' < u›]
      obtain t'' v' where ‹t'' < t' ∧ v' ≤ ev b # v ∧ t'' setinterleaves✓⇘tick_join⇙ ((u'', v'), A)› by blast
      hence ‹ev a # t'' < t ∧ v' ≤ ev b # v ∧
             ev a # t'' setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
        by (cases v') (simp_all add: inR_mvL(1-3) ‹u' = ev a # u''›)
      thus ?thesis by blast
    next
      case inL_mvR
      from ev_setinterleavingptick_ev.hyps(2)[OF inL_mvR(1, 2, 4) ‹ev a # u'' < ev a # u›]
      obtain t'' v' where ‹t'' < t' ∧ v' ≤ v ∧ t'' setinterleaves✓⇘tick_join⇙ ((ev a # u'', v'), A)› by blast
      hence ‹ev b # t'' < t ∧ ev b # v' ≤ ev b # v ∧
             ev b # t'' setinterleaves✓⇘tick_join⇙ ((u', ev b # v'), A)›
        by (simp add: inL_mvR(1-3) ‹u' = ev a # u''›)
      thus ?thesis by blast
    next
      case notin_mvL
      from ev_setinterleavingptick_ev.hyps(4)[OF notin_mvL(1, 2, 4) ‹u'' < u›]
      obtain t'' v' where ‹t'' < t' ∧ v' ≤ ev b # v ∧ t'' setinterleaves✓⇘tick_join⇙ ((u'', v'), A)› by blast
      hence ‹ev a # t'' < t ∧ v' ≤ ev b # v ∧
             ev a # t'' setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
        by (cases v') (simp_all add: notin_mvL(1-3) ‹u' = ev a # u''›)
      thus ?thesis by blast
    next
      case notin_mvR
      from ev_setinterleavingptick_ev.hyps(5)[OF notin_mvR(1, 2, 4) ‹ev a # u'' < ev a # u›]
      obtain t'' v' where ‹t'' < t' ∧ v' ≤ v ∧ t'' setinterleaves✓⇘tick_join⇙ ((ev a # u'', v'), A)› by blast
      hence ‹ev b # t'' < t ∧ ev b # v' ≤ ev b # v ∧
             ev b # t'' setinterleaves✓⇘tick_join⇙ ((u', ev b # v'), A)›
        by (simp add: notin_mvR(1-3) ‹u' = ev a # u''›)
      thus ?thesis by blast
    qed
  qed
next
  case (ev_setinterleavingptick_tick a u s v)
  from ‹u' < ev a # u› consider ‹u' = []› | u'' where ‹u' = ev a # u''› ‹u'' < u›
    by (metis Prefix_Order.prefix_Cons less_list_def)
  thus ?case
  proof cases
    from ev_setinterleavingptick_tick.prems(1)
    show ‹u' = [] ⟹ ?case› by (simp split: if_split_asm) force+
  next
    fix u'' assume ‹u' = ev a # u''› ‹u'' < u›
    from ev_setinterleavingptick_tick.prems obtain t'
      where ‹a ∉ A› ‹t = ev a # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((u, ✓(s) # v), A)›
      by (auto split: if_split_asm)
    from ev_setinterleavingptick_tick.hyps[OF ‹a ∉ A› this(3) ‹u'' < u›]
    obtain t'' v' where ‹t'' < t' ∧ v' ≤ ✓(s) # v ∧ t'' setinterleaves✓⇘tick_join⇙ ((u'', v'), A)› by blast
    hence ‹ev a # t'' < t ∧ v' ≤ ✓(s) # v ∧ ev a # t'' setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
      by (cases v') (simp_all add: ‹a ∉ A› ‹u' = ev a # u''› ‹t = ev a # t'›)
    thus ?case by blast
  qed
next
  case (tick_setinterleavingptick_ev r u b v)
  from ‹u' < ✓(r) # u› consider ‹u' = []› | u'' where ‹u' = ✓(r) # u''› ‹u'' < u›
    by (metis Prefix_Order.prefix_Cons less_list_def)
  thus ?case
  proof cases
    from tick_setinterleavingptick_ev.prems(1)
    show ‹u' = [] ⟹ ?case› by (simp split: if_split_asm) force+
  next
    fix u'' assume ‹u' = ✓(r) # u''› ‹u'' < u›
    hence ‹✓(r) # u'' < ✓(r) # u› by simp
    from tick_setinterleavingptick_ev.prems obtain t'
      where ‹b ∉ A› ‹t = ev b # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((✓(r) # u, v), A)›
      by (auto split: if_split_asm)
    from tick_setinterleavingptick_ev.hyps[OF ‹b ∉ A› this(3) ‹✓(r) # u'' < ✓(r) # u›]
    obtain t'' v' where ‹t'' < t' ∧ v' ≤ v ∧ t'' setinterleaves✓⇘tick_join⇙ ((✓(r) # u'', v'), A)› by blast
    hence ‹ev b # t'' < t ∧ ev b # v' ≤ ev b # v ∧
           ev b # t'' setinterleaves✓⇘tick_join⇙ ((u', ev b # v'), A)›
      by (simp add: ‹b ∉ A› ‹u' = ✓(r) # u''› ‹t = ev b # t'›)
    thus ?case by blast
  qed
next
  case (tick_setinterleavingptick_tick r u s v)
  from ‹u' < ✓(r) # u› consider ‹u' = []› | u'' where ‹u' = ✓(r) # u''› ‹u'' < u›
    by (metis Prefix_Order.prefix_Cons less_list_def)
  thus ?case
  proof cases
    from tick_setinterleavingptick_tick.prems(1)
    show ‹u' = [] ⟹ ?case› by (force split: option.split_asm)
  next
    fix u'' assume ‹u' = ✓(r) # u''› ‹u'' < u›
    from tick_setinterleavingptick_tick.prems(1)
    obtain t' r_s
      where ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((u, v), A)›
      by (auto split: option.split_asm)
    from tick_setinterleavingptick_tick.hyps[OF this(1, 3) ‹u'' < u›]
    obtain t'' v' where ‹t'' < t' ∧ v' ≤ v ∧ t'' setinterleaves✓⇘tick_join⇙ ((u'', v'), A)› by blast
    hence ‹✓(r_s) # t'' < t ∧ ✓(s) # v' ≤ ✓(s) # v ∧ ✓(r_s) # t'' setinterleaves✓⇘tick_join⇙ ((u', ✓(s) # v'), A)›
      by (simp add: ‹tick_join r s = ⌊r_s⌋› ‹u' = ✓(r) # u''› ‹t = ✓(r_s) # t'›)
    thus ?case by blast
  qed
qed


corollary setinterleavesptick_less_prefixR :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ v' < v ⟹
   ∃t' u'. t' < t ∧ u' ≤ u ∧ t' setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
  using setinterleavesptick_less_prefixL setinterleavesptick_sym by blast



lemma setinterleavesptick_le_prefixLR :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹ u' ≤ u ⟹ v' ≤ v ⟹
   (∃t' ≤ t. ∃v'' ≤ v'. t' setinterleaves✓⇘tick_join⇙ ((u', v''), A)) ∨
   (∃t' ≤ t. ∃u'' ≤ u'. t' setinterleaves✓⇘tick_join⇙ ((u'', v'), A))›
proof (induct ‹(tick_join, u, A, v)› arbitrary: t u u' v v')
  case Nil_setinterleavingptick_Nil thus ?case by simp
next
  case (ev_setinterleavingptick_Nil a u) thus ?case by simp fastforce
next
  case (tick_setinterleavingptick_Nil r u) thus ?case by simp
next
  case (Nil_setinterleavingptick_ev b v) thus ?case by simp fastforce
next
  case (Nil_setinterleavingptick_tick s v) thus ?case by simp
next
  case (ev_setinterleavingptick_ev a u b v)
  show ?case
  proof (cases ‹u' = [] ∨ v' = []›)
    show ‹u' = [] ∨ v' = [] ⟹ ?case› by force
  next
    assume ‹¬ (u' = [] ∨ v' = [])›
    with ev_setinterleavingptick_ev.prems(2, 3)
    obtain u'' v'' where ‹u' = ev a # u''› ‹u'' ≤ u› ‹v' = ev b # v''› ‹v'' ≤ v›
      by (meson Prefix_Order.prefix_Cons)
    from ev_setinterleavingptick_ev.prems(1)
    consider (both_in)   t' where ‹a ∈ A› ‹b ∈ A› ‹a = b› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, v), A)›
    |      (inR_mvL)   t' where ‹a ∉ A› ‹b ∈ A› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), A)›
    |      (inL_mvR)   t' where ‹a ∈ A› ‹b ∉ A› ‹t = ev b # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), A)›
    |      (notin_mvL) t' where ‹a ∉ A› ‹b ∉ A› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), A)›
    |      (notin_mvR) t' where ‹a ∉ A› ‹b ∉ A› ‹t = ev b # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), A)›
      by (auto split: if_split_asm)
    thus ?case
    proof cases
      case both_in
      from ev_setinterleavingptick_ev.hyps(1)[OF both_in(1-3, 5) ‹u'' ≤ u› ‹v'' ≤ v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u'', v'''), A)›
        hence ‹ev b # t'' ≤ t ∧ ev b # v''' ≤ v' ∧
             ev b # t'' setinterleaves✓⇘tick_join⇙ ((u', ev b # v'''), A)›
          by (simp add: ‹u' = ev a # u''› ‹v' = ev b # v''› both_in(2-4))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u''', v''), A)›
        hence ‹ev a # t'' ≤ t ∧ ev a # u''' ≤ u' ∧
             ev a # t'' setinterleaves✓⇘tick_join⇙ ((ev a # u''', v'), A)›
          by (simp add: ‹u' = ev a # u''› ‹v' = ev b # v''› both_in(2-4))
        thus ?thesis by blast
      qed
    next
      case inR_mvL
      from ev_setinterleavingptick_ev.hyps(3)[OF inR_mvL(1, 2, 4) ‹u'' ≤ u› ‹v' ≤ ev b # v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v'› ‹t'' setinterleaves✓⇘tick_join⇙ ((u'', v'''), A)›
        hence ‹ev a # t'' ≤ t ∧ v''' ≤ v' ∧
             ev a # t'' setinterleaves✓⇘tick_join⇙ ((u', v'''), A)›
          by (cases v''') (simp_all add: ‹u' = ev a # u''› ‹v' = ev b # v''› inR_mvL(1, 3))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u''', v'), A)›
        hence ‹ev a # t'' ≤ t ∧ ev a # u''' ≤ u' ∧
             ev a # t'' setinterleaves✓⇘tick_join⇙ ((ev a # u''', v'), A)›
          by (simp add: ‹u' = ev a # u''› ‹v' = ev b # v''› inR_mvL(1, 3))
        thus ?thesis by blast
      qed
    next
      case inL_mvR
      from ev_setinterleavingptick_ev.hyps(2)[OF inL_mvR(1, 2, 4) ‹u' ≤ ev a # u› ‹v'' ≤ v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u', v'''), A)›
        hence ‹ev b # t'' ≤ t ∧ ev b # v''' ≤ v' ∧
             ev b # t'' setinterleaves✓⇘tick_join⇙ ((u', ev b # v'''), A)›
          by (simp add: ‹u' = ev a # u''› ‹v' = ev b # v''› inL_mvR(2, 3))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u'› ‹t'' setinterleaves✓⇘tick_join⇙ ((u''', v''), A)›
        hence ‹ev b # t'' ≤ t ∧ u''' ≤ u' ∧
             ev b # t'' setinterleaves✓⇘tick_join⇙ ((u''', v'), A)›
          by (cases u''') (simp_all add: ‹u' = ev a # u''› ‹v' = ev b # v''› inL_mvR(2, 3))
        thus ?thesis by blast
      qed
    next
      case notin_mvL
      from ev_setinterleavingptick_ev.hyps(4)[OF notin_mvL(1, 2, 4) ‹u'' ≤ u› ‹v' ≤ ev b # v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v'› ‹t'' setinterleaves✓⇘tick_join⇙ ((u'', v'''), A)›
        hence ‹ev a # t'' ≤ t ∧ v''' ≤ v' ∧
             ev a # t'' setinterleaves✓⇘tick_join⇙ ((u', v'''), A)›
          by (cases v''') (simp_all add: ‹u' = ev a # u''› ‹v' = ev b # v''› notin_mvL(1, 3))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u''', v'), A)›
        hence ‹ev a # t'' ≤ t ∧ ev a # u''' ≤ u' ∧
             ev a # t'' setinterleaves✓⇘tick_join⇙ ((ev a # u''', v'), A)›
          by (simp add: ‹u' = ev a # u''› ‹v' = ev b # v''› notin_mvL(1, 3))
        thus ?thesis by blast
      qed
    next
      case notin_mvR
      from ev_setinterleavingptick_ev.hyps(5)[OF notin_mvR(1, 2, 4) ‹u' ≤ ev a # u› ‹v'' ≤ v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u', v'''), A)›
        hence ‹ev b # t'' ≤ t ∧ ev b # v''' ≤ v' ∧
             ev b # t'' setinterleaves✓⇘tick_join⇙ ((u', ev b # v'''), A)›
          by (simp add: ‹u' = ev a # u''› ‹v' = ev b # v''› notin_mvR(2, 3))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u'› ‹t'' setinterleaves✓⇘tick_join⇙ ((u''', v''), A)›
        hence ‹ev b # t'' ≤ t ∧ u''' ≤ u' ∧
             ev b # t'' setinterleaves✓⇘tick_join⇙ ((u''', v'), A)›
          by (cases u''') (simp_all add: ‹u' = ev a # u''› ‹v' = ev b # v''› notin_mvR(2, 3))
        thus ?thesis by blast
      qed
    qed
  qed
next
  case (ev_setinterleavingptick_tick a u s v)
  show ?case
  proof (cases ‹u' = [] ∨ v' = []›)
    show ‹u' = [] ∨ v' = [] ⟹ ?case› by force
  next
    assume ‹¬ (u' = [] ∨ v' = [])›
    with ev_setinterleavingptick_tick.prems(2, 3)
    obtain u'' v'' where ‹u' = ev a # u''› ‹u'' ≤ u› ‹v' = ✓(s) # v''› ‹v'' ≤ v›
      by (meson Prefix_Order.prefix_Cons)
    from ev_setinterleavingptick_tick.prems(1)
    obtain t' where ‹a ∉ A› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, ✓(s) # v), A)›
      by (auto split: if_split_asm)
    from ev_setinterleavingptick_tick.hyps[OF this(1, 3) ‹u'' ≤ u› ‹v' ≤ ✓(s) # v›]
    show ?case
    proof (elim disjE exE conjE)
      fix t'' v''' assume ‹t'' ≤ t'› ‹v''' ≤ v'› ‹t'' setinterleaves✓⇘tick_join⇙ ((u'', v'''), A)›
      hence ‹ev a # t'' ≤ t ∧ v''' ≤ v' ∧ ev a # t'' setinterleaves✓⇘tick_join⇙ ((u', v'''), A)›
        by (cases v''') (simp_all add: ‹a ∉ A› ‹t = ev a # t'› ‹u' = ev a # u''› ‹v' = ✓(s) # v''›)
      thus ?case by blast
    next
      fix t'' u''' assume ‹t'' ≤ t'› ‹u''' ≤ u''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u''', v'), A)›
      hence ‹ev a # t'' ≤ t ∧ ev a # u''' ≤ u' ∧ ev a # t'' setinterleaves✓⇘tick_join⇙ ((ev a # u''', v'), A)›
        by (simp add: ‹a ∉ A› ‹t = ev a # t'› ‹u' = ev a # u''› ‹v' = ✓(s) # v''›)
      thus ?case by blast
    qed
  qed
next
  case (tick_setinterleavingptick_ev r u b v)
  show ?case
  proof (cases ‹u' = [] ∨ v' = []›)
    show ‹u' = [] ∨ v' = [] ⟹ ?case› by force
  next
    assume ‹¬ (u' = [] ∨ v' = [])›
    with tick_setinterleavingptick_ev.prems(2, 3)
    obtain u'' v'' where ‹u' = ✓(r) # u''› ‹u'' ≤ u› ‹v' = ev b # v''› ‹v'' ≤ v›
      by (meson Prefix_Order.prefix_Cons)
    from tick_setinterleavingptick_ev.prems(1)
    obtain t' where ‹b ∉ A› ‹t = ev b # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((✓(r) # u, v), A)›
      by (auto split: if_split_asm)
    from tick_setinterleavingptick_ev.hyps[OF this(1, 3) ‹u' ≤ ✓(r) # u› ‹v'' ≤ v›]
    show ?case
    proof (elim disjE exE conjE)
      fix t'' v''' assume ‹t'' ≤ t'› ‹v''' ≤ v''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u', v'''), A)›
      hence ‹ev b # t'' ≤ t ∧ ev b # v''' ≤ v' ∧ ev b # t'' setinterleaves✓⇘tick_join⇙ ((u', ev b # v'''), A)›
        by (simp add: ‹b ∉ A› ‹t = ev b # t'› ‹u' = ✓(r) # u''› ‹v' = ev b # v''›)
      thus ?case by blast
    next
      fix t'' u''' assume ‹t'' ≤ t'› ‹u''' ≤ u'› ‹t'' setinterleaves✓⇘tick_join⇙ ((u''', v''), A)›
      hence ‹ev b # t'' ≤ t ∧ u''' ≤ u' ∧ ev b # t'' setinterleaves✓⇘tick_join⇙ ((u''', v'), A)›
        by (cases u''') (simp_all add: ‹b ∉ A› ‹t = ev b # t'› ‹u' = ✓(r) # u''› ‹v' = ev b # v''›)
      thus ?case by blast
    qed
  qed
next
  case (tick_setinterleavingptick_tick r u s v)
  show ?case
  proof (cases ‹u' = [] ∨ v' = []›)
    show ‹u' = [] ∨ v' = [] ⟹ ?case› by force
  next
    assume ‹¬ (u' = [] ∨ v' = [])›
    with tick_setinterleavingptick_tick.prems(2, 3)
    obtain u'' v'' where ‹u' = ✓(r) # u''› ‹u'' ≤ u› ‹v' = ✓(s) # v''› ‹v'' ≤ v›
      by (meson Prefix_Order.prefix_Cons)
    from tick_setinterleavingptick_tick.prems(1)
    obtain t' r_s where ‹t = ✓(r_s) # t'› ‹tick_join r s = ⌊r_s⌋›
      ‹t' setinterleaves✓⇘tick_join⇙ ((u, v), A)›
      by (auto split: option.split_asm)
    from tick_setinterleavingptick_tick.hyps[OF this(2, 3) ‹u'' ≤ u› ‹v'' ≤ v›]
    show ?case
    proof (elim disjE exE conjE)
      fix t'' v'''
      assume ‹t'' ≤ t'› ‹v''' ≤ v''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u'', v'''), A)›
      hence ‹✓(r_s) # t'' ≤ t ∧ ✓(s) # v''' ≤ v' ∧
             ✓(r_s) # t'' setinterleaves✓⇘tick_join⇙ ((u', ✓(s) # v'''), A)›
        by (simp add: ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›
            ‹u' = ✓(r) # u''› ‹v' = ✓(s) # v''›)
      thus ?case by blast
    next
      fix t'' u'''
      assume ‹t'' ≤ t'› ‹u''' ≤ u''› ‹t'' setinterleaves✓⇘tick_join⇙ ((u''', v''), A)›
      hence ‹✓(r_s) # t'' ≤ t ∧ ✓(r) # u''' ≤ u' ∧
             ✓(r_s) # t'' setinterleaves✓⇘tick_join⇙ ((✓(r) # u''', v'), A)› 
        by (simp add: ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›
            ‹u' = ✓(r) # u''› ‹v' = ✓(s) # v''›)
      thus ?case by blast
    qed
  qed
qed



subsection ‹Hiding Events›

lemma setinterleavesptick_trace_hide :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), S) ⟹
   trace_hide t (ev ` A) setinterleaves✓⇘tick_join⇙
   ((trace_hide u (ev ` A), trace_hide v (ev ` A)), S)›
proof (induct ‹(tick_join, u, S, v)› arbitrary: t u v)
  case Nil_setinterleavingptick_Nil
  thus ?case by simp
next
  case (ev_setinterleavingptick_Nil a u)
  from ev_setinterleavingptick_Nil.prems obtain t' where ‹a ∉ S› ‹t = ev a # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((u, []), S)› by (auto split: if_split_asm)
  from ev_setinterleavingptick_Nil.hyps[OF this(1, 3)]
  show ?case by (simp add: image_iff[of ‹ev _›] ‹a ∉ S› ‹t = ev a # t'›)
next
  case (tick_setinterleavingptick_Nil r u)
  from tick_setinterleavingptick_Nil have False by simp
  thus ?case ..
next
  case (Nil_setinterleavingptick_ev b v)
  from Nil_setinterleavingptick_ev.prems obtain t' where ‹b ∉ S› ‹t = ev b # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ (([], v), S)› by (auto split: if_split_asm)
  from Nil_setinterleavingptick_ev.hyps[OF this(1, 3)]
  show ?case by (simp add: image_iff[of ‹ev _›] ‹b ∉ S› ‹t = ev b # t'›)
next
  case (Nil_setinterleavingptick_tick s v)
  from Nil_setinterleavingptick_tick.prems have False by simp
  thus ?case ..
next
  case (ev_setinterleavingptick_ev a u b v)
  from ev_setinterleavingptick_ev.prems
  consider (both_in)   t' where ‹a ∈ S› ‹b ∈ S› ‹a = b› ‹t = ev a # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((u, v), S)›
  |        (inR_mvL)   t' where ‹a ∉ S› ‹b ∈ S› ‹t = ev a # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), S)›
  |        (inL_mvR)   t' where ‹a ∈ S› ‹b ∉ S› ‹t = ev b # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), S)›
  |        (notin_mvL) t' where ‹a ∉ S› ‹b ∉ S› ‹t = ev a # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), S)›
  |        (notin_mvR) t' where ‹a ∉ S› ‹b ∉ S› ‹t = ev b # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), S)›
    by (auto split: if_split_asm)
  thus ?case
  proof cases
    case both_in
    from ev_setinterleavingptick_ev.hyps(1)[OF both_in(1-3, 5)]
    show ?thesis by (simp add: both_in(2-5) image_iff[of ‹ev _›])
  next
    case inR_mvL
    from ev_setinterleavingptick_ev.hyps(3)[OF inR_mvL(1, 2, 4)]
    show ?thesis by (cases ‹trace_hide v (ev ` A)›)
        (auto simp add: inR_mvL(1-3) setinterleavingptick_simps
          split: if_split_asm eventptick.split)
  next
    case inL_mvR
    from ev_setinterleavingptick_ev.hyps(2)[OF inL_mvR(1, 2, 4)]
    show ?thesis by (cases ‹trace_hide u (ev ` A)›)
        (auto simp add: inL_mvR(1-3) setinterleavingptick_simps
          split: if_split_asm eventptick.split)
  next
    case notin_mvL
    from ev_setinterleavingptick_ev.hyps(4)[OF notin_mvL(1, 2, 4)]
    show ?thesis by (cases ‹trace_hide v (ev ` A)›)
        (auto simp add: notin_mvL(1-3) setinterleavingptick_simps
          split: if_split_asm eventptick.split)
  next
    case notin_mvR
    from ev_setinterleavingptick_ev.hyps(5)[OF notin_mvR(1, 2, 4)]
    show ?thesis by (cases ‹trace_hide u (ev ` A)›)
        (auto simp add: notin_mvR(1-3) setinterleavingptick_simps
          split: if_split_asm eventptick.split)
  qed
next
  case (ev_setinterleavingptick_tick a u s v)
  from ev_setinterleavingptick_tick.prems obtain t' where ‹a ∉ S› ‹t = ev a # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((u, ✓(s) # v), S)› by (auto split: if_split_asm)
  from ev_setinterleavingptick_tick.hyps[OF this(1, 3)]
  show ?case by (simp add: image_iff[of ‹ev _›] image_iff[of ‹✓(_)›] ‹a ∉ S› ‹t = ev a # t'›)
next
  case (tick_setinterleavingptick_ev r u b v)
  from tick_setinterleavingptick_ev.prems obtain t' where ‹b ∉ S› ‹t = ev b # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((✓(r) # u, v), S)› by (auto split: if_split_asm)
  from tick_setinterleavingptick_ev.hyps[OF this(1, 3)]
  show ?case by (simp add: image_iff[of ‹ev _›] image_iff[of ‹✓(_)›] ‹b ∉ S› ‹t = ev b # t'›)
next
  case (tick_setinterleavingptick_tick r u s v)
  from tick_setinterleavingptick_tick.prems
  obtain r_s t' where ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((u, v), S)› by (auto split: option.split_asm)
  from tick_setinterleavingptick_tick.hyps[OF this(1, 3)]
  show ?case by (simp add: image_iff[of ‹✓(_)›] ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›)
qed


lemma trace_hide_map_map_eventptick :
  ‹trace_hide (map (map_eventptick f g) t) S =
   map (map_eventptick f g) (trace_hide t (map_eventptick f g -` S))›
  by (induct t) simp_all


lemma tickFree_trace_hide_map_ev_comp_of_ev :
  ‹tF t ⟹ trace_hide (map (ev ∘ of_ev) t) (ev ` A) =
            map (ev ∘ of_ev) (trace_hide t (ev ` A))›
  by (induct t) (auto simp add: image_iff)


lemma tickFree_disjoint_setinterleavesptick_appendL :
  ‹tF u1 ⟹ {a. ev a ∈ set u1} ∩ A = {} ⟹ t setinterleaves✓⇘tick_join⇙ ((u2, v), A)
   ⟹ map (ev ∘ of_ev) u1 @ t setinterleaves✓⇘tick_join⇙ ((u1 @ u2, v), A)›
proof (induct u1)
  case Nil
  from Nil.prems(3) show ?case by simp
next
  case (Cons e u1)
  from Cons.prems(1, 2) obtain a
    where ‹e = ev a› ‹a ∉ A› ‹tF u1› ‹{a. ev a ∈ set u1} ∩ A = {} ›
    by (auto simp add: disjoint_iff is_ev_def)
  from Cons.hyps[OF this(3, 4) Cons.prems(3)]
  have ‹map (ev ∘ of_ev) u1 @ t setinterleaves✓⇘tick_join⇙ ((u1 @ u2, v), A)› .
  with ‹e = ev a› ‹a ∉ A›
  show ?case by (cases v)
      (auto simp add: setinterleavingptick_simps comp_def split: eventptick.split)
qed

corollary tickFree_disjoint_setinterleavesptick_appendR :
  ‹⟦tF v1; {a. ev a ∈ set v1} ∩ A = {}; t setinterleaves✓⇘tick_join⇙ ((u, v2), A)⟧
   ⟹ map (ev ∘ of_ev) v1 @ t setinterleaves✓⇘tick_join⇙ ((u, v1 @ v2), A)›
  by (metis setinterleavesptick_sym tickFree_disjoint_setinterleavesptick_appendL)


lemma tickFree_disjoint_setinterleavesptick_append_tailL :
  ‹t @ map (ev ∘ of_ev) u2 setinterleaves✓⇘tick_join⇙ ((u1 @ u2, v), A)›
  if ‹tF u2› ‹{a. ev a ∈ set u2} ∩ A = {}› ‹t setinterleaves✓⇘tick_join⇙ ((u1, v), A)›
proof -
  have ‹t @ map (ev ∘ of_ev) u2 setinterleaves✓⇘tick_join⇙ ((u1 @ u2, v), A) ⟷
        map (ev ∘ of_ev) (rev u2) @ rev t setinterleaves✓⇘tick_join⇙ ((rev u2 @ rev u1, rev v), A)›
    by (subst rev_setinterleavesptick_rev_rev_iff[symmetric])
      (simp add: rev_map)
  also have …
  proof (rule tickFree_disjoint_setinterleavesptick_appendL)
    show ‹tF (rev u2)› by (simp add: that(1))
  next
    show ‹{a. ev a ∈ set (rev u2)} ∩ A = {}› by (simp add: that(2))
  next
    show ‹rev t setinterleaves✓⇘tick_join⇙ ((rev u1, rev v), A)›
      by (simp add: rev_setinterleavesptick_rev_rev_iff that(3))
  qed
  finally show ?thesis .
qed


corollary tickFree_disjoint_setinterleavesptick_append_tailR :
  ‹⟦tF v2; {a. ev a ∈ set v2} ∩ A = {}; t setinterleaves✓⇘tick_join⇙ ((u, v1), A)⟧
   ⟹ t @ map (ev ∘ of_ev) v2 setinterleaves✓⇘tick_join⇙ ((u, v1 @ v2), A)›
  by (metis setinterleavesptick_sym tickFree_disjoint_setinterleavesptick_append_tailL)


lemma disjoint_trace_hide_setinterleavesptick :
  ‹t setinterleaves✓⇘tick_join⇙
   ((trace_hide u (ev ` A), trace_hide v (ev ` A)), S) ⟹
   ∃t'. t = trace_hide t' (ev ` A) ∧
   t' setinterleaves✓⇘tick_join⇙ ((u, v), S)› if ‹A ∩ S = {}›
  for t :: ‹('a, 't) traceptick› and u :: ‹('a, 'r) traceptick› and v :: ‹('a, 's) traceptick›
proof -
  let ?th = trace_hide and ?A = ‹ev ` A›
  show ‹t setinterleaves✓⇘tick_join⇙
        ((?th u ?A, ?th v ?A), S) ⟹ ∃t'. t = ?th t' ?A ∧ t' setinterleaves✓⇘tick_join⇙ ((u, v), S)›
  proof (induct ‹(tick_join, u, S, v)› arbitrary: t u v)
    case Nil_setinterleavingptick_Nil
    then show ?case by simp
  next
    case (ev_setinterleavingptick_Nil a u)
    from ev_setinterleavingptick_Nil.prems
    consider t' where ‹a ∉ S› ‹a ∉ A› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th [] ?A), S)›
    | ‹a ∈ A› ‹t setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th [] ?A), S)›
      by (auto split: if_split_asm)
    thus ?case
    proof cases
      fix t' assume ‹a ∉ S› ‹a ∉ A› ‹t = ev a # t'›
        ‹t' setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th [] ?A), S)›
      from ev_setinterleavingptick_Nil.hyps[OF this(1, 4)] obtain t''
        where ‹t' = ?th t'' ?A ∧ t'' setinterleaves✓⇘tick_join⇙ ((u, []), S)› ..
      hence ‹t = ?th (ev a # t'') ?A ∧ ev a # t'' setinterleaves✓⇘tick_join⇙ ((ev a # u, []), S)›
        by (simp add: ‹a ∉ A› ‹a ∉ S› ‹t = ev a # t'› image_iff[of ‹ev _›])
      thus ?case ..
    next
      assume ‹a ∈ A›
      with ‹A ∩ S = {}› have ‹a ∉ S› by blast
      moreover assume ‹t setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th [] ?A), S)›
      ultimately obtain t' where ‹t = ?th t' ?A› ‹t' setinterleaves✓⇘tick_join⇙ ((u, []), S)›
        using ev_setinterleavingptick_Nil.hyps by blast
      hence ‹t = ?th (ev a # t') ?A ∧ ev a # t' setinterleaves✓⇘tick_join⇙ ((ev a # u, []), S)›
        by (simp add: ‹a ∈ A› ‹a ∉ S›)
      thus ?case ..
    qed
  next
    case (tick_setinterleavingptick_Nil r u)
    from tick_setinterleavingptick_Nil.prems have False by (simp add: image_iff[of ‹✓(_)›])
    thus ?case ..
  next
    case (Nil_setinterleavingptick_ev b v)
    from Nil_setinterleavingptick_ev.prems
    consider t' where ‹b ∉ S› ‹b ∉ A› ‹t = ev b # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((?th [] ?A, ?th v ?A), S)›
    | ‹b ∈ A› ‹t setinterleaves✓⇘tick_join⇙ ((?th [] ?A, ?th v ?A), S)›
      by (auto split: if_split_asm)
    thus ?case
    proof cases
      fix t' assume ‹b ∉ S› ‹b ∉ A› ‹t = ev b # t'›
        ‹t' setinterleaves✓⇘tick_join⇙ ((?th [] ?A, ?th v ?A), S)›
      from Nil_setinterleavingptick_ev.hyps[OF this(1, 4)] obtain t''
        where ‹t' = ?th t'' ?A ∧ t'' setinterleaves✓⇘tick_join⇙ (([], v), S)› ..
      hence ‹t = ?th (ev b # t'') ?A ∧ ev b # t'' setinterleaves✓⇘tick_join⇙ (([], ev b # v), S)›
        by (simp add: ‹b ∉ A› ‹b ∉ S› ‹t = ev b # t'› image_iff[of ‹ev _›])
      thus ?case ..
    next
      assume ‹b ∈ A›
      with ‹A ∩ S = {}› have ‹b ∉ S› by blast
      moreover assume ‹t setinterleaves✓⇘tick_join⇙ ((?th [] ?A, ?th v ?A), S)›
      ultimately obtain t' where ‹t = ?th t' ?A› ‹t' setinterleaves✓⇘tick_join⇙ (([], v), S)›
        using Nil_setinterleavingptick_ev.hyps by blast
      hence ‹t = ?th (ev b # t') ?A ∧ ev b # t' setinterleaves✓⇘tick_join⇙ (([], ev b # v), S)›
        by (simp add: ‹b ∈ A› ‹b ∉ S›)
      thus ?case ..
    qed
  next
    case (Nil_setinterleavingptick_tick s v)
    from Nil_setinterleavingptick_tick.prems have False by (simp add: image_iff[of ‹✓(_)›])
    thus ?case ..
  next
    case (ev_setinterleavingptick_ev a u b v)
    show ?case
    proof (cases ‹a ∈ A›; cases ‹b ∈ A›)
      assume ‹a ∈ A› ‹b ∈ A›
      with ev_setinterleavingptick_ev.prems
      have * : ‹t setinterleaves✓⇘tick_join⇙ ((?th (ev a # u) ?A, ?th v ?A), S)›
        ‹t setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th (ev b # v) ?A), S)› by simp_all
      from ‹A ∩ S = {}› ‹a ∈ A› ‹b ∈ A› have ‹a ∉ S› ‹b ∉ S› by blast+
      from ev_setinterleavingptick_ev.hyps(4)[OF this "*"(2)]
        ev_setinterleavingptick_ev.hyps(5)[OF this "*"(1)]
      obtain t' where ‹t = ?th t' ?A›
        ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), S) ∨
         t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), S)› by blast
      hence ‹t = ?th (ev b # t') ?A ∧ ev b # t' setinterleaves✓⇘tick_join⇙ ((ev a # u, ev b # v), S) ∨
             t = ?th (ev a # t') ?A ∧ ev a # t' setinterleaves✓⇘tick_join⇙ ((ev a # u, ev b # v), S)›
        by (auto simp add: ‹a ∈ A› ‹b ∈ A› ‹a ∉ S› ‹b ∉ S›)
      thus ?case by blast
    next
      assume ‹a ∈ A› ‹b ∉ A›
      with ev_setinterleavingptick_ev.prems
      have * : ‹t setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th (ev b # v) ?A), S)› by simp
      from ‹A ∩ S = {}› ‹a ∈ A› have ‹a ∉ S› by blast
      from ev_setinterleavingptick_ev.hyps(3)[OF ‹a ∉ S› _ "*"(1)]
        ev_setinterleavingptick_ev.hyps(4)[OF ‹a ∉ S› _ "*"] obtain t'
        where ‹t = ?th t' ?A› ‹t' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), S)› by blast
      hence ‹t = ?th (ev a # t') ?A ∧
               ev a # t' setinterleaves✓⇘tick_join⇙ ((ev a # u, ev b # v), S)›
        by (simp add: ‹a ∈ A› ‹a ∉ S›)
      thus ?case ..
    next
      assume ‹a ∉ A› ‹b ∈ A›
      with ev_setinterleavingptick_ev.prems
      have * : ‹t setinterleaves✓⇘tick_join⇙ ((?th (ev a # u) ?A, ?th v ?A), S)› by simp
      from ‹A ∩ S = {}› ‹b ∈ A› have ‹b ∉ S› by blast
      from ev_setinterleavingptick_ev.hyps(2)[OF _ ‹b ∉ S› "*"]
        ev_setinterleavingptick_ev.hyps(5)[OF _ ‹b ∉ S› "*"] obtain t'
        where ‹t = ?th t' ?A› ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), S)› by blast
      hence ‹t = ?th (ev b # t') ?A ∧
             ev b # t' setinterleaves✓⇘tick_join⇙ ((ev a # u, ev b # v), S)›
        by (simp add: ‹b ∈ A› ‹b ∉ S›)
      thus ?case ..
    next
      assume ‹a ∉ A› ‹b ∉ A›
      hence ‹?th (ev a # u) ?A = ev a # ?th u ?A›
        ‹?th (ev b # v) ?A = ev b # ?th v ?A› by auto
      from ev_setinterleavingptick_ev.prems[unfolded this]
      have ‹t setinterleaves✓⇘tick_join⇙ ((ev a # ?th u ?A, ev b # ?th v ?A), S)› .
      then consider (mv_both) t' where ‹a ∈ S› ‹b ∈ S› ‹a = b› ‹t = ev a # t'›
        ‹t' setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th v ?A), S)›
      | (mvL) t' where ‹a ∉ S› ‹t = ev a # t'›
        ‹t' setinterleaves✓⇘tick_join⇙ ((?th u ?A, ev b # ?th v ?A), S)›
      | (mvR) t' where ‹b ∉ S› ‹t = ev b # t'›
        ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # ?th u ?A, ?th v ?A), S)›
        by (auto split: if_split_asm)
      thus ?case
      proof cases
        case mv_both
        from ev_setinterleavingptick_ev.hyps(1)[OF mv_both(1-3, 5)] obtain t''
          where ‹t' = ?th t'' ?A ∧ t'' setinterleaves✓⇘tick_join⇙ ((u, v), S)› ..
        hence ‹t = ?th (ev b # t'') ?A ∧ ev b # t'' setinterleaves✓⇘tick_join⇙ ((ev a # u, ev b # v), S)›
          by (simp add: mv_both(2-4) ‹b ∉ A› image_iff[of ‹ev _›] )
        thus ?thesis ..
      next
        case mvL
        from ev_setinterleavingptick_ev.hyps(3, 4)
          [OF mvL(1) _ mvL(3)[folded ‹?th (ev b # v) ?A = ev b # ?th v ?A›]]
        obtain t'' where ‹t' = ?th t'' ?A›
          ‹t'' setinterleaves✓⇘tick_join⇙ ((u, ev b # v), S)› by blast
        hence ‹t = ?th (ev a # t'') ?A ∧
               ev a # t'' setinterleaves✓⇘tick_join⇙ ((ev a # u, ev b # v), S)›
          by (simp add: mvL(1, 2) ‹a ∉ A› image_iff[of ‹ev _›]) 
        thus ?thesis ..
      next
        case mvR
        from ev_setinterleavingptick_ev.hyps(2, 5)
          [OF _ mvR(1) mvR(3)[folded ‹?th (ev a # u) ?A = ev a # ?th u ?A›]]
        obtain t'' where ‹t' = ?th t'' ?A›
          ‹t'' setinterleaves✓⇘tick_join⇙ ((ev a # u, v), S)› by blast
        hence ‹t = ?th (ev b # t'') ?A ∧
               ev b # t'' setinterleaves✓⇘tick_join⇙ ((ev a # u, ev b # v), S)›
          by (simp add: mvR(1, 2) ‹b ∉ A› image_iff[of ‹ev _›]) 
        thus ?thesis ..
      qed
    qed
  next
    case (ev_setinterleavingptick_tick a u s v)
    from ev_setinterleavingptick_tick.prems
    consider t' where ‹a ∉ S› ‹a ∉ A› ‹t = ev a # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th (✓(s) # v) ?A), S)›
    | ‹a ∈ A› ‹t setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th (✓(s) # v) ?A), S)›
      by (auto split: if_split_asm)
    thus ?case
    proof cases
      fix t' assume ‹a ∉ S› ‹a ∉ A› ‹t = ev a # t'›
        ‹t' setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th (✓(s) # v) ?A), S)›
      from ev_setinterleavingptick_tick.hyps[OF this(1, 4)] obtain t''
        where ‹t' = ?th t'' ?A› ‹t'' setinterleaves✓⇘tick_join⇙ ((u, ✓(s) # v), S)› by blast
      hence ‹t = ?th (ev a # t'') ?A ∧
             ev a # t'' setinterleaves✓⇘tick_join⇙ ((ev a # u, ✓(s) # v), S)›
        by (simp add: ‹a ∉ A› ‹a ∉ S› ‹t = ev a # t'› image_iff[of ‹ev _›])
      thus ?case ..
    next
      assume ‹a ∈ A›
      with ‹A ∩ S = {}› have ‹a ∉ S› by blast
      moreover assume ‹t setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th (✓(s) # v) ?A), S)›
      ultimately obtain t' where ‹t = ?th t' ?A› ‹t' setinterleaves✓⇘tick_join⇙ ((u, ✓(s) # v), S)›
        using ev_setinterleavingptick_tick.hyps by blast
      hence ‹t = ?th (ev a # t') ?A ∧ ev a # t' setinterleaves✓⇘tick_join⇙ ((ev a # u, ✓(s) # v), S)›
        by (simp add: ‹a ∈ A› ‹a ∉ S›)
      thus ?case ..
    qed
  next
    case (tick_setinterleavingptick_ev r u b v)
    from tick_setinterleavingptick_ev.prems
    consider t' where ‹b ∉ S› ‹b ∉ A› ‹t = ev b # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((?th (✓(r) # u) ?A, ?th v ?A), S)›
    | ‹b ∈ A› ‹t setinterleaves✓⇘tick_join⇙ ((?th (✓(r) # u) ?A, ?th v ?A), S)›
      by (auto split: if_split_asm)
    thus ?case
    proof cases
      fix t' assume ‹b ∉ S› ‹b ∉ A› ‹t = ev b # t'›
        ‹t' setinterleaves✓⇘tick_join⇙ ((?th (✓(r) # u) ?A, ?th v ?A), S)›
      from tick_setinterleavingptick_ev.hyps[OF this(1, 4)] obtain t''
        where ‹t' = ?th t'' ?A› ‹t'' setinterleaves✓⇘tick_join⇙ ((✓(r) # u, v), S)› by blast
      hence ‹t = ?th (ev b # t'') ?A ∧
             ev b # t'' setinterleaves✓⇘tick_join⇙ ((✓(r) # u, ev b # v), S)›
        by (simp add: ‹b ∉ A› ‹b ∉ S› ‹t = ev b # t'› image_iff[of ‹ev _›])
      thus ?case ..
    next
      assume ‹b ∈ A›
      with ‹A ∩ S = {}› have ‹b ∉ S› by blast
      moreover assume ‹t setinterleaves✓⇘tick_join⇙ ((?th (✓(r) # u) ?A, ?th v ?A), S)›
      ultimately obtain t' where ‹t = ?th t' ?A› ‹t' setinterleaves✓⇘tick_join⇙ ((✓(r) # u, v), S)›
        using tick_setinterleavingptick_ev.hyps by blast
      hence ‹t = ?th (ev b # t') ?A ∧ ev b # t' setinterleaves✓⇘tick_join⇙ ((✓(r) # u, ev b # v), S)›
        by (simp add: ‹b ∈ A› ‹b ∉ S›)
      thus ?case ..
    qed
  next
    case (tick_setinterleavingptick_tick r u s v)
    from tick_setinterleavingptick_tick.prems obtain r_s t'
      where ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›
        ‹t' setinterleaves✓⇘tick_join⇙ ((?th u ?A, ?th v ?A), S)›
      by (auto split: if_split_asm option.split_asm)
    from tick_setinterleavingptick_tick.hyps[OF this(1, 3)] obtain t''
      where ‹t' = ?th t'' ?A› ‹t'' setinterleaves✓⇘tick_join⇙ ((u, v), S)› by blast
    hence ‹t = ?th (✓(r_s) # t'') ?A ∧
           ✓(r_s) # t'' setinterleaves✓⇘tick_join⇙ ((✓(r) # u, ✓(s) # v), S)›
      by (simp add: ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'› image_iff[of ‹✓(_)›])
    thus ?case ..
  qed
qed



lemma setinterleavesptick_inj_map_map_eventptick_iff_weak :
  ‹map (map_eventptick f id) t setinterleaves✓⇘tick_join⇙
   ((map (map_eventptick f id) u, map (map_eventptick f id) v), f ` A) ⟷
   t setinterleaves✓⇘tick_join⇙ ((u, v), A)› if ‹inj f›
  by (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    (auto simp add: image_iff map_eventptick_eq_ev_iff map_eventptick_eq_tick_iff
      dest!: injD[OF ‹inj f›] split: option.split_asm)


lemma setinterleavesptick_inj_map_map_eventptick_iff_strong :
  ‹t setinterleaves✓⇘tick_join⇙
   ((map (map_eventptick f id) u, map (map_eventptick f id) v), f ` A) ⟷
    (∃t'. t = map (map_eventptick f id) t' ∧
    t' setinterleaves✓⇘tick_join⇙ ((u, v), A))› if ‹inj f›
  ― ‹We could probably prove a stronger version with
     term‹inj_on f (A ∪ {a. ev a ∈ set u ∨ ev a ∈ set v})› instead of term‹inj f›.›
proof -
  let ?map = ‹map (map_eventptick f id)›
  have ‹t setinterleaves✓⇘tick_join⇙ ((?map u, ?map v), f ` A) ⟹ ∃t'. t = ?map t'›
  proof (induct ‹(tick_join, u, A, v)› arbitrary: t u v)
    case Nil_setinterleavingptick_Nil
    thus ?case by simp
  next
    case (ev_setinterleavingptick_Nil a u)
    from ev_setinterleavingptick_Nil.prems obtain t'
      where ‹a ∉ A› ‹t = ev (f a) # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((?map u, ?map []), f ` A)›
      by (auto split: if_split_asm)
    from ev_setinterleavingptick_Nil.hyps[OF this(1, 3)]
    obtain t'' where ‹t' = ?map t''› ..
    hence ‹t = ?map (ev a # t'')› by (simp add: ‹t = ev (f a) # t'›)
    thus ?case ..
  next
    case (tick_setinterleavingptick_Nil r u)
    from tick_setinterleavingptick_Nil.prems have False by simp
    thus ?case ..
  next
    case (Nil_setinterleavingptick_ev b v)
    from Nil_setinterleavingptick_ev.prems obtain t'
      where ‹b ∉ A› ‹t = ev (f b) # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((?map [], ?map v), f ` A)›
      by (auto split: if_split_asm)
    from Nil_setinterleavingptick_ev.hyps[OF this(1, 3)]
    obtain t'' where ‹t' = ?map t''› ..
    hence ‹t = ?map (ev b # t'')› by (simp add: ‹t = ev (f b) # t'›)
    thus ?case ..
  next
    case (Nil_setinterleavingptick_tick s v)
    from Nil_setinterleavingptick_tick.prems have False by simp
    thus ?case ..
  next
    case (ev_setinterleavingptick_ev a u b v)
    from ev_setinterleavingptick_ev.prems
    consider (mv_left) t' where ‹a ∉ A› ‹t = ev (f a) # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((?map u, ?map (ev b # v)), f ` A)›
    | (mv_right) t' where ‹b ∉ A› ‹t = ev (f b) # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((?map (ev a # u), ?map v), f ` A)›
    | (mv_both) t' where ‹a ∈ A› ‹b ∈ A› ‹a = b› ‹t = ev (f b) # t'›
      ‹t' setinterleaves✓⇘tick_join⇙ ((?map u, ?map v), f ` A)›
      by (auto simp add: image_iff split: if_split_asm dest!: injD[OF ‹inj f›])
    thus ?case
    proof cases
      case mv_left
      from ev_setinterleavingptick_ev.hyps(3, 4)[OF mv_left(1) _ mv_left(3)]
      obtain t'' where ‹t' = ?map t''› by blast
      hence ‹t = ?map (ev a # t'')› by (simp add: mv_left(2))
      thus ?thesis ..
    next
      case mv_right
      from ev_setinterleavingptick_ev.hyps(2, 5)[OF _ mv_right(1, 3)]
      obtain t'' where ‹t' = ?map t''› by blast
      hence ‹t = ?map (ev b # t'')› by (simp add: mv_right(2))
      thus ?thesis ..
    next
      case mv_both
      from ev_setinterleavingptick_ev.hyps(1)[OF mv_both(1-3, 5)]
      obtain t'' where ‹t' = ?map t''› ..
      hence ‹t = ?map (ev b # t'')› by (simp add: mv_both(4))
      thus ?thesis ..
    qed
  next
    case (ev_setinterleavingptick_tick a u s v)
    from ev_setinterleavingptick_tick.prems obtain t'
      where ‹a ∉ A› ‹t = ev (f a) # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((?map u, ?map (✓(s) # v)), f ` A)›
      by (auto split: if_split_asm)
    from ev_setinterleavingptick_tick.hyps[OF this(1, 3)]
    obtain t'' where ‹t' = ?map t''› ..
    hence ‹t = ?map (ev a # t'')› by (simp add: ‹t = ev (f a) # t'›)
    thus ?case ..
  next
    case (tick_setinterleavingptick_ev r u b v)
    from tick_setinterleavingptick_ev.prems obtain t'
      where ‹b ∉ A› ‹t = ev (f b) # t'› ‹t' setinterleaves✓⇘tick_join⇙ ((?map (✓(r) # u), ?map v), f ` A)›
      by (auto split: if_split_asm)
    from tick_setinterleavingptick_ev.hyps[OF this(1, 3)]
    obtain t'' where ‹t' = ?map t''› ..
    hence ‹t = ?map (ev b # t'')› by (simp add: ‹t = ev (f b) # t'›)
    thus ?case ..
  next
    case (tick_setinterleavingptick_tick r u s v)
    from tick_setinterleavingptick_tick.prems obtain r_s t'
      where ‹tick_join r s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›
        ‹t' setinterleaves✓⇘tick_join⇙ ((?map u, ?map v), f ` A)›
      by (auto split: option.split_asm)
    from tick_setinterleavingptick_tick.hyps[OF this(1, 3)]
    obtain t'' where ‹t' = ?map t''› ..
    hence ‹t = ?map (✓(r_s) # t'')› by (simp add: ‹t = ✓(r_s) # t'›)
    thus ?case ..
  qed
  with setinterleavesptick_inj_map_map_eventptick_iff_weak[OF ‹inj f›]
  show ?thesis by blast
qed




lemma setinterleavesptick_append_setinterleavesptick :
  ‹t1 @ t2 setinterleaves✓⇘tick_join⇙ ((u1 @ u2, v1 @ v2), A)›
  if ‹t1 setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
    and ‹t2 setinterleaves✓⇘tick_join⇙ ((u2, v2), A)›
  using that(1) proof (induct ‹(tick_join, u1, A, v1)› arbitrary: t1 u1 v1)
  case Nil_setinterleavingptick_Nil
  from Nil_setinterleavingptick_Nil.prems(1) have ‹t1 = []› by simp
  with that(2) show ?case by simp
next
  case (ev_setinterleavingptick_Nil a u1)
  from ev_setinterleavingptick_Nil.prems(1) obtain t1' where ‹a ∉ A› ‹t1 = ev a # t1'›
    ‹t1' setinterleaves✓⇘tick_join⇙ ((u1, []), A)› by (auto split: if_split_asm)
  from ev_setinterleavingptick_Nil.hyps[OF this(1, 3)]
  show ?case
    by (cases v2)
      (auto simp add: ‹a ∉ A› ‹t1 = ev a # t1'› setinterleavingptick_simps
        split: eventptick.split)
next
  case (tick_setinterleavingptick_Nil r u1)
  from tick_setinterleavingptick_Nil.prems(1) have False by simp
  thus ?case ..
next
  case (Nil_setinterleavingptick_ev b v1)
  from Nil_setinterleavingptick_ev.prems(1) obtain t1' where ‹b ∉ A› ‹t1 = ev b # t1'›
    ‹t1' setinterleaves✓⇘tick_join⇙ (([], v1), A)› by (auto split: if_split_asm)
  from Nil_setinterleavingptick_ev.hyps[OF this(1, 3)]
  show ?case
    by (cases u2)
      (auto simp add: ‹b ∉ A› ‹t1 = ev b # t1'› setinterleavingptick_simps
        split: eventptick.split)
next
  case (Nil_setinterleavingptick_tick s v1)
  from Nil_setinterleavingptick_tick.prems(1) have False by simp
  thus ?case ..
next
  case (ev_setinterleavingptick_ev a u1 b v1)
  from ev_setinterleavingptick_ev.prems
  consider (mv_both) t' where ‹a ∈ A› ‹b ∈ A› ‹a = b› ‹t1 = ev a # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
  | (mvL) t' where ‹a ∉ A› ‹t1 = ev a # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((u1, ev b # v1), A)›
  | (mvR) t' where ‹b ∉ A› ‹t1 = ev b # t'›
    ‹t' setinterleaves✓⇘tick_join⇙ ((ev a # u1, v1), A)›
    by (auto split: if_split_asm)
  thus ?case
  proof cases
    case mv_both
    from ev_setinterleavingptick_ev.hyps(1)[OF mv_both(1-3, 5)]
    show ?thesis by (simp add: mv_both(2-4))
  next
    case mvL
    from ev_setinterleavingptick_ev.hyps(3, 4)[OF mvL(1) _ mvL(3)]
    show ?thesis by (simp add: mvL(1, 2))
  next
    case mvR
    from ev_setinterleavingptick_ev.hyps(2, 5)[OF _ mvR(1, 3)]
    show ?thesis by (simp add: mvR(1, 2))
  qed
next
  case (ev_setinterleavingptick_tick a u1 s v1)
  from ev_setinterleavingptick_tick.prems(1)
  obtain t1' where ‹a ∉ A› ‹t1 = ev a # t1'›
    ‹t1' setinterleaves✓⇘tick_join⇙ ((u1, ✓(s) # v1), A)› by (auto split: if_split_asm)
  from ev_setinterleavingptick_tick.hyps[OF this(1, 3)]
  show ?case
    by (cases v2)
      (auto simp add: ‹a ∉ A› ‹t1 = ev a # t1'› setinterleavingptick_simps
        split: eventptick.split)
next
  case (tick_setinterleavingptick_ev r u1 b v1)
  from tick_setinterleavingptick_ev.prems(1) obtain t1' where ‹b ∉ A› ‹t1 = ev b # t1'›
    ‹t1' setinterleaves✓⇘tick_join⇙ ((✓(r) # u1, v1), A)› by (auto split: if_split_asm)
  from tick_setinterleavingptick_ev.hyps[OF this(1, 3)]
  show ?case
    by (cases u2)
      (auto simp add: ‹b ∉ A› ‹t1 = ev b # t1'› setinterleavingptick_simps
        split: eventptick.split)
next
  case (tick_setinterleavingptick_tick r u1 s v1)
  from tick_setinterleavingptick_tick.prems(1) obtain r_s t1'
    where ‹tick_join r s = ⌊r_s⌋› ‹t1 = ✓(r_s) # t1'›
      ‹t1' setinterleaves✓⇘tick_join⇙ ((u1, v1), A)›
    by (auto split: option.split_asm)
  from tick_setinterleavingptick_tick.hyps[OF this(1, 3)]
  show ?case by (simp add: ‹tick_join r s = ⌊r_s⌋› ‹t1 = ✓(r_s) # t1'›)
qed




lemma setinterleavesptick_set_subsetL :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   {a. ev a ∈ set (drop n u)} ⊆ {a. ev a ∈ set (drop n t)}›
proof (induct t arbitrary: n u v)
  case Nil
  thus ?case by (auto dest: Nil_setinterleavesptick)
next
  case (Cons e t)
  from Cons.prems consider (mv_left) a u' where ‹a ∉ A› ‹e = ev a› ‹u = ev a # u'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u', v), A)›
  | (mv_right) a v' where ‹a ∉ A› ‹e = ev a› ‹v = ev a # v'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u, v'), A)›
  | (mv_both_ev) a u' v' where ‹a ∈ A› ‹e = ev a› ‹u = ev a # u'› ‹v = ev a # v'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
  | (mv_both_tick) r s r_s u' v' where ‹tick_join r s = ⌊r_s⌋› ‹e = ✓(r_s)›
    ‹u = ✓(r) # u'› ‹v = ✓(s) # v'› ‹t setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
    by (cases e) (auto elim: Cons_ev_setinterleavesptickE Cons_tick_setinterleavesptickE)
  thus ?case
  proof cases
    case mv_left
    from Cons.hyps[OF mv_left(4)] show ?thesis
      by (cases n, simp_all add: mv_left(2, 3) subset_iff) (metis drop0)
  next
    case mv_right
    from Cons.hyps[OF mv_right(4)] show ?thesis
      by (cases n, simp_all add: subset_iff)
        (metis drop0, meson Suc_n_not_le_n in_mono nle_le set_drop_subset_set_drop)
  next
    case mv_both_ev
    from Cons.hyps[OF mv_both_ev(5)] show ?thesis
      by (cases n, simp_all add: mv_both_ev(2, 3) subset_iff) (metis drop0)
  next
    case mv_both_tick
    from Cons.hyps[OF mv_both_tick(5)] show ?thesis
      by (cases n, simp_all add: mv_both_tick(3) subset_iff) (metis drop0)
  qed
qed

lemma setinterleavesptick_set_subsetR :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   {a. ev a ∈ set (drop n v)} ⊆ {a. ev a ∈ set (drop n t)}›
  by (rule setinterleavesptick_set_subsetL)
    (fact setinterleavesptick_sym[THEN iffD2])









section ‹Synchronization Product›

subsection ‹Definition›

definition super_ref_Syncptick ::
  ‹['r ⇒ 's ⇒ 't option, ('a, 'r) refusalptick, 'a set, ('a, 's) refusalptick] ⇒ ('a, 't) refusalptick›
  where ‹super_ref_Syncptick tick_join X_P A X_Q ≡
         {ev a |a. ev a ∈ X_P ∧ ev a ∈ X_Q ∨ (a ∈ A ∧ (ev a ∈ X_P ∨ ev a ∈ X_Q))} ∪
         {✓(r_s) |r s r_s. tick_join r s = ⌊r_s⌋ ∧ (✓(r) ∈ X_P ∨ ✓(s) ∈ X_Q)} ∪
         ―‹This is the last addition: since we generalize with the parameter term‹tick_join›,
            we must add the following term to refuse the unreachable ticks.›
         {✓(r_s) |r_s. ∄r s. tick_join r s = ⌊r_s⌋}›



text ‹
For proving that the invariant const‹is_process› is preserved, we will need a kind
of injectivity for the parameter term‹tick_join›. We implement this through a ⬚‹locale›.›

locale Syncptick_locale =
  fixes tick_join :: ‹'r ⇒ 's ⇒ 't option› (infixl ‹⊗✓› 100)
  assumes inj_tick_join :
    ‹r ⊗✓ s = ⌊r_s⌋ ⟹ r' ⊗✓ s' = ⌊r_s⌋ ⟹ r' = r ∧ s' = s›
begin


sublocale Syncptick_locale_sym : Syncptick_locale ‹λs r. r ⊗✓ s›
  by unfold_locales (simp add: inj_tick_join)


lift_definition Syncptick ::
  ‹[('a, 'r) processptick, 'a set, ('a, 's) processptick] ⇒ ('a, 't) processptick›
  (‹(_ ⟦_⟧✓ _)› [70, 0, 71] 70)
  is ‹λP A Q.
      ({(t, X). ∃t_P t_Q X_P X_Q.
                (t_P, X_P) ∈ ℱ P ∧ (t_Q, X_Q) ∈ ℱ Q ∧
                t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
                X ⊆ super_ref_Syncptick (⊗✓) X_P A X_Q} ∪
       {(t @ u, X) |t u t_P t_Q X.
                    ftF u ∧ (tF t ∨ u = []) ∧ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
                    (t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q)},
       {t @ u |t u t_P t_Q.
               ftF u ∧ (tF t ∨ u = []) ∧ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
               (t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q)})›
proof -
  show ‹?thesis P A Q›
    (is ‹is_process(?f, ?d)›) for P and Q :: ‹('a, 's) processptick› and A
  proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv, intro conjI impI allI)
    have ‹([], {}) ∈ ℱ P› and ‹([], {}) ∈ ℱ Q› by (simp_all add: is_processT1)
    with Nil_setinterleavingptick_Nil show ‹([], {}) ∈ ?f› by fast
  next 
    show ‹(t, X) ∈ ?f ⟹ ftF t› for t X
      by simp (metis (no_types, opaque_lifting) D_T F_imp_front_tickFree T_imp_front_tickFree
          append.right_neutral front_tickFree_append front_tickFree_setinterleavesptick_iff)
  next
    fix t u assume ‹(t @ u, {}) ∈ ?f›
    then consider (fail) t_P t_Q X_P X_Q where 
      ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q› ‹t @ u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A)›
    | (div) t' u' t_P t_Q where
      ‹t @ u = t' @ u'› ‹ftF u'› ‹tF t' ∨ u' = []› ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A)›
      ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q› by simp blast
    thus ‹(t, {}) ∈ ?f›
    proof cases
      case fail
      from fail(3) obtain t' u'
        where * : ‹t' ≤ t_P› ‹u' ≤ t_Q› ‹t setinterleaves✓⇘(⊗✓)⇙ ((t', u'), A)›
        by (auto dest!: append_setinterleavesptick intro: prefixI)
      from fail(1, 2) "*"(1, 2) F_T is_processT3_TR have ‹t' ∈ 𝒯 P› ‹u' ∈ 𝒯 Q› by blast+
      thus ‹(t, {}) ∈ ?f› by simp (metis T_F_spec "*"(3))
    next
      case div
      show ‹(t, {}) ∈ ?f›
      proof (cases ‹length t' ≤ length t›)
        assume ‹length t' ≤ length t›
        with div(1-3) have ‹ftF (take (length t - length t') u') ∧
                            (tF t' ∨ take (length t - length t') u' = []) ∧
                            t = t' @ take (length t - length t') u'›
          by (simp add: append_eq_conv_conj)
            (metis append_take_drop_id front_tickFree_dw_closed)
        with div(4, 5) show ‹(t, {}) ∈ ?f› by blast
      next
        assume ‹¬ length t' ≤ length t›
        with div obtain r' where ‹t' = t @ r'›
          by (metis append_eq_append_conv_if append_take_drop_id)
        with div(4) obtain t'' u''
          where * : ‹t'' ≤ t_P› ‹u'' ≤ t_Q› ‹t setinterleaves✓⇘(⊗✓)⇙ ((t'', u''), A)›
          by (auto dest!: append_setinterleavesptick intro: prefixI)
        from "*"(1, 2) have ‹t'' ∈ 𝒯 P ∧ u'' ∈ 𝒯 Q› by (meson D_T div(5) is_processT3_TR)
        hence $ : ‹(t'', {}) ∈ ℱ P› ‹(u'', {}) ∈ ℱ Q› by (simp_all add: T_F)
        have $$ : ‹{ev a| a. ev a ∈ {} ∧ ev a ∈ {} ∨ (a ∈ A ∧ (ev a ∈ {} ∨ ev a ∈ {}))} ∪
                   {✓(r ⊗✓ s)| r s. ✓(r) ∈ {} ∨ ✓(s) ∈ {}} = {}› by simp
        show ‹(t, {}) ∈ ?f› by (auto intro!: "$" "*"(3))
      qed
    qed
  next
    { fix t X Y
      assume ‹(t, Y) ∈ ?f ∧ X ⊆ Y›
      then consider ‹t ∈ ?d›
        | (fail) t_P t_Q X_P X_Q where
          ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A)›
          ‹Y ⊆ super_ref_Syncptick (⊗✓) X_P A X_Q› by blast
      thus ‹(t, X) ∈ ?f›
      proof cases
        show ‹t ∈ ?d ⟹ (t, X) ∈ ?f› by blast
      next
        case fail
        define X_P' where ‹X_P' ≡ X_P ∩ ({ev a| a. ev a ∈ X} ∪
                                          {✓(r)| r s r_s. r ⊗✓ s = ⌊r_s⌋ ∧ ✓(r_s) ∈ X})›
        define X_Q' where ‹X_Q' ≡ X_Q ∩ ({ev a| a. ev a ∈ X} ∪
                                          {✓(s)| r s r_s. r ⊗✓ s = ⌊r_s⌋ ∧ ✓(r_s) ∈ X})›
        have ‹(t_P, X_P') ∈ ℱ P› unfolding X_P'_def by (meson fail(1) inf_le1 process_charn)
        moreover have ‹(t_Q, X_Q') ∈ ℱ Q› unfolding X_Q'_def by (meson fail(2) inf_le1 process_charn)
        moreover have ‹X ⊆ super_ref_Syncptick (⊗✓) X_P' A X_Q'›
          by (subst ‹(t, Y) ∈ ?f ∧ X ⊆ Y›[THEN conjunct2, THEN Int_absorb1, symmetric])
            (use fail(4) in ‹fastforce simp add: X_P'_def X_Q'_def subset_iff super_ref_Syncptick_def›)
        ultimately show ‹(t, X) ∈ ?f› using fail(3) by simp blast
      qed } note processT4 = this

    fix t X Y
    assume ‹(t, X) ∈ ?f ∧ (∀e. e ∈ Y ⟶ (t @ [e], {}) ∉ ?f)›
    then consider ‹t ∈ ?d› | ‹(t, X) ∈ ?f ∧ t ∉ ?d› by linarith
    thus ‹(t, X ∪ Y) ∈ ?f›
    proof cases
      show ‹t ∈ ?d ⟹ (t, X ∪ Y) ∈ ?f› by blast
    next
      assume ‹(t, X) ∈ ?f ∧ t ∉ ?d›
      then obtain t_P X_P t_Q X_Q
        where assms : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A)›
          ‹X ⊆ super_ref_Syncptick (⊗✓) X_P A X_Q› by blast
      have assms5 : ‹e ∈ Y ⟹ t @ [e] setinterleaves✓⇘(⊗✓)⇙ ((t', u'), A) ⟹
                     ((t', {}) ∈ ℱ P ⟶ (u', {}) ∉ ℱ Q) ∧
                     ((u', {}) ∈ ℱ Q ⟶ (t', {}) ∉ ℱ P)› for e t' u'
        using ‹(t, X) ∈ ?f ∧ (∀e. e ∈ Y ⟶ (t @ [e], {}) ∉ ?f)› by auto

      define Y_ev_inside and Y_ev_notin and Y_tick
        where * : ‹Y_ev_inside ≡ {a. ev a ∈ Y ∧ a ∈ A}›
          ‹Y_ev_notin  ≡ {a. ev a ∈ Y ∧ a ∉ A}›
          ‹Y_tick      ≡ {r_s |r s r_s. r ⊗✓ s = ⌊r_s⌋ ∧ ✓(r_s) ∈ Y}›

      define Y_ev_inside_P and Y_ev_inside_Q and Y_ev_notin_P
        and Y_ev_notin_Q and Y_tick_P and Y_tick_Q
        where ** : ‹Y_ev_inside_P ≡ {a∈Y_ev_inside. (t_P @ [ev a], {}) ∉ ℱ P}›
          ‹Y_ev_inside_Q ≡ {a∈Y_ev_inside. (t_Q @ [ev a], {}) ∉ ℱ Q}›
          ‹Y_ev_notin_P  ≡ {a∈Y_ev_notin.  (t_P @ [ev a], {}) ∉ ℱ P}›
          ‹Y_ev_notin_Q  ≡ {a∈Y_ev_notin.  (t_Q @ [ev a], {}) ∉ ℱ Q}›
          ‹Y_tick_P      ≡ {r_s∈Y_tick. ∃r s. r ⊗✓ s = ⌊r_s⌋ ∧ (t_P @ [✓(r)], {}) ∉ ℱ P}›
          ‹Y_tick_Q      ≡ {r_s∈Y_tick. ∃r s. r ⊗✓ s = ⌊r_s⌋ ∧ (t_Q @ [✓(s)], {}) ∉ ℱ Q}›

      have "€" : ‹∀a∈Y_ev_inside. (t_P @ [ev a], {}) ∉ ℱ P ∨ (t_Q @ [ev a], {}) ∉ ℱ Q›
      proof (rule ccontr)
        assume ‹¬ (∀a∈Y_ev_inside. (t_P @ [ev a], {}) ∉ ℱ P ∨ (t_Q @ [ev a], {}) ∉ ℱ Q)›
        then obtain a where facts : ‹a ∈ A› ‹ev a ∈ Y› ‹(t_P @ [ev a], {}) ∈ ℱ P›
          ‹(t_Q @ [ev a], {}) ∈ ℱ Q›
          unfolding "*" by blast
        have ‹t @ [ev a] setinterleaves✓⇘(⊗✓)⇙ ((t_P @ [ev a], t_Q @ [ev a]), A)›
          by (simp add: facts(1) assms(3) setinterleavesptick_snoc_inside)
        with facts(2-4) assms5 show False by blast
      qed
      hence "££" : ‹Y_ev_inside_P ∪ Y_ev_inside_Q = Y_ev_inside› by (auto simp add: "**")

      have "€€" : ‹∀a∈Y_ev_notin. (t_P @ [ev a], {}) ∉ ℱ P ∨ (t_Q @ [ev a], {}) ∉ ℱ Q›
      proof (rule ccontr)
        assume ‹¬ (∀a∈Y_ev_notin. (t_P @ [ev a], {}) ∉ ℱ P ∨ (t_Q @ [ev a], {}) ∉ ℱ Q)›
        then obtain a where facts : ‹a ∉ A› ‹ev a ∈ Y› ‹(t_P @ [ev a], {}) ∈ ℱ P›
          ‹(t_Q @ [ev a], {}) ∈ ℱ Q› unfolding "*" by blast
        have ‹t @ [ev a] setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q @ [ev a]), A) ∨
              t @ [ev a] setinterleaves✓⇘(⊗✓)⇙ ((t_P @ [ev a], t_Q), A)›
          by (simp add: facts(1) assms(3) setinterleavesptick_snoc_notinL)
        with facts assms(1-3) assms5 show False by (metis is_processT4_empty)
      qed
      hence "£££" : ‹Y_ev_notin_P ∪ Y_ev_notin_Q = Y_ev_notin› by (auto simp add: "**")

      have "€€€" : ‹∀r_s∈Y_tick. ∃r s. r ⊗✓ s = ⌊r_s⌋ ∧ ((t_P @ [✓(r)], {}) ∉ ℱ P ∨ (t_Q @ [✓(s)], {}) ∉ ℱ Q)›
      proof (rule ccontr)
        assume ‹¬ (∀r_s∈Y_tick. ∃r s. r ⊗✓ s = ⌊r_s⌋ ∧
                    ((t_P @ [✓(r)], {}) ∉ ℱ P ∨ (t_Q @ [✓(s)], {}) ∉ ℱ Q))›
        then obtain r_s r s where facts : ‹✓(r_s) ∈ Y› ‹r ⊗✓ s = ⌊r_s⌋›
          ‹(t_P @ [✓(r)], {}) ∈ ℱ P› ‹(t_Q @ [✓(s)], {}) ∈ ℱ Q›
          unfolding "*" by blast
        have ‹t @ [✓(r_s)] setinterleaves✓⇘(⊗✓)⇙ ((t_P @ [✓(r)], t_Q @ [✓(s)]), A)›
          by (simp add: facts(2) assms(3) setinterleavesptick_snoc_tick)
        with facts assms5 show False by blast
      qed
      hence "££££" : ‹Y_tick_P ∪ Y_tick_Q = Y_tick› unfolding "**" by blast

      define X_P' and X_Q'
        where *** : ‹X_P' ≡ X_P ∪ ev ` Y_ev_inside_P ∪ ev ` Y_ev_notin_P ∪
                            {✓(r) |r s r_s. r ⊗✓ s = ⌊r_s⌋ ∧ r_s ∈ Y_tick_P}›
          ‹X_Q' ≡ X_Q ∪ ev ` Y_ev_inside_Q ∪ ev ` Y_ev_notin_Q ∪
                  {✓(s) |r s r_s. r ⊗✓ s = ⌊r_s⌋ ∧ r_s ∈ Y_tick_Q}›

      have $ : ‹(t_P, X_P') ∈ ℱ P› ‹(t_Q, X_Q') ∈ ℱ Q›
        by (auto simp add: "**" "***" intro!: is_processT5 assms dest: inj_tick_join)

      have ‹Y ⊆ super_ref_Syncptick (⊗✓) X_P' A X_Q'›
      proof (rule subsetI)
        show ‹e ∈ super_ref_Syncptick (⊗✓) X_P' A X_Q'› if ‹e ∈ Y› for e
        proof (cases e)
          from ‹e ∈ Y› show ‹e = ev a ⟹ e ∈ super_ref_Syncptick (⊗✓) X_P' A X_Q'› for a
            by (cases ‹a ∈ A›, simp_all add: "*" "**" "***" image_iff super_ref_Syncptick_def)
              (use "*"(1) "€" in blast,
                meson "$"(2) assms(1, 3) assms5 is_processT4_empty
                setinterleavesptick_snoc_notinL setinterleavesptick_snoc_notinR)
        next
          show ‹e ∈ super_ref_Syncptick (⊗✓) X_P' A X_Q'› if ‹e = ✓(r_s)› for r_s
          proof (cases ‹∃r s. r ⊗✓ s = ⌊r_s⌋›)
            assume ‹∃r s. r ⊗✓ s = ⌊r_s⌋›
            then obtain r s where ‹r ⊗✓ s = ⌊r_s⌋› by blast
            with ‹e ∈ Y› ‹e = ✓(r_s)› have ‹r_s ∈ Y_tick›
              by (auto simp add: "*")
            thus ‹e ∈ super_ref_Syncptick (⊗✓) X_P' A X_Q'›
              by (simp add: "*" super_ref_Syncptick_def)
                (metis (mono_tags, lifting) "*"(3) "***"(1,2) "££££"
                  Un_iff mem_Collect_eq ‹e = ✓(r_s)›)
          next
            show ‹∄r s. r ⊗✓ s = ⌊r_s⌋ ⟹
                  e ∈ super_ref_Syncptick (⊗✓) X_P' A X_Q'›
              by (simp add: ‹e = ✓(r_s)› super_ref_Syncptick_def)
          qed
        qed
      qed
      moreover from assms(4) have ‹X ⊆ super_ref_Syncptick (⊗✓) X_P' A X_Q'›
        by (fastforce simp add: "***" subset_iff super_ref_Syncptick_def)
      ultimately show ‹(t, X ∪ Y) ∈ ?f› using "$" assms(3) by auto
    qed
  next
    show processT9: ‹t ∈ ?d› if ‹t @ [✓(r_s)] ∈ ?d› for t r_s
    proof -
      from ‹t @ [✓(r_s)] ∈ ?d› obtain u v t_P t_Q
        where assms : ‹ftF v› ‹tF u ∨ v = []›
          ‹t @ [✓(r_s)] = u @ v›
          ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A)›
          ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q› by blast
      from assms(2) show ‹t ∈ ?d›
      proof (elim disjE)
        assume ‹tF u›
        with assms(3) obtain v' where ‹v = v' @ [✓(r_s)]› ‹t = u @ v'›
          by (cases v rule: rev_cases) auto
        from ‹v = v' @ [✓(r_s)]› assms(1) front_tickFree_dw_closed
        have ‹ftF v'› by blast
        with ‹t = u @ v'› ‹tF u› assms(1, 4, 5) show ‹t ∈ ?d› by blast
      next
        assume ‹v = []›
        with assms(3) obtain u' where ‹u = u' @ [✓(r_s)]› ‹t = u'› by auto
        from snoc_tick_setinterleavesptickE[OF assms(4)[unfolded this(1)]]
        obtain r s t_P' t_Q' where ‹r ⊗✓ s = ⌊r_s⌋›
          ‹u' setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), A)›
          ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]› by metis
        with assms(5) ‹t = u'› show ‹t ∈ ?d›
          by simp (metis append.right_neutral front_tickFree_Nil
              is_processT3_TR_append is_processT9)
      qed
    qed

    fix t X r_s
    assume ‹(t @ [✓(r_s)], {}) ∈ ?f›
    then consider (div) ‹t @ [✓(r_s)] ∈ ?d›
      | (fail) t_P t_Q X_P X_Q
      where ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹(t @ [✓(r_s)]) setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A)› by auto
    thus ‹(t, X - {✓(r_s)}) ∈ ?f›
    proof cases
      show ‹t @ [✓(r_s)] ∈ ?d ⟹ (t, X - {✓(r_s)}) ∈ ?f› by (drule processT9) simp
    next
      case fail
      from fail(3)[THEN snoc_tick_setinterleavesptickE]
      obtain r s t_P' t_Q' where * : ‹r ⊗✓ s = ⌊r_s⌋›
        ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), A)›
        ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]› by metis
      from fail(1, 2) have ‹t_P' @ [✓(r)] ∈ 𝒯 P› ‹t_Q' @ [✓(s)] ∈ 𝒯 Q›
        by (simp_all add: "*"(3, 4) F_T)
      hence ‹(t_P', UNIV - {✓(r)}) ∈ ℱ P›
        ‹(t_Q', UNIV - {✓(s)}) ∈ ℱ Q› by (meson is_processT6_TR)+
      moreover have ‹X - {✓(r_s)} ⊆ super_ref_Syncptick (⊗✓) (UNIV - {✓(r)}) A (UNIV - {✓(s)})›
        by (simp add: subset_iff super_ref_Syncptick_def)
          (metis "*"(1) eventptick.exhaust option.inject)
      ultimately show ‹(t, X - {✓(r_s)}) ∈ ?f› using "*"(2) by fast
    qed
  next
    show ‹s ∈ ?d ∧ tF s ∧ ftF t ⟹ s @ t ∈ ?d› for s t
      using front_tickFree_append by fastforce
  next  
    show ‹s ∈ ?d ⟹ (s, X) ∈ ?f› for s X by blast
  qed
qed


text ‹
Here term‹X ⊆ super_ref_Syncptick (⊗✓) X_P A X_Q› may seem surprising
(instead of for example term‹X = super_ref_Syncptick (⊗✓) X_P A X_Q›,
closer to the specification of const‹Sync›).
Actually, edge cases in the behaviour of const‹tick› ensure that a definition
with the latter would violate the invariant.
›

end

abbreviation (in Syncptick_locale) Interptick ::
  ‹[('a, 'r) processptick, ('a, 's) processptick] ⇒
   ('a, 't) processptick› (‹(_ |||✓ _)› [72, 73] 72)
  where ‹P |||✓ Q ≡ P ⟦ {} ⟧✓ Q›

abbreviation (in Syncptick_locale) Parptick ::
  ‹[('a, 'r) processptick, ('a, 's) processptick] ⇒
   ('a, 't) processptick› (‹(_ ||✓ _)› [74, 75] 74)
  where ‹P ||✓ Q ≡ P ⟦ UNIV ⟧✓ Q›

notation (in Syncptick_locale) Syncptick_locale_sym.Syncptick
  (‹(_ ⟦_⟧✓sym _)› [70, 0, 71] 70)

notation (in Syncptick_locale) Syncptick_locale_sym.Interptick
  (‹(_ |||✓sym _)› [72, 73] 72)

notation (in Syncptick_locale) Syncptick_locale_sym.Parptick
  (‹(_ ||✓sym _)› [74, 75] 74)




subsection ‹Projections›

context Syncptick_locale begin

lemma D_Syncptick' :
  ‹𝒟 (P ⟦A⟧✓ Q) = 
   {t @ u |t u t_P t_Q.
           ftF u ∧ (tF t ∨ u = []) ∧ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
           (t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q)}›
  by (simp add: Divergences.rep_eq Syncptick.rep_eq DIVERGENCES_def)

corollary D_Syncptick :
  ―‹This version is easier to use.›
  ‹𝒟 (P ⟦A⟧✓ Q) = 
   {t @ u |t u t_P t_Q.
           tF t ∧ ftF u ∧ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
           (t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q)}›
  (is ‹_ = ?rhs›)
proof (intro subset_antisym subsetI)
  show ‹d ∈ ?rhs ⟹ d ∈ 𝒟 (P ⟦A⟧✓ Q)› for d
    by (auto simp add: D_Syncptick')
next
  fix d assume ‹d ∈ 𝒟 (P ⟦A⟧✓ Q)›
  then obtain t u t_P t_Q
    where * : ‹d = t @ u› ‹ftF u› ‹tF t ∨ u = []›
      ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A)›
      ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
    unfolding D_Syncptick' by blast
  show ‹d ∈ ?rhs›
  proof (cases ‹tF t›)
    from "*" show ‹tF t ⟹ d ∈ ?rhs› by blast
  next
    assume ‹¬ tF t›
    with "*"(1, 3) have ‹u = []› ‹d = t› by simp_all
    from D_imp_front_tickFree ‹d = t› ‹d ∈ 𝒟 (P ⟦A⟧✓ Q)›
    have ‹ftF t› by blast
    with ‹¬ tF t› obtain r_s t' where ‹t = t' @ [✓(r_s)]›
      by (meson nonTickFree_n_frontTickFree)
    with "*"(4) obtain r t_P' s t_Q'
      where ** : ‹r ⊗✓ s = ⌊r_s⌋›
        ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
        ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), A)›
      by (auto simp add: ‹t = t' @ [✓(r_s)]›
          elim: snoc_tick_setinterleavesptickE)
    have ‹t_P' ∈ 𝒟 P ∧ t_Q' ∈ 𝒯 Q ∨ t_P' ∈ 𝒯 P ∧ t_Q' ∈ 𝒟 Q›
      by (metis "*"(5) "**"(2, 3) is_processT3_TR_append is_processT9)
    with "**"(4) ‹d = t› ‹ftF t› ‹t = t' @ [✓(r_s)]›
      front_tickFree_nonempty_append_imp show ‹d ∈ ?rhs› by blast
  qed
qed


lemma F_Syncptick' :
  ‹ℱ (P ⟦A⟧✓ Q) = 
   {(t, X). ∃t_P t_Q X_P X_Q.
            (t_P, X_P) ∈ ℱ P ∧ (t_Q, X_Q) ∈ ℱ Q ∧
            t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
            X ⊆ super_ref_Syncptick (⊗✓) X_P A X_Q} ∪
   {(t @ u, X) |t u t_P t_Q X.
                ftF u ∧ (tF t ∨ u = []) ∧ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
                (t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q)}›
  by (simp add: Failures.rep_eq Syncptick.rep_eq FAILURES_def)

lemma F_Syncptick :
  ‹ℱ (P ⟦A⟧✓ Q) = 
   {(t, X). ∃t_P t_Q X_P X_Q.
            (t_P, X_P) ∈ ℱ P ∧ (t_Q, X_Q) ∈ ℱ Q ∧
            t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
            X ⊆ super_ref_Syncptick (⊗✓) X_P A X_Q} ∪
   {(t @ u, X) |t u t_P t_Q X.
                tF t ∧ ftF u ∧ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
                (t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q)}›
  unfolding F_Syncptick' using D_Syncptick[of P A Q, unfolded D_Syncptick']
  by (intro arg_cong2[where f = ‹(∪)›], simp)
    (simp add: set_eq_iff, blast)


lemma T_Syncptick' :
  ‹𝒯 (P ⟦A⟧✓ Q) =
   {t. ∃t_P t_Q. t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒯 Q ∧ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A)} ∪
   {t @ u |t u t_P t_Q.
           ftF u ∧ (tF t ∨ u = []) ∧
           t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
           (t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q)}›
  by (simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Syncptick') blast

lemma T_Syncptick :
  ‹𝒯 (P ⟦A⟧✓ Q) =
   {t. ∃t_P t_Q. t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒯 Q ∧ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A)} ∪
   {t @ u |t u t_P t_Q.
           tF t ∧ ftF u ∧ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
           (t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q)}›
  unfolding T_Syncptick' using D_Syncptick[of P A Q, unfolded D_Syncptick']
  by (intro arg_cong2[where f = ‹(∪)›]) (simp_all add: set_eq_iff)


lemmas Syncptick_projs' = F_Syncptick' D_Syncptick' T_Syncptick'
  ―‹Classical versions, but the ones below are often more convenient to use.›

lemmas Syncptick_projs  = F_Syncptick  D_Syncptick  T_Syncptick


lemma (in Syncptick_locale) Syncptick_same_tick_join_on_strict_ticks_of :
  ‹Syncptick_locale.Syncptick tick_join' P S Q = P ⟦S⟧✓ Q›
  if ‹Syncptick_locale tick_join'› and ‹⋀r s. r ∈ ✓s(P) ⟹ s ∈ ✓s(Q) ⟹ tick_join' r s = r ⊗✓ s›
proof -
  interpret tjoin_interpreted : Syncptick_locale tick_join'
    by (fact ‹Syncptick_locale tick_join'›)
  show ‹Syncptick_locale.Syncptick tick_join' P S Q = P ⟦S⟧✓ Q›
  proof (rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 (tjoin_interpreted.Syncptick P S Q) ⟹ t ∈ 𝒟 (P ⟦S⟧✓ Q)› for t
      by (simp add: D_Syncptick tjoin_interpreted.D_Syncptick)
        (metis tickFree_setinterleavesptick_any_tick_join)
  next
    show ‹t ∈ 𝒟 (P ⟦S⟧✓ Q) ⟹ t ∈ 𝒟 (tjoin_interpreted.Syncptick P S Q)› for t
      by (simp add: D_Syncptick tjoin_interpreted.D_Syncptick)
        (metis tickFree_setinterleavesptick_any_tick_join)
  next
    fix t X assume ‹(t, X) ∈ ℱ (tjoin_interpreted.Syncptick P S Q)›
      ‹t ∉ 𝒟 (tjoin_interpreted.Syncptick P S Q)›
    then obtain t_P X_P t_Q X_Q where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
      ‹t setinterleaves✓⇘tick_join'⇙ ((t_P, t_Q), S)›
      ‹X ⊆ super_ref_Syncptick tick_join' X_P S X_Q›
      unfolding tjoin_interpreted.Syncptick_projs by blast
    define X_P_plus where ‹X_P_plus ≡ X_P ∪ {✓(r) |r. t_P @ [✓(r)] ∉ 𝒯 P - 𝒟 P}›
    define X_Q_plus where ‹X_Q_plus ≡ X_Q ∪ {✓(s) |s. t_Q @ [✓(s)] ∉ 𝒯 Q - 𝒟 Q}›
    have ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
    proof (cases ‹tF t›)
      show ‹tF t ⟹ t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
        using "*"(3) tickFree_setinterleavesptick_any_tick_join by blast
    next
      assume ‹¬ tF t›
      then obtain t' r_s where ‹tF t'› ‹t = t' @ [✓(r_s)]›
        by (metis F_imp_front_tickFree ‹(t, X) ∈ ℱ (tjoin_interpreted.Syncptick P S Q)›
            front_tickFree_append_iff nonTickFree_n_frontTickFree not_Cons_self2)
      with "*"(3) obtain t_P' r t_Q' s where ** : ‹tick_join' r s = ⌊r_s⌋›
        ‹t' setinterleaves✓⇘tick_join'⇙ ((t_P', t_Q'), S)›
        ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
        by (auto elim: snoc_tick_setinterleavesptickE)
      have ‹r ∈ ✓s(P) ∧ s ∈ ✓s(Q)›
      proof (rule ccontr)
        assume ‹¬ (r ∈ ✓s(P) ∧ s ∈ ✓s(Q))›
        hence ‹t_P' @ [✓(r)] ∈ 𝒟 P ∨ t_Q' @ [✓(s)] ∈ 𝒟 Q›
          by (metis "*"(1, 2) "**"(3, 4) F_T strict_ticks_of_memI)
        with ‹t ∉ 𝒟 (tjoin_interpreted.Syncptick P S Q)› show False
          by (simp add: tjoin_interpreted.D_Syncptick')
            (metis "*"(1-3) "**"(3, 4) F_T append.right_neutral front_tickFree_Nil)
      qed
      moreover from "**"(2) have ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)›
        using ‹tF t'› tickFree_setinterleavesptick_any_tick_join by blast
      ultimately show ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
        by (subst rev_setinterleavesptick_rev_rev_iff[symmetric],
            subst (asm) rev_setinterleavesptick_rev_rev_iff[symmetric])
          (use "**"(1) that(2) in ‹auto simp add: ‹t = t' @ [✓(r_s)]› "**"(3, 4)›)
    qed
    moreover from "*"(1) is_processT5_S7' is_processT8 is_processT9
    have ‹(t_P, X_P_plus) ∈ ℱ P› by (fastforce simp add: X_P_plus_def)
    moreover from "*"(2) is_processT5_S7' is_processT8 is_processT9
    have ‹(t_Q, X_Q_plus) ∈ ℱ Q› by (fastforce simp add: X_Q_plus_def)
    moreover have ‹e ∈ X ⟹ e ∈ super_ref_Syncptick (⊗✓) X_P_plus S X_Q_plus› for e
      using "*"(4)[THEN set_mp, of e]
      by (cases e, simp_all add: X_P_plus_def X_Q_plus_def super_ref_Syncptick_def subset_iff)
        (metis strict_ticks_of_memI that(2) tjoin_interpreted.inj_tick_join)
    ultimately show ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q)› by (simp add: F_Syncptick) blast
  next
    fix t X assume ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q)› ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)›
    then obtain t_P X_P t_Q X_Q where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
      ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
      ‹X ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
      unfolding Syncptick_projs by blast
    define X_P_plus where ‹X_P_plus ≡ X_P ∪ {✓(r) |r. t_P @ [✓(r)] ∉ 𝒯 P - 𝒟 P}›
    define X_Q_plus where ‹X_Q_plus ≡ X_Q ∪ {✓(s) |s. t_Q @ [✓(s)] ∉ 𝒯 Q - 𝒟 Q}›
    have ‹t setinterleaves✓⇘tick_join'⇙ ((t_P, t_Q), S)›
    proof (cases ‹tF t›)
      show ‹tF t ⟹ t setinterleaves✓⇘tick_join'⇙ ((t_P, t_Q), S)›
        using "*"(3) tickFree_setinterleavesptick_any_tick_join by blast
    next
      assume ‹¬ tF t›
      then obtain t' r_s where ‹tF t'› ‹t = t' @ [✓(r_s)]›
        by (metis F_imp_front_tickFree ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q)›
            front_tickFree_append_iff nonTickFree_n_frontTickFree not_Cons_self2)
      with "*"(3) obtain t_P' r t_Q' s where ** : ‹r ⊗✓ s = ⌊r_s⌋›
        ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)›
        ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
        by (auto elim: snoc_tick_setinterleavesptickE)
      have ‹r ∈ ✓s(P) ∧ s ∈ ✓s(Q)›
      proof (rule ccontr)
        assume ‹¬ (r ∈ ✓s(P) ∧ s ∈ ✓s(Q))›
        hence ‹t_P' @ [✓(r)] ∈ 𝒟 P ∨ t_Q' @ [✓(s)] ∈ 𝒟 Q›
          by (metis "*"(1, 2) "**"(3, 4) F_T strict_ticks_of_memI)
        with ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)› show False
          by (simp add: D_Syncptick')
            (metis "*"(1-3) "**"(3, 4) F_T append.right_neutral front_tickFree_Nil)
      qed
      moreover from "**"(2) have ‹t' setinterleaves✓⇘tick_join'⇙ ((t_P', t_Q'), S)›
        using ‹tF t'› tickFree_setinterleavesptick_any_tick_join by blast
      ultimately show ‹t setinterleaves✓⇘tick_join'⇙ ((t_P, t_Q), S)›
        by (subst rev_setinterleavesptick_rev_rev_iff[symmetric],
            subst (asm) rev_setinterleavesptick_rev_rev_iff[symmetric])
          (use "**"(1) that(2) in ‹auto simp add: ‹t = t' @ [✓(r_s)]› "**"(3, 4)›)
    qed
    moreover from "*"(1) is_processT5_S7' is_processT8 is_processT9
    have ‹(t_P, X_P_plus) ∈ ℱ P› by (fastforce simp add: X_P_plus_def)
    moreover from "*"(2) is_processT5_S7' is_processT8 is_processT9
    have ‹(t_Q, X_Q_plus) ∈ ℱ Q› by (fastforce simp add: X_Q_plus_def)
    moreover have ‹e ∈ X ⟹ e ∈ super_ref_Syncptick tick_join' X_P_plus S X_Q_plus› for e
      using "*"(4)[THEN set_mp, of e]
      by (cases e, simp_all add: X_P_plus_def X_Q_plus_def super_ref_Syncptick_def subset_iff)
        (metis strict_ticks_of_memI that(2) inj_tick_join)
    ultimately show ‹(t, X) ∈ ℱ (tjoin_interpreted.Syncptick P S Q)›
      by (simp add: tjoin_interpreted.F_Syncptick) blast
  qed
qed




subsection ‹First Properties›

abbreviation range_tick_join :: ‹'t set›
  where ‹range_tick_join ≡ {r_s |r_s r s. r ⊗✓ s = ⌊r_s⌋}›

lemma setinterleavesptick_imp_set_range_tick_join :
  ‹t setinterleaves✓⇘(⊗✓)⇙ ((u, v), A) ⟹
   {r_s. ✓(r_s) ∈ set t} ⊆ range_tick_join›
  by (induct ‹((⊗✓), u, A, v)› arbitrary: t u v)
    (auto simp add: subset_iff split: if_split_asm option.split_asm)+

end



lemma
  ― ‹Of course not suitable for simplifier.›
  ‹t setinterleaves✓⇘λs r. tick_join r s⇙ ((v, u), A) ⟷
   t setinterleaves✓⇘λr s. tick_join r s⇙ ((u, v), A)›
  by (fact setinterleavesptick_sym)

lemma super_ref_Syncptick_sym :
  ― ‹Of course not suitable for simplifier.›
  ‹super_ref_Syncptick (λs r. tick_join r s) X_Q S X_P =
   super_ref_Syncptick (λr s. tick_join r s) X_P S X_Q›
  by (auto simp add: super_ref_Syncptick_def)


lemma super_ref_Syncptick_mono :
  ‹A ⊆ A' ⟹ X_P ⊆ X_P' ⟹ X_Q ⊆ X_Q' ⟹
   super_ref_Syncptick tick_join X_P A X_Q ⊆
   super_ref_Syncptick tick_join X_P' A' X_Q'›
  by (auto simp add: super_ref_Syncptick_def)



context Syncptick_locale begin

lemma Syncptick_sym : ‹Q ⟦A⟧✓sym P = P ⟦A⟧✓ Q›
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 (Q ⟦A⟧✓sym P) ⟹ t ∈ 𝒟 (P ⟦A⟧✓ Q)› for t
    by (simp add: Syncptick_locale_sym.D_Syncptick D_Syncptick)
      (subst setinterleavesptick_sym, blast)
next
  show ‹t ∈ 𝒟 (P ⟦A⟧✓ Q) ⟹ t ∈ 𝒟 (Q ⟦A⟧✓sym P)› for t
    by (simp add: Syncptick_locale_sym.D_Syncptick D_Syncptick)
      (subst setinterleavesptick_sym, blast)
next
  show ‹(t, X) ∈ ℱ (Q ⟦A⟧✓sym P) ⟹ (t, X) ∈ ℱ (P ⟦A⟧✓ Q)› for t X
    by (simp add: Syncptick_locale_sym.F_Syncptick F_Syncptick)
      (subst (1 2) setinterleavesptick_sym,
        subst super_ref_Syncptick_sym, blast)
next
  show ‹(t, X) ∈ ℱ (P ⟦A⟧✓ Q) ⟹ (t, X) ∈ ℱ (Q ⟦A⟧✓sym P)› for t X
    by (simp add: Syncptick_locale_sym.F_Syncptick F_Syncptick)
      (subst (1 2) setinterleavesptick_sym,
        subst super_ref_Syncptick_sym, blast)
qed


lemma interpretable_inj_on_range_tick_join :
  ‹inj_on g range_tick_join ⟹
   Syncptick_locale (λr s. case r ⊗✓ s of ⌊r_s⌋ ⇒ ⌊g r_s⌋ | ◇ ⇒ ◇)›
  by (unfold_locales, simp split: option.split_asm)
    (metis (mono_tags, lifting) inj_onD inj_tick_join mem_Collect_eq)


lemma inj_on_map_map_eventptick_setinterleavesptick :
  ‹t setinterleaves✓⇘(⊗✓)⇙ ((u, v), A) ⟹
   map (map_eventptick id g) t
   setinterleaves✓⇘λr s. case r ⊗✓ s of ⌊r_s⌋ ⇒ ⌊g r_s⌋ | ◇ ⇒ ◇⇙ ((u, v), A)›
  (is ‹_ ⟹ _ setinterleaves✓⇘?tick_join'⇙ ((u, v), A)›)
  if inj_on_g : ‹inj_on g range_tick_join›
proof (induct ‹((⊗✓), u, A, v)› arbitrary: t u v)
  case (tick_setinterleavingptick_tick r u s v)
  from tick_setinterleavingptick_tick.prems [simplified]
  obtain r_s t' where * : ‹r ⊗✓ s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›
    ‹t' setinterleaves✓⇘(⊗✓)⇙ ((u, v), A)›
    by (auto split: option.split_asm)
  from tick_setinterleavingptick_tick.hyps[OF "*"(1, 3)]
  have ‹map (map_eventptick id g) t'
        setinterleaves✓⇘?tick_join'⇙ ((u, v), A)› .
  thus ?case by (simp add: "*"(1, 2))
qed auto



lemma vimage_inj_on_subset_super_ref_Syncptick_iff :
  ‹map_eventptick id g -` X ⊆
   super_ref_Syncptick (⊗✓) X_P A X_Q ⟷
   X ⊆ super_ref_Syncptick (λr s. case r ⊗✓ s of ⌊r_s⌋ ⇒ ⌊g r_s⌋ | ◇ ⇒ ◇) X_P A X_Q›
  (is ‹?lhs1 ⊆ ?lhs2 ⟷ X ⊆ ?rhs›)
  if inj_on_g : ‹inj_on g range_tick_join›
proof -
  let ?tick_join' = ‹λr s. case r ⊗✓ s of ⌊r_s⌋ ⇒ ⌊g r_s⌋ | ◇ ⇒ ◇›
  interpret Syncptick' : Syncptick_locale ?tick_join'
    by (intro interpretable_inj_on_range_tick_join inj_on_g)
  from inv_into_f_f inj_on_g have expanded_tick_join :
    ‹tick_join =
     (λr s. case ?tick_join' r s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊inv_into range_tick_join g r_s⌋)›
    by (fastforce split: split: option.split)
  let ?f1 = ‹map_eventptick id g›
  let ?f2 = ‹map_eventptick id (inv_into range_tick_join g)›
  show ‹?lhs1 ⊆ ?lhs2 ⟷ X ⊆ ?rhs›
  proof (intro iffI subsetI)
    show ‹e ∈ ?rhs› if ‹?lhs1 ⊆ ?lhs2› ‹e ∈ X› for e
    proof (cases e)
      fix a assume ‹e = ev a›
      with ‹e ∈ X› have ‹?f2 e ∈ ?f1 -` X› by simp
      with ‹?lhs1 ⊆ ?lhs2› have ‹?f2 e ∈ ?lhs2› by blast
      with ‹e = ev a› show ‹e ∈ ?rhs›
        by (auto simp add: super_ref_Syncptick_def)
    next
      show ‹e ∈ ?rhs› if ‹e = ✓(r_s)› for r_s
      proof (cases ‹∃r s. ?tick_join' r s = ⌊r_s⌋›)
        from ‹e = ✓(r_s)› show ‹∄r s. ?tick_join' r s = ⌊r_s⌋ ⟹ e ∈ ?rhs›
          by (simp add: super_ref_Syncptick_def)
      next
        assume ‹∃r s. ?tick_join' r s = ⌊r_s⌋›
        with ‹e = ✓(r_s)› ‹e ∈ X›
        have ‹?f2 e ∈ ?f1 -` X›
          by (auto split: option.split_asm)
            (metis (no_types, lifting) expanded_tick_join option.simps(5))
        with ‹?lhs1 ⊆ ?lhs2› have ‹?f2 e ∈ ?lhs2› by blast
        with ‹e = ✓(r_s)› show ‹e ∈ ?rhs›
          by (simp add: super_ref_Syncptick_def)
            (metis (no_types, lifting) expanded_tick_join option.simps(5))
      qed
    qed
  next
    show ‹e ∈ ?lhs2› if ‹X ⊆ ?rhs› and ‹e ∈ ?lhs1› for e
    proof (cases e)
      fix a assume ‹e = ev a›
      with ‹e ∈ ?lhs1› have ‹ev a ∈ X› by simp
      with ‹X ⊆ ?rhs› have ‹ev a ∈ ?rhs› by blast
      thus ‹e ∈ ?lhs2› by (auto simp add: ‹e = ev a› super_ref_Syncptick_def)
    next
      show ‹e ∈ ?lhs2› if ‹e = ✓(s_r)› for s_r
      proof (cases ‹∃s r. tick_join s r = ⌊s_r⌋›)
        from ‹e = ✓(s_r)› show ‹∄s r. tick_join s r = ⌊s_r⌋ ⟹ e ∈ ?lhs2›
          by (simp add: super_ref_Syncptick_def)
      next
        assume ‹∃s r. tick_join s r = ⌊s_r⌋›
        with ‹e = ✓(s_r)› ‹e ∈ ?lhs1›
        have ‹✓(g s_r) ∈ X› by simp
        with ‹X ⊆ ?rhs› have ‹✓(g s_r) ∈ ?rhs› by blast
        with ‹e = ✓(s_r)› show ‹e ∈ ?lhs2›
          by (simp add: super_ref_Syncptick_def)
            (metis Syncptick'.inj_tick_join option.simps(5))
      qed
    qed
  qed
qed


text ‹The two following lemmas are necessary for the proof of continuity.›

lemma finite_setinterleavesptick_tick_join :
  ‹finite {(u, v). t setinterleaves✓⇘(⊗✓)⇙ ((u, v), A)}›
  (is ‹finite {(u, v). ?f t u v}›)
proof (induct t)
  have ‹{(u, v). ?f [] u v} = {([], [])}› by (auto simp add: Nil_setinterleavesptick)
  thus ‹finite {(u, v). ?f [] u v}› by simp
next
  fix e t assume ‹finite {(u, v). ?f t u v}›
  have * : ‹{(x # u, v) | u v. ?f t u v} = (λ(u, v). (x # u, v)) ` {(u, v). ?f t u v}›
    ‹{(u, y # v) | u v. ?f t u v} = (λ(u, v). (u, y # v)) ` {(u, v). ?f t u v}›
    ‹{(x # u, y # v) | u v. ?f t u v} = (λ(u, v). (x # u, y # v)) ` {(u, v). ?f t u v}›
    for x y by auto
  show ‹finite {(u, v). ?f (e # t) u v}›
  proof (cases e)
    fix a assume ‹e = ev a›
    hence ‹?f (e # t) u v ⟹
           u ≠ [] ∧ hd u = ev a ∧ ?f t (tl u) v ∨
           v ≠ [] ∧ hd v = ev a ∧ ?f t u (tl v) ∨
           u ≠ [] ∧ hd u = ev a ∧ v ≠ [] ∧ hd v = ev a ∧ ?f t (tl u) (tl v)› for u v
      by (cases e) (auto elim: Cons_ev_setinterleavesptickE Cons_tick_setinterleavesptickE)
    hence ‹{(u, v). ?f (e # t) u v} ⊆
           {(ev a # u, v) | u v. ?f t u v} ∪
           {(u, ev a # v) | u v. ?f t u v} ∪
           {(ev a # u, ev a # v) | u v. ?f t u v}›
      by (simp add: subset_iff) (metis list.collapse)
    moreover have ‹finite {(ev a # u, v) | u v. ?f t u v}›
      by (simp add: "*"(1) ‹finite {(u, v). ?f t u v}›)
    moreover have ‹finite {(u, ev a # v) | u v. ?f t u v}›
      by (simp add: "*"(2) ‹finite {(u, v). ?f t u v}›)
    moreover have ‹finite {(ev a # u, ev a # v) | u v. ?f t u v}›
      by (simp add: "*"(3) ‹finite {(u, v). ?f t u v}›)
    ultimately show ‹finite {(u, v). ?f (e # t) u v}›
      by (simp add: finite_subset)
  next
    show ‹finite {(u, v). ?f (e # t) u v}› if ‹e = ✓(r_s)› for r_s
    proof (cases ‹r_s ∈ range_tick_join›)
      assume ‹r_s ∈ range_tick_join›
      then obtain r s where ‹r ⊗✓ s = ⌊r_s⌋› by blast
      hence ‹?f (e # t) u v ⟹
             u ≠ [] ∧ hd u = ✓(r) ∧ v ≠ [] ∧ hd v = ✓(s) ∧ ?f t (tl u) (tl v)› for u v
        by (cases u; cases v)
          (auto simp add: ‹e = ✓(r_s)› setinterleavingptick_simps inj_tick_join
            split: eventptick.splits option.split_asm if_split_asm)
      hence ‹{(u, v). ?f (e # t) u v} ⊆ {(✓(r) # u, ✓(s) # v) |u v. ?f t u v}›
        by (simp add: subset_iff) (metis list.collapse)
      moreover have ‹finite {(✓(r) # u, ✓(s) # v) |u v. ?f t u v}›
        by (simp add: "*"(3) ‹finite {(u, v). ?f t u v}›)
      ultimately show ‹finite {(u, v). ?f (e # t) u v}›
        by (simp add: finite_subset)
    next
      assume ‹r_s ∉ range_tick_join›
      hence ‹¬ ?f (e # t) u v› for u v
        by (cases u; cases v)
          (auto simp add: ‹e = ✓(r_s)› setinterleavingptick_simps
            split: eventptick.splits option.split_asm)
      thus ‹finite {(u, v). ?f (e # t) u v}› by simp
    qed
  qed
qed


lemma finite_setinterleavesptick_tick_join_Syncptick:
  ‹finite {(t_P, t_Q, u). u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), A) ∧
                          (∃v. t = u @ v ∧ ftF v ∧ (tF u ∨ v = []))}›
  (is ‹finite {(t_P, t_Q, u). ?f u t_P t_Q ∧ ?g t u}›)
proof -
  have ‹{(t_P, t_Q, u) |t_P t_Q. ?f u t_P t_Q} ⊆
        (λ(t_P, t_Q). (t_P, t_Q, u)) ` {(t_P, t_Q). ?f u t_P t_Q}› for u by auto
  hence ‹finite {(t_P, t_Q, u) |t_P t_Q. ?f u t_P t_Q}› for u
    by (rule finite_subset) (simp add: finite_setinterleavesptick_tick_join)
  moreover have ‹{(t_P, t_Q, u). ?f u t_P t_Q ∧ ?g t u} ⊆
                 (⋃u ∈ {u. u ≤ t}. {(t_P, t_Q, u) |t_P t_Q. ?f u t_P t_Q})›
    unfolding less_eq_list_def prefix_def by blast
  moreover have ‹finite {u. u ≤ t}› by (prove_finite_subset_of_prefixes t)
  ultimately show ?thesis by (simp add: finite_subset)
qed


end



(*<*)
end
  (*>*)