Theory Combining_Sequential_Composition_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 Sequential Composition Generalized›

(*<*)
theory Combining_Sequential_Composition_Generalized 
  imports Process_Normalization
begin
  (*>*)


section ‹Definitions›

section ‹General Patterns›

definition combined_Seq_ε ::
  ‹[('σ0, 'a, 'r, 'α0) Ad_scheme, 'r ⇒ ('σ1, 'a, 's, 'α1) Ad_scheme, 'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'σ] ⇒ 'a set›
  where ‹combined_Seq_ε A0 A1 i0 i1 σs ≡
           if i0 σs ∈ ρ A0
         then   if i1 σs ∈ ρ (A1 ⌈ω A0 (i0 σs)⌉)
              then {}
              else ε (A1 ⌈ω A0 (i0 σs)⌉) (i1 σs)
         else ε A0 (i0 σs)›

definition combinend_Seq_ε ::
  ‹[('σ0, 'a, 'r, 'α0) And_scheme, 'r ⇒ ('σ1, 'a, 's, 'α1) And_scheme, 'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'σ] ⇒ 'a set›
  where ‹combinend_Seq_ε A0 A1 i0 i1 σs ≡
           if i0 σs ∈ ρ A0
         then   if i1 σs ∈ (⋃r∈ω A0 (i0 σs). ρ (A1 r))
              then {}
              else (⋃r ∈ ω A0 (i0 σs). ε (A1 r) (i1 σs))
         else ε A0 (i0 σs)›

lemmas combine_Seq_ε_defs = combined_Seq_ε_def combinend_Seq_ε_def


fun combined_Seq :: 
  ‹[('σ0, 'e, 'r, 'α0) Ad_scheme, 'r ⇒ ('σ1, 'e, 's, 'α1) Ad_scheme,
    'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'σ0 ⇒ 'σ1 ⇒ 'σ] ⇒ ('σ, 'e, 's) Ad›
  and combinend_Seq ::
  ‹[('σ0, 'e, 'r, 'α0) And_scheme, 'r ⇒ ('σ1, 'e, 's, 'α1) And_scheme,
     'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'σ0 ⇒ 'σ1 ⇒ 'σ] ⇒ ('σ, 'e, 's) And›
  where ‹combined_Seq A0 A1 i0 i1 f =
         ⦇τ = λσs e.  if i0 σs ∈ ρ A0
                    then   if i1 σs ∈ ρ (A1 ⌈ω A0 (i0 σs)⌉)
                         then ◇
                          else update_right (A1 ⌈ω A0 (i0 σs)⌉) (i0 σs) (i1 σs) e (f_up_opt f) (λσ. ⌊σ⌋)
                    else update_left  A0 (i0 σs) (i1 σs) e (f_up_opt f) (λσ. ⌊σ⌋),
          ω = λσs. case ω A0 (i0 σs) of ◇ ⇒ ◇ | ⌊r⌋ ⇒ ω (A1 r) (i1 σs)⦈›
  |     ‹combinend_Seq A0 A1 i0 i1 f = 
         ⦇τ = λσs e. if i0 σs ∈ ρ A0
                    then   if i1 σs ∈ (⋃r∈ω A0 (i0 σs). ρ (A1 r))
                         then {}
                         else (⋃r∈ω A0 (i0 σs). update_right (A1 r) (i0 σs) (i1 σs) e (f_up_set f) (λσ. {σ}))
                    else      update_left A0 (i0 σs) (i1 σs) e (f_up_set f) (λσ. {σ}),
          ω = λσs. ⋃r∈ω A0 (i0 σs). ω (A1 r) (i1 σs)⦈›



section ‹Specializations› 

definition combinedPairlist_Seqptick ::
  ‹[('σ, 'e, 'r, 'α) Ad_scheme, 'r ⇒ ('σ, 'e, 's, 'β) Ad_scheme] ⇒ ('σ list, 'e, 's) Ad›
  where ‹combinedPairlist_Seqptick A0 A1 ≡ combined_Seq A0 A1 hd (λσs. hd (tl σs)) (λs t. [s, t])›
definition combinendPairlist_Seqptick ::
  ‹[('σ, 'e, 'r, 'α) And_scheme, 'r ⇒ ('σ, 'e, 's, 'β) And_scheme] ⇒ ('σ list, 'e, 's) And› 
  where ‹combinendPairlist_Seqptick A0 A1 ≡ combinend_Seq A0 A1 hd (λσs. hd (tl σs)) (λs t. [s, t])›

definition combinedPair_Seqptick ::
  ‹[('σ0, 'e, 'r, 'α) Ad_scheme, 'r ⇒ ('σ1, 'e, 's, 'β) Ad_scheme] ⇒ ('σ0 × 'σ1, 'e, 's) Ad› 
  where ‹combinedPair_Seqptick A0 A1 ≡ combined_Seq A0 A1 fst snd Pair›
definition combinendPair_Seqptick ::
  ‹[('σ0, 'e, 'r, 'α) And_scheme, 'r ⇒ ('σ1, 'e, 's, 'β) And_scheme] ⇒ ('σ0 × 'σ1, 'e, 's) And› 
  where ‹combinendPair_Seqptick A0 A1 ≡ combinend_Seq A0 A1 fst snd Pair›

definition combinedListslenL_Seqptick ::
  ‹[('σ list, 'e, 'r, 'α) Ad_scheme, nat, 'r ⇒ ('σ list, 'e, 's, 'β) Ad_scheme] ⇒ ('σ list, 'e, 's) Ad› 
  where ‹combinedListslenL_Seqptick A0 len0 A1 ≡ combined_Seq A0 A1 (take len0) (drop len0) (@)›
definition combinendListslenL_Seqptick ::
  ‹[('σ list, 'e, 'r, 'α) And_scheme, nat, 'r ⇒ ('σ list, 'e, 's, 'β) And_scheme] ⇒ ('σ list, 'e, 's) And› 
  where ‹combinendListslenL_Seqptick A0 len0 A1 ≡ combinend_Seq A0 A1 (take len0) (drop len0) (@)›

definition combinedRlist_Seqptick ::
  ‹[('σ, 'e, 'r, 'α) Ad_scheme, 'r ⇒ ('σ list, 'e, 's, 'β) Ad_scheme] ⇒ ('σ list, 'e, 's) Ad› 
  where ‹combinedRlist_Seqptick A0 A1 ≡ combined_Seq A0 A1 hd tl (#)›
definition combinendRlist_Seqptick ::
  ‹[('σ, 'e, 'r, 'α) And_scheme, 'r ⇒ ('σ list, 'e, 's, 'β) And_scheme]  ⇒ ('σ list, 'e, 's) And› 
  where ‹combinendRlist_Seqptick A0 A1 ≡ combinend_Seq A0 A1 hd tl (#)›


lemmas combinePairlist_Seqptick_defs = combinedPairlist_Seqptick_def combinendPairlist_Seqptick_def
  and combinePair_Seqptick_defs = combinedPair_Seqptick_def combinendPair_Seqptick_def
  and combineListslenL_Seqptick = combinedListslenL_Seqptick_def combinendListslenL_Seqptick_def
  and combineRlist_Seqptick_defs = combinedRlist_Seqptick_def combinendRlist_Seqptick_def

lemmas combine_Seq_defs =
  combinePairlist_Seqptick_defs combinePair_Seqptick_defs combineListslenL_Seqptick combineRlist_Seqptick_defs


bundle combine_Seq_syntax begin

notation combinedPairlist_Seqptick (‹⟪_ d⊗;✓Pairlist _⟫› [0, 0])
notation combinendPairlist_Seqptick (‹⟪_ nd⊗;✓Pairlist _⟫› [0, 0])
notation combinedPair_Seqptick (‹⟪_ d⊗;✓Pair _⟫› [0, 0])
notation combinendPair_Seqptick (‹⟪_ nd⊗;✓Pair _⟫› [0, 0])
notation combinedListslenL_Seqptick (‹⟪_ d⊗_;ListslenL _⟫› [0, 0, 0])
notation combinendListslenL_Seqptick (‹⟪_ nd⊗_;ListslenL _⟫› [0, 0, 0])
notation combinedRlist_Seqptick (‹⟪_ d⊗;✓Rlist _⟫› [0, 0])
notation combinendRlist_Seqptick (‹⟪_ nd⊗;✓Rlist _⟫› [0, 0])

end


unbundle combine_Seq_syntax



section ‹First Properties›

lemma ε_combinePairlist_Seqptick :
  ‹ε ⟪A0 d⊗;✓Pairlist A1⟫ σs = combined_Seq_ε A0 A1 hd (hd ∘ tl) σs›
  ‹ε ⟪B0 nd⊗;✓Pairlist B1⟫ σs = combinend_Seq_ε B0 B1 hd (hd ∘ tl) σs›
  by (auto simp add: combine_Seq_ε_defs combinePairlist_Seqptick_defs
      ε_simps ρ_simps option.case_eq_if)

lemma ε_combinePair_Seqptick : 
  ‹ε ⟪A0 d⊗;✓Pair A1⟫ σs = combined_Seq_ε A0 A1 fst snd σs›
  ‹ε ⟪B0 nd⊗;✓Pair B1⟫ σs = combinend_Seq_ε B0 B1 fst snd σs›
  by (auto simp add: combine_Seq_ε_defs combinePair_Seqptick_defs
      ε_simps ρ_simps option.case_eq_if)

lemma ε_combineListslenL_Seqptick : 
  ‹ε ⟪A0 d⊗len0;ListslenL A1⟫ σs = combined_Seq_ε A0 A1 (take len0) (drop len0) σs›
  ‹ε ⟪B0 nd⊗len0;ListslenL B1⟫ σs = combinend_Seq_ε B0 B1 (take len0) (drop len0) σs›
  by (auto simp add: combine_Seq_ε_defs combineListslenL_Seqptick
      ε_simps ρ_simps option.case_eq_if)

lemma ε_combineRlist_Seqptick :
  ‹ε ⟪A0 d⊗;✓Rlist A1⟫ σs = combined_Seq_ε A0 A1 hd tl σs›
  ‹ε ⟪B0 nd⊗;✓Rlist B1⟫ σs = combinend_Seq_ε B0 B1 hd tl σs›
  by (auto simp add: combine_Seq_ε_defs combineRlist_Seqptick_defs
      ε_simps ρ_simps option.case_eq_if)



subsection ‹Reachability›

lemma ℛd_combinedListslenL_Seqptick_subset: 
  ‹ℛd ⟪A0 d⊗len0;ListslenL A1⟫ (s0 @ s1) ⊆ {t0 @ t1 |t0 t1. t0 ∈ ℛd A0 s0}› (is ‹?SA ⊆ _›)
  if same_length_ℛd: ‹⋀t0. t0 ∈ ℛd A0 s0 ⟹ length t0 = len0›
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = t0 @ t1 ∧ t0 ∈ ℛd A0 s0› for t
  proof (induct rule: ℛd.induct)
    case init show ?case by (metis ℛd.init)
  next
    case (step σ' σ'' a)
    from step.hyps(2) same_length_ℛd obtain t0 t1
      where ‹σ' = t0 @ t1› ‹t0 ∈ ℛd A0 s0› ‹length t0 = len0› by blast
    with step.hyps(3) show ?case
      by (auto simp add: combineListslenL_Seqptick map_option_case
          split: if_split_asm option.splits) (metis ℛd.step)
  qed
qed

lemma ℛnd_combinendListslenL_Seqptick_subset: 
  ‹ℛnd ⟪A0 nd⊗len0;ListslenL A1⟫ (s0 @ s1) ⊆ {t0 @ t1 |t0 t1. t0 ∈ ℛnd A0 s0}› (is ‹?SA ⊆ _›)
  if same_length_ℛnd: ‹⋀t0. t0 ∈ ℛnd A0 s0 ⟹ length t0 = len0›
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = t0 @ t1 ∧ t0 ∈ ℛnd A0 s0› for t
  proof (induct rule: ℛnd.induct)
    case init show ?case by (metis ℛnd.init)
  next
    case (step σ' σ'' a)
    from step.hyps(2) same_length_ℛnd obtain t0 t1
      where ‹σ' = t0 @ t1› ‹t0 ∈ ℛnd A0 s0› ‹length t0 = len0› by blast
    with step.hyps(3) show ?case
      by (auto simp add: combineListslenL_Seqptick split: if_split_asm) (metis ℛnd.step)
  qed
qed


lemma ℛd_combinedPairlist_Seqptick_subset: 
  ‹ℛd ⟪A0 d⊗;✓Pairlist A1⟫ [s0, s1] ⊆ {[t0, t1] |t0 t1. t0 ∈ ℛd A0 s0}› (is ‹?SA ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = [t0, t1] ∧ t0 ∈ ℛd A0 s0 › for t
  proof (induct rule: ℛd.induct)
    case init show ?case by (metis ℛd.init)
  next
    case (step σ' σ'' a)
    from step.hyps(2) obtain t0 t1 where ‹σ' = [t0, t1]› ‹t0 ∈ ℛd A0 s0› by blast
    with step.hyps(3) show ?case
      by (auto simp add: combinePairlist_Seqptick_defs map_option_case
          split: if_split_asm option.split_asm) (metis ℛd.step)
  qed
qed

lemma ℛnd_combinendPairlist_Seqptick_subset: 
  ‹ℛnd ⟪A0 nd⊗;✓Pairlist A1⟫ [s0, s1] ⊆ {[t0, t1] |t0 t1. t0 ∈ ℛnd A0 s0}› (is ‹?SA ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = [t0, t1] ∧ t0 ∈ ℛnd A0 s0 › for t
  proof (induct rule: ℛnd.induct)
    case init show ?case by (metis ℛnd.init)
  next
    case (step σ' σ'' a)
    from step.hyps(2) obtain t0 t1 where ‹σ' = [t0, t1]› ‹t0 ∈ ℛnd A0 s0› by blast
    with step.hyps(3) show ?case
      by (auto simp add: combinePairlist_Seqptick_defs split: if_split_asm) (metis ℛnd.step)
  qed
qed


lemma ℛd_combinedPair_Seqptick_subset: 
  ‹ℛd ⟪A0 d⊗;✓Pair A1⟫ (s0, s1) ⊆ {(t0, t1) |t0 t1. t0 ∈ ℛd A0 s0}› (is ‹?SA ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = (t0, t1) ∧ t0 ∈ ℛd A0 s0 › for t
  proof (induct rule: ℛd.induct)
    case init show ?case by (metis ℛd.init)
  next
    case (step σ' σ'' a)
    from step.hyps(2) obtain t0 t1 where ‹σ' = (t0, t1)› ‹t0 ∈ ℛd A0 s0› by blast
    with step.hyps(3) show ?case
      by (auto simp add: combinePair_Seqptick_defs map_option_case
          split: if_split_asm option.split_asm) (metis ℛd.step)
  qed
qed

lemma ℛnd_combinendPair_Seqptick_subset: 
  ‹ℛnd ⟪A0 nd⊗;✓Pair A1⟫ (s0, s1) ⊆ {(t0, t1) |t0 t1. t0 ∈ ℛnd A0 s0}› (is ‹?SA ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = (t0, t1) ∧ t0 ∈ ℛnd A0 s0 › for t
  proof (induct rule: ℛnd.induct)
    case init show ?case by (metis ℛnd.init)
  next
    case (step σ' σ'' a)
    from step.hyps(2) obtain t0 t1 where ‹σ' = (t0, t1)› ‹t0 ∈ ℛnd A0 s0› by blast
    with step.hyps(3) show ?case
      by (auto simp add: combinePair_Seqptick_defs split: if_split_asm) (metis ℛnd.step)
  qed
qed


lemma ℛd_combinedRlist_Seqptick_subset: 
  ‹ℛd ⟪A0 d⊗;✓Rlist A1⟫ (s0 # s1) ⊆ {t0 # t1 |t0 t1. t0 ∈ ℛd A0 s0}› (is ‹?SA ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = t0 # t1 ∧ t0 ∈ ℛd A0 s0 › for t
  proof (induct rule: ℛd.induct)
    case init show ?case by (metis ℛd.init)
  next
    case (step σ' σ'' a)
    from step.hyps(2) obtain t0 t1 where ‹σ' = t0 # t1› ‹t0 ∈ ℛd A0 s0› by blast
    with step.hyps(3) show ?case
      by (auto simp add: combineRlist_Seqptick_defs map_option_case
          split: if_split_asm option.split_asm) (metis ℛd.step)
  qed
qed

lemma ℛnd_combinendRlist_Seqptick_subset: 
  ‹ℛnd ⟪A0 nd⊗;✓Rlist A1⟫ (s0 # s1) ⊆ {t0 # t1 |t0 t1. t0 ∈ ℛnd A0 s0}› (is ‹?SA ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = t0 # t1 ∧ t0 ∈ ℛnd A0 s0 › for t
  proof (induct rule: ℛnd.induct)
    case init show ?case by (metis ℛnd.init)
  next
    case (step σ' σ'' a)
    from step.hyps(2) obtain t0 t1 where ‹σ' = t0 # t1› ‹t0 ∈ ℛnd A0 s0› by blast
    with step.hyps(3) show ?case
      by (auto simp add: combineRlist_Seqptick_defs split: if_split_asm) (metis ℛnd.step)
  qed
qed



section ‹Normalization› 

lemma τ_combinePairlist_Seqptick_behaviour:
  ‹τ ⟪⟪A0 d⊗;✓Pairlist A1⟫⟫d↪nd [s0, s1] e = τ ⟪⟪A0⟫d↪nd nd⊗;✓Pairlist (λr. ⟪A1 r⟫d↪nd)⟫ [s0, s1] e›
  by (auto simp add: combinePairlist_Seqptick_defs det_ndet_conv_defs option.case_eq_if ε_simps ρ_simps)

lemma τ_combinePair_Seqptick_behaviour:
  ‹τ ⟪⟪A0 d⊗;✓Pair A1⟫⟫d↪nd (s0, s1) e = τ ⟪⟪A0⟫d↪nd nd⊗;✓Pair (λr. ⟪A1 r⟫d↪nd)⟫ (s0, s1) e›
  by (auto simp add: combinePair_Seqptick_defs det_ndet_conv_defs option.case_eq_if ε_simps ρ_simps)

lemma τ_combineListslenL_Seqptick_behaviour:
  ‹τ ⟪⟪A0 d⊗len0;ListslenL A1⟫⟫d↪nd (σs0 @ σs1) e = τ ⟪⟪A0⟫d↪nd nd⊗len0;ListslenL (λr. ⟪A1 r⟫d↪nd)⟫ (σs0 @ σs1) e›
  by (auto simp add: combineListslenL_Seqptick det_ndet_conv_defs option.case_eq_if ε_simps ρ_simps)

lemma τ_combineRlist_Seqptick_behaviour:
  ‹τ ⟪⟪A0 d⊗;✓Rlist A1⟫⟫d↪nd (s0 # σs1) e = τ ⟪⟪A0⟫d↪nd nd⊗;✓Rlist (λr. ⟪A1 r⟫d↪nd)⟫ (s0 # σs1) e›
  by (auto simp add: combineRlist_Seqptick_defs det_ndet_conv_defs option.case_eq_if ε_simps ρ_simps)


text ‹Behaviour of normalisations›

lemma PSKIPS_combinePairlist_Seqptick_behaviour:
  ‹PSKIPS⟪⟪A0 d⊗;✓Pairlist A1⟫⟫d [s0, s1] = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗;✓Pairlist (λr. ⟪A1 r⟫d↪nd)⟫⟫nd [s0, s1]›
  by (fold PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d,
      rule PSKIPS_nd_eqI_strong_id, unfold ℛnd_from_det_to_ndet)
    (all ‹drule set_mp[OF ℛd_combinedPairlist_Seqptick_subset]›,
      auto simp add: combinePairlist_Seqptick_defs from_det_to_ndet_def ρ_simps split: option.split)

lemma P_combinePairlist_Seqptick_behaviour:
  ‹P⟪⟪A0 d⊗;✓Pairlist A1⟫⟫d [s0, s1] = P⟪⟪⟪A0⟫d↪nd nd⊗;✓Pairlist (λr. ⟪A1 r⟫d↪nd)⟫⟫nd [s0, s1]›
  by (fold P_nd_from_det_to_ndet_is_P_d,
      rule P_nd_eqI_strong_id, unfold ℛnd_from_det_to_ndet)
    (drule set_mp[OF ℛd_combinedPairlist_Seqptick_subset],
      auto simp add: combinePairlist_Seqptick_defs from_det_to_ndet_def ρ_simps split: option.split)


lemma PSKIPS_combinePair_Seqptick_behaviour:
  ‹PSKIPS⟪⟪A0 d⊗;✓Pair A1⟫⟫d (s0, s1) = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗;✓Pair (λr. ⟪A1 r⟫d↪nd)⟫⟫nd (s0, s1)›
  by (fold PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d,
      rule PSKIPS_nd_eqI_strong_id, unfold ℛnd_from_det_to_ndet)
    (all ‹drule set_mp[OF ℛd_combinedPair_Seqptick_subset]›,
      auto simp add: combinePair_Seqptick_defs from_det_to_ndet_def ρ_simps split: option.split)

lemma P_combinePair_Seqptick_behaviour:
  ‹P⟪⟪A0 d⊗;✓Pair A1⟫⟫d (s0, s1) = P⟪⟪⟪A0⟫d↪nd nd⊗;✓Pair (λr. ⟪A1 r⟫d↪nd)⟫⟫nd (s0, s1)›
  by (fold P_nd_from_det_to_ndet_is_P_d,
      rule P_nd_eqI_strong_id, unfold ℛnd_from_det_to_ndet)
    (drule set_mp[OF ℛd_combinedPair_Seqptick_subset],
      auto simp add: combinePair_Seqptick_defs from_det_to_ndet_def ρ_simps split: option.split)


lemma PSKIPS_combineRlist_Seqptick_behaviour:
  ‹PSKIPS⟪⟪A0 d⊗;✓Rlist A1⟫⟫d (s0 # s1) = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗;✓Rlist (λr. ⟪A1 r⟫d↪nd)⟫⟫nd (s0 # s1)›
  by (fold PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d,
      rule PSKIPS_nd_eqI_strong_id, unfold ℛnd_from_det_to_ndet)
    (all ‹drule set_mp[OF ℛd_combinedRlist_Seqptick_subset]›,
      auto simp add: combineRlist_Seqptick_defs from_det_to_ndet_def ρ_simps split: option.split)

lemma P_combineRlist_Seqptick_behaviour:
  ‹P⟪⟪A0 d⊗;✓Rlist A1⟫⟫d (s0 # s1) = P⟪⟪⟪A0⟫d↪nd nd⊗;✓Rlist (λr. ⟪A1 r⟫d↪nd)⟫⟫nd (s0 # s1)›
  by (fold P_nd_from_det_to_ndet_is_P_d,
      rule P_nd_eqI_strong_id, unfold ℛnd_from_det_to_ndet)
    (drule set_mp[OF ℛd_combinedRlist_Seqptick_subset],
      auto simp add: combineRlist_Seqptick_defs from_det_to_ndet_def ρ_simps split: option.split)


lemma PSKIPS_combineListslenL_Seqptick_behaviour:
  ‹PSKIPS⟪⟪A0 d⊗len0;ListslenL A1⟫⟫d (σs0 @ σs1) = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗len0;ListslenL (λr. ⟪A1 r⟫d↪nd)⟫⟫nd (σs0 @ σs1)›
  if ‹⋀σs0'. σs0' ∈ ℛd A0 σs0 ⟹ length σs0' = len0›
  by (fold PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d,
      rule PSKIPS_nd_eqI_strong_id, unfold ℛnd_from_det_to_ndet)
    (all ‹drule set_mp[OF ℛd_combinedListslenL_Seqptick_subset[OF that], rotated]›,
      auto simp add: combineListslenL_Seqptick from_det_to_ndet_def ρ_simps split: option.split)

lemma P_combineListslenL_Seqptick_behaviour:
  ‹P⟪⟪A0 d⊗len0;ListslenL A1⟫⟫d (σs0 @ σs1) = P⟪⟪⟪A0⟫d↪nd nd⊗len0;ListslenL (λr. ⟪A1 r⟫d↪nd)⟫⟫nd (σs0 @ σs1)›
  if ‹⋀σt0. σt0 ∈ ℛd A0 σs0 ⟹ length σt0 = len0›
  by (fold P_nd_from_det_to_ndet_is_P_d,
      rule P_nd_eqI_strong_id, unfold ℛnd_from_det_to_ndet)
    (drule set_mp[OF ℛd_combinedListslenL_Seqptick_subset[OF that], rotated],
      auto simp add: combineListslenL_Seqptick from_det_to_ndet_def ρ_simps split: option.split)



(*<*)
end
  (*>*)