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 tt1A)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=aaaa Asa setinterleaves ((t, u), A) 
                              (tl sa) setinterleaves ((list,lista), A)" by auto
       from th0pre a b c have th0pre1: "a=aaaa Asa 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=aaaa Asa 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: "aAaa Asa setinterleaves ((t, u), A) 
                             (tl sa) setinterleaves ((list,aa#lista), A)" by auto
      from th1pre a b c have th1pre1: "aAaa Asa 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: "aAaa Asa 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: "aaAa Asa setinterleaves ((t, u), A) 
                             (tl sa) setinterleaves ((a#list,lista), A)" by auto
      from th2pre a b c have th2pre1: "aaAa Asa 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: "aaAa Asa 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: "aaAa Asa 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: "aaAa Asa 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: "aaAa Asa 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: "aaAa Asa 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=aaaa Asa setinterleaves ((t, u), A) 
      (tl sa) setinterleaves ((list,lista), A)" by auto
      from th0pre a b c have th0pre1: "a=aaaa Asa 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=aaaAsa setinterleaves ((t, u), A)  y1  A  
      (sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto 
      from b c have th1pre: "aAaa Asa setinterleaves ((t, u), A) 
      (tl sa) setinterleaves ((list,aa#lista), A)" by auto
      from th1pre a b c have th1pre1: "aAaa Asa 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: "aAaa Asa setinterleaves ((t, u), A)  y1  A  
      (sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto  
      from b c have th2pre: "aaAa Asa setinterleaves ((t, u), A) 
      (tl sa) setinterleaves ((a#list,lista), A)" by auto
      from th2pre a b c have th2pre1: "aaAa Asa 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: "aaAa Asa setinterleaves ((t, u), A)  y1  A  
      (sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto
      from b c have th3pre: "aaAa Asa 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: "aaAa Asa 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: "aaAa Asa 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: "aaAa Asa 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=aaaa As1 setinterleaves ((t, u), A)
      (tl s1) setinterleaves ((list,lista), A)" by auto
      from th0pre a b c have th0pre1: "a=aaaa As1 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=aaaa As1 setinterleaves ((t, u), A) 
      rev s1 setinterleaves ((rev t, rev u), A)"   using addSync by fastforce 
      from b c have th1pre: "aAaa As1 setinterleaves ((t, u), A)
      (tl s1) setinterleaves ((list,aa#lista), A)" by auto
      from th1pre a b c have th1pre1: "aAaa As1 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: "aAaa As1 setinterleaves ((t, u), A) 
      rev s1 setinterleaves ((rev t, rev u), A)"  using addNonSync by fastforce  
      from b c have th2pre: "aaAa As1 setinterleaves ((t, u), A)
      (tl s1) setinterleaves ((a#list,lista), A)" by auto
      from th2pre a b c have th2pre1: "aaAa As1 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: "aaAa As1 setinterleaves ((t, u), A) 
      rev s1 setinterleaves ((rev t, rev u), A)"  
        using addNonSync by fastforce 
      from b c have th3pre: "aaAa As1 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: "aaAa As1 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: "aaAa As1 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: "aaAa As1 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: "aaAa As1 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: "aaAa 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: "(aset(u)aset(t)aset(t)aset(u))aAsetinterleaving(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. t1set ut1A)"  
    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. t1set u1t1A)  
  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)
                  t1tau1us 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=aaa A(s@t) setinterleaves ((ta, u), A)length s >1 
       yb=tl s" by blast
       with b c have thp4: "a=aaa 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=aaa 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 syb setinterleaves ((yt, yu), A)ytlistyulista"  using thp5 by blast 
       from thp thp1 have thp2: "a=aaa 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=aaa 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=aaa A (s @ t) setinterleaves ((ta, u), A)  length s=0
       s setinterleaves (([], []), A)" by auto
       from thp1 have thp7: "a=aaa 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=aaa At1 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: "aAaa 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: "aAaa A(s @ t) setinterleaves ((ta, u), A)
      length s>0yt1list 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: "yt1lista#yt1ta"  
        by (simp add: le_less less_cons) 
      from b c have th1pre3: "aAaa Atl 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: "aAaa A(s @ t) setinterleaves ((ta, u), A)
      length s>0 a#yt1ta yu1 u s setinterleaves ((a#yt1, yu1), A)" 
        using th1pre th1pre3  by fastforce  
      have th1pre5:"aAaa A(s @ t) setinterleaves ((ta, u), A)length s=0 []ta [] u 
      s setinterleaves (([], []), A)" by auto
      have th1: "aAaa At1 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: "aaAa 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: "aaAa A(s @ t) setinterleaves ((ta, u), A)
      length s>0yt2ta 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: "yu2listaaa#yu2u"   
        by (simp add: le_less less_cons) 
      from b c have th2pre3: "aaAa Atl 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: "aaAa A(s @ t) setinterleaves ((ta, u), A)
      length s>0 yt2ta aa#yu2 u s setinterleaves ((yt2, aa#yu2), A)" 
        using th2pre th2pre3  by fastforce  
      have th2pre5:"aaAa A(s @ t) setinterleaves ((ta, u), A)length s=0 
      []ta [] u s setinterleaves (([], []), A)" by auto
      have th2: "aaAa At1 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: "aaAa A(s @ t) setinterleaves ((ta, u), A)tl (s @ t) 
      setinterleaves ((ta, lista), A)hd (s@t)=aatl (s @ t)setinterleaves((list, u), A)hd(s@t)=a" 
        by auto
      from a b c th3pre obtain yt31 yu31 where th3pre1: "aaAa A
      (s @ t) setinterleaves ((ta, u), A)tl (s @ t) setinterleaves ((ta, lista), A)
      hd (s@t)=aalength s>0yt31ta 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: "aaAaA(s@t)setinterleaves ((ta, u),A)
      tl (s @ t) setinterleaves ((list, u), A)hd (s@t)=alength s>0yt32list 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: "aaAa Atl 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: "aaAa A(s @ t) setinterleaves ((ta, u), A)
      length s>0tl (s @ t) setinterleaves ((ta, lista), A)hd (s@t)=aa yt31ta 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: "aaAa Atl 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: "aaAa A(s @ t) setinterleaves ((ta, u), A)
      length s>0tl (s @ t) setinterleaves ((list, u), A)hd (s@t)=a a#yt32ta 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:"aaAa A(s @ t) setinterleaves ((ta, u), A)length s=0 
      []ta [] u s setinterleaves (([], []), A)" by auto
      have th3: "aaAa At1 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. u1utickFree u1  (u2utickFree u2u2u1)"   
      by (metis append.right_neutral append_eq_first_pref_spec front_tickFree_charn le_list_def 
         tickFree_Nil)
    from A A1 have AA1: "u1=uu=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. t1ttickFree t1  (t2ttickFree t2t2t1)"
      by (metis append.right_neutral append_eq_first_pref_spec front_tickFree_charn le_list_def 
      tickFree_Nil)
    from B B1 have BB1: "t1=tt=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=ut1=ttickFree s" 
      by (simp add: C C1)
    from AA1 BB1 have CC2: "u1=ut=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=ttickFree 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=(Yinsert tick (ev ` A)))(Y2=(Y - insert tick (ev ` A)))" 
      by blast
    from A1 have AA1: "Y1  Y2 = Y" 
      by blast 
    from A1 have newAA: "yY1. y insert tick (ev ` A)" 
      by blast
    from A1 have newAAA: "yY2. y insert tick (ev ` A)" 
      by blast
    from B A1 have AA2: "zY1.(t@[z], {})   P  (u@[z], {})   Q" 
    proof(cases "z  Y1. (t@[z], {}) P  (u@[z], {})   Q")
      case True
      from True obtain z1 where TrA: "z1Y1(t@[z1], {}) P  (u@[z1], {})   Q" 
        by blast
      from TrA A have TrB: 
             "sa setinterleaves ((t,u),insert tick(ev ` A)); 
               z1insert 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=Z1Z2" 
      by blast
    from A2 have BAA: "zZ1. (t@[z], {})   P" 
      by blast
    from A2 have BAAA: "zZ2. (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: "yY2. (t@[y], {})  P  (u@[y], {})  Q" 
    proof(cases "yY2. ((t@[y], {})  P)((u@[y], {})  Q)")
      case True
      from True obtain y1 where innAA: "y1Y2(((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=(XaZ1Y2)" 
      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=(YaZ2Y2)" 
      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)=((XaYaY1Y2)  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:"((XaYaY1Y2)insert tick(ev `A))=((XaYa)insert tick(ev `A)Y1)" 
      by (simp add: Int_Un_distrib2)
    from AA1 BA B1 B2 have A65: "(XbbYbb)((XaYa)Y) " 
      by auto  
    from AA1 BA B1 B2 have A66:"(XbbYbb)((XaYa)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)