Theory Events_Ticks_CSP_PTick_Laws

(***********************************************************************************
 * 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 ‹Events and Ticks›

(*<*)
theory Events_Ticks_CSP_PTick_Laws
  imports Multi_Sequential_Composition_Generalized
    Multi_Synchronization_Product_Generalized
begin
  (*>*)


section ‹Preliminaries›

lemma strict_events_of_memE_optimized_tickFree :
  ‹(⋀t. t ∈ 𝒯 P ⟹ t ∉ 𝒟 P ⟹ ev a ∈ set t ⟹ tF t ⟹ thesis) ⟹ thesis› if ‹a ∈ α(P)›
proof -
  from ‹a ∈ α(P)› obtain t where ‹t ∈ 𝒯 P› ‹t ∉ 𝒟 P› ‹ev a ∈ set t›
    by (meson strict_events_of_memE)
  have ‹(if tF t then t else butlast t) ∈ 𝒯 P›
    by simp (metis ‹t ∈ 𝒯 P› append_butlast_last_id is_processT3_TR_append tickFree_Nil)
  moreover have ‹(if tF t then t else butlast t) ∉ 𝒟 P›
    using T_imp_front_tickFree ‹t ∈ 𝒯 P› ‹t ∉ 𝒟 P› div_butlast_when_non_tickFree_iff by blast
  moreover from T_nonTickFree_imp_decomp ‹ev a ∈ set t› ‹t ∈ 𝒯 P›
  have ‹ev a ∈ set (if tF t then t else butlast t)› by force
  moreover from T_imp_front_tickFree ‹t ∈ 𝒯 P› front_tickFree_iff_tickFree_butlast
  have ‹tF (if tF t then t else butlast t)› by (metis (full_types))
  ultimately show ‹(⋀t. t ∈ 𝒯 P ⟹ t ∉ 𝒟 P ⟹ ev a ∈ set t ⟹ tF t ⟹ thesis) ⟹ thesis› by blast
qed

lemma events_of_memE_optimized_tickFree :
  ‹(⋀t. t ∈ 𝒯 P ⟹ ev a ∈ set t ⟹ tF t ⟹ thesis) ⟹ thesis› if ‹a ∈ α(P)›
proof -
  from ‹a ∈ α(P)› obtain t where ‹t ∈ 𝒯 P› ‹ev a ∈ set t›
    by (meson events_of_memE)
  have ‹(if tF t then t else butlast t) ∈ 𝒯 P›
    by simp (metis ‹t ∈ 𝒯 P› append_butlast_last_id is_processT3_TR_append tickFree_Nil)
  moreover from T_nonTickFree_imp_decomp ‹ev a ∈ set t› ‹t ∈ 𝒯 P›
  have ‹ev a ∈ set (if tF t then t else butlast t)› by force
  moreover from T_imp_front_tickFree ‹t ∈ 𝒯 P› front_tickFree_iff_tickFree_butlast
  have ‹tF (if tF t then t else butlast t)› by (metis (full_types))
  ultimately show ‹(⋀t. t ∈ 𝒯 P ⟹ ev a ∈ set t ⟹ tF t ⟹ thesis) ⟹ thesis› by blast
qed



section ‹Sequential Composition›

subsection ‹Events›

lemma events_of_Seqptick : ‹α(P ;✓ Q) = α(P) ∪ (⋃r ∈ ✓s(P). α(Q r))›
proof (intro subset_antisym subsetI)
  show ‹a ∈ α(P ;✓ Q) ⟹ a ∈ α(P) ∪ (⋃r ∈ ✓s(P). α(Q r))› for a
  proof (elim events_of_memE)
    fix t assume ‹t ∈ 𝒯 (P ;✓ Q)› ‹ev a ∈ set t›
    from this(1) consider (T_P) t' where ‹t = map (ev ∘ of_ev) t'› ‹t' ∈ 𝒯 P› ‹tF t'›
      | (T_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹u ∈ 𝒯 (Q r)›
      | (D_P) t' u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
      unfolding Seqptick_projs by blast
    thus ‹a ∈ α(P) ∪ (⋃r ∈ ✓s(P). α(Q r))›
    proof cases
      case T_P
      from T_P(1, 3) ‹ev a ∈ set t› have ‹ev a ∈ set t'›
        by (meson tickFree_map_ev_of_ev_eq_imp_ev_mem_iff)
      with T_P(2) have ‹a ∈ α(P)› by (rule events_of_memI)
      thus ‹a ∈ α(P) ∪ (⋃r ∈ ✓s(P). α(Q r))› by simp
    next
      case T_Q
      have ‹r ∈ ✓s(P) ∨ 𝒟 P ≠ {}›
        by (metis T_Q(2) empty_iff strict_ticks_of_memI)
      thus ‹a ∈ α(P) ∪ (⋃r ∈ ✓s(P). α(Q r))›
      proof (elim disjE)
        from T_Q
        show ‹r ∈ ✓s(P) ⟹ a ∈ α(P) ∪ (⋃r ∈ ✓s(P). α(Q r))›
          by simp (metis Un_iff ‹ev a ∈ set t› events_of_memI set_append
              tickFree_map_ev_of_ev_eq_imp_ev_mem_iff)
      next
        assume ‹𝒟 P ≠ {}›
        hence ‹α(P) = UNIV› by (simp add: events_of_is_strict_events_of_or_UNIV)
        thus ‹a ∈ α(P) ∪ (⋃r ∈ ✓s(P). α(Q r))› by simp
      qed
    next
      case D_P
      have ‹α(P) = UNIV›
        by (metis D_P(2) empty_iff events_of_is_strict_events_of_or_UNIV)
      thus ‹a ∈ α(P) ∪ (⋃r ∈ ✓s(P). α(Q r))› by simp
    qed
  qed
next
  show ‹a ∈ α(P) ∪ (⋃r ∈ ✓s(P). α(Q r)) ⟹ a ∈ α(P ;✓ Q)› for a
  proof (elim UnE UnionE events_of_memE, safe)
    fix t assume ‹t ∈ 𝒯 P› ‹ev a ∈ set t›
    then obtain t' where ‹t' ∈ 𝒯 P› ‹tF t'› ‹ev a ∈ set t'›
      by (cases t rule: rev_cases, simp_all)
        (metis prefixI ‹ev a ∈ set t› append_T_imp_tickFree eventptick.disc(1) is_processT3_TR
          not_Cons_self2 tickFree_Cons_iff tickFree_Nil tickFree_append_iff)
    thus ‹a ∈ α(P ;✓ Q)› by (auto simp add: Seqptick_projs rev_image_eqI intro!: events_of_memI)
  next
    fix a r assume ‹a ∈ α(Q r)› ‹r ∈ ✓s(P)›
    from ‹r ∈ ✓s(P)› obtain t where ‹t @ [✓(r)] ∈ 𝒯 P› by (meson strict_ticks_of_memD)
    moreover from ‹a ∈ α(Q r)› obtain u
      where ‹u ∈ 𝒯 (Q r)› ‹ev a ∈ set u› by (meson events_of_memD)
    ultimately have ‹map (ev ∘ of_ev) t @ u ∈ 𝒯 (P ;✓ Q)› ‹ev a ∈ set (map (ev ∘ of_ev) t @ u)›
      by (auto simp add: Seqptick_projs) (metis append_T_imp_tickFree not_Cons_self2)
    thus ‹a ∈ α(P ;✓ Q)› by (simp add: events_of_memI)
  qed
qed

― ‹Big approximation.›
lemma events_of_Seqptick_subset : ‹α(P ;✓ Q) ⊆ α(P) ∪ (⋃r. α(Q r))›
  by (auto simp add: events_of_Seqptick)


― ‹Big approximation.›
corollary events_of_Seq_subset : ‹α(P ; Q) ⊆ α(P) ∪ α(Q)›
  by (simp add: events_of_Seq)


lemma strict_events_of_Seqptick_subset : ‹α(P ;✓ Q) ⊆ α(P) ∪ (⋃r ∈ ✓s(P).α(Q r))›
proof (rule subsetI)
  show ‹a ∈ α(P ;✓ Q) ⟹ a ∈ α(P) ∪ (⋃r ∈ ✓s(P).α(Q r))› for a
  proof (elim strict_events_of_memE)
    fix t assume ‹t ∈ 𝒯 (P ;✓ Q)› ‹t ∉ 𝒟 (P ;✓ Q)› ‹ev a ∈ set t›
    from this(1, 2) consider (T_P) t' where ‹t = map (ev ∘ of_ev) t'› ‹t' ∈ 𝒯 P› ‹t' ∉ 𝒟 P› ‹tF t'›
      | (T_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹t' ∉ 𝒟 P› ‹tF t'› ‹u ∈ 𝒯 (Q r)› ‹u ∉ 𝒟 (Q r)›
      by (auto simp add: Seqptick_projs) (metis T_imp_front_tickFree)
    thus ‹a ∈ α(P) ∪ (⋃r ∈ ✓s(P).α(Q r))›
    proof cases
      case T_P
      have ‹ev a ∈ set t'›
        by (metis T_P(1, 4) ‹ev a ∈ set t› tickFree_map_ev_of_ev_eq_imp_ev_mem_iff)
      have ‹a ∈ α(P)›
        by (meson T_P(2, 3) ‹ev a ∈ set t'› strict_events_of_memI)
      thus ‹a ∈ α(P) ∪ (⋃r ∈ ✓s(P).α(Q r))› by simp
    next
      case T_Q
      have ‹r ∈ ✓s(P)› by (meson T_Q(2, 3) is_processT9 strict_ticks_of_memI)
      thus ‹a ∈ α(P) ∪ (⋃r ∈ ✓s(P).α(Q r))›
        by simp (metis T_Q UnE ‹ev a ∈ set t› is_processT3_TR_append set_append
            strict_events_of_memI tickFree_map_ev_of_ev_eq_imp_ev_mem_iff)
    qed
  qed
qed



subsection ‹Ticks›

lemma ticks_of_Seqptick :
  ‹✓s(P ;✓ Q) = (if 𝒟 P = {} then (⋃r ∈ ✓s(P). ✓s(Q r)) else UNIV)›
proof (split if_split, intro conjI impI)
  show ‹𝒟 P ≠ {} ⟹ ✓s(P ;✓ Q) = UNIV›
    by (simp add: Seqptick_projs ticks_of_is_strict_ticks_of_or_UNIV)
      (metis front_tickFree_Nil nonempty_divE)
next
  show ‹𝒟 P = {} ⟹ ✓s(P ;✓ Q) = (⋃r∈✓s(P). ✓s(Q r))› if ‹𝒟 P = {}›
  proof (intro subset_antisym subsetI)
    from ‹𝒟 P = {}› ticks_of_memI[of _ _ ‹Q _›]
    show ‹s ∈ ✓s(P ;✓ Q) ⟹ s ∈ (⋃r∈✓s(P). ✓s(Q r))› for s
      by (auto simp add: Seqptick_projs strict_ticks_of_def append_eq_map_conv
          append_eq_append_conv2 Cons_eq_append_conv elim!: ticks_of_memE)
        (blast, metis append_Nil)
  next
    show ‹s ∈ (⋃r∈✓s(P). ✓s(Q r)) ⟹ s ∈ ✓s(P ;✓ Q)› for s
      by (auto simp add: Seqptick_projs ticks_of_def elim!: strict_ticks_of_memE)
        (meson append.assoc append_T_imp_tickFree not_Cons_self2)
  qed
qed


lemma ‹✓s(P ;✓ Q) ⊆ ⋃ {✓s(Q r) |r. r ∈ ✓s(P)}›
  ― ‹Already proven earlier in the construction.›
  by (fact strict_ticks_of_Seqptick_subset)




section ‹Synchronization Product›

subsection ‹Events›

lemma (in Syncptick_locale) events_of_Syncptick_subset : ‹α(P ⟦S⟧✓ Q) ⊆ α(P) ∪ α(Q)›
  by (subst events_of_def, simp add: T_Syncptick subset_iff)
    (metis UNIV_I empty_iff events_of_is_strict_events_of_or_UNIV
      events_of_memI setinterleavesptick_preserves_ev_notin_set)

lemma (in Syncptick_locale) events_of_Interptick: ‹α(P |||✓ Q) = α(P) ∪ α(Q)›
proof (rule subset_antisym[OF events_of_Syncptick_subset])
  show ‹α(P) ∪ α(Q) ⊆ α(P |||✓ Q)›
  proof (rule subsetI, elim UnE)
    fix a assume ‹a ∈ α(P)›
    then obtain t_P where ‹tF t_P› ‹ev a ∈ set t_P› ‹t_P ∈ 𝒯 P›
      by (meson events_of_memE_optimized_tickFree)
    have ‹map ev (map of_ev t_P) setinterleaves✓⇘tick_join⇙ ((t_P, []), {})›
      by (simp add: ‹tF t_P› setinterleavesptick_NilR_iff)
    hence ‹map ev (map of_ev t_P) ∈ 𝒯 (P |||✓ Q)›
      by (simp add: T_Syncptick) (metis ‹t_P ∈ 𝒯 P› is_processT1_TR)
    moreover from ‹ev a ∈ set t_P› have ‹ev a ∈ set (map ev (map of_ev t_P))› by force
    ultimately show ‹a ∈ α(P |||✓ Q)› by (metis events_of_memI)
  next
    fix a assume ‹a ∈ α(Q)›
    then obtain t_Q where ‹tF t_Q› ‹ev a ∈ set t_Q› ‹t_Q ∈ 𝒯 Q›
      by (meson events_of_memE_optimized_tickFree)
    have ‹map ev (map of_ev t_Q) setinterleaves✓⇘tick_join⇙ (([], t_Q), {})›
      by (simp add: ‹tF t_Q› setinterleavesptick_NilL_iff)
    hence ‹map ev (map of_ev t_Q) ∈ 𝒯 (P |||✓ Q)›
      by (simp add: T_Syncptick) (metis ‹t_Q ∈ 𝒯 Q› is_processT1_TR)
    moreover from ‹ev a ∈ set t_Q› have ‹ev a ∈ set (map ev (map of_ev t_Q))› by force
    ultimately show ‹a ∈ α(P |||✓ Q)› by (metis events_of_memI)
  qed
qed


lemma (in Syncptick_locale) strict_events_of_Syncptick_subset :
  ‹α(P ⟦S⟧✓ Q) ⊆ α(P) ∪ α(Q)›
proof (rule subsetI)
  fix a assume ‹a ∈ α(P ⟦S⟧✓ Q)›
  then obtain t where ‹t ∈ 𝒯 (P ⟦S⟧✓ Q)› ‹ev a ∈ set t› ‹tF t› ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)›
    by (blast elim: strict_events_of_memE_optimized_tickFree)
  from ‹t ∈ 𝒯 (P ⟦S⟧✓ Q)› ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)›
  obtain t_P t_Q where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
    and setinter : ‹t setinterleaves✓⇘tick_join⇙ ((t_P, t_Q), S)›
    unfolding Syncptick_projs by blast
  from this(3) setinterleavesptick_preserves_ev_notin_set ‹ev a ∈ set t›
  have ‹ev a ∈ set t_P ∨ ev a ∈ set t_Q› by metis
  moreover have ‹t_P ∉ 𝒟 P ∧ t_Q ∉ 𝒟 Q›
  proof (rule ccontr)
    assume ‹¬ (t_P ∉ 𝒟 P ∧ t_Q ∉ 𝒟 Q)›
    with ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› ‹tF t› front_tickFree_Nil setinter
    have ‹t ∈ 𝒟 (P ⟦S⟧✓ Q)› unfolding D_Syncptick by blast
    with ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)› show False ..
  qed
  ultimately show ‹a ∈ α(P) ∪ α(Q)›
    by (meson UnCI ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› strict_events_of_memI)
qed



subsection ‹Ticks›

lemma (in Syncptick_locale)
  ‹✓s(P ⟦S⟧✓ Q) ⊆ {r_s |r_s r s. r ⊗✓ s = Some r_s ∧ r ∈ ✓s(P) ∧ s ∈ ✓s(Q)}›
  ― ‹Already proven earlier in the construction.›
  by (fact strict_ticks_of_Syncptick_subset)

lemma (in Syncptick_locale) ticks_of_no_div_Syncptick_subset :
  ‹𝒟 (P ⟦S⟧✓ Q) = {} ⟹
   ✓s(P ⟦S⟧✓ Q) ⊆ {r_s |r_s r s. tick_join r s = Some r_s ∧ r ∈ ✓s(P) ∧ s ∈ ✓s(Q)}›
  using strict_ticks_of_Syncptick_subset
  by (simp add: ticks_of_is_strict_ticks_of_or_UNIV subset_iff) blast



section ‹Architectural Operators›

subsection ‹Events›

lemma events_of_MultiSeq_subset :
  (* Should be in HOL-CSPM *)
  ‹α(SEQ l ∈@ L. P l) ⊆ (⋃l ∈ set L. ⋃r. α(P l))›
  by (induct L rule: rev_induct)
    (auto intro!: subset_trans[OF events_of_Seq_subset])

lemma events_of_MultiSeqptick_subset :
  ‹α((SEQ✓ l ∈@ L. P l) r) ⊆ (⋃l ∈ set L. ⋃r. α(P l r))›
  by (induct L arbitrary: r)
    (auto intro!: subset_trans[OF events_of_Seqptick_subset])

lemma strict_events_of_MultiSeq_subset :
  (* Should be in HOL-CSPM *)
  ‹α(SEQ l ∈@ L. P l) ⊆ (⋃l ∈ set L. ⋃r. α(P l))›
  by (induct L rule: rev_induct)
    (auto intro!: subset_trans[OF strict_events_of_Seq_subseteq]
      split: if_split_asm)

lemma strict_events_of_MultiSeqptick_subset :
  ‹α((SEQ✓ l ∈@ L. P l) r) ⊆ (⋃l ∈ set L. ⋃r. α(P l r))›
  by (induct L arbitrary: r, simp)
    (auto intro!: subset_trans[OF strict_events_of_Seqptick_subset])



lemma events_of_MultiSyncptick_subset :
  ‹α(⟦S⟧✓ l ∈@ L. P l) ⊆ (⋃l ∈ set L. α(P l))›
  by (induct L rule: induct_list012, simp_all)
    (metis eq_id_iff events_of_Renaming order.order_iff_strict
      image_id events_of_is_strict_events_of_or_UNIV, 
      use SyncRlist.events_of_Syncptick_subset in fastforce)

lemma events_of_MultiInterptick :
  ‹α(|||✓ l ∈@ L. P l) = (⋃l ∈ set L. α(P l))›
  by (induct L rule: induct_list012,
      simp_all add: SyncRlist.events_of_Interptick)
    (metis events_of_Renaming events_of_is_strict_events_of_or_UNIV id_apply image_id)

lemma strict_events_of_MultiSyncptick_subset : 
  ‹α(⟦S⟧✓ l ∈@ L. P l) ⊆ (⋃l ∈ set L. α(P l))›
  by (induct L rule: induct_list012, simp_all add: strict_events_of_inj_on_Renaming)
    (use SyncRlist.strict_events_of_Syncptick_subset in fastforce)



subsection ‹Ticks›

text ‹
We only look at const‹strict_ticks_of› lemmas: const‹ticks_of› is harder
to deal with because it requires more control on the divergences. 
›

lemma strict_ticks_of_MultiSeqptick_subset :
  ‹✓s((SEQ✓ l ∈@ L. P l) r) ⊆ (if L = [] then {r} else (⋃r. ✓s(P (last L) r)))›
proof (induct L arbitrary: r)
  case Nil show ?case by simp
next
  case (Cons l L)
  have ‹(SEQ✓ m ∈@ (l # L). P m) r = P l r ;✓ SEQ✓ l ∈@ L. P l› by simp
  also have ‹✓s(…) ⊆ ⋃ {✓s((SEQ✓ l ∈@ L. P l) r') |r'. r' ∈ ✓s(P l r)}›
    by (fact strict_ticks_of_Seqptick_subset)
  also have ‹… ⊆ ⋃ {if L = [] then {r'} else ⋃r. ✓s(P (last L) r) |r'. r' ∈ ✓s(P l r)}›
    using Cons.hyps by (blast intro: Union_subsetI)
  also have ‹… ⊆ (if l # L = [] then {r} else ⋃r. ✓s(P (last (l # L)) r))› by auto
  finally show ?case .
qed

lemma strict_ticks_of_MultiSeq_subset :
  ‹✓s(SEQ l ∈@ L. P l) ⊆ (if L = [] then {undefined} else (⋃r. ✓s(P (last L))))›
  using strict_ticks_of_MultiSeqptick_subset[of L ‹λl r. P l›]
  unfolding MultiSeqptick_const by auto



lemma strict_ticks_of_MultiSyncptick_subset : 
  ‹✓s(⟦S⟧✓ l ∈@ L. P l) ⊆
   {l. length l = length L ∧ (∀i < length L. l ! i ∈ ✓s(P (L ! i)))}›
proof (induct L rule: induct_list012)
  case 1 show ?case by simp
next
  case (2 l0) show ?case
    by (auto intro!: subset_trans[OF strict_ticks_of_RenamingTick_subset])
next
  case (3 l0 l1 L)
  have ‹⟦S⟧✓ l ∈@ (l0 # l1 # L). P l = P l0 ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l1 # L). P l› by simp
  also have ‹✓s(…) ⊆ {r # s |r s. r ∈ ✓s(P l0) ∧ s ∈ ✓s(⟦S⟧✓ l ∈@ (l1 # L). P l)}›
    by (rule subset_trans[OF SyncRlist.strict_ticks_of_Syncptick_subset]) blast
  also have ‹… ⊆
    {r # s |r s. r ∈ ✓s(P l0) ∧
                 s ∈ {l. length l = length (l1 # L) ∧
                          (∀i<length (l1 # L). l ! i ∈ ✓s(P ((l1 # L) ! i)))}}›
    using "3.hyps"(2) by blast
  also have ‹… = {l. length l = length (l0 # l1 # L) ∧
                      (∀i<length (l0 # l1 # L). l ! i ∈ ✓s(P ((l0 # l1 # L) ! i)))}›
    (is ‹?S1 = ?S2›)
  proof (unfold set_eq_iff, intro allI)
    show ‹l ∈ ?S1 ⟷ l ∈ ?S2› for l
      by (cases l, auto, metis less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc)
  qed
  finally show ?case .
qed


(*<*)
end
  (*>*)