Theory Finite_Ticks

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

chapter ‹Finite Ticks Predicate›


(*<*)
theory Finite_Ticks
  imports "HOL-CSPM"
begin
  (*>*)



section ‹Definitions›

text ‹Due to our generalization, the generalized sequential composition
      will require this additional assumption for continuity.
      Intuitively, having an infinite number of possible terminations after
      a given trace will lead to a infinite branching preventing continuity,
      to a certain extent like what happens with global non deterministic choice.›


definition finite_all_ticks :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ bool›
  where ‹finite_all_ticks P ≡ ∀t ∈ 𝒯 P. finite {r. t @ [✓(r)] ∈ 𝒯 P}›

lemma finite_all_ticksI : ‹(⋀t. t ∈ 𝒯 P ⟹ finite {r. t @ [✓(r)] ∈ 𝒯 P}) ⟹ finite_all_ticks P›
  by (simp add: finite_all_ticks_def)

lemma finite_all_ticksD : ‹finite_all_ticks P ⟹ finite {r. t @ [✓(r)] ∈ 𝒯 P}›
  by (simp add: finite_all_ticks_def)
    (meson is_processT3_TR_append not_finite_existsD)


text ‹Actually, when a \<^const>‹tick› only appears in divergences, it will not matter
      for continuity. We therefore introduce the modified predicate, which is much more useful.›

definition finite_ticks :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ bool› (‹𝔽⇩✓'(_')›)
  where ‹𝔽⇩✓(P) ≡ ∀t ∈ 𝒯 P. finite {r. t @ [✓(r)] ∈ 𝒯 P - 𝒟 P}›

lemma finite_ticksI :
  ‹(⋀t. t ∈ 𝒯 P ⟹ t ∉ 𝒟 P ⟹ finite {r. t @ [✓(r)] ∈ 𝒯 P}) ⟹ 𝔽⇩✓(P)›
  by (simp add: finite_ticks_def)
    (metis (mono_tags, lifting) Collect_cong append_T_imp_tickFree front_tickFree_Cons_iff
      is_processT7 is_processT9 not_Cons_self2 not_finite_existsD)

lemma finite_ticksD :
  ‹𝔽⇩✓(P) ⟹ t ∉ 𝒟 P ⟹ finite {r. t @ [✓(r)] ∈ 𝒯 P}›
  by (simp add: finite_ticks_def)
    (metis (lifting) Collect_cong is_processT3_TR_append
      is_processT9 not_finite_existsD)


lemma finite_all_ticks_imp_finite_ticks [simp] : ‹finite_all_ticks P ⟹ 𝔽⇩✓(P)›
  by (simp add: finite_all_ticksD finite_ticksI)

lemma finite_all_ticks_is_finite_ticks_or_finite_UNIV :
  ‹finite_all_ticks P ⟷ (if 𝒟 P = {} then 𝔽⇩✓(P) else finite (UNIV :: 'r set))›
  ―‹This is justifying why \<^const>‹finite_all_ticks› is not really interesting.›
  for P :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof (rule iffI)
  show ‹if 𝒟 P = {} then 𝔽⇩✓(P) else finite (UNIV :: 'r set)›
    if ‹finite_all_ticks P›
  proof (split if_split, intro conjI impI)
    from ‹finite_all_ticks P› show ‹𝒟 P = {} ⟹ 𝔽⇩✓(P)›
      by (simp add: finite_ticksI finite_all_ticksD)
  next
    assume ‹𝒟 P ≠ {}›
    with nonempty_divE obtain t where ‹tF t› ‹t ∈ 𝒟 P› by blast
    hence ‹t @ [✓(r)] ∈ 𝒟 P› for r by (simp add: is_processT7)
    with ‹finite_all_ticks P› show ‹finite (UNIV :: 'r set)›
      by (metis (mono_tags, lifting) Collect_cong D_T UNIV_I ‹t ∈ 𝒟 P›
          finite_all_ticks_def mem_Collect_eq top_set_def)
  qed
next
  show ‹if 𝒟 P = {} then 𝔽⇩✓(P) else finite (UNIV :: 'r set) ⟹ finite_all_ticks P›
    by (simp add: finite_ticksD finite_all_ticks_def split: if_split_asm)
      (meson rev_finite_subset subset_UNIV)
qed



text ‹We also introduce the concept that a function can preserve \<^const>‹finite_ticks›.
      Unfortunately, we will not succeed in proving continuity under this condition
      for generalized sequential composition.›

definition finite_ticks_fun :: ‹(('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ ('b, 's) process⇩p⇩t⇩i⇩c⇩k) ⇒ bool› (‹𝔽⇩✓⇩⇒'(_')›)
  where ‹𝔽⇩✓⇩⇒(f) ≡ ∀P. 𝔽⇩✓(P) ⟶ 𝔽⇩✓(f P)›

lemma finite_ticks_funI: ‹(⋀P. 𝔽⇩✓(P) ⟹ 𝔽⇩✓(f P)) ⟹ 𝔽⇩✓⇩⇒(f)›
  by (simp add: finite_ticks_fun_def)

lemma finite_ticks_funD: ‹𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓(P) ⟹ 𝔽⇩✓(f P)›
  by (simp add: finite_ticks_fun_def)



section ‹Properties›

named_theorems finite_ticks_simps
named_theorems finite_ticks_fun_simps

subsection ‹Constant Processes›

lemma finite_ticks_BOT [finite_ticks_simps] : ‹𝔽⇩✓(⊥)›
  by (simp add: finite_ticks_def BOT_projs)

lemma finite_ticks_fun_BOT [finite_ticks_fun_simps] : ‹𝔽⇩✓⇩⇒(⊥)›
  by (simp add: finite_ticks_fun_def finite_ticks_BOT)

lemma finite_ticks_SKIP [finite_ticks_simps] : ‹𝔽⇩✓(SKIP r)›
  by (simp add: finite_ticks_def SKIP_projs)

lemma finite_ticks_STOP [finite_ticks_simps] : ‹𝔽⇩✓(STOP)›
  by (simp add: finite_ticks_def T_STOP)

lemma finite_ticks_SKIPS_iff [finite_ticks_simps] : ‹𝔽⇩✓(SKIPS R) ⟷ finite R›
  by (auto simp add: finite_ticks_def SKIPS_projs)


subsection ‹Other properties›

lemma finite_strict_ticks_of_imp_finite_ticks [finite_ticks_simps] :
  ‹finite ❙✓❙s(P) ⟹ 𝔽⇩✓(P)›
  by (metis (mono_tags, lifting) finite_subset finite_ticksI
      is_processT9 mem_Collect_eq strict_ticks_of_memI subsetI)

lemma finite_strict_ticks_of_image_imp_finite_ticks_fun [finite_ticks_fun_simps] :
  ‹(⋀x. finite ❙✓❙s(f x)) ⟹ 𝔽⇩✓⇩⇒(f)›
  by (simp add: finite_strict_ticks_of_imp_finite_ticks finite_ticks_funI)


lemma anti_mono_finite_ticks [finite_ticks_simps] :
  ‹𝔽⇩✓(P)› if ‹P ⊑ Q› ‹𝔽⇩✓(Q)›
proof (rule finite_ticksI)
  fix t assume ‹t ∈ 𝒯 P› ‹t ∉ 𝒟 P›
  have ‹{r. t @ [✓(r)] ∈ 𝒯 P} = {r. t @ [✓(r)] ∈ 𝒯 Q}›
    by (meson ‹t ∉ 𝒟 P› is_processT9 le_approx2T ‹P ⊑ Q›)
  also have ‹finite …›
  proof (rule ‹𝔽⇩✓(Q)›[THEN finite_ticksD])
    from ‹t ∉ 𝒟 P› le_approx1 ‹P ⊑ Q› show ‹t ∉ 𝒟 (Q)› by blast
  qed
  finally show ‹finite {r. t @ [✓(r)] ∈ 𝒯 P}› .
qed

lemma anti_mono_finite_ticks_fun [finite_ticks_fun_simps] :
  ‹f ⊑ g ⟹ 𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(f)›
  by (metis anti_mono_finite_ticks finite_ticks_fun_def fun_below_iff)


lemma finite_ticks_LUB_iff [finite_ticks_fun_simps] :
  ‹𝔽⇩✓(⨆i. Y i) ⟷ (∀i. 𝔽⇩✓(Y i))› if ‹chain Y›
proof safe
  from anti_mono_finite_ticks is_ub_thelub ‹chain Y›
  show ‹𝔽⇩✓(⨆i. Y i) ⟹ 𝔽⇩✓(Y i)› for i by blast
next
  show ‹𝔽⇩✓(⨆i. Y i)› if ‹∀i. 𝔽⇩✓(Y i)›
  proof (rule finite_ticksI)
    fix t assume ‹t ∈ 𝒯 (⨆i. Y i)› ‹t ∉ 𝒟 (⨆i. Y i)›
    from ‹t ∉ 𝒟 (⨆i. Y i)› obtain j where ‹t ∉ 𝒟 (Y j)›
      by (metis D_LUB_2 ‹chain Y› limproc_is_thelub)
    have ‹{r. t @ [✓(r)] ∈ 𝒯 (⨆i. Y i)} = {r. t @ [✓(r)] ∈ 𝒯 (Y j)}›
      by (meson ‹chain Y› ‹t ∉ 𝒟 (Y j)› is_processT9 is_ub_thelub le_approx2T)
    also have ‹finite …›
      by (fact ‹∀i. 𝔽⇩✓(Y i)›[THEN spec, THEN finite_ticksD, OF ‹t ∉ 𝒟 (Y j)›])
    finally show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (⨆i. Y i)}› .
  qed
qed


lemma adm_finite_ticks [finite_ticks_simps] : ‹adm (λP. 𝔽⇩✓(P))›
  by (rule admI) (simp add: finite_ticks_LUB_iff)

lemma finite_ticks_fix [finite_ticks_simps] :
  ‹𝔽⇩✓(μ X. f X)› if ‹cont f› and ‹𝔽⇩✓⇩⇒(f)›
proof (induct rule: fix_ind)
  show ‹adm finite_ticks› by (fact adm_finite_ticks)
next
  show ‹𝔽⇩✓(⊥)› by (fact finite_ticks_BOT)
next
  show ‹𝔽⇩✓((Λ X. f X)⋅X)› if ‹𝔽⇩✓(X)› for X
    by (simp add: ‹cont f›) (fact finite_ticks_funD[OF ‹𝔽⇩✓⇩⇒(f)› ‹𝔽⇩✓(X)›])
qed



lemma adm_finite_ticks_fun [finite_ticks_fun_simps] : ‹adm (λf. 𝔽⇩✓⇩⇒(f))›
  by (simp add: admI ch2ch_fun finite_ticks_LUB_iff finite_ticks_fun_def lub_fun)

lemma finite_ticks_fun_fix [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(μ X. f X)› if ‹cont f› and ‹⋀x. 𝔽⇩✓⇩⇒(x) ⟹ 𝔽⇩✓⇩⇒(f x)›
proof (induct f rule: cont_fix_ind)
  from ‹cont f› show ‹cont f› .
next
  from adm_finite_ticks_fun show ‹adm (λf. 𝔽⇩✓⇩⇒(f))› .
next
  from finite_ticks_fun_BOT show ‹𝔽⇩✓⇩⇒(⊥)› .
next
  from ‹⋀y. 𝔽⇩✓⇩⇒(y) ⟹ 𝔽⇩✓⇩⇒(f y)› show ‹𝔽⇩✓⇩⇒(x) ⟹ 𝔽⇩✓⇩⇒(f x)› for x .
qed


lemma finite_ticks_fun_id [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(id)› ‹𝔽⇩✓⇩⇒(λx. x)›
  by (simp_all add: finite_ticks_funI)

lemma finite_ticks_fun_const_iff [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(λx. P) ⟷ 𝔽⇩✓(P)›
  by (meson finite_ticks_STOP finite_ticks_fun_def)

lemma finite_ticks_fun_comp [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓⇩⇒(λx. g (f x))›
  by (simp add: finite_ticks_fun_def)



section ‹Laws›

subsection ‹Laws of \<^term>‹𝔽⇩✓(P)››

lemma finite_ticks_Ndet [finite_ticks_simps] :
  ‹𝔽⇩✓(P ⊓ Q)› if ‹𝔽⇩✓(P)› ‹𝔽⇩✓(Q)›
proof (rule finite_ticksI)
  fix t assume ‹t ∈ 𝒯 (P ⊓ Q)› ‹t ∉ 𝒟 (P ⊓ Q)›
  from ‹t ∈ 𝒯 (P ⊓ Q)›
  have ‹t ∈ 𝒯 P ∧ t ∈ 𝒯 Q ∨ t ∈ 𝒯 P ∧ (∀r. t @ [✓(r)] ∉ 𝒯 Q) ∨ (∀r. t @ [✓(r)] ∉ 𝒯 P) ∧ t ∈ 𝒯 Q›
    unfolding T_Ndet by (metis Un_iff is_processT3_TR_append)
  with ‹𝔽⇩✓(P)› ‹𝔽⇩✓(Q)› ‹t ∉ 𝒟 (P ⊓ Q)› show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (P ⊓ Q)}›
    by (auto simp add: Ndet_projs dest: finite_ticksD)
qed


lemma finite_ticks_Det [finite_ticks_simps] :
  ‹𝔽⇩✓(P □ Q)› if ‹𝔽⇩✓(P)› ‹𝔽⇩✓(Q)›
proof -
  have ‹𝔽⇩✓(P □ Q) = 𝔽⇩✓(P ⊓ Q)› by (simp add: finite_ticks_def Det_projs Ndet_projs)
  with ‹𝔽⇩✓(P)› ‹𝔽⇩✓(Q)› show ‹𝔽⇩✓(P □ Q)› by (simp add: finite_ticks_Ndet)
qed


lemma finite_ticks_Sliding [finite_ticks_simps] :
  ‹𝔽⇩✓(P) ⟹ 𝔽⇩✓(Q) ⟹ 𝔽⇩✓(P ⊳ Q)›
  by (simp add: Sliding_def finite_ticks_Ndet finite_ticks_Det)


lemma finite_ticks_Interrupt [finite_ticks_simps] :
  ‹𝔽⇩✓(P △ Q)› if ‹𝔽⇩✓(P)› ‹𝔽⇩✓(Q)›
proof (cases ‹Q = ⊥›)
  show ‹Q = ⊥ ⟹ 𝔽⇩✓(P △ Q)› by (simp add: finite_ticks_BOT)
next
  show ‹𝔽⇩✓(P △ Q)› if ‹Q ≠ ⊥›
  proof (rule finite_ticksI)
    fix t assume ‹t ∈ 𝒯 (P △ Q)› ‹t ∉ 𝒟 (P △ Q)›
    have ‹{r. t @ [✓(r)] ∈ 𝒯 (P △ Q)} ⊆
          {r. t @ [✓(r)] ∈ 𝒯 P} ∪
          (⋃u ∈ {u. ∃v. t = u @ v ∧ u ∈ 𝒯 P}. {r. drop (length u) t @ [✓(r)] ∈ 𝒯 Q})›
      by (simp add: subset_iff T_Interrupt)
        (metis Prefix_Order.prefix_length_le Prefix_Order.same_prefix_nil
          append_eq_append_conv_if append_eq_first_pref_spec butlast_append butlast_snoc)
    moreover have ‹finite …›
    proof (rule finite_UnI)
      from D_Interrupt ‹t ∉ 𝒟 (P △ Q)› have ‹t ∉ 𝒟 P› by blast
      thus ‹finite {r. t @ [✓(r)] ∈ 𝒯 P}› by (simp add: finite_ticksD ‹𝔽⇩✓(P)›)
    next
      show ‹finite (⋃u∈{u. ∃v. t = u @ v ∧ u ∈ 𝒯 P}. {r. drop (length u) t @ [✓(r)] ∈ 𝒯 Q})›
      proof (rule finite_UN_I)
        show ‹finite {u. ∃v. t = u @ v ∧ u ∈ 𝒯 P}› by (prove_finite_subset_of_prefixes t)
      next
        fix u assume ‹u ∈ {u. ∃v. t = u @ v ∧ u ∈ 𝒯 P}›
        then obtain v where ‹u ∈ 𝒯 P› ‹t = u @ v› by blast
        with ‹t ∈ 𝒯 (P △ Q)› append_T_imp_tickFree consider ‹tF u› | ‹v = []› by blast
        thus ‹finite {r. drop (length u) t @ [✓(r)] ∈ 𝒯 Q}›
        proof cases
          assume ‹tF u›
          with ‹u ∈ 𝒯 P› ‹t ∉ 𝒟 (P △ Q)› have ‹v ∉ 𝒟 Q›
            by (simp add: D_Interrupt ‹t = u @ v›)
          thus ‹tF u ⟹ finite {r. drop (length u) t @ [✓(r)] ∈ 𝒯 Q}›
            by (simp add: ‹t = u @ v› finite_ticksD ‹𝔽⇩✓(Q)›)
        next
          from BOT_iff_Nil_D ‹Q ≠ ⊥› have ‹[] ∉ 𝒟 Q› by blast
          with ‹𝔽⇩✓(Q)› finite_ticksD have ‹finite {r. [✓(r)] ∈ 𝒯 Q}› by force
          thus ‹v = [] ⟹ finite {r. drop (length u) t @ [✓(r)] ∈ 𝒯 Q}›
            by (simp add: ‹t = u @ v›)
        qed
      qed
    qed
    ultimately show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (P △ Q)}› by (fact finite_subset)
  qed
qed


lemma finite_ticks_Throw [finite_ticks_simps] :
  ‹𝔽⇩✓(P Θ a∈A. Q a)› if ‹𝔽⇩✓(P)› ‹⋀a. a ∈ A ⟹ 𝔽⇩✓(Q a)›
proof (rule finite_ticksI)
  fix t assume ‹t ∈ 𝒯 (P Θ a∈A. Q a)› ‹t ∉ 𝒟 (P Θ a∈A. Q a)›
  then consider ‹t ∈ 𝒯 P› ‹set t ∩ ev ` A = {}›
    | t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
      ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q a)›
    unfolding Throw_projs by blast
  thus ‹finite {r. t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)}›
  proof cases
    assume ‹t ∈ 𝒯 P› ‹set t ∩ ev ` A = {}›
    hence ‹{r. t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)} ⊆ {r. t @ [✓(r)] ∈ 𝒯 P}›
      by (auto simp add: T_Throw D_T is_processT7 disjoint_iff image_iff)
        (metis (no_types) butlast.simps(2) butlast_append butlast_snoc in_set_conv_decomp)
    moreover have ‹finite …›
    proof (rule ‹𝔽⇩✓(P)›[THEN finite_ticksD])
      from ‹set t ∩ ev ` A = {}›
      have ‹t ∈ 𝒟 P ⟹ (if tF t then t else butlast t) ∈ 𝒟 (P Θ a∈A. Q a)›
        by (cases t rule: rev_cases, simp_all add: D_Throw)
          (metis D_imp_front_tickFree ‹set t ∩ ev ` A = {}› append.right_neutral butlast_snoc
            div_butlast_when_non_tickFree_iff front_tickFree_Nil front_tickFree_nonempty_append_imp
            not_Cons_self2 not_is_ev tickFree_Cons_iff tickFree_append_iff)
      with ‹t ∉ 𝒟 (P Θ a∈A. Q a)› D_imp_front_tickFree div_butlast_when_non_tickFree_iff
      show ‹t ∉ 𝒟 P› by blast
    qed
    ultimately show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)}› by (fact finite_subset)
  next
    fix t1 a t2 assume * : ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
      ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q a)›
    from ‹t ∉ 𝒟 (P Θ a∈A. Q a)›
    have ‹t ∉ {t1 @ t2 |t1 t2. t1 ∈ 𝒟 P ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF t2}›
      by (simp add: D_Throw UnI1)

    with "*" have ‹{r. t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)} = {r. t2 @ [✓(r)] ∈ 𝒯 (Q a)}›
      by (simp add: T_Throw, safe)
        (metis Cons_eq_appendI append_assoc butlast_snoc front_tickFree_charn
          non_tickFree_tick tickFree_Nil tickFree_append_iff tickFree_imp_front_tickFree,
          solves ‹simp add: Throw_T_third_clause_breaker›, metis)
    also have ‹finite …›
    proof (rule ‹⋀a. a ∈ A ⟹ 𝔽⇩✓(Q a)›[THEN finite_ticksD, OF ‹a ∈ A›])
      from ‹t ∉ 𝒟 (P Θ a∈A. Q a)› ‹t1 @ [ev a] ∈ 𝒯 P› ‹set t1 ∩ ev ` A = {}›
      show ‹t2 ∉ 𝒟 (Q a)› by (auto simp add: D_Throw ‹t = t1 @ ev a # t2› ‹a ∈ A›)
    qed
    finally show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)}› .
  qed
qed


lemma finite_ticks_Renaming [finite_ticks_simps] :
  ‹𝔽⇩✓(Renaming P f g)› if ‹finitary f› ‹finitary g› ‹𝔽⇩✓(P)›
proof (rule finite_ticksI)
  fix t assume ‹t ∉ 𝒟 (Renaming P f g)›
  hence ‹{s. t @ [✓(s)] ∈ 𝒯 (Renaming P f g)} ⊆
         (⋃u∈{u. t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u ∧ u ∈ 𝒯 P}. {g r |r. u @ [✓(r)] ∈ 𝒯 P})›
    by (auto simp add: subset_iff Renaming_projs append_eq_map_conv tick_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff)
      (use is_processT3_TR_append in blast,
        metis append_Nil butlast_append event⇩p⇩t⇩i⇩c⇩k.disc(2) front_tickFree_iff_tickFree_butlast
        map_event⇩p⇩t⇩i⇩c⇩k_tickFree snoc_eq_iff_butlast tickFree_butlast)
  moreover have ‹finite …›
  proof (rule finite_UN_I)
    have ‹finitary (map_event⇩p⇩t⇩i⇩c⇩k f g)› by (simp add: Cont_RenH2 ‹finitary f› ‹finitary g›)
    have ‹{u. t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u ∧ u ∈ 𝒯 P} ⊆ {u. t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u}› by blast
    moreover from Cont_RenH4 ‹finitary (map_event⇩p⇩t⇩i⇩c⇩k f g)› have ‹finite …› by blast
    ultimately show ‹finite {u. t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u ∧ u ∈ 𝒯 P}› by (fact finite_subset)
  next
    fix u assume ‹u ∈ {u. t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u ∧ u ∈ 𝒯 P}›
    hence ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹u ∈ 𝒯 P› by simp_all
    with ‹t ∉ 𝒟 (Renaming P f g)› have ‹u ∉ 𝒟 P›
      by (simp add: D_Renaming)
        (metis (no_types, opaque_lifting) D_imp_front_tickFree append_Nil append_Nil2
          div_butlast_when_non_tickFree_iff front_tickFree_charn map_butlast
          map_event⇩p⇩t⇩i⇩c⇩k_tickFree snoc_eq_iff_butlast tickFree_Nil)
    thus ‹finite {g r |r. u @ [✓(r)] ∈ 𝒯 P}›
      by (simp add: finite_ticksD ‹𝔽⇩✓(P)›)
  qed
  ultimately show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (Renaming P f g)}› by (fact finite_subset)
qed


lemma finite_ticks_Seq [finite_ticks_simps] :
  ‹𝔽⇩✓(P ❙; Q)› if ‹𝔽⇩✓(Q)›
proof (cases ‹Q = ⊥›)
  from not_finite_existsD show ‹Q = ⊥ ⟹ 𝔽⇩✓(P ❙; Q)›
    by (auto simp add: finite_ticks_def Seq_projs BOT_projs)
next
  show ‹𝔽⇩✓(P ❙; Q)› if ‹Q ≠ ⊥›
  proof (rule finite_ticksI)
    fix t assume ‹t ∉ 𝒟 (P ❙; Q)›
    hence ‹{r. t @ [✓(r)] ∈ 𝒯 (P ❙; Q)} ⊆
           (⋃u ∈ {u. ∃v r. t = u @ v ∧ u @ [✓(r)] ∈ 𝒯 P}. {r. drop (length u) t @ [✓(r)] ∈ 𝒯 Q})›
      by (auto simp add: Seq_projs intro: is_processT9)
        (metis (no_types, opaque_lifting) T_imp_front_tickFree append_butlast_last_id
          append_eq_conv_conj butlast_append butlast_snoc front_tickFree_nonempty_append_imp
          last_appendR list.distinct(1) non_tickFree_tick tickFree_append_iff)
    moreover have ‹finite …›
    proof (rule finite_UN_I)
      show ‹finite {u. ∃v r. t = u @ v ∧ u @ [✓(r)] ∈ 𝒯 P}›
        by (prove_finite_subset_of_prefixes t)
    next
      fix u assume ‹u ∈ {u. ∃v r. t = u @ v ∧ u @ [✓(r)] ∈ 𝒯 P}›
      then obtain v r where ‹u @ [✓(r)] ∈ 𝒯 P› ‹t = u @ v› by blast
      with append_T_imp_tickFree consider ‹tF u› | ‹v = []› by blast
      thus ‹finite {r. drop (length u) t @ [✓(r)] ∈ 𝒯 Q}›
      proof cases
        assume ‹tF u›
        with ‹u @ [✓(r)] ∈ 𝒯 P› ‹t ∉ 𝒟 (P ❙; Q)› have ‹v ∉ 𝒟 Q›
          by (auto simp add: D_Seq ‹t = u @ v›)
        thus ‹tF u ⟹ finite {r. drop (length u) t @ [✓(r)] ∈ 𝒯 Q}›
          by (simp add: ‹t = u @ v› finite_ticksD ‹𝔽⇩✓(Q)›)
      next
        from BOT_iff_Nil_D ‹Q ≠ ⊥› have ‹[] ∉ 𝒟 Q› by blast
        with ‹𝔽⇩✓(Q)› finite_ticksD have ‹finite {r. [✓(r)] ∈ 𝒯 Q}› by force
        thus ‹v = [] ⟹ finite {r. drop (length u) t @ [✓(r)] ∈ 𝒯 Q}›
          by (simp add: ‹t = u @ v›)
      qed
    qed
    ultimately show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (P ❙; Q)}› by (fact finite_subset)
  qed
qed



lemma finite_ticks_Sync [finite_ticks_simps] :
  ‹𝔽⇩✓(P ⟦S⟧ Q)› if ‹𝔽⇩✓(P) ∨ 𝔽⇩✓(Q)›
proof (rule finite_ticksI)
  fix t assume ‹t ∉ 𝒟 (P ⟦S⟧ Q)›
  have ‹{r. t @ [✓(r)] ∈ 𝒯 (P ⟦S⟧ Q)} ⊆
        (⋃(t_P, t_Q)∈{(t_P, t_Q). t setinterleaves ((t_P, t_Q), range tick ∪ ev ` S)}.
                      {r. t_P @ [✓(r)] ∈ 𝒯 P ∧ t_P ∉ 𝒟 P ∧ t_Q @ [✓(r)] ∈ 𝒯 Q ∧ t_Q ∉ 𝒟 Q})›
    (is ‹_ ⊆ ?rhs›)
  proof (rule subsetI)
    fix r assume ‹r ∈ {r. t @ [✓(r)] ∈ 𝒯 (P ⟦S⟧ Q)}›
    hence ‹t @ [✓(r)] ∈ 𝒯 (P ⟦S⟧ Q)› ..
    moreover from ‹t ∉ 𝒟 (P ⟦S⟧ Q)› have ‹t @ [✓(r)] ∉ 𝒟 (P ⟦S⟧ Q)›
      by (meson is_processT9)
    ultimately obtain t_P t_Q where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› ‹t_P ∉ 𝒟 P› ‹t_Q ∉ 𝒟 Q›
      ‹(t @ [✓(r)]) setinterleaves ((t_P, t_Q), range tick ∪ ev ` S)›
      by (simp add: Sync_projs)
        (metis (no_types, lifting) append.right_neutral front_tickFree_Nil setinterleaving_sym)
    from this(1-4) SyncWithTick_imp_NTF[OF this(5)] show ‹r ∈ ?rhs›
      by simp (metis T_imp_front_tickFree front_tickFree_append_iff is_processT7 not_Cons_self2)
  qed
  moreover have ‹finite …›
  proof (rule finite_UN_I, safe)
    show ‹finite {(t_P, t_Q). t setinterleaves ((t_P, t_Q), range tick ∪ ev ` S)}›
      by (fact finite_interleaves)
  next
    from ‹𝔽⇩✓(P) ∨ 𝔽⇩✓(Q)› finite_ticksD 
    show ‹finite {r. t_P @ [✓(r)] ∈ 𝒯 P ∧ t_P ∉ 𝒟 P ∧
                     t_Q @ [✓(r)] ∈ 𝒯 Q ∧ t_Q ∉ 𝒟 Q}› for t_P t_Q by fastforce
  qed
  ultimately show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (P ⟦S⟧ Q)}› by (fact finite_subset)
qed

corollary ‹𝔽⇩✓(P) ∨ 𝔽⇩✓(Q) ⟹ 𝔽⇩✓(P ||  Q)›
  and ‹𝔽⇩✓(P) ∨ 𝔽⇩✓(Q) ⟹ 𝔽⇩✓(P ||| Q)›
  by (fact finite_ticks_Sync)+

(* 
lemma finite_ticks_Hiding [finite_ticks_simps] :
  ‹𝔽⇩✓(P \ S)› if ‹finite S› and ‹𝔽⇩✓(P)›
  ― ‹Probably complicated proof.›
  oops
 *)


lemma finite_ticks_GlobalNdet [finite_ticks_simps] :
  ‹finite A ⟹ (⋀a. a ∈ A ⟹ 𝔽⇩✓(P a)) ⟹ 𝔽⇩✓(⊓a∈A. P a)›
  ―‹We can't expect \<^term>‹infinite A› here, see @{thm finite_ticks_SKIPS_iff[no_vars]}.›
  by (induct A rule: induct_subset_empty_single)
    (simp_all add: GlobalNdet_distrib_unit finite_ticks_Ndet finite_ticks_STOP)

lemma finite_ticks_GlobalDet [finite_ticks_simps] :
  ‹finite A ⟹ (⋀a. a ∈ A ⟹ 𝔽⇩✓(P a)) ⟹ 𝔽⇩✓(□a∈A. P a)›
  by (induct A rule: finite_induct)
    (simp_all add: GlobalDet_distrib_unit_bis finite_ticks_Det finite_ticks_STOP)

lemma ‹L = [] ⟹ 𝔽⇩✓(SEQ l∈@L. P l)› by (simp add: finite_ticks_SKIP)

lemma finite_ticks_MultiSeq_nonempty [finite_ticks_simps] :
  ‹L ≠ [] ⟹ 𝔽⇩✓(P (last L)) ⟹ 𝔽⇩✓(SEQ l∈@L. P l)›
  by (induct L rule: rev_induct) (simp_all add: finite_ticks_Seq)

lemma finite_ticks_MultiSync [finite_ticks_simps] :
  ‹(⋀m. m ∈# M ⟹ 𝔽⇩✓(P m)) ⟹ 𝔽⇩✓(❙⟦S❙⟧ m∈#M. P m)›
  by (induct M rule: induct_subset_mset_empty_single)
    (simp_all add: finite_ticks_Sync finite_ticks_STOP)

corollary ‹(⋀m. m ∈# M ⟹ 𝔽⇩✓(P m)) ⟹ 𝔽⇩✓(❙|❙|  m∈#M. P m)›
  and ‹(⋀m. m ∈# M ⟹ 𝔽⇩✓(P m)) ⟹ 𝔽⇩✓(❙|❙|❙| m∈#M. P m)›
  by (fact finite_ticks_MultiSync)+


lemma finite_ticks_Mprefix_iff [finite_ticks_simps] :
  ‹𝔽⇩✓(□a∈A → P a) ⟷ (∀a∈A. 𝔽⇩✓(P a))›
proof (safe intro!: finite_ticksI)
  fix t a assume ‹𝔽⇩✓(□a∈A → P a)› ‹a ∈ A› ‹t ∈ 𝒯 (P a)› ‹t ∉ 𝒟 (P a)›
  have ‹{r. t @ [✓(r)] ∈ 𝒯 (P a)} = {r. (ev a # t) @ [✓(r)] ∈ 𝒯 (□a∈A → P a)}›
    by (auto simp add: ‹a ∈ A› T_Mprefix)
  also have ‹finite …›
    by (rule ‹𝔽⇩✓(□a∈A → P a)›[THEN finite_ticksD])
      (simp add: D_Mprefix ‹t ∉ 𝒟 (P a)›)
  finally show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (P a)}› .
next
  fix t assume ‹∀a∈A. 𝔽⇩✓(P a)› ‹t ∈ 𝒯 (□a∈A → P a)› ‹t ∉ 𝒟 (□a∈A → P a)›
  from ‹t ∈ 𝒯 (□a∈A → P a)› consider ‹t = []› | u a where ‹a ∈ A› ‹t = ev a # u›
    by (auto simp add: T_Mprefix)
  thus ‹finite {r. t @ [✓(r)] ∈ 𝒯 (□a∈A → P a)}›
  proof cases
    show ‹t = [] ⟹ finite {r. t @ [✓(r)] ∈ 𝒯 (□a∈A → P a)}› by (simp add: T_Mprefix)
  next
    fix u a assume ‹a ∈ A› ‹t = ev a # u›
    hence ‹{r. t @ [✓(r)] ∈ 𝒯 (□a∈A → P a)} = {r. u @ [✓(r)] ∈ 𝒯 (P a)}›
      by (simp add: set_eq_iff T_Mprefix)
    also have ‹finite …›
      by (rule ‹∀a∈A. 𝔽⇩✓(P a)›[THEN bspec, OF ‹a ∈ A›, THEN finite_ticksD])
        (use ‹t ∉ 𝒟 (□a∈A → P a)› in ‹simp add: ‹t = ev a # u› D_Mprefix ‹a ∈ A››)
    finally show ‹finite {r. t @ [✓(r)] ∈ 𝒯 (□a∈A → P a)}› .
  qed
qed

lemma finite_ticks_Mndetprefix_iff [finite_ticks_simps] :
  ‹𝔽⇩✓(⊓a∈A → P a) ⟷ (∀a∈A. 𝔽⇩✓(P a))›
proof -
  have ‹𝔽⇩✓(⊓a∈A → P a) ⟷ 𝔽⇩✓(□a∈A → P a)›
    by (simp add: finite_ticks_def Mndetprefix_projs Mprefix_projs)
  thus ‹𝔽⇩✓(⊓a∈A → P a) ⟷ (∀a∈A. 𝔽⇩✓(P a))› by (simp add: finite_ticks_Mprefix_iff)
qed

lemma finite_ticks_write0_iff [finite_ticks_simps] : ‹𝔽⇩✓(a → P) ⟷ 𝔽⇩✓(P)›
  by (simp add: write0_def finite_ticks_Mprefix_iff)

lemma finite_ticks_write_iff [finite_ticks_simps] : ‹𝔽⇩✓(c❙!a → P) ⟷ 𝔽⇩✓(P)›
  by (simp add: write_def finite_ticks_Mprefix_iff)

lemma finite_ticks_read_iff :
  ‹𝔽⇩✓(c❙?a∈A → P a) ⟷ (∀b∈c ` A. 𝔽⇩✓(P (inv_into A c b)))›
  by (simp add: read_def finite_ticks_Mprefix_iff)

lemma finite_ticks_inj_on_read_iff [finite_ticks_simps] :
  ‹inj_on c A ⟹ 𝔽⇩✓(c❙?a∈A → P a) ⟷ (∀a∈A. 𝔽⇩✓(P a))›
  by (simp add: read_def finite_ticks_Mprefix_iff)

lemma finite_ticks_ndet_write_iff :
  ‹𝔽⇩✓(c❙!❙!a∈A → P a) ⟷ (∀b∈c ` A. 𝔽⇩✓(P (inv_into A c b)))›
  by (simp add: ndet_write_def finite_ticks_Mndetprefix_iff)

lemma finite_ticks_inj_on_ndet_write_iff [finite_ticks_simps] :
  ‹inj_on c A ⟹ 𝔽⇩✓(c❙!❙!a∈A → P a) ⟷ (∀a∈A. 𝔽⇩✓(P a))›
  by (simp add: ndet_write_def finite_ticks_Mndetprefix_iff)



subsection ‹Laws of \<^term>‹𝔽⇩✓⇩⇒(f)››

lemma finite_ticks_fun_Det [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(λx. f x □ g x)›
  by (simp add: finite_ticks_Det finite_ticks_fun_def)

lemma finite_ticks_fun_Ndet [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(λx. f x ⊓ g x)›
  by (simp add: finite_ticks_Ndet finite_ticks_fun_def)

lemma finite_ticks_fun_Sliding [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(λx. f x ⊳ g x)›
  by (simp add: finite_ticks_Sliding finite_ticks_fun_def)

lemma finite_ticks_fun_Interrupt [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(λx. f x △ g x)›
  by (simp add: finite_ticks_Interrupt finite_ticks_fun_def)

lemma finite_ticks_fun_Throw [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(f) ⟹ (⋀a. a ∈ A ⟹ 𝔽⇩✓⇩⇒(g a)) ⟹ 𝔽⇩✓⇩⇒(λx. f x Θ a∈A. g a x)›
  by (simp add: finite_ticks_Throw finite_ticks_fun_def)

lemma finite_ticks_fun_Renaming [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(P) ⟹ finitary f ⟹ finitary g ⟹ 𝔽⇩✓⇩⇒(λx. Renaming (P x) f g)›
  by (simp add: finite_ticks_Renaming finite_ticks_fun_def)

lemma finite_ticks_fun_RenamingF [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(P) ⟹ 𝔽⇩✓⇩⇒(λx. (P x) ⟦a := b⟧ ⟦c := d⟧)›
  by (simp add: finite_ticks_fun_Renaming)

lemma finite_ticks_fun_Seq [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(λx. f x ❙; g x)›
  by (simp add: finite_ticks_Seq finite_ticks_fun_def)

lemma finite_ticks_fun_Sync [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(λx. f x ⟦S⟧ g x)›
  by (simp add: finite_ticks_Sync finite_ticks_fun_def)

corollary ‹𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(λx. f x ||  g x)›
  and ‹𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓⇩⇒(g) ⟹ 𝔽⇩✓⇩⇒(λx. f x ||| g x)›
  by (fact finite_ticks_fun_Sync)+


(* lemma finite_ticks_fun_Hiding [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(f) ⟹ 𝔽⇩✓⇩⇒(λx. f x \ S)›
  by (simp add: finite_ticks_Hiding finite_ticks_fun_def)
 *)


lemma finite_ticks_fun_GlobalNdet [finite_ticks_fun_simps] :
  ‹finite A ⟹ (⋀a. a ∈ A ⟹ 𝔽⇩✓⇩⇒(f a)) ⟹ 𝔽⇩✓⇩⇒(λx. ⊓a∈A. f a x)›
  by (simp add: finite_ticks_GlobalNdet finite_ticks_fun_def)

lemma finite_ticks_fun_GlobalDet :
  ‹finite A ⟹ (⋀a. a ∈ A ⟹ 𝔽⇩✓⇩⇒(f a)) ⟹ 𝔽⇩✓⇩⇒(λx. □a∈A. f a x)›
  by (simp add: finite_ticks_GlobalDet finite_ticks_fun_def)

lemma finite_ticks_fun_MultiSeq [finite_ticks_fun_simps] :
  ‹L = [] ⟹ 𝔽⇩✓⇩⇒(λx. SEQ l∈@L. f l x)›
  ‹L ≠ [] ⟹ 𝔽⇩✓⇩⇒(f (last L)) ⟹ 𝔽⇩✓⇩⇒(λx. SEQ l∈@L. f l x)›
  by (simp_all add: finite_ticks_MultiSeq_nonempty finite_ticks_fun_def finite_ticks_SKIP)

lemma finite_ticks_fun_MultiSync [finite_ticks_fun_simps] :
  ‹(⋀m. m ∈# M ⟹ 𝔽⇩✓⇩⇒(f m)) ⟹ 𝔽⇩✓⇩⇒(λx. ❙⟦S❙⟧ m∈#M. f m x)›
  by (simp add: finite_ticks_MultiSync finite_ticks_fun_def)

corollary ‹(⋀m. m ∈# M ⟹ 𝔽⇩✓⇩⇒(f m)) ⟹ 𝔽⇩✓⇩⇒(λx. ❙|❙|  m∈#M. f m x)›
  and ‹(⋀m. m ∈# M ⟹ 𝔽⇩✓⇩⇒(f m)) ⟹ 𝔽⇩✓⇩⇒(λx. ❙|❙|❙| m∈#M. f m x)›
  by (fact finite_ticks_fun_MultiSync)+


lemma finite_ticks_fun_Mprefix_iff :
  ‹𝔽⇩✓⇩⇒(λx. □a∈A → f a x) ⟷ (∀a ∈ A. 𝔽⇩✓⇩⇒(f a))›
  by (auto simp add: finite_ticks_fun_def finite_ticks_Mprefix_iff)

lemma finite_ticks_fun_Mprefix [finite_ticks_fun_simps] :
  ‹(⋀a. a ∈ A ⟹ 𝔽⇩✓⇩⇒(f a)) ⟹ 𝔽⇩✓⇩⇒(λx. □a∈A → f a x)›
  by (simp add: finite_ticks_fun_Mprefix_iff)

lemma finite_ticks_fun_Mndetprefix_iff [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(λx. ⊓a∈A → f a x) ⟷ (∀a ∈ A. 𝔽⇩✓⇩⇒(f a))›
  by (auto simp add: finite_ticks_fun_def finite_ticks_Mndetprefix_iff)

lemma finite_ticks_fun_Mndetprefix [finite_ticks_fun_simps] :
  ‹(⋀a. a ∈ A ⟹ 𝔽⇩✓⇩⇒(f a)) ⟹ 𝔽⇩✓⇩⇒(λx. ⊓a∈A → f a x)›
  by (simp add: finite_ticks_fun_Mndetprefix_iff)

lemma finite_ticks_fun_write0_iff [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(λx. a → f x) ⟷ 𝔽⇩✓⇩⇒(f)›
  by (simp add: write0_def finite_ticks_fun_Mprefix_iff)

lemma finite_ticks_fun_write_iff [finite_ticks_fun_simps] :
  ‹𝔽⇩✓⇩⇒(λx. c❙!a → f x) ⟷ 𝔽⇩✓⇩⇒(f)›
  by (simp add: write_def finite_ticks_fun_Mprefix_iff)

lemma finite_ticks_fun_read_iff :
  ‹𝔽⇩✓⇩⇒(λx. c❙?a∈A → f a x) ⟷ (∀b∈c ` A. 𝔽⇩✓⇩⇒(f (inv_into A c b)))›
  by (simp add: read_def finite_ticks_fun_Mprefix_iff)

lemma finite_ticks_fun_read [finite_ticks_fun_simps] :
  ‹(⋀a. a ∈ A ⟹ 𝔽⇩✓⇩⇒(λx. f a x)) ⟹ 𝔽⇩✓⇩⇒(λx. c❙?a∈A → f a x)›
  by (simp add: read_def o_def inv_into_into finite_ticks_fun_Mprefix_iff)

lemma finite_ticks_fun_ndet_write_iff :
  ‹𝔽⇩✓⇩⇒(λx. c❙!❙!a∈A → f a x) ⟷ (∀b∈c ` A. 𝔽⇩✓⇩⇒(f (inv_into A c b)))›
  by (simp add: ndet_write_def finite_ticks_fun_Mndetprefix_iff)

lemma finite_ticks_fun_ndet_write [finite_ticks_fun_simps] :
  ‹(⋀a. a ∈ A ⟹ 𝔽⇩✓⇩⇒(λx. f a x)) ⟹ 𝔽⇩✓⇩⇒(λx. c❙!❙!a∈A → f a x)›
  by (simp add: ndet_write_def o_def inv_into_into finite_ticks_fun_Mndetprefix_iff)



(*<*)
end
  (*>*)