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