Theory Combining_Synchronization_Product_Generalized

(***********************************************************************************
 * 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
 ***********************************************************************************)


chapter ‹Combining Automata for Generalized Synchronization Product›

(*<*)
theory Combining_Synchronization_Product_Generalized
  imports Combining_Synchronization_Product
begin
  (*>*)


section ‹Definitions›

subsection ‹Specializations›

definition combinedPairlist_Syncptick ::
  ‹[('σ, 'e, 'r, 'α) Ad_scheme, 'e set, ('σ, 'e, 'r, 'β) Ad_scheme] ⇒ ('σ list, 'e, 'r list) Ad›
  where ‹combinedPairlist_Syncptick A0 E A1 ≡
         combined_Sync A0 E A1 hd (λσs. hd (tl σs)) (λs t. [s, t]) (λs t. ⌊[s, t]⌋)›
definition combinendPairlist_Syncptick ::
  ‹[('σ, 'e, 'r, 'α) And_scheme, 'e set, ('σ, 'e, 'r, 'β) And_scheme] ⇒ ('σ list, 'e, 'r list) And›
  where ‹combinendPairlist_Syncptick A0 E A1 ≡ combinend_Sync A0 E A1 hd (λσs. hd (tl σs)) (λs t. [s, t]) (λs t. ⌊[s, t]⌋)›

definition combinedPair_Syncptick ::
  ‹[('σ0, 'e, 'r0, 'α) Ad_scheme, 'e set, ('σ1, 'e, 'r1, 'β) Ad_scheme] ⇒ ('σ0 × 'σ1, 'e, 'r0 × 'r1) Ad›
  where ‹combinedPair_Syncptick A0 E A1 ≡ combined_Sync A0 E A1 fst snd Pair (λs r. ⌊(s, r)⌋)›
definition combinendPair_Syncptick ::
  ‹[('σ0, 'e, 'r0, 'α) And_scheme, 'e set, ('σ1, 'e, 'r1, 'β) And_scheme] ⇒ ('σ0 × 'σ1, 'e, 'r0 × 'r1) And›
  where ‹combinendPair_Syncptick A0 E A1 ≡ combinend_Sync A0 E A1 fst snd Pair (λs r. ⌊(s, r)⌋)›

definition combinedListslenL_Syncptick ::
  ‹[('σ list, 'e, 'r list, 'α) Ad_scheme, nat, 'e set, ('σ list, 'e, 'r list, 'β) Ad_scheme] ⇒ ('σ list, 'e, 'r list) Ad›
  where ‹combinedListslenL_Syncptick A0 len0 E A1 ≡ combined_Sync A0 E A1 (take len0) (drop len0) (@) (λs r. ⌊s @ r⌋)›
definition combinendListslenL_Syncptick ::
  ‹[('σ list, 'e, 'r list, 'α) And_scheme, nat, 'e set, ('σ list, 'e, 'r list, 'β) And_scheme] ⇒ ('σ list, 'e, 'r list) And›
  where ‹combinendListslenL_Syncptick A0 len0 E A1 ≡ combinend_Sync A0 E A1 (take len0) (drop len0) (@) (λs r. ⌊s @ r⌋)›

definition combinedRlist_Syncptick ::
  ‹[('σ, 'e, 'r, 'α) Ad_scheme, 'e set, ('σ list, 'e, 'r list, 'β) Ad_scheme] ⇒ ('σ list, 'e, 'r list) Ad›
  where ‹combinedRlist_Syncptick A0 E A1 ≡ combined_Sync A0 E A1 hd tl (#) (λs r. ⌊s # r⌋)›
definition combinendRlist_Syncptick ::
  ‹[('σ, 'e, 'r, 'α) And_scheme, 'e set, ('σ list, 'e, 'r list, 'β) And_scheme] ⇒ ('σ list, 'e, 'r list) And›
  where ‹combinendRlist_Syncptick A0 E A1 ≡ combinend_Sync A0 E A1 hd tl (#) (λs r. ⌊s # r⌋)›

lemmas combinePairlist_Syncptick_defs = combinedPairlist_Syncptick_def combinendPairlist_Syncptick_def
  and combinePair_Syncptick_defs = combinedPair_Syncptick_def combinendPair_Syncptick_def
  and combineListslenL_Syncptick_defs = combinedListslenL_Syncptick_def combinendListslenL_Syncptick_def
  and combineRlist_Syncptick_defs = combinedRlist_Syncptick_def combinendRlist_Syncptick_def

lemmas combine_Syncptick_defs =
  combinePairlist_Syncptick_defs combinePair_Syncptick_defs combineListslenL_Syncptick_defs combineRlist_Syncptick_defs


bundle combinend_Syncptick_syntax begin

notation combinedPairlist_Syncptick (‹⟪_ d⊗⟦_⟧✓Pairlist _⟫› [0, 0, 0])
notation combinendPairlist_Syncptick (‹⟪_ nd⊗⟦_⟧✓Pairlist _⟫› [0, 0, 0])
notation combinedPair_Syncptick (‹⟪_ d⊗⟦_⟧✓Pair _⟫› [0, 0, 0])
notation combinendPair_Syncptick (‹⟪_ nd⊗⟦_⟧✓Pair _⟫› [0, 0, 0])
notation combinedListslenL_Syncptick (‹⟪_ d⊗⟦_, _⟧✓ListslenL _⟫› [0, 0, 0, 0])
notation combinendListslenL_Syncptick (‹⟪_ nd⊗⟦_, _⟧✓ListslenL _⟫› [0, 0, 0, 0])
notation combinedRlist_Syncptick (‹⟪_ d⊗⟦_⟧✓Rlist _⟫› [0, 0, 0])
notation combinendRlist_Syncptick (‹⟪_ nd⊗⟦_⟧✓Rlist _⟫› [0, 0, 0])

end

unbundle combinend_Syncptick_syntax



section ‹First Properties›

lemma finite_trans_combinend_Syncptick_simps [simp] : 
  ‹finite_trans A0 ⟹ finite_trans A1 ⟹ finite_trans ⟪A0 nd⊗⟦E⟧✓Pairlist A1⟫›
  ‹finite_trans B0 ⟹ finite_trans B1 ⟹ finite_trans ⟪B0 nd⊗⟦E⟧✓Pair B1⟫›
  ‹finite_trans C0 ⟹ finite_trans C1 ⟹ finite_trans ⟪C0 nd⊗⟦len0, E⟧✓ListslenL C1⟫›
  ‹finite_trans D0 ⟹ finite_trans D1 ⟹ finite_trans ⟪D0 nd⊗⟦E⟧✓Rlist D1⟫›
  unfolding combinendPairlist_Syncptick_def combinendPair_Syncptick_def combinendListslenL_Syncptick_def combinendRlist_Syncptick_def 
  by (simp_all add: finite_trans_def finite_image_set2)

lemma ε_combinePairlist_Syncptick:
  ‹ε ⟪A0 d⊗⟦E⟧✓Pairlist A1⟫ σs = combine_Sync_ε A0 E A1 hd (hd ∘ tl) σs›
  ‹ε ⟪B0 nd⊗⟦E⟧✓Pairlist B1⟫ σs = combine_Sync_ε B0 E B1 hd (hd ∘ tl) σs›
  by (auto simp add: combine_Sync_ε_def_bis combinePairlist_Syncptick_defs ε_simps)

lemma ε_combinePair_Syncptick:
  ‹ε ⟪A0 d⊗⟦E⟧✓Pair A1⟫ σs = combine_Sync_ε A0 E A1 fst snd σs›
  ‹ε ⟪B0 nd⊗⟦E⟧✓Pair B1⟫ σs = combine_Sync_ε B0 E B1 fst snd σs›
  by (auto simp add: combine_Sync_ε_def_bis combinePair_Syncptick_defs ε_simps)

lemma ε_combineListslenL_Syncptick: 
  ‹ε ⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫ σs = combine_Sync_ε A0 E A1 (take len0) (drop len0) σs›
  ‹ε ⟪B0 nd⊗⟦len0, E⟧✓ListslenL B1⟫ σs = combine_Sync_ε B0 E B1 (take len0) (drop len0) σs›
  by (auto simp add: combine_Sync_ε_def_bis combineListslenL_Syncptick_defs ε_simps)

lemma ε_combineRlist_Syncptick:
  ‹ε ⟪A0 d⊗⟦E⟧✓Rlist A1⟫ σs = combine_Sync_ε A0 E A1 hd tl σs›
  ‹ε ⟪B0 nd⊗⟦E⟧✓Rlist B1⟫ σs = combine_Sync_ε B0 E B1 hd tl σs›
  by (auto simp add: combine_Sync_ε_def_bis combineRlist_Syncptick_defs ε_simps)


lemma ρ_combinePairlist_Syncptick:
  ‹ρ ⟪A0 d⊗⟦E⟧✓Pairlist A1⟫ = {σs. hd σs ∈ ρ A0 ∧ hd (tl σs) ∈ ρ A1}›
  ‹ρ ⟪B0 nd⊗⟦E⟧✓Pairlist B1⟫ = {σs. hd σs ∈ ρ B0 ∧ hd (tl σs) ∈ ρ B1}›
  by (auto simp add: combinePairlist_Syncptick_defs ρ_simps split: option.split)

lemma ρ_combinePair_Syncptick:
  ‹ρ ⟪A0 d⊗⟦E⟧✓Pair A1⟫ = {(σ0, σ1). σ0 ∈ ρ A0 ∧ σ1 ∈ ρ A1}›
  ‹ρ ⟪B0 nd⊗⟦E⟧✓Pair B1⟫ = {(σ0, σ1). σ0 ∈ ρ B0 ∧ σ1 ∈ ρ B1}›
  by (auto simp add: combinePair_Syncptick_defs ρ_simps split: option.split)

lemma ρ_combineListslenL_Syncptick: 
  ‹ρ ⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫ = {σs. take len0 σs ∈ ρ A0 ∧ drop len0 σs ∈ ρ A1}›
  ‹ρ ⟪B0 nd⊗⟦len0, E⟧✓ListslenL B1⟫ = {σs. take len0 σs ∈ ρ B0 ∧ drop len0 σs ∈ ρ B1}›
  by (auto simp add: combineListslenL_Syncptick_defs ρ_simps split: option.split)

lemma ρ_combineRlist_Syncptick:
  ‹ρ ⟪A0 d⊗⟦E⟧✓Rlist A1⟫ = {σs. hd σs ∈ ρ A0 ∧ tl σs ∈ ρ A1}›
  ‹ρ ⟪B0 nd⊗⟦E⟧✓Rlist B1⟫ = {σs. hd σs ∈ ρ B0 ∧ tl σs ∈ ρ B1}›
  by (auto simp add: combineRlist_Syncptick_defs ρ_simps split: option.split)



section ‹Transitions are unchanged in the Generalization›

text ‹
In the generalization, only the const‹ω› function is modified.
›

lemma τ_combinePairlist_Syncptick :
  ‹τ ⟪A0 d⊗⟦E⟧✓Pairlist A1⟫ = τ ⟪A0 d⊗⟦E⟧Pairlist A1⟫›
  ‹τ ⟪B0 nd⊗⟦E⟧✓Pairlist B1⟫ = τ ⟪B0 nd⊗⟦E⟧Pairlist B1⟫›
  by (simp_all add: combine_Sync_defs combine_Syncptick_defs)

lemma τ_combinePair_Syncptick :
  ‹τ ⟪A0 d⊗⟦E⟧✓Pair A1⟫ = τ ⟪A0 d⊗⟦E⟧Pair A1⟫›
  ‹τ ⟪B0 nd⊗⟦E⟧✓Pair B1⟫ = τ ⟪B0 nd⊗⟦E⟧Pair B1⟫›
  by (simp_all add: combine_Sync_defs combine_Syncptick_defs)

lemma τ_combineListslenL_Syncptick :
  ‹τ ⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫ = τ ⟪A0 d⊗⟦len0, E⟧ListslenL A1⟫›
  ‹τ ⟪B0 nd⊗⟦len0, E⟧✓ListslenL B1⟫ = τ ⟪B0 nd⊗⟦len0, E⟧ListslenL B1⟫›
  by (simp_all add: combine_Sync_defs combine_Syncptick_defs)

text ‹
term‹τ ⟪A0 d⊗⟦E⟧✓Rlist A1⟫› and term‹τ ⟪B0 nd⊗⟦E⟧✓Rlist B1⟫›
cannot be obtained that easily because of the types of terminations.›



section ‹Reachability›

lemma ℛd_combinedListslenL_Syncptick_subset: 
  ‹ℛd ⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫ (s0 @ s1) ⊆ {t0 @ t1| t0 t1. t0 ∈ ℛd A0 s0 ∧ t1 ∈ ℛd A1 s1}› (is ‹?SA ⊆ _›)
  if ‹⋀t0. t0 ∈ ℛd A0 s0 ⟹ length t0 = len0›
  by (subst same_τ_implies_same_ℛd[of _ _ ‹⟪A0 d⊗⟦len0, E⟧ListslenL A1⟫›])
    (simp_all add: τ_combineListslenL_Syncptick ℛd_combinedListslenL_Sync_subset that)

lemma ℛnd_combinendListslenL_Syncptick_subset: 
  ‹ℛnd ⟪B0 nd⊗⟦len0, E⟧✓ListslenL B1⟫ (s0 @ s1) ⊆ {t0 @ t1| t0 t1. t0 ∈ ℛnd B0 s0 ∧ t1 ∈ ℛnd B1 s1}› (is ‹?SB ⊆ _›)
  if ‹⋀t0. t0 ∈ ℛnd B0 s0 ⟹ length t0 = len0›
  by (subst same_τ_implies_same_ℛnd[of _ _ ‹⟪B0 nd⊗⟦len0, E⟧ListslenL B1⟫›])
    (simp_all add: τ_combineListslenL_Syncptick ℛnd_combinendListslenL_Sync_subset that)


lemma ℛd_combinedPairlist_Syncptick_subset:
  ‹ℛd ⟪A0 d⊗⟦E⟧✓Pairlist A1⟫ [s0, s1] ⊆ {[t0, t1]| t0 t1. t0 ∈ ℛd A0 s0 ∧ t1 ∈ ℛd A1 s1}› (is ‹?SA ⊆ _›)
  and ℛnd_combinendPairlist_Syncptick_subset:
  ‹ℛnd ⟪B0 nd⊗⟦E⟧✓Pairlist B1⟫ [s0, s1] ⊆ {[t0, t1]| t0 t1. t0 ∈ ℛnd B0 s0 ∧ t1 ∈ ℛnd B1 s1}› (is ‹?SB ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = [t0, t1] ∧ t0 ∈ ℛd A0 s0 ∧ t1 ∈ ℛd A1 s1› for t
    by (ℛd_subset_method defs: combinePairlist_Syncptick_defs)
  show ‹t ∈ ?SB ⟹ ∃t0 t1. t = [t0, t1] ∧ t0 ∈ ℛnd B0 s0 ∧ t1 ∈ ℛnd B1 s1› for t
    by (ℛnd_subset_method defs: combinePairlist_Syncptick_defs)
qed

lemma ℛd_combinedPair_Syncptick_subset:
  ‹ℛd ⟪A0 d⊗⟦E⟧✓Pair A1⟫ (s0, s1) ⊆ ℛd A0 s0 × ℛd A1 s1› (is ‹?SA ⊆ _›)
  and ℛnd_combinendPair_Syncptick_subset:
  ‹ℛnd ⟪B0 nd⊗⟦E⟧✓Pair B1⟫ (s0, s1) ⊆ ℛnd B0 s0 × ℛnd B1 s1› (is ‹?SB ⊆ _›)
proof -
  have ‹t ∈ ?SA ⟹ fst t ∈ ℛd A0 s0 ∧ snd t ∈ ℛd A1 s1› for t 
    by (ℛd_subset_method defs: combinePair_Syncptick_defs)
  thus ‹?SA ⊆ ℛd A0 s0 × ℛd A1 s1› by force
next
  have ‹t ∈ ?SB ⟹ fst t ∈ ℛnd B0 s0 ∧ snd t ∈ ℛnd B1 s1› for t
    by (ℛnd_subset_method defs: combinePair_Syncptick_defs)
  thus ‹?SB ⊆ ℛnd B0 s0 × ℛnd B1 s1› by force
qed


lemma ℛd_combinedRlist_Syncptick_subset:
  ‹ℛd ⟪A0 d⊗⟦E⟧✓Rlist A1⟫ (s0 # σs) ⊆ {t0 # σt| t0 σt. t0 ∈ ℛd A0 s0 ∧ σt ∈ ℛd A1 σs}› (is ‹?SA ⊆ _›)
  and ℛnd_combinendRlist_Syncptick_subset: 
  ‹ℛnd ⟪B0 nd⊗⟦E⟧✓Rlist B1⟫ (s0 # σs) ⊆ {t0 # σt| t0 σt. t0 ∈ ℛnd B0 s0 ∧ σt ∈ ℛnd B1 σs}› (is ‹?SB ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 σt. t = t0 # σt ∧ t0 ∈ ℛd A0 s0 ∧ σt ∈ ℛd A1 σs› for t
    by (ℛd_subset_method defs: combineRlist_Syncptick_defs)
next
  show ‹t ∈ ?SB ⟹ ∃t0 σt. t = t0 # σt ∧ t0 ∈ ℛnd B0 s0 ∧ σt ∈ ℛnd B1 σs› for t
    by (ℛnd_subset_method defs: combineRlist_Syncptick_defs)
qed



section ‹Normalization› 


lemma ω_combinePairlist_Syncptick_behaviour:
  ‹ω ⟪⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⟫d↪nd [s0, s1] = ω ⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pairlist ⟪A1⟫d↪nd⟫ [s0, s1]›
  by (simp add: combinePairlist_Syncptick_defs det_ndet_conv_defs option.case_eq_if)

lemma ω_combinePair_Syncptick_behaviour:
  ‹ω ⟪⟪A0 d⊗⟦E⟧✓Pair A1⟫⟫d↪nd (s0, s1) = ω ⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pair ⟪A1⟫d↪nd⟫ (s0, s1)›
  by (simp add: combinePair_Syncptick_defs det_ndet_conv_defs option.case_eq_if)

lemma ω_combineListslenL_Syncptick_behaviour:
  ‹ω ⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⟫d↪nd (σs0 @ σs1) = ω ⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧✓ListslenL ⟪A1⟫d↪nd⟫ (σs0 @ σs1)›
  by (simp add: combineListslenL_Syncptick_defs det_ndet_conv_defs option.case_eq_if)

lemma ω_combineRlist_Syncptick_behaviour:
  ‹ω ⟪⟪A0 d⊗⟦E⟧✓Rlist A1⟫⟫d↪nd (s0 # σs1) = ω ⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Rlist ⟪A1⟫d↪nd⟫ (s0 # σs1)›
  by (simp add: combineRlist_Syncptick_defs det_ndet_conv_defs option.case_eq_if)


lemma τ_combinePairlist_Syncptick_behaviour_when_indep:
  ‹ε A0 s0 ∩ ε A1 s1 ⊆ E ⟹
   τ ⟪⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⟫d↪nd [s0, s1] e = τ ⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pairlist ⟪A1⟫d↪nd⟫ [s0, s1] e›
  by (auto simp add: combinePairlist_Syncptick_defs det_ndet_conv_defs option.case_eq_if ε_simps)

lemma τ_combinePair_Syncptick_behaviour_when_indep:
  ‹ε A0 s0 ∩ ε A1 s1 ⊆ E ⟹ 
   τ ⟪⟪A0 d⊗⟦E⟧✓Pair A1⟫⟫d↪nd (s0, s1) e = τ ⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pair ⟪A1⟫d↪nd⟫ (s0, s1) e›
  by (auto simp add: combinePair_Syncptick_defs det_ndet_conv_defs option.case_eq_if ε_simps)

lemma τ_combineListslenL_Syncptick_behaviour_when_indep:
  ‹ε A0 σs0 ∩ ε A1 σs1 ⊆ E ⟹ length σs0 = len0 ⟹ 
   τ ⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⟫d↪nd (σs0 @ σs1) e = τ ⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧✓ListslenL ⟪A1⟫d↪nd⟫ (σs0 @ σs1) e›
  by (auto simp add: combineListslenL_Syncptick_defs det_ndet_conv_defs option.case_eq_if ε_simps)

lemma τ_combineRlist_Syncptick_behaviour_when_indep:
  ‹ε A0 s0 ∩ ε A1 σs1 ⊆ E ⟹
   τ ⟪⟪A0 d⊗⟦E⟧✓Rlist A1⟫⟫d↪nd (s0 # σs1) e = τ ⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Rlist ⟪A1⟫d↪nd⟫ (s0 # σs1) e›
  by (auto simp add: combineRlist_Syncptick_defs det_ndet_conv_defs option.case_eq_if ε_simps)



lemma PSKIPS_combinePairlist_Syncptick_behaviour_when_indep:
  ‹PSKIPS⟪⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⟫d [s0, s1] = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pairlist ⟪A1⟫d↪nd⟫⟫nd [s0, s1]›
  if ‹indep_enabl A0 s0 E A1 s1›
  by (PSKIPS_when_indep_method R_d_subset: ℛd_combinedPairlist_Syncptick_subset, simp_all)
    (metis τ_combinePairlist_Syncptick_behaviour_when_indep indep_enablD that,
      metis ω_combinePairlist_Syncptick_behaviour)

lemma P_combinePairlist_Syncptick_behaviour_when_indep:
  ‹P⟪⟪A0 d⊗⟦E⟧✓Pairlist A1⟫⟫d [s0, s1] = P⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pairlist ⟪A1⟫d↪nd⟫⟫nd [s0, s1]›
  if ‹indep_enabl A0 s0 E A1 s1›
  by (P_when_indep_method R_d_subset: ℛd_combinedPairlist_Syncptick_subset, simp_all)
    (metis τ_combinePairlist_Syncptick_behaviour_when_indep indep_enablD that)


lemma PSKIPS_combinePair_Syncptick_behaviour_when_indep:
  ‹PSKIPS⟪⟪A0 d⊗⟦E⟧✓Pair A1⟫⟫d (s0, s1) = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pair ⟪A1⟫d↪nd⟫⟫nd (s0, s1)›
  if ‹indep_enabl A0 s0 E A1 s1›
  by (PSKIPS_when_indep_method R_d_subset: ℛd_combinedPair_Syncptick_subset, all ‹elim SigmaE›)
    (metis τ_combinePair_Syncptick_behaviour_when_indep indep_enablD that,
      auto simp add: ω_combinePair_Syncptick_behaviour option.case_eq_if)

lemma P_combinePair_Syncptick_behaviour_when_indep:
  ‹P⟪⟪A0 d⊗⟦E⟧✓Pair A1⟫⟫d (s0, s1) = P⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Pair ⟪A1⟫d↪nd⟫⟫nd (s0, s1)›
  if ‹indep_enabl A0 s0 E A1 s1›
  by (P_when_indep_method R_d_subset: ℛd_combinedPair_Syncptick_subset, elim SigmaE)
    (metis τ_combinePair_Syncptick_behaviour_when_indep indep_enablD that)


lemma PSKIPS_combineListslenL_Syncptick_behaviour_when_indep:
  ‹PSKIPS⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⟫d (σs0 @ σs1) = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧✓ListslenL ⟪A1⟫d↪nd⟫⟫nd (σs0 @ σs1)› 
  if ‹indep_enabl A0 σs0 E A1 σs1› and ‹⋀σt0. σt0 ∈ ℛd A0 σs0 ⟹ length σt0 = len0›
  by (PSKIPS_when_indep_method R_d_subset: ℛd_combinedListslenL_Syncptick_subset, simp_all add: that(2))
    (metis τ_combineListslenL_Syncptick_behaviour_when_indep indep_enablD that,
      metis ω_combineListslenL_Syncptick_behaviour)

lemma P_combineListslenL_Syncptick_behaviour_when_indep:
  ‹P⟪⟪A0 d⊗⟦len0, E⟧✓ListslenL A1⟫⟫d (σs0 @ σs1) = P⟪⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧✓ListslenL ⟪A1⟫d↪nd⟫⟫nd (σs0 @ σs1)›
  if ‹indep_enabl A0 σs0 E A1 σs1› and ‹⋀σt0. σt0 ∈ ℛd A0 σs0 ⟹ length σt0 = len0›
  by (P_when_indep_method R_d_subset: ℛd_combinedListslenL_Syncptick_subset, simp_all add: that(2))
    (metis τ_combineListslenL_Syncptick_behaviour_when_indep indep_enablD that)


lemma PSKIPS_combineRlist_Syncptick_behaviour_when_indep:
  ‹PSKIPS⟪⟪A0 d⊗⟦E⟧✓Rlist A1⟫⟫d (s0 # σs1) = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Rlist ⟪A1⟫d↪nd⟫⟫nd (s0 # σs1)›
  if ‹indep_enabl A0 s0 E A1 σs1›
  by (PSKIPS_when_indep_method R_d_subset: ℛd_combinedRlist_Syncptick_subset, simp_all)
    (metis τ_combineRlist_Syncptick_behaviour_when_indep indep_enablD that,
      metis ω_combineRlist_Syncptick_behaviour)

lemma P_combineRlist_Syncptick_behaviour_when_indep:
  ‹P⟪⟪A0 d⊗⟦E⟧✓Rlist A1⟫⟫d (s0 # σs1) = P⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧✓Rlist ⟪A1⟫d↪nd⟫⟫nd (s0 # σs1)›
  if ‹indep_enabl A0 s0 E A1 σs1›
  by (P_when_indep_method R_d_subset: ℛd_combinedRlist_Syncptick_subset, simp)
    (metis τ_combineRlist_Syncptick_behaviour_when_indep indep_enablD that)


(*<*)
end
  (*>*)