Theory Process_Restriction_Space

(***********************************************************************************
 * 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 ‹Depth Operator›

(*<*)
theory Process_Restriction_Space
  imports "Restriction_Spaces-HOLCF" "HOL-CSP.Basic_CSP_Laws"
begin
  (*>*)

subsection ‹Definition›

instantiation processptick :: (type, type) order_restriction_space
begin

lift_definition restriction_processptick ::
  ‹[('a, 'r) processptick, nat] ⇒ ('a, 'r) processptick›
  is ‹λP n. (ℱ P ∪ {(t @ u, X) |t u X. t ∈ 𝒯 P ∧ length t = n ∧ tF t ∧ ftF u},
             𝒟 P ∪ { t @ u     |t u.   t ∈ 𝒯 P ∧ length t = n ∧ tF t ∧ ftF u})›
proof -
  show ‹?thesis P n› (is ‹is_process (?f, ?d)›) for P and n
  proof (unfold is_process_def FAILURES_def fst_conv DIVERGENCES_def snd_conv, intro conjI impI allI)
    show ‹([], {}) ∈ ?f› by (simp add: process_charn)
  next
    show ‹(t, X) ∈ ?f ⟹ ftF t› for t X
      by simp (meson front_tickFree_append is_processT)
  next
    fix t u
    assume ‹(t @ u, {}) ∈ ?f›
    then consider ‹(t @ u, {}) ∈ ℱ P›
      | t' u' where ‹t @ u = t' @ u'› ‹t' ∈ 𝒯 P› ‹length t' = n› ‹tF t'› ‹ftF u'› by blast
    thus ‹(t, {}) ∈ ?f›
    proof cases
      assume ‹(t @ u, {}) ∈ ℱ P›
      with is_processT3 have ‹(t, {}) ∈ ℱ P› by auto
      thus ‹(t, {}) ∈ ?f› by fast
    next
      fix t' u' assume * : ‹t @ u = t' @ u'› ‹t' ∈ 𝒯 P› ‹length t' = n› ‹tF t'› ‹ftF u'›
      show ‹(t, {}) ∈ ?f›
      proof (cases ‹t ≤ t'›)
        assume ‹t ≤ t'›
        with "*"(2) is_processT3_TR have ‹t ∈ 𝒯 P› by auto
        thus ‹(t, {}) ∈ ?f› by (simp add: T_F)
      next
        assume ‹¬ t ≤ t'›
        with "*"(1) have ‹t = t' @ take (length t - length t') u'›
          by (metis (no_types, lifting) Prefix_Order.prefixI append_Nil2
              diff_is_0_eq nle_le take_all take_append take_eq_Nil)
        with "*"(2, 3, 4, 5) show ‹(t, {}) ∈ ?f›
          by simp (metis append_take_drop_id front_tickFree_dw_closed)
      qed
    qed
  next
    show ‹(t, Y) ∈ ?f ∧ X ⊆ Y ⟹ (t, X) ∈ ?f› for t X Y
      by simp (meson is_processT4)
  next
    show ‹(t, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (t @ [c], {}) ∉ ?f) ⟹ (t, X ∪ Y) ∈ ?f› for t X Y
      by (auto simp add: is_processT5)
  next
    show ‹(t @ [✓(r)], {}) ∈ ?f ⟹ (t, X - {✓(r)}) ∈ ?f› for t r X
      by (simp, elim disjE exE, solves ‹simp add: is_processT6›)
        (metis append_assoc butlast_snoc front_tickFree_dw_closed
          nonTickFree_n_frontTickFree non_tickFree_tick tickFree_append_iff)
  next
    from front_tickFree_append is_processT7 tickFree_append_iff
    show ‹t ∈ ?d ∧ tF t ∧ ftF u ⟹ t @ u ∈ ?d› for t u by fastforce
  next
    from D_F show ‹t ∈ ?d ⟹ (t, X) ∈ ?f› for t X by blast
  next
    show ‹t @ [✓(r)] ∈ ?d ⟹ t ∈ ?d› for t r
      by simp (metis butlast_append butlast_snoc front_tickFree_iff_tickFree_butlast is_processT9
          non_tickFree_tick tickFree_Nil tickFree_append_iff tickFree_imp_front_tickFree)
  qed
qed



subsection ‹Projections›

context fixes P :: ‹('a, 'r) processptick› begin

lemma F_restriction_processptick :
  ‹ℱ (P ↓ n) = ℱ P ∪ {(t @ u, X) |t u X. t ∈ 𝒯 P ∧ length t = n ∧ tF t ∧ ftF u}›
  by (simp add: Failures_def FAILURES_def restriction_processptick.rep_eq)     

lemma D_restriction_processptick :
  ‹𝒟 (P ↓ n) = 𝒟 P ∪ {t @ u |t u. t ∈ 𝒯 P ∧ length t = n ∧ tF t ∧ ftF u}›
  by (simp add: Divergences_def DIVERGENCES_def restriction_processptick.rep_eq)

lemma T_restriction_processptick :
  ‹𝒯 (P ↓ n) = 𝒯 P ∪ {t @ u |t u. t ∈ 𝒯 P ∧ length t = n ∧ tF t ∧ ftF u}›
  using F_restriction_processptick by (auto simp add: Failures_def Traces_def TRACES_def)

lemmas restriction_processptick_projs = F_restriction_processptick D_restriction_processptick T_restriction_processptick


lemma D_restriction_processptickE:
  assumes ‹t ∈ 𝒟 (P ↓ n)›
  obtains ‹t ∈ 𝒟 P› and ‹length t ≤ n›
  | u v where ‹t = u @ v› ‹u ∈ 𝒯 P› ‹length u = n› ‹tF u› ‹ftF v›
proof -
  note assms = that
  from ‹t ∈ 𝒟 (P ↓ n)› have ‹ftF t› by (simp add: D_imp_front_tickFree)
  from ‹t ∈ 𝒟 (P ↓ n)› consider ‹t ∈ 𝒟 P›
    | u v where ‹t = u @ v› ‹u ∈ 𝒯 P› ‹length u = n› ‹tF u› ‹ftF v›
    by (simp add: D_restriction_processptick) blast
  thus thesis
  proof cases
    show ‹t = u @ v ⟹ u ∈ 𝒯 P ⟹ length u = n ⟹ tF u ⟹ ftF v ⟹ thesis› for u v
      by (fact assms(2))
  next
    show thesis if ‹t ∈ 𝒟 P›
    proof (cases ‹length t ≤ n›)
      from ‹t ∈ 𝒟 P› show ‹length t ≤ n ⟹ thesis› by (rule assms(1))
    next
      show thesis if ‹¬ length t ≤ n›
      proof (intro assms(2) exI)
        show ‹t = take n t @ drop n t› by simp
      next
        show ‹take n t ∈ 𝒯 P› by (metis D_T ‹t ∈ 𝒟 P› append_take_drop_id is_processT3_TR_append)
      next
        show ‹length (take n t) = n› by (simp add: min_def ‹¬ length t ≤ n›)
      next
        show ‹tF (take n t)› by (metis ‹ftF t› append_take_drop_id drop_eq_Nil2
              front_tickFree_append_iff ‹¬ length t ≤ n›)
      next
        show ‹ftF (drop n t)› by (metis ‹ftF t› append_take_drop_id drop_eq_Nil
              front_tickFree_append_iff that)
      qed
    qed
  qed
qed


lemma F_restriction_processptickE :
  assumes ‹(t, X) ∈ ℱ (P ↓ n)›
  obtains ‹(t, X) ∈ ℱ P› and ‹length t ≤ n›
  | u v where ‹t = u @ v› ‹u ∈ 𝒯 P› ‹length u = n› ‹tF u› ‹ftF v›
proof -
  from ‹(t, X) ∈ ℱ (P ↓ n)› consider ‹(t, X) ∈ ℱ P› | ‹t ∈ 𝒟 (P ↓ n)›
    unfolding restriction_processptick_projs by blast
  thus thesis
  proof cases
    show ‹(t, X) ∈ ℱ P ⟹ thesis›
      by (metis F_T F_imp_front_tickFree append_take_drop_id
          drop_eq_Nil front_tickFree_nonempty_append_imp
          is_processT3_TR_append length_take min_def that)
  next
    show ‹t ∈ 𝒟 (P ↓ n) ⟹ thesis› by (meson D_restriction_processptickE is_processT8 that)
  qed
qed


lemma T_restriction_processptickE :
  ‹⟦t ∈ 𝒯 (P ↓ n); t ∈ 𝒯 P ⟹ length t ≤ n ⟹ thesis;
    ⋀u v. t = u @ v ⟹ u ∈ 𝒯 P ⟹ length u = n ⟹ tF u ⟹ ftF v ⟹ thesis⟧ ⟹ thesis›
  by (fold T_F_spec, elim F_restriction_processptickE) (simp_all add: T_F)


lemmas restriction_processptick_elims =
  F_restriction_processptickE D_restriction_processptickE T_restriction_processptickE


lemma D_restriction_processptickI :
  ‹t ∈ 𝒟 P ∨ t ∈ 𝒯 P ∧ (length t = n ∧ tF t ∨ n < length t) ⟹ t ∈ 𝒟 (P ↓ n)›
  by (simp add: D_restriction_processptick, elim disjE conjE)
    (solves simp, use front_tickFree_Nil in blast, 
      metis (no_types) T_imp_front_tickFree append_self_conv front_tickFree_nonempty_append_imp
      id_take_nth_drop is_processT3_TR_append leD length_take min.absorb4 take_all_iff)

lemma F_restriction_processptickI :
  ‹(t, X) ∈ ℱ P ∨ t ∈ 𝒯 P ∧ (length t = n ∧ tF t ∨ n < length t) ⟹ (t, X) ∈ ℱ (P ↓ n)›
  by (metis (mono_tags, lifting) D_restriction_processptickI F_restriction_processptick Un_iff is_processT8)

lemma T_restriction_processptickI :
  ‹t ∈ 𝒯 P ∨ t ∈ 𝒯 P ∧ (length t = n ∧ tF t ∨ n < length t) ⟹ t ∈ 𝒯 (P ↓ n)›
  using F_restriction_processptickI T_F_spec by blast



lemma F_restriction_processptick_Suc_length_iff_F :
  ‹(t, X) ∈ ℱ (P ↓ Suc (length t)) ⟷ (t, X) ∈ ℱ P›
  and D_restriction_processptick_Suc_length_iff_D :
  ‹t ∈ 𝒟 (P ↓ Suc (length t)) ⟷ t ∈ 𝒟 P›
  and T_restriction_processptick_Suc_length_iff_T :
  ‹t ∈ 𝒯 (P ↓ Suc (length t)) ⟷ t ∈ 𝒯 P›
  by (auto simp add: restriction_processptick_projs)


lemma length_less_in_F_restriction_processptick :
  ‹length t < n ⟹ (t, X) ∈ ℱ (P ↓ n) ⟹ (t, X) ∈ ℱ P›
  by (auto elim: F_restriction_processptickE)

lemma length_le_in_T_restriction_processptick :
  ‹length t ≤ n ⟹ t ∈ 𝒯 (P ↓ n) ⟹ t ∈ 𝒯 P›
  by (auto elim: T_restriction_processptickE)

lemma length_less_in_D_restriction_processptick :
  ‹length t < n ⟹ t ∈ 𝒟 (P ↓ n) ⟹ t ∈ 𝒟 P›
  by (auto elim: D_restriction_processptickE)

lemma not_tickFree_in_F_restriction_processptick_iff :
  ‹length t ≤ n ⟹ ¬ tF t ⟹ (t, X) ∈ ℱ (P ↓ n) ⟷ (t, X) ∈ ℱ P›
  by (auto simp add: F_restriction_processptick)

lemma not_tickFree_in_D_restriction_processptick_iff :
  ‹length t ≤ n ⟹ ¬ tF t ⟹ t ∈ 𝒟 (P ↓ n) ⟷ t ∈ 𝒟 P›
  by (auto simp add: D_restriction_processptick)

end


(* TODO: move this in HOL-CSP ? *)
lemma front_tickFreeE :
  ‹⟦ftF t; tF t ⟹ thesis; ⋀t' r. t = t' @ [✓(r)] ⟹ tF t' ⟹ thesis⟧ ⟹ thesis›
  by (metis front_tickFree_append_iff nonTickFree_n_frontTickFree not_Cons_self2)


subsection ‹Proof obligation›

instance
proof intro_classes
  fix P Q :: ‹('a, 'r) processptick›
  have ‹P ↓ 0 = ⊥› by (simp add: BOT_iff_Nil_D D_restriction_processptick)
  thus ‹P ↓ 0 ⊑FD Q ↓ 0› by simp
next
  show ‹P ↓ n ↓ m = P ↓ min n m› for P :: ‹('a, 'r) processptick› and n m
  proof (rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 (P ↓ n ↓ m) ⟹ t ∈ 𝒟 (P ↓ min n m)› for t
      by (elim restriction_processptick_elims)
        (auto simp add: D_restriction_processptick intro: front_tickFree_append)
  next
    show ‹t ∈ 𝒟 (P ↓ min n m) ⟹ t ∈ 𝒟 (P ↓ n ↓ m)› for t
      by (elim restriction_processptick_elims)
        (auto simp add: restriction_processptick_projs min_def split: if_split_asm)
  next
    fix t X assume ‹(t, X) ∈ ℱ (P ↓ n ↓ m)› ‹t ∉ 𝒟 (P ↓ n ↓ m)›
    hence ‹(t, X) ∈ ℱ P ∧ length t ≤ min n m›
      by (elim F_restriction_processptickE) (auto simp add: restriction_processptick_projs)
    thus ‹(t, X) ∈ ℱ (P ↓ min n m)› unfolding F_restriction_processptick by blast
  next
    fix t X assume ‹(t, X) ∈ ℱ (P ↓ min n m)› ‹t ∉ 𝒟 (P ↓ min n m)›
    hence ‹(t, X) ∈ ℱ P ∧ length t ≤ min n m›
      by (elim F_restriction_processptickE) (auto simp add: restriction_processptick_projs)
    thus ‹(t, X) ∈ ℱ (P ↓ n ↓ m)› unfolding F_restriction_processptick by blast
  qed
next
  show ‹P ⊑FD Q ⟹ P ↓ n ⊑FD Q ↓ n› for P Q :: ‹('a, 'r) processptick› and n
    by (simp add: refine_defs restriction_processptick_projs
        flip: T_F_spec) blast
next  
  fix P Q :: ‹('a, 'r) processptick› assume ‹¬ P ⊑FD Q›
  then consider t where ‹t ∈ 𝒟 Q› ‹t ∉ 𝒟 P›
    | t X where ‹(t, X) ∈ ℱ Q› ‹(t, X) ∉ ℱ P›
    unfolding refine_defs by auto
  thus ‹∃n. ¬ P ↓ n ⊑FD Q ↓ n›
  proof cases
    fix t assume ‹t ∈ 𝒟 Q› ‹t ∉ 𝒟 P›
    with D_restriction_processptick_Suc_length_iff_D
    have ‹t ∈ 𝒟 (Q ↓ Suc (length t)) ∧ t ∉ 𝒟 (P ↓ Suc (length t))› by blast
    hence ‹¬ P ↓ Suc (length t) ⊑FD Q ↓ Suc (length t)› unfolding refine_defs by blast
    thus ‹∃n. ¬ P ↓ n ⊑FD Q ↓ n› ..
  next
    fix t X assume ‹(t, X) ∈ ℱ Q› ‹(t, X) ∉ ℱ P›
    with F_restriction_processptick_Suc_length_iff_F
    have ‹(t, X) ∈ ℱ (Q ↓ Suc (length t)) ∧ (t, X) ∉ ℱ (P ↓ Suc (length t))› by blast
    hence ‹¬ P ↓ Suc (length t) ⊑FD Q ↓ Suc (length t)› unfolding refine_defs by blast
    thus ‹∃n. ¬ P ↓ n ⊑FD Q ↓ n› ..
  qed
qed


―‹Of course, we immediately recover the structure of class‹restriction_space›.›

corollary ‹OFCLASS(('a, 'r) processptick, restriction_space_class)›
  by intro_classes

end

instance processptick :: (type, type) pcpo_restriction_space
proof intro_classes
  show ‹P ↓ 0 ⊑ Q ↓ 0› for P Q :: ‹('a, 'r) processptick›
    by (metis below_refl restriction_0_related)
next
  show ‹P ↓ n ⊑ Q ↓ n› if ‹P ⊑ Q› for P Q :: ‹('a, 'r) processptick› and n
  proof (unfold le_approx_def Refusals_after_def, safe)
    from ‹P ⊑ Q›[THEN le_approx1] ‹P ⊑ Q›[THEN le_approx2T]
    show ‹t ∈ 𝒟 (Q ↓ n) ⟹ t ∈ 𝒟 (P ↓ n)› for t
      by (simp add: D_restriction_processptick subset_iff) (metis D_T)
  next
    from ‹P ⊑ Q›[THEN le_approx2] ‹P ⊑ Q›[THEN le_approx_lemma_T]
    show ‹t ∉ 𝒟 (P ↓ n) ⟹ (t, X) ∈ ℱ (P ↓ n) ⟹ (t, X) ∈ ℱ (Q ↓ n)›
      and ‹t ∉ 𝒟 (P ↓ n) ⟹ (t, X) ∈ ℱ (Q ↓ n) ⟹ (t, X) ∈ ℱ (P ↓ n)› for t X
      by (auto simp add: restriction_processptick_projs)
  next
    from ‹P ⊑ Q›[THEN le_approx3] ‹P ⊑ Q›[THEN le_approx2T]
    show ‹t ∈ min_elems (𝒟 (P ↓ n)) ⟹ t ∈ 𝒯 (Q ↓ n)› for t
      by (simp add: min_elems_def restriction_processptick_projs ball_Un subset_iff)
        (metis is_processT7)
  qed
next
  fix P Q :: ‹('a, 'r) processptick›
  assume ‹¬ P ⊑ Q›
  then consider t where ‹t ∈ 𝒟 Q› ‹t ∉ 𝒟 P›
    | t X where ‹t ∉ 𝒟 P› ‹(t, X) ∈ ℱ P ⟷ (t, X) ∉ ℱ Q›
    | t where ‹t ∈ min_elems (𝒟 P)› ‹t ∉ 𝒯 Q›
    unfolding le_approx_def Refusals_after_def by blast
  thus ‹∃n. ¬ P ↓ n ⊑ Q ↓ n›
  proof cases
    fix t assume ‹t ∈ 𝒟 Q› ‹t ∉ 𝒟 P›
    hence ‹t ∈ 𝒟 (Q ↓ Suc (length t))› ‹t ∉ 𝒟 (P ↓ Suc (length t))›
      by (simp_all add: D_restriction_processptick_Suc_length_iff_D)
    hence ‹¬ P ↓ Suc (length t) ⊑ Q ↓ Suc (length t)›
      unfolding le_approx_def by blast
    thus ‹∃n. ¬ P ↓ n ⊑ Q ↓ n› ..
  next
    fix t X assume ‹t ∉ 𝒟 P› ‹(t, X) ∈ ℱ P ⟷ (t, X) ∉ ℱ Q›
    hence ‹t ∉ 𝒟 (P ↓ Suc (length t))›
      ‹(t, X) ∈ ℱ (P ↓ Suc (length t)) ⟷ (t, X) ∉ ℱ (Q ↓ Suc (length t))›
      by (simp_all add: D_restriction_processptick_Suc_length_iff_D
          F_restriction_processptick_Suc_length_iff_F)
    hence ‹¬ P ↓ Suc (length t) ⊑ Q ↓ Suc (length t)›
      unfolding le_approx_def Refusals_after_def by blast
    thus ‹∃n. ¬ P ↓ n ⊑ Q ↓ n› ..
  next
    fix t assume ‹t ∈ min_elems (𝒟 P)› ‹t ∉ 𝒯 Q›
    hence ‹t ∈ min_elems (𝒟 (P ↓ Suc (length t)))› ‹t ∉ 𝒯 (Q ↓ Suc (length t))›
      by (simp_all add: min_elems_def D_restriction_processptick_Suc_length_iff_D
          T_restriction_processptick_Suc_length_iff_T)
        (meson length_less_in_D_restriction_processptick less_SucI less_length_mono)
    hence ‹¬ P ↓ Suc (length t) ⊑ Q ↓ Suc (length t)›
      unfolding le_approx_def by blast
    thus ‹∃n. ¬ P ↓ n ⊑ Q ↓ n› ..
  qed
next
  show ‹chain S ⟹ ∃P. range S <<| P› for S :: ‹nat ⇒ ('a, 'r) processptick›
    by (simp add: cpo_class.cpo)
next
  show ‹∃P :: ('a, 'r) processptick. ∀Q. P ⊑ Q› by blast
qed


setup ‹Sign.add_const_constraint (const_name‹restriction›, SOME typ‹('a, 'r) processptick ⇒ nat ⇒ ('a, 'r) processptick›)›
  ― ‹Only allow const‹restriction› for typ‹('a, 'r) processptick›
     (otherwise we would often have to specify).›



subsection ‹Compatibility with Refinements›

lemma leF_restriction_processptickI: ‹P ↓ n ⊑F Q ↓ n›
  if ‹⋀s X. (s, X) ∈ ℱ Q ⟹ length s ≤ n ⟹ (s, X) ∈ ℱ (P ↓ n)›
proof (unfold failure_refine_def, safe)
  show ‹(s, X) ∈ ℱ (Q ↓ n) ⟹ (s, X) ∈ ℱ (P ↓ n)› for s X
  proof (elim F_restriction_processptickE exE conjE)
    show ‹(s, X) ∈ ℱ Q ⟹ length s ≤ n ⟹ (s, X) ∈ ℱ (P ↓ n)›
      by (simp add: F_restriction_processptick) (meson F_restriction_processptickE that)
  next
    fix s' t'
    assume ‹s = s' @ t'› ‹s' ∈ 𝒯 Q› ‹length s' = n› ‹tickFree s'› ‹front_tickFree t'›
    from ‹s' ∈ 𝒯 Q› ‹length s' = n› have ‹s' ∈ 𝒯 P›
      by (metis F_T T_F dual_order.refl length_le_in_T_restriction_processptick that)
    with ‹s = s' @ t'› ‹length s' = n› ‹tickFree s'› ‹front_tickFree t'›
    show ‹(s, X) ∈ ℱ (P ↓ n)› by (simp add: F_restriction_processptick) blast
  qed
qed


lemma leT_restriction_processptickI: ‹P ↓ n ⊑T Q ↓ n›
  if ‹⋀s. s ∈ 𝒯 Q ⟹ length s ≤ n ⟹ s ∈ 𝒯 (P ↓ n)›
proof (unfold trace_refine_def, safe)
  show ‹s ∈ 𝒯 (Q ↓ n) ⟹ s ∈ 𝒯 (P ↓ n)› for s
  proof (elim T_restriction_processptickE exE conjE)
    show ‹s ∈ 𝒯 Q ⟹ length s ≤ n ⟹ s ∈ 𝒯 (P ↓ n)›
      by (simp add: T_restriction_processptick) (meson T_restriction_processptickE that)
  next
    fix s' t'
    assume ‹s = s' @ t'› ‹s' ∈ 𝒯 Q› ‹length s' = n› ‹tickFree s'› ‹front_tickFree t'›
    from ‹s' ∈ 𝒯 Q› ‹length s' = n› have ‹s' ∈ 𝒯 P›
      using length_le_in_T_restriction_processptick that by blast
    with ‹s = s' @ t'› ‹length s' = n› ‹tickFree s'› ‹front_tickFree t'›
    show ‹s ∈ 𝒯 (P ↓ n)› by (simp add: T_restriction_processptick) blast
  qed
qed


lemma leDT_restriction_processptickI: ‹P ↓ n ⊑DT Q ↓ n›
  if ‹⋀s. s ∈ 𝒯 Q ⟹ length s ≤ n ⟹ s ∈ 𝒯 (P ↓ n)›
    and ‹⋀s. length s ≤ n ⟹ s ∈ 𝒟 Q ⟹ s ∈ 𝒟 (P ↓ n)›
proof (rule leD_leT_imp_leDT)
  show ‹P ↓ n ⊑T Q ↓ n› by (simp add: leT_restriction_processptickI that(1))
next
  show ‹P ↓ n ⊑D Q ↓ n›
  proof (unfold divergence_refine_def, rule subsetI)
    show ‹s ∈ 𝒟 (Q ↓ n) ⟹ s ∈ 𝒟 (P ↓ n)› for s
    proof (elim D_restriction_processptickE exE conjE)
      show ‹s ∈ 𝒟 Q ⟹ length s ≤ n ⟹ s ∈ 𝒟 (P ↓ n)›
        by (simp add: D_restriction_processptick) (meson D_restriction_processptickE that(2))
    next
      fix s' t'
      assume ‹s = s' @ t'› ‹s' ∈ 𝒯 Q› ‹length s' = n› ‹tickFree s'› ‹front_tickFree t'›
      from ‹s' ∈ 𝒯 Q› ‹length s' = n› have ‹s' ∈ 𝒯 P›
        using length_le_in_T_restriction_processptick that(1) by blast
      with ‹s = s' @ t'› ‹length s' = n› ‹tickFree s'› ‹front_tickFree t'›
      show ‹s ∈ 𝒟 (P ↓ n)› by (simp add: D_restriction_processptick) blast
    qed
  qed
qed


lemma leFD_restriction_processptickI: ‹P ↓ n ⊑FD Q ↓ n›
  if ‹⋀s X. (s, X) ∈ ℱ Q ⟹ length s ≤ n ⟹ (s, X) ∈ ℱ (P ↓ n)›
    and ‹⋀s. s ∈ 𝒟 Q ⟹ length s ≤ n ⟹ s ∈ 𝒟 (P ↓ n)›
proof (rule leF_leD_imp_leFD)
  show ‹P ↓ n ⊑F Q ↓ n› by (simp add: leF_restriction_processptickI that(1))
next
  show ‹P ↓ n ⊑D Q ↓ n›  by (meson T_F_spec leDT_imp_leD leDT_restriction_processptickI that)
qed



subsection ‹First Laws›

lemma restriction_processptick_0 [simp] : ‹P ↓ 0 = ⊥›
  by (simp add: BOT_iff_Nil_D D_restriction_processptick)

lemma restriction_processptick_BOT [simp] : ‹(⊥ :: ('a, 'r) processptick) ↓ n = ⊥›
  by (simp add: BOT_iff_Nil_D D_restriction_processptick D_BOT)

lemma restriction_processptick_is_BOT_iff :
  ‹P ↓ n = ⊥ ⟷ n = 0 ∨ P = ⊥›
  by (auto simp add: BOT_iff_Nil_D D_restriction_processptick)


lemma restriction_processptick_STOP [simp] : ‹STOP ↓ n = (if n = 0 then ⊥ else STOP)›
  by (simp add: STOP_iff_T T_restriction_processptick T_STOP)

lemma restriction_processptick_is_STOP_iff : ‹P ↓ n = STOP ⟷ n ≠ 0 ∧ P = STOP›
  by (simp add: STOP_iff_T T_restriction_processptick set_eq_iff)
    (metis (no_types, lifting) append_self_conv2 front_tickFree_single gr0I
      less_numeral_extra(3) list.discI list.size(3) tickFree_Nil)


lemma restriction_processptick_SKIP [simp] : ‹SKIP r ↓ n = (if n = 0 then ⊥ else SKIP r)›
  by simp (auto simp add: Process_eq_spec restriction_processptick_projs SKIP_projs)

lemma restriction_processptick_is_SKIP_iff : ‹P ↓ n = SKIP r ⟷ n ≠ 0 ∧ P = SKIP r›
proof (intro iffI conjI)
  show ‹n ≠ 0 ∧ P = SKIP r ⟹ P ↓ n = SKIP r› by simp
next
  show ‹P ↓ n = SKIP r ⟹ n ≠ 0› by (metis restriction_processptick_0 SKIP_neq_BOT)
next
  show ‹P ↓ n = SKIP r ⟹ P = SKIP r›
    by (simp add: Process_eq_spec set_eq_iff SKIP_projs
        restriction_processptick_projs, safe; metis)
qed


lemma restriction_processptick_SKIPS [simp] : ‹SKIPS R ↓ n = (if n = 0 then ⊥ else SKIPS R)›
  by simp (auto simp add: Process_eq_spec restriction_processptick_projs SKIPS_projs)

lemma restriction_processptick_is_SKIPS_iff : ‹P ↓ n = SKIPS R ⟷ n ≠ 0 ∧ P = SKIPS R›
proof (cases ‹R = {}›)
  show ‹R = {} ⟹ P ↓ n = SKIPS R ⟷ n ≠ 0 ∧ P = SKIPS R›
    by (simp add: restriction_processptick_is_STOP_iff)
next
  show ‹P ↓ n = SKIPS R ⟷ n ≠ 0 ∧ P = SKIPS R› if ‹R ≠ {}›
  proof (intro iffI conjI)
    show ‹n ≠ 0 ∧ P = SKIPS R ⟹ P ↓ n = SKIPS R› by simp
  next
    show ‹P ↓ n = SKIPS R ⟹ n ≠ 0› 
      by (metis BOT_iff_Nil_D D_SKIPS empty_iff restriction_processptick_0)
  next
    show ‹P ↓ n = SKIPS R ⟹ P = SKIPS R›
      by (simp add: Process_eq_spec ‹R ≠ {}› SKIPS_projs
          restriction_processptick_projs, safe; blast)
  qed
qed



subsection ‹Monotony›

subsubsection ‹term‹P ↓ n› is an Approximation of the term‹P››

lemma restriction_processptick_approx_self : ‹P ↓ n ⊑ P›
proof (unfold le_approx_def Refusals_after_def, safe)
  show ‹t ∈ 𝒟 P ⟹ t ∈ 𝒟 (P ↓ n)› for t by (simp add: D_restriction_processptick)
next
  show ‹t ∉ 𝒟 (P ↓ n) ⟹ (t, X) ∈ ℱ (P ↓ n) ⟹ (t, X) ∈ ℱ P› for t X
    by (auto simp add: D_restriction_processptick elim: F_restriction_processptickE)
next
  show ‹t ∉ 𝒟 (P ↓ n) ⟹ (t, X) ∈ ℱ P ⟹ (t, X) ∈ ℱ (P ↓ n)› for t X
    by (auto simp add: restriction_processptick_projs)
next
  show ‹t ∈ min_elems (𝒟 (P ↓ n)) ⟹ t ∈ 𝒯 P› for t
    by (auto simp add: min_elems_def D_restriction_processptick ball_Un D_T)
      (metis append.right_neutral front_tickFree_charn less_append nil_less2)
qed

lemma restriction_processptick_FD_self : ‹P ↓ n ⊑FD P›
  by (simp add: le_approx_imp_le_ref restriction_processptick_approx_self)

lemma restriction_processptick_F_self : ‹P ↓ n ⊑F P›
  by (simp add: restriction_processptick_FD_self leFD_imp_leF)

lemma restriction_processptick_D_self : ‹P ↓ n ⊑D P›
  by (simp add: restriction_processptick_FD_self leFD_imp_leD)

lemma restriction_processptick_T_self : ‹P ↓ n ⊑T P›
  by (simp add: restriction_processptick_F_self leF_imp_leT) 

lemma restriction_processptick_DT_self : ‹P ↓ n ⊑DT P›
  by (simp add: restriction_processptick_D_self restriction_processptick_T_self leD_leT_imp_leDT)



subsubsection ‹Monotony of term‹(↓)››

lemma Suc_right_mono_restriction_processptick : ‹P ↓ n ⊑ P ↓ Suc n›
  by (metis restriction_processptick_approx_self restriction_chainD
      restriction_chain_restrictions)

lemma Suc_right_mono_restriction_processptick_FD : ‹P ↓ n ⊑FD P ↓ Suc n›
  by (simp add: Suc_right_mono_restriction_processptick le_approx_imp_le_ref)

lemma Suc_right_mono_restriction_processptick_F  : ‹P ↓ n ⊑F P ↓ Suc n›
  by (simp add: Suc_right_mono_restriction_processptick_FD leFD_imp_leF)

lemma Suc_right_mono_restriction_processptick_D  : ‹P ↓ n ⊑D P ↓ Suc n›
  by (simp add: Suc_right_mono_restriction_processptick_FD leFD_imp_leD)

lemma Suc_right_mono_restriction_processptick_T  : ‹P ↓ n ⊑T P ↓ Suc n›
  by (simp add: Suc_right_mono_restriction_processptick_FD leFD_imp_leF leF_imp_leT)

lemma Suc_right_mono_restriction_processptick_DT : ‹P ↓ n ⊑DT P ↓ Suc n›
  by (simp add: Suc_right_mono_restriction_processptick_D
      Suc_right_mono_restriction_processptick_T leD_leT_imp_leDT)


lemma le_right_mono_restriction_processptick : ‹n ≤ m ⟹ P ↓ n ⊑ P ↓ m›
  by (metis restriction_processptick_approx_self restriction_chain_def_ter
      restriction_chain_restrictions)


lemma le_right_mono_restriction_processptick_FD : ‹n ≤ m ⟹ P ↓ n ⊑FD P ↓ m›
  by (simp add: le_approx_imp_le_ref le_right_mono_restriction_processptick)

lemma le_right_mono_restriction_processptick_F : ‹n ≤ m ⟹ P ↓ n ⊑F P ↓ m›
  by (simp add: leFD_imp_leF le_right_mono_restriction_processptick_FD)

lemma restriction_processptick_le_right_mono_D : ‹n ≤ m ⟹ P ↓ n ⊑D P ↓ m›
  by (simp add: leFD_imp_leD le_right_mono_restriction_processptick_FD)

lemma restriction_processptick_le_right_mono_T : ‹n ≤ m ⟹ P ↓ n ⊑T P ↓ m›
  by (simp add: leF_imp_leT le_right_mono_restriction_processptick_F)

lemma restriction_processptick_le_right_mono_DT : ‹n ≤ m ⟹ P ↓ n ⊑DT P ↓ m›
  by (simp add: restriction_processptick_le_right_mono_D
      restriction_processptick_le_right_mono_T leD_leT_imp_leDT)



subsubsection ‹Interpretations of Refinements›

lemma ex_not_restriction_leD : ‹∃n. ¬ P ↓ n ⊑D Q ↓ n› if ‹¬ P ⊑D Q›
proof -
  from ‹¬ P ⊑D Q› obtain t where ‹t ∈ 𝒟 Q› ‹t ∉ 𝒟 P›
    unfolding divergence_refine_def by blast
  hence ‹t ∈ 𝒟 (Q ↓ Suc (length t))› ‹t ∉ 𝒟 (P ↓ Suc (length t))›
    by (simp_all add: D_restriction_processptick_Suc_length_iff_D)
  hence ‹¬ P ↓ Suc (length t) ⊑D Q ↓ Suc (length t)›
    unfolding divergence_refine_def by blast
  thus ‹∃n. ¬ P ↓ n ⊑D Q ↓ n› ..
qed

interpretation PRS_leF : PreorderRestrictionSpace ‹(↓)› ‹(⊑F)›
proof unfold_locales
  show ‹P ↓ 0 ⊑F Q ↓ 0› for P Q :: ‹('a, 'r) processptick› by simp
next
  show ‹P ⊑F Q ⟹ P ↓ n ⊑F Q ↓ n› for P Q :: ‹('a, 'r) processptick› and n
    by (simp add: failure_refine_def F_restriction_processptick
        flip: T_F_spec) blast
next
  fix P Q :: ‹('a, 'r) processptick› assume ‹¬ P ⊑F Q›
  then obtain t X where ‹(t, X) ∈ ℱ Q› ‹(t, X) ∉ ℱ P›
    unfolding failure_refine_def by auto
  with F_restriction_processptick_Suc_length_iff_F
  have ‹(t, X) ∈ ℱ (Q ↓ Suc (length t)) ∧ (t, X) ∉ ℱ (P ↓ Suc (length t))› by blast
  hence ‹¬ P ↓ Suc (length t) ⊑F Q ↓ Suc (length t)› unfolding failure_refine_def by blast
  thus ‹∃n. ¬ P ↓ n ⊑F Q ↓ n› ..
next
  show ‹P ⊑F Q ⟹ Q ⊑F R ⟹ P ⊑F R› for P Q R :: ‹('a, 'r) processptick›
    by (fact trans_F)
qed


interpretation PRS_leT : PreorderRestrictionSpace ‹(↓)› ‹(⊑T)›
proof unfold_locales
  show ‹P ↓ 0 ⊑T Q ↓ 0› for P Q :: ‹('a, 'r) processptick› by simp
next
  show ‹P ⊑T Q ⟹ P ↓ n ⊑T Q ↓ n› for P Q :: ‹('a, 'r) processptick› and n
    by (auto simp add: trace_refine_def T_restriction_processptick)
next
  fix P Q :: ‹('a, 'r) processptick› assume ‹¬ P ⊑T Q›
  then obtain t where ‹t ∈ 𝒯 Q› ‹t ∉ 𝒯 P›
    unfolding trace_refine_def by auto
  with T_restriction_processptick_Suc_length_iff_T
  have ‹t ∈ 𝒯 (Q ↓ Suc (length t)) ∧ t ∉ 𝒯 (P ↓ Suc (length t))› by blast
  hence ‹¬ P ↓ Suc (length t) ⊑T Q ↓ Suc (length t)› unfolding trace_refine_def by blast
  thus ‹∃n. ¬ P ↓ n ⊑T Q ↓ n› ..
next
  show ‹P ⊑T Q ⟹ Q ⊑T R ⟹ P ⊑T R› for P Q R :: ‹('a, 'r) processptick›
    by (fact trans_T)
qed


interpretation PRS_leDT : PreorderRestrictionSpace ‹(↓)› ‹(⊑DT)›
proof unfold_locales
  show ‹P ↓ 0 ⊑DT Q ↓ 0› for P Q :: ‹('a, 'r) processptick› by simp
next
  show ‹P ⊑DT Q ⟹ P ↓ n ⊑DT Q ↓ n› for P Q :: ‹('a, 'r) processptick› and n
    by (auto simp add: refine_defs restriction_processptick_projs)
next
  fix P Q :: ‹('a, 'r) processptick› assume ‹¬ P ⊑DT Q›
  hence ‹¬ P ⊑D Q ∨ ¬ P ⊑T Q› unfolding trace_divergence_refine_def by blast
  with ex_not_restriction_leD PRS_leT.ex_not_restriction_related
  have ‹(∃n. ¬ P ↓ n ⊑D Q ↓ n) ∨ (∃n. ¬ P ↓ n ⊑T Q ↓ n)› by blast
  thus ‹∃n. ¬ P ↓ n ⊑DT Q ↓ n›
    unfolding trace_divergence_refine_def by blast
next
  show ‹P ⊑DT Q ⟹ Q ⊑DT R ⟹ P ⊑DT R› for P Q R :: ‹('a, 'r) processptick›
    by (fact trans_DT)
qed



subsection ‹Continuity›

context begin

private lemma chain_restriction_processptick : ‹chain Y ⟹ chain (λi. Y i ↓ n)›
  by (simp add: mono_restriction_below po_class.chain_def)


private lemma cont_prem_restriction_processptick :
  ‹(⨆ i. Y i) ↓ n = (⨆ i. Y i ↓ n)› (is ‹?lhs = ?rhs›) if ‹chain Y›
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (auto simp add: limproc_is_thelub chain_restriction_processptick
        D_restriction_processptick LUB_projs ‹chain Y›)
next
  show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    by (simp add: limproc_is_thelub chain_restriction_processptick
        D_restriction_processptick LUB_projs ‹chain Y›)
      (metis D_T append_eq_append_conv is_processT3_TR_append)
next
  show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
    by (auto simp add: limproc_is_thelub chain_restriction_processptick
        F_restriction_processptick LUB_projs ‹chain Y›)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (simp add: limproc_is_thelub chain_restriction_processptick
        F_restriction_processptick LUB_projs ‹chain Y›)
      (metis F_T append_eq_append_conv is_processT3_TR_append)
qed


lemma restriction_processptick_cont [simp] : ‹cont (λx. f x ↓ n)› if ‹cont f›
proof (rule contI2)
  show ‹monofun (λx. f x ↓ n)›
    by (simp add: cont2monofunE mono_restriction_below monofunI ‹cont f›)
next
  show ‹chain Y ⟹ f (⨆i. Y i) ↓ n ⊑ (⨆i. f (Y i) ↓ n)› for Y
    by (simp add: ch2ch_cont cont2contlubE cont_prem_restriction_processptick ‹cont f›)
qed

end



subsection ‹Completeness›

text ‹Processes are actually an instance of class‹complete_restriction_space›.›

lemma chain_restriction_chain :
  ‹restriction_chain σ ⟹ chain σ› for σ :: ‹nat ⇒ ('a, 'r) processptick›
  by (metis po_class.chainI restriction_processptick_approx_self restriction_chainD)


lemma restricted_LUB_restriction_chain_is :
  ‹(λn. (⨆n. σ n) ↓ n) = σ› if ‹restriction_chain σ›
proof (rule ext)
  have ‹chain σ› by (simp add: chain_restriction_chain ‹restriction_chain σ›)
  moreover have ‹σ = (λn. σ n ↓ n)›
    by (simp add: restricted_restriction_chain_is ‹restriction_chain σ›)
  ultimately have ‹chain (λn. σ n ↓ n)› by simp

  have ‹length t < n ⟹ t ∈ 𝒟 (σ n) ⟷ (∀i. t ∈ 𝒟 (σ i))› for t n
  proof safe
    show ‹t ∈ 𝒟 (σ i)› if ‹length t < n› ‹t ∈ 𝒟 (σ n)› for i
    proof (cases ‹i ≤ n›)
      from ‹t ∈ 𝒟 (σ n)› ‹chain σ› le_approx_def po_class.chain_mono
      show ‹i ≤ n ⟹ t ∈ 𝒟 (σ i)› by blast
    next
      from ‹length t < n› ‹t ∈ 𝒟 (σ n)› show ‹¬ i ≤ n ⟹ t ∈ 𝒟 (σ i)›
        by (induct n, simp_all)
          (metis ‹restriction_chain σ› length_less_in_D_restriction_processptick
            nat_le_linear restriction_chain_def_ter)
    qed
  next
    show ‹∀i. t ∈ 𝒟 (σ i) ⟹ t ∈ 𝒟 (σ n)› by simp
  qed
  hence * : ‹length t < n ⟹ t ∈ 𝒟 (σ n) ⟷ t ∈ 𝒟 (⨆i. σ i)› for t n
    by (simp add: D_LUB ‹chain σ› limproc_is_thelub)

  show ‹(⨆n. σ n) ↓ n = σ n› for n
  proof (subst (3) ‹σ = (λn. σ n ↓ n)›, rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 ((⨆n. σ n) ↓ n) ⟹ t ∈ 𝒟 (σ n ↓ n)› for t
    proof (elim D_restriction_processptickE)
      show ‹t ∈ 𝒟 (⨆n. σ n) ⟹ length t ≤ n ⟹ t ∈ 𝒟 (σ n ↓ n)›
        by (simp add: ‹chain σ› limproc_is_thelub D_LUB D_restriction_processptick)
    next
      show ‹⟦t = u @ v; u ∈ 𝒯 (⨆n. σ n); length u = n; tF u; ftF v⟧ ⟹ t ∈ 𝒟 (σ n ↓ n)› for u v
        by (auto simp add: ‹chain σ› limproc_is_thelub LUB_projs restriction_processptick_projs)
    qed
  next
    fix t assume ‹t ∈ 𝒟 (σ n ↓ n)›
    hence ‹ftF t› by (simp add: D_imp_front_tickFree)
    with ‹t ∈ 𝒟 (σ n ↓ n)› consider ‹length t < n› ‹t ∈ 𝒟 (σ n)›
      | t' r where ‹t = t' @ [✓(r)]› ‹tF t'› ‹length t' < n› ‹t' ∈ 𝒟 (σ n)›
      | u v  where ‹t = u @ v› ‹u ∈ 𝒯 (σ n)› ‹length u = n› ‹tF u› ‹ftF v›
      by (auto elim!: D_restriction_processptickE)
        (metis D_T Suc_le_lessD antisym_conv2 append.right_neutral
          front_tickFree_Nil front_tickFree_nonempty_append_imp
          is_processT9 length_append_singleton nonTickFree_n_frontTickFree)
    thus ‹t ∈ 𝒟 ((⨆n. σ n) ↓ n)›
    proof cases
      show ‹length t < n ⟹ t ∈ 𝒟 (σ n) ⟹ t ∈ 𝒟 ((⨆n. σ n) ↓ n)›
        by (simp add: D_restriction_processptick "*")
    next
      fix t' r assume ‹t = t' @ [✓(r)]› ‹tF t'› ‹length t' < n› ‹t' ∈ 𝒟 (σ n)›
      from ‹length t' < n› ‹t' ∈ 𝒟 (σ n)› have ‹t' ∈ 𝒟 ((⨆n. σ n) ↓ n)›
        by (simp add: D_restriction_processptick "*")
      thus ‹t ∈ 𝒟 ((⨆n. σ n) ↓ n)›
        by (simp add: ‹t = t' @ [✓(r)]› ‹tF t'› is_processT7)
    next
      fix u v assume ‹t = u @ v› ‹u ∈ 𝒯 (σ n)› ‹length u = n› ‹tF u› ‹ftF v›
      from ‹length u = n› ‹u ∈ 𝒯 (σ n)› have ‹u ∈ 𝒯 (σ (Suc n))›
        by (metis length_le_in_T_restriction_processptick nat_le_linear
            restriction_chainD ‹restriction_chain σ›)
      from ‹chain σ› ‹u ∈ 𝒯 (σ (Suc n))› D_T le_approx2T po_class.chain_mono
      have ‹i ≤ Suc n ⟹ u ∈ 𝒯 (σ i)› for i by blast
      moreover have ‹Suc n < i ⟹ u ∈ 𝒯 (σ i)› for i
        by (subst T_restriction_processptick_Suc_length_iff_T[symmetric])
          (metis ‹length u = n› ‹u ∈ 𝒯 (σ (Suc n))›
            restriction_chain_def_bis ‹restriction_chain σ›)
      ultimately have ‹u ∈ 𝒯 (⨆i. σ i)›
        by (metis T_LUB_2 ‹chain σ› limproc_is_thelub linorder_not_le)
      with ‹ftF v› ‹length u = n› ‹tF u› show ‹t ∈ 𝒟 ((⨆n. σ n) ↓ n)›
        by (auto simp add: ‹t = u @ v› D_restriction_processptick)
    qed
  next
    show ‹(t, X) ∈ ℱ ((⨆n. σ n) ↓ n) ⟹ t ∉ 𝒟 ((⨆n. σ n) ↓ n) ⟹ (t, X) ∈ ℱ (σ n ↓ n)› for t X
      by (meson ‹chain σ› is_processT8 is_ub_thelub proc_ord2a restriction_processptick_approx_self)
  next
    fix t X assume ‹(t, X) ∈ ℱ (σ n ↓ n)› ‹t ∉ 𝒟 (σ n ↓ n)›
    hence ‹length t ≤ n› ‹(t, X) ∈ ℱ (σ n)› ‹t ∉ 𝒟 (σ n)›
      by (auto elim!: F_restriction_processptickE simp add: D_restriction_processptick)
    thus ‹(t, X) ∈ ℱ ((⨆i. σ i) ↓ n)›
      by (simp add: F_restriction_processptick)
        (meson ‹chain σ› is_ub_thelub le_approx2)
  qed
qed


instance processptick :: (type, type) complete_restriction_space
proof (intro_classes, rule restriction_convergentI)
  show ‹σ ─↓→ (⨆i. σ i)› if ‹restriction_chain σ› for σ :: ‹nat ⇒ ('a, 'b) processptick›
  proof (subst restricted_LUB_restriction_chain_is[symmetric])
    from ‹restriction_chain σ› show ‹restriction_chain σ› .
  next
    from restriction_tendsto_restrictions
    show ‹(λn. (⨆i. σ i) ↓ n) ─↓→ (⨆i. σ i)› .
  qed
qed


text ‹This is a very powerful result. Now we can write fixed-point equations for processes
      like term‹υ X. f X›, providing the fact that term‹f› is const‹constructive›.›



setup ‹Sign.add_const_constraint (const_name‹restriction›, NONE)›
  ― ‹Back to normal.›

(*<*)
end
  (*>*)