Theory Sync

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

section‹ The Synchronizing Operator ›

theory  Sync
  imports Process "HOL-Library.Infinite_Set"
begin

subsection‹Basic Concepts›

fun setinterleaving:: "'a trace × ('a event) set × 'a trace ⇒ ('a trace)set"
  where

  si_empty1: "setinterleaving([], X, []) = {[]}"
| si_empty2: "setinterleaving([], X, (y # t)) = 
               (if (y ∈ X) 
                then {} 
                else {z.∃ u. z = (y # u) ∧ u ∈ setinterleaving ([], X, t)})"
| si_empty3: "setinterleaving((x # s), X, []) = 
               (if (x ∈ X) 
                then {} 
                else {z.∃ u. z = (x # u) ∧ u ∈ setinterleaving (s, X, [])})"
 
| si_neq   : "setinterleaving((x # s), X, (y # t)) = 
               (if (x ∈ X) 
                then if (y ∈ X) 
                     then if (x = y) 
                          then {z.∃ u. z = (x#u) ∧ u ∈ setinterleaving(s, X, t)} 
                          else {}
                     else {z.∃ u. z = (y#u) ∧ u ∈ setinterleaving ((x#s), X, t)}
                else if (y ∉ X) 
                     then {z.∃ u. z = (x # u) ∧ u ∈ setinterleaving (s, X, (y # t))} 
                          ∪ {z.∃ u. z = (y # u) ∧ u ∈ setinterleaving((x # s), X, t)} 
                     else {z.∃ u. z = (x # u) ∧ u ∈ setinterleaving (s, X, (y # t))})"

fun setinterleavingList::"'a trace × ('a event) set × 'a trace ⇒ ('a trace)list" 
  where

  si_empty1l: "setinterleavingList([], X, []) = [[]]"
| si_empty2l: "setinterleavingList([], X, (y # t)) = 
               (if (y ∈ X) 
                then [] 
                else map (λz. y#z) (setinterleavingList ([], X, t)))"
| si_empty3l: "setinterleavingList((x # s), X, []) = 
               (if (x ∈ X) 
                then [] 
                else map (λz. x#z) (setinterleavingList (s, X, [])))"

 
 
| si_neql   : "setinterleavingList((x # s), X, (y # t)) = 
               (if (x ∈ X) 
                then if (y ∈ X) 
                     then if (x = y) 
                          then map (λz. x#z)  (setinterleavingList(s, X, t))
                          else []
                     else map (λz. y#z)  (setinterleavingList ((x#s), X, t))
                else if (y ∉ X) 
                     then map (λz. x#z)  (setinterleavingList (s, X, (y # t)))
                          @ map (λz. y#z)  (setinterleavingList ((x#s), X, t)) 
                     else map (λz. x#z)  (setinterleavingList (s, X, (y # t))))"

lemma finiteSetinterleavingList: "finite (set (setinterleavingList(s, X, t)))" 
  by auto

lemma sym : "setinterleaving(s, X, t)= setinterleaving(t, X, s)"
  by (rule setinterleaving.induct[of "λ(s,X,t). setinterleaving (s, X, t) 
  = setinterleaving (t, X, s)" "(s, X, t)", simplified], auto)

 

abbreviation "setinterleaves_syntax"  ("_ setinterleaves '(()'(_, _')(), _')" [60,0,0,0]70)
  where      "u setinterleaves ((s, t), X) == (u ∈ setinterleaving(s, X, t))"

 
subsection‹Consequences›

lemma emptyLeftProperty:"∀s. s setinterleaves (([], t), A)⟶s=t" 
  by (induct t) auto
 

lemma emptyLeftSelf: " (∀t1. t1∈ set t⟶t1∉A)⟶t setinterleaves (([], t), A) "
  by (induct t) auto


lemma emptyLeftNonSync: "s setinterleaves (([], t), A) ⟹ ∀a. a ∈ set t ⟶ a ∉ A"
proof (induct t arbitrary: s)
  case Nil
  show ?case by simp
next
  case (Cons a t)
  thus ?case by (cases s; simp split: if_split_asm)
qed
 

lemma ftf_Sync1: "a ∉ set(u) ∧ a ∉ set(t) ∧ s setinterleaves ((t, u), A) ⟶ a ∉ set(s)"
proof (induction "length t + length u" arbitrary:s t u rule:nat_less_induct)
  case 1
  show ?case 
    apply(cases t) using sym emptyLeftProperty apply blast
    apply(cases u) using sym emptyLeftProperty apply blast
    apply(simp split:if_splits, intro conjI impI, elim conjE disjE exE)
         apply (metis "1.hyps" add_less_le_mono length_Cons lessI order_refl set_ConsD)
        apply (metis "1.hyps" add_Suc_right length_Cons lessI set_ConsD) 
       apply (metis "1.hyps" add_less_mono length_Cons lessI set_ConsD) 
      apply (metis "1.hyps" add_Suc_right length_Cons lessI set_ConsD) 
     apply (metis (no_types, opaque_lifting) "1.hyps" add.commute add_Suc_right insert_iff 
                                         length_Cons lessI list.simps(15)) 
    by (metis "1.hyps" add_less_le_mono length_Cons lessI order_refl set_ConsD)
qed

lemma addNonSyncEmpty: "sa setinterleaves (([], u), A) ∧ y1 ∉ A ⟶
    (sa @ [y1]) setinterleaves (([y1], u), A) ∧ (sa @ [y1]) setinterleaves (([], u @ [y1]), A)"
  proof (induction "length u" arbitrary:sa u rule:nat_less_induct)
    case 1
    then show ?case 
      apply(cases u) 
       apply simp 
    proof-
      fix a list
      assume a: "∀m<length u. ∀x. m = length x ⟶(∀xa. xa setinterleaves (([], x), A) ∧ y1 ∉ A ⟶
       (xa @ [y1]) setinterleaves (([y1], x), A) ∧ (xa @ [y1]) setinterleaves (([], x @ [y1]), A))"
      and b: "u = a # list"
      from b have th: "sa setinterleaves (([], u), A)⟹(tl sa) setinterleaves (([], list), A)"  
        by (metis emptyLeftNonSync emptyLeftProperty emptyLeftSelf list.distinct(1) list.sel(3) 
        list.set_sel(2))
      from a b th have th1: "sa setinterleaves (([], u), A) ∧ y1 ∉ A⟶ ((tl sa) @ [y1]) 
      setinterleaves (([y1], list), A)∧((tl sa)@[y1]) setinterleaves (([], list@[y1]), A)" by auto
      thus "sa setinterleaves (([], u), A) ∧ y1 ∉ A ⟶
        (sa @ [y1]) setinterleaves (([y1], u), A) ∧ (sa @ [y1]) setinterleaves (([], u @ [y1]), A)"
        using  b th by auto  
    qed
  qed

lemma addNonSync: "sa setinterleaves ((t,u),A)∧ y1 ∉ A⟶
(sa@[y1]) setinterleaves ((t@[y1],u),A)∧(sa@[y1]) setinterleaves ((t,u@[y1]),A)"
proof (induction "length t + length u" arbitrary:sa t u rule:nat_less_induct)
  case 1
  then show ?case  
    apply(cases t)   
     apply (simp add: addNonSyncEmpty) 
    apply (cases u) 
     apply (metis Sync.sym addNonSyncEmpty append_self_conv2) 
  proof-
    fix a list aa lista
    assume a: "∀m<length t + length u. ∀x xa. m = length x + length xa ⟶
    (∀xb. xb setinterleaves ((x, xa), A) ∧ y1 ∉ A ⟶(xb @ [y1]) setinterleaves ((x @ [y1], xa), A) 
    ∧ (xb @ [y1]) setinterleaves ((x, xa @ [y1]), A))"
    and b: " t = a # list" 
    and c: "u = aa # lista"
    thus " sa setinterleaves ((t, u), A) ∧ y1 ∉ A ⟶
     (sa @ [y1]) setinterleaves ((t @ [y1], u), A) ∧ (sa @ [y1]) setinterleaves ((t, u @ [y1]), A)"
     proof-
       from b c have th0pre: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A) ⟹
                              (tl sa) setinterleaves ((list,lista), A)" by auto
       from th0pre a b c have th0pre1: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∉ A⟹
       ((tl sa) @ [y1]) setinterleaves ((list@ [y1], lista), A)∧
       ((tl sa) @ [y1]) setinterleaves ((list, lista@ [y1]), A)"  
        by (metis add_less_mono length_Cons lessI)  
      from  th0pre th0pre1 b c have th0: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∉ A ⟶
      (sa @ [y1]) setinterleaves ((t @ [y1], u), A)∧(sa @ [y1]) setinterleaves ((t, u @ [y1]), A)"  
        by auto 
      from b c have th1pre: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A) ⟹
                             (tl sa) setinterleaves ((list,aa#lista), A)" by auto
      from th1pre a b c have th1pre1: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∉ A⟹
      ((tl sa) @ [y1]) setinterleaves ((list@ [y1], aa#lista), A)∧
      ((tl sa) @ [y1]) setinterleaves ((list, aa#lista@ [y1]), A)"  
        by (metis add_Suc append_Cons length_Cons lessI) 
      from  th1pre th1pre1 b c  have th1: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∉ A ⟶  
      (sa @ [y1]) setinterleaves ((t @ [y1], u), A)∧(sa @ [y1]) setinterleaves ((t, u @ [y1]), A)" 
        by auto  
      from b c have th2pre: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A) ⟹
                             (tl sa) setinterleaves ((a#list,lista), A)" by auto
      from th2pre a b c have th2pre1: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∉ A⟹
      ((tl sa) @ [y1]) setinterleaves ((a#list@ [y1], lista), A)∧
      ((tl sa) @ [y1]) setinterleaves ((a#list, lista@ [y1]), A)"  
        by (metis add_Suc_right append_Cons length_Cons lessI)  
      from  th2pre th2pre1 b c have th2: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∉ A ⟶ 
      (sa @ [y1]) setinterleaves ((t @ [y1], u), A)∧(sa @ [y1]) setinterleaves ((t, u @ [y1]), A)" 
        by auto
      from b c have th3pre: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)⟹
     (tl sa) setinterleaves ((a#list,lista), A)∨(tl sa)setinterleaves ((list,aa#lista), A)" by auto
      from th3pre a b c have th3pre1: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)∧
      (tl sa) setinterleaves ((a#list,lista), A)∧ y1 ∉ A ⟹
      ((tl sa) @ [y1]) setinterleaves ((a#list@ [y1], lista ), A)∧((tl sa) @ [y1]) setinterleaves 
      ((a#list, lista@ [y1] ), A)" 
        by (metis add_Suc_right append_Cons length_Cons lessI)  
      from th3pre a b c have th3pre2: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)∧
      (tl sa) setinterleaves ((list,aa#lista), A)∧ y1 ∉ A ⟹((tl sa) @ [y1]) setinterleaves 
      ((list@ [y1], aa#lista ), A)∧((tl sa) @ [y1]) setinterleaves ((list, aa#lista @ [y1]), A)"  
        by (metis add_Suc append_Cons length_Cons lessI)         
      from th3pre th3pre1 th3pre2 a b c have th3: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A) ∧ 
      y1 ∉ A ⟶(sa @ [y1]) setinterleaves ((t @ [y1], u), A) ∧ 
      (sa @ [y1]) setinterleaves ((t, u @ [y1]), A)" by auto 
      show ?thesis  
        using b c th0 th1 th2 th3 by auto
    qed
  qed
qed

lemma addSyncEmpty: "sa setinterleaves (([], u), A) ∧ y1 ∈ A ⟶ 
                    (sa @ [y1]) setinterleaves (([y1], u @ [y1]), A)"
  proof (induction "length u" arbitrary:sa u rule:nat_less_induct)
    case 1
    then show ?case 
      apply(cases u) 
       apply simp 
    proof-
      fix a list
      assume a: "∀m<length u. ∀x. m = length x ⟶(∀xa. xa setinterleaves (([], x), A) ∧ y1 ∈ A 
                 ⟶ (xa @ [y1]) setinterleaves (([y1], x @ [y1]), A))"
      and b: "u = a # list"  
      from b have th: "sa setinterleaves (([], u), A)⟹(tl sa) setinterleaves (([], list), A)"  
        by (metis emptyLeftNonSync emptyLeftProperty emptyLeftSelf list.distinct(1) list.sel(3) 
           list.set_sel(2))
      from a th have th1: "sa setinterleaves (([], u), A) ∧ y1 ∈ A⟹ 
      ((tl sa) @ [y1]) setinterleaves (([y1], list @ [y1]), A)" using b by auto
      thus "sa setinterleaves (([], u), A) ∧ y1 ∈ A ⟶ 
           (sa @ [y1]) setinterleaves (([y1], u @ [y1]), A)" using b th by auto  
    qed
  qed 
 
lemma addSync: "sa setinterleaves ((t,u),A)∧ y1 ∈ A⟶(sa@[y1]) setinterleaves ((t@[y1],u@[y1]),A)"
  find_theorems ‹(@)› name: cases
proof (induction "length t + length u" arbitrary:sa t u rule:nat_less_induct)
  case 1
  then show ?case 
    apply(cases t) 
     apply (simp add: addSyncEmpty)
    apply(cases u) 
     apply (metis Sync.sym addSyncEmpty append.left_neutral) 
  proof-
    fix a list aa lista
    assume a: "∀m<length t + length u. ∀x xa. m = length x + length xa ⟶
                 (∀xb. xb setinterleaves ((x, xa), A) ∧ y1 ∈ A ⟶ (xb @ [y1]) setinterleaves 
                 ((x @ [y1], xa @ [y1]), A))"
    and b: "t = a # list "
    and c: " u = aa # lista"
    thus "sa setinterleaves((t, u),A)∧y1 ∈A⟶(sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)"
    proof-
      from b c have th0pre: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A) ⟹
      (tl sa) setinterleaves ((list,lista), A)" by auto
      from th0pre a b c have th0pre1: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∈ A⟹
      ((tl sa) @ [y1]) setinterleaves ((list@ [y1], lista @ [y1]), A)"  
        by (metis add_less_mono length_Cons lessI)  
      from  th0pre th0pre1 b c have th0: "a=aa∧a∈A⟹sa setinterleaves ((t, u), A) ∧ y1 ∈ A ⟶ 
      (sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto 
      from b c have th1pre: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A) ⟹
      (tl sa) setinterleaves ((list,aa#lista), A)" by auto
      from th1pre a b c have th1pre1: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∈ A⟹
      ((tl sa) @ [y1]) setinterleaves ((list@ [y1], aa#lista @ [y1]), A)"  
        by (metis add_Suc append_Cons length_Cons lessI) 
      from  th1pre th1pre1 b c  have th1: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∈ A ⟶ 
      (sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto  
      from b c have th2pre: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A) ⟹
      (tl sa) setinterleaves ((a#list,lista), A)" by auto
      from th2pre a b c have th2pre1: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∈ A⟹
      ((tl sa) @ [y1]) setinterleaves ((a#list@ [y1], lista @ [y1]), A)"  
        by (metis add_Suc_right append_Cons length_Cons lessI)  
      from  th2pre th2pre1 b c have th2: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∈ A ⟶ 
      (sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto
      from b c have th3pre: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)⟹
      (tl sa) setinterleaves((a#list,lista), A)∨(tl sa)setinterleaves ((list,aa#lista), A)" by auto
      from th3pre a b c have th3pre1: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)∧
      (tl sa) setinterleaves ((a#list,lista), A)∧ y1 ∈ A ⟹
      ((tl sa) @ [y1]) setinterleaves ((a#list@ [y1], lista @ [y1]), A)" 
        by (metis add_Suc_right append_Cons length_Cons lessI)  
      from th3pre a b c have th3pre2: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)∧
      (tl sa) setinterleaves ((list,aa#lista), A)∧ y1 ∈ A ⟹
      ((tl sa) @ [y1]) setinterleaves ((list@ [y1], aa#lista @ [y1]), A)" 
        by (metis add_Suc append_Cons length_Cons lessI)         
      from th3pre th3pre1 th3pre2 a b c have th3: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A) ∧ 
      y1 ∈ A ⟶ (sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto 
      show ?thesis  
        using b c th0 th1 th2 th3 by auto
    qed
  qed
qed
 

lemma doubleReverse: "s1 setinterleaves ((t, u), A)⟶(rev s1) setinterleaves ((rev t, rev u), A)"
proof (induction "length t + length u" arbitrary:s1 t u rule:nat_less_induct)
  case 1
  then show ?case 
    apply(cases t)  
    using emptyLeftNonSync 
     apply (metis emptyLeftProperty emptyLeftSelf rev.simps(1) set_rev)  
    apply(cases u) 
    using sym 
     apply (metis (no_types, lifting) emptyLeftNonSync emptyLeftProperty emptyLeftSelf 
     rev.simps(1) set_rev) 
  proof-
    fix a list aa lista
    assume a: "∀m<length t + length u. ∀x xa. m = length x + length xa ⟶
               (∀xb. xb setinterleaves ((x, xa), A) ⟶rev xb setinterleaves ((rev x, rev xa), A))"
    and b: "t = a # list"
    and c: "u = aa # lista"
    thus "s1 setinterleaves ((t, u), A) ⟶rev s1 setinterleaves ((rev t, rev u), A)"  
    proof-
      from b c have th0pre: "a=aa∧aa∈ A⟹s1 setinterleaves ((t, u), A)⟹
      (tl s1) setinterleaves ((list,lista), A)" by auto
      from th0pre a b c have th0pre1: "a=aa∧aa∈ A⟹s1 setinterleaves ((t, u), A)⟹
      ((rev (tl s1)) setinterleaves ((rev list, rev lista), A))"  
        by (metis add_less_mono length_Cons lessI)
      from  th0pre th0pre1 b c have th0: "a=aa∧aa∈ A⟹s1 setinterleaves ((t, u), A) ⟶
      rev s1 setinterleaves ((rev t, rev u), A)"   using addSync by fastforce 
      from b c have th1pre: "a∉A∧aa∈ A⟹s1 setinterleaves ((t, u), A)⟹
      (tl s1) setinterleaves ((list,aa#lista), A)" by auto
      from th1pre a b c have th1pre1: "a∉A∧aa∈ A⟹s1 setinterleaves ((t, u), A)⟹
      ((rev (tl s1)) setinterleaves ((rev list, rev (aa#lista)), A))"  
        by (metis add_less_mono1 length_Cons lessI)          
      from  th1pre th1pre1 b c have th1: "a∉A∧aa∈ A⟹s1 setinterleaves ((t, u), A) ⟶
      rev s1 setinterleaves ((rev t, rev u), A)"  using addNonSync by fastforce  
      from b c have th2pre: "aa∉A∧a∈ A⟹s1 setinterleaves ((t, u), A)⟹
      (tl s1) setinterleaves ((a#list,lista), A)" by auto
      from th2pre a b c have th2pre1: "aa∉A∧a∈ A⟹s1 setinterleaves ((t, u), A)⟹
      ((rev (tl s1)) setinterleaves ((rev (a#list), rev lista), A))"  
        by (metis add_Suc_right length_Cons lessI)        
      from  th2pre th2pre1 b c have th2: "aa∉A∧a∈ A⟹s1 setinterleaves ((t, u), A) ⟶
      rev s1 setinterleaves ((rev t, rev u), A)"  
        using addNonSync by fastforce 
      from b c have th3pre: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)⟹
      (tl s1) setinterleaves ((a#list,lista),A)∨(tl s1) setinterleaves((list,aa#lista), A)" by auto
      from th3pre a b c have th3pre1: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)∧
      (tl s1) setinterleaves ((a#list,lista), A) ⟹
      ((rev (tl s1)) setinterleaves ((rev (a#list), rev (lista)), A))"   
        by (metis add_Suc_right length_Cons lessI)
      from th3pre a b c have th3pre2: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)∧
      (tl s1) setinterleaves ((list,aa#lista), A) ⟹
      ((rev (tl s1)) setinterleaves ((rev (list), rev (aa#lista)), A))"  
        by (metis add_less_mono1 length_Cons lessI)
      from  th3pre1 have th3pre31: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)∧
      ((rev (tl s1)) setinterleaves ((rev (a#list), rev (lista)), A))⟶
      ((rev (tl s1))@[aa]) setinterleaves ((rev (a#list), (rev (lista))@[aa]), A)"
        by (simp add: addNonSync)
      from  th3pre2 have th3pre32: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)∧
      ((rev (tl s1)) setinterleaves ((rev (list), rev (aa#lista)), A))⟶
      ((rev (tl s1))@[a]) setinterleaves (((rev (list)@[a]), (rev (aa#lista))), A)"
        by (simp add: addNonSync)
      from th3pre th3pre1 th3pre2 th3pre31 th3pre32 a b c have th3: "aa∉A∧a∉ A⟹
      s1 setinterleaves ((t, u), A) ⟶rev s1 setinterleaves ((rev t, rev u), A)" by force
      show?thesis  
        using b c th0 th1 th2 th3 by auto
    qed 
  qed
qed
 
 
lemma  ftf_Sync21: "(a∈set(u)∧a∉set(t)∨a∈set(t)∧a∉set(u))∧a∈A⟶setinterleaving(u, A ,t)= {}"
proof (induction "length t + length u" arbitrary: t u rule:nat_less_induct)
  case 1
  then show ?case 
    apply(cases t)  
    using Sync.sym emptyLeftNonSync apply fastforce 
    apply(cases u)  
     apply auto[1]
    apply(simp split:if_splits, intro conjI impI, elim conjE disjE exE)
             apply blast
            apply auto[1]  
           apply blast 
          apply auto[1]  
         apply auto[1]  
    using less_SucI apply blast  
       apply auto[1] 
      apply auto[1]  
    using list.simps(15) apply auto[1] 
    by auto 
qed

lemma ftf_Sync32: "u=u1@[tick]∧t=t1@[tick]∧s setinterleaves ((t, u), insert tick (ev ` A))⟹
                  ∃s1. s1 setinterleaves ((t1, u1), insert tick (ev ` A))∧ (s=s1@[tick])"
proof-
  assume h: "u=u1@[tick]∧t=t1@[tick]∧s setinterleaves ((t, u), insert tick (ev ` A))"
  thus "∃s1. s1 setinterleaves ((t1, u1), insert tick (ev ` A))∧ (s=s1@[tick])"
  proof-
    from h have a:"rev u=tick#rev u1" by auto
    from h have b:"rev t=tick#rev t1" by auto
    from h have ab: "(rev s)  setinterleaves ((tick#rev t1, tick#rev u1), insert tick (ev ` A))" 
      using doubleReverse by fastforce
    from h obtain ss where c: "ss  setinterleaves  ((rev t1, rev u1), insert tick (ev ` A))∧ 
    ss=tl(rev s)" using ab by auto 
    from c have d: "(rev ss)  setinterleaves  (( t1,  u1), insert tick (ev ` A))" 
      using doubleReverse by fastforce
    from d have e: "rev s=tick#ss"  
      using ab append_Cons_eq_iff c by auto
    show ?thesis  
      using d e by blast
  qed
qed


lemma SyncWithTick_imp_NTF: 
  "(s @ [tick]) setinterleaves ((t, u),insert tick (ev ` A)) 
   ⟹ t∈ 𝒯 P ⟹ u ∈ 𝒯 Q
   ⟹ ∃t1 u1. t=t1@[tick] ∧ u=u1@[tick]∧ s setinterleaves ((t1, u1), insert tick (ev ` A))"  
proof-
  assume h: "(s @ [tick]) setinterleaves ((t, u), insert tick (ev ` A))"
  and h1: "t∈ 𝒯 P"
  and h2: "u∈ 𝒯 Q"
  thus "∃t1 u1. t=t1@[tick] ∧ u=u1@[tick]∧ s setinterleaves ((t1, u1), insert tick (ev ` A))"
  proof-
    from h have a: "(tick#rev s) setinterleaves ((rev t, rev u), insert tick (ev ` A))" 
      using doubleReverse by fastforce
    from h obtain tt uu where b: "t=tt@[tick]∧u=uu@[tick]"  
      by (metis T_nonTickFree_imp_decomp empty_iff ftf_Sync1 ftf_Sync21 h1 h2 insertI1 
          non_tickFree_tick tickFree_append tickFree_def)
    from h b have d: "s setinterleaves ((tt, uu), insert tick (ev ` A))"  
      using ftf_Sync32 by blast
    show ?thesis  
      using b d by blast
  qed 
qed

lemma synPrefix1: 
   " ta = [] 
     ⟹ ∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶  
                 t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)"
proof-
  assume a: "ta = []"
  obtain u1 where th: "u1=s" by blast
  from a have th2: "(s @ t) setinterleaves ((ta, u), A) ⟶ (s @ t)= u"  
    by (simp add: a emptyLeftProperty)
  from a have th3: "(s @ t) setinterleaves ((ta, u), A) ⟶ (∀t1. t1∈set u⟶t1∉A)"  
    by (simp add: emptyLeftNonSync)
  from a th have th1: "(s @ t) setinterleaves ((ta, u), A) ⟶ [] ≤ ta ∧ u1 ≤ u " 
    using le_list_def th2 by blast 
  from a th have thh1: "(s @ t) setinterleaves ((ta, u), A)∧ (∀t1. t1∈set u1⟶t1∉A) ⟶ 
  s setinterleaves (([], u1), A)"  by (simp add: emptyLeftSelf)
  thus "∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶ t1 ≤ ta ∧ u1 ≤ u ∧ 
  s setinterleaves ((t1, u1), A)" using th th1 th2 th3 thh1 by fastforce 
qed
 

lemma synPrefix: "∃t1 u1. (s @ t) setinterleaves ((ta, u), A)⟶
                  t1≤ta∧u1≤u∧s setinterleaves ((t1, u1), A)"
proof (induction "length ta + length u" arbitrary: s t ta u rule:nat_less_induct)
  case 1
  then show ?case 
    apply(cases ta)  
     using synPrefix1 apply fastforce 
    apply(cases u) 
     using sym synPrefix1 apply metis 
   proof-
     fix a list aa lista s t
     assume a: " ∀m<length ta + length u. ∀x xa. m = length x + length xa ⟶
                 (∀xb xc. ∃t1 u1. (xb @ xc) setinterleaves ((x, xa), A) ⟶
                 t1 ≤ x ∧ u1 ≤ xa ∧ xb setinterleaves ((t1, u1), A))"
     and b: "ta = a # list"
     and c: "u = aa # lista " 
     thus " ∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶ t1 ≤ ta ∧ u1 ≤ u ∧ 
            s setinterleaves ((t1, u1), A)" 
     proof-
       from a have th0: "∀xb xc. ∃t1 u1. (xb @ xc) setinterleaves ((list, lista), A) ⟶
                                  t1 ≤ list ∧ u1 ≤ lista ∧ xb setinterleaves ((t1, u1), A)"  
         by (metis add_less_le_mono b c impossible_Cons le_cases not_le_imp_less)
       from b c obtain yb where thp: "a=aa∧a∈ A∧(s@t) setinterleaves ((ta, u), A)∧length s >1 ⟹
       yb=tl s" by blast
       with b c have thp4: "a=aa∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧length s >1 ⟹s=a#yb" 
         by (auto, metis Cons_eq_append_conv list.sel(3) list.size(3) not_less0)
       have thp5: "a=aa∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧length s >1 ⟹
       (yb @ t) setinterleaves ((list, lista), A)"  using b c thp4 by auto 
       from th0 obtain yt yu where thp1: "a = aa ∧ a ∈ A ⟹ (s @ t) setinterleaves ((ta, u), A) ∧ 
       1 < length s⟹yb setinterleaves ((yt, yu), A)∧yt≤list∧yu≤lista"  using thp5 by blast 
       from thp thp1 have thp2: "a=aa∧a∈ A⟹ (s @ t) setinterleaves ((ta, u), A)∧ length s >1⟶ 
       s setinterleaves ((a#yt, aa#yu), A)" using thp4 by auto 
       from b c have thp3: "a=aa∧a∈ A⟹ (s @ t) setinterleaves ((ta, u), A) ∧ length s=1⟶
       s setinterleaves (([a], [aa]), A)" 
         using append_eq_append_conv2[of s t "[aa]"] by (auto, metis append_Nil2 
         append_eq_append_conv length_Cons list.size(3))
       have thp6: "a=aa∧a∈ A⟹ (s @ t) setinterleaves ((ta, u), A) ∧ length s=0⟶
       s setinterleaves (([], []), A)" by auto
       from thp1 have thp7: "a=aa∧a∈ A⟹ (s @ t) setinterleaves ((ta, u), A)∧ length s >1⟹
       (a # yt)≤ta ∧(aa # yu)≤u"  by (metis b c le_less less_cons)  
       have th: "a=aa∧a∈ A⟹∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶ 
       t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)"
       proof -
         assume dd:"a=aa ∧ a∈ A"
         consider (aa) "length s = 0" | (bb) "length s = 1" | (cc) "length s > 1"
           by linarith
         then show ?thesis 
         proof cases 
           case aa
           with thp6 show ?thesis 
             by (rule_tac x="[]" in exI, rule_tac x="[]" in exI, simp) 
         next
           case bb
           with dd thp3 b c show ?thesis 
             by (rule_tac x="[a]" in exI, rule_tac x="[a]" in exI, auto simp add: le_list_def)            
         next
           case cc
           with dd thp2 thp7 b c show ?thesis
             by (rule_tac x="a#yt" in exI, rule_tac x="a#yu" in exI, auto simp add: le_list_def)   
        qed
      qed
      from b c have th1pre: "a∉A∧aa∈ A∧(s @ t) setinterleaves ((ta, u), A) ⟶
      tl (s @ t) setinterleaves ((list, u), A)∧hd (s@t)=a" by auto 
      from a b c obtain yt1 yu1 where th1pre1: "a∉A∧aa∈ A∧(s @ t) setinterleaves ((ta, u), A)∧
      length s>0⟶yt1≤list∧ yu1 ≤ u∧ tl s setinterleaves ((yt1, yu1), A)"  
        by (metis (no_types, lifting) length_Cons length_greater_0_conv lessI plus_nat.simps(2) 
        th1pre tl_append2)
      from b have th1pre2: "yt1≤list⟶a#yt1≤ta"  
        by (simp add: le_less less_cons) 
      from b c have th1pre3: "a∉A∧aa∈ A∧tl s setinterleaves ((yt1, yu1), A)⟶
      (a#(tl s)) setinterleaves ((a#yt1, yu1), A)"  
        by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)  
      from b c th1pre1 th1pre2 have th1pre4: "a∉A∧aa∈ A∧(s @ t) setinterleaves ((ta, u), A)∧
      length s>0 ⟶a#yt1≤ta∧ yu1 ≤u∧ s setinterleaves ((a#yt1, yu1), A)" 
        using th1pre th1pre3  by fastforce  
      have th1pre5:"a∉A∧aa∈ A∧(s @ t) setinterleaves ((ta, u), A)∧length s=0 ⟶[]≤ta∧ [] ≤u∧ 
      s setinterleaves (([], []), A)" by auto
      have th1: "a∉A∧aa∈ A⟹∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶ 
      t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)"  using th1pre4 th1pre5 by blast 
      from b c have th2pre: "aa∉A∧a∈ A∧(s @ t) setinterleaves ((ta, u), A) ⟶
      tl (s @ t) setinterleaves ((ta, lista), A)∧hd (s@t)=aa" by auto 
      from a b c obtain yt2 yu2 where th2pre1: "aa∉A∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧
      length s>0⟶yt2≤ta∧ yu2 ≤ lista∧ (tl s) setinterleaves ((yt2, yu2), A)"  
        by (metis (no_types, lifting) add_Suc_right length_Cons length_greater_0_conv lessI 
        th2pre tl_append2)  
      from c have th2pre2: "yu2≤lista⟶aa#yu2≤u"   
        by (simp add: le_less less_cons) 
      from b c have th2pre3: "aa∉A∧a∈ A∧tl s setinterleaves ((yt2, yu2), A)⟶
      (aa#(tl s)) setinterleaves ((yt2, aa#yu2), A)"  
        by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)  
      from b c th2pre1 th2pre2 have th2pre4: "aa∉A∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧
      length s>0 ⟶yt2≤ta∧ aa#yu2 ≤u∧ s setinterleaves ((yt2, aa#yu2), A)" 
        using th2pre th2pre3  by fastforce  
      have th2pre5:"aa∉A∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧length s=0 ⟶
      []≤ta∧ [] ≤u∧ s setinterleaves (([], []), A)" by auto
      have th2: "aa∉A∧a∈ A⟹∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶ 
      t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)"  using th2pre4 th2pre5 by blast      
      from b c have th3pre: "aa∉A∧a∉ A∧(s @ t) setinterleaves ((ta, u), A)⟶tl (s @ t) 
      setinterleaves ((ta, lista), A)∧hd (s@t)=aa∨tl (s @ t)setinterleaves((list, u), A)∧hd(s@t)=a" 
        by auto
      from a b c th3pre obtain yt31 yu31 where th3pre1: "aa∉A∧a∉ A∧
      (s @ t) setinterleaves ((ta, u), A)∧tl (s @ t) setinterleaves ((ta, lista), A)∧
      hd (s@t)=aa∧length s>0⟶yt31≤ta∧ yu31 ≤ lista∧ (tl s) setinterleaves ((yt31, yu31), A)" 
        by(metis(no_types,lifting)add_Suc_right length_Cons length_greater_0_conv lessI tl_append2) 
      from a b c th3pre obtain yt32 yu32 where th3pre2: "aa∉A∧a∉A∧(s@t)setinterleaves ((ta, u),A)∧
      tl (s @ t) setinterleaves ((list, u), A)∧hd (s@t)=a∧length s>0⟶yt32≤list∧ yu32 ≤u∧ 
      (tl s) setinterleaves ((yt32, yu32), A)"  
        by (metis add_less_mono1 impossible_Cons le_neq_implies_less length_greater_0_conv 
        nat_le_linear tl_append2)
      from b c have th3pre3: "aa∉A∧a∉ A∧tl s setinterleaves ((yt31, yu31), A)⟶
      (aa#(tl s)) setinterleaves ((yt31, aa#yu31), A)"  
        by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident) 
      from b c th3pre1 th3pre2 have th3pre4: "aa∉A∧a∉ A∧(s @ t) setinterleaves ((ta, u), A)∧
      length s>0∧tl (s @ t) setinterleaves ((ta, lista), A)∧hd (s@t)=aa ⟶yt31≤ta∧ aa#yu31 ≤u∧ 
      s setinterleaves ((yt31, aa#yu31), A)"  
        by (metis hd_append2 le_less length_greater_0_conv less_cons list.exhaust_sel th3pre3)
      from b c have th3pre5: "aa∉A∧a∉ A∧tl s setinterleaves ((yt32, yu32), A)⟶
      (a#(tl s)) setinterleaves ((a#yt32, yu32), A)"  
        by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident) 
      from b c th3pre1 th3pre2 have th3pre6: "aa∉A∧a∉ A∧(s @ t) setinterleaves ((ta, u), A)∧
      length s>0∧tl (s @ t) setinterleaves ((list, u), A)∧hd (s@t)=a ⟶a#yt32≤ta∧ yu32 ≤u∧ 
      s setinterleaves ((a#yt32, yu32), A)" 
        using th3pre th3pre5  by (metis hd_append2 le_less length_greater_0_conv less_cons 
        list.exhaust_sel)
      have th3pre7:"aa∉A∧a∉ A∧(s @ t) setinterleaves ((ta, u), A)∧length s=0 ⟶
      []≤ta∧ [] ≤u∧ s setinterleaves (([], []), A)" by auto
      have th3: "aa∉A∧a∉ A⟹∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶ 
      t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)"  
        using th3pre th3pre4 th3pre6 th3pre7 by blast 
      with a b c th th1 th2 show ?thesis
        by fastforce
    qed
  qed
qed

lemma SyncWithTick_imp_NTF1: 
"(s @ [tick]) setinterleaves ((t, u), insert tick (ev ` A)) 
 ⟹ t∈ 𝒯 P ⟹ u∈ 𝒯 Q
 ⟹ ∃ t u Xa Y. (t, Xa) ∈ ℱ P ∧ ( (u, Y) ∈ ℱ Q ∧ 
                 s setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                 X - {tick} = (Xa ∪ Y) ∩ insert tick (ev ` A) ∪ Xa ∩ Y)"
  apply (drule SyncWithTick_imp_NTF)
    apply simp
   apply simp 
proof -
  assume A: "t ∈ 𝒯 P"
  and B: "u ∈ 𝒯 Q"
  and C: "∃t1 u1. t = t1 @ [tick]∧u = u1@[tick]∧s setinterleaves ((t1, u1), insert tick (ev ` A))" 
  from C obtain t1 u1 
    where D: "t = t1 @ [tick] ∧ u = u1 @ [tick] ∧ 
                  s setinterleaves ((t1, u1), insert tick (ev ` A))" by blast
  from A B D have E: "(t1, X-{tick}) ∈ ℱ P ∧ (u1, X-{tick}) ∈ ℱ Q"  
    by (simp add: T_F process_charn)  
  thus  " ∃t u Xa Y. (t, Xa) ∈ ℱ P ∧ (u, Y) ∈ ℱ Q ∧ 
                     s setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                     X - {tick} = (Xa ∪ Y) ∩ insert tick (ev ` A) ∪ Xa ∩ Y"
    using A B C D E by blast
qed

lemma ftf_Sync: 
  "front_tickFree u
   ⟹ front_tickFree t
   ⟹ s setinterleaves ((t, u),insert tick (ev ` A))
   ⟹ front_tickFree s"
proof-
  assume A: "front_tickFree u"
  assume B: "front_tickFree t"
  assume C: "s setinterleaves ((t, u), insert tick (ev ` A))"
  thus "front_tickFree s" 
  proof-
    from A obtain u1 where A1: "∀ u2. u1≤u∧tickFree u1∧  (u2≤u∧tickFree u2⟶u2≤u1)"   
      by (metis append.right_neutral append_eq_first_pref_spec front_tickFree_charn le_list_def 
         tickFree_Nil)
    from A A1 have AA1: "u1=u∨u=u1@[tick]" 
      by (metis(no_types, lifting) antisym append_Nil2 append_eq_first_pref_spec append_is_Nil_conv 
      front_tickFree_charn le_list_def less_list_def less_self nonTickFree_n_frontTickFree)
    from B obtain t1 where B1: "∀ t2. t1≤t∧tickFree t1∧  (t2≤t∧tickFree t2⟶t2≤t1)"
      by (metis append.right_neutral append_eq_first_pref_spec front_tickFree_charn le_list_def 
      tickFree_Nil)
    from B B1 have BB1: "t1=t∨t=t1@[tick]" 
      by (metis(no_types, lifting) antisym append_Nil2 append_eq_first_pref_spec append_is_Nil_conv 
      front_tickFree_charn le_list_def less_list_def less_self nonTickFree_n_frontTickFree)
    from A1 B1 have C1: "∀s1. s1 setinterleaves ((t1, u1), insert tick (ev ` A))⟶tickFree s1"  
      by (meson ftf_Sync1 tickFree_def)
    from AA1 BB1 have CC1: "u1=u∧t1=t⟶tickFree s" 
      by (simp add: C C1)
    from AA1 BB1 have CC2: "u1=u∧t=t1@[tick]⟶tickFree s"  using ftf_Sync21  
      by (metis A1 C equals0D insertI1 non_tickFree_tick tickFree_append tickFree_def)
    from AA1 BB1 have CC3: "u=u1@[tick]∧t1=t⟶tickFree s"  using ftf_Sync21 
      by (metis B1 C insertI1 insert_not_empty mk_disjoint_insert non_tickFree_tick tickFree_append 
      tickFree_def) 
    from AA1 BB1 have CC4: "u=u1@[tick]∧t=t1@[tick]⟹
    ∃s1. s1 setinterleaves ((t1, u1), insert tick (ev ` A))∧(s=s1@[tick])"  
      using C ftf_Sync32 by blast  
    from C1 CC4 have CC5: "front_tickFree s"  
      using AA1 BB1 CC1 CC2 CC3 tickFree_implies_front_tickFree 
      tickFree_implies_front_tickFree_single by auto
    with A1 B1 C1 AA1 BB1 show ?thesis  
      using CC1 CC2 CC3 tickFree_implies_front_tickFree by auto
    qed
  qed

lemma is_processT5_SYNC2: "
⋀ sa Y t u Xa Ya.  (t,Xa) ∈ ℱ P ∧ (u,Ya) ∈ ℱ Q ∧ (sa setinterleaves ((t,u),insert tick (ev ` A))) 
  ⟹∀c. c ∈ Y ⟶
        (∀ t1 u1. (sa@[c]) setinterleaves ((t1,u1),insert tick (ev ` A))⟶
        (((t1,{}) ∈ ℱ P⟶(u1, {}) ∉ ℱ Q)∧((t1,{}) ∈ ℱ Q⟶(u1, {}) ∉ ℱ P))) 
  ⟹ ∃t2 u2 Xb. (t2, Xb) ∈ ℱ P ∧ 
                  (∃Yb. (u2, Yb) ∈ ℱ Q ∧
                        sa setinterleaves ((t2, u2), insert tick (ev ` A)) ∧
                        ( Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y = 
                            (Xb ∪ Yb) ∩ insert tick (ev ` A) ∪ Xb ∩ Yb)"  
proof -
  fix sa Y t u Xa Ya
  assume A: "(t,Xa) ∈ ℱ P ∧ (u,Ya) ∈ ℱ Q ∧(sa setinterleaves ((t,u),insert tick (ev ` A)))" 
  and B: " ∀c. c ∈ Y ⟶
               (∀ t1 u1. (sa@[c]) setinterleaves ((t1,u1),insert tick (ev ` A)) ⟶
               (((t1,{}) ∈ ℱ P ⟶
               (u1, {}) ∉ ℱ Q) ∧ ((t1,{}) ∈ ℱ Q⟶(u1, {}) ∉ ℱ P)))"
  thus "∃t2 u2 Xb. (t2, Xb) ∈ ℱ P ∧ 
                   (∃Yb. (u2, Yb) ∈ ℱ Q ∧ sa setinterleaves ((t2, u2), insert tick (ev ` A)) ∧
                   (Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y = 
                      (Xb ∪ Yb) ∩ insert tick (ev ` A) ∪ Xb ∩ Yb)"
  proof-
    from A B obtain Y1 Y2 
               where A1: "(Y1=(Y∩insert tick (ev ` A)))∧(Y2=(Y - insert tick (ev ` A)))" 
      by blast
    from A1 have AA1: "Y1 ∪ Y2 = Y" 
      by blast 
    from A1 have newAA: "∀y∈Y1. y∈ insert tick (ev ` A)" 
      by blast
    from A1 have newAAA: "∀y∈Y2. y∉ insert tick (ev ` A)" 
      by blast
    from B A1 have AA2: "∀z∈Y1.(t@[z], {}) ∉ ℱ P ∨ (u@[z], {}) ∉ ℱ Q" 
    proof(cases "∃z ∈ Y1. (t@[z], {})∈ℱ P ∧ (u@[z], {}) ∈ ℱ Q")
      case True
      from True obtain z1 where TrA: "z1∈Y1∧(t@[z1], {})∈ℱ P ∧ (u@[z1], {}) ∈ ℱ Q" 
        by blast
      from TrA A have TrB: 
             "⟦sa setinterleaves ((t,u),insert tick(ev ` A)); 
               z1∈insert tick (ev ` A)⟧
              ⟹(sa@[z1]) setinterleaves ((t@[z1],(u@[z1])),insert tick (ev ` A))"    
      proof- 
        have a: "(rev sa) setinterleaves ((rev t,rev u),insert tick (ev ` A))"  
          using local.A doubleReverse by blast
        have b: "(z1#rev sa)  setinterleaves  ((z1#rev t,z1# rev u),insert tick (ev ` A))"  
          using TrA a newAA by auto
        show ?thesis  
          using b doubleReverse by fastforce
      qed
      then show ?thesis  
        using A1 B TrA local.A by blast  
    next
      case False
      then show ?thesis 
        by blast
    qed
    from A B A1 obtain Z1 Z2 where A2: "(Z1=Y1∩{z.(t@[z], {})∉ℱ P})∧(Z2=Y1-{z.(t@[z], {})∉ℱ P})" 
      by blast
    from A2 have BA: "Y1=Z1∪Z2" 
      by blast
    from A2 have BAA: "∀z∈Z1. (t@[z], {}) ∉ ℱ P" 
      by blast
    from A2 have BAAA: "∀z∈Z2. (u@[z], {})∉ ℱ Q"  
      using AA2 by blast
    from A2 BA BAA have A3: "(t, Z1)∈ ℱ P"   
      by (meson F_T NF_NT is_processT5_S7 local.A)  
    from A A1 have A43: "∀y∈Y2. (t@[y], {})∉ ℱ P ∧ (u@[y], {})∉ ℱ Q" 
    proof(cases "∃y∈Y2. ((t@[y], {})∈ ℱ P)∨((u@[y], {})∈ ℱ Q)")
      case True
      from True obtain y1 where innAA: "y1∈Y2∧(((t@[y1], {})∈ ℱ P)∨((u@[y1], {})∈ ℱ Q))" by blast
      from innAA have innAAA: "y1∉ insert tick (ev ` A)"  
        using newAAA by auto
      from innAA have innAA1: 
             "⟦sa setinterleaves ((t,u),insert tick (ev ` A)); 
               y1 ∉ insert tick (ev ` A)⟧
              ⟹ ((t@[y1], {})∈ ℱ P
                   ⟶(sa@[y1]) setinterleaves ((t@[y1],u),insert tick (ev ` A))) ∧
                      ((u@[y1], {})∈ ℱ Q⟶(sa@[y1]) setinterleaves((t,u@[y1]),insert tick (ev`A)))" 
        by (simp add: addNonSync)        
      with A B innAA1 innAA show ?thesis  
        by (metis A1 DiffD1 innAAA is_processT4_empty)
    next
      case False
      then show ?thesis by blast
    qed
    from A1  A2 obtain Xbb where B1: "Xbb=(Xa∪Z1∪Y2)" 
      by blast
    from A B1 A3 A43  have A5: "(t, Xbb)∈ ℱ P"   
      by (meson BAA is_processT5_S1)
    from A1 A2 obtain Ybb where B2: "Ybb=(Ya∪Z2∪Y2)" 
      by blast
    from A B have A52: "(u, Ybb)∈ ℱ Q"  
      by (metis A43 B2 BAAA is_processT5_S1)   
    from A1 A2 have A61: "(Xbb ∪ Ybb)∩insert tick (ev ` A)=((Xa∪Ya∪Y1∪Y2) ∩ insert tick (ev ` A))"  
      using B1 B2 by blast
    from A1 have A62: "(Y1) ∩ insert tick (ev ` A)=Y1"  
      using inf.orderE by auto
    from A1 have A63: "(Y2) ∩ insert tick (ev ` A)={}"  
      by (simp add: AA1 Int_commute) 
    from A61 A62 A63 have A64:"((Xa∪Ya∪Y1∪Y2)∩insert tick(ev `A))=((Xa∪Ya)∩insert tick(ev `A)∪Y1)" 
      by (simp add: Int_Un_distrib2)
    from AA1 BA B1 B2 have A65: "(Xbb∩Ybb)⊆((Xa∩Ya)∪Y) " 
      by auto  
    from AA1 BA B1 B2 have A66:"(Xbb∩Ybb)⊇((Xa∩Ya)∪Y2)" 
      by auto    
    from A1 A2  have A66: "((Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y) = ((Xbb ∪ Ybb) ∩ 
    insert tick (ev ` A) ∪ Xbb ∩ Ybb)"
    proof -
      have f1: "(Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y = Y ∪ Xa ∩ Ya ∪ ((Xa ∪ Ya) ∩ 
      insert tick (ev ` A) ∪ Xbb ∩ Ybb)"using A65 by auto
      have "Xa ∩ Ya ∪ Y2 ∪ Xbb ∩ Ybb = Xbb ∩ Ybb"
        by (meson A66 le_iff_sup)
      then have "(Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y = Xbb ∩ Ybb ∪ ((Xa ∪ Ya) ∩ 
      insert tick (ev ` A) ∪ Y1)" using f1 A1 by auto
      then show ?thesis
        using A61 A64 by force
    qed
    with A5 A52 A66 show ?thesis  
      using local.A by blast  
  qed
qed

lemma pt3: 
  "ta ∈ 𝒯 P 
   ⟹ u ∈ 𝒯 Q ⟹ (s @ t) setinterleaves ((ta, u), insert tick (ev ` A))
   ⟹ ∃t u X. (t, X) ∈ ℱ P ∧
                (∃Y. (u, Y) ∈ ℱ Q ∧ 
                     s setinterleaves ((t, u), insert tick (ev ` A)) ∧
                     tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})"  
proof-
  assume a1: "ta ∈ 𝒯 P"
  assume a2: "u ∈ 𝒯 Q"
  assume a3: "(s @ t) setinterleaves ((ta, u), insert tick (ev ` A))"
  have aa: "ta ∈ 𝒯 P ⟹u ∈ 𝒯 Q ⟹ (s @ t) setinterleaves ((ta, u), insert tick (ev ` A))⟹
                ∃t u. t ∈ 𝒯 P ∧(u ∈ 𝒯 Q ∧s setinterleaves ((t, u), insert tick (ev ` A)))" 
    using is_processT3_ST_pref synPrefix by blast
  thus "∃t u X. (t, X) ∈ ℱ P ∧(∃Y. (u, Y) ∈ ℱ Q ∧
                 s setinterleaves ((t, u), insert tick (ev ` A)) ∧
                 tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})"  
    using NF_NT a1 a2 a3 by blast
qed



subsection‹The Sync Operator Definition›

lift_definition Sync :: "['a process,'a set,'a process] => 'a process"    ("(3(_ ⟦_⟧/ _))" [64,0,65] 64)  
  is "λP A Q. ({(s,R).∃ t u X Y. (t,X) ∈ ℱ P ∧ (u,Y) ∈ ℱ Q ∧ 
                                 (s setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧ 
                                 R = (X ∪ Y) ∩ ((ev`A) ∪ {tick}) ∪ X ∩ Y}    ∪ 
               {(s,R).∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧ 
                                 s = r@v ∧ 
                                 (r setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧ 
                                 (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)},
               
               {s.   ∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧ 
                                s = r@v ∧ 
                                (r setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧ 
                                (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)})"
proof -
  show "is_process ({(s,R).∃ t u X Y. (t,X) ∈ ℱ P ∧ (u,Y) ∈ ℱ Q ∧ 
                                      (s setinterleaves ((t,u),(ev`(A :: 'a set)) ∪ {tick})) ∧ 
                                      R = (X ∪ Y) ∩ ((ev`A) ∪ {tick}) ∪ X ∩ Y} ∪ 
                    {(s,R).∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧ 
                                      s = r@v ∧ 
                                      (r setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧      
                                      (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)},
                
                    {s.    ∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧ 
                                      s = r@v ∧ 
                                      (r setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧ 
                                      (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)})"
                    (is "is_process(?f, ?d)") for P Q A
  unfolding is_process_def FAILURES_def DIVERGENCES_def
  proof (simp only: fst_conv snd_conv, intro conjI)
    show "([], {}) ∈ ?f" 
      apply auto 
      by (metis Int_commute Int_empty_right Sync.si_empty1 Un_empty empty_iff insert_iff is_processT1) 
  next 
    show " ∀s X. (s, X) ∈ ?f ⟶ front_tickFree s" 
      apply (auto simp:is_processT2 append_T_imp_tickFree front_tickFree_append D_imp_front_tickFree) 
        using ftf_Sync is_processT2 apply blast
       using D_imp_front_tickFree ftf_Sync is_processT2_TR apply blast
      using D_imp_front_tickFree ftf_Sync is_processT2_TR by blast  
  next
    show "∀s t. (s @ t, {}) ∈ ?f ⟶ (s, {}) ∈ ?f" 
      apply auto   
          apply(drule F_T) 
          apply(drule F_T) 
    proof(goal_cases)
      case (1 s t ta u X Y)
      then show ?case 
        using pt3 by fastforce
  next
    case (2 s t ta u r v)
    have aa: "front_tickFree v 
               ⟹ s@t = r @ v ⟹ r setinterleaves ((ta, u), insert tick (ev ` A)) 
               ⟹ ∀t u r. r setinterleaves ((t,u),insert tick(ev `A)) ⟶
                            (∀v. s=r@v⟶front_tickFree v ⟶
                            ¬tickFree r ∧ v≠[]∨(t ∈ 𝒟 P ⟶
                            u ∉ 𝒯 Q) ∧ (t ∈ 𝒟 Q ⟶ u ∉ 𝒯 P))
               ⟹ tickFree r ⟹ ta ∈ 𝒟 P ⟹ u ∈ 𝒯 Q ⟹ s<r" 
      apply(simp add: append_eq_append_conv2) 
      by (metis append_Nil2 front_tickFree_Nil front_tickFree_dw_closed le_list_def less_list_def)
    from 2(1,2,3,4,5,6,7) Sync.sym aa have a1: "s<r" by blast
    have aaa: "r setinterleaves ((ta, u), insert tick (ev ` A)) 
               ⟹ tickFree r ⟹ ta ∈ 𝒟 P
               ⟹ u ∈ 𝒯 Q ⟹ s<r 
               ⟹ ∃t u X. (t, X) ∈ ℱ P ∧ (∃Y. (u, Y) ∈ ℱ Q ∧
                          s setinterleaves ((t, u), insert tick (ev ` A)) ∧
                          tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})"
      apply(drule D_T) 
      apply(simp add: le_list_def less_list_def)  
      using Sync.sym pt3 by blast
    have aab: "∃t u X. (t, X) ∈ ℱ P ∧(∃Y. (u, Y) ∈ ℱ Q ∧ 
                       s setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                       tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})" 
      using 2(1,2,3,4,5,6,7) aa aaa Sync.sym by auto
    then show ?case by auto  
  next
    case (3 s t ta u r v)
    have aa: "front_tickFree v ⟹s @ t = r @ v 
             ⟹ r setinterleaves ((ta, u), insert tick (ev ` A)) 
             ⟹ ∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
                    (∀v. s = r @ v ⟶front_tickFree v ⟶¬ tickFree r ∧ v ≠ [] ∨ 
                           (t ∈ 𝒟 P ⟶ u ∉ 𝒯 Q) ∧ (t ∈ 𝒟 Q ⟶ u ∉ 𝒯 P)) 
             ⟹ tickFree r 
             ⟹ ta ∈ 𝒟 Q ⟹ u ∈ 𝒯 P ⟹ s<r"  
      apply(simp add: append_eq_append_conv2) 
      by (metis append_Nil2 front_tickFree_Nil front_tickFree_dw_closed le_list_def less_list_def)
    
    have aaa: "r setinterleaves ((ta, u), insert tick (ev ` A)) 
               ⟹ tickFree r ⟹ ta ∈ 𝒟 Q ⟹ u ∈ 𝒯 P ⟹s<r
               ⟹ ∃t u X. (t, X) ∈ ℱ P ∧ 
                           (∃Y. (u, Y) ∈ ℱ Q ∧s setinterleaves ((t, u), insert tick (ev ` A)) ∧
                            tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})" 
      apply(drule D_T) 
      apply(simp add: le_list_def less_list_def)  
      using Sync.sym pt3 by blast
    from 3(1,2,3,4,5,6,7) Sync.sym aa have a1: "s<r"  
      by blast
    have aab: "∃t u X. (t, X) ∈ ℱ P ∧ (∃Y. (u, Y) ∈ ℱ Q ∧ 
                       s setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                       tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})" 
      using 3(1,2,3,4,5,6,7) aa aaa Sync.sym by auto 
    then show ?case 
      by auto 
  next
    case (4 s t ta u)
    from 4(3) have a1: "ta ∈ 𝒯 P"  
      by (simp add: D_T)
    then show ?case  
      using "4"(1) "4"(4) pt3 by blast  
  next
    case (5 s t ta u)
    from 5(3) have a1: "ta ∈ 𝒯 Q"  
      by (simp add: D_T)
    then show ?case  
      using "5"(1) "5"(4) Sync.sym pt3 by blast
  qed      
  next 
    show "∀s X Y. (s, Y) ∈ ?f ∧ X ⊆ Y ⟶ (s, X) ∈ ?f"   
      apply auto 
    proof(goal_cases)
      case (1 s X t u Xa Ya)
      have aa: "X ⊆ ((Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya )⟹∃x1 y1. x1⊆Xa ∧ y1⊆Ya ∧ 
      X=((x1 ∪ y1) ∩ insert tick (ev ` A) ∪ x1 ∩ y1)" 
        apply(simp add: Set.subset_iff_psubset_eq) 
        apply(erule disjE) 
         defer 
         apply blast 
      proof-
        assume A: "X ⊂ (Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya" 
        from A obtain X1 where B: "X1=((Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya)-X" 
          by blast
        from A obtain x where C: "x=Xa-X1" 
          by blast
        from A obtain y where D: "y=Ya-X1" 
          by blast
        from A B C D have E: "X = (x ∪ y) ∩ insert tick (ev ` A) ∪ x ∩ y" 
          by blast
        thus " ∃x1. (x1 ⊂ Xa ∨ x1 = Xa) ∧ (∃y1. (y1 ⊂ Ya ∨ y1 = Ya) ∧ X = (x1 ∪ y1) ∩ 
        insert tick (ev ` A) ∪ x1 ∩ y1)"
          using A B C D E by (metis Un_Diff_Int inf.strict_order_iff inf_sup_absorb) 
      qed 
      then show ?case using 1(1,2,3,4,5)  
        by (meson process_charn)
    qed
   
  next  
    let ?f1 = "{(s,R). ∃ t u X Y. (t,X) ∈ ℱ P ∧ (u,Y) ∈ ℱ Q ∧ 
                       (s setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧ 
                       R = (X ∪ Y) ∩ ((ev`A) ∪ {tick}) ∪ X ∩ Y}" 
    have is_processT5_SYNC3: 
              "⋀sa X Y.(sa, X) ∈?f1 ⟹(∀c. c∈Y⟶(sa@[c],{})∉?f)⟹(sa, X∪Y) ∈ ?f1" 
      apply(clarsimp) 
      apply(rule is_processT5_SYNC2[simplified]) 
       apply(auto simp:is_processT5) apply blast  
      by (metis Sync.sym Un_empty_right inf_sup_absorb inf_sup_aci(5) insert_absorb insert_not_empty)  
    show "∀s X Y. (s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟶ (s, X ∪ Y) ∈ ?f"
      apply(intro allI impI, elim conjE UnE)
       apply(rule rev_subsetD)
        apply(rule is_processT5_SYNC3)
      by(auto)  
  next
    show "∀s X. (s @ [tick], {}) ∈ ?f ⟶ (s, X - {tick}) ∈ ?f" 
      apply auto 
          apply(drule F_T) 
          apply(drule F_T)  
          using SyncWithTick_imp_NTF1 apply fastforce 
         apply(metis append_assoc append_same_eq front_tickFree_dw_closed nonTickFree_n_frontTickFree 
         non_tickFree_tick tickFree_append) 
        apply(metis butlast_append butlast_snoc front_tickFree_charn non_tickFree_tick tickFree_append 
        tickFree_implies_front_tickFree) 
       apply (metis NT_ND append_Nil2 front_tickFree_Nil is_processT3_ST is_processT9_S_swap 
       SyncWithTick_imp_NTF) 
      by (metis NT_ND append_Nil2 front_tickFree_Nil is_processT3_ST is_processT9_S_swap 
      SyncWithTick_imp_NTF)
      
  next
    show "∀s t. s ∈ ?d ∧ tickFree s ∧ front_tickFree t ⟶ s @ t ∈ ?d" 
      apply auto
         using front_tickFree_append apply blast 
        using front_tickFree_append apply blast 
       apply blast
      by blast
  next  
    show "∀s X. s ∈ ?d ⟶  (s, X) ∈ ?f"
      by blast
  next  
    show "∀s. s @ [tick] ∈ ?d ⟶ s ∈ ?d"  
      apply auto
         apply (metis butlast_append butlast_snoc front_tickFree_charn non_tickFree_tick 
         tickFree_append tickFree_implies_front_tickFree)
        apply (metis butlast_append butlast_snoc front_tickFree_charn non_tickFree_tick 
        tickFree_append tickFree_implies_front_tickFree) 
       apply (metis D_T append.right_neutral front_tickFree_Nil is_processT3_ST is_processT9 
       SyncWithTick_imp_NTF) 
      by (metis D_T append.right_neutral front_tickFree_Nil is_processT3_ST is_processT9 
      SyncWithTick_imp_NTF) 
  qed
qed

subsection‹The Projections›

lemma
  F_Sync    : "ℱ (P ⟦ A ⟧ Q) = 
                   {(s,R).∃ t u X Y. (t,X) ∈ ℱ P ∧ 
                                       (u,Y) ∈ ℱ Q ∧ 
                                       s setinterleaves ((t,u),(ev`A) ∪ {tick}) ∧ 
                                       R = (X ∪ Y) ∩ ((ev`A) ∪ {tick}) ∪ X ∩ Y} ∪ 
                   {(s,R).∃ t u r v. front_tickFree v ∧ 
                                       (tickFree r ∨ v=[]) ∧ 
                                       s = r@v ∧ 
                                       r setinterleaves ((t,u),(ev`A)∪{tick}) ∧ 
                                       (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}"
  by (simp add: Failures.rep_eq Sync.rep_eq FAILURES_def)   

lemma
  D_Sync    : "𝒟 (P ⟦ A ⟧ Q) = 
                   {s.    ∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧ 
                            s = r@v ∧ r setinterleaves ((t,u),(ev`A) ∪ {tick}) ∧ 
                            (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}"
  by (simp add: Divergences.rep_eq Sync.rep_eq DIVERGENCES_def)   
 

lemma
  T_Sync    : "𝒯 (P ⟦ A ⟧ Q) = 
                   {s.    ∃ t u. t ∈ 𝒯 P ∧ u ∈ 𝒯 Q ∧ 
                                 s setinterleaves ((t,u),(ev`A) ∪ {tick})}∪
                   {s.    ∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧ 
                                 s = r@v ∧ r setinterleaves ((t,u),(ev`A) ∪ {tick}) ∧ 
                                 (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}"
  by (simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Sync) blast
  
  
subsection‹Syntax for Interleave and Parallel Operator ›

abbreviation Inter_syntax  ("(_|||_)" [72,73] 72)
  where "P ||| Q ≡ (P ⟦ {} ⟧ Q)"

abbreviation Par_syntax  ("(_||_)" [74,75] 74)
  where "P || Q  ≡ (P ⟦ UNIV ⟧ Q)"

subsection‹ Continuity Rule ›

lemma mono_Sync_D1:  
"P ⊑ Q ⟹ 𝒟 (Q ⟦ A ⟧ S) ⊆ 𝒟 (P ⟦ A ⟧ S)"
  apply(auto simp: D_Sync)
  using le_approx1 apply blast
  using le_approx_lemma_T apply blast
   apply (metis append_Nil2 le_approx1 subsetCE tickFree_Nil tickFree_implies_front_tickFree) 
  by (metis append_Nil2 le_approx_lemma_T subsetCE tickFree_Nil tickFree_implies_front_tickFree)

lemma mono_Sync_D2:
"P ⊑ Q⟹(∀ s. s ∉ 𝒟 (P  ⟦ A ⟧  S) ⟶ Ra (P  ⟦ A ⟧  S) s = Ra (Q  ⟦ A ⟧  S) s)"
  apply auto 
   apply(simp add: Ra_def D_Sync F_Sync)
   apply (metis (no_types, lifting) F_T append_Nil2 front_tickFree_Nil le_approx2)
  apply(simp add: Ra_def D_Sync F_Sync)
  apply(insert le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q]  
               le_approx1[of P Q] le_approx2T[of P Q], auto) 
      apply blast
     apply blast
    apply blast
  using front_tickFree_Nil apply blast
  using front_tickFree_Nil by blast

lemma interPrefixEmpty: "s setinterleaves ((t,[]),A)∧t1<t⟹∃s1<s. s1 setinterleaves ((t1, []), A)"
  by (metis (no_types, lifting) Sync.sym emptyLeftProperty le_list_def nil_le2 
  order.strict_implies_order synPrefix1)

lemma interPrefix:"∃u1 s1. s setinterleaves((t,u),A)∧t1<t⟶u1≤u∧s1<s∧s1 setinterleaves((t1,u1),A)"
proof (induction "length t + length u" arbitrary:s t u t1 rule:nat_less_induct)
  case 1
  then show ?case 
    apply(cases t)
     apply auto[1]
    apply(cases u)   
     apply (meson interPrefixEmpty nil_le2)   
  proof- 
    fix a list aa lista 
    assume a: " ∀m<length t + length u.  ∀x xa. m = length x + length xa ⟶ (∀xb xc. ∃u1 s1. 
    xb setinterleaves((x, xa),A)∧xc < x ⟶ u1 ≤ xa ∧ s1 < xb ∧ s1 setinterleaves ((xc, u1), A))"
    and b: "t = a # list"
    and c: "u = aa # lista"
    thus "∃u1 s1. s setinterleaves((t, u),A)∧t1<t⟶u1 ≤u∧s1<s∧s1 setinterleaves ((t1, u1), A)"  
    proof-
      from b c have th0pre: "a=aa∧aa∈ A⟹s setinterleaves ((t, u), A) ⟹
      (tl s) setinterleaves ((list,lista), A)" by auto    
      from a obtain yu ys  
        where th0pre1: "a=aa∧aa∈ A ∧ s setinterleaves ((t, u), A)∧ t1 < a # list ∧ length t1>0
                        ⟹ yu ≤ lista ∧ ys<tl s ∧ ys setinterleaves ((tl t1, yu), A)"    
        apply (simp add: le_list_def less_list_def append_eq_Cons_conv) 
        by (metis add_less_mono b c length_Cons lessI list.sel(3) th0pre)        
      from th0pre th0pre1  b c 
      have th0pre2: "a=aa ∧ aa∈A
                     ⟹ s setinterleaves ((a # list, u), A) ∧ t1<a#list∧length t1>0
                     ⟹ (a#ys)setinterleaves((a#tl t1, a#yu), A)∧a#ys<s∧a#yu≤u∧t1=a#tl t1"   
        apply (simp add: le_list_def less_list_def  Cons_eq_append_conv)  
        by (metis append_Cons list.exhaust_sel list.inject list.sel(3))
      have th0pre3: "a=aa∧aa∈A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list∧length t1=0⟹
      []<s∧[]≤u∧ [] setinterleaves ((t1, []), A)"  
        apply (simp add: le_list_def less_list_def) using c by auto
      from  th0pre2 th0pre3 c  have th0 : "a=aa∧aa∈A⟹s setinterleaves ((a # list, u), A)∧ 
      t1 < a # list⟹∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)"  by fastforce
      from b c have th1pre: "a∉A∧aa∈ A⟹s setinterleaves ((a # list, u), A) ⟹
      (tl s) setinterleaves ((list,aa#lista), A)" by auto
      from a obtain yu1 ys1  where th1pre1: "a∉A∧aa∈ A∧s setinterleaves ((a # list, u), A)∧ 
      t1 < a # list∧length t1>0⟹yu1≤u∧ys1<tl s∧ys1 setinterleaves ((tl t1, yu1), A)"  
        apply (simp add: le_list_def less_list_def append_eq_Cons_conv)  
        by (metis add_Suc b c length_Cons lessI list.sel(3) th1pre)
      from th1pre1 have th1pre2: "a∉A∧aa∈ A ∧ ys1 setinterleaves ((tl t1, yu1), A)⟹
      (a#ys1) setinterleaves ((a#tl t1, yu1), A)" apply simp  
        by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
      from th1pre th1pre1  b c have th1pre3: "a∉A∧aa∈ A⟹s setinterleaves ((a # list, u), A)∧ 
      t1<a#list∧length t1>0⟹(a#ys1) setinterleaves ((a#tl t1, yu1), A)∧a#ys1<s∧yu1≤u∧t1=a#tl t1"  
        apply (simp add: le_list_def less_list_def )  
        by (metis append_Cons list.exhaust_sel list.inject list.sel(3) th1pre2)
      have th1preEmpty: "a∉A∧aa∈ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list∧length t1=0
      ⟹[]<s∧[]≤u∧ [] setinterleaves ((t1, []), A)" apply (simp add: le_list_def less_list_def) 
        using c by auto
      from c have th1: "a∉A∧aa∈ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list⟹
      ∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)"   using th1pre3 th1preEmpty by fastforce
      from b c have th2pre: "aa∉A∧a∈ A⟹s setinterleaves ((a # list, u), A) ⟹
      (tl s) setinterleaves ((a#list,lista), A)" by auto
      from a  th2pre obtain yu2 ys2  where th2pre1: "aa∉A∧a∈ A∧s setinterleaves ((a # list, u), A)∧ 
      t1 < a # list∧length t1>0⟹yu2≤lista∧ys2<tl s∧ys2 setinterleaves ((t1, yu2), A)"  
        apply (simp add: le_list_def less_list_def)   
        by (metis add_Suc_right b c length_Cons lessI)    
      from th2pre1 have th2pre2: "aa∉A∧a∈ A ∧ ys2 setinterleaves ((t1, yu2), A)⟹
      (aa#ys2) setinterleaves ((t1, aa#yu2), A)" apply simp  
        by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
      from th2pre th2pre1  b c have th2pre3: "aa∉A∧a∈ A ⟹s setinterleaves ((a # list, u), A)∧ 
      t1 < a # list∧length t1>0⟹(aa#ys2) setinterleaves ((t1, aa#yu2), A)∧aa#ys2<s∧aa#yu2≤u"  
        apply (simp add: le_list_def less_list_def )  using th2pre2 by auto
      have th2preEmpty: "aa∉A∧a∈ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list∧length t1=0
      ⟹[]<s∧[]≤u∧ [] setinterleaves ((t1, []), A)" apply (simp add: le_list_def less_list_def) 
        using c by auto
      from th2pre3 b c have th2: "aa∉A∧a∈ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list⟹
      ∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)"  
        using th2preEmpty by blast
      from b c have th3pre: "aa∉A∧a∉ A⟹s setinterleaves ((a # list, u), A) ⟹
      (tl s) setinterleaves ((a#list,lista), A)∧hd s=aa∨(tl s) setinterleaves ((list,u), A)∧hd s=a" 
        by auto
      from a c b th3pre obtain yu3 ys3  where th3pre1: "(aa∉A∧a∉ A∧s setinterleaves 
      ((a # list, u), A)∧ t1 < a # list∧length t1>0∧(tl s) setinterleaves ((a#list,lista), A)⟶
      yu3≤lista∧ys3<tl s∧ys3 setinterleaves((t1,yu3),A))" apply(simp add:le_list_def less_list_def) 
        by (metis (no_types, lifting) add_Suc length_Cons lessI) 
      have adsmallPrefix: "t1<a # list∧length t1>0⟹tl t1<list"  
        using less_tail by fastforce
      from a b c th3pre adsmallPrefix obtain yu30 ys30   where th3pre12: "(aa∉A∧a∉ A⟹
      (tl s) setinterleaves ((list,u), A)∧hd s=a∧tl t1< list⟶yu30≤u∧ys30<tl s∧
      ys30 setinterleaves ((tl t1, yu30), A))" apply (simp add: le_list_def less_list_def)  
        by (metis (no_types, lifting) add_Suc_right length_Cons lessI)  
      have th3pre1more1: "yu3≤lista ⟹aa#yu3≤u " using c  
        by (metis le_less less_cons)
      have th3pre1more2: "aa∉A∧a∉ A∧s setinterleaves ((a # list, aa#lista), A) ∧
      (tl s) setinterleaves ((a#list,lista), A)∧hd s=aa∧ys3<tl s ⟹aa#ys3<s " using c 
        by (metis less_cons list.exhaust_sel list.sel(2) nil_less)
      have  th3pre1more21: "aa ∉ A ∧a ∉ A ∧ ys3<tl s∧ys3 setinterleaves ((t1, yu3), A) ∧ 
      hd s = aa ⟶(aa # ys3) setinterleaves ((t1, aa # yu3), A)"
        by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
      from th3pre1more1 th3pre1more2 th3pre1more21 th3pre1 have th3pre1more3: "(aa∉A∧a∉ A∧
      s setinterleaves ((a # list, u), A)∧ t1 < a # list∧length t1>0∧(tl s) setinterleaves 
      ((a#list,lista), A)∧hd s=aa⟶aa#yu3≤u∧aa#ys3<s∧(aa#ys3) setinterleaves ((t1, aa#yu3), A))" 
        using c by blast     
      have th3pre1more32: "aa∉A∧a∉ A∧s setinterleaves ((a # list, aa#lista), A) ∧
      (tl s) setinterleaves ((list,aa#lista), A)∧hd s=a∧ys30<tl s ⟹a#ys30<s " using c 
        by (metis less_cons list.exhaust_sel list.sel(2) nil_less)
      have  th3pre1more213: "aa ∉ A ∧a ∉ A ∧ ys30<tl s∧ys30 setinterleaves ((tl t1, yu30), A) ∧ 
      hd s = a ∧t1<a#list⟶(a # ys30) setinterleaves ((a#tl t1, yu30), A)"  
        by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
      from  th3pre1more32 th3pre12 th3pre1more213 have th3pre1more33: "(aa∉A∧a∉ A∧s setinterleaves 
      ((a # list, u), A)∧ t1 < a # list∧length t1>0∧(tl s) setinterleaves ((list,aa#lista), A)∧
      hd s=a⟶yu30≤u∧a#ys30<s∧(a#ys30) setinterleaves ((t1, yu30), A))" 
        by (metis adsmallPrefix c hd_append2 le_list_def length_greater_0_conv list.exhaust_sel 
        list.sel(1) order.strict_implies_order)  
      from th3pre1more3 th3pre1more33 b c th3pre  have th3NoEmpty: "aa∉A∧a∉ A⟹s setinterleaves 
      ((a # list, u), A)∧t1 < a # list∧length t1>0⟹∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)" 
        apply (simp add: le_list_def less_list_def)  
        by (metis append.simps(2))   
      have th3preEmpty: "aa∉A∧a∉ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list∧length t1=0
      ⟹[]<s∧[]≤u∧ [] setinterleaves ((t1, []), A)"
        apply (simp add: le_list_def less_list_def) using c by auto    
      from th3NoEmpty th3preEmpty have th3: "aa∉A∧a∉ A⟹s setinterleaves ((a # list, u), A)∧t1 < 
      a # list⟹∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)" 
        by blast      
      show?thesis  
        using b c th0 th1 th2 th3 by auto
    qed 
  qed  
qed

lemma mono_Sync2a:
   "r∈min_elems(𝒟 (P ⟦A⟧ S))
   ⟹ ∃t u. r setinterleaves ((t, u),insert tick (ev ` A)) ∧
             (t ∈ min_elems(𝒟 P) ∧ u ∈ 𝒯 S ∨ t ∈ min_elems(𝒟 S) ∧ 
             u ∈ 𝒯 P ∧ u ∈ (𝒯 P - (𝒟 P-min_elems(𝒟 P))))" 
proof- 
  fix r
  assume A: "r ∈ min_elems(𝒟 (P  ⟦A⟧ S))"
  thus "∃t u. r setinterleaves ((t, u), insert tick (ev ` A))∧(t ∈ min_elems(𝒟 P) ∧ 
              u ∈ 𝒯 S ∨ t ∈ min_elems(𝒟 S) ∧ u ∈ 𝒯 P ∧ u ∈ (𝒯 P - (𝒟 P-min_elems(𝒟 P))))" 
  proof(cases "∀t u r1. r1≤r∧ r1 setinterleaves((t, u),insert tick (ev ` A))
                        ⟶ (t ∉ min_elems(𝒟 P)) ∧ (t ∉ min_elems(𝒟 S))")
    case True
    from A have AA: "r ∈ 𝒟 (P  ⟦A⟧ S)"  
      using elem_min_elems by blast
    from AA obtain t1 u1 where A1: 
                   "∃r1≤r. r1 setinterleaves ((t1, u1), insert tick (ev ` A)) ∧
                              (t1 ∈ 𝒟 P ∨ t1 ∈ 𝒟 S)" apply(simp add: D_Sync) 
                              using le_list_def by blast
    from True A1 have A2: "(t1 ∉ min_elems(𝒟 P)) ∧ (t1 ∉ min_elems(𝒟 S))"  
      by blast
    from A1 A2 min_elems5 obtain tm1 tm2 
      where tmA: "(t1∈𝒟 P ⟶ 
                  (tm1≤t1∧tm1∈ min_elems(𝒟 P))) ∧ (t1∈𝒟 S⟶(tm2≤t1∧tm2∈ min_elems(𝒟 S)))"  
      by metis
    from A2 tmA have AB1: "(t1∈𝒟 P⟶tm1<t1)∧(t1∈𝒟 S⟶tm2<t1)" 
      by (metis A1 order.not_eq_order_implies_strict)
    from A1 AB1 obtain um1 rm1 um2 rm2 where AB2: " (t1∈𝒟 P⟶um1≤u1 ∧ rm1 setinterleaves 
    ((tm1, um1),insert tick (ev ` A)))∧(t1∈𝒟 S⟶um2≤u1 ∧ rm2 setinterleaves 
    ((tm2, um2), insert tick (ev ` A)))" by (meson interPrefix)     
    from A1 A2 True tmA AB1 have A3: "(t1∈𝒟 P⟶rm1<r∧rm1∈𝒟(P⟦A⟧S))∧(t1∈𝒟 S⟶rm2<r∧rm2∈ 𝒟(P⟦A⟧S))"  
      by (meson dual_order.strict_implies_order interPrefix order_trans) 
    from A3 AA have ATrue: "r ∉ min_elems(𝒟 (P  ⟦A⟧ S))" using min_elems_def  
      using A1 by blast   
    with A ATrue show ?thesis 
      by blast 
  next
    case False
    from A have dsync: "r∈𝒟 (P ⟦A⟧ S)"  
      by (simp add: local.A elem_min_elems)
    from dsync obtain r1 t2 u2 
      where C: "r1≤r∧ r1 setinterleaves ((t2, u2), insert tick (ev ` A)) ∧
               ((t2 ∈ 𝒟 P ∧ u2 ∈ 𝒯 S) ∨ (t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 P))" 
               apply(simp add: D_Sync)  
               using le_list_def by blast
    from C have r1D: "r1 ∈ 𝒟 (P ⟦A⟧ S)" apply(simp add: D_Sync)  
      using front_tickFree_Nil by blast
    from A C r1D have eq: "r1=r" apply(simp add: min_elems_def) 
      using le_neq_trans by blast
    from A False have minAa: "(t2 ∈ 𝒟 P∧u2∈𝒯 S)⟶(t2 ∈ min_elems(𝒟 P))"  
    proof(cases "t2 ∈ 𝒟 P ∧u2 ∈ 𝒯 S∧ t2 ∉ min_elems(𝒟 P)")
      case True
      from True obtain t3 where inA: "t3<t2∧t3∈min_elems(𝒟 P)" 
        by (metis le_imp_less_or_eq min_elems5)
      from inA obtain r3 u3 where inA1: "u3≤u2∧r3 setinterleaves((t3,u3),insert tick(ev ` A))∧r3<r"  
        using C eq interPrefix by blast 
      from inA1 have inA3: "u3 ∈ 𝒯 S"  
        using True is_processT3_ST_pref by blast
      from inA1 have inA2: "r3 ∈ 𝒟(P ⟦A⟧ S)" apply (simp add: D_Sync)  
        using elem_min_elems front_tickFree_Nil inA inA3 by blast 
      with A eq inA1 show ?thesis 
        by(simp add: min_elems_def) 
    next
      case False
      then show ?thesis 
        by blast
    qed
    from A False have minAb1: "(t2 ∈ 𝒟 S∧u2∈ 𝒯 P)⟶(t2 ∈ min_elems(𝒟 S))"  
    proof(cases "t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 P∧ t2 ∉ min_elems(𝒟 S)")
      case True
      from True obtain t3 r3 u3 where inA: "t3<t2∧t3∈min_elems(𝒟 S)" 
      and inA1: "u3≤u2∧r3 setinterleaves ((t3, u3), insert tick (ev ` A))∧r3<r"
        by (metis C eq interPrefix le_less min_elems5)
      from inA1 have inA3: "u3 ∈ 𝒯 P"  
        using True is_processT3_ST_pref by blast
      from inA1 have inA2: "r3 ∈ 𝒟 (P ⟦A⟧ S)" apply (simp add: D_Sync)  
        using elem_min_elems front_tickFree_Nil inA inA3 by blast 
      with A eq inA1 show ?thesis 
        by(simp add: min_elems_def)
    next
      case False
      then show ?thesis 
        by blast
    qed
    from A False have minAb2: "(t2 ∈ 𝒟 S∧u2∈ 𝒯 P)⟶(u2 ∈ (𝒯 P-(𝒟 P-min_elems(𝒟 P))))" 
    proof(cases "t2 ∈ 𝒟 S ∧u2 ∈ 𝒯 P∧ u2 ∈(𝒟 P-min_elems(𝒟 P))")
      case True
      from True have inAAA: "u2∈𝒟 P∧u2∉min_elems(𝒟 P)" 
        by blast
      from inAAA obtain u3  where inA: "u3<u2∧u3∈min_elems(𝒟 P)"  
        by (metis le_neq_trans min_elems5) 
      from inA obtain t3 r3 where inA1: "t3≤t2∧r3 setinterleaves((t3,u3),insert tick(ev ` A))∧r3<r"  
        using C Sync.sym eq interPrefix by blast
      from inA1 have inA3: "u3 ∈ 𝒟 P∧t3 ∈ 𝒯 S"  
        using D_T True elem_min_elems inA is_processT3_ST_pref by blast 
      from inA1 have inA2: "r3 ∈ 𝒟 (P ⟦A⟧ S)" apply (simp add: D_Sync)  
        using Sync.sym front_tickFree_Nil inA3 by blast  
      with A inA1 inA2 show ?thesis 
        by(simp add: min_elems_def)
    next
      case False
      then show ?thesis 
        by blast
    qed
    with A C show ?thesis   
      using eq minAa minAb1 by blast  
  qed
qed
 
lemma mono_Sync_D3: 
  assumes ordered: "P ⊑ Q" 
  shows "min_elems (𝒟 (P ⟦A⟧ S)) ⊆ 𝒯(Q ⟦A⟧ S)" 
proof- 
  have mono_sync2b:"P ⊑ Q ⟹ ∀r. r ∈ min_elems(𝒟 (P⟦A⟧S))⟶r ∈ 𝒯(Q⟦A⟧S)" 
    apply(frule impI)
    apply(auto simp: mono_Sync2a) 
  proof - 
    fix r
    assume A: "P ⊑ Q"
    and B: "r ∈ min_elems(𝒟(P⟦A⟧S))" 
    from B obtain t u 
      where E: "r setinterleaves ((t, u), insert tick (ev ` A)) ∧ (t ∈ min_elems(𝒟 P)  ∧
                u ∈ 𝒯 S ∨ t ∈ min_elems(𝒟 S) ∧ u ∈ (𝒯 P-(𝒟 P - min_elems(𝒟 P))))" 
               using mono_Sync2a  by blast
    from E have F:"(t ∈ 𝒯 Q ∧ u ∈ 𝒯 S) ∨ (t ∈ 𝒯 S ∧ u ∈ 𝒯 Q)"  
      using le_approx2T le_approx3 ordered by blast     
    thus "r ∈ 𝒯 (Q ⟦A⟧ S)"  
      by (metis (no_types, lifting) E Sync.sym T_Sync UnCI Un_commute insert_is_Un mem_Collect_eq) 
  qed 
  show ?thesis 
    apply(insert ordered) 
    apply(frule mono_sync2b) 
    by blast
qed

lemma mono_D_Sync: "𝒟 (S ⟦ A ⟧ Q) = 𝒟 (Q ⟦ A ⟧ S)"
  by(auto simp: D_Sync)

lemma mono_T_Sync: "𝒯 (S ⟦ A ⟧ Q) = 𝒯 (Q ⟦ A ⟧ S)"
  apply(auto simp: T_Sync)  
  using Sync.sym by fastforce+
   

lemma mono_F_Sync: "ℱ (S ⟦ A ⟧ Q)  = ℱ (Q ⟦ A ⟧ S) "
  apply auto  
   apply (simp add: F_Sync)
  using Sync.sym apply blast
  apply (simp add: F_Sync)
  using Sync.sym by blast

lemma mono_Ra_Sync: "Ra (S ⟦ A ⟧ Q) s = Ra (Q ⟦ A ⟧ S) s"
  apply auto
   apply (auto simp: Ra_def)
  by (auto simp: mono_F_Sync)

lemma mono_Sync[simp]     : "P ⊑ Q ⟹ (P ⟦ A ⟧ S) ⊑ (Q ⟦ A ⟧ S)"
  by(auto simp: le_approx_def mono_Sync_D1 mono_Sync_D2 mono_Sync_D3)

lemma mono_Sync_sym [simp]: "P ⊑ Q ⟹ (S ⟦ A ⟧ P) ⊑ (S ⟦ A ⟧ Q)"
  by (metis Process_eq_spec mono_D_Sync mono_F_Sync mono_Sync)

lemma chain_Sync1: "chain Y ⟹ chain (λi. Y i  ⟦ A ⟧ S)"
  by(simp add: chain_def) 

lemma chain_Sync2: "chain Y ⟹ chain (λi. S  ⟦ A ⟧ Y i)"
  by(simp add: chain_def)

lemma empty_setinterleaving : "[] setinterleaves ((t, u), A) ⟹ t = []"  
  by (cases t, cases u, auto, cases u, simp_all split:if_splits) 

lemma inters_fin_fund: "finite{(t, u). s setinterleaves ((t, u), A)}"
proof (induction "length s" arbitrary:s rule:nat_less_induct)
  case 1
  have A:"{(t, u). s setinterleaves((t, u), A)} ⊆ {([],[])} ∪ 
                   {(t, u). s setinterleaves ((t, u), A) ∧ 
                            (∃ a list. t = a#list  ∧ a ∉ A) ∧ u = []} ∪ 
                   {(t, u). s setinterleaves ((t, u), A) ∧ 
                            (∃ a list. u = a#list ∧ a ∉ A) ∧ t = []} ∪ 
                   {(t, u). s setinterleaves ((t, u), A) ∧ 
                            (∃ a list aa lista. u = a#list ∧ t = aa#lista)}" 
           (is "?A ⊆ {([],[])} ∪ ?B ∪ ?C ∪ ?D") 
    apply (rule subsetI, safe)
          apply(simp_all add: neq_Nil_conv)   
         apply (metis Sync.si_empty2 Sync.sym empty_iff list.exhaust_sel)
        using list.exhaust_sel apply blast
       apply (metis Sync.sym emptyLeftNonSync list.exhaust_sel list.set_intros(1))    
      using list.exhaust_sel apply blast
     apply (metis emptyLeftNonSync list.exhaust_sel list.set_intros(1))
    by (metis Sync.si_empty2 Sync.sym empty_iff list.exhaust_sel)
  have a1:"?B ⊆ { ((hd s#list), [])| list. (tl s) setinterleaves ((list, []), A) ∧ (hd s) ∉ A}" 
  (is "?B  ⊆ ?B1") by auto
  define f where a2:"f = (λa (t, (u::'a event list)). ((a::'a event)#t, ([]::'a event list)))"
  have a3:"?B1 ⊆ {(hd s # list, []) |list. tl s setinterleaves ((list, []), A)} " (is "?B1  ⊆ ?B2") 
    by blast
  from a1 a3 have a13:"?B ⊆ ?B2" 
    by simp
  have AA: "finite ?B" 
  proof (cases s)
    case Nil
    then show ?thesis 
      using not_finite_existsD by fastforce
  next
    case (Cons a list)
    hence aa:"finite{(t,u).(tl s) setinterleaves((t, u), A)}"using 1[THEN spec, of "length (tl s)"] 
      by (simp)
    have "{(hd s#list, [])|list. tl s setinterleaves((list,[]),A)}⊆(λ(t, u).f(hd s)(t, u)) `{(t, u). 
    tl s setinterleaves ((t, u), A)}" using a2 by auto
    hence "finite ?B2" using finite_imageI [of "{(t, u). (tl s) setinterleaves ((t, u), A)}" 
    "λ(t, u). f (hd s) (t, u)", OF aa] using rev_finite_subset by auto 
    then show ?thesis using a13 
      by (meson rev_finite_subset)
  qed
  have a1:"?C ⊆ { ([],(hd s#list))| list. (tl s) setinterleaves (([],list), A) ∧ (hd s) ∉ A}" 
  (is "?C  ⊆ ?C1") by auto
  define f where a2:"f = (λa ((t::'a event list), u). (([]::'a event list), (a::'a event)#u))"
  have a3:"?C1 ⊆ {([],hd s # list) |list. tl s setinterleaves (([],list), A)} " (is "?C1  ⊆ ?C2") 
    by blast
  from a1 a3 have a13:"?C ⊆ ?C2" 
    by simp
  have AAA:"finite ?C"
  proof (cases s)
    case Nil
    then show ?thesis 
      using not_finite_existsD by fastforce
  next
    case (Cons a list)
    hence aa:"finite {(t,u).(tl s)setinterleaves((t, u), A)}"using 1[THEN spec, of "length (tl s)"] 
      by (simp)
    have "{([], hd s # list) |list. tl s setinterleaves (([], list), A)} ⊆ (λ(t, u). 
    f (hd s) (t, u)) ` {(t, u). tl s setinterleaves ((t, u), A)}" using a2 by auto
    hence "finite ?C2" using finite_imageI [of "{(t, u). (tl s) setinterleaves ((t, u), A)}" 
    "λ(t, u). f (hd s) (t, u)", OF aa] using rev_finite_subset by auto 
    then show ?thesis using a13 
      by (meson rev_finite_subset)
  qed
  have dd0:"?D ⊆ {(a#l, aa#la)|a aa l la. s setinterleaves ((a#l, aa#la), A)}" (is "?D ⊆ ?D1")
    apply (rule subsetI, auto, simp split:if_splits) 
    by (blast, blast, metis, blast)
  have AAAA:"finite ?D" 
  proof (cases s)
    case Nil
    hence "?D ⊆ {([],[])}" 
      using empty_setinterleaving by auto
    then show ?thesis 
      using infinite_super by auto
  next
    case (Cons a list)
    hence dd1:"?D1 ⊆ {(a#l, u)| l u. list setinterleaves ((l, u), A)} 
                ∪ {(t, a#la)| t la. list setinterleaves ((t, la), A)} 
                ∪ {(a#l, a#la)|l la. list setinterleaves ((l, la), A)}"(is "?D1 ⊆ ?D2 ∪ ?D3 ∪ ?D4") 
      by (rule_tac subsetI, auto split:if_splits)
    with Cons have aa:"finite {(t,u). list setinterleaves ((t, u), A)}" 
      using 1[THEN spec, of "length list"] by (simp)
    define f where a2:"f = (λ (t, (u::'a event list)). ((a::'a event)# t, u))" 
    with Cons have "?D2 ⊆ (f ` {(t, u). list setinterleaves ((t, u), A)})" 
      using a2 by auto
    hence dd2:"finite ?D2"
      using finite_imageI [of "{(t, u). list setinterleaves ((t, u), A)}" f, OF aa]
      by (meson rev_finite_subset)
    define f where a2:"f = (λ ((t::'a event list),u). (t,(a::'a event)#u))" 
    with Cons have "?D3 ⊆ (f ` {(t, u). list setinterleaves ((t, u), A)})" 
      using a2 by auto
    hence dd3:"finite ?D3"       
      using finite_imageI [of "{(t, u). list setinterleaves ((t, u), A)}" f, OF aa]
      by (meson rev_finite_subset) 
    define f where a2:"f = (λ (t,u). ((a::'a event)#t,(a::'a event)#u))" 
    with Cons have "?D4 ⊆ (f ` {(t, u). list setinterleaves ((t, u), A)})" 
      using a2 by auto
    hence dd4:"finite ?D4"
      using finite_imageI [of "{(t, u). list setinterleaves ((t, u), A)}" f, OF aa]
      by (meson rev_finite_subset)       
    with dd0 dd1 dd2 dd3 dd4 show ?thesis 
      by (simp add: finite_subset) 
  qed    
  from A AA AAA AAAA show ?case 
    by (simp add: finite_subset)    
qed

lemma inters_fin: "finite{(t, u, r). r setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                                     (∃v. x = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = []))}" 
                  (is "finite ?A")
proof -
  have a:"?A⊆(⋃r ∈ {r. r ≤ x}. {a. ∃t u. a=(t,u,r)∧r setinterleaves((t,u),insert tick(ev ` A))})" 
  (is "?A ⊆ (⋃r ∈ {r. r ≤ x}. ?P r)")
    using le_list_def by fastforce
  have b:"∀(r::'a event list). finite (?P r)"
  proof(rule allI)
    fix r::"'a event list"
    define f where "f= (λ((t::'a event list), (u::'a event list)). (t,u,r))"
    hence "?P r ⊆ (f ` {(t, u). r setinterleaves ((t, u), insert tick (ev ` A) )})" 
      by auto
    then show "finite (?P r)" 
      using inters_fin_fund[of r "insert tick (ev ` A)"] finite_imageI[of "{(t, u). r setinterleaves 
      ((t, u), insert tick (ev ` A))}" f]  by (meson rev_finite_subset)   
  qed
  have "{t. ∃t2. x = t @ t2} = {r. ∃ra. r @ ra = x}" 
    by blast
  hence "finite {r. r ≤ x}" using prefixes_fin[of x, simplified Let_def, THEN conjunct1] 
    by (auto simp add:le_list_def) 
  with a b show ?thesis 
    by (meson finite_UN_I infinite_super)
qed  

 
lemma limproc_Sync_D: 
  "chain Y⟹ 𝒟 (lim_proc(range Y)⟦A⟧ S) = 𝒟(lim_proc(range(λi. Y i ⟦A⟧ S)))" 
  apply(auto simp:Process_eq_spec  F_Sync D_Sync T_Sync F_LUB D_LUB T_LUB chain_Sync1) 
      apply blast 
     apply blast 
    using front_tickFree_Nil apply blast
    using front_tickFree_Nil apply blast 
  proof - 
    fix x
    assume A: "chain Y"
    and B: " ∀xa. ∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧ 
                            x = r @ v ∧ r setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                            (t ∈ 𝒟 (Y xa) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ u ∈ 𝒯 (Y xa))"
    thus   "∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧ x = r @ v ∧ 
                      r setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                      ((∀x. t ∈ 𝒟 (Y x)) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ (∀x. u ∈ 𝒯 (Y x)))" 
    proof(cases "∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
                          (r≤x ⟶ ((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ 
                           (t ∈ 𝒟 S ⟶ (∃x. u ∉ 𝒯 (Y x))))") 
      case True 
      from A obtain tryunion where Ctryy: 
                "tryunion={(t, u, r). r setinterleaves ((t, u), insert tick (ev ` A)) ∧
                                      (∃v.(x = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = [])))}" 
        by simp
      from Ctryy inters_fin have tolfin: "finite tryunion" 
        by auto
      obtain tryunion1 
        where Ctryy1: "tryunion1 = {n. ∃(t,u, r) ∈ tryunion.
                                         (t ∈ 𝒟 (Y n) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ u ∈ 𝒯 (Y n))}" by simp
      from B Ctryy1 Ctryy have Ctryy3: "∀n. n∈tryunion1"  
        by blast  
      from Ctryy3 have Ctryy2: "infinite tryunion1"   
        using finite_nat_set_iff_bounded by auto  
      from Ctryy2 Ctryy1 tolfin obtain  r2 t2 u2 
        where Ee: "(t2,u2, r2) ∈ tryunion ∧ 
                   infinite {n. (t2 ∈ 𝒟 (Y n) ∧ u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y n))}"  
        by auto
      from True Ee  Ctryy obtain x1 x2 
        where Ee1: "((t2 ∉ 𝒟 (Y x1)) ∨ u2 ∉ 𝒯 S) ∧ (t2 ∈ 𝒟 S ⟶  (u2 ∉ 𝒯 (Y x2)))" 
        apply (simp add: le_list_def) by blast       
      from Ee Ee1 Ctryy obtain x3 
        where Ee2: "(x1≤x3) ∧ (x2≤x3) ∧ (t2 ∈ 𝒟 (Y x3) ∧ u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y x3))"  
        apply(simp add: infinite_nat_iff_unbounded_le)  
      proof - 
        assume a1: "r2 setinterleaves ((t2, u2), insert tick (ev ` A)) ∧ 
                    (∃v. x = r2 @ v ∧ front_tickFree v ∧ (tickFree r2 ∨ v = [])) ∧ 
                    ((∀m. ∃n≥m. t2 ∈ 𝒟 (Y n) ∧ u2 ∈ 𝒯 S) ∨ 
                     (∀m. ∃n≥m. t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y n)))"
        assume a2: "⋀x3. x1 ≤ x3 ∧ x2 ≤ x3∧(t2 ∈ 𝒟 (Y x3) ∧ u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y x3)) 
                    ⟹ thesis"
        obtain nn :: "nat ⇒ nat" 
          where f3: "∀x0. (∃v1≥x0. t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y v1)) = 
                          (x0 ≤ nn x0 ∧ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y (nn x0)))" by moura
        obtain nna :: "nat ⇒ nat" 
          where "∀x0. (∃v1≥x0. t2 ∈ 𝒟 (Y v1) ∧ u2 ∈ 𝒯 S) = 
                      (x0 ≤ nna x0 ∧ t2 ∈ 𝒟 (Y (nna x0)) ∧ u2 ∈ 𝒯 S)" by moura
        then have f4: "(∀n. n ≤ nna n ∧ t2 ∈ 𝒟 (Y (nna n)) ∧ u2 ∈ 𝒯 S) ∨ 
                       (∀n. n ≤ nn n ∧ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y (nn n)))" using f3 a1 by presburger
        have "(∃n. ¬ n ≤ nn n ∨ t2 ∉ 𝒟 S ∨ u2 ∉ 𝒯 (Y (nn n))) ∨ 
              (∃n≥x1. x2 ≤ n ∧ (t2 ∈ 𝒟 (Y n) ∧ 
                      u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y n)))" by (metis le_cases order.trans) 
        moreover 
        { assume "∃n. ¬ n ≤ nn n ∨ t2 ∉ 𝒟 S ∨ u2 ∉ 𝒯 (Y (nn n))"
          then have "∀n. n ≤ nna n ∧ t2 ∈ 𝒟 (Y (nna n)) ∧ u2 ∈ 𝒯 S" 
            using f4 by blast
          then have "∃n≥x1. x2 ≤ n ∧ (t2 ∈ 𝒟 (Y n) ∧ u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y n))"
            by (metis (no_types) le_cases order.trans) 
        } 
        ultimately show ?thesis 
          using a2 by blast 
      qed 
      from A have Abb1: "∀n1 n2. n1≤n2 ⟶ Y n1 ⊑ Y n2" 
        by (simp add: po_class.chain_mono)
      from A Abb1 have Abb2: "∀n1 n2. n1>n2 ∧ t ∉ 𝒟 (Y n2) ⟶ t ∉ 𝒟 (Y n1)" 
        using le_approx1 less_imp_le_nat by blast
      from A Abb1 have Abb3: "∀n1 n2. n1>n2 ∧ t ∉ 𝒯 (Y n2) ⟶ t ∉ 𝒯 (Y n1)"  
        by (meson NT_ND le_approx2T less_imp_le_nat)
      from Abb2 Ee2 have Ab1: "t2 ∉ 𝒟 (Y x1)⟶t2 ∉ 𝒟 (Y x3)"  
        by (meson Abb1 le_approx1 less_imp_le_nat subsetCE)
      from Abb3 have Ab2: "u2 ∉ 𝒯 (Y x2)⟶u2 ∉ 𝒯 (Y x3)"  
        by (meson Abb1 Ee2 NT_ND le_approx2T less_imp_le_nat)
      from True Ee Ee1  Ee2 Ab1 Ab2 show ?thesis  
        by blast 
    next 
      case False 
      from A B False obtain t u r 
        where Bb1: "r setinterleaves ((t, u), insert tick (ev ` A)) ∧ r ≤ x ∧ 
                    ((∀x. t ∈ 𝒟 (Y x)) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ (∀x. u ∈ 𝒯 (Y x)))"   
        by auto
      from B have Bb21: "front_tickFree x"  
        by (metis D_imp_front_tickFree append_Nil2 front_tickFree_append ftf_Sync is_processT2_TR)
      from B Bb1 have Bb2: "∃v. front_tickFree v ∧ (tickFree r ∨ v = [])∧ x = r @ v"  
        by (metis Bb21 front_tickFree_Nil front_tickFree_mono le_list_def)  
      then show ?thesis  
        using Bb1 by blast  
    qed  
  qed  
   

lemma limproc_Sync_F_annex1: 
  " chain Y
    ⟹ ∀n. (a, b) ∈ ℱ (Y n ⟦A⟧ S) 
    ⟹ ∃x. a ∉ 𝒟 (Y x ⟦A⟧ S) 
    ⟹ ∃t u X. (∀x. (t, X) ∈ ℱ (Y x)) ∧ 
                (∃Y. (u, Y) ∈ ℱ S ∧ a setinterleaves((t, u),insert tick (ev ` A)) ∧ 
                b = (X ∪ Y) ∩ insert tick (ev ` A) ∪ X ∩ Y)"
proof - 
  fix a b
  assume A: "chain Y"
  assume B: "∀n. (a, b) ∈ ℱ (Y n ⟦A⟧ S)"
  assume C: "∃x. a ∉ 𝒟 (Y x ⟦A⟧ S)"
  thus "∃t u X. (∀x. (t, X) ∈ ℱ (Y x)) ∧
                (∃Y. (u, Y) ∈ ℱ S ∧ 
                     a setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                     b = (X ∪ Y) ∩ insert tick (ev ` A) ∪ X ∩ Y)" 
  proof- 
    from B C obtain x1 where D: "a ∉ 𝒟 (Y x1 ⟦A⟧ S)" 
      by blast
    from B D obtain t1 u1 X1 Y1 where E: 
         "a setinterleaves ((t1, u1), insert tick (ev ` A)) ∧
         (t1, X1) ∈ ℱ (Y x1) ∧ (u1, Y1) ∈ ℱ S ∧ 
         b = (X1 ∪ Y1) ∩ insert tick (ev ` A) ∪ X1 ∩ Y1" 
      apply(auto simp: D_Sync F_Sync) 
      by fastforce
    from B D E have F: "t1 ∉ 𝒟 (Y x1) ∧ t1 ∈ 𝒯(Y x1)" apply(auto simp: D_Sync)  
      using F_T front_tickFree_Nil apply blast  
      by (simp add: F_T)
    from F have ee: "∀i. (t1, X1) ∈ ℱ (Y i)∧(u1, Y1)∈ ℱ S∧ a setinterleaves 
    ((t1, u1), insert tick (ev ` A))∧ b = (X1 ∪ Y1) ∩ insert tick (ev ` A) ∪ X1 ∩ Y1"  
      using E chain_lemma is_processT8_S le_approx2 local.A by metis
    with A B C D E F ee  show?thesis 
      by blast 
  qed
qed

lemma limproc_Sync_F_annex2: 
 "chain Y 
  ⟹ ∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
      (∀v. a = r @ v ⟶ front_tickFree v ⟶ 
           ¬ tickFree r ∧ v ≠ [] ∨ ((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ 
           (t ∈ 𝒟 S ⟶ (∃x. u ∉ 𝒯 (Y x))))
  ⟹ ∃x. a ∉ 𝒟(Y x ⟦ A ⟧ S)" 
  apply(auto simp: D_Sync) 
proof-
  fix a
  assume A: "∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶ 
                     (∀v. a = r @ v ⟶  front_tickFree v ⟶ 
                          ¬ tickFree r ∧ v ≠ [] ∨ 
                         ((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶  (∃x. u ∉ 𝒯 (Y x))))"
  assume B: "chain Y"
  thus "∃x. ∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
           (∀v. a = r @ v ⟶  front_tickFree v ⟶ 
           ¬ tickFree r∧v≠[] ∨ (t ∈ 𝒟 (Y x) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y x)))" 
  proof- 
    from B have D: "((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ (∃x. u ∉ 𝒯 (Y x)))
                    ⟹  (∃x. ((t ∈ 𝒟 (Y x) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y x))))" 
      by (meson D_T chain_lemma le_approx1 le_approx2T subsetCE)
    from A obtain tryunion 
      where Ctryy: "tryunion={(t, u, r). r setinterleaves ((t, u), insert tick (ev ` A)) ∧
                    (∃v. a = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = []))}" 
      by simp
    from Ctryy have tolfin: "finite tryunion" 
      using inters_fin by auto 
    from B have Abb1: "∀n1 n2. n1≤n2 ⟶ Y n1 ⊑ Y n2"  
      by (simp add: po_class.chain_mono)
   from A Abb1 have Abb2: "∀n1 n2 t. n1>n2∧t ∉ 𝒟 (Y n2)⟶t ∉ 𝒟 (Y n1)" 
      using le_approx1 less_imp_le_nat by blast
   from A Abb1 have Abb3: "∀n1 n2 t. n1>n2∧t ∉ 𝒯 (Y n2)⟶t ∉ 𝒯 (Y n1)"  
      by (meson NT_ND le_approx2T less_imp_le_nat)
    from Abb2 Abb3 
    have oneIndexPre: "∀t u. ((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ 
                             (∃x. u ∉ 𝒯 (Y x))) ⟶
                             (∃x. (t ∉ 𝒟 (Y x) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y x)))"
      by (meson B D_T ND_F_dir2' chain_lemma le_approx1 subsetCE)  
    from A B oneIndexPre Abb2 Abb3  
    have oneIndex: "∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶ 
                            (∀v. a = r @ v ⟶front_tickFree v ⟶ ¬ tickFree r∧v≠[] ∨
                            ( ∃x.( (( t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ (u ∉ 𝒯 (Y x))))))" by blast
    define proUnion1 
      where finiUnion: "proUnion1 = {n. ∃(t,u, r)∈tryunion. (((t ∈ 𝒟 (Y n) ⟶ u ∉ 𝒯 S) ∧ 
                                            (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y n)))∧ 
                                            (∀m. ( (t ∈ 𝒟 (Y m)⟶u ∉ 𝒯 S) ∧ 
                                                   (t ∈ 𝒟 S⟶u ∉ 𝒯 (Y m)))⟶n≤m))}"
    from B 
    have finiSet1: "⋀r t u. (t,u, r) ∈ tryunion 
                             ⟹ finite {n1.(((t ∈ 𝒟 (Y n1)⟶u ∉ 𝒯 S) ∧ 
                                 (t∈𝒟 S⟶u∉𝒯(Y n1)))∧(∀m1. ((t ∈ 𝒟 (Y m1) ⟶
                                     u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y m1)))⟶n1≤m1))}"  
     by (metis (no_types, lifting) infinite_nat_iff_unbounded mem_Collect_eq not_less)
   from B tolfin finiUnion oneIndex finiSet1  have finiSet: "finite proUnion1"  
     by auto   
   from finiSet obtain proMax where ann: "proMax=Max(proUnion1)"  
     by blast   
   from ann Abb2 have ann1: "∀num∈proUnion1. ∀t. t ∉ 𝒟 (Y num)⟶t ∉ 𝒟 (Y proMax)"  
     by (meson Abb1 Max_ge finiSet le_approx1 subsetCE)    
   from ann Abb3 have ann2: "∀num∈proUnion1.  ∀t. t ∉ 𝒯 (Y num)⟶t ∉ 𝒯 (Y proMax)"  
     by (meson Abb1 D_T Max_ge finiSet le_approx2T)
   from finiUnion 
   have ann3: "∀num∈proUnion1. ∃r t u. r setinterleaves((t, u),insert tick (ev ` A)) ⟶ 
                                   (∀v. a = r @ v ⟶front_tickFree v ⟶ 
                                         ¬ tickFree r ∧ v ≠ [] ∨(( ((t∉𝒟(Y num))∨u ∉ 𝒯 S) ∧ 
                                         (t ∈ 𝒟 S ⟶ (u ∉ 𝒯 (Y num))))))" by auto
   obtain proUnion2 
     where ann0: "proUnion2 ={(t, u, r).∃n. (t, u, r) ∈ tryunion ∧
                                            ((t ∈ 𝒟 (Y n)⟶u ∉ 𝒯 S) ∧ 
                                            (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y n)))}" by auto 
   from ann0 Ctryy finiUnion 
   have ann1: "⋀t u r.  (t, u, r)∈ proUnion2
                        ⟹∃num. num∈proUnion1 ∧ ((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧ 
                                 (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num)))"    
   proof- 
     fix t u r
     assume a:  "(t, u, r)∈ proUnion2"
     define P where PP:"P = (λnum. ((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num))))"
     thus "∃num. num∈proUnion1∧ P num" 
     proof- 
       from finiUnion obtain minIndexRB where ann1preB: "minIndexRB={n. (P n)}" 
         by auto
       from B ann1preB obtain minmin where ab: "(minmin::nat) = Inf (minIndexRB)" 
         by auto
       from ann0 ann1preB PP have ann1preNoEmpty1: "minIndexRB ≠ {}" 
         using a by blast
       from ab ann1preNoEmpty1 have ann1pre0:"minmin ∈ minIndexRB" 
         using Inf_nat_def wellorder_Least_lemma(1) by force        
       have "minmin∈ {n. ∃t u r. (t,u,r)∈tryunion ∧ ((t ∈ 𝒟 (Y n) ⟶ u ∉ 𝒯 S) ∧ 
                                 (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y n))) ∧ (∀m. (t ∈ 𝒟 (Y m) ⟶ 
                                   u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y m)) ⟶ n ≤ m)}"  
         apply(rule CollectI,rule_tac x=t in exI,rule_tac x=u in exI,rule_tac x=r in exI,intro conjI)
            using a ann0 apply blast          
           using PP ann1pre0 ann1preB apply blast
           using PP ann1pre0 ann1preB apply blast 
          by (simp add: Inf_nat_def PP ab ann1preB wellorder_Least_lemma(2)) 
       then show ?thesis  
         using ann1pre0 ann1preB finiUnion by blast 
     qed 
   qed 
   from ann1 
   have ann12: "∀t u r. ∃num.(t, u, r) ∈ proUnion2 ⟶ num∈proUnion1 ∧
                             ((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num)))" by auto
   from ann0 Ctryy 
   have ann2: "∀t u r. (t, u, r) ∈ proUnion2 ⟶ 
                        (r setinterleaves ((t, u), insert tick (ev ` A)) ∧
                        (∃v. a = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = [])) ∧ 
                        (∃nu1. (t ∈ 𝒟 (Y nu1) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y nu1))))" by simp 
   have ann15: "∀t u r. (r setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                         (∃v. a = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = [])) ∧ 
                         (∃nu1. (t ∈ 𝒟 (Y nu1) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y nu1)))) ⟶
                                (t, u, r) ∈ proUnion2"  
     using Ctryy ann0 by blast   
   from  ann12 ann15 
   have ann01: "∀t u r. ((r setinterleaves ((t, u), insert tick (ev ` A)) ∧
                        (∃v. a = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = [])) ∧ 
                        (∃nu1. (t ∈ 𝒟 (Y nu1)⟶u ∉ 𝒯 S) ∧ 
                        (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y nu1))))⟶
                           (∃num∈proUnion1. ((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧ 
                              (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num)))))"    by blast  
   from ann01  
   have annhelp: "∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
                  (∀v. a = r @ v ⟶ front_tickFree v ⟶(tickFree r ∨ v = [])⟶
                  (∃num∈proUnion1.((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num)))))"
     by (metis oneIndex)     
   from Abb1 Abb2 
   have annHelp2: "∀nn t u.
                      nn ∈ proUnion1 ∧ (t ∈ 𝒟 (Y nn) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y nn)) ⟶
                      (t ∈ 𝒟 (Y proMax) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y proMax))" 
     by (metis Abb3 Max_ge ann finiSet le_neq_trans) 
   from  annHelp2 annhelp 
   have annHelp1: "∀t u r.
                       r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
                       (∀v. a = r @ v ⟶
                            front_tickFree v ⟶
                            tickFree r ∨ v = [] ⟶ (t ∈ 𝒟 (Y proMax) ⟶ u ∉ 𝒯 S) ∧ 
                                                    (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y proMax)))" by blast       
   with A B  show ?thesis  
     by blast 
 qed 
qed

lemma limproc_Sync_F: 
 "chain Y ⟹ ℱ(lim_proc (range Y)⟦ A ⟧S) = ℱ(lim_proc (range (λi. Y i ⟦ A ⟧ S)))" 
  apply(auto simp add: Process_eq_spec D_Sync F_Sync F_LUB D_LUB T_LUB chain_Sync1) 
       apply blast 
      apply blast 
     apply blast 
    using front_tickFree_Nil apply blast
   using front_tickFree_Nil apply blast     
  proof- 
    fix a b
    assume A1: " ∀x. (∃t u X. (t, X) ∈ ℱ (Y x) ∧ 
                              (∃Y. (u, Y) ∈ ℱ S ∧ 
                              a setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                              b = (X ∪ Y) ∩ insert tick (ev ` A) ∪ X ∩ Y)) ∨
                     (∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧  a = r @ v ∧ 
                              r setinterleaves ((t, u), insert tick (ev ` A)) ∧ 
                              (t ∈ 𝒟 (Y x) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ u ∈ 𝒯 (Y x)))"
    and B: " ∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶ 
                     (∀v. a = r @ v ⟶  front_tickFree v ⟶ 
                         ¬ tickFree r ∧ v ≠ [] ∨ 
                         ((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶  (∃x. u ∉ 𝒯 (Y x))))"
    and C: "chain Y"
    thus  "∃t u X. (∀x. (t, X) ∈ ℱ (Y x)) ∧(∃Y. (u, Y) ∈ ℱ S ∧ a setinterleaves 
    ((t, u), insert tick (ev ` A)) ∧ b = (X ∪ Y) ∩ insert tick (ev ` A) ∪ X ∩ Y)" 
    proof (cases "∃m. a ∉ 𝒟(Y m ⟦ A ⟧ S)") 
      case True 
      then obtain m where "a ∉ 𝒟(Y m ⟦ A ⟧ S)" 
        by blast
      with A1 have D: "∀n. (a, b)∈ ℱ (Y n ⟦ A ⟧ S)"
        by (auto simp: F_Sync)
      with A1 B C  show ?thesis 
        apply(erule_tac x=m in allE)    
        apply(frule limproc_Sync_F_annex2) 
         apply simp 
        by(simp add: limproc_Sync_F_annex1) 
    next 
      case False
      with False have E: "∀n.  a ∈ 𝒟 (Y n ⟦ A ⟧ S)" 
        by blast
      with C E B show ?thesis 
        apply auto 
        apply(drule limproc_Sync_F_annex2) 
         apply blast 
        by fast 
    qed 
  qed
  
lemma cont_left_Sync : "chain Y ⟹ ((⨆ i. Y i) ⟦ A ⟧ S) = (⨆ i. (Y i ⟦ A ⟧ S))"
  by(simp add: Process_eq_spec chain_Sync1 limproc_Sync_D limproc_Sync_F limproc_is_thelub) 
  
lemma cont_right_Sync : "chain Y ⟹ (S ⟦ A ⟧ (⨆ i. Y i)) = (⨆ i. (S ⟦ A ⟧ Y i))"
  by (metis (no_types, lifting) Process_eq_spec cont_left_Sync lub_eq mono_D_Sync mono_F_Sync)

lemma Sync_cont[simp]: 
assumes f:"cont f" 
and     g:"cont g"
shows     "cont (λx. (f x) ⟦A⟧ (g x))" 
proof - 
  have A : "⋀x. cont g ⟹ cont (λy. y ⟦A⟧ (g x))" 
    apply (rule contI2, rule monofunI) 
     apply(auto) 
    by (simp add: cont_left_Sync)
  have B : "⋀y. cont g ⟹ cont (λx. y ⟦A⟧ g x)" 
    apply(rule_tac c="(λ x. y  ⟦A⟧ x)" in cont_compose) 
     apply(rule contI2, rule monofunI) 
      apply (simp) 
     apply (simp add: cont_right_Sync) 
    by simp 
  show ?thesis using f g  
    apply(rule_tac  f="(λx. (λ f. f ⟦A⟧ g x))" in cont_apply) 
    by(auto intro:contI2 simp:A B)
qed 



end