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  xFSM.inputs M 
            tFSM.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  (dset 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 (SR 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  (dset 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  (dset 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 (pRRP 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 "(pRRP M q q' pP pM prs M'. io_targets M' (p_io pR) (FSM.initial M'))  (pRR 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 (pRRP 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 (pRRP 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