Theory Throw_Non_Destructive

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


section ‹Non Destructiveness of Throw›


(*<*)
theory Throw_Non_Destructive
  imports Process_Restriction_Space "HOL-CSP_OpSem.Initials"
begin
  (*>*)


subsection ‹Equality›

lemma Depth_Throw_1_is_constant: ‹P Θ a ∈ A. Q1 a ↓ 1 = P Θ a ∈ A. Q2 a ↓ 1›
proof (rule FD_antisym)
  show ‹P Θ a ∈ A. Q2 a ↓ 1 ⊑FD P Θ a ∈ A. Q1 a ↓ 1› for Q1 Q2
  proof (unfold refine_defs, safe)
    show div :  ‹t ∈ 𝒟 (Throw P A Q1 ↓ 1) ⟹ t ∈ 𝒟 (Throw P A Q2 ↓ 1)› for t
    proof (elim D_restriction_processptickE) 
      assume ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a)› and ‹length t ≤ 1›
      from ‹length t ≤ 1› consider ‹t = []› | e where ‹t = [e]› by (cases t) simp_all
      thus ‹t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)›
      proof cases
        from ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a)› show ‹t = [] ⟹ t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)›
          by (simp add: D_restriction_processptick D_Throw)
      next
        fix e assume ‹t = [e]›
        with ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a)›
        consider ‹[] ∈ 𝒟 P› | a where ‹t = [ev a]› ‹[ev a] ∈ 𝒟 P› ‹a ∉ A›
          | a where ‹t = [ev a]› ‹[ev a] ∈ 𝒯 P› ‹a ∈ A›
          by (auto simp add: D_Throw disjoint_iff image_iff)
            (metis D_T append_Nil eventptick.exhaust process_charn,
              metis append_Nil empty_iff empty_set hd_append2 hd_in_set in_set_conv_decomp set_ConsD)
        thus ‹t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)›
        proof cases
          show ‹t = [ev a] ⟹ [ev a] ∈ 𝒯 P ⟹ a ∈ A ⟹ t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)› for a
            by (simp add: D_restriction_processptick T_Throw)
              (metis append_Nil append_self_conv front_tickFree_charn inf_bot_left
                is_ev_def is_processT1_TR length_0_conv length_Cons list.set(1)
                tickFree_Cons_iff tickFree_Nil)
        next
          show ‹[] ∈ 𝒟 P ⟹ t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)›
            by (simp flip: BOT_iff_Nil_D add: D_BOT)
              (use ‹t = [e]› front_tickFree_single in blast)
        next
          show ‹t = [ev a] ⟹ [ev a] ∈ 𝒟 P ⟹ a ∉ A ⟹ t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)› for a  
            by (simp add: D_restriction_processptick D_Throw disjoint_iff image_iff)
              (metis append.right_neutral empty_set eventptick.disc(1) eventptick.sel(1)
                front_tickFree_Nil list.simps(15) singletonD tickFree_Cons_iff tickFree_Nil)
        qed
      qed
    next
      fix u v assume * : ‹t = u @ v› ‹u ∈ 𝒯 (Throw P A Q1)› ‹length u = 1› ‹tF u› ‹ftF v›
      from ‹length u = 1› ‹tF u› obtain a where ‹u = [ev a]›
        by (cases u) (auto simp add: is_ev_def)
      with "*"(2) show ‹t ∈ 𝒟 (Throw P A Q2 ↓ 1)›
        by (simp add: ‹t = u @ v› D_restriction_processptick Throw_projs Cons_eq_append_conv)
          (metis (no_types) "*"(3-5) One_nat_def append_Nil empty_set inf_bot_left
            insert_disjoint(2) is_processT1_TR list.simps(15))
    qed

    show ‹(t, X) ∈ ℱ (Throw P A Q1 ↓ 1) ⟹ (t, X) ∈ ℱ (Throw P A Q2 ↓ 1)› for t X
    proof (elim F_restriction_processptickE)
      assume ‹(t, X) ∈ ℱ (P Θ a ∈ A. Q1 a)› ‹length t ≤ 1›
      then consider ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a)› | ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` A = {}›
        | a where ‹t = [ev a]› ‹[ev a] ∈ 𝒯 P› ‹a ∈ A›
        by (auto simp add: F_Throw D_Throw)
      thus ‹(t, X) ∈ ℱ (P Θ a ∈ A. Q2 a ↓ 1)›
      proof cases
        from D_F div ‹length t ≤ 1›
        show ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a) ⟹ (t, X) ∈ ℱ (P Θ a ∈ A. Q2 a ↓ 1)›
          using D_restriction_processptickI by blast
      next
        show ‹(t, X) ∈ ℱ P ⟹ set t ∩ ev ` A = {} ⟹ (t, X) ∈ ℱ (Throw P A Q2 ↓ 1)›
          by (simp add: F_restriction_processptick F_Throw)
      next
        show ‹⟦t = [ev a]; [ev a] ∈ 𝒯 P; a ∈ A⟧ ⟹ (t, X) ∈ ℱ (Throw P A Q2 ↓ 1)› for a
          by (simp add: F_restriction_processptick T_Throw)
            (metis append.right_neutral append_Nil empty_set eventptick.disc(1)
              front_tickFree_Nil inf_bot_left is_processT1_TR length_Cons
              list.size(3) tickFree_Cons_iff tickFree_Nil)
      qed
    next
      fix u v assume * : ‹t = u @ v› ‹u ∈ 𝒯 (Throw P A Q1)› ‹length u = 1› ‹tF u› ‹ftF v›
      from ‹length u = 1› ‹tF u› obtain a where ‹u = [ev a]›
        by (cases u) (auto simp add: is_ev_def)
      with "*"(2) show ‹(t, X) ∈ ℱ (Throw P A Q2 ↓ 1)›
        by (simp add: ‹t = u @ v› F_restriction_processptick Throw_projs Cons_eq_append_conv)
          (metis (no_types) "*"(3-5) One_nat_def append_Nil empty_set inf_bot_left
            insert_disjoint(2) is_processT1_TR list.simps(15))
    qed
  qed

  thus ‹P Θ a ∈ A. Q2 a ↓ 1 ⊑FD P Θ a ∈ A. Q1 a ↓ 1› by simp
qed



subsection ‹Refinement›

lemma restriction_processptick_Throw_FD :
  ‹(P Θ a ∈ A. Q a) ↓ n ⊑FD (P ↓ n) Θ a ∈ A. (Q a ↓ n)› (is ‹?lhs ⊑FD ?rhs›)
proof (unfold refine_defs, safe)
  show ‹t ∈ 𝒟 ?lhs› if ‹t ∈ 𝒟 ?rhs› for t
  proof -
    from ‹t ∈ 𝒟 ?rhs›
    consider t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒟 (P ↓ n)› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 (P ↓ n)›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q a ↓ n)›
      unfolding D_Throw by blast
    thus ‹t ∈ 𝒟 ?lhs›
    proof cases
      show ‹⟦t = t1 @ t2; t1 ∈ 𝒟 (P ↓ n); tF t1; set t1 ∩ ev ` A = {}; ftF t2⟧ ⟹ t ∈ 𝒟 ?lhs› for t1 t2
        by (elim D_restriction_processptickE, simp_all add: Throw_projs D_restriction_processptick)
          (blast, metis (no_types, lifting) front_tickFree_append inf_sup_aci(8) inf_sup_distrib2 sup_bot_right)
    next
      fix t1 a t2
      assume ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 (P ↓ n)›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q a ↓ n)›
      from ‹t2 ∈ 𝒟 (Q a ↓ n)› show ‹t ∈ 𝒟 ?lhs›
      proof (elim D_restriction_processptickE)
        from ‹t1 @ [ev a] ∈ 𝒯 (P ↓ n)› show ‹t2 ∈ 𝒟 (Q a) ⟹ length t2 ≤ n ⟹ t ∈ 𝒟 ?lhs›
        proof (elim T_restriction_processptickE)
          from ‹a ∈ A› ‹set t1 ∩ ev ` A = {}› ‹t = t1 @ ev a # t2›
          show ‹t2 ∈ 𝒟 (Q a) ⟹ t1 @ [ev a] ∈ 𝒯 P ⟹ t ∈ 𝒟 ?lhs›
            by (auto simp add: D_restriction_processptick D_Throw)
        next
          fix u v assume ‹t2 ∈ 𝒟 (Q a)› ‹length t2 ≤ n› ‹t1 @ [ev a] = u @ v›
            ‹u ∈ 𝒯 P› ‹length u = n› ‹tF u› ‹ftF v›
          from ‹t1 @ [ev a] = u @ v› ‹ftF v› consider ‹t1 @ [ev a] = u›
            | v' where ‹t1 = u @ v'› ‹v = v' @ [ev a]› ‹ftF v'›
            by (cases v rule: rev_cases) (simp_all add: front_tickFree_append_iff)
          thus ‹t ∈ 𝒟 ?lhs›
          proof cases
            from ‹a ∈ A› ‹length u = n› ‹set t1 ∩ ev ` A = {}› ‹t2 ∈ 𝒟 (Q a)› ‹tF u› ‹u ∈ 𝒯 P›
            show ‹t1 @ [ev a] = u ⟹ t ∈ 𝒟 ?lhs›
              by (simp add: D_restriction_processptick T_Throw ‹t = t1 @ ev a # t2›)
                (metis Cons_eq_appendI D_imp_front_tickFree append_Nil append_assoc is_processT1_TR)
          next
            from ‹ftF v› ‹length u = n› ‹set t1 ∩ ev ` A = {}› ‹t = t1 @ ev a # t2› ‹u ∈ 𝒯 P›
            show ‹t1 = u @ v' ⟹ v = v' @ [ev a] ⟹ ftF v' ⟹ t ∈ 𝒟 ?lhs› for v'
              by (simp add: D_restriction_processptick T_Throw)
                (metis D_imp_front_tickFree Int_assoc Un_Int_eq(3) append_assoc
                  front_tickFree_append front_tickFree_nonempty_append_imp
                  inf_bot_right list.distinct(1) same_append_eq set_append ‹t ∈ 𝒟 ?rhs›)
          qed
        qed
      next
        from ‹t1 @ [ev a] ∈ 𝒯 (P ↓ n)›
        show ‹⟦t2 = u @ v; u ∈ 𝒯 (Q a); length u = n; tF u; ftF v⟧ ⟹ t ∈ 𝒟 ?lhs› for u v
        proof (elim T_restriction_processptickE)
          assume ‹t2 = u @ v› ‹u ∈ 𝒯 (Q a)› ‹length u = n› ‹tF u›
            ‹ftF v› ‹t1 @ [ev a] ∈ 𝒯 P› ‹length (t1 @ [ev a]) ≤ n›
          from ‹a ∈ A› ‹set t1 ∩ ev ` A = {}› ‹t1 @ [ev a] ∈ 𝒯 P› ‹u ∈ 𝒯 (Q a)›
          have ‹t1 @ ev a # u ∈ 𝒯 (P Θ a∈A. Q a)› by (auto simp add: T_Throw)
          moreover have ‹n < length (t1 @ ev a # u)› by (simp add: ‹length u = n›)
          ultimately have ‹t1 @ ev a # u ∈ 𝒟 ?lhs› by (simp add: D_restriction_processptickI)
          moreover have ‹t = (t1 @ ev a # u) @ v› by (simp add: ‹t = t1 @ ev a # t2› ‹t2 = u @ v›)
          moreover from ‹t1 @ [ev a] ∈ 𝒯 P› ‹tF u› append_T_imp_tickFree
          have ‹tF (t1 @ ev a # u)› by auto
          ultimately show ‹t ∈ 𝒟 ?lhs› using ‹ftF v› is_processT7 by blast
        next
          fix w x assume ‹t2 = u @ v› ‹u ∈ 𝒯 (Q a)› ‹length u = n› ‹tF u› ‹ftF v›
            ‹t1 @ [ev a] = w @ x› ‹w ∈ 𝒯 P› ‹length w = n› ‹tF w› ‹ftF x›
          from ‹t1 @ [ev a] = w @ x› consider ‹t1 @ [ev a] = w›
            | x' where ‹t1 = w @ x'› ‹x = x' @ [ev a]›
            by (cases x rule: rev_cases) simp_all
          thus ‹t ∈ 𝒟 ?lhs›
          proof cases
            assume ‹t1 @ [ev a] = w›
            with ‹a ∈ A› ‹set t1 ∩ ev ` A = {}› ‹u ∈ 𝒯 (Q a)› ‹w ∈ 𝒯 P›
            have ‹t1 @ ev a # u ∈ 𝒯 (P Θ a∈A. Q a)› by (auto simp add: T_Throw)
            moreover have ‹n < length (t1 @ ev a # u)› by (simp add: ‹length u = n›)
            ultimately have ‹t1 @ ev a # u ∈ 𝒟 ?lhs› by (blast intro: D_restriction_processptickI)
            moreover have ‹t = (t1 @ ev a # u) @ v›
              by (simp add: ‹t = t1 @ ev a # t2› ‹t2 = u @ v›)
            moreover from ‹t1 @ [ev a] = w› ‹tF u› ‹tF w› have ‹tF (t1 @ ev a # u)› by auto
            ultimately show ‹t ∈ 𝒟 ?lhs› using ‹ftF v› is_processT7 by blast
          next
            fix x' assume ‹t1 = w @ x'› ‹x = x' @ [ev a]›
            from ‹set t1 ∩ ev ` A = {}› ‹t1 = w @ x'› ‹w ∈ 𝒯 P›
            have ‹w ∈ 𝒯 P ∧ set w ∩ ev ` A = {}› by auto
            hence ‹w ∈ 𝒯 (P Θ a∈A. Q a)› by (simp add: T_Throw)
            with ‹length w = n› ‹tF w› have ‹w ∈ 𝒟 ?lhs›
              by (blast intro: D_restriction_processptickI)
            moreover have ‹t = w @ x @ t2›
              by (simp add: ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] = w @ x›)
            moreover from D_imp_front_tickFree[OF ‹t ∈ 𝒟 ?rhs›] ‹t = t1 @ ev a # t2› ‹t1 = w @ x'›
              front_tickFree_nonempty_append_imp that tickFree_append_iff
            have ‹ftF (x @ t2)› by (simp add: ‹t = w @ x @ t2› front_tickFree_append_iff)
            ultimately show ‹t ∈ 𝒟 ?lhs› by (simp add: ‹tF w› is_processT7)
          qed
        qed
      qed
    qed
  qed

  thus ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
    by (meson is_processT8 le_approx2 mono_Throw restriction_processptick_approx_self)
qed



subsection ‹Non Destructiveness›

lemma Throw_non_destructive :
  ‹non_destructive (λ(P :: ('a, 'r) processptick, Q). P Θ a ∈ A. Q a)›
proof (rule order_non_destructiveI, clarify)
  fix P P' :: ‹('a, 'r) processptick› and Q Q' :: ‹'a ⇒ ('a, 'r) processptick› and n
  assume ‹(P, Q) ↓ n = (P', Q') ↓ n› ‹0 < n›
  hence ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›
    by (simp_all add: restriction_prod_def)
  show ‹P Θ a ∈ A. Q a ↓ n ⊑FD P' Θ a ∈ A. Q' a ↓ n›
  proof (rule leFD_restriction_processptickI)
    show ‹t ∈ 𝒟 (P' Θ a ∈ A. Q' a) ⟹ t ∈ 𝒟 (P Θ a ∈ A. Q a ↓ n)› for t
      by (metis (no_types, lifting) ext ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›[unfolded restriction_fun_def]
          in_mono le_ref1 mono_Throw_FD restriction_processptick_FD_self
          restriction_processptick_Throw_FD)
  next
    show ‹(s, X) ∈ ℱ (P' Θ a ∈ A. Q' a) ⟹ (s, X) ∈ ℱ (P Θ a ∈ A. Q a ↓ n)› for s X
      by (metis (no_types, lifting) ext ‹P ↓ n = P' ↓ n›
          ‹Q ↓ n = Q' ↓ n›[unfolded restriction_fun_def]
          in_mono le_ref2 mono_Throw_FD restriction_processptick_FD_self
          restriction_processptick_Throw_FD)
  qed
qed



lemma ThrowR_constructive_if_disjoint_initials :
  ‹constructive (λQ :: 'a ⇒ ('a, 'r) processptick. P Θ a ∈ A. Q a)›
  if ‹A ∩ {e. ev e ∈ P0} = {}›
proof (rule order_constructiveI)
  fix Q Q' :: ‹'a ⇒ ('a, 'r) processptick› and n assume ‹Q ↓ n = Q' ↓ n›

  { let ?lhs = ‹Throw P A Q ↓ Suc n›
    fix t u v
    assume ‹t = u @ v› ‹u ∈ 𝒯 (Throw P A Q')› ‹length u = Suc n› ‹tF u› ‹ftF v›
    from ‹u ∈ 𝒯 (Throw P A Q')› consider ‹u ∈ 𝒯 P› ‹set u ∩ ev ` A = {}›
      | (divL) t1 t2 where ‹u = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1›
        ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | (traces) t1 a t2 where ‹u = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q' a)›
      unfolding T_Throw by blast
    hence ‹u ∈ 𝒟 ?lhs›
    proof cases
      assume ‹u ∈ 𝒯 P› ‹set u ∩ ev ` A = {}›
      hence ‹u ∈ 𝒯 (Throw P A Q)› by (simp add: T_Throw)
      with ‹length u = Suc n› ‹tF u› show ‹u ∈ 𝒟 ?lhs›
        by (simp add: D_restriction_processptickI)
    next
      case divL
      hence ‹u ∈ 𝒟 (Throw P A Q)› by (auto simp add: D_Throw)
      thus ‹u ∈ 𝒟 ?lhs› by (simp add: D_restriction_processptickI)
    next
      case traces
      from ‹length u = Suc n› traces(1) have ‹length t2 ≤ n› by simp
      with ‹t2 ∈ 𝒯 (Q' a)› ‹Q ↓ n = Q' ↓ n› have ‹t2 ∈ 𝒯 (Q a)›
        by (metis T_restriction_processptickI restriction_fun_def
            length_le_in_T_restriction_processptick)
      with traces(1-4) have ‹u ∈ 𝒯 (Throw P A Q)› by (auto simp add: T_Throw)
      thus ‹u ∈ 𝒟 ?lhs›
        by (simp add: D_restriction_processptickI ‹length u = Suc n› ‹tF u›)
    qed
    hence ‹t ∈ 𝒟 ?lhs› by (simp add: ‹ftF v› ‹t = u @ v› ‹tF u› is_processT7)
  } note * = this

  show ‹(P Θ a ∈ A. Q a) ↓ Suc n ⊑FD P Θ a ∈ A. Q' a ↓ Suc n› (is ‹?lhs ⊑FD ?rhs›)
  proof (unfold refine_defs, safe)
    show div : ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    proof (elim D_restriction_processptickE)
      assume ‹t ∈ 𝒟 (P Θ a ∈ A. Q' a)› ‹length t ≤ Suc n›
      from this(1) consider (divL) t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒟 P›
        ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | (divR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q' a)›
        unfolding D_Throw by blast
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        case divL
        hence ‹t ∈ 𝒟 (P Θ a ∈ A. Q a)› by (auto simp add: D_Throw)
        thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_processptickI)
      next
        case divR
        from divR(2,4) that have ‹t1 ≠ []›
          by (cases t1) (auto intro: initials_memI)
        with divR(1) ‹length t ≤ Suc n› nat_less_le have ‹length t2 < n› by force
        with ‹t2 ∈ 𝒟 (Q' a)› ‹Q ↓ n = Q' ↓ n› have ‹t2 ∈ 𝒟 (Q a)›
          by (metis D_restriction_processptickI restriction_fun_def
              length_less_in_D_restriction_processptick)
        with divR(1-4) have ‹t ∈ 𝒟 (Throw P A Q)› by (auto simp add: D_Throw)
        thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_processptickI)
      qed
    next
      show ‹t = u @ v ⟹ u ∈ 𝒯 (Throw P A Q') ⟹ length u = Suc n ⟹
            tF u ⟹ ftF v ⟹ t ∈ 𝒟 ?lhs› for u v by (fact "*")
    qed

    show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
    proof (elim F_restriction_processptickE)
      assume ‹(t, X) ∈ ℱ (Throw P A Q')› ‹length t ≤ Suc n›
      from this(1) consider ‹t ∈ 𝒟 (Throw P A Q')› | ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` A = {}›
        | (failR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
          ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ ℱ (Q' a)›
        unfolding Throw_projs by auto
      thus ‹(t, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹t ∈ 𝒟 (Throw P A Q')›
        hence ‹t ∈ 𝒟 ?rhs› by (simp add: D_restriction_processptickI)
        with D_F div show ‹(t, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` A = {}›
        hence ‹(t, X) ∈ ℱ (Throw P A Q)› by (simp add: F_Throw)
        thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_processptickI)
      next
        case failR
        from failR(2, 4) that have ‹t1 ≠ []›
          by (cases t1) (auto intro: initials_memI)
        with failR(1) ‹length t ≤ Suc n› nat_less_le have ‹length t2 < n› by force
        with ‹(t2, X) ∈ ℱ (Q' a)› ‹Q ↓ n = Q' ↓ n› have ‹(t2, X) ∈ ℱ (Q a)›
          by (metis F_restriction_processptickI restriction_fun_def
              length_less_in_F_restriction_processptick)
        with failR(1-4) have ‹(t, X) ∈ ℱ (Throw P A Q)› by (auto simp add: F_Throw)
        thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_processptickI)
      qed
    next
      show ‹t = u @ v ⟹ u ∈ 𝒯 (Throw P A Q') ⟹ length u = Suc n ⟹
            tF u ⟹ ftF v ⟹ (t, X) ∈ ℱ ?lhs› for u v
        by (simp add: "*" is_processT8)
    qed
  qed
qed


(*<*)
end
  (*>*)