Theory Test_Suite

section ‹Test Suites›

text ‹This theory introduces a predicate @{text "implies_completeness"} and proves that
      any test suite satisfying this predicate is sufficient to check the reduction conformance
      relation between two (possibly nondeterministic FSMs)› 


theory Test_Suite
imports Helper_Algorithms Adaptive_Test_Case Traversal_Set 
begin

subsection ‹Preliminary Definitions›


type_synonym ('a,'b,'c) preamble = "('a,'b,'c) fsm"
type_synonym ('a,'b,'c) traversal_path = "('a × 'b × 'c × 'a) list"
type_synonym ('a,'b,'c) separator = "('a,'b,'c) fsm"

text ‹A test suite contains of
        1) a set of d-reachable states with their associated preambles
        2) a map from d-reachable states to their associated m-traversal paths 
        3) a map from d-reachable states and associated m-traversal paths to the set of states to r-distinguish the targets of those paths from
        4) a map from pairs of r-distinguishable states to a separator›
datatype ('a,'b,'c,'d) test_suite = Test_Suite "('a × ('a,'b,'c) preamble) set"   
                                               "'a ⇒ ('a,'b,'c) traversal_path set" 
                                               "('a × ('a,'b,'c) traversal_path) ⇒ 'a set" 
                                               "('a × 'a) ⇒ (('d,'b,'c) separator × 'd × 'd) set"




subsection ‹A Sufficiency Criterion for Reduction Testing›

(* to simplify the soundness proof, this formalisation also requires tps to contain nothing but the m-traversal paths;
   this could be lifted by requiring that for every additional path the suite retains additional paths such that all "non-deadlock"
   (w.r.t. the set of all (tps q) paths) states are output complete for the inputs applied *)  

fun implies_completeness_for_repetition_sets :: "('a,'b,'c,'d) test_suite ⇒ ('a,'b,'c) fsm ⇒ nat ⇒ ('a set × 'a set) list ⇒ bool" where
  "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets = 
    ( (initial M,initial_preamble M) ∈ prs 
    ∧ (∀ q P . (q,P) ∈ prs ⟶ (is_preamble P M q) ∧ (tps q) ≠ {})
    ∧ (∀ q1 q2 A d1 d2 . (A,d1,d2) ∈ separators (q1,q2) ⟶ (A,d2,d1) ∈ separators (q2,q1) ∧ is_separator M q1 q2 A d1 d2)
    ∧ (∀ q . q ∈ states M ⟶ (∃d ∈ set repetition_sets. q ∈ fst d))
    ∧ (∀ d . d ∈ set repetition_sets ⟶ ((fst d ⊆ states M) ∧ (snd d = fst d ∩ fst ` prs) ∧ (∀ q1 q2 . q1 ∈ fst d ⟶ q2 ∈ fst d ⟶ q1 ≠ q2 ⟶ separators (q1,q2) ≠ {})))
    ∧ (∀ q . q ∈ image fst prs ⟶ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q) 
    ∧ (∀ q p d . q ∈ image fst prs ⟶ (p,d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟶ 
          ( (∀ p1 p2 p3 . p=p1@p2@p3 ⟶ p2 ≠ [] ⟶ target q p1 ∈ fst d ⟶ target q (p1@p2) ∈ fst d ⟶ target q p1 ≠ target q (p1@p2) ⟶ (p1 ∈ tps q ∧ (p1@p2) ∈ tps q ∧ target q p1 ∈ rd_targets (q,(p1@p2)) ∧ target q (p1@p2) ∈ rd_targets (q,p1)))
          ∧ (∀ p1 p2 q' . p=p1@p2 ⟶ q' ∈ image fst prs ⟶ target q p1 ∈ fst d ⟶ q' ∈ fst d ⟶ target q p1 ≠ q' ⟶ (p1 ∈ tps q ∧ [] ∈ tps q' ∧ target q p1 ∈ rd_targets (q',[]) ∧ q' ∈ rd_targets (q,p1))))
          ∧ (∀ q1 q2 . q1 ≠ q2 ⟶ q1 ∈ snd d ⟶ q2 ∈ snd d ⟶ ([] ∈ tps q1 ∧ [] ∈ tps q2 ∧ q1 ∈ rd_targets (q2,[]) ∧ q2 ∈ rd_targets (q1,[]))))
  )"

definition implies_completeness :: "('a,'b,'c,'d) test_suite ⇒ ('a,'b,'c) fsm ⇒ nat ⇒ bool" where
  "implies_completeness T M m = (∃ repetition_sets . implies_completeness_for_repetition_sets T M m repetition_sets)"



lemma implies_completeness_for_repetition_sets_simps : 
  assumes "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets"
  shows "(initial M,initial_preamble M) ∈ prs" 
    and "⋀ q P . (q,P) ∈ prs ⟹ (is_preamble P M q) ∧ (tps q) ≠ {}"
    and "⋀ q1 q2 A d1 d2 . (A,d1,d2) ∈ separators (q1,q2) ⟹ (A,d2,d1) ∈ separators (q2,q1) ∧ is_separator M q1 q2 A d1 d2"
    and "⋀ q . q ∈ states M ⟹ (∃d ∈ set repetition_sets. q ∈ fst d)"
    and "⋀ d . d ∈ set repetition_sets ⟹ (fst d ⊆ states M) ∧ (snd d = fst d ∩ fst ` prs)"
    and "⋀ d q1 q2 . d ∈ set repetition_sets ⟹ q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ separators (q1,q2) ≠ {}"
    and "⋀ q . q ∈ image fst prs ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q" 
    and "⋀ q p d p1 p2 p3 . q ∈ image fst prs ⟹ (p,d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟹ p=p1@p2@p3 ⟹ p2 ≠ [] ⟹ target q p1 ∈ fst d ⟹ target q (p1@p2) ∈ fst d ⟹ target q p1 ≠ target q (p1@p2) ⟹ (p1 ∈ tps q ∧ (p1@p2) ∈ tps q ∧ target q p1 ∈ rd_targets (q,(p1@p2)) ∧ target q (p1@p2) ∈ rd_targets (q,p1))"
    and "⋀ q p d p1 p2 q' . q ∈ image fst prs ⟹ (p,d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟹ p=p1@p2 ⟹ q' ∈ image fst prs ⟹ target q p1 ∈ fst d ⟹ q' ∈ fst d ⟹ target q p1 ≠ q' ⟹ (p1 ∈ tps q ∧ [] ∈ tps q' ∧ target q p1 ∈ rd_targets (q',[]) ∧ q' ∈ rd_targets (q,p1))"
    and "⋀ q p d q1 q2 . q ∈ image fst prs ⟹ (p,d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟹ q1 ≠ q2 ⟹ q1 ∈ snd d ⟹ q2 ∈ snd d ⟹ ([] ∈ tps q1 ∧ [] ∈ tps q2 ∧ q1 ∈ rd_targets (q2,[]) ∧ q2 ∈ rd_targets (q1,[]))"
proof-

  show "(initial M,initial_preamble M) ∈ prs" 
  and  "⋀ q . q ∈ image fst prs ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q"
    using assms unfolding implies_completeness_for_repetition_sets.simps by blast+

  show "⋀ q1 q2 A d1 d2 . (A,d1,d2) ∈ separators (q1,q2) ⟹ (A,d2,d1) ∈ separators (q2,q1) ∧ is_separator M q1 q2 A d1 d2"
  and  "⋀ q P . (q,P) ∈ prs ⟹ (is_preamble P M q) ∧ (tps q) ≠ {}"
  and  "⋀ q . q ∈ states M ⟹ (∃d ∈ set repetition_sets. q ∈ fst d)"
  and  "⋀ d . d ∈ set repetition_sets ⟹ (fst d ⊆ states M) ∧ (snd d = fst d ∩ fst ` prs)"
  and  "⋀ d q1 q2 . d ∈ set repetition_sets ⟹ q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ separators (q1,q2) ≠ {}"
    using assms unfolding implies_completeness_for_repetition_sets.simps by force+

  show "⋀ q p d p1 p2 p3 . q ∈ image fst prs ⟹ (p,d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟹ p=p1@p2@p3 ⟹ p2 ≠ [] ⟹ target q p1 ∈ fst d ⟹ target q (p1@p2) ∈ fst d ⟹ target q p1 ≠ target q (p1@p2) ⟹ (p1 ∈ tps q ∧ (p1@p2) ∈ tps q ∧ target q p1 ∈ rd_targets (q,(p1@p2)) ∧ target q (p1@p2) ∈ rd_targets (q,p1))"
    using assms unfolding implies_completeness_for_repetition_sets.simps by (metis (no_types, lifting))

  show "⋀ q p d p1 p2 q' . q ∈ image fst prs ⟹ (p,d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟹ p=p1@p2 ⟹ q' ∈ image fst prs ⟹ target q p1 ∈ fst d ⟹ q' ∈ fst d ⟹ target q p1 ≠ q' ⟹ (p1 ∈ tps q ∧ [] ∈ tps q' ∧ target q p1 ∈ rd_targets (q',[]) ∧ q' ∈ rd_targets (q,p1))"
    using assms unfolding implies_completeness_for_repetition_sets.simps by (metis (no_types, lifting))

  show "⋀ q p d q1 q2 . q ∈ image fst prs ⟹ (p,d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟹ q1 ≠ q2 ⟹ q1 ∈ snd d ⟹ q2 ∈ snd d ⟹ ([] ∈ tps q1 ∧ [] ∈ tps q2 ∧ q1 ∈ rd_targets (q2,[]) ∧ q2 ∈ rd_targets (q1,[]))"
    using assms unfolding implies_completeness_for_repetition_sets.simps by (metis (no_types, lifting))
qed




subsection ‹A Pass Relation for Test Suites and Reduction Testing›

fun passes_test_suite :: "('a,'b,'c) fsm ⇒ ('a,'b,'c,'d) test_suite ⇒ ('e,'b,'c) fsm ⇒ bool" where
  "passes_test_suite M (Test_Suite prs tps rd_targets separators) M' = (
    ― ‹Reduction on preambles: as the preambles contain all responses of M to their chosen inputs, M' must not exhibit any other response›
    (∀ q P io x y y' . (q,P) ∈ prs ⟶ io@[(x,y)] ∈ L P ⟶ io@[(x,y')] ∈ L M' ⟶ io@[(x,y')] ∈ L P) 
    ― ‹Reduction on traversal-paths applied after preambles (i.e., completed paths in preambles) - note that tps q is not necessarily prefix-complete›
    ∧ (∀ q P pP ioT pT x y y' . (q,P) ∈ prs ⟶ path P (initial P) pP ⟶ target (initial P) pP = q ⟶ pT ∈ tps q ⟶ ioT@[(x,y)] ∈ set (prefixes (p_io pT)) ⟶ (p_io pP)@ioT@[(x,y')] ∈ L M' ⟶ (∃ pT' . pT' ∈ tps q ∧ ioT@[(x,y')] ∈ set (prefixes (p_io pT'))))
    ― ‹Passing separators: if M' contains an IO-sequence that in the test suite leads through a preamble and an m-traversal path and the target of the latter is to be r-distinguished from some other state, then M' passes the corresponding ATC›
    ∧ (∀ q P pP pT . (q,P) ∈ prs ⟶ path P (initial P) pP ⟶ target (initial P) pP = q ⟶ pT ∈ tps q ⟶ (p_io pP)@(p_io pT) ∈ L M' ⟶ (∀ q' A d1 d2 qT . q' ∈ rd_targets (q,pT) ⟶ (A,d1,d2) ∈ separators (target q pT, q') ⟶ qT ∈ io_targets M' ((p_io pP)@(p_io pT)) (initial M') ⟶ pass_separator_ATC M' A qT d2))
    )"                                                                                                                                                                                                                                                                                                   





subsection ‹Soundness of Sufficient Test Suites›


lemma passes_test_suite_soundness_helper_1 :
  assumes "is_preamble P M q"
  and     "observable M"
  and     "io@[(x,y)] ∈ L P"
  and     "io@[(x,y')] ∈ L M"
shows     "io@[(x,y')] ∈ L P"
proof -
  have   "is_submachine P M"
  and *: "⋀ q' x t t' . q'∈reachable_states P ⟹ x∈FSM.inputs M ⟹
            t∈FSM.transitions P ⟹ t_source t = q' ⟹ t_input t = x ⟹
            t'∈FSM.transitions M ⟹ t_source t' = q' ⟹ t_input t' = x ⟹ t' ∈ FSM.transitions P"
    using assms(1)  unfolding is_preamble_def by blast+

  have "initial P = initial M"
    unfolding submachine_simps[OF ‹is_submachine P M›]
    by simp
  
  obtain p where "path M (initial M) p" and "p_io p = io @ [(x,y')]"
    using assms(4) unfolding submachine_simps[OF ‹is_submachine P M›] by auto
  
  obtain p' t where "p = p'@[t]"
    using ‹p_io p = io @ [(x,y')]› by (induction p rule: rev_induct; auto)

  have "path M (initial M) p'" and "t ∈ transitions M" and "t_source t = target (initial M) p'"
    using ‹path M (initial M) p› path_append_transition_elim
    unfolding ‹p = p'@[t]› by force+

  have "p_io p' = io" and "t_input t = x" and "t_output t = y'"
    using ‹p_io p = io @ [(x,y')]› unfolding ‹p = p'@[t]› by force+
     

  have "p_io p' ∈ LS P (FSM.initial M)"
    using assms(3) unfolding ‹p_io p' = io› ‹initial P = initial M›
    by (meson language_prefix) 

  have "FSM.initial M ∈ reachable_states P"
    unfolding submachine_simps(1)[OF ‹is_submachine P M›, symmetric]
    using reachable_states_initial by blast
  
  obtain pp where "path P (initial P) pp" and "p_io pp = io @ [(x,y)]"
    using assms(3) by auto
  then obtain pp' t' where "pp = pp'@[t']"
  proof -
    assume a1: "⋀pp' t'. pp = pp' @ [t'] ⟹ thesis"
    have "pp ≠ []"
      using ‹p_io pp = io @ [(x, y)]› by auto
    then show ?thesis
      using a1 by (metis (no_types) rev_exhaust)
  qed 

  have "path P (initial P) pp'" and "t' ∈ transitions P" and "t_source t' = target (initial P) pp'"
    using ‹path P (initial P) pp› path_append_transition_elim
    unfolding ‹pp = pp'@[t']› by force+
  have "p_io pp' = io" and "t_input t' = x"
    using ‹p_io pp = io @ [(x,y)]› unfolding ‹pp = pp'@[t']› by force+

  have "path M (initial M) pp'"
    using ‹path P (initial P) pp'› submachine_path_initial[OF ‹is_submachine P M›] by blast
  
  have "pp' = p'"
    using observable_path_unique[OF assms(2) ‹path M (initial M) pp'› ‹path M (initial M) p'› ]
    unfolding ‹p_io pp' = io› ‹p_io p' = io›
    by blast
  then have "t_source t' = target (initial M) p'"
    using ‹t_source t' = target (initial P) pp'› unfolding ‹initial P = initial M› by blast


  have "path P (FSM.initial M) p'"
    using observable_preamble_paths[OF assms(1,2) ‹path M (initial M) p'› 
                                                  ‹p_io p' ∈ LS P (FSM.initial M)› 
                                                  ‹FSM.initial M ∈ reachable_states P›]
    by assumption
  then have "target (initial M) p' ∈ reachable_states P"
    using reachable_states_intro unfolding ‹initial P = initial M›[symmetric] by blast
  moreover have "x ∈ inputs M"
    using ‹t ∈ transitions M› ‹t_input t = x› fsm_transition_input by blast


  have "t ∈ transitions P"
    using *[OF ‹target (initial M) p' ∈ reachable_states P› ‹x ∈ inputs M› ‹t' ∈ transitions P› 
               ‹t_source t' = target (initial M) p'› ‹t_input t' = x› ‹t ∈ transitions M› 
               ‹t_source t = target (FSM.initial M) p'› ‹t_input t = x›]
    by assumption

  then have "path P (initial P) (p'@[t])"
    using ‹path P (initial P) pp'› ‹t_source t = target (initial M) p'›
    unfolding ‹pp' = p'› ‹initial P = initial M› 
    using path_append_transition by simp
  then show ?thesis 
    unfolding ‹p = p'@[t]›[symmetric] LS.simps
    using ‹p_io p = io@[(x,y')]›
    by force
qed



lemma passes_test_suite_soundness :
  assumes "implies_completeness (Test_Suite prs tps rd_targets separators) M m"
  and     "observable M"
  and     "observable M'"
  and     "inputs M' = inputs M"
  and     "completely_specified M"
  and     "L M' ⊆ L M"
shows     "passes_test_suite M (Test_Suite prs tps rd_targets separators) M'"
proof -
  obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets"
    using assms(1) unfolding implies_completeness_def by blast


  have t1: "(initial M, initial_preamble M) ∈ prs" 
    using implies_completeness_for_repetition_sets_simps(1)[OF repetition_sets_def] by assumption
  have t2: "⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q ∧ tps q ≠ {}"
    using implies_completeness_for_repetition_sets_simps(2)[OF repetition_sets_def] by assumption
  have t3: "⋀ q1 q2 A d1 d2. (A, d1, d2) ∈ separators (q1, q2) ⟹ (A, d2, d1) ∈ separators (q2, q1) ∧ is_separator M q1 q2 A d1 d2"
    using implies_completeness_for_repetition_sets_simps(3)[OF repetition_sets_def] by assumption
  
  have t5: "⋀q. q ∈ FSM.states M ⟹ (∃d∈set repetition_sets. q ∈ fst d)"
    using implies_completeness_for_repetition_sets_simps(4)[OF repetition_sets_def] by assumption

  have t6: "⋀ q. q ∈ fst ` prs ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} 
                                                            ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q"
    using implies_completeness_for_repetition_sets_simps(7)[OF repetition_sets_def] by assumption

  have t7: "⋀ d. d ∈ set repetition_sets ⟹ fst d ⊆ FSM.states M"
  and  t8: "⋀ d. d ∈ set repetition_sets ⟹ snd d ⊆ fst d"
  and  t9: "⋀ d q1 q2. d ∈ set repetition_sets ⟹ q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ separators (q1, q2) ≠ {}"
    using implies_completeness_for_repetition_sets_simps(5,6)[OF repetition_sets_def] 
    by blast+

  have t10: "⋀ q p d p1 p2 p3.
              q ∈ fst ` prs ⟹
              (p, d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟹
              p = p1 @ p2 @ p3 ⟹
              p2 ≠ [] ⟹
              target q p1 ∈ fst d ⟹
              target q (p1 @ p2) ∈ fst d ⟹
              target q p1 ≠ target q (p1 @ p2) ⟹
              p1 ∈ tps q ∧ p1 @ p2 ∈ tps q ∧ target q p1 ∈ rd_targets (q, p1 @ p2) ∧ target q (p1 @ p2) ∈ rd_targets (q, p1)"
    using implies_completeness_for_repetition_sets_simps(8)[OF repetition_sets_def] by assumption

  have t11: "⋀ q p d p1 p2 q'.
              q ∈ fst ` prs ⟹
              (p, d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟹
              p = p1 @ p2 ⟹
              q' ∈ fst ` prs ⟹
              target q p1 ∈ fst d ⟹
              q' ∈ fst d ⟹ 
              target q p1 ≠ q' ⟹ 
              p1 ∈ tps q ∧ [] ∈ tps q' ∧ target q p1 ∈ rd_targets (q', []) ∧ q' ∈ rd_targets (q, p1)"
    using implies_completeness_for_repetition_sets_simps(9)[OF repetition_sets_def] by assumption


  have "⋀ q P io x y y' . (q,P) ∈ prs ⟹ io@[(x,y)] ∈ L P ⟹ io@[(x,y')] ∈ L M' ⟹ io@[(x,y')] ∈ L P"
  proof -
    fix q P io x y y' assume "(q,P) ∈ prs" and "io@[(x,y)] ∈ L P" and "io@[(x,y')] ∈ L M'"

    have "is_preamble P M q"
      using ‹(q,P) ∈ prs› ‹⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q ∧ tps q ≠ {}› by blast

    have "io@[(x,y')] ∈ L M"
      using ‹io@[(x,y')] ∈ L M'› assms(6) by blast

    show "io@[(x,y')] ∈ L P"
      using passes_test_suite_soundness_helper_1[OF ‹is_preamble P M q› assms(2) ‹io@[(x,y)] ∈ L P› ‹io@[(x,y')] ∈ L M›]
      by assumption
  qed
  then have p1: "(∀ q P io x y y' . (q,P) ∈ prs ⟶ io@[(x,y)] ∈ L P ⟶ io@[(x,y')] ∈ L M' ⟶ io@[(x,y')] ∈ L P)"
    by blast



  have "⋀ q P pP ioT pT x x' y y' . (q,P) ∈ prs ⟹ 
                                     path P (initial P) pP ⟹ 
                                     target (initial P) pP = q ⟹ 
                                     pT ∈ tps q ⟹ 
                                     ioT @ [(x, y)] ∈ set (prefixes (p_io pT)) ⟹ 
                                     (p_io pP)@ioT@[(x',y')] ∈ L M' ⟹ 
                                     (∃ pT' . pT' ∈ tps q ∧ ioT @ [(x', y')] ∈ set (prefixes (p_io pT')))"
  proof -
    fix q P pP ioT pT x x' y y' 
    assume "(q,P) ∈ prs"  
       and "path P (initial P) pP" 
       and "target (initial P) pP = q" 
       and "pT ∈ tps q" 
       and "ioT @ [(x, y)] ∈ set (prefixes (p_io pT))" 
       and "(p_io pP)@ioT@[(x',y')] ∈ L M'"

    have "is_preamble P M q"
      using ‹(q,P) ∈ prs› ‹⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q ∧ tps q ≠ {}› by blast
    then have "q ∈ states M"
      unfolding is_preamble_def
      by (metis ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› path_target_is_state submachine_path) 


    have "initial P = initial M"
      using ‹is_preamble P M q› unfolding is_preamble_def by auto
    have "path M (initial M) pP"
      using ‹is_preamble P M q› unfolding is_preamble_def using submachine_path_initial
      using ‹path P (FSM.initial P) pP› by blast
    

    have "(p_io pP)@ioT@[(x',y')] ∈ L M"
      using ‹(p_io pP)@ioT@[(x',y')] ∈ L M'› assms(6) by blast
    then obtain pM' where "path M (initial M) pM'" and "p_io pM' = (p_io pP)@ioT@[(x',y')]" 
      by auto

    let ?pP = "take (length pP) pM'"
    let ?pT = "take (length ioT) (drop (length pP) pM')"
    let ?t  = "last pM'"


    have "pM' = ?pP @ ?pT @ [?t]"
    proof -
      have "length pM' = (length pP) + (length ioT) + 1"
        using ‹p_io pM' = (p_io pP)@ioT@[(x',y')]› 
        unfolding length_map[of "(λ t . (t_input t, t_output t))", of pM', symmetric] 
                  length_map[of "(λ t . (t_input t, t_output t))", of pP, symmetric] 
        by auto
      then show ?thesis
        by (metis (no_types, lifting) add_diff_cancel_right' antisym_conv antisym_conv2 
              append_butlast_last_id append_eq_append_conv2 butlast_conv_take drop_Nil drop_eq_Nil 
              le_add1 less_add_one take_add) 
    qed   

    have "p_io ?pP = p_io pP"  
      using ‹p_io pM' = (p_io pP)@ioT@[(x',y')]›
      by (metis (no_types, lifting) append_eq_conv_conj length_map take_map)

    have "p_io ?pT = ioT" 
      using ‹p_io pM' = (p_io pP)@ioT@[(x',y')]›
      using ‹pM' = ?pP @ ?pT @ [?t]›
      by (metis (no_types, lifting) append_eq_conv_conj length_map map_append take_map) 
      
    have "p_io [?t] = [(x',y')]"
      using ‹p_io pM' = (p_io pP)@ioT@[(x',y')]›
      using ‹pM' = ?pP @ ?pT @ [?t]›
      by (metis (no_types, lifting) append_is_Nil_conv last_appendR last_map last_snoc list.simps(8) list.simps(9))

    have "path M (initial M) ?pP"
      using ‹path M (initial M) pM'› ‹pM' = ?pP @ ?pT @ [?t]›
      by (meson path_prefix_take)
      
    have "?pP = pP"
      using observable_path_unique[OF ‹observable M› ‹path M (initial M) ?pP› ‹path M (initial M) pP› ‹p_io ?pP = p_io pP›]
      by assumption
    then have "path M q (?pT@[?t])"
      by (metis ‹FSM.initial P = FSM.initial M› ‹pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']› ‹path M (FSM.initial M) pM'› ‹target (FSM.initial P) pP = q› path_suffix)
    then have "path M q ?pT" 
         and  "?t ∈ transitions M" 
         and  "t_source ?t = target q ?pT"
      by auto

    have "inputs M ≠ {}"
      using language_io(1)[OF ‹(p_io pP)@ioT@[(x',y')] ∈ L M›, of x' y']
      by auto 

    have "q ∈ fst ` prs"
      using ‹(q,P) ∈ prs›
      using image_iff by fastforce 

    obtain ioT' where "p_io pT = (ioT @ [(x, y)]) @ ioT'"
      using ‹ioT @ [(x, y)] ∈ set (prefixes (p_io pT))›
      unfolding prefixes_set 
      by moura
    then have "length pT > length ioT"
      using length_map[of "(λ t . (t_input t, t_output t))" pT] 
      by auto
    
    obtain pT' d' where "(pT @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m"
      using t6[OF ‹q ∈ fst ` prs›] ‹pT ∈ tps q›
      by blast

    let ?p = "pT @ pT'"

    have "path M q ?p"
    and  "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)) repetition_sets = Some d'"
    and  "⋀ p' p''. ?p = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None"
      using ‹(pT @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m›
            m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m] 
      by blast+

    let ?pIO = "take (length ioT) pT"
    have "?pIO = take (length ioT) ?p" 
      using ‹length pT > length ioT› by auto
    then have "?p = ?pIO@(drop (length ioT) ?p)"
      by auto
    have "(drop (length ioT) ?p) ≠ []" 
      using ‹length pT > length ioT› by auto

    have "p_io ?pIO = ioT" 
    proof -
      have "p_io ?pIO = take (length ioT) (p_io pT)"
        by (simp add: take_map)
      moreover have "take (length ioT) (p_io pT) = ioT"
        using ‹p_io pT = (ioT @ [(x, y)]) @ ioT'› by auto
      ultimately show ?thesis by simp
    qed
    then have "p_io ?pIO = p_io ?pT"
      using ‹p_io ?pT = ioT› by simp
    
    have "path M q ?pIO"
      using ‹path M q ?p› unfolding ‹?pIO = take (length ioT) ?p› 
      using path_prefix_take by metis

    have "?pT = ?pIO"
      using observable_path_unique[OF ‹observable M› ‹path M q ?pIO› ‹path M q ?pT› ‹p_io ?pIO = p_io ?pT›] 
      by simp

    show "(∃ pT' . pT' ∈ tps q ∧ ioT @ [(x', y')] ∈ set (prefixes (p_io pT')))"
    proof (cases "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (?pT@[?t]))) repetition_sets = None")
      case True

      obtain pT' d' where "(?pT @ [?t] @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m"
        using m_traversal_path_extension_exist[OF ‹completely_specified M› ‹q ∈ states M› ‹inputs M ≠ {}› t5 t8 ‹path M q (?pT@[?t])› True]
        by auto
      then have "?pT @ [?t] @ pT' ∈ tps q"
        using t6[OF ‹q ∈ fst ` prs›] by force

      moreover have "ioT @ [(x', y')] ∈ set (prefixes (p_io (?pT @ [?t] @ pT')))"
        using ‹p_io ?pIO = ioT› ‹p_io [?t] = [(x',y')]› 
        unfolding ‹?pT = ?pIO› prefixes_set by force

      ultimately show ?thesis 
        by blast
    next
      case False
      
      note ‹path M q (?pT @ [?t])› 
      moreover obtain d' where "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (?pT@[?t]))) repetition_sets = Some d'"
        using False by blast

      moreover have "∀ p' p''. (?pT @ [?t]) = p' @ p'' ∧ p'' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None"
      proof -
        have "⋀ p' p''. (?pT @ [?t]) = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None"
        proof -
          fix p' p'' assume "(?pT @ [?t]) = p' @ p''" and "p'' ≠ []" 
          then obtain pIO' where "?pIO = p' @ pIO'"
            unfolding ‹?pT = ?pIO›
            by (metis butlast_append butlast_snoc)
          then have "?p = p'@pIO'@(drop (length ioT) ?p)"
            using ‹?p = ?pIO@((drop (length ioT) ?p))›
            by (metis append.assoc) 
  
          have "pIO' @ drop (length ioT) (pT @ pT') ≠ []"
            using ‹(drop (length ioT) ?p) ≠ []› by auto
  
          show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None"
            using ‹⋀ p' p''. ?p = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None›
                  [of p' "pIO'@(drop (length ioT) ?p)", OF ‹?p = p'@pIO'@(drop (length ioT) ?p)› ‹pIO' @ drop (length ioT) (pT @ pT') ≠ []›]
            by assumption
        qed
        then show ?thesis by blast
      qed

      ultimately have "((?pT @ [?t]),d') ∈ m_traversal_paths_with_witness M q repetition_sets m"
        using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m] 
        by auto
      then have "(?pT @ [?t]) ∈ tps q"
        using t6[OF ‹q ∈ fst ` prs›] by force
      moreover have "ioT @ [(x', y')] ∈ set (prefixes (p_io (?pT @ [?t])))"
        using ‹p_io ?pT = ioT› ‹p_io [?t] = [(x',y')]›
        unfolding prefixes_set by force

      ultimately show ?thesis 
        by blast
    qed
  qed
  then have p2: "(∀ q P pP ioT pT x y y' . (q,P) ∈ prs ⟶ 
                                            path P (initial P) pP ⟶ 
                                            target (initial P) pP = q ⟶ 
                                            pT ∈ tps q ⟶ 
                                            ioT @ [(x, y)] ∈ set (prefixes (p_io pT)) ⟶ 
                                            (p_io pP)@ioT@[(x,y')] ∈ L M' ⟶ 
                                            (∃ pT' . pT' ∈ tps q ∧ ioT @ [(x, y')] ∈ set (prefixes (p_io pT'))))"
    by blast


  have "⋀ q P pP pT q' A d1 d2 qT . (q,P) ∈ prs ⟹ 
                                      path P (initial P) pP ⟹ 
                                      target (initial P) pP = q ⟹ 
                                      pT ∈ tps q ⟹ 
                                      q' ∈ rd_targets (q,pT) ⟹ 
                                      (A,d1,d2) ∈ separators (target q pT, q') ⟹ 
                                      qT ∈ io_targets M' ((p_io pP)@(p_io pT)) (initial M') ⟹ 
                                      pass_separator_ATC M' A qT d2"
  proof -
    fix q P pP pT q' A d1 d2 qT
    assume "(q,P) ∈ prs" 
    and    "path P (initial P) pP" 
    and    "target (initial P) pP = q" 
    and    "pT ∈ tps q"  
    and    "q' ∈ rd_targets (q,pT)" 
    and    "(A,d1,d2) ∈ separators (target q pT, q')" 
    and    "qT ∈ io_targets M' ((p_io pP)@(p_io pT)) (initial M')"

    have "q ∈ fst ` prs"
      using ‹(q,P) ∈ prs› by force
    have "is_preamble P M q"
      using ‹(q,P) ∈ prs› ‹⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q ∧ tps q ≠ {}› by blast
    then have "q ∈ states M"
      unfolding is_preamble_def
      by (metis ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› path_target_is_state submachine_path) 

    have "initial P = initial M"
      using ‹is_preamble P M q› unfolding is_preamble_def by auto
    have "path M (initial M) pP"
      using ‹is_preamble P M q› unfolding is_preamble_def using submachine_path_initial
      using ‹path P (FSM.initial P) pP› by blast

    have "is_separator M (target q pT) q' A d1 d2"
      using t3[OF ‹(A,d1,d2) ∈ separators (target q pT, q')›]
      by blast

    have "qT ∈ states M'"
      using ‹qT ∈ io_targets M' ((p_io pP)@(p_io pT)) (initial M')›
            io_targets_states
      by (metis (no_types, lifting) subsetD) 

    obtain pT' d' where "(pT @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m"
      using t6[OF ‹q ∈ fst ` prs›] ‹pT ∈ tps q› 
      by blast
    then have "path M q pT"
      using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m] 
      by auto
    then have "target q pT ∈ FSM.states M"
      using path_target_is_state by metis

    have "q' ∈ FSM.states M"
      using is_separator_separated_state_is_state[OF ‹is_separator M (target q pT) q' A d1 d2›] by simp

    have "¬ pass_separator_ATC M' A qT d2 ⟹ ¬ LS M' qT ⊆ LS M (target q pT)"
      using pass_separator_ATC_fail_no_reduction[OF ‹observable M'› ‹observable M› ‹qT ∈ states M'›
                                                    ‹target q pT ∈ FSM.states M› ‹q' ∈ FSM.states M› 
                                                    ‹is_separator M (target q pT) q' A d1 d2› ‹inputs M' = inputs M›]
      by assumption

    moreover have "LS M' qT ⊆ LS M (target q pT)"
    proof -
      have "(target q pT) = target (initial M) (pP@pT)"
        using ‹target (initial P) pP = q› unfolding ‹initial P = initial M› by auto

      have "path M (initial M) (pP@pT)"
        using ‹path M (initial M) pP› ‹target (initial P) pP = q› ‹path M q pT› unfolding ‹initial P = initial M› by auto
      
      then have "(target q pT) ∈ io_targets M (p_io pP @ p_io pT) (FSM.initial M)"
        unfolding io_targets.simps ‹(target q pT) = target (initial M) (pP@pT)›
        using map_append by blast 
      
      show ?thesis
        using observable_language_target[OF ‹observable M› ‹(target q pT) ∈ io_targets M (p_io pP @ p_io pT) (FSM.initial M)› 
                                            ‹qT ∈ io_targets M' ((p_io pP)@(p_io pT)) (initial M')› ‹L M' ⊆ L M›]
        by assumption
    qed

    ultimately show "pass_separator_ATC M' A qT d2"
      by blast
  qed
  then have p3: "(∀ q P pP pT . (q,P) ∈ prs ⟶ 
                                  path P (initial P) pP ⟶ 
                                  target (initial P) pP = q ⟶ 
                                  pT ∈ tps q ⟶ 
                                  (p_io pP)@(p_io pT) ∈ L M' ⟶ 
                                  (∀ q' A d1 d2 qT . q' ∈ rd_targets (q,pT) ⟶ 
                                  (A,d1,d2) ∈ separators (target q pT, q') ⟶ 
                                  qT ∈ io_targets M' ((p_io pP)@(p_io pT)) (initial M') ⟶ 
                                  pass_separator_ATC M' A qT d2))"
    by blast


  show ?thesis 
    using p1 p2 p3
    unfolding passes_test_suite.simps 
    by blast
qed




subsection ‹Exhaustiveness of Sufficient Test Suites›

text ‹This subsection shows that test suites satisfying the sufficiency criterion are exhaustive.
      That is, for a System Under Test with at most m states that contains an error (i.e.: is not
      a reduction) a test suite sufficient for m will not pass.›


subsubsection ‹R Functions›


(* collect all proper suffixes of p that target q' if applied to q *)
definition R :: "('a,'b,'c) fsm ⇒ 'a ⇒ 'a ⇒ ('a × 'b × 'c × 'a) list ⇒ ('a × 'b × 'c × 'a) list ⇒ ('a × 'b × 'c × 'a) list set" where
  "R M q q' pP p = {pP @ p' | p' . p' ≠ [] ∧ target q p' = q' ∧ (∃ p'' . p = p'@p'')}" 

(* add one completed path of some Preamble of q' to R if a preamble exists *)
definition RP :: "('a,'b,'c) fsm ⇒ 'a ⇒ 'a ⇒ ('a × 'b × 'c × 'a) list ⇒ ('a × 'b × 'c × 'a) list ⇒ ('a × ('a,'b,'c) preamble) set ⇒ ('d,'b,'c) fsm ⇒ ('a × 'b × 'c × 'a) list set" where
  "RP M q q' pP p PS M' = (if ∃ P' .  (q',P') ∈ PS then insert (SOME pP' . ∃ P' .  (q',P') ∈ PS ∧ path P' (initial P') pP' ∧ target (initial P') pP' = q' ∧ p_io pP' ∈ L M') (R M q q' pP p) else (R M q q' pP p))" 



lemma RP_from_R :
  assumes "⋀ q P . (q,P) ∈ PS ⟹ is_preamble P M q"
  and     "⋀ q P io x y y' . (q,P) ∈ PS ⟹ io@[(x,y)] ∈ L P ⟹ io@[(x,y')] ∈ L M' ⟹ io@[(x,y')] ∈ L P"
  and     "completely_specified M'"
  and     "inputs M' = inputs M"
shows "(RP M q q' pP p PS M' = R M q q' pP p) 
          ∨ (∃ P' pP' . (q',P') ∈ PS ∧ 
                        path P' (initial P') pP' ∧ 
                        target (initial P') pP' = q' ∧ 
                        path M (initial M) pP' ∧ 
                        target (initial M) pP' = q' ∧ 
                        p_io pP' ∈ L M' ∧ 
                        RP M q q' pP p PS M' = 
                        insert pP' (R M q q' pP p))"
proof (rule ccontr)
  assume "¬ (RP M q q' pP p PS M' = R M q q' pP p ∨ (∃ P' pP' . (q',P') ∈ PS ∧ path P' (initial P') pP' ∧ target (initial P') pP' = q' ∧ path M (initial M) pP' ∧ target (initial M) pP' = q' ∧ p_io pP' ∈ L M' ∧ RP M q q' pP p PS M' = insert pP' (R M q q' pP p)))"
  then have "(RP M q q' pP p PS M' ≠ R M q q' pP p)"
       and  "¬ (∃ P' pP' . (q',P') ∈ PS ∧ 
                            path P' (initial P') pP' ∧ 
                            target (initial P') pP' = q' ∧ 
                            path M (initial M) pP' ∧ 
                            target (initial M) pP' = q' ∧ 
                            p_io pP' ∈ L M' ∧ 
                            RP M q q' pP p PS M' = insert pP' (R M q q' pP p))"
    by blast+

  let ?p = "SOME pP' . ∃ P' .  (q',P') ∈ PS ∧ path P' (initial P') pP' ∧ target (initial P') pP' = q' ∧ p_io pP' ∈ L M'"

  have "∃ P' .  (q',P') ∈ PS"
    using ‹(RP M q q' pP p PS M' ≠ R M q q' pP p)› unfolding RP_def by auto
  then obtain P' where "(q',P') ∈ PS"
    by auto
  then have "is_preamble P' M q'"
    using assms by blast

  obtain pP' where "path P' (initial P') pP'" and "target (initial P') pP' = q'" and "p_io pP' ∈ L M'"
    using preamble_pass_path[OF ‹is_preamble P' M q'›  
          assms(2)[OF ‹(q',P') ∈ PS›] assms(3,4)] 
    by force
  then have "∃ pP' . ∃ P' .  (q',P') ∈ PS ∧ path P' (initial P') pP' ∧ target (initial P') pP' = q' ∧ p_io pP' ∈ L M'"
    using ‹(q',P') ∈ PS› by blast
  have "∃ P' .  (q',P') ∈ PS ∧ path P' (initial P') ?p ∧ target (initial P') ?p = q' ∧ p_io ?p ∈ L M'"
    using someI_ex[OF ‹∃ pP' . ∃ P' .  (q',P') ∈ PS ∧ path P' (initial P') pP' ∧ target (initial P') pP' = q' ∧ p_io pP' ∈ L M'›] 
    by blast

  then obtain P'' where "(q',P'') ∈ PS" and "path P'' (initial P'') ?p" and "target (initial P'') ?p = q'" and "p_io ?p ∈ L M'"
    by auto
  then have "is_preamble P'' M q'"
    using assms by blast

  
  have "initial P'' = initial M"
    using ‹is_preamble P'' M q'› unfolding is_preamble_def by auto
  have "path M (initial M) ?p"
    using ‹is_preamble P'' M q'› unfolding is_preamble_def using submachine_path_initial
    using ‹path P'' (FSM.initial P'') ?p› by blast
  have "target (initial M) ?p = q'"
    using ‹target (initial P'') ?p = q'› unfolding ‹initial P'' = initial M› by assumption

  have "RP M q q' pP p PS M' = insert ?p (R M q q' pP p)"
    using ‹∃ P' .  (q',P') ∈ PS› unfolding RP_def by auto

  then have "(∃ P' pP' . (q',P') ∈ PS ∧ 
                          path P' (initial P') pP' ∧ 
                          target (initial P') pP' = q' ∧ 
                          path M (initial M) pP' ∧ 
                          target (initial M) pP' = q' ∧ 
                          p_io pP' ∈ L M' ∧ 
                          RP M q q' pP p PS M' = insert pP' (R M q q' pP p))"
    using ‹(q',P'') ∈ PS› ‹path P'' (initial P'') ?p› ‹target (initial P'') ?p = q'› 
          ‹path M (initial M) ?p› ‹target (initial M) ?p = q'› ‹p_io ?p ∈ L M'› by blast
  then show "False"
    using ‹¬ (∃ P' pP' . (q',P') ∈ PS ∧ path P' (initial P') pP' ∧ target (initial P') pP' = q' ∧ path M (initial M) pP' ∧ target (initial M) pP' = q' ∧ p_io pP' ∈ L M' ∧ RP M q q' pP p PS M' = insert pP' (R M q q' pP p))›
    by blast
qed


lemma RP_from_R_inserted :
  assumes "⋀ q P . (q,P) ∈ PS ⟹ is_preamble P M q"
  and     "⋀ q P io x y y' . (q,P) ∈ PS ⟹ io@[(x,y)] ∈ L P ⟹ io@[(x,y')] ∈ L M' ⟹ io@[(x,y')] ∈ L P"
  and     "completely_specified M'"
  and     "inputs M' = inputs M"
  and     "pP' ∈ RP M q q' pP p PS M'"
  and     "pP' ∉ R M q q' pP p"
obtains P' where  "(q',P') ∈ PS" 
                  "path P' (initial P') pP'" 
                  "target (initial P') pP' = q'" 
                  "path M (initial M) pP'"
                  "target (initial M) pP' = q'"
                  "p_io pP' ∈ L M'"
                  "RP M q q' pP p PS M' = insert pP' (R M q q' pP p)"
proof -
  have "(RP M q q' pP p PS M' ≠ R M q q' pP p)"
    using assms(5,6) by blast

  then have "(∃P' pP'.
              (q', P') ∈ PS ∧
              path P' (FSM.initial P') pP' ∧
              target (FSM.initial P') pP' = q' ∧
              path M (FSM.initial M) pP' ∧ target (FSM.initial M) pP' = q' ∧ p_io pP' ∈ L M' ∧ RP M q q' pP p PS M' = insert pP' (R M q q' pP p))"
        using RP_from_R[OF assms(1-4), of PS _ _ q q' pP p] by force
  then obtain P' pP'' where "(q', P') ∈ PS"
                            "path P' (FSM.initial P') pP''"
                            "target (FSM.initial P') pP'' = q'"
                            "path M (FSM.initial M) pP''" 
                            "target (FSM.initial M) pP'' = q'" 
                            "p_io pP'' ∈ L M'"
                            "RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)"
    by blast

  moreover have "pP'' = pP'" using ‹RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)› assms(5,6) by simp
  ultimately show ?thesis using that[of P'] unfolding ‹pP'' = pP'› by blast
qed


lemma finite_R :
  assumes "path M q p"
  shows "finite (R M q q' pP p)"
proof -
  have "⋀ p' . p' ∈ (R M q q' pP p) ⟹ p' ∈ set (prefixes (pP@p))"
  proof -
    fix p' assume "p' ∈ (R M q q' pP p)"
    then obtain p'' where "p' = pP @ p''"
      unfolding R_def by blast
    then obtain p''' where "p = p'' @ p'''"
      using ‹p' ∈ (R M q q' pP p)› unfolding R_def by blast
    
    show "p' ∈ set (prefixes (pP@p))"
      unfolding prefixes_set ‹p' = pP @ p''› ‹p = p'' @ p'''› by auto
  qed
  then have "(R M q q' pP p) ⊆ set (prefixes (pP@p))"
    by blast
  then show ?thesis
    using rev_finite_subset by auto 
qed

lemma finite_RP :
  assumes "path M q p"
  and     "⋀ q P . (q,P) ∈ PS ⟹ is_preamble P M q"
  and     "⋀ q P io x y y' . (q,P) ∈ PS ⟹ io@[(x,y)] ∈ L P ⟹ io@[(x,y')] ∈ L M' ⟹ io@[(x,y')] ∈ L P"
  and     "completely_specified M'"
  and     "inputs M' = inputs M"
shows "finite (RP M q q' pP p PS M')"
  using finite_R[OF assms(1), of q' pP ]
        RP_from_R[OF assms(2,3,4,5), of PS _ _ q q' pP p] by force
  

lemma R_component_ob :
  assumes "pR' ∈ R M q q' pP p"
  obtains pR where "pR' = pP@pR"
  using assms unfolding R_def by blast


lemma R_component :
  assumes "(pP@pR) ∈ R M q q' pP p" 
shows "pR = take (length pR) p"
and   "length pR ≤ length p"
and   "t_target (p ! (length pR - 1)) = q'"
and   "pR ≠ []"
proof -
  let ?R = "R M q q' p"

  have "pR ≠ []" and "target q pR = q'" and "∃ p'' . p = pR@p''"
    using ‹pP@pR ∈ R M q q' pP p› unfolding R_def by blast+
  then obtain pR' where "p = pR@pR'"
    by blast

  then show "pR = take (length pR) p" and "length pR ≤ length p"
    by auto
  
  show "t_target (p ! (length pR - 1)) = q'"
    using ‹pR ≠ []› ‹target q pR = q'› unfolding target.simps visited_states.simps
    by (metis (no_types, lifting) Suc_diff_1 ‹pR = take (length pR) p› 
          append_butlast_last_id last.simps last_map length_butlast lessI list.map_disc_iff 
          not_gr_zero nth_append_length nth_take take_eq_Nil) 

  show "pR ≠ []" 
    using ‹pR ≠ []› 
    by assumption
qed


lemma R_component_observable :
  assumes "pP@pR ∈ R M (target (initial M) pP) q' pP p"
  and     "observable M"
  and     "path M (initial M) pP"
  and     "path M (target (initial M) pP) p"
shows "io_targets M (p_io pP @ p_io pR) (initial M) = {target (target (initial M) pP) (take (length pR) p)}"
proof -
  have "pR = take (length pR) p"
  and  "length pR ≤ length p"
  and  "t_target (p ! (length pR - 1)) = q'"
    using R_component[OF assms(1)] by blast+

  let ?q = "(target (initial M) pP)"
  have "path M ?q (take (length pR) p)"
    using assms(4) by (simp add: path_prefix_take) 
  have "p_io (take (length pR) p) = p_io pR"
    using ‹pR = take (length pR) p› by auto
    

  have *:"path M (initial M) (pP @ (take (length pR) p))"
    using ‹path M (initial M) pP› ‹path M ?q (take (length pR) p)› by auto
  have **:"p_io (pP @ (take (length pR) p)) = (p_io pP @ p_io pR)"
    using ‹p_io (take (length pR) p) = p_io pR› by auto
  
  have "target (initial M) (pP @ (take (length pR) p)) = target ?q (take (length pR) p)"
    by auto 
  then have "target ?q (take (length pR) p) ∈ io_targets M (p_io pP @ p_io pR) (initial M)"
    unfolding io_targets.simps using * **
    by (metis (mono_tags, lifting) mem_Collect_eq) 

  show "io_targets M (p_io pP @ p_io pR) (initial M) = {target ?q (take (length pR) p)}"
    using observable_io_targets[OF ‹observable M› language_state_containment[OF * **]]
    by (metis (no_types) ‹target (target (FSM.initial M) pP) (take (length pR) p) ∈ io_targets M (p_io pP @ p_io pR) (FSM.initial M)› singleton_iff)
qed


lemma R_count :                        
  assumes "minimal_sequence_to_failure_extending_preamble_path M M' PS pP io"
  and     "observable M"
  and     "observable M'"
  and     "⋀ q P. (q, P) ∈ PS ⟹ is_preamble P M q"
  and     "path M (target (initial M) pP) p"
  and     "butlast io = p_io p @ ioX"
shows "card (⋃ (image (λ pR . io_targets M' (p_io pR) (initial M')) (R M (target (initial M) pP) q' pP p))) = card (R M (target (initial M) pP) q' pP p)"
  (is "card ?Tgts = card ?R")
and   "⋀ pR . pR ∈ (R M (target (initial M) pP) q' pP p) ⟹ ∃ q . io_targets M' (p_io pR) (initial M') = {q}"
and   "⋀ pR1 pR2 . pR1 ∈ (R M (target (initial M) pP) q' pP p) ⟹ 
                    pR2 ∈ (R M (target (initial M) pP) q' pP p) ⟹ 
                    pR1 ≠ pR2 ⟹ 
                    io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}"
proof -

  have "sequence_to_failure_extending_preamble_path M M' PS pP io"
  and  "⋀ p' io' . sequence_to_failure_extending_preamble_path M M' PS p' io' ⟹ length io ≤ length io'"
    using ‹minimal_sequence_to_failure_extending_preamble_path M M' PS pP io›
    unfolding minimal_sequence_to_failure_extending_preamble_path_def   
    by blast+

  obtain q P where "(q,P) ∈ PS"
              and  "path P (initial P) pP"
              and  "target (initial P) pP = q"
              and  "((p_io pP) @ butlast io) ∈ L M" 
              and  "((p_io pP) @ io) ∉ L M"
              and  "((p_io pP) @ io) ∈ L M'"

    using ‹sequence_to_failure_extending_preamble_path M M' PS pP io›
    unfolding sequence_to_failure_extending_preamble_path_def  
    by blast

  have "is_preamble P M q"
    using ‹(q,P) ∈ PS› ‹⋀ q P. (q, P) ∈ PS ⟹ is_preamble P M q› by blast
  then have "q ∈ states M"
    unfolding is_preamble_def
    by (metis ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› path_target_is_state submachine_path) 

  have "initial P = initial M"
    using ‹is_preamble P M q› unfolding is_preamble_def by auto
  have "path M (initial M) pP"
    using ‹is_preamble P M q› unfolding is_preamble_def using submachine_path_initial
    using ‹path P (FSM.initial P) pP› by blast
  have "target (initial M) pP = q"
    using ‹target (initial P) pP = q› unfolding ‹initial P = initial M› by assumption

  then have "path M q p"
    using ‹path M (target (initial M) pP) p› by auto

  have "io ≠ []"
    using ‹((p_io pP) @ butlast io) ∈ L M› ‹((p_io pP) @ io) ∉ L M› by auto


  (* get the full path along (butlast io) in M, of which p is a (possibly proper) prefix *)

  obtain pX where "path M (target (initial M) pP) (p@pX)" and "p_io (p@pX) = butlast io"
  proof -
    have "p_io pP @ p_io p @ ioX ∈ L M"
      using ‹((p_io pP) @ butlast io) ∈ L M› 
      unfolding ‹butlast io = p_io p @ ioX› 
      by assumption

    obtain p1 p23 where "path M (FSM.initial M) p1" 
                    and "path M (target (FSM.initial M) p1) p23"
                    and "p_io p1 = p_io pP" 
                    and "p_io p23 = p_io p @ ioX"
      using language_state_split[OF ‹p_io pP @ p_io p @ ioX ∈ L M›] 
      by blast

    have "p1 = pP"
      using observable_path_unique[OF ‹observable M› ‹path M (FSM.initial M) p1› ‹path M (FSM.initial M) pP› ‹p_io p1 = p_io pP›] 
      by assumption
    then have "path M (target (FSM.initial M) pP) p23"
      using ‹path M (target (FSM.initial M) p1) p23› by auto
    then have "p_io p @ ioX ∈ LS M (target (initial M) pP)"
      using ‹p_io p23 = p_io p @ ioX› language_state_containment by auto

    obtain p2 p3 where "path M (target (FSM.initial M) pP) p2" 
                   and "path M (target (target (FSM.initial M) pP) p2) p3" 
                   and "p_io p2 = p_io p" 
                   and "p_io p3 = ioX"
      using language_state_split[OF ‹p_io p @ ioX ∈ LS M (target (initial M) pP)›] 
      by blast

    have "p2 = p"
      using observable_path_unique[OF ‹observable M› ‹path M (target (FSM.initial M) pP) p2› ‹path M (target (FSM.initial M) pP) p› ‹p_io p2 = p_io p›] 
      by assumption
    then have "path M (target (FSM.initial M) pP) (p@p3)"
      using ‹path M (target (FSM.initial M) pP) p› ‹path M (target (target (FSM.initial M) pP) p2) p3› 
      by auto
    moreover have "p_io (p@p3) = butlast io"
      unfolding ‹butlast io = p_io p @ ioX› using ‹p_io p3 = ioX› 
      by auto
    ultimately show ?thesis 
      using that[of p3] 
      by simp
  qed


  (* finiteness properties *)

  have "finite ?R"
    using finite_R[OF ‹path M (target (initial M) pP) p›]
    by assumption
  moreover have "⋀ pR . pR ∈ ?R ⟹ finite (io_targets M' (p_io pR) (initial M'))"
    using io_targets_finite by metis
  ultimately have "finite ?Tgts"
    by blast


  (* path properties *)
  
  obtain pP' p' where "path M' (FSM.initial M') pP'" 
                and   "path M' (target (FSM.initial M') pP') p'" 
                and   "p_io pP' = p_io pP" 
                and   "p_io p' = io"
    using language_state_split[OF ‹((p_io pP) @ io) ∈ L M'›]
    by blast

  have "length p ≤ length (butlast io)"
    using ‹butlast io = p_io p @ ioX› by auto
  moreover have "length (butlast io) < length io"
    using ‹io ≠ []› by auto
  ultimately have "length p < length p'"
    unfolding ‹p_io p' = io› length_map[of "(λ t . (t_input t, t_output t))", symmetric] by simp


  let ?q = "(target (FSM.initial M') pP')"

  have "⋀ pR . pP@pR ∈ ?R ⟹ path M' ?q (take (length pR) p') ∧ p_io (take (length pR) p') = p_io pR"
  proof -
    fix pR assume "pP@pR ∈ ?R"
    then have  "pR = take (length pR) p ∧ length pR ≤ length p"
      using R_component(1,2) by metis
    then have "p_io pR = take (length pR) (butlast io)"
      unfolding ‹butlast io = p_io p @ ioX›
      by (metis (no_types, lifting) length_map take_le take_map)
    moreover have "p_io (take (length pR) p') = take (length pR) io"
      by (metis (full_types) ‹p_io p' = io› take_map)
    moreover have "take (length pR) (butlast io) = take (length pR) io"
      by (meson ‹length (butlast io) < length io› ‹length p ≤ length (butlast io)› 
            ‹pR = take (length pR) p ∧ length pR ≤ length p› dual_order.strict_trans2 take_butlast)
    ultimately have "p_io (take (length pR) p') = p_io pR"
      by simp 
    moreover have "path M' ?q (take (length pR) p')"
      using ‹path M' (target (FSM.initial M') pP') p'›
      by (simp add: path_prefix_take) 
    ultimately show "path M' ?q (take (length pR) p') ∧ p_io (take (length pR) p') = p_io pR"
      by blast
  qed


  (* every element in R reaches exactly one state in M' *)

  have singleton_prop': "⋀ pR . pP@pR ∈ ?R ⟹ io_targets M' (p_io (pP@pR)) (initial M') = {target ?q (take (length pR) p')}"
  proof -
    fix pR assume "pP@pR ∈ ?R"
    then have "path M' ?q (take (length pR) p')" and "p_io (take (length pR) p') = p_io pR"
      using ‹⋀ pR . pP@pR ∈ ?R ⟹ path M' ?q (take (length pR) p') ∧ p_io (take (length pR) p') = p_io pR› by blast+

    have *:"path M' (initial M') (pP' @ (take (length pR) p'))"
      using ‹path M' (initial M') pP'› ‹path M' ?q (take (length pR) p')› by auto
    have **:"p_io (pP' @ (take (length pR) p')) = (p_io (pP@pR))"
      using ‹p_io pP' = p_io pP› ‹p_io (take (length pR) p') = p_io pR› by auto
    
    have "target (initial M') (pP' @ (take (length pR) p')) = target ?q (take (length pR) p')"
      by auto 
    then have "target ?q (take (length pR) p') ∈ io_targets M' (p_io (pP@pR)) (initial M')"
      unfolding io_targets.simps using * **
      by (metis (mono_tags, lifting) mem_Collect_eq) 

    show "io_targets M' (p_io (pP@pR)) (initial M') = {target ?q (take (length pR) p')}"
      using observable_io_targets[OF ‹observable M'› language_state_containment[OF * **]]
      by (metis (no_types) ‹target (target (FSM.initial M') pP') (take (length pR) p') ∈ io_targets M' (p_io (pP@pR)) (FSM.initial M')› singleton_iff)
  qed

  have singleton_prop: "⋀ pR . pR ∈ ?R ⟹ io_targets M' (p_io pR) (initial M') = {target ?q (take (length pR - length pP) p')}"
  proof -
    fix pR assume "pR ∈ ?R"
    then obtain pR' where "pR = pP@pR'"
      using R_component_ob[of _ M "(target (FSM.initial M) pP)" q' pP p] by blast
    have **: "(length (pP @ pR') - length pP) = length pR'"
      by auto

    show "io_targets M' (p_io pR) (initial M') = {target ?q (take (length pR - length pP) p')}"
      using singleton_prop'[of pR'] ‹pR ∈ ?R› unfolding ‹pR = pP@pR'› ** by blast
  qed
  then show "⋀ pR . pR ∈ ?R ⟹ ∃ q . io_targets M' (p_io pR) (initial M') = {q}"
    by blast

  (* distinct elements in R reach distinct states in M' *)
  have pairwise_dist_prop': "⋀ pR1 pR2 . pP@pR1 ∈ ?R ⟹ pP@pR2 ∈ ?R ⟹ pR1 ≠ pR2 ⟹ io_targets M' (p_io (pP@pR1)) (initial M') ∩ io_targets M' (p_io (pP@pR2)) (initial M') = {}"
  proof -
    
    have diff_prop: "⋀ pR1 pR2 . pP@pR1 ∈ ?R ⟹ pP@pR2 ∈ ?R ⟹ length pR1 < length pR2 ⟹ io_targets M' (p_io (pP@pR1)) (initial M') ∩ io_targets M' (p_io (pP@pR2)) (initial M') = {}"
    proof -
      fix pR1 pR2 assume "pP@pR1 ∈ ?R" and "pP@pR2 ∈ ?R" and "length pR1 < length pR2"

      let ?i = "length pR1 - 1"
      let ?j = "length pR2 - 1"

      have "pR1 = take (length pR1) p" and ‹length pR1 ≤ length p› and "t_target (p ! ?i) = q'"
        using R_component[OF ‹pP@pR1 ∈ ?R›]
        by simp+
      have "length pR1 ≠ 0"
        using ‹pP@pR1 ∈ ?R› unfolding R_def
        by simp 
      then have "?i < ?j" 
        using ‹length pR1 < length pR2›
        by (simp add: less_diff_conv) 


      have "pR2 = take (length pR2) p" and ‹length pR2 ≤ length p› and "t_target (p ! ?j) = q'"
        using R_component[OF ‹pP@pR2 ∈ ?R›]
        by simp+
      then have "?j < length (butlast io)"
        using ‹length p ≤ length (butlast io)› ‹length pR1 < length pR2› by linarith


      have "?q ∈ io_targets M' (p_io pP) (FSM.initial M')"
        unfolding ‹p_io pP' = p_io pP›[symmetric] io_targets.simps
        using ‹path M' (initial M') pP'› by auto

      have "t_target (p ! ?i) = t_target (p ! ?j)"
        using ‹t_target (p ! ?i) = q'› ‹t_target (p ! ?j) = q'› by simp
      moreover have "(p @ pX) ! ?i = p ! ?i"
        by (meson ‹length pR1 < length pR2› ‹length pR2 ≤ length p› less_imp_diff_less less_le_trans nth_append)
      moreover have "(p @ pX) ! ?j = p ! ?j"
        by (metis (no_types) ‹length pR1 < length pR2› ‹pR2 = take (length pR2) p› diff_less less_imp_diff_less less_nat_zero_code less_numeral_extra(1) not_le_imp_less not_less_iff_gr_or_eq nth_append take_all)
      ultimately have "t_target (p' ! ?i) ≠ t_target (p' ! ?j)"
        using minimal_sequence_to_failure_extending_preamble_no_repetitions_along_path[OF assms(1,2) ‹path M (target (initial M) pP) (p@pX)› ‹p_io (p @ pX) = butlast io› ‹?q ∈ io_targets M' (p_io pP) (FSM.initial M')› ‹path M' (target (FSM.initial M') pP') p'› ‹p_io p' = io› ‹?i < ?j› ‹?j < length (butlast io)› assms(4)]
        by auto

      have t1: "io_targets M' (p_io (pP@pR1)) (initial M') = {t_target (p' ! ?i)}"
      proof -
        have "(p' ! ?i) = last (take (length pR1) p')"
          using ‹length pR1 ≤ length p› ‹length p < length p'›
          by (metis Suc_diff_1 ‹length pR1 ≠ 0› dual_order.strict_trans2 length_0_conv length_greater_0_conv less_imp_diff_less take_last_index)
        then have *: "target (target (FSM.initial M') pP') (take (length pR1) p') = t_target (p' ! ?i)"
          unfolding target.simps visited_states.simps
          by (metis (no_types, lifting) ‹length p < length p'› ‹length pR1 ≠ 0› gr_implies_not_zero last.simps last_map length_0_conv map_is_Nil_conv take_eq_Nil) 
        have **: "(length (pP @ pR1) - length pP) = length pR1"
          by auto
        show ?thesis
          using singleton_prop[OF ‹pP@pR1 ∈ ?R›]
          unfolding * ** by assumption
      qed

      have t2: "io_targets M' (p_io (pP@pR2)) (initial M') = {t_target (p' ! ?j)}"
      proof -
        have "(p' ! ?j) = last (take (length pR2) p')"
          using ‹length pR2 ≤ length p› ‹length p < length p'›
          by (metis Suc_diff_1 ‹length pR1 - 1 < length pR2 - 1› le_less_trans less_imp_diff_less 
                linorder_neqE_nat not_less_zero take_last_index zero_less_diff)
        then have *: "target (target (FSM.initial M') pP') (take (length pR2) p') = t_target (p' ! ?j)"
          unfolding target.simps visited_states.simps
          by (metis (no_types, lifting) Nil_is_map_conv ‹length p < length p'› ‹length pR1 < length pR2› 
                last.simps last_map list.size(3) not_less_zero take_eq_Nil)
        have **: "(length (pP @ pR2) - length pP) = length pR2"
          by auto  
        show ?thesis
          using singleton_prop'[OF ‹pP@pR2 ∈ ?R›]
          unfolding * ** by assumption
      qed

      show "io_targets M' (p_io (pP@pR1)) (initial M') ∩ io_targets M' (p_io (pP@pR2)) (initial M') = {}"
        using ‹t_target (p' ! ?i) ≠ t_target (p' ! ?j)›
        unfolding t1 t2 by simp
    qed


    fix pR1 pR2 assume "pP@pR1 ∈ ?R" and "pP@pR2 ∈ ?R" and "pR1 ≠ pR2"
    then have "length pR1 ≠ length pR2"
      unfolding R_def
      by auto 

    then consider (a) "length pR1 < length pR2" | (b) "length pR2 < length pR1"
      using nat_neq_iff by blast 
    then show "io_targets M' (p_io (pP@pR1)) (initial M') ∩ io_targets M' (p_io (pP@pR2)) (initial M') = {}"
    proof cases
      case a
      show ?thesis using diff_prop[OF ‹pP@pR1 ∈ ?R› ‹pP@pR2 ∈ ?R› a] by blast
    next
      case b
      show ?thesis using diff_prop[OF ‹pP@pR2 ∈ ?R› ‹pP@pR1 ∈ ?R› b] by blast
    qed
  qed

  then show pairwise_dist_prop: "⋀ pR1 pR2 . pR1 ∈ ?R ⟹ pR2 ∈ ?R ⟹ pR1 ≠ pR2 ⟹ io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}" 
    using R_component_ob
    by (metis (no_types, lifting)) 


  (* combining results *)

  let ?f = "(λ pR . io_targets M' (p_io pR) (initial M'))"
  
  have p1: "(⋀S1 S2. S1 ∈ ?R ⟹ S2 ∈ ?R ⟹ S1 = S2 ∨ ?f S1 ∩ ?f S2 = {})"
    using pairwise_dist_prop by blast
  have p2: "(⋀S. S ∈ R M (target (FSM.initial M) pP) q' pP p ⟹ io_targets M' (p_io S) (FSM.initial M') ≠ {})"
    using singleton_prop by blast
  have c1: "card (R M (target (FSM.initial M) pP) q' pP p) = card ((λS. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p)"
    using card_union_of_distinct[of ?R, OF p1 ‹finite ?R› p2] by force

  have p3: "(⋀S. S ∈ (λS. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p ⟹ ∃t. S = {t})"
    using singleton_prop by blast
  have c2:"card ((λS. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p) = card (⋃S∈R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io S) (FSM.initial M'))"
    using card_union_of_singletons[of "((λS. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p)", OF p3] by force

    
  show "card ?Tgts = card ?R"
    unfolding c1 c2 by blast
qed


lemma R_update :
  "R M q q' pP (p@[t]) = (if (target q (p@[t]) = q')
                          then insert (pP@p@[t]) (R M q q' pP p)
                          else (R M q q' pP p))"
  (is "?R1 = ?R2")
proof (cases "(target q (p@[t]) = q')")
  case True
  then have *: "?R2 = insert (pP@p@[t]) (R M q q' pP p)"
    by auto
  
  have "⋀ p' . p' ∈ R M q q' pP (p@[t]) ⟹ p' ∈ insert (pP@p@[