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 mem_Collect_eq by metis
    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@[t]) (R M q q' pP p)"
  proof -
    fix p' assume "p' ∈ R M q q' pP (p@[t])"

    obtain p'' where "p' = pP @ p''"
      using R_component_ob[OF ‹p' ∈ R M q q' pP (p@[t])›] by blast

    obtain p''' where "p'' ≠ []" and "target q p'' = q'" and "p @ [t] = p'' @ p'''"
      using ‹p' ∈ R M q q' pP (p@[t])› unfolding R_def ‹p' = pP @ p''›
      by auto 

    show "p' ∈ insert (pP@p@[t]) (R M q q' pP p)"
    proof (cases p''' rule: rev_cases)
      case Nil
      then have "p' = pP@(p@[t])" using ‹p' = pP @ p''› ‹p @ [t] = p'' @ p'''› by auto
      then show ?thesis by blast
    next
      case (snoc p'''' t')
      then have "p = p'' @ p''''" using ‹p @ [t] = p'' @ p'''› by auto
      then show ?thesis 
        unfolding R_def using ‹p'' ≠ []› ‹target q p'' = q'›
        by (simp add: ‹p' = pP @ p''›) 
    qed
  qed
  moreover have "⋀ p' . p' ∈ insert (pP@p@[t]) (R M q q' pP p) ⟹ p' ∈ R M q q' pP (p@[t])"
  proof -
    fix p' assume "p' ∈ insert (pP@p@[t]) (R M q q' pP p)"
    then consider (a) "p' = (pP@p@[t])" | (b) "p' ∈ (R M q q' pP p)" by blast
    then show "p' ∈ R M q q' pP (p@[t])" proof cases
      case a
      then show ?thesis using True unfolding R_def
        by simp 
    next
      case b
      then show ?thesis unfolding R_def
        using append.assoc by blast 
    qed 
  qed
  ultimately show ?thesis 
    unfolding * by blast
next
  case False
  then have *: "?R2 = (R M q q' pP p)"
    by auto

  have "⋀ p' . p' ∈ R M q q' pP (p@[t]) ⟹ p' ∈ (R M q q' pP p)"
  proof -
    fix p' assume "p' ∈ R M q q' pP (p@[t])"

    obtain p'' where "p' = pP @ p''"
      using R_component_ob[OF ‹p' ∈ R M q q' pP (p@[t])›] by blast

    obtain p''' where "p'' ≠ []" and "target q p'' = q'" and "p @ [t] = p'' @ p'''"
      using ‹p' ∈ R M q q' pP (p@[t])› unfolding R_def ‹p' = pP @ p''› by blast

    show "p' ∈ (R M q q' pP p)"
    proof (cases p''' rule: rev_cases)
      case Nil
      then have "p' = pP@(p@[t])" using ‹p' = pP @ p''› ‹p @ [t] = p'' @ p'''› by auto
      then show ?thesis
        using False ‹p @ [t] = p'' @ p'''› ‹target q p'' = q'› local.Nil by auto
    next
      case (snoc p'''' t')
      then have "p = p'' @ p''''" using ‹p @ [t] = p'' @ p'''› by auto
      then show ?thesis 
        unfolding R_def using ‹p'' ≠ []› ‹target q p'' = q'›
        by (simp add: ‹p' = pP @ p''›) 
    qed
  qed
  moreover have "⋀ p' . p' ∈ (R M q q' pP p) ⟹ p' ∈ R M q q' pP (p@[t])"
  proof -
    fix p' assume "p' ∈ (R M q q' pP p)"
    then show "p' ∈ R M q q' pP (p@[t])" unfolding R_def
      using append.assoc by blast 
  qed
  ultimately show ?thesis 
    unfolding * by blast
qed


lemma R_union_card_is_suffix_length :
  assumes "path M (initial M) pP"
  and     "path M (target (initial M) pP) p"
shows "(∑ q ∈ states M . card (R M (target (initial M) pP) q pP p)) = length p"
using assms(2) proof (induction p rule: rev_induct)
  case Nil
  have "⋀ q' . R M (target (initial M) pP) q' pP [] = {}"
    unfolding R_def by auto 
  then show ?case
    by simp 
next
  case (snoc t p)
  then have "path M (target (initial M) pP) p"
    by auto

  let ?q = "(target (initial M) pP)"
  let ?q' = "target ?q (p @ [t])"

  have "⋀ q . q ≠ ?q' ⟹ R M ?q q pP (p@[t]) = R M ?q q pP p"
    using R_update[of M ?q _ pP p t] by force
  then have *: "(∑ q ∈ states M - {?q'} . card (R M (target (initial M) pP) q pP (p@[t]))) 
                  = (∑ q ∈ states M - {?q'} . card (R M (target (initial M) pP) q pP p))"
    by force



  have "R M ?q ?q' pP (p@[t]) = insert (pP@p@[t]) (R M ?q ?q' pP p)"
    using R_update[of M ?q ?q' pP p t] by force 
  moreover have "(pP@p@[t]) ∉ (R M ?q ?q' pP p)"
    unfolding R_def by simp 
  ultimately have **: "card (R M (target (initial M) pP) ?q' pP (p@[t])) = Suc (card (R M (target (initial M) pP) ?q' pP p))"
    using finite_R[OF ‹path M (target (initial M) pP) (p@[t])›] finite_R[OF ‹path M (target (initial M) pP) p›]
    by simp


  have "?q' ∈ states M"
    using path_target_is_state[OF ‹path M (target (FSM.initial M) pP) (p @ [t])›] by assumption
  then have ***: "(∑ q ∈ states M . card (R M (target (initial M) pP) q pP (p@[t]))) 
                    = (∑ q ∈ states M - {?q'} . card (R M (target (initial M) pP) q pP (p@[t]))) + (card (R M (target (initial M) pP) ?q' pP (p@[t])))"
       and ****: "(∑ q ∈ states M . card (R M (target (initial M) pP) q pP p)) 
                    = (∑ q ∈ states M - {?q'} . card (R M (target (initial M) pP) q pP p)) + (card (R M (target (initial M) pP) ?q' pP p))"
    by (metis (no_types, lifting) Diff_insert_absorb add.commute finite_Diff fsm_states_finite mk_disjoint_insert sum.insert)+

  have "(∑ q ∈ states M . card (R M (target (initial M) pP) q pP (p@[t]))) = Suc (∑ q ∈ states M . card (R M (target (initial M) pP) q pP p))"
    unfolding **** *** ** * by simp

  then show ?case
    unfolding snoc.IH[OF ‹path M (target (initial M) pP) p›] by auto
qed



lemma RP_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"
  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 "card (⋃ (image (λ pR . io_targets M' (p_io pR) (initial M')) (RP M (target (initial M) pP) q' pP p PS M'))) 
        = card (RP M (target (initial M) pP) q' pP p PS M')"
  (is "card ?Tgts = card ?RP")
and "⋀ pR . pR ∈ (RP M (target (initial M) pP) q' pP p PS M') ⟹ ∃ q . io_targets M' (p_io pR) (initial M') = {q}"
and "⋀ pR1 pR2 . pR1 ∈ (RP M (target (initial M) pP) q' pP p PS M') ⟹ pR2 ∈ (RP M (target (initial M) pP) q' pP p PS M') ⟹ pR1 ≠ pR2 ⟹ io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}"
proof -
  let ?P1 = "card (⋃ (image (λ pR . io_targets M' (p_io pR) (initial M')) (RP M (target (initial M) pP) q' pP p PS M'))) = card (RP M (target (initial M) pP) q' pP p PS M')"
  let ?P2 = "∀ pR . pR ∈ (RP M (target (initial M) pP) q' pP p PS M') ⟶ (∃ q . io_targets M' (p_io pR) (initial M') = {q})"
  let ?P3 = "∀ pR1 pR2 . pR1 ∈ (RP M (target (initial M) pP) q' pP p PS M') ⟶ pR2 ∈ (RP M (target (initial M) pP) q' pP p PS M') ⟶ pR1 ≠ pR2 ⟶ io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}"
  let ?combined_goals = "?P1 ∧ ?P2 ∧ ?P3"
    
  let ?q = "(target (initial M) pP)"
  let ?R = "R M ?q q' pP p"

  consider (a) "(?RP = ?R)" |
           (b) "(∃ 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 = insert pP' ?R)"
    using RP_from_R[OF assms(4,7,8,9), of PS _ _ ?q q' pP p] by force

  then have ?combined_goals proof cases
    case a
    show ?thesis unfolding a using R_count[OF assms(1-6)] by blast
  next
    case b
    

    (* properties from R_count *)

    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
  
  
    (* finiteness properties *)
  
    have "finite ?RP"                                          
      using finite_RP[OF ‹path M (target (initial M) pP) p› assms(4,7,8,9)] by force
    moreover have "⋀ pR . pR ∈ ?RP ⟹ 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)"
        by (metis (no_types, lifting) assms(6) 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"
        using ‹length p ≤ length (butlast io)› ‹pR = take (length pR) p ∧ length pR ≤ length p›
              butlast_take_le dual_order.trans 
        by blast
      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'_R: "⋀ 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_R: "⋀ 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'_R[of pR'] ‹pR ∈ ?R› unfolding ‹pR = pP@pR'› ** by blast
    qed


    (* RP props *)

    from b obtain P' pP'' where "(q',P') ∈ PS"
                          and   "path P' (initial P') pP''"
                          and   "target (initial P') pP'' = q'"
                          and   "path M (initial M) pP''"
                          and   "target (initial M) pP'' = q'"
                          and   "p_io pP'' ∈ L M'"
                          and   "?RP = insert pP'' ?R"
      by blast
    have "initial P' = initial M"
      using assms(4)[OF ‹(q',P') ∈ PS›] unfolding is_preamble_def by auto

    

    (* revisiting singleton_prop *)

    have "⋀ pR . pR ∈ ?RP ⟹ pR ∈ ?R ∨ pR = pP''"
      using ‹?RP = insert pP'' ?R› by blast
    then have rp_cases[consumes 1, case_names in_R inserted]: "⋀ pR P . (pR ∈ ?RP) ⟹ (pR ∈ ?R ⟹ P) ⟹ (pR = pP'' ⟹ P) ⟹ P" 
      by force 

    have singleton_prop_RP: "⋀ pR . pR ∈ ?RP ⟹ ∃ q . io_targets M' (p_io pR) (initial M') = {q}"
    proof - 
      fix pR assume "pR ∈ ?RP"
      then show "∃ q . io_targets M' (p_io pR) (initial M') = {q}" 
      proof (cases rule: rp_cases)
        case in_R
        then show ?thesis using singleton_prop_R by blast
      next
        case inserted
        show ?thesis 
          using observable_io_targets[OF ‹observable M'› ‹p_io pP'' ∈ L M'›] unfolding inserted
          by meson 
      qed
    qed
    then have ?P2 by blast


    (* distinctness in RP *)

    have pairwise_dist_prop_RP: "⋀ pR1 pR2 . pR1 ∈ ?RP ⟹ pR2 ∈ ?RP ⟹ pR1 ≠ pR2 ⟹ io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}"
    proof -
      
      have pairwise_dist_prop_R: "⋀ 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_count(3)[OF assms(1-6)] by force

      have pairwise_dist_prop_PS: "⋀ pR1 . pR1 ∈ ?RP ⟹ pR1 ≠ pP'' ⟹ io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pP'') (initial M') = {}"
      proof -
        fix pR1 assume "pR1 ∈ ?RP" and "pR1 ≠ pP''"
        then have "pR1 ∈ ?R"
          using ‹⋀ pR . pR ∈ ?RP ⟹ pR ∈ ?R ∨ pR = pP''› by blast
        
        obtain pR' where "pR1 = pP@pR'"
          using R_component_ob[OF ‹pR1 ∈ ?R›] by blast
        then have "pP@pR' ∈ ?R"
          using ‹pR1 ∈ ?R› by blast

        have "pR' = take (length pR') p" 
         and "length pR' ≤ length p" 
         and "t_target (p ! (length pR' - 1)) = q'" 
         and "pR' ≠ []"
          using R_component[OF ‹pP@pR' ∈ ?R›] by blast+

        let ?i = "(length pR') - 1"
        have "?i < length p"
          using ‹length pR' ≤ length p› ‹pR' ≠ []›
          using diff_less dual_order.strict_trans1 less_numeral_extra(1) by blast 
        then have "?i < length (butlast io)"
          using ‹length p ≤ length (butlast io)› less_le_trans by blast 


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

        have "t_target (p' ! (length pR' - 1)) ∉ io_targets M' (p_io pP'') (FSM.initial M')"
        proof -
          (* 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

          (* get index properties *)

          have "target (FSM.initial M') pP' ∈ io_targets M' (p_io pP) (FSM.initial M')"
            using ‹p_io pP' = p_io pP› ‹path M' (FSM.initial M') pP'› observable_path_io_target by auto 
  
          have "(t_target (p ! (length pR' - 1)), P') ∈ PS"
            using ‹(q',P') ∈ PS› unfolding ‹t_target (p ! (length pR' - 1)) = q'› by assumption
          then have "(t_target ((p @ pX) ! ?i), P') ∈ PS"
            by (metis ‹length pR' - 1 < length p› nth_append)
  
          have "target (FSM.initial P') pP'' = t_target (p ! (length pR' - 1))"
            unfolding ‹target (initial M) pP'' = q'› ‹t_target (p ! (length pR' - 1)) = q'› ‹initial P' = initial M› by simp
          then have "target (FSM.initial P') pP'' = t_target ((p @ pX) ! ?i)"
            by (metis ‹length pR' - 1 < length p› nth_append)
            

          show ?thesis
            using minimal_sequence_to_failure_extending_preamble_no_repetitions_with_other_preambles
                    [OF assms(1,2) ‹path M (target (initial M) pP) (p@pX)› ‹p_io (p@pX) = butlast io› 
                        ‹target (FSM.initial M') pP' ∈ io_targets M' (p_io pP) (FSM.initial M')› 
                        ‹path M' (target (FSM.initial M') pP') p'› ‹p_io p' = io› assms(4) 
                        ‹?i < length (butlast io)› ‹(t_target ((p @ pX) ! ?i), P') ∈ PS› 
                        ‹path P' (initial P') pP''› ‹target (FSM.initial P') pP'' = t_target ((p @ pX) ! ?i)›]
            by blast
        qed
        then show "io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pP'') (initial M') = {}"
          unfolding ‹io_targets M' (p_io pR1) (initial M') = {t_target (p' ! ?i)}› 
          by blast
      qed


      fix pR1 pR2 assume "pR1 ∈ ?RP" and "pR2 ∈ ?RP" and "pR1 ≠ pR2"

      then consider (a) "pR1 ∈ ?R ∧ pR2 ∈ ?R" |
                    (b) "pR1 = pP''" |
                    (c) "pR2 = pP''" 
        using ‹⋀ pR . pR ∈ ?RP ⟹ pR ∈ ?R ∨ pR = pP''› ‹pR1 ≠ pR2› by blast
      then show "io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}"
      proof cases
        case a
        then show ?thesis using pairwise_dist_prop_R[of pR1 pR2, OF _ _ ‹pR1 ≠ pR2›] by blast
      next
        case b
        then show ?thesis using pairwise_dist_prop_PS[OF ‹pR2 ∈ ?RP›] ‹pR1 ≠ pR2› by blast
      next
        case c
        then show ?thesis using pairwise_dist_prop_PS[OF ‹pR1 ∈ ?RP›] ‹pR1 ≠ pR2› by blast
      qed
    qed
    then have ?P3 by blast


    let ?f = "(λ pR . io_targets M' (p_io pR) (initial M'))"
  
    have p1: "(⋀S1 S2. S1 ∈ ?RP ⟹ S2 ∈ ?RP ⟹ S1 = S2 ∨ ?f S1 ∩ ?f S2 = {})"
      using pairwise_dist_prop_RP by blast
    have p2: "(⋀S. S ∈ ?RP ⟹ io_targets M' (p_io S) (FSM.initial M') ≠ {})"
      using singleton_prop_RP by blast
    have c1: "card ?RP = card ((λS. io_targets M' (p_io S) (FSM.initial M')) ` ?RP)"
      using card_union_of_distinct[of ?RP, OF p1 ‹finite ?RP› p2] by force
  
    have p3: "(⋀S. S ∈ (λS. io_targets M' (p_io S) (FSM.initial M')) ` ?RP ⟹ ∃t. S = {t})"
      using singleton_prop_RP by blast
    have c2:"card ((λS. io_targets M' (p_io S) (FSM.initial M')) ` ?RP) = card (⋃S∈?RP. 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')) ` ?RP)", OF p3] by force
        
    have ?P1
      unfolding c1 c2 by blast

    show ?combined_goals 
      using ‹?P1› ‹?P2› ‹?P3› 
      by blast
  qed

  

  then show "card (⋃ (image (λ pR . io_targets M' (p_io pR) (initial M')) (RP M (target (initial M) pP) q' pP p PS M'))) = card (RP M (target (initial M) pP) q' pP p PS M')"
       and  "⋀ pR . pR ∈ (RP M (target (initial M) pP) q' pP p PS M') ⟹ ∃ q . io_targets M' (p_io pR) (initial M') = {q}"
       and  "⋀ pR1 pR2 . pR1 ∈ (RP M (target (initial M) pP) q' pP p PS M') ⟹ pR2 ∈ (RP M (target (initial M) pP) q' pP p PS M') ⟹ pR1 ≠ pR2 ⟹ io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}"
    by blast+
qed



lemma RP_target: 
  assumes "pR ∈ (RP M q q' pP p PS M')" 
  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 "target (initial M) pR = q'"
proof -
  show "target (initial M) pR = q'"
  proof (cases "pR ∈ R M q q' pP p")
    case True
    then show ?thesis unfolding R_def by force
  next
    case False
    then have "RP M q q' pP p PS M' ≠ R M q q' pP p"
      using assms(1) 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(2-5), of PS _ _ q q' pP p] by force
    then obtain pP' where "target (FSM.initial M) pP' = q'" and "RP M q q' pP p PS M' = insert pP' (R M q q' pP p)"
      by blast
    
    have "pR = pP'"
      using ‹RP M q q' pP p PS M' = insert pP' (R M q q' pP p)› ‹pR ∈ (RP M q q' pP p PS M')› False by blast

    show ?thesis using ‹target (FSM.initial M) pP' = q'› unfolding ‹pR = pP'› by assumption
  qed
qed 


subsubsection ‹Proof of Exhaustiveness›

lemma passes_test_suite_exhaustiveness_helper_1 :
  assumes "completely_specified M'"
  and     "inputs M' = inputs M"
  and     "observable M"
  and     "observable M'"
  and     "(q,P) ∈ PS"
  and     "path P (initial P) pP"
  and     "target (initial P) pP = q"
  and     "p_io pP @ p_io p ∈ L M'"  
  and     "(p, d) ∈ m_traversal_paths_with_witness M q repetition_sets m"
  and     "implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets"
  and     "passes_test_suite M (Test_Suite PS tps rd_targets separators) M'"
  and     "q' ≠ q''"
  and     "q' ∈ fst d"
  and     "q'' ∈ fst d"
  and     "pR1 ∈ (RP M q q' pP p PS M')"
  and     "pR2 ∈ (RP M q q'' pP p PS M')"
shows "io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}"
proof -

  let ?RP1 = "(RP M q q' pP p PS M')"
  let ?RP2 = "(RP M q q'' pP p PS M')"
  let ?R1  = "(R M q q' pP p)"
  let ?R2  = "(R M q q'' pP p)"

  (* sufficiency properties *)


  have t1: "(initial M, initial_preamble M) ∈ PS" 
    using ‹implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets› 
    unfolding implies_completeness_for_repetition_sets.simps by blast
  have t2: "⋀ q P. (q, P) ∈ PS ⟹ is_preamble P M q"
    using ‹implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets› 
    unfolding implies_completeness_for_repetition_sets.simps by force
  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 (Test_Suite PS tps rd_targets separators) M m repetition_sets› 
    unfolding implies_completeness_for_repetition_sets.simps by force  


  have t5: "⋀q. q ∈ FSM.states M ⟹ (∃d∈set repetition_sets. q ∈ fst d)"
    using ‹implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets› 
    unfolding implies_completeness_for_repetition_sets.simps by force

  have t6: "⋀ q. q ∈ fst ` PS ⟹ 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 (Test_Suite PS tps rd_targets separators) M m repetition_sets› 
    unfolding implies_completeness_for_repetition_sets.simps by auto

  have "⋀ d. d ∈ set repetition_sets ⟹ fst d ⊆ FSM.states M ∧ snd d = fst d ∩ fst ` PS ∧ (∀q1 q2. q1 ∈ fst d ⟶ q2 ∈ fst d ⟶ q1 ≠ q2 ⟶ separators (q1, q2) ≠ {})"
    using ‹implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets› 
    unfolding implies_completeness_for_repetition_sets.simps by force
  then have t7: "⋀ d. d ∈ set repetition_sets ⟹ fst d ⊆ FSM.states M"
  and  t8: "⋀ d. d ∈ set repetition_sets ⟹ snd d ⊆ fst d"
  and  t8': "⋀ d. d ∈ set repetition_sets ⟹ snd d = fst d ∩ fst ` PS"
  and  t9: "⋀ d q1 q2. d ∈ set repetition_sets ⟹ q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ separators (q1, q2) ≠ {}"
    by blast+

  have t10: "⋀ q p d p1 p2 p3.
              q ∈ fst ` PS ⟹
              (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 (Test_Suite PS tps rd_targets separators) M m repetition_sets› 
    unfolding implies_completeness_for_repetition_sets.simps
    by (metis (no_types, lifting)) 

  have t11: "⋀ q p d p1 p2 q'.
              q ∈ fst ` PS ⟹
              (p, d) ∈ m_traversal_paths_with_witness M q repetition_sets m ⟹
              p = p1 @ p2 ⟹
              q' ∈ fst ` PS ⟹
              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 (Test_Suite PS tps rd_targets separators) M m repetition_sets› 
    unfolding implies_completeness_for_repetition_sets.simps
    by (metis (no_types, lifting)) 

  have t12: "⋀ q p d q1 q2.
              q ∈ fst ` PS ⟹
              (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 ‹implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets› 
    unfolding implies_completeness_for_repetition_sets.simps
    by (metis (no_types, lifting)) 


  (* pass properties *)

  have pass1: "⋀ q P io x y y' . (q,P) ∈ PS ⟹ io@[(x,y)] ∈ L P ⟹ io@[(x,y')] ∈ L M' ⟹ io@[(x,y')] ∈ L P" 
    using ‹passes_test_suite M (Test_Suite PS tps rd_targets separators) M'›
    unfolding passes_test_suite.simps
    by meson 

  have pass2: "⋀ q P pP ioT pT x y y' . (q,P) ∈ PS ⟹ 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')))"
    using ‹passes_test_suite M (Test_Suite PS tps rd_targets separators) M'›
    unfolding passes_test_suite.simps by blast

  have pass3: "⋀ q P pP pT q' A d1 d2 qT . (q,P) ∈ PS ⟹ path P (initial P) pP ⟹ target (initial P) pP = q ⟹ pT ∈ tps q ⟹ (p_io pP)@(p_io pT) ∈ L M' ⟹ 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"  
    using ‹passes_test_suite M (Test_Suite PS tps rd_targets separators) M'›
    unfolding passes_test_suite.simps by blast


  (* additional props *)

  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› submachine_path_initial ‹path P (FSM.initial P) pP› 
    unfolding is_preamble_def  
    by blast
  moreover have "target (initial M) pP = q"
    using ‹target (initial P) pP = q› 
    unfolding ‹initial P = initial M› 
    by assumption
  ultimately have "q ∈ states M"
    using path_target_is_state 
    by metis


  have "q ∈ fst ` PS"
    using ‹(q,P) ∈ PS› by force

  have "d ∈ set repetition_sets" 
    using ‹(p, 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]
    using find_set by force

  have "q' ∈ states M"
    by (meson ‹d ∈ set repetition_sets› assms(13) subset_iff t7)
  have "q'' ∈ states M"
    by (meson ‹d ∈ set repetition_sets› assms(14) subset_iff t7)


  have "target (initial M) pR1 = q'"
    using RP_target[OF ‹pR1 ∈ ?RP1› t2 pass1 ‹completely_specified M'› ‹inputs M' = inputs M›] by force
  then have "target (initial M) pR1 ∈ fst d"
    using ‹q' ∈ fst d› by blast
    

  have "target (initial M) pR2 = q''"
    using RP_target[OF ‹pR2 ∈ ?RP2› t2 pass1 ‹completely_specified M'› ‹inputs M' = inputs M›] by force
  then have "target (initial M) pR2 ∈ fst d"
    using ‹q'' ∈ fst d› by blast

  have "pR1 ≠ pR2"
    using ‹target (initial M) pR1 = q'› ‹target (initial M) pR2 = q''› ‹q' ≠ q''› by auto


  obtain A t1 t2 where "(A,t1,t2) ∈ separators (q',q'')"
    using t9[OF ‹d ∈ set repetition_sets› ‹q' ∈ fst d› ‹q'' ∈ fst d› ‹q' ≠ q''›]
    by auto
  have "(A,t2,t1) ∈ separators (q'',q')" and "is_separator M q' q'' A t1 t2"
    using t3[OF ‹(A,t1,t2) ∈ separators (q',q'')›] by simp+
  then have "is_separator M q'' q' A t2 t1"
    using is_separator_sym by force

  show "io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}" 
  proof (rule ccontr) 
    assume "io_targets M' (p_io pR1) (FSM.initial M') ∩ io_targets M' (p_io pR2) (FSM.initial M') ≠ {}"
    then obtain qT where "qT ∈ io_targets M' (p_io pR1) (FSM.initial M')"
                   and   "qT ∈ io_targets M' (p_io pR2) (FSM.initial M')"
      by blast

    then have "qT ∈ states M'"
      using path_target_is_state unfolding io_targets.simps by force

    consider (a) "pR1 ∈ ?R1 ∧ pR2 ∈ ?R2" |
             (b) "pR1 ∈ ?R1 ∧ pR2 ∉ ?R2" |
             (c) "pR1 ∉ ?R1 ∧ pR2 ∈ ?R2" |
             (d) "pR1 ∉ ?R1 ∧ pR2 ∉ ?R2"
      by blast

    then show "False" proof cases
      case a
      then have "pR1 ∈ ?R1" and "pR2 ∈ ?R2" by auto
                
      obtain pR1' where "pR1 = pP@pR1'" using R_component_ob[OF ‹pR1 ∈ ?R1›] by blast
      obtain pR2' where "pR2 = pP@pR2'" using R_component_ob[OF ‹pR2 ∈ ?R2›] by blast

      have "pR1' = take (length pR1') p" and "length pR1' ≤ length p" and "t_target (p ! (length pR1' - 1)) = q'" and "pR1' ≠ []"
        using R_component[of pP pR1' M q q' p] ‹pR1 ∈ ?R1› unfolding ‹pR1 = pP@pR1'› by blast+ 

      have "pR2' = take (length pR2') p" and "length pR2' ≤ length p" and "t_target (p ! (length pR2' - 1)) = q''" and "pR2' ≠ []"
        using R_component[of pP pR2' M q q'' p] ‹pR2 ∈ ?R2› unfolding ‹pR2 = pP@pR2'› by blast+ 

      have "target q pR1' = q'"
        using ‹target (initial M) pR1 = q'› ‹pR1' ≠ []› unfolding target.simps visited_states.simps ‹pR1 = pP@pR1'› by simp 
      then have "target q pR1' ∈ fst d"
        using ‹q' ∈ fst d› by blast

      have "target q pR2' = q''"
        using ‹target (initial M) pR2 = q''› ‹pR2' ≠ []› unfolding target.simps visited_states.simps ‹pR2 = pP@pR2'› by simp 
      then have "target q pR2' ∈ fst d"
        using ‹q'' ∈ fst d› by blast

      have "pR1' ≠ pR2'"
        using ‹pR1 ≠ pR2› unfolding ‹pR1 = pP@pR1'› ‹pR2 = pP@pR2'› by simp
      then have "length pR1' ≠ length pR2'"
        using ‹pR1' = take (length pR1') p› ‹pR2' = take (length pR2') p› by auto
      then consider (a1) "length pR1' < length pR2'" | (a2) "length pR2' < length pR1'"
        using nat_neq_iff by blast 
      then have "pR1' ∈ tps q ∧ pR2' ∈ tps q ∧ q' ∈ rd_targets (q, pR2') ∧ q'' ∈ rd_targets (q, pR1')"
      proof cases
        case a1
        then have "pR2' = pR1' @ (drop (length pR1') pR2')"
          using ‹pR1' = take (length pR1') p› ‹pR2' = take (length pR2') p›
          by (metis append_take_drop_id less_imp_le_nat take_le) 
        then have "p = pR1' @ (drop (length pR1') pR2') @ (drop (length pR2') p)"
          using ‹pR2' = take (length pR2') p›
          by (metis append.assoc append_take_drop_id)

        have "(drop (length pR1') pR2') ≠ []"
          using a1 ‹pR2' = take (length pR2') p› by auto
        have "target q (pR1' @ drop (length pR1') pR2') ∈ fst d"
          using ‹pR2' = pR1' @ (drop (length pR1') pR2')›[symmetric] ‹target q pR2' ∈ fst d› by auto

        show ?thesis
          using t10[OF ‹q ∈ fst ` PS› ‹(p, d) ∈ m_traversal_paths_with_witness M q repetition_sets m› 
                       ‹p = pR1' @ (drop (length pR1') pR2') @ (drop (length pR2') p)› 
                       ‹(drop (length pR1') pR2') ≠ []› ‹target q pR1' ∈ fst d› 
                       ‹target q (pR1' @ drop (length pR1') pR2') ∈ fst d›]
          unfolding ‹pR2' = pR1' @ (drop (length pR1') pR2')›[symmetric] ‹target q pR1' = q'›  ‹target q pR2' = q''›
          using ‹q' ≠ q''›
          by blast
      next
        case a2
        then have "pR1' = pR2' @ (drop (length pR2') pR1')"
          using ‹pR1' = take (length pR1') p› ‹pR2' = take (length pR2') p›
          by (metis append_take_drop_id less_imp_le_nat take_le) 
        then have "p = pR2' @ (drop (length pR2') pR1') @ (drop (length pR1') p)"
          using ‹pR1' = take (length pR1') p›
          by (metis append.assoc append_take_drop_id)

        have "(drop (length pR2') pR1') ≠ []"
          using a2 ‹pR1' = take (length pR1') p› by auto
        have "target q (pR2' @ drop (length pR2') pR1') ∈ fst d"
          using ‹pR1' = pR2' @ (drop (length pR2') pR1')›[symmetric] ‹target q pR1' ∈ fst d› by auto

        show ?thesis
          using t10[OF ‹q ∈ fst ` PS› ‹(p, d) ∈ m_traversal_paths_with_witness M q repetition_sets m›
                       ‹p = pR2' @ (drop (length pR2') pR1') @ (drop (length pR1') p)› 
                       ‹(drop (length pR2') pR1') ≠ []› ‹target q pR2' ∈ fst d› 
                       ‹target q (pR2' @ drop (length pR2') pR1') ∈ fst d›]
          unfolding ‹pR1' = pR2' @ (drop (length pR2') pR1')›[symmetric] ‹target q pR1' = q'› ‹target q pR2' = q''›
          using ‹q' ≠ q''›
          by blast
      qed 
      then have "pR1' ∈ tps q" and "pR2' ∈ tps q" and "q' ∈ rd_targets (q, pR2')" and "q'' ∈ rd_targets (q, pR1')"
        by simp+

      

      have "p_io pP @ p_io pR1' ∈ L M'"
        using language_prefix_append[OF ‹p_io pP @ p_io p ∈ L M'›, of "length pR1'"]
        using ‹pR1' = take (length pR1') p› by simp
      have "pass_separator_ATC M' A qT t2"
        using pass3[OF ‹(q, P) ∈ PS› ‹path P (initial P) pP› ‹target (initial P) pP = q› ‹pR1' ∈ tps q› 
                       ‹p_io pP @ p_io pR1' ∈ L M'› ‹q'' ∈ rd_targets (q, pR1')›, of A t1 t2]
              ‹(A, t1, t2) ∈ separators (q', q'')› ‹qT ∈ io_targets M' (p_io pR1) (FSM.initial M')› 
        unfolding ‹target q pR1' = q'› ‹pR1 = pP @ pR1'› by auto


      have "p_io pP @ p_io pR2' ∈ L M'"
        using language_prefix_append[OF ‹p_io pP @ p_io p ∈ L M'›, of "length pR2'"]
        using ‹pR2' = take (length pR2') p› by simp
      have "pass_separator_ATC M' A qT t1"
        using pass3[OF ‹(q, P) ∈ PS› ‹path P (initial P) pP› ‹target (initial P) pP = q› ‹pR2' ∈ tps q›
                       ‹p_io pP @ p_io pR2' ∈ L M'› ‹q' ∈ rd_targets (q, pR2')›, of A t2 t1]
              ‹(A, t2, t1) ∈ separators (q'', q')› ‹qT ∈ io_targets M' (p_io pR2) (FSM.initial M')› 
        unfolding ‹target q pR2' = q''› ‹pR2 = pP @ pR2'› by auto

      (* the state qT reached by both paths cannot satisfy the ATC that r-distinguishes their respective targets for both targets at the same time *)

      have "qT ≠ qT"
        using pass_separator_ATC_reduction_distinction[OF ‹observable M› ‹observable M'› ‹inputs M' = inputs M› ‹pass_separator_ATC M' A qT t2› ‹pass_separator_ATC M' A qT t1› ‹q' ∈ states M› ‹q'' ∈ states M› ‹q' ≠ q''› ‹qT ∈ states M'› ‹qT ∈ states M'› ‹is_separator M q' q'' A t1 t2› ‹completely_specified M'›]
        by assumption
      then show False
        by simp

    next
      case b

      then have "pR1 ∈ ?R1" and "pR2 ∉ ?R2"
        using ‹pR1 ∈ ?RP1› by auto
                
      obtain pR1' where "pR1 = pP@pR1'" using R_component_ob[OF ‹pR1 ∈ ?R1›] by blast
      

      have "pR1' = take (length pR1') p" and "length pR1' ≤ length p" and "t_target (p ! (length pR1' - 1)) = q'" and "pR1' ≠ []"
        using R_component[of pP pR1' M q q' p] ‹pR1 ∈ ?R1› unfolding ‹pR1 = pP@pR1'› by blast+ 

      have "target q pR1' = q'"
        using ‹target (initial M) pR1 = q'› ‹pR1' ≠ []› unfolding target.simps visited_states.simps ‹pR1 = pP@pR1'› by simp 
      then have "target q pR1' ∈ fst d" and "target q pR1' ≠ q''"
        using ‹q' ∈ fst d› ‹q' ≠ q''› by blast+


      obtain P' where "(q'', P') ∈ PS"
                      "path P' (FSM.initial P') pR2"
                      "target (FSM.initial P') pR2 = q''"
                      "path M (FSM.initial M) pR2" 
                      "target (FSM.initial M) pR2 = q''" 
                      "p_io pR2 ∈ L M'"
                      "RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)"
        using RP_from_R_inserted[OF t2 pass1 ‹completely_specified M'› ‹inputs M' = inputs M› ‹pR2 ∈ ?RP2› ‹pR2 ∉ ?R2›, 
                                 of "λ q P io x y y' . q" "λ q P io x y y' . y"] 
        by blast


      
      have "q'' ∈ fst ` PS" using ‹(q'',P') ∈ PS› by force
      have "p = pR1' @ (drop (length pR1') p)" using ‹pR1' = take (length pR1') p›
        by (metis append_take_drop_id)

      have "pR1' ∈ tps q" and "[] ∈ tps q''" and "target q pR1' ∈ rd_targets (q'', [])" and "q'' ∈ rd_targets (q, pR1')"
        using t11[OF ‹q ∈ fst ` PS› ‹(p, d) ∈ m_traversal_paths_with_witness M q repetition_sets m›
                     ‹p = pR1' @ (drop (length pR1') p)› ‹q'' ∈ fst ` PS› 
                     ‹target q pR1' ∈ fst d› ‹q'' ∈ fst d› ‹target q pR1' ≠ q''›]
        by simp+


      have "p_io pP @ p_io pR1' ∈ L M'"
        using language_prefix_append[OF ‹p_io pP @ p_io p ∈ L M'›, of "length pR1'"]
        using ‹pR1' = take (length pR1') p› by simp
      have "pass_separator_ATC M' A qT t2"
        using pass3[OF ‹(q, P) ∈ PS› ‹path P (initial P) pP› ‹target (initial P) pP = q› ‹pR1' ∈ tps q› 
                       ‹p_io pP @ p_io pR1' ∈ L M'› ‹q'' ∈ rd_targets (q, pR1')›, of A t1 t2]
              ‹(A, t1, t2) ∈ separators (q', q'')› ‹qT ∈ io_targets M' (p_io pR1) (FSM.initial M')› 
        unfolding ‹target q pR1' = q'› ‹pR1 = pP @ pR1'› by auto

      have "pass_separator_ATC M' A qT t1"
        using pass3[OF ‹(q'', P') ∈ PS› ‹path P' (FSM.initial P') pR2› ‹target (FSM.initial P') pR2 = q''› 
                       ‹[] ∈ tps q''› _ ‹target q pR1' ∈ rd_targets (q'', [])›, of A t2 t1 qT]
              ‹(A, t2, t1) ∈ separators (q'', q')› ‹qT ∈ io_targets M' (p_io pR2) (FSM.initial M')› ‹p_io pR2 ∈ L M'›
        unfolding ‹target q pR1' = q'› by auto

      have "qT ≠ qT"
        using pass_separator_ATC_reduction_distinction[OF ‹observable M› ‹observable M'› ‹inputs M' = inputs M› 
                                                          ‹pass_separator_ATC M' A qT t2› 
                                                          ‹pass_separator_ATC M' A qT t1› ‹q' ∈ states M› 
                                                          ‹q'' ∈ states M› ‹q' ≠ q''› ‹qT ∈ states M'› 
                                                          ‹qT ∈ states M'› ‹is_separator M q' q'' A t1 t2› 
                                                          ‹completely_specified M'›]
        by assumption
      then show False
        by simp
    next
      case c
      then have "pR2 ∈ ?R2" and "pR1 ∉ ?R1"
        using ‹pR2 ∈ ?RP2› by auto
                
      obtain pR2' where "pR2 = pP@pR2'" using R_component_ob[OF ‹pR2 ∈ ?R2›] by blast
      

      have "pR2' = take (length pR2') p" 
       and "length pR2' ≤ length p" 
       and "t_target (p ! (length pR2' - 1)) = q''" 
       and "pR2' ≠ []"
        using R_component[of pP pR2' M q q'' p] ‹pR2 ∈ ?R2› 
        unfolding ‹pR2 = pP@pR2'› 
        by blast+ 

      have "target q pR2' = q''"
        using ‹target (initial M) pR2 = q''› ‹pR2' ≠ []› 
        unfolding target.simps visited_states.simps ‹pR2 = pP@pR2'›
        by simp 
      then have "target q pR2' ∈ fst d" and "target q pR2' ≠ q'"
        using ‹q'' ∈ fst d› ‹q' ≠ q''› by blast+


      obtain P' where "(q', P') ∈ PS"
                      "path P' (FSM.initial P') pR1"
                      "target (FSM.initial P') pR1 = q'"
                      "path M (FSM.initial M) pR1" 
                      "target (FSM.initial M) pR1 = q'" 
                      "p_io pR1 ∈ L M'"
                      "RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)"
        using RP_from_R_inserted[OF t2 pass1 ‹completely_specified M'› ‹inputs M' = inputs M› ‹pR1 ∈ ?RP1› ‹pR1 ∉ ?R1›, 
                                 of "λ q P io x y y' . q" "λ q P io x y y' . y"] 
        by blast

      
      have "q' ∈ fst ` PS" using ‹(q',P') ∈ PS› by force
      have "p = pR2' @ (drop (length pR2') p)" using ‹pR2' = take (length pR2') p›
        by (metis append_take_drop_id)

      have "pR2' ∈ tps q" and "[] ∈ tps q'" and "target q pR2' ∈ rd_targets (q', [])" and "q' ∈ rd_targets (q, pR2')"
        using t11[OF ‹q ∈ fst ` PS› ‹(p, d) ∈ m_traversal_paths_with_witness M q repetition_sets m› 
                     ‹p = pR2' @ (drop (length pR2') p)› ‹q' ∈ fst ` PS› ‹target q pR2' ∈ fst d› 
                     ‹q' ∈ fst d› ‹target q pR2' ≠ q'›]
        by simp+


      have "p_io pP @ p_io pR2' ∈ L M'"
        using language_prefix_append[OF ‹p_io pP @ p_io p ∈ L M'›, of "length pR2'"]
        using ‹pR2' = take (length pR2') p› by simp
      have "pass_separator_ATC M' A qT t1"
        using pass3[OF ‹(q, P) ∈ PS› ‹path P (initial P) pP› ‹target (initial P) pP = q› ‹pR2' ∈ tps q› 
                       ‹p_io pP @ p_io pR2' ∈ L M'› ‹q' ∈ rd_targets (q, pR2')›, of A t2 t1]
              ‹(A, t2, t1) ∈ separators (q'', q')› ‹qT ∈ io_targets M' (p_io pR2) (FSM.initial M')› 
        unfolding ‹target q pR2' = q''› ‹pR2 = pP @ pR2'› by auto

      have "pass_separator_ATC M' A qT t2"
        using pass3[OF ‹(q', P') ∈ PS› ‹path P' (FSM.initial P') pR1› ‹target (FSM.initial P') pR1 = q'› 
                       ‹[] ∈ tps q'› _ ‹target q pR2' ∈ rd_targets (q', [])›, of A t1 t2 qT]
              ‹(A, t1, t2) ∈ separators (q', q'')› ‹qT ∈ io_targets M' (p_io pR1) (FSM.initial M')› ‹p_io pR1 ∈ L M'›
        unfolding ‹target q pR2' = q''› by auto

      have "qT ≠ qT"
        using pass_separator_ATC_reduction_distinction[OF ‹observable M› ‹observable M'› ‹inputs M' = inputs M›
                                                          ‹pass_separator_ATC M' A qT t1› ‹pass_separator_ATC M' A qT t2› 
                                                          ‹q'' ∈ states M› ‹q' ∈ states M› _ ‹qT ∈ states M'› ‹qT ∈ states M'› 
                                                          ‹is_separator M q'' q' A t2 t1› ‹completely_specified M'›]
              ‹q' ≠ q''› by simp
      then show False
        by simp
    next
      case d

      then have "pR1 ∉ ?R1" and "pR2 ∉ ?R2"
        by auto
                
      obtain P' where "(q', P') ∈ PS"
                      "path P' (FSM.initial P') pR1"
                      "target (FSM.initial P') pR1 = q'"
                      "path M (FSM.initial M) pR1" 
                      "target (FSM.initial M) pR1 = q'" 
                      "p_io pR1 ∈ L M'"
                      "RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)"
        using RP_from_R_inserted[OF t2 pass1 ‹completely_specified M'› ‹inputs M' = inputs M› 
                                    ‹pR1 ∈ ?RP1› ‹pR1 ∉ ?R1›, of "λ q P io x y y' . q" "λ q P io x y y' . y"] 
        by blast

      have "q' ∈ snd d"
        by (metis IntI ‹(q', P') ∈ PS› ‹d ∈ set repetition_sets› assms(13) fst_eqD image_eqI t8')

      obtain P'' where "(q'', P'') ∈ PS"
                      "path P'' (FSM.initial P'') pR2"
                      "target (FSM.initial P'') pR2 = q''"
                      "path M (FSM.initial M) pR2" 
                      "target (FSM.initial M) pR2 = q''" 
                      "p_io pR2 ∈ L M'"
                      "RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)"
        using RP_from_R_inserted[OF t2 pass1 ‹completely_specified M'› ‹inputs M' = inputs M› ‹pR2 ∈ ?RP2› ‹pR2 ∉ ?R2›, 
                                 of "λ q P io x y y' . q" "λ q P io x y y' . y"] 
        by blast

      have "q'' ∈ snd d"
        by (metis IntI ‹(q'', P'') ∈ PS› ‹d ∈ set repetition_sets› assms(14) fst_eqD image_eqI t8')

      have "[] ∈ tps q'" and "[] ∈ tps q''" and "q' ∈ rd_targets (q'', [])" and "q'' ∈ rd_targets (q', [])"
        using t12[OF ‹q ∈ fst ` PS› ‹(p, d) ∈ m_traversal_paths_with_witness M q repetition_sets m› ‹q' ≠ q''› ‹q' ∈ snd d› ‹q'' ∈ snd d›]
        by simp+


      have "pass_separator_ATC M' A qT t1"
        using pass3[OF ‹(q'', P'') ∈ PS› ‹path P'' (initial P'') pR2› ‹target (initial P'') pR2 = q''› 
                       ‹[] ∈ tps q''› _ ‹q' ∈ rd_targets (q'', [])›, of A t2 t1 qT]
              ‹p_io pR2 ∈ L M'› ‹(A, t2, t1) ∈ separators (q'', q')› ‹qT ∈ io_targets M' (p_io pR2) (FSM.initial M')› 
        by auto
      
      have "pass_separator_ATC M' A qT t2"
        using pass3[OF ‹(q', P') ∈ PS› ‹path P' (initial P') pR1› ‹target (initial P') pR1 = q'› 
                       ‹[] ∈ tps q'› _ ‹q'' ∈ rd_targets (q', [])›, of A t1 t2 qT]
              ‹p_io pR1 ∈ L M'› ‹(A, t1, t2) ∈ separators (q', q'')› ‹qT ∈ io_targets M' (p_io pR1) (FSM.initial M')› 
        by auto

      have "qT ≠ qT"
        using pass_separator_ATC_reduction_distinction[OF ‹observable M› ‹observable M'› 
                                                          ‹inputs M' = inputs M› ‹pass_separator_ATC M' A qT t1›
                                                          ‹pass_separator_ATC M' A qT t2› ‹q'' ∈ states M› 
                                                          ‹q' ∈ states M› _ ‹qT ∈ states M'› ‹qT ∈ states M'› 
                                                          ‹is_separator M q'' q' A t2 t1› ‹completely_specified M'›]
              ‹q' ≠ q''› by simp
      then show False
        by simp
    qed
  qed
qed




lemma passes_test_suite_exhaustiveness :
  assumes "passes_test_suite M (Test_Suite prs tps rd_targets separators) M'"
  and     "implies_completeness (Test_Suite prs tps rd_targets separators) M m"
  and     "observable M" 
  and     "observable M'"
  and     "inputs M' = inputs M"
  and     "inputs M ≠ {}"
  and     "completely_specified M"
  and     "completely_specified M'"
  and     "size M' ≤ m"
shows     "L M' ⊆ L M"
proof (rule ccontr)
  assume "¬ L M' ⊆ L M"

  (* sufficiency properties *)

  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(2) 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"
    using implies_completeness_for_repetition_sets_simps(2)[OF repetition_sets_def] 
    by blast
  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  t8':  "⋀ d. d ∈ set repetition_sets ⟹ snd d = fst d ∩ fst ` prs"
  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 t12: "⋀ q p d q1 q2.
              q ∈ 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 implies_completeness_for_repetition_sets_simps(10)[OF repetition_sets_def] by assumption
  


  (* pass properties *)

  have pass1: "⋀ q P io x y y' . (q,P) ∈ prs ⟹ io@[(x,y)] ∈ L P ⟹ io@[(x,y')] ∈ L M' ⟹ io@[(x,y')] ∈ L P" 
    using ‹passes_test_suite M (Test_Suite prs tps rd_targets separators) M'›
    unfolding passes_test_suite.simps
    by meson 

  have pass2: "⋀ 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')))"
    using ‹passes_test_suite M (Test_Suite prs tps rd_targets separators) M'›
    unfolding passes_test_suite.simps 
    by blast

  have pass3: "⋀ 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 ⟹ (p_io pP)@(p_io pT) ∈ L M' ⟹ 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"  
    using ‹passes_test_suite M (Test_Suite prs tps rd_targets separators) M'›
    unfolding passes_test_suite.simps 
    by blast


  (* seq to failure *)


  obtain pP io where "minimal_sequence_to_failure_extending_preamble_path M M' prs pP io"
    using minimal_sequence_to_failure_extending_preamble_ex[OF t1 ‹¬ L M' ⊆ L M›] 
    by blast

  then have "sequence_to_failure_extending_preamble_path M M' prs pP io" 
            "⋀ io'. sequence_to_failure_extending_preamble_path M M' prs pP io' ⟹ length io ≤ length io'"
    unfolding minimal_sequence_to_failure_extending_preamble_path_def
    by blast+

  obtain q P where "q ∈ states M"
               and "(q,P) ∈ prs"
               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' prs pP io›
    unfolding sequence_to_failure_extending_preamble_path_def 
    by blast

  let ?xF = "fst (last io)"
  let ?yF = "snd (last io)"
  let ?xyF = "(?xF,?yF)"
  let ?ioF = "butlast io"
  have "io ≠ []"
    using ‹((p_io pP) @ io) ∉ L M› ‹((p_io pP) @ butlast io) ∈ L M› by auto
  then have "io = ?ioF@[?xyF]"
    by auto

  have "?xF ∈ inputs M'"
    using language_io(1)[OF ‹((p_io pP) @ io) ∈ L M'›, of ?xF ?yF] ‹io ≠ []› by auto 
  then have "?xF ∈ inputs M"
    using ‹inputs M' = inputs M› by simp

  have "q ∈ fst ` prs"
    using ‹(q,P) ∈ prs› by force
  have "is_preamble P M q"
    using ‹(q,P) ∈ prs› t2 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


  (* io must be a proper extension of some m-traversal path, as all m-traversal paths pass *)
  obtain pM dM ioEx where "(pM,dM) ∈ m_traversal_paths_with_witness M q repetition_sets m"
                    and   "io = (p_io pM)@ioEx"
                    and   "ioEx ≠ []"
  proof -
    
    obtain pF where "path M q pF" and "p_io pF = ?ioF"
      using observable_path_suffix[OF ‹((p_io pP) @ ?ioF) ∈ L M› ‹path M (initial M) pP› ‹observable M› ]
      unfolding ‹target (initial M) pP = q›
      by blast

    obtain tM where "tM ∈ transitions M" and "t_source tM = target q pF" and "t_input tM = ?xF"
      using ‹?xF ∈ inputs M› path_target_is_state[OF ‹path M q pF›]
            ‹completely_specified M›
      unfolding completely_specified.simps
      by blast

    then have "path M q (pF@[tM])"
      using ‹path M q pF› path_append_transition by simp

    show ?thesis proof (cases "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (pF@[tM]))) repetition_sets")
      case None

      (* if no repetition_sets witness exists for (pF@[tM]), then it is a proper prefix of some m-traversal path and hence also in L M, providing a contradiction*)

      obtain pF' d' where "((pF@[tM]) @ pF', 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 (pF@[tM])› None]
        by blast
      then have "(pF@[tM]) @ pF' ∈ tps q"
        using t6[OF ‹q ∈ fst ` prs›] by force

      have "(p_io pF) @ [(?xF,t_output tM)] ∈ set (prefixes (p_io ((pF@[tM])@pF')))"
        using ‹t_input tM = ?xF›
        unfolding prefixes_set by auto

      have "p_io pP @ p_io pF @ [?xyF] ∈ L M'"
        using ‹((p_io pP) @ io) ∈ L M'› unfolding ‹p_io pF = ?ioF› ‹io = ?ioF@[?xyF]›[symmetric] by assumption

      obtain pT' where "pT' ∈ tps q" 
                 and   "p_io pF @ [(fst (last io), snd (last io))] ∈ set (prefixes (p_io pT'))"
        using pass2[OF ‹(q,P) ∈ prs› ‹path P (initial P) pP› ‹target (initial P) pP = q› ‹(pF@[tM]) @ pF' ∈ tps q› 
                       ‹(p_io pF) @ [(?xF,t_output tM)] ∈ set (prefixes (p_io ((pF@[tM])@pF')))› ‹p_io pP @ p_io pF @ [?xyF] ∈ L M'›]
        by blast

      have "path M q pT'"
      proof -
        obtain pT'' d'' where "(pT'@pT'', d'') ∈ m_traversal_paths_with_witness M q repetition_sets m"
          using ‹pT' ∈ tps q› t6[OF ‹q ∈ fst ` prs›] 
          by blast
        then have "path M q (pT'@pT'')"
          using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›] 
          by force
        then show ?thesis 
          by auto
      qed
      then have "path M (initial M) (pP@pT')"
        using ‹path M (initial M) pP› ‹target (initial M) pP = q› by auto
      then have "(p_io (pP@pT')) ∈ L M"
        unfolding LS.simps by blast
      then have "(p_io pP)@(p_io pT') ∈ L M"
        by auto
      


      have "io ∈ set (prefixes (p_io pT'))"
        using ‹p_io pF @ [(fst (last io), snd (last io))] ∈ set (prefixes (p_io pT'))›
        unfolding ‹p_io pF = ?ioF› ‹io = ?ioF@[?xyF]›[symmetric] by assumption
      then obtain io' where "p_io pT' = io @ io'"
        unfolding prefixes_set mem_Collect_eq by metis
      
      have " p_io pP @ io ∈ L M"
        using ‹(p_io pP)@(p_io pT') ∈ L M› 
        unfolding ‹p_io pT' = io @ io'›
        unfolding append.assoc[symmetric]
        using language_prefix[of "p_io pP @ io" io', of M "initial M"] 
        by blast
      
      then show ?thesis
        using ‹(p_io pP) @ io ∉ L M› by simp
    next
      case (Some d)

      (* get the shortest prefix of pF that still has a RepSet witness *)

      let ?ps = "{ p1 . ∃ p2 . (pF@[tM]) = p1 @ p2 ∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p1)) repetition_sets ≠ None}"

      have "finite ?ps"
      proof -
        have "?ps ⊆ set (prefixes (pF@[tM]))"
          unfolding prefixes_set by force
        moreover have "finite (set (prefixes (pF@[tM])))"
          by simp
        ultimately show ?thesis
          by (simp add: finite_subset) 
      qed
      moreover have "?ps ≠ {}"
      proof -
        have "pF @ [tM] = (pF @ [tM]) @ [] ∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (pF @ [tM]))) repetition_sets ≠ None"
          using Some by auto
        then have "(pF@[tM]) ∈ ?ps"
          by blast
        then show ?thesis by blast
      qed
      ultimately obtain pMin where "pMin ∈ ?ps" and "⋀ p' . p' ∈ ?ps ⟹ length pMin ≤ length p'"
        by (meson leI min_length_elem) 

      obtain pMin' dMin where "(pF@[tM]) = pMin @ pMin'"
                          and "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) pMin)) repetition_sets = Some dMin"
        using ‹pMin ∈ ?ps› by blast
      then have "path M q pMin"
        using ‹path M q (pF@[tM])› by auto

      moreover have "(∀p' p''. pMin = 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''. pMin = 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 "pMin = p' @ p''" and "p'' ≠ []"
          show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None"
          proof (rule ccontr) 
            assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets ≠ None"
            then have "p' ∈ ?ps"
              using ‹(pF@[tM]) = pMin @ pMin'› unfolding ‹pMin = p' @ p''› append.assoc by blast
            
            have "length p' < length pMin"
              using ‹pMin = p' @ p''› ‹p'' ≠ []› by auto
            then show "False"
              using ‹⋀ p' . p' ∈ ?ps ⟹ length pMin ≤ length p'›[OF ‹p' ∈ ?ps›] by simp
          qed
        qed
        then show ?thesis by blast
      qed
      
      ultimately have "(pMin,dMin) ∈ m_traversal_paths_with_witness M q repetition_sets m"
        using ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) pMin)) repetition_sets = Some dMin›
              m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m]
        by blast
      then have "pMin ∈ tps q"
        using t6[OF ‹q ∈ fst ` prs›]
        by force
  
      show ?thesis proof (cases "pMin = (pF@[tM])")
        (* if the m-traversal path is not shorter than io, then again the failure is observed *)
        case True 
        then have "?ioF @ [(?xF, t_output tM)] ∈ set (prefixes (p_io pMin))"
          using ‹p_io pF = ?ioF› ‹t_input tM = ?xF› unfolding prefixes_set by force

        obtain pMinF where "pMinF ∈ tps q" and "io ∈ set (prefixes (p_io pMinF))"
          using pass2[OF ‹(q,P) ∈ prs› ‹path P (initial P) pP› ‹target (initial P) pP = q› ‹pMin ∈ tps q› ‹?ioF @ [(?xF, t_output tM)] ∈ set (prefixes (p_io pMin))›, of ?yF]
          using ‹p_io pP @ io ∈ L M'›
          unfolding ‹io = ?ioF@[?xyF]›[symmetric]
          by blast

        have "path M q pMinF"
        proof -
          obtain pT'' d'' where "(pMinF@pT'', d'') ∈ m_traversal_paths_with_witness M q repetition_sets m"
            using ‹pMinF ∈ tps q› t6[OF ‹q ∈ fst ` prs›] by blast
          then have "path M q (pMinF@pT'')"
            using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›] 
            by force
          then show ?thesis by auto
        qed
        then have "path M (initial M) (pP@pMinF)"
          using ‹path M (initial M) pP› ‹target (initial M) pP = q› by auto
        then have "(p_io (pP@pMinF)) ∈ L M"
          unfolding LS.simps by blast
        then have "(p_io pP)@(p_io pMinF) ∈ L M"
          by auto
        
        obtain io' where "p_io pMinF = io @ io'"
          using ‹io ∈ set (prefixes (p_io pMinF))›
          unfolding prefixes_set mem_Collect_eq by metis
        
        have " p_io pP @ io ∈ L M"
          using ‹(p_io pP)@(p_io pMinF) ∈ L M› 
          unfolding ‹p_io pMinF = io @ io'›
          unfolding append.assoc[symmetric]
          using language_prefix[of "p_io pP @ io" io', of M "initial M"] 
          by blast        
        then show ?thesis
          using ‹(p_io pP) @ io ∉ L M› by simp
      next
        case False
        then obtain pMin'' where "pF = pMin @ pMin''"
          using ‹(pF@[tM]) = pMin @ pMin'›
          by (metis butlast_append butlast_snoc) 
        then have "io = (p_io pMin) @ (p_io pMin'') @ [?xyF]"
          using ‹io = ?ioF @ [?xyF]› ‹p_io pF = ?ioF›
          by (metis (no_types, lifting) append_assoc map_append)
        then show ?thesis 
          using that[OF ‹(pMin,dMin) ∈ m_traversal_paths_with_witness M q repetition_sets m›, of "(p_io pMin'') @ [?xyF]"] 
          by auto
      qed
    qed
  qed


  (* collect length properties on pM to ultimately show that M' must have at least m+1 states *)

  have "p_io pP @ p_io pM ∈ L M'"
    using ‹((p_io pP) @ io) ∈ L M'› unfolding ‹io = (p_io pM)@ioEx› append.assoc[symmetric]
    using language_prefix[of "p_io pP @ p_io pM" ioEx M' "initial M'"] by blast

  have no_shared_targets_for_distinct_states : "⋀ q' q'' pR1 pR2. q' ≠ q'' ⟹
                                                  q' ∈ fst dM ⟹
                                                  q'' ∈ fst dM ⟹
                                                  pR1 ∈ RP M q q' pP pM prs M' ⟹
                                                  pR2 ∈ RP M q q'' pP pM prs M' ⟹ 
                                                  io_targets M' (p_io pR1) (initial M') ∩ io_targets M' (p_io pR2) (initial M') = {}"
    using passes_test_suite_exhaustiveness_helper_1[OF ‹completely_specified M'› ‹inputs M' = inputs M› ‹observable M› ‹observable M'› ‹(q,P) ∈ prs› ‹path P (initial P) pP› ‹target (FSM.initial P) pP = q› ‹p_io pP @ p_io pM ∈ L M'› ‹(pM, dM) ∈ m_traversal_paths_with_witness M q repetition_sets m› repetition_sets_def ‹passes_test_suite M (Test_Suite prs tps rd_targets separators) M'›]
    by blast



  have "path M q pM"
  and  "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) pM)) repetition_sets = Some dM"
    using ‹(pM,dM) ∈ 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 force+
  then have "path M (target (FSM.initial M) pP) pM"
    unfolding ‹(target (FSM.initial M) pP) = q› by simp

  have "dM ∈ set repetition_sets"
    using find_set[OF ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) pM)) repetition_sets = Some dM›] by assumption
  have "Suc (m - card (snd dM)) ≤ length (filter (λt. t_target t ∈ fst dM) pM)"
    using find_condition[OF ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) pM)) repetition_sets = Some dM›] by assumption

  obtain ioX where "butlast io = (p_io pM)@ioX"
    using ‹io = (p_io pM)@ioEx›
    by (simp add: ‹ioEx ≠ []› butlast_append) 


  have RP_card : "⋀ q' . card (⋃pR∈RP M (target (FSM.initial M) pP) q' pP pM prs M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP pM prs M')"
  and  RP_targets: "⋀ q' pR . pR ∈ RP M (target (FSM.initial M) pP) q' pP pM prs M' ⟹ ∃q. io_targets M' (p_io pR) (FSM.initial M') = {q}"
  and  no_shared_targets_for_identical_states: "⋀ q' pR1 pR2 . pR1 ∈ RP M (target (FSM.initial M) pP) q' pP pM prs M' ⟹ pR2 ∈ RP M (target (FSM.initial M) pP) q' pP pM prs M' ⟹ pR1 ≠ pR2 ⟹ io_targets M' (p_io pR1) (FSM.initial M') ∩ io_targets M' (p_io pR2) (FSM.initial M') = {}"
    using RP_count[OF ‹minimal_sequence_to_failure_extending_preamble_path M M' prs pP io› ‹observable M› ‹observable M'› t2 ‹path M (target (FSM.initial M) pP) pM› ‹butlast io = (p_io pM)@ioX› pass1 ‹completely_specified M'› ‹inputs M' = inputs M›, of "λ q P io x y y' . q" "λ q P io x y y' . y"]
    by blast+

  have snd_dM_prop: "⋀ q' . q' ∈ snd dM ⟹ (⋃ pR ∈ (RP M q q' pP pM prs M') . io_targets M' (p_io pR) (initial M')) ≠ (⋃ pR ∈ (R M q q' pP pM) . io_targets M' (p_io pR) (initial M'))"
  proof -
    fix q' assume "q' ∈ snd dM"

    let ?RP = "(RP M q q' pP pM prs M')"
    let ?R  = "(R M q q' pP pM)"
    let ?P  = "λ pP' . ∃P'. (q', P') ∈ prs ∧ path P' (FSM.initial P') pP' ∧ target (FSM.initial P') pP' = q' ∧ p_io pP' ∈ L M'"

    
    obtain PQ where "(q',PQ) ∈ prs"
      using ‹q' ∈ snd dM› t8'[OF ‹dM ∈ set repetition_sets›] by auto
    then have "is_preamble PQ M q'" and "∃P'. (q', P') ∈ prs"
      using t2 by blast+

    obtain pq where "path PQ (initial PQ) pq" and "target (initial PQ) pq = q'" and "p_io pq ∈ L M'"
      using preamble_pass_path[OF ‹is_preamble PQ M q'› pass1[OF ‹(q',PQ) ∈ prs›] ‹completely_specified M'› ‹inputs M' = inputs M›] 
      by force
    then have "∃ pP' . ?P pP'"
      using ‹(q',PQ) ∈ prs› by blast

    define pPQ where pPQ_def: "pPQ = (SOME pP'. ?P pP')"

    have "?P pPQ"
      unfolding pPQ_def using someI_ex[OF ‹∃ pP' . ?P pP'›] by assumption
    then obtain PQ' where "(q',PQ') ∈ prs" 
                      and "path PQ' (initial PQ') pPQ" 
                      and "target (initial PQ') pPQ = q'" 
                      and "p_io pPQ ∈ L M'"
      by blast

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

    obtain pPQ' where "path M' (initial M') pPQ'" and "p_io pPQ' = p_io pPQ"
      using ‹p_io pPQ ∈ L M'› by auto

    then have "io_targets M' (p_io pPQ) (initial M') = {target (initial M') pPQ'}"
      using ‹observable M'› by (metis (mono_tags, lifting) observable_path_io_target) 
    
    moreover have "target (initial M') pPQ' ∉ (⋃ (image (λ pR . io_targets M' (p_io pR) (initial M')) ?R))"
    proof 
      assume "target (initial M') pPQ' ∈ (⋃ (image (λ pR . io_targets M' (p_io pR) (initial M')) ?R))"
      then obtain pR where "pR ∈ ?R" and "target (initial M') pPQ' ∈ io_targets M' (p_io pR) (initial M')"
        by blast

      obtain pR' where "pR = pP@pR'"
        using R_component_ob[OF ‹pR ∈ ?R›] by blast
      then have "pP@pR' ∈ ?R"
        using ‹pR ∈ ?R› by simp
      have "pR' = take (length pR') pM" 
       and "length pR' ≤ length pM" 
       and "t_target (pM ! (length pR' - 1)) = q'" 
       and "pR' ≠ []"
        using R_component[OF ‹pP@pR' ∈ ?R›] 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) (pM@pX)" and "p_io (pM@pX) = butlast io"
      proof -
        have "p_io pP @ p_io pM @ ioX ∈ L M"
          using ‹((p_io pP) @ butlast io) ∈ L M› 
          unfolding ‹butlast io = p_io pM @ 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 pM @ ioX"
          using language_state_split[OF ‹p_io pP @ p_io pM @ 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 pM @ ioX ∈ LS M (target (initial M) pP)"
          using ‹p_io p23 = p_io pM @ 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 pM" 
                       and "p_io p3 = ioX"
          using language_state_split[OF ‹p_io pM @ ioX ∈ LS M (target (initial M) pP)›] 
          by blast
    
        have "p2 = pM"
          using observable_path_unique[OF ‹observable M› ‹path M (target (FSM.initial M) pP) p2› 
                                          ‹path M (target (FSM.initial M) pP) pM› ‹p_io p2 = p_io pM›] 
          by assumption
        then have "path M (target (FSM.initial M) pP) (pM@p3)"
          using ‹path M (target (FSM.initial M) pP) pM› ‹path M (target (target (FSM.initial M) pP) p2) p3› 
          by auto
        moreover have "p_io (pM@p3) = butlast io"
          unfolding ‹butlast io = p_io pM @ ioX› using ‹p_io p3 = ioX› 
          by auto
        ultimately show ?thesis 
          using that[of p3] by simp
      qed

      obtain pP' pIO where "path M' (FSM.initial M') pP'" 
                       and "path M' (target (FSM.initial M') pP') pIO" 
                       and "p_io pP' = p_io pP"
                       and "p_io pIO = io"
        using language_state_split[OF ‹((p_io pP) @ io) ∈ L M'›] 
        by blast
  
      have "target (initial M') pP' ∈ io_targets M' (p_io pP) (FSM.initial M')"
        using ‹path M' (FSM.initial M') pP'› 
        unfolding ‹p_io pP' = p_io pP›[symmetric] 
        by auto

      let ?i = "length pR' - 1"
      have "?i < length pR'"
        using ‹pR' ≠ []› by auto
      have "?i < length (butlast io)"
        using ‹pR' = take (length pR') pM› ‹pR' ≠ []›
        unfolding ‹p_io (pM@pX) = butlast io›[symmetric] 
        using leI by fastforce 

      have "t_target ((pM @ pX) ! (length pR' - 1)) = q'"
        by (metis ‹length pR' - 1 < length pR'› ‹length pR' ≤ length pM› ‹t_target (pM ! (length pR' - 1)) = q'› 
              dual_order.strict_trans1 nth_append) 
      then have "(t_target ((pM @ pX) ! (length pR' - 1)), PQ') ∈ prs"
        using ‹(q',PQ') ∈ prs› by simp
      have "target (FSM.initial PQ') pPQ = t_target ((pM @ pX) ! (length pR' - 1))"
        using ‹t_target ((pM @ pX) ! (length pR' - 1)) = q'› ‹target (FSM.initial PQ') pPQ = q'› 
        by blast


      have "t_target (pIO ! ?i) ∉ io_targets M' (p_io pPQ) (FSM.initial M')"
        using minimal_sequence_to_failure_extending_preamble_no_repetitions_with_other_preambles
          [OF ‹minimal_sequence_to_failure_extending_preamble_path M M' prs pP io› ‹observable M› ‹
              path M (target (initial M) pP) (pM@pX)› ‹p_io (pM@pX) = butlast io›
              ‹target (initial M') pP' ∈ io_targets M' (p_io pP) (FSM.initial M')› 
              ‹path M' (target (FSM.initial M') pP') pIO› ‹p_io pIO = io› t2
              ‹?i < length (butlast io)› ‹(t_target ((pM @ pX) ! (length pR' - 1)), PQ') ∈ prs›
              ‹path PQ' (initial PQ') pPQ› ‹target (FSM.initial PQ') pPQ = t_target ((pM @ pX) ! (length pR' - 1))›]
        by blast

      moreover have "io_targets M' (p_io pPQ) (FSM.initial M') = {target (initial M') pPQ'}"
        using ‹path M' (initial M') pPQ'›
        using ‹io_targets M' (p_io pPQ) (FSM.initial M') = {target (FSM.initial M') pPQ'}› ‹p_io pPQ' = p_io pPQ› by auto 
      moreover have "io_targets M' (p_io (pP@pR')) (FSM.initial M') = {t_target (pIO ! ?i)}"
      proof -
        have "(take (length pR') pIO) ≠ []" 
          using ‹p_io pIO = io› ‹?i < length pR'›
          using ‹io = p_io pM @ ioEx› ‹pR' = take (length pR') pM› by auto
        moreover have "pIO ! ?i = last (take (length pR') pIO)" 
          using ‹p_io pIO = io› ‹?i < length pR'›
          by (metis (no_types, lifting) ‹io = p_io pM @ ioEx› ‹length pR' ≤ length pM› ‹pR' = take (length pR') pM› 
                butlast.simps(1) last_conv_nth length_butlast length_map neq_iff nth_take take_le take_map)
        ultimately have "t_target (pIO ! ?i) = target (target (FSM.initial M') pP') (take (length pR') pIO)"
          unfolding target.simps visited_states.simps
          by (simp add: last_map) 
        then have "t_target (pIO ! ?i) = target (initial M') (pP' @ (take (length pR') pIO))"
          by auto 
          
        have "path M' (target (FSM.initial M') pP') (take (length pR') pIO)"
          using ‹path M' (target (FSM.initial M') pP') pIO›
          by (simp add: path_prefix_take) 
        then have "path M' (initial M') (pP' @ (take (length pR') pIO))"
          using ‹path M' (FSM.initial M') pP'› by auto
        moreover have "p_io (pP' @ (take (length pR') pIO)) = (p_io (pP@pR'))"
        proof -
          have "p_io (take (length pR') pIO) = p_io pR'"
            using ‹p_io pIO = io› ‹pR' = take (length pR') pM› ‹p_io (pM@pX) = butlast io› ‹length pR' ≤ length pM›
            by (metis (no_types, lifting) ‹io = p_io pM @ ioEx› length_map take_le take_map) 
          then show ?thesis
            using ‹p_io pP' = p_io pP› by auto
        qed
        ultimately have "io_targets M' (p_io (pP@pR')) (FSM.initial M') = {target (initial M') (pP' @ (take (length pR') pIO))}"
          by (metis (mono_tags, lifting) assms(4) observable_path_io_target)

        then show ?thesis
          unfolding ‹t_target (pIO ! ?i) = target (initial M') (pP' @ (take (length pR') pIO))›
          by assumption
      qed

      ultimately have "target (initial M') pPQ' ∉ io_targets M' (p_io pR) (initial M')"
        unfolding ‹pR = pP@pR'› by auto
      then show "False"
        using ‹target (initial M') pPQ' ∈ io_targets M' (p_io pR) (initial M')›
        by blast
    qed

    ultimately have "io_targets M' (p_io pPQ) (initial M') ∩ (⋃ (image (λ pR . io_targets M' (p_io pR) (initial M')) ?R)) = {}"
      by force

    then show "(⋃ pR ∈ (RP M q q' pP pM prs M') . io_targets M' (p_io pR) (initial M')) ≠ (⋃ pR ∈ (R M q q' pP pM) . io_targets M' (p_io pR) (initial M'))"
      unfolding ‹?RP = insert pPQ (R M q q' pP pM)›
      using ‹io_targets M' (p_io pPQ) (FSM.initial M') = {target (FSM.initial M') pPQ'}› 
      by force
  qed

  (* create a function that separates the additional entries for the preambles in the RP sets of states in (snd dM) *)

  then obtain f where f_def: "⋀ q' . q' ∈ snd dM ⟹ (RP M q q' pP pM prs M') = insert (f q') (R M q q' pP pM) ∧ (f q') ∉ (R M q q' pP pM)"
  proof -
    define f where f_def : "f = (λ q' . SOME p . (RP M q q' pP pM prs M') = insert p (R M q q' pP pM) ∧ p ∉ (R M q q' pP pM))"

    have "⋀ q' . q' ∈ snd dM ⟹ (RP M q q' pP pM prs M') = insert (f q') (R M q q' pP pM) ∧ (RP M q q' pP pM prs M') ≠ (R M q q' pP pM)"
    proof -
      fix q' assume "q' ∈ snd dM"

      have "(⋃pR∈RP M q q' pP pM prs M'. io_targets M' (p_io pR) (FSM.initial M')) ≠ (⋃pR∈R M q q' pP pM. io_targets M' (p_io pR) (FSM.initial M'))"
        using snd_dM_prop[OF ‹q' ∈ snd dM›]
        by assumption
      then have "(RP M q q' pP pM prs M') ≠ (R M q q' pP pM)"
        by blast
      then obtain x where "(RP M q q' pP pM prs M') = insert x (R M q q' pP pM)"
        using RP_from_R[OF t2 pass1 ‹completely_specified M'› ‹inputs M' = inputs M›, of prs "λ q P io x y y' . q" "λ q P io x y y' . y" q q' pP pM]
        by force
      then have "x ∉ (R M q q' pP pM)"
        using ‹(RP M q q' pP pM prs M') ≠ (R M q q' pP pM)›
        by auto 
      then have "∃ p . (RP M q q' pP pM prs M') = insert p (R M q q' pP pM) ∧ p ∉ (R M q q' pP pM)"
        using ‹(RP M q q' pP pM prs M') = insert x (R M q q' pP pM)› by blast

      show "(RP M q q' pP pM prs M') = insert (f q') (R M q q' pP pM) ∧ (RP M q q' pP pM prs M') ≠ (R M q q' pP pM)"
        using someI_ex[OF ‹∃ p . (RP M q q' pP pM prs M') = insert p (R M q q' pP pM) ∧ p ∉ (R M q q' pP pM)›]
        unfolding f_def by auto 
    qed

    then show ?thesis using that by force
  qed



  (* 
     combine counting results on RP (from R) to show that the path along pM collects 
     at least m+1 distinct io-targets (i.e. visites at least m+1 distinct states) in M' 
   *)


  have "(∑ q' ∈ fst dM . card (⋃ pR ∈ (RP M q q' pP pM prs M') . io_targets M' (p_io pR) (initial M'))) ≥ Suc m"
  proof -

    have "⋀ nds . finite nds ⟹ nds ⊆ fst dM ⟹ (∑ q' ∈ nds . card (RP M q q' pP pM prs M')) ≥ length (filter (λt. t_target t ∈ nds) pM) + card (nds ∩ snd dM)"
    proof -
      fix nds assume "finite nds" and "nds ⊆ fst dM"
      then show "(∑ q' ∈ nds . card (RP M q q' pP pM prs M')) ≥ length (filter (λt. t_target t ∈ nds) pM) + card (nds ∩ snd dM)"
      proof induction
        case empty
        then show ?case by auto
      next
        case (insert q' nds)
        then have leq1: "length (filter (λt. t_target t ∈ nds) pM) + card (nds ∩ snd dM) ≤ (∑q'∈nds. card (RP M q q' pP pM prs M'))"
          by blast

        have p4: "(card (R M q q' pP pM)) = length (filter (λt. t_target t = q') pM)" 
        using ‹path M q pM› proof (induction pM rule: rev_induct)
          case Nil
          then show ?case unfolding R_def by auto
        next
          case (snoc t pM)
          then have "path M q pM" and "card (R M q q' pP pM) = length (filter (λt. t_target t = q') pM)"
            by auto

          show ?case proof (cases "target q (pM @ [t]) = q'")
            case True
            then have "(R M q q' pP (pM @ [t])) = insert (pP @ pM @ [t]) (R M q q' pP pM)"
              unfolding R_update[of M q q' pP pM t] by simp
            moreover have "(pP @ pM @ [t]) ∉ (R M q q' pP pM)"
              unfolding R_def by auto
            ultimately have "card (R M q q' pP (pM @ [t])) = Suc (card (R M q q' pP pM))"
              using finite_R[OF ‹path M q pM›, of q' pP] by simp 
            then show ?thesis 
              using True unfolding ‹card (R M q q' pP pM) = length (filter (λt. t_target t = q') pM)› by auto
          next
            case False
            then have "card (R M q q' pP (pM @ [t])) = card (R M q q' pP pM)"
              unfolding R_update[of M q q' pP pM t] by simp
            then show ?thesis 
              using False unfolding ‹card (R M q q' pP pM) = length (filter (λt. t_target t = q') pM)› by auto
          qed 
        qed

        show ?case proof (cases "q' ∈ snd dM")
          case True
          then have p0: "(RP M q q' pP pM prs M') = insert (f q') (R M q q' pP pM)" and "(f q') ∉ (R M q q' pP pM)"
            using f_def by blast+
          then have "card (RP M q q' pP pM prs M') = Suc (card (R M q q' pP pM))"
            by (simp add: ‹path M q pM› finite_R)
          then have p1: "(∑q' ∈ (insert q' nds). card (RP M q q' pP pM prs M')) = (∑q'∈nds. card (RP M q q' pP pM prs M')) + Suc (card (R M q q' pP pM))"
            by (simp add: insert.hyps(1) insert.hyps(2))

          have p2: "length (filter (λt. t_target t ∈ insert q' nds) pM) = length (filter (λt. t_target t ∈ nds) pM) + length (filter (λt. t_target t = q') pM)"
            using ‹q' ∉ nds› by (induction pM; auto)
          have p3: "card ((insert q' nds) ∩ snd dM) = Suc (card (nds ∩ snd dM))"
            using True ‹finite nds› ‹q' ∉ nds› by simp

          show ?thesis 
            using leq1
            unfolding  p1 p2 p3 p4 by simp
        next
          case False

          have "card (RP M q q' pP pM prs M') ≥ (card (R M q q' pP pM))"
          proof (cases "(RP M q q' pP pM prs M') = (R M q q' pP pM)")
            case True
            then show ?thesis using finite_R[OF ‹path M q pM›, of q' pP] by auto
          next
            case False
            then obtain pX where "(RP M q q' pP pM prs M') = insert pX (R M q q' pP pM)"
              using RP_from_R[OF t2 pass1 ‹completely_specified M'› ‹inputs M' = inputs M›, of prs "λ q P io x y y' . q" "λ q P io x y y' . y" q q' pP pM] 
              by force
            then show ?thesis using finite_R[OF ‹path M q pM›, of q' pP]
              by (simp add: card_insert_le) 
          qed
          then have p1: "(∑q' ∈ (insert q' nds). card (RP M q q' pP pM prs M')) ≥ ((∑q'∈nds. card (RP M q q' pP pM prs M')) + (card (R M q q' pP pM)))"
            by (simp add: insert.hyps(1) insert.hyps(2))


          have p2: "length (filter (λt. t_target t ∈ insert q' nds) pM) = length (filter (λt. t_target t ∈ nds) pM) + length (filter (λt. t_target t = q') pM)"
            using ‹q' ∉ nds› by (induction pM; auto)
          have p3: "card ((insert q' nds) ∩ snd dM) = (card (nds ∩ snd dM))"
            using False ‹finite nds› ‹q' ∉ nds› by simp

          have "length (filter (λt. t_target t ∈ nds) pM) + length (filter (λt. t_target t = q') pM) + card (nds ∩ snd dM) ≤ (∑q'∈nds. card (RP M q q' pP pM prs M')) + length (filter (λt. t_target t = q') pM)"
            using leq1 add_le_cancel_right by auto 

          then show ?thesis 
            using p1 
            unfolding p2 p3 p4 by simp
        qed
      qed 
    qed

    moreover have "finite (fst dM)"
      using t7[OF ‹dM ∈ set repetition_sets›] fsm_states_finite[of M]
      using rev_finite_subset by auto 
    ultimately have "(∑ q' ∈ fst dM . card (RP M q q' pP pM prs M')) ≥ length (filter (λt. t_target t ∈ fst dM) pM) + card (fst dM ∩ snd dM)"
      by blast
    have "(fst dM ∩ snd dM) = (snd dM)"
      using t8[OF ‹dM ∈ set repetition_sets›] by blast
    have "(∑ q' ∈ fst dM . card (RP M q q' pP pM prs M')) ≥ length (filter (λt. t_target t ∈ fst dM) pM) + card (snd dM)"
      using ‹(∑ q' ∈ fst dM . card (RP M q q' pP pM prs M')) ≥ length (filter (λt. t_target t ∈ fst dM) pM) + card (fst dM ∩ snd dM)› 
      unfolding ‹(fst dM ∩ snd dM) = (snd dM)› 
      by assumption
    moreover have "(∑q'∈fst dM. card (⋃pR∈RP M q q' pP pM prs M'. io_targets M' (p_io pR) (FSM.initial M'))) = (∑ q' ∈ fst dM . card (RP M q q' pP pM prs M'))"
      using RP_card ‹FSM.initial P = FSM.initial M› ‹target (FSM.initial P) pP = q› by auto 
    ultimately have "(∑q'∈fst dM. card (⋃pR∈RP M q q' pP pM prs M'. io_targets M' (p_io pR) (FSM.initial M'))) ≥ length (filter (λt. t_target t ∈ fst dM) pM) + card (snd dM)"
      by linarith
    moreover have "Suc m ≤ length (filter (λt. t_target t ∈ fst dM) pM) + card (snd dM)"
      using ‹Suc (m - card (snd dM)) ≤ length (filter (λt. t_target t ∈ fst dM) pM)›
      by linarith 
    ultimately show ?thesis 
      by linarith
  qed


  moreover have "(∑ q' ∈ fst dM . card (⋃ pR ∈ (RP M q q' pP pM prs M') . io_targets M' (p_io pR) (initial M'))) ≤ card (states M')"
  proof -
    have "finite (fst dM)"
      by (meson ‹dM ∈ set repetition_sets› fsm_states_finite rev_finite_subset t7) 

    have "(⋀x1. finite (RP M q x1 pP pM prs M'))"
      using finite_RP[OF ‹path M q pM› t2 pass1 ‹completely_specified M'› ‹inputs M' = inputs M›] by force

    have "(⋀y1. finite (io_targets M' (p_io y1) (FSM.initial M')))"
      by (meson io_targets_finite)

    have "(⋀y1. io_targets M' (p_io y1) (FSM.initial M') ⊆ states M')"
      by (meson io_targets_states)
      
    show ?thesis 
      using distinct_union_union_card
        [ of "fst dM" "λ q' . (RP M q q' pP pM prs M')" "λ pR . io_targets M' (p_io pR) (initial M')"
        , OF ‹finite (fst dM)›
             no_shared_targets_for_distinct_states
             no_shared_targets_for_identical_states
             ‹(⋀x1. finite (RP M q x1 pP pM prs M'))›
             io_targets_finite
             io_targets_states
             fsm_states_finite[of M']] 
      unfolding ‹(target (FSM.initial M) pP) = q› by force
  qed

  (* create a contradiction due to the assumption that M' has at most m states *)

  moreover have "card (states M') ≤ m"
    using ‹size M' ≤ m› by auto

  ultimately show False
    by linarith
qed


subsection ‹Completeness of Sufficient Test Suites›

text ‹This subsection combines the soundness and exhaustiveness properties of sufficient test suites
      to show completeness: for any System Under Test with at most m states a test suite sufficient 
      for m passes if and only if the System Under Test is a reduction of the specification.›


lemma passes_test_suite_completeness :
  assumes "implies_completeness T M m"
  and     "observable M" 
  and     "observable M'"
  and     "inputs M' = inputs M"
  and     "inputs M ≠ {}"
  and     "completely_specified M"
  and     "completely_specified M'"
  and     "size M' ≤ m"
shows     "(L M' ⊆ L M) ⟷ passes_test_suite M T M'"
  using passes_test_suite_exhaustiveness[OF _ _ assms(2-8)]
        passes_test_suite_soundness[OF _ assms(2,3,4,6)] 
        assms(1) 
        test_suite.exhaust[of T]
  by metis




subsection ‹Additional Test Suite Properties›

(* Whether a (sufficient) test suite can be represented as a finite set of IO sequences *)
(* (tps q) must already be finite for a sufficient test suite due to being a subset of the maximal m-traversal paths *)
fun is_finite_test_suite :: "('a,'b,'c,'d) test_suite ⇒ bool" where
  "is_finite_test_suite (Test_Suite prs tps rd_targets separators) = 
    ((finite prs) ∧ (∀ q p . q ∈ fst ` prs ⟶ finite (rd_targets (q,p))) ∧ (∀ q q' . finite (separators (q,q'))))" 

end