Theory State_Separator

section ‹State Separators›

text ‹This theory defined state separators.
      A state separator @{text "S"} of some pair of states @{text "q1"}, @{text "q2"} of some FSM @{text "M"} 
      is an acyclic single-input FSM based on the product machine @{text "P"} of @{text "M"} with initial state
      @{text "q1"} and @{text "M"} with initial state @{text "q2"} such that every maximal length
      sequence in the language of @{text "S"} is either in the language of @{text "q1"} or the
      language of @{text "q2"}, but not both.
      That is, @{text "C"} represents a strategy of distinguishing @{text "q1"} and @{text "q2"} in 
      every complete submachine of @{text "P"}.
      In testing, separators are used to distinguish states reached in the SUT to establish a lower
      bound on the number of distinct states in the SUT.›


theory State_Separator
imports "../Product_FSM" Backwards_Reachability_Analysis 
begin

subsection ‹Canonical Separators›

subsubsection ‹Construction›

fun canonical_separator :: "('a,'b,'c) fsm  'a  'a  (('a × 'a) + 'a,'b,'c) fsm"  where
  "canonical_separator M q1 q2 = (canonical_separator' M ((product (from_FSM M q1) (from_FSM M q2))) q1 q2)"


lemma canonical_separator_simps :
  assumes "q1  states M" and "q2  states M"
  shows "initial (canonical_separator M q1 q2) = Inl (q1,q2)"
        "states (canonical_separator M q1 q2) 
            = (image Inl (states (product (from_FSM M q1) (from_FSM M q2))))  {Inr q1, Inr q2}"
        "inputs (canonical_separator M q1 q2) = inputs M"
        "outputs (canonical_separator M q1 q2) = outputs M"
        "transitions (canonical_separator M q1 q2) 
            = shifted_transitions (transitions ((product (from_FSM M q1) (from_FSM M q2)))) 
                   distinguishing_transitions (h_out M) q1 q2 (states ((product (from_FSM M q1) (from_FSM M q2)))) (inputs ((product (from_FSM M q1) (from_FSM M q2))))"
proof -
  have *: "initial ((product (from_FSM M q1) (from_FSM M q2))) = (q1,q2)"
    unfolding restrict_to_reachable_states_simps product_simps using assms by auto
  have ***: "inputs ((product (from_FSM M q1) (from_FSM M q2))) = inputs M"
    unfolding restrict_to_reachable_states_simps product_simps using assms by auto
  have ****: "outputs ((product (from_FSM M q1) (from_FSM M q2))) = outputs M"
    unfolding restrict_to_reachable_states_simps product_simps using assms by auto
  
  show "initial (canonical_separator M q1 q2) = Inl (q1,q2)"
        "states (canonical_separator M q1 q2) = (image Inl (states (product (from_FSM M q1) (from_FSM M q2))))  {Inr q1, Inr q2}"
        "inputs (canonical_separator M q1 q2) = inputs M"
        "outputs (canonical_separator M q1 q2) = outputs M"
        "transitions (canonical_separator M q1 q2) = shifted_transitions (transitions ((product (from_FSM M q1) (from_FSM M q2))))  distinguishing_transitions (h_out M) q1 q2 (states ((product (from_FSM M q1) (from_FSM M q2)))) (inputs ((product (from_FSM M q1) (from_FSM M q2))))"
    unfolding canonical_separator.simps canonical_separator'_simps[OF *, of M] *** **** by blast+
qed


lemma distinguishing_transitions_alt_def :
  "distinguishing_transitions (h_out M) q1 q2 PS (inputs M) = 
    {(Inl (q1',q2'),x,y,Inr q1) | q1' q2' x y . (q1',q2')  PS  ( q' . (q1',x,y,q')  transitions M)  ¬( q' . (q2',x,y,q')  transitions M)}
     {(Inl (q1',q2'),x,y,Inr q2) | q1' q2' x y . (q1',q2')  PS  ¬( q' . (q1',x,y,q')  transitions M)  ( q' . (q2',x,y,q')  transitions M)}"
   (is "?dts = ?dl  ?dr")
proof -
  have " t . t  ?dts  t  ?dl  t  ?dr" 
    unfolding distinguishing_transitions_def h_out.simps by fastforce
  moreover have " t . t  ?dl  t  ?dr  t  ?dts"  
  proof -
    fix t assume "t  ?dl  t  ?dr"
    then obtain q1' q2' where "t_source t = Inl (q1',q2')" and "(q1',q2')  PS"
      by auto
    
    consider (a) "t  ?dl" |
             (b) "t  ?dr" 
      using t  ?dl  t  ?dr by blast
    then show "t  ?dts" proof cases
      case a
      then have "t_target t = Inr q1" and "( q' . (q1',t_input t,t_output t,q')  transitions M)" 
            and "¬( q' . (q2',t_input t,t_output t,q')  transitions M)"
        using t_source t = Inl (q1',q2') by force+
      then have "t_output t  h_out M (q1',t_input t) - h_out M (q2',t_input t)"
        unfolding h_out.simps by blast
      then have "t  (λy. (Inl (q1', q2'), t_input t, y, Inr q1)) ` (h_out M (q1', t_input t) - h_out M (q2', t_input t))"
        using t_source t = Inl (q1',q2') t_target t = Inr q1
        by (metis (mono_tags, lifting) imageI surjective_pairing) 
      moreover have "((q1',q2'),t_input t)  PS × inputs M"
        using fsm_transition_input ( q' . (q1',t_input t,t_output t,q')  transitions M) 
              (q1',q2')  PS 
        by auto 
      ultimately show ?thesis 
        unfolding distinguishing_transitions_def by fastforce
    next
      case b
      then have "t_target t = Inr q2" and "¬( q' . (q1',t_input t,t_output t,q')  transitions M)" 
            and "( q' . (q2',t_input t,t_output t,q')  transitions M)"
        using t_source t = Inl (q1',q2') by force+
      then have "t_output t  h_out M (q2',t_input t) - h_out M (q1',t_input t)"
        unfolding h_out.simps by blast
      then have "t  (λy. (Inl (q1', q2'), t_input t, y, Inr q2)) ` (h_out M (q2', t_input t) - h_out M (q1', t_input t))"
        using t_source t = Inl (q1',q2') t_target t = Inr q2
        by (metis (mono_tags, lifting) imageI surjective_pairing) 
      moreover have "((q1',q2'),t_input t)  PS × inputs M"
        using fsm_transition_input ( q' . (q2',t_input t,t_output t,q')  transitions M) (q1',q2')  PS 
        by auto 
      ultimately show ?thesis 
        unfolding distinguishing_transitions_def by fastforce
    qed
  qed
  ultimately show ?thesis by blast
qed


lemma distinguishing_transitions_alt_alt_def :
  "distinguishing_transitions (h_out M) q1 q2 PS (inputs M) = 
    { t .  q1' q2' . t_source t = Inl (q1',q2')  (q1',q2')  PS  t_target t = Inr q1  ( t'   transitions M . t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)  ¬( t'   transitions M . t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)}
   { t .  q1' q2' . t_source t = Inl (q1',q2')  (q1',q2')  PS  t_target t = Inr q2  ¬( t'   transitions M . t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)  ( t'   transitions M . t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)}"
  
proof -
  have "{(Inl (q1',q2'),x,y,Inr q1) | q1' q2' x y . (q1',q2')  PS  ( q' . (q1',x,y,q')  transitions M)  ¬( q' . (q2',x,y,q')  transitions M)}
        = { t .  q1' q2' . t_source t = Inl (q1',q2')  (q1',q2')  PS  t_target t = Inr q1  ( t'   transitions M . t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)  ¬( t'   transitions M . t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)}"
    by force
  moreover have "{(Inl (q1',q2'),x,y,Inr q2) | q1' q2' x y . (q1',q2')  PS  ¬( q' . (q1',x,y,q')  transitions M)  ( q' . (q2',x,y,q')  transitions M)}
        = { t .  q1' q2' . t_source t = Inl (q1',q2')  (q1',q2')  PS  t_target t = Inr q2  ¬( t'   transitions M . t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)  ( t'   transitions M . t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)}"
    by force
  ultimately show ?thesis  
    unfolding distinguishing_transitions_alt_def by force
qed
   

lemma shifted_transitions_alt_def :
  "shifted_transitions ts = {(Inl (q1',q2'), x, y, (Inl (q1'',q2''))) | q1' q2' x y q1'' q2'' . ((q1',q2'), x, y, (q1'',q2''))  ts}"   
  unfolding shifted_transitions_def by force


lemma canonical_separator_transitions_helper :
  assumes "q1  states M" and "q2  states M"
  shows "transitions (canonical_separator M q1 q2) = 
          (shifted_transitions  (transitions (product (from_FSM M q1) (from_FSM M q2))))
           {(Inl (q1',q2'),x,y,Inr q1) | q1' q2' x y . (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))  ( q' . (q1',x,y,q')  transitions M)  ¬( q' . (q2',x,y,q')  transitions M)}
           {(Inl (q1',q2'),x,y,Inr q2) | q1' q2' x y . (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))  ¬( q' . (q1',x,y,q')  transitions M)  ( q' . (q2',x,y,q')  transitions M)}"
  unfolding canonical_separator_simps[OF assms]
            restrict_to_reachable_states_simps
            product_simps from_FSM_simps[OF assms(1)] from_FSM_simps[OF assms(2)]
            sup.idem
            distinguishing_transitions_alt_def 
  by blast


definition distinguishing_transitions_left :: "('a, 'b, 'c) fsm  'a  'a  (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
  "distinguishing_transitions_left M q1 q2   {(Inl (q1',q2'),x,y,Inr q1) | q1' q2' x y . (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))  ( q' . (q1',x,y,q')  transitions M)  ¬( q' . (q2',x,y,q')  transitions M)}"
definition distinguishing_transitions_right :: "('a, 'b, 'c) fsm  'a  'a  (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
  "distinguishing_transitions_right M q1 q2  {(Inl (q1',q2'),x,y,Inr q2) | q1' q2' x y . (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))  ¬( q' . (q1',x,y,q')  transitions M)  ( q' . (q2',x,y,q')  transitions M)}"

definition distinguishing_transitions_left_alt :: "('a, 'b, 'c) fsm  'a  'a  (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
  "distinguishing_transitions_left_alt M q1 q2   { t .  q1' q2' . t_source t = Inl (q1',q2')  (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))  t_target t = Inr q1  ( t'   transitions M . t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)  ¬( t'   transitions M . t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)}"
definition distinguishing_transitions_right_alt :: "('a, 'b, 'c) fsm  'a  'a  (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
  "distinguishing_transitions_right_alt M q1 q2  { t .  q1' q2' . t_source t = Inl (q1',q2')  (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))  t_target t = Inr q2  ¬( t'   transitions M . t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)  ( t'   transitions M . t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)}"


definition shifted_transitions_for :: "('a, 'b, 'c) fsm  'a  'a  (('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a)) set" where
"shifted_transitions_for M q1 q2  {(Inl (t_source t),t_input t, t_output t, Inl (t_target t)) | t . t  transitions (product (from_FSM M q1) (from_FSM M q2))}"


lemma shifted_transitions_for_alt_def :
  "shifted_transitions_for M q1 q2 = {(Inl (q1',q2'), x, y, (Inl (q1'',q2''))) | q1' q2' x y q1'' q2'' . ((q1',q2'), x, y, (q1'',q2''))  transitions (product (from_FSM M q1) (from_FSM M q2))}"
  unfolding shifted_transitions_for_def by auto


lemma distinguishing_transitions_left_alt_alt_def :
  "distinguishing_transitions_left M q1 q2 = distinguishing_transitions_left_alt M q1 q2" 
proof -
  have " t . t  distinguishing_transitions_left M q1 q2  t  distinguishing_transitions_left_alt M q1 q2" 
  proof -
    fix t assume "t  distinguishing_transitions_left M q1 q2"
    then obtain q1' q2' x y where "t = (Inl (q1', q2'), x, y, Inr q1)"
                                  "(q1', q2')  states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
                                  "(q'. (q1', x, y, q')  FSM.transitions M)" 
                                  "(q'. (q2', x, y, q')  FSM.transitions M)"
      unfolding distinguishing_transitions_left_def by blast

    have "t_source t = Inl (q1', q2')"
      using t = (Inl (q1', q2'), x, y, Inr q1) by auto
    moreover note (q1', q2')  states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))
    moreover have "t_target t = Inr q1"
      using t = (Inl (q1', q2'), x, y, Inr q1) by auto
    moreover have "(t'FSM.transitions M. t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)" 
      using (q'. (q1', x, y, q')  FSM.transitions M) unfolding t = (Inl (q1', q2'), x, y, Inr q1) by force
    moreover have "¬(t'FSM.transitions M. t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)" 
      using (q'. (q2', x, y, q')  FSM.transitions M) unfolding t = (Inl (q1', q2'), x, y, Inr q1) by force
    ultimately show "t  distinguishing_transitions_left_alt M q1 q2"
      unfolding distinguishing_transitions_left_alt_def by simp
  qed
  moreover have " t . t  distinguishing_transitions_left_alt M q1 q2  t  distinguishing_transitions_left M q1 q2"
    unfolding distinguishing_transitions_left_alt_def distinguishing_transitions_left_def 
    by fastforce
  ultimately show ?thesis by blast 
qed


lemma distinguishing_transitions_right_alt_alt_def :
  "distinguishing_transitions_right M q1 q2 = distinguishing_transitions_right_alt M q1 q2" 
proof -
  have " t . t  distinguishing_transitions_right M q1 q2  t  distinguishing_transitions_right_alt M q1 q2" 
  proof -
    fix t assume "t  distinguishing_transitions_right M q1 q2"
    then obtain q1' q2' x y where "t = (Inl (q1', q2'), x, y, Inr q2)"
                                  "(q1', q2')  states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
                                  "(q'. (q1', x, y, q')  FSM.transitions M)" 
                                  "(q'. (q2', x, y, q')  FSM.transitions M)"
      unfolding distinguishing_transitions_right_def by blast

    have "t_source t = Inl (q1', q2')"
      using t = (Inl (q1', q2'), x, y, Inr q2) by auto
    moreover note (q1', q2')  states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))
    moreover have "t_target t = Inr q2"
      using t = (Inl (q1', q2'), x, y, Inr q2) by auto
    moreover have "¬(t'FSM.transitions M. t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)" 
      using (q'. (q1', x, y, q')  FSM.transitions M) unfolding t = (Inl (q1', q2'), x, y, Inr q2) by force
    moreover have "(t'FSM.transitions M. t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)" 
      using (q'. (q2', x, y, q')  FSM.transitions M) unfolding t = (Inl (q1', q2'), x, y, Inr q2) by force
    ultimately show "t  distinguishing_transitions_right_alt M q1 q2"
      unfolding distinguishing_transitions_right_def distinguishing_transitions_right_alt_def by simp
  qed
  moreover have " t . t  distinguishing_transitions_right_alt M q1 q2  t  distinguishing_transitions_right M q1 q2"
    unfolding distinguishing_transitions_right_def distinguishing_transitions_right_alt_def by fastforce
  ultimately show ?thesis
    by blast
qed

    
lemma canonical_separator_transitions_def :
  assumes "q1  states M" and "q2  states M"
  shows "transitions (canonical_separator M q1 q2) = 
        {(Inl (q1',q2'), x, y, (Inl (q1'',q2''))) | q1' q2' x y q1'' q2'' . ((q1',q2'), x, y, (q1'',q2''))  transitions (product (from_FSM M q1) (from_FSM M q2))}
         (distinguishing_transitions_left M q1 q2)       
         (distinguishing_transitions_right M q1 q2)"
  unfolding canonical_separator_transitions_helper[OF assms]
            shifted_transitions_alt_def 
            distinguishing_transitions_left_def
            distinguishing_transitions_right_def by simp 

lemma canonical_separator_transitions_alt_def :
  assumes "q1  states M" and "q2  states M"
  shows "transitions (canonical_separator M q1 q2) = 
        (shifted_transitions_for M q1 q2)
         (distinguishing_transitions_left_alt M q1 q2)
         (distinguishing_transitions_right_alt M q1 q2)"
proof -
  have *: "(shift_Inl `
            {t  FSM.transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)).
             t_source t  reachable_states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))})
          = {(Inl (t_source t), t_input t, t_output t, Inl (t_target t)) |t.
             t  FSM.transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) 
             t_source t  reachable_states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))}" 
    by blast
  
  show ?thesis
  unfolding canonical_separator_simps[OF assms]
            shifted_transitions_def
            restrict_to_reachable_states_simps
            product_simps from_FSM_simps[OF assms(1)] from_FSM_simps[OF assms(2)]
            sup.idem
  
            distinguishing_transitions_alt_alt_def
            shifted_transitions_for_def 
            * 
            
            distinguishing_transitions_left_alt_def
            distinguishing_transitions_right_alt_def
  by blast
qed




subsubsection ‹State Separators as Submachines of Canonical Separators›

definition is_state_separator_from_canonical_separator :: "(('a × 'a) + 'a, 'b, 'c) fsm  'a  'a  (('a × 'a) + 'a, 'b, 'c) fsm  bool" where
  "is_state_separator_from_canonical_separator CSep q1 q2 S = (
    is_submachine S CSep 
     single_input S
     acyclic S
     deadlock_state S (Inr q1)
     deadlock_state S (Inr q2)
     ((Inr q1)  reachable_states S)
     ((Inr q2)  reachable_states S)
     ( q  reachable_states S . (q  Inr q1  q  Inr q2)  (isl q  ¬ deadlock_state S q))
     ( q  reachable_states S .  x  (inputs CSep) . ( t  transitions S . t_source t = q  t_input t = x)  ( t'  transitions CSep . t_source t' = q  t_input t' = x  t'  transitions S))
)"


subsubsection ‹Canonical Separator Properties›

lemma is_state_separator_from_canonical_separator_simps :
  assumes "is_state_separator_from_canonical_separator CSep q1 q2 S"
  shows "is_submachine S CSep" 
  and   "single_input S"
  and   "acyclic S"
  and   "deadlock_state S (Inr q1)"
  and   "deadlock_state S (Inr q2)"
  and   "((Inr q1)  reachable_states S)"
  and   "((Inr q2)  reachable_states S)"
  and   " q . q  reachable_states S  q  Inr q1  q  Inr q2  (isl q  ¬ deadlock_state S q)"
  and   " q x t . q  reachable_states S  x  (inputs CSep)  ( t  transitions S . t_source t = q  t_input t = x)  t  transitions CSep  t_source t = q  t_input t = x  t  transitions S"
  using assms unfolding is_state_separator_from_canonical_separator_def by blast+


lemma is_state_separator_from_canonical_separator_initial :
  assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
      and "q1  states M"
      and "q2  states M"
  shows "initial A = Inl (q1,q2)"
  using is_state_separator_from_canonical_separator_simps(1)[OF assms(1)] 
  using canonical_separator_simps(1)[OF assms(2,3)] by auto


lemma path_shift_Inl :
  assumes "(image shift_Inl (transitions M))  (transitions C)"
      and " t . t  (transitions C)  isl (t_target t)   t'  transitions M . t = (Inl (t_source t'), t_input t', t_output t', Inl (t_target t'))"
      and "initial C = Inl (initial M)"
      and "(inputs C) = (inputs M)"
      and "(outputs C) = (outputs M)"
    shows "path M (initial M) p = path C (initial C) (map shift_Inl p)"
proof (induction p rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc t p)

  have "path M (initial M) (p@[t])  path C (initial C) (map shift_Inl (p@[t]))"
  proof -
    assume "path M (initial M) (p@[t])"
    then have "path M (initial M) p" by auto
    then have "path C (initial C) (map shift_Inl p)" using snoc.IH
      by auto 

    have "t_source t = target (initial M) p"
      using path M (initial M) (p@[t]) by auto
    then have "t_source (shift_Inl t) = target (Inl (initial M)) (map shift_Inl p)"
      by (cases p rule: rev_cases; auto)
    then have "t_source (shift_Inl t) = target (initial C) (map shift_Inl p)"
      using assms(3) by auto
    moreover have "target (initial C) (map shift_Inl p)  states C"
      using path_target_is_state[OF path C (initial C) (map shift_Inl p)] by assumption
    ultimately have "t_source (shift_Inl t)  states C"
      by auto
    moreover have "t  transitions M"
      using path M (initial M) (p@[t]) by auto
    ultimately have "(shift_Inl t)  transitions C"
      using assms by auto

    show "path C (initial C) (map shift_Inl (p@[t]))"
      using path_append [OF path C (initial C) (map shift_Inl p), of "[shift_Inl t]"]
      using (shift_Inl t)  transitions C t_source (shift_Inl t) = target (initial C) (map shift_Inl p)
      using single_transition_path by force 
  qed

  moreover have "path C (initial C) (map shift_Inl (p@[t]))  path M (initial M) (p@[t])" 
  proof -
    assume "path C (initial C) (map shift_Inl (p@[t]))"
    then have "path C (initial C) (map shift_Inl p)" by auto
    then have "path M (initial M) p" using snoc.IH
      by blast 

    have "t_source (shift_Inl t) = target (initial C) (map shift_Inl p)"
      using path C (initial C) (map shift_Inl (p@[t])) by auto
    then have "t_source (shift_Inl t) = target (Inl (initial M)) (map shift_Inl p)"
      using assms(3) by (cases p rule: rev_cases; auto)
    then have "t_source t = target (initial M) p"
      by (cases p rule: rev_cases; auto)
    moreover have "target (initial M) p  states M"
      using path_target_is_state[OF path M (initial M) p] by assumption
    ultimately have "t_source t  states M"
      by auto
    moreover have "shift_Inl t  transitions C"
      using path C (initial C) (map shift_Inl (p@[t])) by auto
    moreover have "isl (t_target (shift_Inl t))"
      by auto
    ultimately have "t  transitions M" using assms by fastforce

    show "path M (initial M) (p@[t])"
      using path_append [OF path M (initial M) p, of "[t]"]
            single_transition_path[OF t  transitions M]
            t_source t = target (initial M) p by auto
  qed

  ultimately show ?case
    by linarith 
qed


lemma canonical_separator_product_transitions_subset : 
  assumes "q1  states M" and "q2  states M"
  shows "image shift_Inl (transitions (product (from_FSM M q1) (from_FSM M q2)))  (transitions (canonical_separator M q1 q2))"
  unfolding canonical_separator_simps[OF assms] shifted_transitions_def restrict_to_reachable_states_simps 
  by blast


lemma canonical_separator_transition_targets :
  assumes "t  (transitions (canonical_separator M q1 q2))" 
  and "q1  states M" 
  and "q2  states M"
shows "isl (t_target t)  t  {(Inl (t_source t),t_input t, t_output t, Inl (t_target t)) | t . t  transitions (product (from_FSM M q1) (from_FSM M q2))}" 
and   "t_target t = Inr q1  q1  q2  t  (distinguishing_transitions_left_alt M q1 q2)"
and   "t_target t = Inr q2  q1  q2  t  (distinguishing_transitions_right_alt M q1 q2)"
and   "isl (t_target t)  t_target t = Inr q1  t_target t = Inr q2"
unfolding shifted_transitions_for_def
          distinguishing_transitions_left_alt_def
          distinguishing_transitions_right_alt_def
proof -
  let ?shftd = "{(Inl (t_source t),t_input t, t_output t, Inl (t_target t)) | t . t  transitions (product (from_FSM M q1) (from_FSM M q2))}"
  let ?dl    = "{ t .  q1' q2' . t_source t = Inl (q1',q2')  (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))  t_target t = Inr q1  ( t'   transitions M . t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)  ¬( t'   transitions M . t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)}"
  let ?dr    = "{ t .  q1' q2' . t_source t = Inl (q1',q2')  (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))  t_target t = Inr q2  ¬( t'   transitions M . t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t)  ( t'   transitions M . t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t)}"

  have "t  ?shftd  ?dl  ?dr"
    using assms(1) 
    unfolding canonical_separator_transitions_alt_def[OF assms(2,3)]
              shifted_transitions_for_def
              distinguishing_transitions_left_alt_def
              distinguishing_transitions_right_alt_def
    by force

  moreover have p1: " t' . t'  ?shftd  isl (t_target t')" 
  and  p2: " t' . t'  ?dl  t_target t' = Inr q1" 
  and  p3: " t' . t'  ?dr  t_target t' = Inr q2" 
    by auto
  ultimately show "isl (t_target t)  t_target t = Inr q1  t_target t = Inr q2" 
    by fast

  show "isl (t_target t)  t  ?shftd" 
  proof -
    assume "isl (t_target t)"
    then have "t_target t  Inr q1" and "t_target t  Inr q2" by auto
    then have "t  ?dl" and "t  ?dr" by force+
    then show ?thesis using t  ?shftd  ?dl  ?dr by fastforce
  qed

  show "t_target t = Inr q1  q1  q2  t  ?dl" 
  proof -
    assume "t_target t = Inr q1" and "q1  q2"
    then have "¬ isl (t_target t)" and "t_target t  Inr q2" by auto
    then have "t  ?shftd" and "t  ?dr" by force+
    then show ?thesis using t  ?shftd  ?dl  ?dr by fastforce
  qed

  show "t_target t = Inr q2  q1  q2  t  ?dr" 
  proof -
    assume "t_target t = Inr q2" and "q1  q2"
    then have "¬ isl (t_target t)" and "t_target t  Inr q1"  by auto
    then have "t  ?shftd" and "t  ?dl" by force+
    then show ?thesis using t  ?shftd  ?dl  ?dr by fastforce
  qed
qed


lemma canonical_separator_path_shift :
  assumes "q1  states M" and "q2  states M"
  shows "path (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2))) p 
    = path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) (map shift_Inl p)"
proof -
  let ?C = "(canonical_separator M q1 q2)"
  let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
  let ?PR = "(product (from_FSM M q1) (from_FSM M q2))"
  
  have "(inputs ?C) = (inputs ?P)" 
  and  "(outputs ?C) = (outputs ?P)"
    unfolding canonical_separator_simps(3,4)[OF assms] using assms by auto

  have p1: "shift_Inl `
    FSM.transitions
     ((Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)))
     FSM.transitions (canonical_separator M q1 q2)"
    using canonical_separator_product_transitions_subset[OF assms]
    unfolding restrict_to_reachable_states_simps by assumption

  have p2: "(t. t  FSM.transitions (canonical_separator M q1 q2) 
          isl (t_target t) 
          t'FSM.transitions
                ((Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))).
             t = shift_Inl t')"
    using canonical_separator_transition_targets(1)[OF _ assms] unfolding restrict_to_reachable_states_simps by fastforce

  have "path ?PR (initial ?PR) p = path ?C (initial ?C) (map shift_Inl p)"
    using path_shift_Inl[of ?PR ?C, OF p1 p2]  
    unfolding restrict_to_reachable_states_simps canonical_separator_simps(1,2,3,4)[OF assms] using assms by auto
  moreover have "path ?P (initial ?P) p = path ?PR (initial ?PR) p"
    unfolding restrict_to_reachable_states_simps
              restrict_to_reachable_states_path[OF reachable_states_initial] 
    by simp  
  ultimately show ?thesis 
    by simp
qed


lemma canonical_separator_t_source_isl :
  assumes "t  (transitions (canonical_separator M q1 q2))"
  and "q1  states M" and "q2  states M"
  shows "isl (t_source t)"
  using assms(1) 
  unfolding canonical_separator_transitions_alt_def[OF assms(2,3)] 
            shifted_transitions_for_def
            distinguishing_transitions_left_alt_def
            distinguishing_transitions_right_alt_def
  by force


lemma canonical_separator_path_from_shift :
  assumes "path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) p"
      and "isl (target (initial (canonical_separator M q1 q2)) p)"
      and "q1  states M" and "q2  states M"
    shows " p' . path (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2))) p' 
                   p = (map shift_Inl p')"
using assms(1,2) proof (induction p rule: rev_induct)
  case Nil
  show ?case using canonical_separator_path_shift[OF assms(3,4), of "[]"] by fast
next
  case (snoc t p)
  then have "isl (t_target t)" by auto

  let ?C = "(canonical_separator M q1 q2)"
  let ?P = "(product (from_FSM M q1) (from_FSM M q2))"

  have "t  transitions ?C" and "t_source t = target (initial ?C) p" 
    using snoc.prems by auto
  then have "isl (t_source t)"
    using canonical_separator_t_source_isl[of t M q1 q2, OF _ assms(3,4)] by blast  
  then have "isl (target (initial (canonical_separator M q1 q2)) p)"
    using t_source t = target (initial ?C) p by auto

  have "path ?C (initial ?C) p" using snoc.prems by auto
  then obtain p' where "path ?P (initial ?P) p'"
                   and "p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p'"
    using snoc.IH[OF _ isl (target (initial (canonical_separator M q1 q2)) p)] by blast
  then have "target (initial ?C) p = Inl (target (initial ?P) p')"
  proof (cases p rule: rev_cases)
    case Nil
    then show ?thesis 
      unfolding target.simps visited_states.simps using p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p' canonical_separator_simps(1)[OF assms(3,4)]
      by (simp add: assms(3) assms(4)) 
  next
    case (snoc ys y)
    then show ?thesis 
      unfolding target.simps visited_states.simps using p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p' by (cases p' rule: rev_cases; auto)
  qed
  
  obtain t' where "t'  transitions ?P" 
              and "t = (Inl (t_source t'), t_input t', t_output t', Inl (t_target t'))"
    using canonical_separator_transition_targets(1)[OF t  transitions ?C assms(3,4) isl (t_target t)]
    by blast 
  
  have "path ?P (initial ?P) (p'@[t'])"
    by (metis path (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) (FSM.initial (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))) p' 
          t = shift_Inl t' t'  FSM.transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) 
          t_source t = target (FSM.initial (canonical_separator M q1 q2)) p 
          target (FSM.initial (canonical_separator M q1 q2)) p = Inl (target (FSM.initial (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))) p') 
          fst_conv path_append_transition sum.inject(1))
  moreover have "p@[t] = map shift_Inl (p'@[t'])"
    using p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p' 
          t = (Inl (t_source t'), t_input t', t_output t', Inl (t_target t')) 
    by auto
  ultimately show ?case 
    by meson
qed
    

lemma shifted_transitions_targets :
  assumes "t  (shifted_transitions ts)"
  shows "isl (t_target t)"
  using assms unfolding shifted_transitions_def by force


lemma distinguishing_transitions_left_sources_targets :
  assumes "t  (distinguishing_transitions_left_alt M q1 q2)"
      and "q2  states M"  
    obtains q1' q2' t' where "t_source t = Inl (q1',q2')" 
                            "q1'  states M" 
                            "q2'  states M" 
                            "t'  transitions M" 
                            "t_source t' = q1'" 
                            "t_input t' = t_input t" 
                            "t_output t' = t_output t" 
                            "¬ (t'' transitions M. t_source t'' = q2'  t_input t'' = t_input t  t_output t'' = t_output t)" 
                            "t_target t = Inr q1"
  using assms(1) assms(2) fsm_transition_source path_target_is_state 
  unfolding distinguishing_transitions_left_alt_def
  by fastforce


lemma distinguishing_transitions_right_sources_targets :
  assumes "t  (distinguishing_transitions_right_alt M q1 q2)"
      and "q1  states M"  
    obtains q1' q2' t' where "t_source t = Inl (q1',q2')" 
                            "q1'  states M" 
                            "q2'  states M" 
                            "t'  transitions M" 
                            "t_source t' = q2'" 
                            "t_input t' = t_input t" 
                            "t_output t' = t_output t" 
                            "¬ (t'' transitions M. t_source t'' = q1'  t_input t'' = t_input t  t_output t'' = t_output t)" 
                            "t_target t = Inr q2"
  using assms(1) assms(2) fsm_transition_source path_target_is_state 
  unfolding distinguishing_transitions_right_alt_def
  by fastforce


lemma product_from_transition_split :
  assumes "t  transitions (product (from_FSM M q1) (from_FSM M q2))"
  and     "q1  states M"
  and     "q2  states M"
shows   "(t' transitions M. t_source t' = fst (t_source t)  t_input t' = t_input t  t_output t' = t_output t)"
and     "(t' transitions M. t_source t' = snd (t_source t)  t_input t' = t_input t  t_output t' = t_output t)"
  using product_transition_split_ob[OF assms(1)]
  unfolding product_transitions_alt_def from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)] by blast+


lemma shifted_transitions_underlying_transition :
  assumes "tS  shifted_transitions_for M q1 q2"
  and     "q1  states M"
  and     "q2  states M"
  obtains t where "tS = (Inl (t_source t), t_input t, t_output t, Inl (t_target t))"
            and   "t  (transitions ((product (from_FSM M q1) (from_FSM M q2))))"
            and   "(t'(transitions M).
                            t_source t' = fst (t_source t) 
                            t_input t' = t_input t  t_output t' = t_output t)"
            and   "(t'(transitions M).
                            t_source t' = snd (t_source t) 
                            t_input t' = t_input t  t_output t' = t_output t)"
proof -
  obtain t where "tS = (Inl (t_source t), t_input t, t_output t, Inl (t_target t))"
           and   *: "t  (transitions ((product (from_FSM M q1) (from_FSM M q2))))"
    using assms unfolding shifted_transitions_for_def shifted_transitions_def restrict_to_reachable_states_simps by blast
  moreover have "(t'(transitions M).
                            t_source t' = fst (t_source t) 
                            t_input t' = t_input t  t_output t' = t_output t)"
    using product_from_transition_split(1)[OF _ assms(2,3)]
          *
    unfolding restrict_to_reachable_states_simps by blast
  moreover have "(t'(transitions M).
                            t_source t' = snd (t_source t) 
                            t_input t' = t_input t  t_output t' = t_output t)"
    using product_from_transition_split(2)[OF _ assms(2,3)]
          *
    unfolding restrict_to_reachable_states_simps by blast
  ultimately show ?thesis
    using that by blast 
qed
     

lemma shifted_transitions_observable_against_distinguishing_transitions_left :
  assumes "t1  (shifted_transitions_for M q1 q2)"
  and     "t2  (distinguishing_transitions_left M q1 q2)"
  and     "q1  states M"
  and     "q2  states M"
shows "¬ (t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2)"
  using assms(1,2)
  unfolding product_transitions_def from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)]
            shifted_transitions_for_def distinguishing_transitions_left_def
  by force

lemma shifted_transitions_observable_against_distinguishing_transitions_right :
  assumes "t1  (shifted_transitions_for M q1 q2)"
  and     "t2  (distinguishing_transitions_right M q1 q2)"
  and     "q1  states M"
  and     "q2  states M"
shows "¬ (t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2)"
  using assms
  unfolding product_transitions_def from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)] 
            shifted_transitions_for_def distinguishing_transitions_right_def
  by force


lemma distinguishing_transitions_left_observable_against_distinguishing_transitions_right :
  assumes "t1  (distinguishing_transitions_left M q1 q2)"
  and     "t2  (distinguishing_transitions_right M q1 q2)"
shows "¬ (t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2)"
  using assms 
  unfolding distinguishing_transitions_left_def distinguishing_transitions_right_def by force


lemma distinguishing_transitions_left_observable_against_distinguishing_transitions_left :
  assumes "t1  (distinguishing_transitions_left M q1 q2)"
  and     "t2  (distinguishing_transitions_left M q1 q2)"
  and     "t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2"
shows "t1 = t2"
  using assms unfolding distinguishing_transitions_left_def by force


lemma distinguishing_transitions_right_observable_against_distinguishing_transitions_right :
  assumes "t1  (distinguishing_transitions_right M q1 q2)"
  and     "t2  (distinguishing_transitions_right M q1 q2)"
  and     "t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2"
shows "t1 = t2"
  using assms unfolding distinguishing_transitions_right_def by force


lemma shifted_transitions_observable_against_shifted_transitions :
  assumes "t1  (shifted_transitions_for M q1 q2)"
  and     "t2  (shifted_transitions_for M q1 q2)"
  and     "observable M"
  and     "t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2"
shows "t1 = t2" 
proof -
  obtain t1' where d1: "t1 = (Inl (t_source t1'), t_input t1', t_output t1', Inl (t_target t1'))"
             and   h1: "t1'  (transitions (product (from_FSM M q1) (from_FSM M q2)))"
    using assms(1) unfolding shifted_transitions_for_def by auto

  obtain t2' where d2: "t2 = (Inl (t_source t2'), t_input t2', t_output t2', Inl (t_target t2'))"
             and   h2: "t2'  (transitions (product (from_FSM M q1) (from_FSM M q2)))"
    using assms(2) unfolding shifted_transitions_for_def by auto

  have "observable (product (from_FSM M q1) (from_FSM M q2))"
    using from_FSM_observable[OF assms(3)] 
          product_observable 
    by metis
  
  then have "t1' = t2'"
    using d1 d2 h1 h2 t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2
    by (metis fst_conv observable.elims(2) prod.expand snd_conv sum.inject(1)) 
  then show ?thesis using d1 d2 by auto
qed
  

lemma canonical_separator_observable :
  assumes "observable M"
  and     "q1  states M"
  and     "q2  states M"
shows "observable (canonical_separator M q1 q2)" (is "observable ?CSep")
proof -

  have  " t1 t2 . t1  (transitions ?CSep)  
                             t2  (transitions ?CSep)  
                    t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2  t_target t1 = t_target t2" 
  proof -
    fix t1 t2 assume "t1  (transitions ?CSep)" 
              and    "t2  (transitions ?CSep)"
              and    *: "t_source t1 = t_source t2  t_input t1 = t_input t2  t_output t1 = t_output t2"
    
    moreover have "transitions ?CSep = shifted_transitions_for M q1 q2 
                                       distinguishing_transitions_left M q1 q2 
                                       distinguishing_transitions_right M q1 q2"
      using canonical_separator_transitions_alt_def[OF assms(2,3)] 
      unfolding distinguishing_transitions_left_alt_alt_def distinguishing_transitions_right_alt_alt_def by assumption

    ultimately consider "t1  shifted_transitions_for M q1 q2  t2  shifted_transitions_for M q1 q2"
                      | "t1  shifted_transitions_for M q1 q2  t2  distinguishing_transitions_left M q1 q2"
                      | "t1  shifted_transitions_for M q1 q2  t2  distinguishing_transitions_right M q1 q2"
                      | "t1  distinguishing_transitions_left M q1 q2  t2  shifted_transitions_for M q1 q2"
                      | "t1  distinguishing_transitions_left M q1 q2  t2  distinguishing_transitions_left M q1 q2"
                      | "t1  distinguishing_transitions_left M q1 q2  t2  distinguishing_transitions_right M q1 q2"
                      | "t1  distinguishing_transitions_right M q1 q2  t2  shifted_transitions_for M q1 q2"
                      | "t1  distinguishing_transitions_right M q1 q2  t2  distinguishing_transitions_left M q1 q2"
                      | "t1  distinguishing_transitions_right M q1 q2  t2  distinguishing_transitions_right M q1 q2"
      by force
    then show "t_target t1 = t_target t2" proof cases
      case 1
      then show ?thesis using shifted_transitions_observable_against_shifted_transitions[of t1 M q1 q2 t2, OF _ _ assms(1) *] by fastforce
    next
      case 2
      then show ?thesis using shifted_transitions_observable_against_distinguishing_transitions_left[OF _ _ assms(2,3), of t1 t2] * by fastforce
    next
      case 3
      then show ?thesis using shifted_transitions_observable_against_distinguishing_transitions_right[OF _ _ assms(2,3), of t1 t2] * by fastforce
    next
      case 4
      then show ?thesis using shifted_transitions_observable_against_distinguishing_transitions_left[OF _ _ assms(2,3), of t2 t1] * by fastforce
    next
      case 5
      then show ?thesis using * unfolding distinguishing_transitions_left_def by fastforce
    next
      case 6
      then show ?thesis using * unfolding distinguishing_transitions_left_def distinguishing_transitions_right_def by fastforce
    next
      case 7
      then show ?thesis using shifted_transitions_observable_against_distinguishing_transitions_right[OF _ _ assms(2,3), of t2 t1] * by fastforce
    next
      case 8
      then show ?thesis using * unfolding distinguishing_transitions_left_def distinguishing_transitions_right_def by fastforce
    next
      case 9
      then show ?thesis using * unfolding distinguishing_transitions_right_def by fastforce
    qed 
  qed
  then show ?thesis unfolding observable.simps by blast
qed


lemma canonical_separator_targets_ineq :
  assumes "t  transitions (canonical_separator M q1 q2)" 
      and "q1  states M" and "q2  states M" and "q1  q2"
  shows "isl (t_target t)  t  (shifted_transitions_for M q1 q2)"
    and "t_target t = Inr q1  t  (distinguishing_transitions_left M q1 q2)"
    and "t_target t = Inr q2  t  (distinguishing_transitions_right M q1 q2)"
proof -
  show "isl (t_target t)  t  (shifted_transitions_for M q1 q2)"
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) canonical_separator_transition_targets(1) shifted_transitions_for_def)
  show "t_target t = Inr q1  t  (distinguishing_transitions_left M q1 q2)"
    by (metis assms(1) assms(2) assms(3) assms(4) canonical_separator_transition_targets(2) distinguishing_transitions_left_alt_alt_def)
  show "t_target t = Inr q2  t  (distinguishing_transitions_right M q1 q2)"
    by (metis assms(1) assms(2) assms(3) assms(4) canonical_separator_transition_targets(3) distinguishing_transitions_right_alt_alt_def)
qed


lemma canonical_separator_targets_observable :
  assumes "t  transitions (canonical_separator M q1 q2)" 
      and "q1  states M" and "q2  states M" and "q1  q2"
  shows "isl (t_target t)  t  (shifted_transitions_for M q1 q2)"
    and "t_target t = Inr q1  t  (distinguishing_transitions_left M q1 q2)"
    and "t_target t = Inr q2  t  (distinguishing_transitions_right M q1 q2)"
proof -
  show "isl (t_target t)  t  (shifted_transitions_for M q1 q2)"
    by (metis assms canonical_separator_targets_ineq(1))
  show "t_target t = Inr q1  t  (distinguishing_transitions_left M q1 q2)"
    by (metis assms canonical_separator_targets_ineq(2))
  show "t_target t = Inr q2  t  (distinguishing_transitions_right M q1 q2)"
    by (metis assms canonical_separator_targets_ineq(3))
qed


lemma canonical_separator_maximal_path_distinguishes_left :
  assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 S" (is "is_state_separator_from_canonical_separator ?C q1 q2 S")
      and "path S (initial S) p"
      and "target (initial S) p = Inr q1"  
      and "observable M"
      and "q1  states M" and "q2  states M" and "q1  q2"
shows "p_io p  LS M q1 - LS M q2"
proof (cases p rule: rev_cases)
  case Nil
  then have "initial S = Inr q1" using assms(3) by auto
  then have "initial ?C = Inr q1"
    using assms(1) assms(5) assms(6) is_state_separator_from_canonical_separator_initial by fastforce
  then show ?thesis using canonical_separator_simps(1) Inr_Inl_False
    using assms(5) assms(6) by fastforce 
next
  case (snoc p' t) 
  then have "path S (initial S) (p'@[t])"
    using assms(2) by auto
  then have "t  transitions S" and "t_source t = target (initial S) p'" by auto


  have "path ?C (initial ?C) (p'@[t])"
    using path S (initial S) (p'@[t]) assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S] by (meson submachine_path_initial)
  then have "path ?C (initial ?C) (p')" and "t  transitions ?C"
    by auto

  have "isl (target (initial S) p')"
  proof (rule ccontr)
    assume "¬ isl (target (initial S) p')"
    moreover have "target (initial S) p'  states S"
      using path S (initial S) (p'@[t]) by auto
    ultimately have "target (initial S) p' = Inr q1  target (initial S) p' = Inr q2"
      using t  FSM.transitions (canonical_separator M q1 q2) t_source t = target (FSM.initial S) p' assms(5) assms(6) canonical_separator_t_source_isl by fastforce            
    moreover have "deadlock_state S (Inr q1)" and "deadlock_state S (Inr q2)"
      using assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S] by presburger+
    ultimately show "False" 
      using t  transitions S t_source t = target (initial S) p' unfolding deadlock_state.simps
      by metis 
  qed
  then obtain q1' q2' where "target (initial S) p' = Inl (q1',q2')" using isl_def prod.collapse by metis
  then have "isl (target (initial ?C) p')"
     using assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S]
     by (metis (no_types, lifting) Nil_is_append_conv assms(2) isl_def list.distinct(1) list.sel(1) path.cases snoc submachine_path_initial) 


  obtain pC where "path (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2))) pC"
              and "p' = map shift_Inl pC"
    by (metis (mono_tags, lifting) isl (target (FSM.initial (canonical_separator M q1 q2)) p') 
          path (canonical_separator M q1 q2) (FSM.initial (canonical_separator M q1 q2)) p' 
          assms(5) assms(6) canonical_separator_path_from_shift)
  then have "path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) pC"
    by (simp add: assms(5) assms(6))
  then have "path (from_FSM M q1) q1 (left_path pC)" and "path (from_FSM M q2) q2 (right_path pC)"
    using product_path[of "from_FSM M q1" "from_FSM M q2" q1 q2 pC] by presburger+

  have "path M q1 (left_path pC)"
    using from_FSM_path[OF assms(5) path (from_FSM M q1) q1 (left_path pC)] by assumption
  have "path M q2 (right_path pC)"
    using from_FSM_path[OF assms(6) path (from_FSM M q2) q2 (right_path pC)] by assumption
  
  have "t_target t = Inr q1"
    using path S (initial S) (p'@[t]) snoc assms(3) by auto
  then have "t  (distinguishing_transitions_left M q1 q2)"
    using canonical_separator_targets_ineq(2)[OF t  transitions ?C assms(5,6,7)] by auto
  then have "t  (distinguishing_transitions_left_alt M q1 q2)"
    using distinguishing_transitions_left_alt_alt_def by force

  have "t_source t = Inl (q1',q2')"
    using target (initial S) p' = Inl (q1',q2') t_source t = target (initial S) p' by auto

  then obtain t' where "q1'  states M"
                        and "q2'  states M"
                        and "t'  transitions M"
                        and "t_source t' = q1'"
                        and "t_input t' = t_input t"
                        and "t_output t' = t_output t"
                        and "¬ (t'' transitions M. t_source t'' = q2'  t_input t'' = t_input t  t_output t'' = t_output t)"
    using t  (distinguishing_transitions_left_alt M q1 q2) assms(5,6) fsm_transition_source path_target_is_state 
    unfolding distinguishing_transitions_left_alt_def reachable_states_def by fastforce


  have "initial S = Inl (q1,q2)"
    by (meson assms(1) assms(5) assms(6) is_state_separator_from_canonical_separator_initial)
  have "length p' = length pC"
    using p' = map shift_Inl pC by auto
  then have "target (initial S) p' = Inl (target (q1,q2) pC)"
    using p' = map shift_Inl pC initial S = Inl (q1,q2) by (induction p' pC rule: list_induct2; auto)
  then have "target (q1,q2) pC = (q1',q2')"
     using target (initial S) p' = Inl (q1',q2') by auto 
  then have "target q2 (right_path pC) = q2'"
    using product_target_split(2) by fastforce
  then have "¬ (t' transitions M. t_source t' = target q2 (right_path pC)  t_input t' = t_input t  t_output t' = t_output t)"
    using ¬ (t' transitions M. t_source t' = q2'  t_input t' = t_input t  t_output t' = t_output t) by blast

  have "target q1 (left_path pC) = q1'"
    using target (q1,q2) pC = (q1',q2') product_target_split(1) by fastforce
  then have "path M q1 ((left_path pC)@[t'])"
    using path M q1 (left_path pC) t'  transitions M t_source t' = q1'
    by (simp add: path_append_transition)
  then have "p_io ((left_path pC)@[t'])  LS M q1" 
    unfolding LS.simps by force 
  moreover have "p_io p' = p_io (left_path pC)"
    using p' = map shift_Inl pC by auto
  ultimately have "p_io (p'@[t])  LS M q1"
    using t_input t' = t_input t t_output t' = t_output t by auto
    
  have "p_io (right_path pC) @  [(t_input t, t_output t)]  LS M q2"
    using observable_path_language_step[OF assms(4) path M q2 (right_path pC) ¬ (t' transitions M. t_source t' = target q2 (right_path pC)  t_input t' = t_input t  t_output t' = t_output t)] by assumption
  moreover have "p_io p' = p_io (right_path pC)"
    using p' = map shift_Inl pC by auto
  ultimately have "p_io (p'@[t])  LS M q2"
    by auto

  show ?thesis 
    using p_io (p'@[t])  LS M q1 p_io (p'@[t])  LS M q2 snoc by blast
qed


lemma canonical_separator_maximal_path_distinguishes_right :
  assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 S" 
          (is "is_state_separator_from_canonical_separator ?C q1 q2 S")
      and "path S (initial S) p"
      and "target (initial S) p = Inr q2"  
      and "observable M"
      and "q1  states M" and "q2  states M" and "q1  q2"
shows "p_io p  LS M q2 - LS M q1"
proof (cases p rule: rev_cases)
  case Nil
  then have "initial S = Inr q2" using assms(3) by auto
  then have "initial ?C = Inr q2"
    using assms(1) assms(5) assms(6) is_state_separator_from_canonical_separator_initial by fastforce
  then show ?thesis using canonical_separator_simps(1) Inr_Inl_False
    using assms(5) assms(6) by fastforce  
next
  case (snoc p' t) 
  then have "path S (initial S) (p'@[t])"
    using assms(2) by auto
  then have "t  transitions S" and "t_source t = target (initial S) p'" 
    by auto

  have "path ?C (initial ?C) (p'@[t])"
    using path S (initial S) (p'@[t]) assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S] 
    by (meson submachine_path_initial)
  then have "path ?C (initial ?C) (p')" and "t  transitions ?C"
    by auto

  have "isl (target (initial S) p')"
  proof (rule ccontr)
    assume "¬ isl (target (initial S) p')"
    moreover have "target (initial S) p'  states S"
      using path S (initial S) (p'@[t]) by auto
    ultimately have "target (initial S) p' = Inr q1  target (initial S) p' = Inr q2"
      
      using assms(1) unfolding is_state_separator_from_canonical_separator_def
      by (metis t  FSM.transitions (canonical_separator M q1 q2) t_source t = target (FSM.initial S) p' 
            assms(5) assms(6) canonical_separator_t_source_isl)   
    moreover have "deadlock_state S (Inr q1)" and "deadlock_state S (Inr q2)"
      using assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S] by presburger+
    ultimately show "False" 
      using t  transitions S t_source t = target (initial S) p' unfolding deadlock_state.simps
      by metis 
  qed
  then obtain q1' q2' where "target (initial S) p' = Inl (q1',q2')" 
    using isl_def prod.collapse by metis
  then have "isl (target (initial ?C) p')"
     using assms(1) is_state_separator_from_canonical_separator_def[of ?C q1 q2 S]
     by (metis (no_types, lifting) Nil_is_append_conv assms(2) isl_def list.distinct(1) list.sel(1) 
         path.cases snoc submachine_path_initial) 

  obtain pC where "path (product (from_FSM M q1) (from_FSM M q2)) (initial (product (from_FSM M q1) (from_FSM M q2))) pC"
              and "p' = map shift_Inl pC"
    using canonical_separator_path_from_shift[OF path ?C (initial ?C) (p') isl (target (initial ?C) p')]
    using assms(5) assms(6) by blast 
  then have "path (product (from_FSM M q1) (from_FSM M q2)) (q1,q2) pC"
    by (simp add: assms(5) assms(6))

  then have "path (from_FSM M q1) q1 (left_path pC)" and "path (from_FSM M q2) q2 (right_path pC)"
    using product_path[of "from_FSM M q1" "from_FSM M q2" q1 q2 pC] by presburger+

  have "path M q1 (left_path pC)"
    using from_FSM_path[OF assms(5) path (from_FSM M q1) q1 (left_path pC)] by assumption
  have "path M q2 (right_path pC)"
    using from_FSM_path[OF assms(6) path (from_FSM M q2) q2 (right_path pC)] by assumption
  
  have "t_target t = Inr q2"
    using path S (initial S) (p'@[t]) snoc assms(3) by auto
  then have "t  (distinguishing_transitions_right M q1 q2)"
    using canonical_separator_targets_ineq(3)[OF t  transitions ?C assms(5,6,7)] by auto
  then have "t  (distinguishing_transitions_right_alt M q1 q2)"
    unfolding distinguishing_transitions_right_alt_alt_def by assumption

  have "t_source t = Inl (q1',q2')"
    using target (initial S) p' = Inl (q1',q2') t_source t = target (initial S) p' by auto

  then obtain t' where "q1'  states M"
                        and "q2'  states M"
                        and "t'  transitions M"
                        and "t_source t' = q2'"                        
                        and "t_input t' = t_input t"
                        and "t_output t' = t_output t"
                        and "¬ (t'' transitions M. t_source t'' = q1'  t_input t'' = t_input t  t_output t'' = t_output t)"
    using t  (distinguishing_transitions_right_alt M q1 q2) assms(5,6) fsm_transition_source path_target_is_state 
    unfolding distinguishing_transitions_right_alt_def reachable_states_def by fastforce

  
  have "initial S = Inl (q1,q2)"
    by (meson assms(1) assms(5) assms(6) is_state_separator_from_canonical_separator_initial)
  have "length p' = length pC"
    using p' = map shift_Inl pC by auto
  then have "target (initial S) p' = Inl (target (q1,q2) pC)"
    using p' = map shift_Inl pC initial S = Inl (q1,q2) by (induction p' pC rule: list_induct2; auto)
  then have "target (q1,q2) pC = (q1',q2')"
     using target (initial S) p' = Inl (q1',q2') by auto 
  then have "target q1 (left_path pC) = q1'"
    using product_target_split(1) by fastforce
  then have "¬ (t' transitions M. t_source t' = target q1 (left_path pC)  t_input t' = t_input t  t_output t' = t_output t)"
    using ¬ (t' transitions M. t_source t' = q1'  t_input t' = t_input t  t_output t' = t_output t) by blast

  have "target q2 (right_path pC) = q2'"
    using target (q1,q2) pC = (q1',q2') product_target_split(2) by fastforce
  then have "path M q2 ((right_path pC)@[t'])"
    using path M q2 (right_path pC) t'  transitions M t_source t' = q2'
    by (simp add: path_append_transition)
  then have "p_io ((right_path pC)@[t'])  LS M q2" 
    unfolding LS.simps by force 
  moreover have "p_io p' = p_io (right_path pC)"
    using p' = map shift_Inl pC by auto
  ultimately have "p_io (p'@[t])  LS M q2"
    using t_input t' = t_input t t_output t' = t_output t by auto
    

  have "p_io (left_path pC) @  [(t_input t, t_output t)]  LS M q1"
    using observable_path_language_step[OF assms(4) path M q1 (left_path pC) ¬ (t' transitions M. t_source t' = target q1 (left_path pC)  t_input t' = t_input t  t_output t' = t_output t)] by assumption
  moreover have "p_io p' = p_io (left_path pC)"
    using p' = map shift_Inl pC by auto
  ultimately have "p_io (p'@[t])  LS M q1"
    by auto
  
  show ?thesis 
    using p_io (p'@[t])  LS M q2 p_io (p'@[t])  LS M q1 snoc 
    by blast   
qed


lemma state_separator_from_canonical_separator_observable :
  assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
  and     "observable M"
  and     "q1  states M"
  and     "q2  states M"
shows "observable A"
  using submachine_observable[OF _ canonical_separator_observable[OF assms(2,3,4)]]
  using assms(1) unfolding is_state_separator_from_canonical_separator_def 
  by metis


lemma canonical_separator_initial :
  assumes "q1  states M" and "q2  states M"
  shows "initial (canonical_separator M q1 q2) = Inl (q1,q2)" 
    unfolding canonical_separator_simps[OF assms] by simp


lemma canonical_separator_states :
  assumes "Inl (s1,s2)  states (canonical_separator M q1 q2)"
  and     "q1  states M"
  and     "q2  states M"
shows "(s1,s2)  states (product (from_FSM M q1) (from_FSM M q2))"
  using assms(1) reachable_state_is_state
  unfolding canonical_separator_simps[OF assms(2,3)] by fastforce


lemma canonical_separator_transition :
  assumes "t  transitions (canonical_separator M q1 q2)" (is "t  transitions ?C")
  and     "q1  states M"
  and     "q2  states M"
  and     "t_source t = Inl (s1,s2)"
  and     "observable M"
  and     "q1  q2"
shows " s1' s2' . t_target t = Inl (s1',s2')  (s1, t_input t, t_output t, s1')  transitions M  (s2, t_input t, t_output t, s2')  transitions M "
and   "t_target t = Inr q1  ( t' transitions M . t_source t' = s1  t_input t' = t_input t  t_output t' = t_output t) 
                                 (¬( t' transitions M . t_source t' = s2  t_input t' = t_input t  t_output t' = t_output t))"
and   "t_target t = Inr q2  ( t' transitions M . t_source t' = s2  t_input t' = t_input t  t_output t' = t_output t) 
                                 (¬( t' transitions M . t_source t' = s1  t_input t' = t_input t  t_output t' = t_output t))"
and   "( s1' s2' . t_target t = Inl (s1',s2'))  t_target t = Inr q1  t_target t = Inr q2"
proof -
  show " s1' s2' . t_target t = Inl (s1',s2')  (s1, t_input t, t_output t, s1')  transitions M  (s2, t_input t, t_output t, s2')  transitions M"
    using canonical_separator_transition_targets(1)[OF assms(1,2,3)] assms(4)
    unfolding shifted_transitions_for_def[symmetric] 
    unfolding shifted_transitions_for_alt_def 
    unfolding product_transitions_def from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)] by fastforce

  show "t_target t = Inr q1  ( t' transitions M . t_source t' = s1  t_input t' = t_input t  t_output t' = t_output t) 
                                 (¬( t' transitions M . t_source t' = s2  t_input t' = t_input t  t_output t' = t_output t))"
    using canonical_separator_targets_observable(2)[OF assms(1,2,3,6)] assms(4)
    unfolding distinguishing_transitions_left_def by fastforce

  show "t_target t = Inr q2  ( t' transitions M . t_source t' = s2  t_input t' = t_input t  t_output t' = t_output t) 
                                 (¬( t' transitions M . t_source t' = s1  t_input t' = t_input t  t_output t' = t_output t))"
    using canonical_separator_targets_observable(3)[OF assms(1,2,3,6)] assms(4)
    unfolding distinguishing_transitions_right_def by fastforce

  show "( s1' s2' . t_target t = Inl (s1',s2'))  t_target t = Inr q1  t_target t = Inr q2"
    using canonical_separator_transition_targets(4)[OF assms(1,2,3)]
    by (simp add: isl_def) 
qed


lemma canonical_separator_transition_source :
  assumes "t  transitions (canonical_separator M q1 q2)" (is "t  transitions ?C")
  and     "q1  states M"
  and     "q2  states M"
obtains q1' q2' where "t_source t = Inl (q1',q2')"
                      "(q1',q2')  states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
proof -
  consider "t  shifted_transitions_for M q1 q2" | "t  distinguishing_transitions_left_alt M q1 q2" |
       "t  distinguishing_transitions_right_alt M q1 q2"
    using assms(1)
    unfolding canonical_separator_transitions_alt_def[OF assms(2,3)] by blast
  then show ?thesis proof cases
    case 1
    then show ?thesis unfolding shifted_transitions_for_def using that
      using fsm_transition_source by fastforce
  next
    case 2
    then show ?thesis unfolding distinguishing_transitions_left_alt_def using that by fastforce
  next
    case 3
    then show ?thesis unfolding distinguishing_transitions_right_alt_def using that by fastforce
  qed 
qed


lemma canonical_separator_transition_ex :
  assumes "t  transitions (canonical_separator M q1 q2)" (is "t  transitions ?C")
  and     "q1  states M"
  and     "q2  states M"
  and     "t_source t = Inl (s1,s2)"
shows "( t1  transitions M . t_source t1 = s1  t_input t1 = t_input t  t_output t1 = t_output t) 
       ( t2  transitions M . t_source t2 = s2  t_input t2 = t_input t  t_output t2 = t_output t)"
proof -
  consider "t  shifted_transitions_for M q1 q2" | "t  distinguishing_transitions_left_alt M q1 q2" |
       "t  distinguishing_transitions_right_alt M q1 q2"
    using assms(1)
    unfolding canonical_separator_transitions_alt_def[OF assms(2,3)] by blast
  then show ?thesis proof cases
    case 1
    then show ?thesis unfolding shifted_transitions_for_def 
      using product_from_transition_split[OF _ assms(2,3)]
      using assms(4) by force
  next
    case 2
    then show ?thesis unfolding distinguishing_transitions_left_alt_def
      using assms(4) by auto 
      
  next
    case 3
    then show ?thesis unfolding distinguishing_transitions_right_alt_def 
      using assms(4) by auto 
  qed 
qed


lemma canonical_separator_path_split_target_isl :
  assumes "path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) (p@[t])"
  and     "q1  states M"
  and     "q2  states M"
  shows "isl (target (initial (canonical_separator M q1 q2)) p)"
proof -
  let ?C = "(canonical_separator M q1 q2)"
  have "t  transitions ?C"
    using assms by auto
  moreover have "¬ deadlock_state ?C (t_source t)"
    using assms unfolding deadlock_state.simps by blast
  ultimately show ?thesis 
    using canonical_separator_t_source_isl assms
    by fastforce
qed


lemma canonical_separator_path_initial :
  assumes "path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) p" (is "path ?C (initial ?C) p")
  and     "q1  states M"
  and     "q2  states M"
  and     "observable M"
  and     "q1  q2"
shows " s1' s2' . target (initial (canonical_separator M q1 q2)) p = Inl (s1',s2')  ( p1 p2 . path M q1 p1  path M q2 p2  p_io p1 = p_io p2  p_io p1 = p_io p  target q1 p1 = s1'  target q2 p2 = s2')"
and   "target (initial (canonical_separator M q1 q2)) p = Inr q1  ( p1 p2 t . path M q1 (p1@[t])  path M q2 p2  p_io (p1@[t]) = p_io p  p_io p2 = butlast (p_io p))  (¬( p2 . path M q2 p2  p_io p2 = p_io p))"
and   "target (initial (canonical_separator M q1 q2)) p = Inr q2  ( p1 p2 t . path M q1 p1  path M q2 (p2@[t])  p_io p1 = butlast (p_io p)  p_io (p2@[t]) = p_io p)  (¬( p1 . path M q1 p1  p_io p1 = p_io p))"
and   "( s1' s2' . target (initial (canonical_separator M q1 q2)) p = Inl (s1',s2'))  target (initial (canonical_separator M q1 q2)) p = Inr q1  target (initial (canonical_separator M q1 q2)) p = Inr q2"
proof -

  let ?P1 = " s1' s2' . target (initial (canonical_separator M q1 q2)) p = Inl (s1',s2')  ( p1 p2 . path M q1 p1  path M q2 p2  p_io p1 = p_io p2  p_io p1 = p_io p  target q1 p1 = s1'  target q2 p2 = s2')"
  let ?P2 = "target (initial (canonical_separator M q1 q2)) p = Inr q1  ( p1 p2 t . path M q1 (p1@[t])  path M q2 p2  p_io (p1@[t]) = p_io p  p_io p2 = butlast (p_io p))  (¬( p2 . path M q2 p2  p_io p2 = p_io p))"
  let ?P3 = "target (initial (canonical_separator M q1 q2)) p = Inr q2  ( p1 p2 t . path M q1 p1  path M q2 (p2@[t])  p_io p1 = butlast (p_io p)  p_io (p2@[t]) = p_io p)  (¬( p1 . path M q1 p1  p_io p1 = p_io p))"

  have "?P1  ?P2  ?P3"
  using assms(1) proof (induction p rule: rev_induct) 
    case Nil 
    then have "target (FSM.initial (canonical_separator M q1 q2)) [] = Inl (q1, q2)"
      unfolding canonical_separator_simps[OF assms(2,3)] by auto
    then show ?case using assms(2,3,4) by fastforce
  next
    case (snoc t p)
    
    have "path ?C (initial ?C) p" and "t  transitions ?C" and "t_source t = target (initial ?C) p"
      using snoc.prems(1) by auto

    let ?P1' = "(s1' s2'. target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inl (s1', s2')  (p1 p2. path M q1 p1  path M q2 p2  p_io p1 = p_io p2  p_io p1 = p_io (p @ [t])  target q1 p1 = s1'  target q2 p2 = s2'))"
    let ?P2' = "(target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inr q1  (p1 p2 ta. path M q1 (p1 @ [ta])  path M q2 p2  p_io (p1 @ [ta]) = p_io (p @ [t])  p_io p2 = butlast (p_io (p @ [t])))  (p2. path M q2 p2  p_io p2 = p_io (p @ [t])))"
    let ?P3' = "(target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inr q2  (p1 p2 ta. path M q1 p1  path M q2 (p2 @ [ta])  p_io p1 = butlast (p_io (p @ [t]))  p_io (p2 @ [ta]) = p_io (p @ [t]))  (p1. path M q1 p1  p_io p1 = p_io (p @ [t])))"

    let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
    
    obtain p' where "path ?P (initial ?P) p'"
              and   *:"p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p'"
      using canonical_separator_path_from_shift[OF path ?C (initial ?C) p canonical_separator_path_split_target_isl[OF snoc.prems assms(2,3)] assms(2,3)]
      by blast
      
  
    let ?pL = "(map (λt. (fst (t_source t), t_input t, t_output t, fst (t_target t))) p')"
    let ?pR = "(map (λt. (snd (t_source t), t_input t, t_output t, snd (t_target t))) p')"
  
    have "path ?P (q1,q2) p'"
      using path ?P (initial ?P) p' assms(2,3) unfolding product_simps(1) from_FSM_simps(1) by simp  
    then have pL: "path (from_FSM M q1) q1 ?pL"
         and  pR: "path (from_FSM M q2) q2 ?pR"
      using product_path[of "from_FSM M q1" "from_FSM M q2" q1 q2 p'] by simp+

    have "p_io ?pL = p_io p" and "p_io ?pR = p_io p"
      using * by auto

    have pf1: "path (from_FSM M q1) (initial (from_FSM M q1)) ?pL"
      using pL assms(2) unfolding from_FSM_simps(1) by auto
    have pf2: "path (from_FSM M q2) (initial (from_FSM M q2)) ?pR"
      using pR assms(3) unfolding from_FSM_simps(1) by auto
    have pio: "p_io ?pL = p_io ?pR"
      by auto
    
    have "p_io (zip_path ?pL ?pR) = p_io ?pL"
      by (induction p'; auto)

    have zip1: "path ?P (initial ?P) (zip_path ?pL ?pR)"
    and  "target (initial ?P) (zip_path ?pL ?pR) = (target q1 ?pL, target q2 ?pR)"
      using product_path_from_paths[OF pf1 pf2 pio] assms(2,3)
      unfolding from_FSM_simps(1) by simp+
      
    have "p_io (zip_path ?pL ?pR) = p_io p"
      using p_io ?pL = p_io p p_io (zip_path ?pL ?pR) = p_io ?pL by auto 
    have "observable ?P"
      using product_observable[OF from_FSM_observable[OF assms(4)] from_FSM_observable[OF assms(4)]] by assumption
    
    have "p_io p' = p_io p"
      using * by auto
    
    obtain s1 s2 where "t_source t = Inl (s1,s2)"
      using canonical_separator_path_split_target_isl[OF snoc.prems(1) assms(2,3)] 
      by (metis t_source t = target (initial (canonical_separator M q1 q2)) p isl_def old.prod.exhaust)
  
    have "map t_target p = map (Inl o t_target) p'"
      using * by auto
    have "target (initial ?C) p = Inl (target (q1,q2) p')"
      unfolding target.simps visited_states.simps canonical_separator_simps[OF assms(2,3)] 
      unfolding map t_target p = map (Inl o t_target) p'
      by (simp add: last_map)
    then have "target (q1,q2) p'= (s1,s2)"
      using t_source t = target (initial ?C) p t_source t = Inl (s1,s2)
      by auto 
      
    have "target q1 ?pL = s1" and "target q2 ?pR = s2"  
      using product_target_split[OF target (q1,q2) p'= (s1,s2)] by auto

    consider (a) "(s1' s2'. t_target t = Inl (s1', s2'))" |
             (b) "t_target t = Inr q1" |
             (c) "t_target t = Inr q2"
      using canonical_separator_transition(4)[OF t  transitions ?C q1  states M q2  states M t_source t = Inl (s1,s2) observable M q1  q2]
      by blast
    then show "?P1'  ?P2'  ?P3'" proof cases
      case a
      then obtain s1' s2' where "t_target t = Inl (s1',s2')"
        by blast

      let ?t1 = "(s1, t_input t, t_output t, s1')"
      let ?t2 = "(s2, t_input t, t_output t, s2')"

      have "?t1  transitions M" 
      and  "?t2  transitions M"
        using canonical_separator_transition(1)[OF t  transitions ?C q1  states M q2  states M t_source t = Inl (s1,s2) observable M  q1  q2 t_target t = Inl (s1',s2')] 
        by auto

      have "target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inl (s1', s2')"
        using t_target t = Inl (s1',s2') by auto

      have "path M q1 (?pL@[?t1])"
        using path_append_transition[OF from_FSM_path[OF q1  states M pL] ?t1  transitions M] target q1 ?pL = s1 by auto
      moreover have "path M q2 (?pR@[?t2])"
        using path_append_transition[OF from_FSM_path[OF q2  states M pR] ?t2  transitions M] target q2 ?pR = s2 by auto
      moreover have "p_io (?pL@[?t1]) = p_io (?pR@[?t2])"
        by auto
      moreover have "p_io (?pL@[?t1]) = p_io (p@[t])"
        using p_io ?pL = p_io p by auto
      moreover have "target q1 (?pL@[?t1]) = s1'" and "target q2 (?pR@[?t2]) = s2'"
        by auto 
      ultimately have "path M q1 (?pL@[?t1])  path M q2 (?pR@[?t2])  p_io (?pL@[?t1]) = p_io (?pR@[?t2])  p_io (?pL@[?t1]) = p_io (p@[t])  target q1 (?pL@[?t1]) = s1'  target q2 (?pR@[?t2]) = s2'"
        by presburger
      then have "(p1 p2. path M q1 p1  path M q2 p2  p_io p1 = p_io p2  p_io p1 = p_io (p @ [t])  target q1 p1 = s1'  target q2 p2 = s2')"
        by meson
      then have ?P1'
        using target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inl (s1', s2') by auto
      then show ?thesis using target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inl (s1', s2') 
        by auto
    next
      case b
      then have "target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inr q1"
        by auto

      have "(t'(transitions M). t_source t' = s1  t_input t' = t_input t  t_output t' = t_output t)"
      and  "¬ (t'(transitions M). t_source t' = s2  t_input t' = t_input t  t_output t' = t_output t)"
        using canonical_separator_transition(2)[OF t  transitions ?C q1  states M q2  states M t_source t = Inl (s1,s2) observable M  q1  q2 b] by blast+

      then obtain t' where "t'  transitions M" and "t_source t' = s1" and "t_input t' = t_input t" and "t_output t' = t_output t"
        by blast

      have "path M q1 (?pL@[t'])"
        using path_append_transition[OF from_FSM_path[OF q1  states M pL] t'  transitions M] target q1 ?pL = s1 t_source t' = s1 by auto
      moreover have "p_io (?pL@[t']) = p_io (p@[t])"
        using p_io ?pL = p_io p t_input t' = t_input t t_output t' = t_output t by auto
      moreover have "p_io ?pR = butlast (p_io (p @ [t]))"
        using p_io ?pR = p_io p by auto
      ultimately have "path M q1 (?pL@[t'])  path M q2 ?pR  p_io (?pL@[t']) = p_io (p @ [t])  p_io ?pR = butlast (p_io (p @ [t]))"
        using from_FSM_path[OF q2  states M pR] by linarith
      then have "(p1 p2 ta. path M q1 (p1 @ [ta])  path M q2 p2  p_io (p1 @ [ta]) = p_io (p @ [t])  p_io p2 = butlast (p_io (p @ [t])))"
        by meson
            
      moreover have "(p2. path M q2 p2  p_io p2 = p_io (p @ [t]))"
      proof 
        assume "p2. path M q2 p2  p_io p2 = p_io (p @ [t])"
        then obtain p'' where "path M q2 p''  p_io p'' = p_io (p @ [t])"
          by blast
        then have "p''  []" by auto
        then obtain p2 t2 where "p'' = p2@[t2]"
          using rev_exhaust by blast
        then have "path M q2 (p2@[t2])" and "p_io (p2@[t2]) = p_io (p @ [t])"
          using path M q2 p''  p_io p'' = p_io (p @ [t]) by auto
        then have "path M q2 p2" by auto


        then have pf2': "path (from_FSM M q2) (initial (from_FSM M q2)) p2"
          using from_FSM_path_initial[OF q2  states M, of p2] by simp
        have pio': "p_io ?pL = p_io p2"
          using p_io (?pL@[t']) = p_io (p@[t]) p_io (p2@[t2]) = p_io (p @ [t]) by auto

        have zip2: "path ?P (initial ?P) (zip_path ?pL p2)"
        and  "target (initial ?P) (zip_path ?pL p2) = (target q1 ?pL, target q2 p2)"
          using product_path_from_paths[OF pf1 pf2' pio'] assms(2,3)
          unfolding from_FSM_simps(1) by simp+

        have "length p' = length p2"
          using p_io (p2@[t2]) = p_io (p @ [t]) 
          by (metis (no_types, lifting) length_map pio') 
        then have "p_io (zip_path ?pL p2) = p_io p'"
          by (induction p' p2 rule: list_induct2; auto)
        then have "p_io (zip_path ?pL p2) = p_io p"
          using * by auto
        then have "p_io (zip_path ?pL ?pR) = p_io (zip_path ?pL p2)" 
          using p_io (zip_path ?pL ?pR) = p_io p by simp

        have "p_io ?pR = p_io p2"
          using p_io ?pL = p_io p2 pio by auto 


        have l1: "length ?pL = length ?pR" by auto
        have l2: "length ?pR = length ?pL" by auto 
        have l3: "length ?pL = length p2" using length p' = length p2 by auto
        
        have "p2 = ?pR"
          using zip_path_eq_right[OF l1 l2 l3 p_io ?pR = p_io p2 observable_path_unique[OF observable ?P zip1 zip2 p_io (zip_path ?pL ?pR) = p_io (zip_path ?pL p2)]] by simp
        then have "target q2 p2 = s2"
          using target q2 ?pR = s2 by auto
        then have "t2  transitions M" and "t_source t2 = s2"
          using path M q2 (p2@[t2]) by auto
        moreover have "t_input t2 = t_input t  t_output t2 = t_output t"
          using p_io (p2@[t2]) = p_io (p @ [t]) by auto
        ultimately show "False"
          using ¬ (t'(transitions M). t_source t' = s2  t_input t' = t_input t  t_output t' = t_output t) by blast
      qed

      ultimately have ?P2' 
        by blast
      moreover have ?P3' 
        using  q1  q2 t_target t = Inr q1 by auto
      moreover have ?P1'
       using target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inr q1 by auto
     ultimately show ?thesis
       by blast
    next
      case c
      then have "target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inr q2"
        by auto

      have "(t'(transitions M). t_source t' = s2  t_input t' = t_input t  t_output t' = t_output t)"
      and  "¬ (t'(transitions M). t_source t' = s1  t_input t' = t_input t  t_output t' = t_output t)"
        using canonical_separator_transition(3)[OF t  transitions ?C q1  states M q2  states M t_source t = Inl (s1,s2) observable M  q1  q2 c] by blast+

      then obtain t' where "t'  transitions M" and "t_source t' = s2" and "t_input t' = t_input t" and "t_output t' = t_output t"
        by blast

      have "path M q2 (?pR@[t'])"
        using path_append_transition[OF from_FSM_path[OF q2  states M pR] t'  transitions M] target q2 ?pR = s2 t_source t' = s2 by auto
      moreover have "p_io (?pR@[t']) = p_io (p@[t])"
        using p_io ?pR = p_io p t_input t' = t_input t t_output t' = t_output t by auto
      moreover have "p_io ?pL = butlast (p_io (p @ [t]))"
        using p_io ?pL = p_io p by auto
      ultimately have "path M q2 (?pR@[t'])  path M q1 ?pL  p_io (?pR@[t']) = p_io (p @ [t])  p_io ?pL = butlast (p_io (p @ [t]))"
        using from_FSM_path[OF q1  states M pL] by linarith
      then have "(p1 p2 ta. path M q1 p1  path M q2 (p2 @ [ta])  p_io p1 = butlast (p_io (p @ [t]))  p_io (p2 @ [ta]) = p_io (p @ [t]))"
        by meson
            
      moreover have "(p1. path M q1 p1  p_io p1 = p_io (p @ [t]))"
      proof 
        assume "p1. path M q1 p1  p_io p1 = p_io (p @ [t])"
        then obtain p'' where "path M q1 p''  p_io p'' = p_io (p @ [t])"
          by blast
        then have "p''  []" by auto
        then obtain p1 t1 where "p'' = p1@[t1]"
          using rev_exhaust by blast
        then have "path M q1 (p1@[t1])" and "p_io (p1@[t1]) = p_io (p @ [t])"
          using path M q1 p''  p_io p'' = p_io (p @ [t]) by auto
        then have "path M q1 p1" 
          by auto
        then have pf1': "path (from_FSM M q1) (initial (from_FSM M q1)) p1"
          using from_FSM_path_initial[OF q1  states M, of p1] by simp
        have pio': "p_io p1 = p_io ?pR"
          using p_io (?pR@[t']) = p_io (p@[t]) p_io (p1@[t1]) = p_io (p @ [t]) by auto

        have zip2: "path ?P (initial ?P) (zip_path p1 ?pR)"
          using product_path_from_paths[OF pf1' pf2 pio']
          unfolding from_FSM_simps(1) by simp

        have "length p' = length p1"
          using p_io (p1@[t1]) = p_io (p @ [t]) 
          by (metis (no_types, lifting) length_map pio') 
        then have "p_io (zip_path p1 ?pR) = p_io p'"
          using p_io p1 = p_io ?pR by (induction p' p1 rule: list_induct2; auto)
        then have "p_io (zip_path p1 ?pR) = p_io p"
          using * by auto
        then have "p_io (zip_path ?pL ?pR) = p_io (zip_path p1 ?pR)" 
          using p_io (zip_path ?pL ?pR) = p_io p by simp
        
        have l1: "length ?pL = length ?pR" by auto
        have l2: "length ?pR = length p1" using length p' = length p1 by auto
        have l3: "length p1 = length ?pR" using l2 by auto
        
        have "?pL = p1"
          using zip_path_eq_left[OF l1 l2 l3 observable_path_unique[OF observable ?P zip1 zip2 p_io (zip_path ?pL ?pR) = p_io (zip_path p1 ?pR)]] by simp
        then have "target q1 p1 = s1"
          using target q1 ?pL = s1 by auto
        then have "t1  transitions M" and "t_source t1 = s1"
          using path M q1 (p1@[t1]) by auto
        moreover have "t_input t1 = t_input t  t_output t1 = t_output t"
          using p_io (p1@[t1]) = p_io (p @ [t]) by auto
        ultimately show "False"
          using ¬ (t'(transitions M). t_source t' = s1  t_input t' = t_input t  t_output t' = t_output t) by blast
      qed

      ultimately have ?P3' 
        by blast
      moreover have ?P2' 
        using q1  q2 t_target t = Inr q2 by auto
      moreover have ?P1'
        using target (initial (canonical_separator M q1 q2)) (p @ [t]) = Inr q2 by auto
      ultimately show ?thesis
        by blast
    qed 
  qed

  then show  " s1' s2' . target (initial (canonical_separator M q1 q2)) p = Inl (s1',s2')  ( p1 p2 . path M q1 p1  path M q2 p2  p_io p1 = p_io p2  p_io p1 = p_io p  target q1 p1 = s1'  target q2 p2 = s2')"
       and   "target (initial (canonical_separator M q1 q2)) p = Inr q1  ( p1 p2 t . path M q1 (p1@[t])  path M q2 p2  p_io (p1@[t]) = p_io p  p_io p2 = butlast (p_io p))  (¬( p2 . path M q2 p2  p_io p2 = p_io p))"
       and   "target (initial (canonical_separator M q1 q2)) p = Inr q2  ( p1 p2 t . path M q1 p1  path M q2 (p2@[t])  p_io p1 = butlast (p_io p)  p_io (p2@[t]) = p_io p)  (¬( p1 . path M q1 p1  p_io p1 = p_io p))"
    by blast+

  
  show   "( s1' s2' . target (initial (canonical_separator M q1 q2)) p = Inl (s1',s2'))  target (initial (canonical_separator M q1 q2)) p = Inr q1  target (initial (canonical_separator M q1 q2)) p = Inr q2"
  proof (cases p rule: rev_cases)
    case Nil
    then show ?thesis unfolding canonical_separator_simps(1)[OF assms(2,3)] by auto
  next
    case (snoc p' t)
    then have "t  transitions ?C" and "target (initial (canonical_separator M q1 q2)) p = t_target t"
      using assms(1) by auto
    then have "t  (transitions ?C)"
      by auto
    obtain s1 s2 where "t_source t = Inl (s1,s2)"
      using canonical_separator_t_source_isl[OF t  (transitions ?C) assms(2,3)]
      by (metis sum.collapse(1) surjective_pairing)
    show ?thesis
      using canonical_separator_transition(4)[OF t  transitions ?C assms(2,3) t_source t = Inl (s1,s2) assms(4) q1  q2] 
            target (initial (canonical_separator M q1 q2)) p = t_target t
      by simp 
  qed 
qed


(* does not assume observability of M (in contrast to the much stronger canonical_separator_path_initial) *)
lemma canonical_separator_path_initial_ex :
  assumes "path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) p" (is "path ?C (initial ?C) p")
  and     "q1  states M"
  and     "q2  states M"
shows "( p1 . path M q1 p1  p_io p1 = p_io p)  ( p2 . path M q2 p2  p_io p2 = p_io p)"
and   "( p1 p2 . path M q1 p1  path M q2 p2  p_io p1 = butlast (p_io p)  p_io p2 = butlast (p_io p))"
proof -
  have "(( p1 . path M q1 p1  p_io p1 = p_io p)  ( p2 . path M q2 p2  p_io p2 = p_io p))
          ( p1 p2 . path M q1 p1  path M q2 p2  p_io p1 = butlast (p_io p)  p_io p2 = butlast (p_io p))"
  using assms proof (induction p rule: rev_induct) 
    case Nil
    then show ?case by auto
  next
    case (snoc t p)
    then have "path ?C (initial ?C) p" and "t  transitions ?C" and "t_source t = target (initial ?C) p"
      by auto
  
    let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
    
    obtain p' where "path ?P (initial ?P) p'"
              and   *:"p = map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) p'"
      using canonical_separator_path_from_shift[OF path ?C (initial ?C) p canonical_separator_path_split_target_isl[OF snoc.prems(1) assms(2,3)] assms(2,3)]
      by blast
  
    let ?pL = "(map (λt. (fst (t_source t), t_input t, t_output t, fst (t_target t))) p')"
    let ?pR = "(map (λt. (snd (t_source t), t_input t, t_output t, snd (t_target t))) p')"
  
    have "path ?P (q1,q2) p'"
      using path ?P (initial ?P) p' assms(2,3) by simp
  
    then have pL: "path (from_FSM M q1) q1 ?pL"
         and  pR: "path (from_FSM M q2) q2 ?pR"
      using product_path[of "from_FSM M q1" "from_FSM M q2" q1 q2 p'] by auto

    have "p_io ?pL = butlast (p_io (p@[t]))" and "p_io ?pR = butlast (p_io (p@[t]))"
      using * by auto
    then have "path M q1 ?pL  path M q2 ?pR  p_io ?pL = butlast (p_io (p@[t]))  p_io ?pR = butlast (p_io (p@[t]))"
      using from_FSM_path[OF q1  states M pL] from_FSM_path[OF q2  states M pR] by auto
    then have "(p1 p2. path M q1 p1  path M q2 p2  p_io p1 = butlast (p_io (p @ [t]))  p_io p2 = butlast (p_io (p @ [t])))"
      by blast
    
    obtain s1 s2 where "t_source t = Inl (s1,s2)"
      using canonical_separator_path_split_target_isl[OF snoc.prems(1) assms(2,3)] 
      by (metis t_source t = target (initial (canonical_separator M q1 q2)) p isl_def old.prod.exhaust)
  
    have "map t_target p = map (Inl o t_target) p'"
      using * by auto
    then have "target (initial ?C) p = Inl (target (q1,q2) p')"
      unfolding target.simps visited_states.simps canonical_separator_simps(1)[OF assms(2,3)] 
      by (simp add: last_map) 
    then have "target (q1,q2) p'= (s1,s2)"
      using t_source t = target (initial ?C) p t_source t = Inl (s1,s2)
      by auto 
      
    have "target q1 ?pL = s1" and "target q2 ?pR = s2"  
      using product_target_split[OF target (q1,q2) p'= (s1,s2)] by auto
  
    consider (a) "(t1(transitions M). t_source t1 = s1  t_input t1 = t_input t  t_output t1 = t_output t)" |
             (b) "(t2(transitions M). t_source t2 = s2  t_input t2 = t_input t  t_output t2 = t_output t)"
      using canonical_separator_transition_ex[OF t  transitions ?C q1  states M q2  states M t_source t = Inl (s1,s2)] by blast
    then show ?case proof cases
      case a
      then obtain t1 where "t1  transitions M" and "t_source t1 = s1" and "t_input t1 = t_input t" and "t_output t1 = t_output t" 
        by blast
  
      have "t_source t1 = target q1 ?pL"
        using target q1 ?pL = s1 t_source t1 = s1 by auto
      then have "path M q1 (?pL@[t1])"
        using pL t1  transitions M
        by (meson from_FSM_path path_append_transition snoc.prems(2))
      moreover have "p_io (?pL@[t1]) = p_io (p@[t])"
        using * t_input t1 = t_input t t_output t1 = t_output t by auto
      ultimately show ?thesis
        using (p1 p2. path M q1 p1  path M q2 p2  p_io p1 = butlast (p_io (p @ [t]))  p_io p2 = butlast (p_io (p @ [t])))
        by meson
    next
      case b
      then obtain t2 where "t2  transitions M" and "t_source t2 = s2" and "t_input t2 = t_input t" and "t_output t2 = t_output t" 
        by blast
  
      have "t_source t2 = target q2 ?pR"
        using target q2 ?pR = s2 t_source t2 = s2 by auto
      then have "path M q2 (?pR@[t2])"
        using pR t2  transitions M
        by (meson from_FSM_path path_append_transition snoc.prems(3))
      moreover have "p_io (?pR@[t2]) = p_io (p@[t])"
        using * t_input t2 = t_input t t_output t2 = t_output t by auto
      ultimately show ?thesis
        using (p1 p2. path M q1 p1  path M q2 p2  p_io p1 = butlast (p_io (p @ [t]))  p_io p2 = butlast (p_io (p @ [t])))
        by meson
    qed
  qed
  then show "( p1 . path M q1 p1  p_io p1 = p_io p)  ( p2 . path M q2 p2  p_io p2 = p_io p)"
       and  "( p1 p2 . path M q1 p1  path M q2 p2  p_io p1 = butlast (p_io p)  p_io p2 = butlast (p_io p))"
    by blast+
qed


lemma canonical_separator_language :
  assumes "q1  states M"
  and     "q2  states M"
shows "L (canonical_separator M q1 q2)  L (from_FSM M q1)  L (from_FSM M q2)" (is "L ?C  L ?M1  L ?M2")
proof 
  fix io assume "io  L (canonical_separator M q1 q2)"
  then obtain p where *: "path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) p" and **: "p_io p = io"
    by auto
  
  show "io  L (from_FSM M q1)  L (from_FSM M q2)"
    using canonical_separator_path_initial_ex[OF * assms] unfolding ** 
    using from_FSM_path_initial[OF assms(1)] from_FSM_path_initial[OF assms(2)]  
    unfolding LS.simps by blast
qed


lemma canonical_separator_language_prefix :
  assumes "io@[xy]  L (canonical_separator M q1 q2)"
  and     "q1  states M"
  and     "q2  states M"
  and     "observable M"
  and     "q1  q2"
shows "io  LS M q1"
and   "io  LS M q2"
proof -
  let ?C = "(canonical_separator M q1 q2)"
  obtain p where "path ?C (initial ?C) p" and "p_io p = io@[xy]"
    using assms(1) by auto

  consider (a) "(s1' s2'. target (initial (canonical_separator M q1 q2)) p = Inl (s1', s2'))" |
           (b) "target (initial (canonical_separator M q1 q2)) p = Inr q1" | 
           (c) "target (initial (canonical_separator M q1 q2)) p = Inr q2"
    using canonical_separator_path_initial(4)[OF path ?C (initial ?C) p assms(2,3,4,5)] by blast
  then have "io  LS M q1  io  LS M q2"
  proof cases
    case a
    then obtain s1 s2 where *: "target (initial (canonical_separator M q1 q2)) p = Inl (s1, s2)"
      by blast
    show ?thesis using canonical_separator_path_initial(1)[OF path ?C (initial ?C) p assms(2,3,4,5) *] language_prefix
      by (metis (mono_tags, lifting) LS.simps p_io p = io @ [xy] mem_Collect_eq )
  next
    case b
    show ?thesis using canonical_separator_path_initial(2)[OF path ?C (initial ?C) p assms(2,3,4,5) b]
      using p_io p = io @ [xy] by fastforce      
  next
    case c
    show ?thesis using canonical_separator_path_initial(3)[OF path ?C (initial ?C) p assms(2,3,4,5) c]
      using p_io p = io @ [xy] by fastforce
  qed
  then show "io  LS M q1" and   "io  LS M q2"
    by auto
qed


lemma canonical_separator_distinguishing_transitions_left_containment :
  assumes "t  (distinguishing_transitions_left M q1 q2)"
      and "q1  states M" and "q2  states M"
    shows "t  transitions (canonical_separator M q1 q2)" 
  using assms(1) unfolding canonical_separator_transitions_def[OF assms(2,3)] by blast


lemma canonical_separator_distinguishing_transitions_right_containment :
  assumes "t  (distinguishing_transitions_right M q1 q2)"
      and "q1  states M" and "q2  states M"
  shows "t  transitions (canonical_separator M q1 q2)" (is "t  transitions ?C")
   using assms(1) unfolding canonical_separator_transitions_def[OF assms(2,3)] by blast


lemma distinguishing_transitions_left_alt_intro :
  assumes "(s1,s2)  states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
  and "(t  transitions M. t_source t = s1  t_input t = x  t_output t = y)" 
  and "¬(t  transitions M. t_source t = s2  t_input t = x  t_output t = y)" 
shows "(Inl (s1,s2), x, y, Inr q1)  distinguishing_transitions_left_alt M q1 q2"
  using assms unfolding distinguishing_transitions_left_alt_def
  by auto 


lemma distinguishing_transitions_left_right_intro :
  assumes "(s1,s2)  states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
  and "¬(t  transitions M. t_source t = s1  t_input t = x  t_output t = y)" 
  and "(t  transitions M. t_source t = s2  t_input t = x  t_output t = y)" 
shows "(Inl (s1,s2), x, y, Inr q2)  distinguishing_transitions_right_alt M q1 q2"
  using assms unfolding distinguishing_transitions_right_alt_def
  by auto 


lemma canonical_separator_io_from_prefix_left :
  assumes "io @ [io1]  LS M q1"
  and     "io  LS M q2"
  and     "q1  states M"
  and     "q2  states M"
  and     "observable M"
  and     "q1  q2"
shows "io @ [io1]  L (canonical_separator M q1 q2)"
proof -
  let ?C = "canonical_separator M q1 q2"

  obtain p1 where "path M q1 p1" and "p_io p1 = io @ [io1]"
    using io @ [io1]  LS M q1 by auto
  then have "p1  []"
    by auto
  then obtain pL tL where "p1 = pL @ [tL]"
    using rev_exhaust by blast
  then have "path M q1 (pL@[tL])" and "path M q1 pL" and "p_io pL = io" and "tL  transitions M" 
        and "t_input tL = fst io1" and "t_output tL = snd io1" and "p_io (pL@[tL]) = io @ [io1]"
    using path M q1 p1 p_io p1 = io @ [io1] by auto
  then have pLf: "path (from_FSM M q1) (initial (from_FSM M q1)) pL" 
        and pLf': "path (from_FSM M q1) (initial (from_FSM M q1)) (pL@[tL])"
    using from_FSM_path_initial[OF q1  states M] by auto

  obtain pR where "path M q2 pR" and "p_io pR = io"
    using io  LS M q2 by auto
  then have pRf: "path (from_FSM M q2) (initial (from_FSM M q2)) pR"
    using from_FSM_path_initial[OF q2  states M] by auto

  have "p_io pL = p_io pR"
    using p_io pL = io p_io pR = io by auto

  let ?pLR = "zip_path pL pR"
  let ?pCLR = "map shift_Inl ?pLR"
  let ?P = "product (from_FSM M q1) (from_FSM M q2)"

  have "path ?P (initial ?P) ?pLR"
  and  "target (initial ?P) ?pLR = (target q1 pL, target q2 pR)"
    using product_path_from_paths[OF pLf pRf p_io pL = p_io pR]
    unfolding from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)] by linarith+

  have "path ?C (initial ?C) ?pCLR"
    using canonical_separator_path_shift[OF assms(3,4)] path ?P (initial ?P) ?pLR 
    by simp 

  have "isl (target (initial ?C) ?pCLR)" 
    unfolding canonical_separator_simps(1)[OF assms(3,4)] by (cases ?pLR rule: rev_cases; auto)
  then obtain s1 s2 where "target (initial ?C) ?pCLR = Inl (s1,s2)"
    by (metis (no_types, lifting) path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) (map (λt. (Inl (t_source t), t_input t, t_output t, Inl (t_target t))) (map (λt. ((t_source (fst t), t_source (snd t)), t_input (fst t), t_output (fst t), t_target (fst t), t_target (snd t))) (zip pL pR))) 
          assms(3) assms(4) assms(5) assms(6) canonical_separator_path_initial(4) sum.discI(2))
  then have "Inl (s1,s2)  states ?C"
    using path_target_is_state[OF path ?C (initial ?C) ?pCLR] by simp
  then have "(s1,s2)  states ?P"
    using canonical_separator_states[OF _ assms(3,4)] by force

  have "target (initial ?P) ?pLR = (s1,s2)"
    using target (initial ?C) ?pCLR = Inl (s1,s2) assms(3,4) 
    unfolding canonical_separator_simps(1)[OF assms(3,4)] product_simps(1) from_FSM_simps target.simps visited_states.simps 
    by (cases ?pLR rule: rev_cases; auto)
  then have "target q1 pL = s1" and "target q2 pR = s2"
    using target (initial ?P) ?pLR = (target q1 pL, target q2 pR) by auto
  then have "t_source tL = s1"
    using path M q1 (pL@[tL]) by auto

  show ?thesis proof (cases " tR  (transitions M) . t_source tR = target q2 pR  t_input tR = t_input tL  t_output tR = t_output tL")
    case True
    then obtain tR where "tR  (transitions M)" and "t_source tR = target q2 pR" and "t_input tR = t_input tL" and "t_output tR = t_output tL"
      by blast
    
    have "t_source tR  states M"
      unfolding t_source tR = target q2 pR target q2 pR = s2 
      using (s1,s2)  states ?P product_simps(2) from_FSM_simps(2) assms(3,4) by simp

    then have "tR  transitions M"
      using tR  (transitions M) t_input tR = t_input tL t_output tR = t_output tL tL  transitions M by auto

    then have "path M q2 (pR@[tR])" 
      using path M q2 pR t_source tR = target q2 pR path_append_transition by metis
    then have pRf': "path (from_FSM M q2) (initial (from_FSM M q2)) (pR@[tR])"
      using from_FSM_path_initial[OF q2  states M] by auto
    
    let ?PP = "(zip_path (pL@[tL]) (pR@[tR]))"
    let ?PC = "map shift_Inl ?PP"

    have "length pL = length pR"
      using p_io pL = p_io pR map_eq_imp_length_eq by blast
    moreover have "p_io (pL@[tL]) = p_io (pR@[tR])"
      using p_io pR = io t_input tL = fst io1 t_output tL = snd io1 t_input tR = t_input tL t_output tR = t_output tL p_io (pL@[tL]) = io@[io1] by auto
    ultimately have "p_io ?PP = p_io (pL@[tL])"
      by (induction pL pR rule: list_induct2; auto)

    have "p_io ?PC = p_io ?PP"
      by auto
           
    have "path ?P (initial ?P) ?PP"
      using product_path_from_paths(1)[OF pLf' pRf' p_io (pL@[tL]) = p_io (pR@[tR])] by assumption
    then have "path ?C (initial ?C) ?PC"
      using canonical_separator_path_shift[OF assms(3,4)] by simp    
    moreover have "p_io ?PC = io@[io1]"
      using p_io (pL@[tL]) = io@[io1]  p_io ?PP = p_io (pL@[tL])  p_io ?PC = p_io ?PP by simp
    ultimately have " p . path ?C (initial ?C) p  p_io p = io@[io1]"
      by blast
    then show ?thesis unfolding LS.simps by force
  next
    case False

    let ?t = "(Inl (s1,s2), t_input tL, t_output tL, Inr q1)"

    have "(s1,s2)  reachable_states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
      by (metis (no_types, lifting) path (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) (FSM.initial (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))) (zip_path pL pR) target (FSM.initial (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))) (zip_path pL pR) = (s1, s2) reachable_states_intro)
    moreover have "(tRFSM.transitions M.
           t_source tR = target q1 pL  t_input tR = t_input tL  t_output tR = t_output tL)"
      using tL  transitions M path M q1 (pL@[tL])
      by auto     
    ultimately have "?t  (distinguishing_transitions_left_alt M q1 q2)"
      using distinguishing_transitions_left_alt_intro[OF _ _ False ]  q1  q2
      unfolding target q1 pL = s1 target q2 pR = s2
      using (s1, s2)  FSM.states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) by blast
    then have "?t  transitions ?C" 
      using canonical_separator_distinguishing_transitions_left_containment[OF _ assms(3,4)] unfolding distinguishing_transitions_left_alt_alt_def by blast 
    then have "path ?C (initial ?C) (?pCLR@[?t])"
      using path ?C (initial ?C) ?pCLR target (initial ?C) ?pCLR = Inl (s1,s2) 
      by (simp add: path_append_transition)

    have "length pL = length pR"
      using p_io pL = p_io pR 
      using map_eq_imp_length_eq by blast
    then have "p_io ?pCLR = p_io pL" 
      by (induction pL pR rule: list_induct2; auto)
    then have "p_io (?pCLR@[?t]) = io @ [io1]"
      using p_io pL = io t_input tL = fst io1 t_output tL = snd io1
      by auto
    then have " p . path ?C (initial ?C) p  p_io p = io@[io1]"
      using path ?C (initial ?C) (?pCLR@[?t]) by meson
    then show ?thesis 
      unfolding LS.simps by force
  qed
qed





lemma canonical_separator_path_targets_language :
  assumes "path (canonical_separator M q1 q2) (initial (canonical_separator M q1 q2)) p"
  and     "observable M" 
  and     "q1  states M"
  and     "q2  states M"
  and     "q1  q2"
shows "isl (target (initial (canonical_separator M q1 q2)) p)  p_io p  LS M q1  LS M q2"
and   "(target (initial (canonical_separator M q1 q2)) p) = Inr q1  p_io p  LS M q1 - LS M q2  p_io (butlast p)  LS M q1  LS M q2"
and   "(target (initial (canonical_separator M q1 q2)) p) = Inr q2  p_io p  LS M q2 - LS M q1  p_io (butlast p)  LS M q1  LS M q2"
and   "p_io p  LS M q1  LS M q2  isl (target (initial (canonical_separator M q1 q2)) p)"
and   "p_io p  LS M q1 - LS M q2  target (initial (canonical_separator M q1 q2)) p = Inr q1"
and   "p_io p  LS M q2 - LS M q1  target (initial (canonical_separator M q1 q2)) p = Inr q2"
proof -
  let ?C = "canonical_separator M q1 q2"
  let ?tgt = "target (initial ?C) p"

  show "isl ?tgt  p_io p  LS M q1  LS M q2"
  proof -
    assume "isl ?tgt"
    then obtain s1 s2 where "?tgt = Inl (s1,s2)"
      by (metis isl_def old.prod.exhaust)
    then obtain p1 p2 where "path M q1 p1" and "path M q2 p2" and "p_io p1 = p_io p" and "p_io p2 = p_io p" 
      using canonical_separator_path_initial(1)[OF assms(1) q1  states M q2  states M observable M  q1  q2 ?tgt = Inl (s1,s2) ] by force
    then show "p_io p  LS M q1  LS M q2"
      unfolding LS.simps by force
  qed
  moreover show "?tgt = Inr q1  p_io p  LS M q1 - LS M q2  p_io (butlast p)  LS M q1  LS M q2"
  proof -
    assume "?tgt = Inr q1"
    obtain p1 p2 t where "path M q1 (p1 @ [t])" and "path M q2 p2" and "p_io (p1 @ [t]) = p_io p" 
                     and "p_io p2 = butlast (p_io p)" and "(p2. path M q2 p2  p_io p2 = p_io p)" 
      using canonical_separator_path_initial(2)[OF assms(1) q1  states M q2  states M 
            observable M  q1  q2 ?tgt = Inr q1] 
      by meson

    have "path M q1 p1"
      using path M q1 (p1@[t]) by auto
    have "p_io p1 = butlast (p_io p)"
      using p_io (p1 @ [t]) = p_io p 
      by (metis (no_types, lifting) butlast_snoc map_butlast)

    have "p_io p  LS M q1" 
      using path M q1 (p1@[t]) p_io (p1 @ [t]) = p_io p unfolding LS.simps by force
    moreover have "p_io p  LS M q2"
      using (p2. path M q2 p2  p_io p2 = p_io p) unfolding LS.simps by force
    moreover have "butlast (p_io p)  LS M q1"
      using path M q1 p1 p_io p1 = butlast (p_io p) unfolding LS.simps by force
    moreover have "butlast (p_io p)  LS M q2"
      using path M q2 p2 p_io p2 = butlast (p_io p) unfolding LS.simps by force
    ultimately show "p_io p  LS M q1 - LS M q2  p_io (butlast p)  LS M q1  LS M q2"
      by (simp add: map_butlast)
  qed 
  moreover show "?tgt = Inr q2  p_io p  LS M q2 - LS M q1  p_io (butlast p)  LS M q1  LS M q2"
  proof -
    assume "?tgt = Inr q2"
    obtain p1 p2 t where "path M q2 (p2 @ [t])" and "path M q1 p1" and "p_io (p2 @ [t]) = p_io p" 
                     and "p_io p1 = butlast (p_io p)" and "(p2. path M q1 p2  p_io p2 = p_io p)" 
      using canonical_separator_path_initial(3)[OF assms(1) q1  states M q2  states M 
            observable M q1  q2 ?tgt = Inr q2] 
      by meson

    have "path M q2 p2"
      using path M q2 (p2@[t]) by auto
    have "p_io p2 = butlast (p_io p)"
      using p_io (p2 @ [t]) = p_io p 
      by (metis (no_types, lifting) butlast_snoc map_butlast)

    have "p_io p  LS M q2" 
      using path M q2 (p2@[t]) p_io (p2 @ [t]) = p_io p unfolding LS.simps by force
    moreover have "p_io p  LS M q1"
      using (p2. path M q1 p2  p_io p2 = p_io p) unfolding LS.simps by force
    moreover have "butlast (p_io p)  LS M q1"
      using path M q1 p1 p_io p1 = butlast (p_io p) unfolding LS.simps by force
    moreover have "butlast (p_io p)  LS M q2"
      using path M q2 p2 p_io p2 = butlast (p_io p) unfolding LS.simps by force
    ultimately show "p_io p  LS M q2 - LS M q1  p_io (butlast p)  LS M q1  LS M q2"
      by (simp add: map_butlast)
  qed 
  moreover have "isl ?tgt  ?tgt = Inr q1  ?tgt = Inr q2"
    using canonical_separator_path_initial(4)[OF assms(1) q1  states M q2  states M observable M  q1  q2] by force
  ultimately show "p_io p  LS M q1  LS M q2  isl (target (initial (canonical_separator M q1 q2)) p)"
             and  "p_io p  LS M q1 - LS M q2  target (initial (canonical_separator M q1 q2)) p = Inr q1"
             and  "p_io p  LS M q2 - LS M q1  target (initial (canonical_separator M q1 q2)) p = Inr q2"
    by blast+
qed
  

lemma canonical_separator_language_target :
  assumes "io  L (canonical_separator M q1 q2)"
  and     "observable M" 
  and     "q1  states M"
  and     "q2  states M"
  and     "q1  q2"
shows "io  LS M q1 - LS M q2  io_targets (canonical_separator M q1 q2) io (initial (canonical_separator M q1 q2)) = {Inr q1}"
and   "io  LS M q2 - LS M q1  io_targets (canonical_separator M q1 q2) io (initial (canonical_separator M q1 q2)) = {Inr q2}"
proof -
  let ?C = "canonical_separator M q1 q2"
  obtain p where "path ?C (initial ?C) p" and "p_io p = io"
    using assms(1) by force

  show "io  LS M q1 - LS M q2  io_targets (canonical_separator M q1 q2) io (initial (canonical_separator M q1 q2)) = {Inr q1}"
  proof -
    assume "io  LS M q1 - LS M q2"
    then have "p_io p  LS M q1 - LS M q2"
      using p_io p = io by auto
    have "Inr q1  io_targets ?C io (initial ?C)"
      using canonical_separator_path_targets_language(5)[OF path ?C (initial ?C) p assms(2,3,4,5) p_io p  LS M q1 - LS M q2]
      using path ?C (initial ?C) p unfolding io_targets.simps 
      by (metis (mono_tags, lifting) p_io p = io mem_Collect_eq)
    then show ?thesis
      by (metis (mono_tags, lifting) assms(1) assms(2) assms(3) assms(4) canonical_separator_observable observable_io_targets singletonD)
  qed

  show "io  LS M q2 - LS M q1  io_targets (canonical_separator M q1 q2) io (initial (canonical_separator M q1 q2)) = {Inr q2}"
  proof -
    assume "io  LS M q2 - LS M q1"
    then have "p_io p  LS M q2 - LS M q1"
      using p_io p = io by auto
    have "Inr q2  io_targets ?C io (initial ?C)"
      using canonical_separator_path_targets_language(6)[OF path ?C (initial ?C) p assms(2,3,4,5) p_io p  LS M q2 - LS M q1]
      using path ?C (initial ?C) p unfolding io_targets.simps 
      by (metis (mono_tags, lifting) p_io p = io mem_Collect_eq)
    then show ?thesis
      by (metis (mono_tags, lifting) assms(1) assms(2) assms(3) assms(4) canonical_separator_observable observable_io_targets singletonD)
  qed
qed


lemma canonical_separator_language_intersection :
  assumes "io  LS M q1"
  and     "io  LS M q2"
  and     "q1  states M"
  and     "q2  states M"
shows "io  L (canonical_separator M q1 q2)" (is "io  L ?C")
proof -
  let ?P = "product (from_FSM M q1) (from_FSM M q2)"

  have "io  L ?P"
    using io  LS M q1 io  LS M q2 product_language[of "from_FSM M q1" "from_FSM M q2"] 
    unfolding from_FSM_language[OF q1  states M] from_FSM_language[OF q2  states M]
    by blast
  then obtain p where "path ?P (initial ?P) p" and "p_io p = io"
    by auto
  then have *: "path ?C (initial ?C) (map shift_Inl p)"
    using canonical_separator_path_shift[OF assms(3,4)] by auto
  have **: "p_io (map shift_Inl p) = io"
    using p_io p = io by (induction p; auto)
  show "io  L ?C" 
    using language_state_containment[OF * **] by assumption
qed


lemma canonical_separator_deadlock :
  assumes "q1  states M"
      and "q2  states M"
    shows "deadlock_state (canonical_separator M q1 q2) (Inr q1)"
      and "deadlock_state (canonical_separator M q1 q2) (Inr q2)"
  unfolding deadlock_state.simps 
  by (metis assms(1) assms(2) canonical_separator_t_source_isl sum.disc(2))+


lemma canonical_separator_isl_deadlock :
  assumes "Inl (q1',q2')  states (canonical_separator M q1 q2)"
      and "x  inputs M"
      and "completely_specified M"
      and "¬( t  transitions (canonical_separator M q1 q2) . t_source t = Inl (q1',q2')  t_input t = x  isl (t_target t))"
      and "q1  states M"
      and "q2  states M"
obtains y1 y2 where "(Inl (q1',q2'),x,y1,Inr q1)  transitions (canonical_separator M q1 q2)"
                    "(Inl (q1',q2'),x,y2,Inr q2)  transitions (canonical_separator M q1 q2)"
proof -
  let ?C = "(canonical_separator M q1 q2)"
  let ?P = "(product (from_FSM M q1) (from_FSM M q2))"

  have "(q1',q2')  states ?P"
    using assms(1) unfolding canonical_separator_simps[OF assms(5,6)] by fastforce
  then have "(q1',q2')  states ?P"
    using reachable_state_is_state by force
  then have "q1'  states M" and "q2'  states M"
    using assms(5,6) by auto
  then obtain y1 y2 where "y1  h_out M (q1',x)" and "y2  h_out M (q2',x)"
    by (metis (no_types, lifting) assms(2,3) h_out.simps completely_specified_alt_def mem_Collect_eq) 
  moreover have "h_out M (q1',x)  h_out M (q2',x) = {}"
  proof (rule ccontr)
    assume "h_out M (q1', x)  h_out M (q2', x)  {}"
    then obtain y where "y  h_out M (q1', x)  h_out M (q2', x)" by blast
    then obtain q1'' q2'' where "((q1',q2'),x,y,(q1'',q2''))  transitions ?P"
      unfolding product_transitions_def h_out.simps using assms(5,6) by auto
    then have "(Inl (q1',q2'),x,y,Inl (q1'',q2''))  transitions ?C"
      using (q1',q2')  states ?P unfolding canonical_separator_transitions_def[OF assms(5,6)] h_out.simps by blast
    then show "False"
      using assms(4) by auto
  qed
  ultimately have "y1  h_out M (q1',x) - h_out M (q2',x)"
             and  "y2  h_out M (q2',x) - h_out M (q1',x)"
    by blast+

  let ?t1 = "(Inl (q1',q2'),x,y1,Inr q1)"
  let ?t2 = "(Inl (q1',q2'),x,y2,Inr q2)"

  have "?t1  distinguishing_transitions_left M q1 q2"
    using (q1',q2')  states ?P y1  h_out M (q1',x) - h_out M (q2',x)
    unfolding distinguishing_transitions_left_def by auto
  then have "?t1  transitions (canonical_separator M q1 q2)"
    unfolding canonical_separator_transitions_def[OF assms(5,6)] by blast

  have "?t2  distinguishing_transitions_right M q1 q2"
    using (q1',q2')  states ?P y2  h_out M (q2',x) - h_out M (q1',x)
    unfolding distinguishing_transitions_right_def by auto
  then have "?t2  transitions (canonical_separator M q1 q2)"
    unfolding canonical_separator_transitions_def[OF assms(5,6)] by blast

  show ?thesis 
    using that ?t1  transitions (canonical_separator M q1 q2) ?t2  transitions (canonical_separator M q1 q2) by blast
qed


lemma canonical_separator_deadlocks :
  assumes "q1  states M" and "q2  states M"
shows "deadlock_state (canonical_separator M q1 q2) (Inr q1)"
and   "deadlock_state (canonical_separator M q1 q2) (Inr q2)"
  using canonical_separator_t_source_isl[OF _ assms]
  unfolding deadlock_state.simps by force+


lemma state_separator_from_canonical_separator_language_target :
  assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
  and     "io  L A"
  and     "observable M" 
  and     "q1  states M"
  and     "q2  states M"
  and     "q1  q2"
shows "io  LS M q1 - LS M q2  io_targets A io (initial A) = {Inr q1}"
and   "io  LS M q2 - LS M q1  io_targets A io (initial A) = {Inr q2}"
and   "io  LS M q1  LS M q2  io_targets A io (initial A)  {Inr q1, Inr q2} = {}"
proof -
  have "observable A"
    using state_separator_from_canonical_separator_observable[OF assms(1,3,4,5)] by assumption

  let ?C = "canonical_separator M q1 q2"

  obtain p where "path A (initial A) p" and "p_io p = io"
    using assms(2) by force
  then have "path ?C (initial ?C) p"
    using submachine_path_initial[OF is_state_separator_from_canonical_separator_simps(1)[OF assms(1)]] by auto
  then have "io  L ?C"
    using p_io p = io by auto

  show "io  LS M q1 - LS M q2  io_targets A io (initial A) = {Inr q1}"
  proof -
    assume "io  LS M q1 - LS M q2"

    have "target (initial A) p = Inr q1"
      using submachine_path_initial[OF is_state_separator_from_canonical_separator_simps(1)[OF assms(1)] path A (initial A) p] 
            canonical_separator_language_target(1)[OF io  L ?C assms(3,4,5,6) io  LS M q1 - LS M q2] 
            p_io p = io
      unfolding io_targets.simps is_state_separator_from_canonical_separator_initial[OF assms(1,4,5)] 
                canonical_separator_simps product_simps from_FSM_simps[OF assms(4)] from_FSM_simps[OF assms(5)]
      using assms(4) assms(5) canonical_separator_initial by fastforce
    then have "Inr q1  io_targets A io (initial A)"
      using path A (initial A) p p_io p = io unfolding io_targets.simps
      by (metis (mono_tags, lifting) mem_Collect_eq)  
    then show "io_targets A io (initial A) = {Inr q1}"
      using observable_io_targets[OF observable A io  L A]
      by (metis singletonD)   
  qed

  show "io  LS M q2 - LS M q1  io_targets A io (initial A) = {Inr q2}"
  proof -
    assume "io  LS M q2 - LS M q1"

    have "target (initial A) p = Inr q2"
      using submachine_path_initial[OF is_state_separator_from_canonical_separator_simps(1)[OF assms(1)] path A (initial A) p] 
            canonical_separator_language_target(2)[OF io  L ?C assms(3,4,5,6) io  LS M q2 - LS M q1] 
            p_io p = io
      unfolding io_targets.simps is_state_separator_from_canonical_separator_initial[OF assms(1,4,5)] 
                canonical_separator_simps product_simps from_FSM_simps[OF assms(4)] from_FSM_simps[OF assms(5)]
      using assms(4) assms(5) canonical_separator_initial by fastforce
    then have "Inr q2  io_targets A io (initial A)"
      using path A (initial A) p p_io p = io unfolding io_targets.simps
      by (metis (mono_tags, lifting) mem_Collect_eq)  
    then show "io_targets A io (initial A) = {Inr q2}"
      using observable_io_targets[OF observable A io  L A]
      by (metis singletonD)   
  qed

  show "io  LS M q1  LS M q2  io_targets A io (initial A)  {Inr q1, Inr q2} = {}"
  proof -
    let ?P = "product (from_FSM M q1) (from_FSM M q2)"

    assume "io  LS M q1  LS M q2"

    have" q . q  io_targets A io (initial A)  q  {Inr q1, Inr q2}"
    proof -
      fix q assume "q  io_targets A io (initial A)"
      then obtain p where "q = target (initial A) p" and "path A (initial A) p" and "p_io p = io"
        by auto
      then have "path ?C (initial ?C) p"
        using submachine_path_initial[OF is_state_separator_from_canonical_separator_simps(1)[OF assms(1)]] by auto
      then have "isl (target (initial ?C) p)"
        using canonical_separator_path_targets_language(4)[OF _ observable M q1  states M q2  states M  q1  q2]
        using p_io p = io io  LS M q1  LS M q2 by auto
      then show "q  {Inr q1, Inr q2}"
        using q = target (initial A) p 
        unfolding is_state_separator_from_canonical_separator_initial[OF assms(1,4,5)]
        unfolding canonical_separator_simps product_simps from_FSM_simps by auto
    qed

    then show "io_targets A io (initial A)  {Inr q1, Inr q2} = {}"
      by blast
  qed
qed


lemma state_separator_language_intersections_nonempty :
  assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
  and     "observable M"
  and     "q1  states M"
  and     "q2  states M"
  and     "q1  q2"
shows " io . io  (L A  LS M q1) - LS M q2" and " io . io  (L A  LS M q2) - LS M q1"
proof -
  have "Inr q1  reachable_states A"
    using is_state_separator_from_canonical_separator_simps(6)[OF assms(1)] by assumption
  then obtain p where "path A (initial A) p" and "target (initial A) p = Inr q1"
    unfolding reachable_states_def by auto 
  then have "p_io p  LS M q1 - LS M q2"
    using canonical_separator_maximal_path_distinguishes_left[OF assms(1) _ _ assms(2,3,4,5)] by blast
  moreover have "p_io p  L A"
    using path A (initial A) p by auto
  ultimately show " io . io  (L A  LS M q1) - LS M q2" by blast

  have "Inr q2  reachable_states A"
    using is_state_separator_from_canonical_separator_simps(7)[OF assms(1)] by assumption
  then obtain p' where "path A (initial A) p'" and "target (initial A) p' = Inr q2"
    unfolding reachable_states_def by auto 
  then have "p_io p'  LS M q2 - LS M q1"
    using canonical_separator_maximal_path_distinguishes_right[OF assms(1) _ _ assms(2,3,4,5)] by blast
  moreover have "p_io p'  L A"
    using path A (initial A) p' by auto
  ultimately show " io . io  (L A  LS M q2) - LS M q1" by blast
qed


lemma state_separator_language_inclusion :
  assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
  and     "q1  states M"
  and     "q2  states M"
shows "L A  LS M q1  LS M q2"
  using canonical_separator_language[OF assms(2,3)]
  using submachine_language[OF is_state_separator_from_canonical_separator_simps(1)[OF assms(1)]] 
  unfolding from_FSM_language[OF assms(2)] from_FSM_language[OF assms(3)] by blast


lemma state_separator_from_canonical_separator_targets_left_inclusion :
  assumes "observable T" 
  and     "observable M"
  and     "t1  states T"
  and     "q1  states M"
  and     "q2  states M"
  and     "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
  and     "(inputs T) = (inputs M)"
  and     "path A (initial A) p"
  and     "p_io p  LS M q1"
  and     "q1  q2"
shows "target (initial A) p  Inr q2"
and   "target (initial A) p = Inr q1  isl (target (initial A) p)"
proof -
  let ?C = "canonical_separator M q1 q2"
  have c_path: " p . path A (initial A) p  path ?C (initial ?C) p"
    using is_state_separator_from_canonical_separator_simps(1)[OF assms(6)] submachine_path_initial by metis
  have "path ?C (initial ?C) p"
    using assms(8) c_path by auto

  show "target (initial A) p  Inr q2"
  proof 
    assume "target (initial A) p = Inr q2"
    then have "target (initial ?C) p = Inr q2"
      using is_state_separator_from_canonical_separator_simps(1)[OF assms(6)] by auto

    have "(p1. path M q1 p1  p_io p1 = p_io p)"
      using canonical_separator_path_initial(3)[OF path ?C (initial ?C) p assms(4,5,2,10) target (initial ?C) p = Inr q2] by blast
    then have "p_io p  LS M q1"
      unfolding LS.simps by force
    then show "False"
      using p_io p  LS M q1 by blast
  qed
  then have "target (initial ?C) p  Inr q2"
    using is_state_separator_from_canonical_separator_simps(1)[OF assms(6)] unfolding is_submachine.simps by simp
  then have "target (initial ?C) p = Inr q1  isl (target (initial ?C) p)"
  proof (cases p rule: rev_cases)
    case Nil
    then show ?thesis unfolding canonical_separator_simps[OF assms(4,5)] by simp
  next
    case (snoc ys y)
    then show ?thesis
      by (metis path (canonical_separator M q1 q2) (FSM.initial (canonical_separator M q1 q2)) p target (FSM.initial (canonical_separator M q1 q2)) p  Inr q2 assms(10) assms(2) assms(4) assms(5) canonical_separator_path_initial(4) isl_def)        
  qed
  then show "target (initial A) p = Inr q1  isl (target (initial A) p)"
    using is_state_separator_from_canonical_separator_simps(1)[OF assms(6)] unfolding is_submachine.simps by simp
qed


lemma state_separator_from_canonical_separator_targets_right_inclusion :
  assumes "observable T" 
  and     "observable M"
  and     "t1  states T"
  and     "q1  states M"
  and     "q2  states M"
  and     "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
  and     "(inputs T) = (inputs M)"
  and     "path A (initial A) p"
  and     "p_io p  LS M q2"
  and     "q1  q2"
shows "target (initial A) p  Inr q1"
and   "target (initial A) p = Inr q2  isl (target (initial A) p)"
proof -
  let ?C = "canonical_separator M q1 q2"
  have c_path: " p . path A (initial A) p  path ?C (initial ?C) p"
    using is_state_separator_from_canonical_separator_simps(1)[OF assms(6)] submachine_path_initial by metis
  have "path ?C (initial ?C) p"
    using assms(8) c_path by auto

  show "target (initial A) p  Inr q1"
  proof 
    assume "target (initial A) p = Inr q1"
    then have "target (initial ?C) p = Inr q1"
      using is_state_separator_from_canonical_separator_simps(1)[OF assms(6)] by auto

    have "(p1. path M q2 p1  p_io p1 = p_io p)"
      using canonical_separator_path_initial(2)[OF path ?C (initial ?C) p assms(4,5,2,10) target (initial ?C) p = Inr q1 ] by blast
    then have "p_io p  LS M q2"
      unfolding LS.simps by force
    then show "False"
      using p_io p  LS M q2 by blast
  qed

  then have "target (initial ?C) p  Inr q1"
    using is_state_separator_from_canonical_separator_simps(1)[OF assms(6)] unfolding is_submachine.simps by simp
  then have "target (initial ?C) p = Inr q2  isl (target (initial ?C) p)"
  proof (cases p rule: rev_cases)
    case Nil
    then show ?thesis unfolding canonical_separator_simps[OF assms(4,5)] by simp
  next
    case (snoc ys y)
    then show ?thesis
      by (metis path (canonical_separator M q1 q2) (FSM.initial (canonical_separator M q1 q2)) p target (FSM.initial (canonical_separator M q1 q2)) p  Inr q1 assms(10) assms(2) assms(4) assms(5) canonical_separator_path_initial(4) isl_def)
  qed
  then show "target (initial A) p = Inr q2  isl (target (initial A) p)"
    using is_state_separator_from_canonical_separator_simps(1)[OF assms(6)] unfolding is_submachine.simps by simp
qed




subsection ‹Calculating State Separators›

subsubsection ‹Sufficient Condition to Induce a State Separator›

definition state_separator_from_input_choices :: "('a,'b,'c) fsm  (('a × 'a) + 'a,'b,'c) fsm  'a  'a  ((('a × 'a) + 'a) × 'b) list  (('a × 'a) + 'a, 'b, 'c) fsm" where
  "state_separator_from_input_choices M CSep q1 q2 cs = 
    (let css  = set cs;
         cssQ = (set (map fst cs))  {Inr q1, Inr q2};
         S0   = filter_states CSep (λ q . q  cssQ);
         S1   = filter_transitions S0 (λ t . (t_source t, t_input t)  css)          
    in S1)"




lemma state_separator_from_input_choices_simps :      
  assumes "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
shows
  "initial (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = Inl (q1,q2)"
  "states (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = (set (map fst cs))  {Inr q1, Inr q2}"
  "inputs (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = inputs M"
  "outputs (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = outputs M"
  "transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = 
    {t  (transitions (canonical_separator M q1 q2)) .  q1' q2' x . (Inl (q1',q2'),x)  set cs  t_source t = Inl (q1',q2')  t_input t = x  t_target t  (set (map fst cs))  {Inr q1, Inr q2}}"
proof -
  let ?SS = "(state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
  let ?S0 = "filter_states (canonical_separator M q1 q2) (λ q . q  (set (map fst cs))  {Inr q1, Inr q2})"

  have "(λ q . q  (set (map fst cs))  {Inr q1, Inr q2}) (initial (canonical_separator M q1 q2))"
    unfolding canonical_separator_simps[OF assms(1,2)]
    using assms(4) by simp

  have "states ?S0 = (set (map fst cs))  {Inr q1, Inr q2}"
  proof -
    have " qq . qq  states ?S0  qq  (set (map fst cs))  {Inr q1, Inr q2}"
      unfolding filter_states_simps[of "(λ q . q  (set (map fst cs))  {Inr q1, Inr q2})", 
                                   OF (λ q . q  (set (map fst cs))  {Inr q1, Inr q2}) (initial (canonical_separator M q1 q2)) ]
      by fastforce
    moreover have " qq . qq  (set (map fst cs))  {Inr q1, Inr q2}  qq  states ?S0"
    proof -
      fix qq assume "qq  set (map fst cs)  {Inr q1, Inr q2}"
      then consider (a) "qq  set (map fst cs)" | (b) "qq  {Inr q1, Inr q2}"
        by blast
      then show "qq  states ?S0" proof cases
        case a
        then obtain q1' q2' where "qq = Inl (q1',q2')"
          using assms(5) by (metis old.prod.exhaust) 
        then show ?thesis 
          using a assms(3)[of qq]  
          unfolding filter_states_simps[of "(λ q . q  (set (map fst cs))  {Inr q1, Inr q2})", OF (λ q . q  (set (map fst cs))  {Inr q1, Inr q2}) (initial (canonical_separator M q1 q2)) ]
                canonical_separator_simps[OF assms(1,2)] by force
      next
        case b
        then show ?thesis using assms(3)  
          unfolding filter_states_simps[of "(λ q . q  (set (map fst cs))  {Inr q1, Inr q2})", OF (λ q . q  (set (map fst cs))  {Inr q1, Inr q2}) (initial (canonical_separator M q1 q2)) ]
                canonical_separator_simps[OF assms(1,2)] by force
      qed 
    qed
      
    ultimately show ?thesis by blast
  qed
    

  show "initial (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = Inl (q1,q2)"
       "states (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = (set (map fst cs))  {Inr q1, Inr q2}"
       "inputs (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = inputs M"
       "outputs (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = outputs M"
    unfolding canonical_separator_simps[OF assms(1,2)] 
              filter_transitions_simps 
              state_separator_from_input_choices_def 
              Let_def 
              filter_states_simps(1,3,4,5)[of "(λ q . q  (set (map fst cs))  {Inr q1, Inr q2})", OF (λ q . q  (set (map fst cs))  {Inr q1, Inr q2}) (initial (canonical_separator M q1 q2)) ] 
              states ?S0 = (set (map fst cs))  {Inr q1, Inr q2} 
    by simp+

  have alt_def_shared: "{t  {t  FSM.transitions (canonical_separator M q1 q2). t_source t  set (map fst cs)  {Inr q1, Inr q2}  t_target t  set (map fst cs)  {Inr q1, Inr q2}}. (t_source t, t_input t)  set cs}
                        = {t  FSM.transitions (canonical_separator M q1 q2).  q1' q2' x . (Inl (q1', q2'), x)set cs  t_source t = Inl (q1', q2')  t_input t = x  t_target t  set (map fst cs)  {Inr q1, Inr q2}}" 
      (is "?ts1 = ?ts2")
  proof -
    have " t . t  ?ts1  t  ?ts2"
    proof -
      fix t assume "t  ?ts1"
      then have "t  FSM.transitions (canonical_separator M q1 q2)" and "t_source t  set (map fst cs)  {Inr q1, Inr q2}" and "t_target t  set (map fst cs)  {Inr q1, Inr q2}" and "(t_source t, t_input t)  set cs"
        by blast+
      
      have "t_source t  set (map fst cs)"
        using t  FSM.transitions (canonical_separator M q1 q2) t_source t  set (map fst cs)  {Inr q1, Inr q2}
        using canonical_separator_deadlocks[OF assms(1,2)]
        by fastforce
      then obtain q1' q2' where "t_source t = Inl (q1',q2')"
        using assms(5) by (metis old.prod.exhaust) 
      then have "q1' q2' x. (Inl (q1', q2'), x)  set cs  t_source t = Inl (q1', q2')  t_input t = x"
        using (t_source t, t_input t)  set cs by auto
        
      then show "t  ?ts2"
        using t  FSM.transitions (canonical_separator M q1 q2) t_target t  set (map fst cs)  {Inr q1, Inr q2}
        by simp
    qed
    moreover have " t . t  ?ts2  t  ?ts1"
      by force
    ultimately show ?thesis by blast
  qed

  show "transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = 
    {t  (transitions (canonical_separator M q1 q2)) .  q1' q2' x . (Inl (q1',q2'),x)  set cs  t_source t = Inl (q1',q2')  t_input t = x  t_target t  (set (map fst cs))  {Inr q1, Inr q2}}"
    unfolding canonical_separator_simps(1,2,3,4)[OF assms(1,2)] 
    unfolding state_separator_from_input_choices_def Let_def
    unfolding filter_transitions_simps
    unfolding filter_states_simps[of "(λ q . q  (set (map fst cs))  {Inr q1, Inr q2})", OF (λ q . q  (set (map fst cs))  {Inr q1, Inr q2}) (initial (canonical_separator M q1 q2)) ]
    unfolding alt_def_shared by blast
qed


lemma state_separator_from_input_choices_submachine :
  assumes "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
    shows "is_submachine (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) (canonical_separator M q1 q2)"
proof -
  have "(λ q . q  (set (map fst cs))  {Inr q1, Inr q2}) (initial (canonical_separator M q1 q2))"
    unfolding canonical_separator_simps[OF assms(1,2)]
    using assms(4) by simp

  show ?thesis
    unfolding state_separator_from_input_choices_def Let_def
    using submachine_transitive[OF filter_states_submachine[of "(λ q . q  (set (map fst cs))  {Inr q1, Inr q2})", OF (λ q . q  (set (map fst cs))  {Inr q1, Inr q2}) (initial (canonical_separator M q1 q2))]
                                   filter_transitions_submachine[of "filter_states (canonical_separator M q1 q2) (λq. q  set (map fst cs)  {Inr q1, Inr q2})" "(λt. (t_source t, t_input t)  set cs)"]]
    by assumption
qed


lemma state_separator_from_input_choices_single_input :
  assumes "distinct (map fst cs)"
      and "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
    shows "single_input (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
proof -
  have " t1 t2 . t1  FSM.transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) 
          t2  FSM.transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) 
             t_source t1 = t_source t2  t_input t1 = t_input t2"
  proof -
    fix t1 t2
    assume "t1  FSM.transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
       and "t2  FSM.transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
       and "t_source t1 = t_source t2"

    obtain q1' q2' where "(Inl (q1',q2'),t_input t1)  set cs"
                     and "t_source t1 = Inl (q1',q2')"
      using t1  FSM.transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)
      using state_separator_from_input_choices_simps(5)[OF assms(2,3,4,5,6)] by fastforce

    obtain q1'' q2'' where "(Inl (q1'',q2''),t_input t2)  set cs"
                     and "t_source t2 = Inl (q1'',q2'')"
      using t2  FSM.transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)
      using state_separator_from_input_choices_simps(5)[OF assms(2,3,4,5,6)] by fastforce

    have "(Inl (q1',q2'),t_input t2)  set cs"
      using (Inl (q1'',q2''),t_input t2)  set cs t_source t1 = Inl (q1',q2') t_source t2 = Inl (q1'',q2'') t_source t1 = t_source t2 
      by simp
    then show "t_input t1 = t_input t2"
      using (Inl (q1',q2'),t_input t1)  set cs distinct (map fst cs)
      by (meson eq_key_imp_eq_value) 
  qed
  then show ?thesis
    by fastforce
qed


lemma state_separator_from_input_choices_transition_list : 
  assumes "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
      and "t  transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
    shows "(t_source t, t_input t)  set cs"
using state_separator_from_input_choices_simps(5)[OF assms(1,2,3,4,5)] assms(6) by auto


lemma state_separator_from_input_choices_transition_target :
  assumes "t  transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
      and "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
    shows "t  transitions (canonical_separator M q1 q2)  t_target t  {Inr q1, Inr q2}"
  using state_separator_from_input_choices_simps(5)[OF assms(2-6)] assms(1) by fastforce


lemma state_separator_from_input_choices_acyclic_paths' :
  assumes "distinct (map fst cs)"
      and "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
      and " i t . i < length cs 
                     t  transitions (canonical_separator M q1 q2) 
                     t_source t = (fst (cs ! i))
                     t_input  t = snd (cs ! i)
                     t_target t  ((set (map fst (take i cs)))  {Inr q1, Inr q2})"
      and "path (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) q' p"
      and "target q' p = q'"
      and "p  []"
shows "False"
proof -

  let ?S = "(state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"

  from p  [] obtain p' t' where "p = t'#p'"
    using list.exhaust by blast
  then have "path ?S q' (p@[t'])" 
    using assms(8,9) by fastforce

  define f :: "(('a × 'a + 'a) × 'b × 'c × ('a × 'a + 'a))  nat"
    where f_def: "f = (λ t . the (find_index (λ qx . (fst qx) = t_source t  snd qx = t_input t) cs))"
  
  have f_prop: " t . t  set (p@[t'])  (f t < length cs) 
                                       (λ(q, x). (q, x)) (cs ! (f t)) = (t_source t,t_input t)
                                       ( j < f t . (fst (cs ! j))  t_source t)"
  proof -
    fix t assume "t  set (p@[t'])"
    then have "t  set p" using p = t'#p' by auto
    then have "t  transitions ?S" 
      using assms(8)
      by (meson path_transitions subsetD) 
    then have "(t_source t, t_input t)  set cs"
      using state_separator_from_input_choices_transition_list[OF assms(2,3,4,5,6)]
      by blast 
    then have " qx  set cs . (λ qx . (fst qx) = t_source t  snd qx = t_input t) qx"
      by force
    then have "find_index (λ qx . (fst qx) = t_source t  snd qx = t_input t) cs  None"
      by (simp add: find_index_exhaustive) 
    then obtain i where *: "find_index (λ qx . (fst qx) = t_source t  snd qx = t_input t) cs = Some i"
      by auto

    have **: " j . j < i  (fst (cs ! j)) = t_source t  cs ! i = cs ! j"
      using assms(1)
      using nth_eq_iff_index_eq  find_index_index[OF *]
      by (metis (mono_tags, lifting) Suc_lessD length_map less_trans_Suc nth_map)

    have "f t < length cs"
      unfolding f_def using find_index_index(1)[OF *] unfolding * by simp
    moreover have "(λ(q, x). (q, x)) (cs ! (f t)) = (t_source t, t_input t)"
      unfolding f_def using find_index_index(2)[OF *]
      by (metis "*" case_prod_Pair_iden option.sel prod.collapse)
    moreover have " j < f t . (fst (cs ! j))  t_source t"
      unfolding f_def using find_index_index(3)[OF *] unfolding *  
      using assms(1) **
      by (metis (no_types, lifting) "*" qxset cs. fst qx = t_source t  snd qx = t_input t eq_key_imp_eq_value find_index_index(1) nth_mem option.sel prod.collapse)
    
    ultimately show "(f t < length cs)
                       (λ(q, x). (q, x)) (cs ! (f t)) = (t_source t,t_input t)
                       ( j < f t . (fst (cs ! j))  t_source t)" by simp
  qed

  have *: " i . Suc i < length (p@[t'])  f ((p@[t']) ! i) > f ((p@[t']) ! (Suc i))"
  proof -
    fix i assume "Suc i < length (p@[t'])"
    then have "(p@[t']) ! i  set (p@[t'])" and "(p@[t']) ! (Suc i)  set (p@[t'])"
      using Suc_lessD nth_mem by blast+
    then have "(p@[t']) ! i  transitions ?S" and "(p@[t']) ! Suc i  transitions ?S" 
      using path ?S q' (p@[t'])
      by (meson path_transitions subsetD)+
    then have "(p @ [t']) ! i  FSM.transitions (canonical_separator M q1 q2)  t_target ((p @ [t']) ! i)  {Inr q1, Inr q2}" 
      using state_separator_from_input_choices_transition_target[OF _ assms(2-6)] by blast
    
    have "f ((p@[t']) ! i) < length cs"
    and  "(λ(q, x). (q, x)) (cs ! (f ((p@[t']) ! i))) = (t_source ((p@[t']) ! i), t_input ((p@[t']) ! i))"
    and  "(j<f ((p@[t']) ! i). (fst (cs ! j))  t_source ((p@[t']) ! i))"
      using f_prop[OF (p@[t']) ! i  set (p@[t'])] by auto

    have "f ((p@[t']) ! Suc i) < length cs"
    and  "(λ(q, x). (q, x)) (cs ! (f ((p@[t']) ! Suc i))) = (t_source ((p@[t']) ! Suc i), t_input ((p@[t']) ! Suc i))"
    and  "(j<f ((p@[t']) ! Suc i). (fst (cs ! j))  t_source ((p@[t']) ! Suc i))"
      using f_prop[OF (p@[t']) ! Suc i  set (p@[t'])] by auto

    have "t_source ((p @ [t']) ! i) = (fst (cs ! f ((p @ [t']) ! i)))" and "t_input ((p @ [t']) ! i) = snd (cs ! f ((p @ [t']) ! i))"
       using f_prop[OF (p@[t']) ! i  set (p@[t'])]
       by (simp add: prod.case_eq_if)+ 

    have "t_target ((p@[t']) ! i) = t_source ((p@[t']) ! Suc i)"
      using Suc i < length (p@[t']) path ?S q' (p@[t'])
      by (simp add: path_source_target_index) 
    then have "t_target ((p@[t']) ! i)  {Inr q1, Inr q2}"
      using state_separator_from_input_choices_transition_list[OF assms(2,3,4,5,6) (p@[t']) ! Suc i  transitions ?S] assms(6) by force
    then have "t_target ((p @ [t']) ! i)  set (map fst (take (f ((p @ [t']) ! i)) cs))"
      using assms(7)[OF f ((p@[t']) ! i) < length cs _ t_source ((p @ [t']) ! i) = (fst (cs ! f ((p @ [t']) ! i))) t_input ((p @ [t']) ! i) = snd (cs ! f ((p @ [t']) ! i))] 
      using (p @ [t']) ! i  FSM.transitions (canonical_separator M q1 q2)  t_target ((p @ [t']) ! i)  {Inr q1, Inr q2} by blast
    then have "(qx'set (take (f ((p@[t']) ! i)) cs). (fst qx') = t_target ((p@[t']) ! i))" 
      by force 
    then obtain j where "(fst (cs ! j)) = t_source ((p@[t']) ! Suc i)" and "j < f ((p@[t']) ! i)" 
      unfolding t_target ((p@[t']) ! i) = t_source ((p@[t']) ! Suc i)
      by (metis (no_types, lifting) f ((p@[t']) ! i) < length cs in_set_conv_nth leD length_take min_def_raw nth_take)     
    then show "f ((p@[t']) ! i) > f ((p@[t']) ! (Suc i))"
      using (j<f ((p@[t']) ! Suc i). (fst (cs ! j))  t_source ((p@[t']) ! Suc i))
      using leI le_less_trans by blast 
  qed

  have " i j . j < i  i < length (p@[t'])  f ((p@[t']) ! j) > f ((p@[t']) ! i)"
    using list_index_fun_gt[of "p@[t']" f] * by blast
  then have "f t' < f t'"
    unfolding p = t'#p' by fastforce 
  then show "False"
    by auto
qed


lemma state_separator_from_input_choices_acyclic_paths :
  assumes "distinct (map fst cs)"
      and "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
      and " i t . i < length cs 
                     t  transitions (canonical_separator M q1 q2) 
                     t_source t = (fst (cs ! i))
                     t_input  t = snd (cs ! i)
                     t_target t  ((set (map fst (take i cs)))  {Inr q1, Inr q2})"
      and "path (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) q' p"
shows "distinct (visited_states q' p)"
proof (rule ccontr)
  assume "¬ distinct (visited_states q' p)"
  
  obtain i j where p1:"take j (drop i p)  []"
               and p2:"target (target q' (take i p)) (take j (drop i p)) = (target q' (take i p))"
               and p3:"path (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) (target q' (take i p)) (take j (drop i p))"
    using cycle_from_cyclic_path[OF assms(8) ¬ distinct (visited_states q' p)] by blast
  
  show "False"
    using state_separator_from_input_choices_acyclic_paths'[OF assms(1-7) p3 p2 p1] by blast
qed


lemma state_separator_from_input_choices_acyclic :
  assumes "distinct (map fst cs)"
      and "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
      and " i t . i < length cs 
                     t  transitions (canonical_separator M q1 q2)
                     t_source t = (fst (cs ! i))
                     t_input  t = snd (cs ! i)
                     t_target t  ((set (map fst (take i cs)))  {Inr q1, Inr q2})"
    shows "acyclic (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
  unfolding acyclic.simps using state_separator_from_input_choices_acyclic_paths[OF assms] by blast


lemma state_separator_from_input_choices_target :
  assumes " i t . i < length cs
                     t  transitions (canonical_separator M q1 q2) 
                     t_source t = (fst (cs ! i))
                     t_input  t = snd (cs ! i)
                     t_target t  ((set (map fst (take i cs)))  {Inr q1, Inr q2})"
      and "t  FSM.transitions (canonical_separator M q1 q2)"
      and " q1' q2' x . (Inl (q1', q2'), x)set cs  t_source t = Inl (q1', q2')  t_input t = x" 
    shows "t_target t  set (map fst cs)  {Inr q1, Inr q2}" 
proof -
  from assms(3) obtain q1' q2' x where "(Inl (q1', q2'), x)set cs" and "t_source t = Inl (q1', q2')" and "t_input t = x"
    by auto
  then obtain i where "i < length cs" and "t_source t = (fst (cs ! i))" and "t_input  t = snd (cs ! i)"
    by (metis fst_conv in_set_conv_nth snd_conv)
  then have "t_target t  set (map fst (take i cs))  {Inr q1, Inr q2}" using assms(1)[OF _ assms(2)] by blast
  then consider "t_target t  set (map fst (take i cs))" | "t_target t  {Inr q1, Inr q2}" by blast
  then show ?thesis proof cases
    case 1 
    then have "t_target t  set (map fst cs)" 
      by (metis in_set_takeD take_map)
    then show ?thesis by blast
  next
    case 2
    then show ?thesis by auto
  qed 
qed


lemma state_separator_from_input_choices_transitions_alt_def :
  assumes "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
      and " i t . i < length cs
                     t  transitions (canonical_separator M q1 q2) 
                     t_source t = (fst (cs ! i))
                     t_input  t = snd (cs ! i)
                     t_target t  ((set (map fst (take i cs)))  {Inr q1, Inr q2})"
  shows "transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) = 
    {t  (transitions (canonical_separator M q1 q2)) .  q1' q2' x . (Inl (q1',q2'),x)  set cs  t_source t = Inl (q1',q2')  t_input t = x}"
proof -
  have "FSM.transitions (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) =
    {t  FSM.transitions (canonical_separator M q1 q2).
      q1' q2' x . (Inl (q1', q2'), x)set cs 
        t_source t = Inl (q1', q2') 
        t_input t = x  t_target t  set (map fst cs)  {Inr q1, Inr q2}}"
    using state_separator_from_input_choices_simps(5)[OF assms(1,2,3,4,5)] by blast

  moreover have " t . t  FSM.transitions (canonical_separator M q1 q2)    q1' q2' x . (Inl (q1', q2'), x)set cs  t_source t = Inl (q1', q2')  t_input t = x  t_target t  set (map fst cs)  {Inr q1, Inr q2}"
    using state_separator_from_input_choices_target[OF assms(6)] by blast

  ultimately show ?thesis 
    by fast
qed


lemma state_separator_from_input_choices_deadlock :
  assumes "distinct (map fst cs)"
      and "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
      and " i t . i < length cs
                     t  transitions (canonical_separator M q1 q2) 
                     t_source t = (fst (cs ! i))
                     t_input  t = snd (cs ! i)
                     t_target t  ((set (map fst (take i cs)))  {Inr q1, Inr q2})"
      
    shows " qq . qq  states (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)  deadlock_state (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs) qq  qq  {Inr q1, Inr q2}  ( q1' q2' x . qq = Inl (q1',q2')  x  inputs M  (h_out M (q1',x) = {}  h_out M (q2',x) = {}))"
proof -
  let ?C = "(canonical_separator M q1 q2)"
  let ?S = "(state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
 
  fix qq assume "qq  states ?S" and "deadlock_state ?S qq"

  then consider (a) "qq  (set (map fst cs))" | (b) "qq  {Inr q1, Inr q2}"
    using state_separator_from_input_choices_simps(2)[OF assms(2,3,4,5,6)] by blast
  then show "qq  {Inr q1, Inr q2}  ( q1' q2' x . qq = Inl (q1',q2')  x  inputs M  (h_out M (q1',x) = {}  h_out M (q2',x) = {}))"
  proof cases
    case a
    then obtain q1' q2' x where "(Inl (q1',q2'),x)  set cs" and  "qq = Inl (q1',q2')" using assms(6) by fastforce
    then have "Inl (q1',q2')  states (canonical_separator M q1 q2)" and "x  inputs M" using assms(4) by blast+
    then have "(q1', q2')  states (product (from_FSM M q1) (from_FSM M q2))"
      using canonical_separator_simps(2)[OF assms(2,3)] by fastforce

    have "h_out M (q1',x) = {}  h_out M (q2',x) = {}"
    proof (rule ccontr)
      assume "¬ (h_out M (q1', x) = {}  h_out M (q2', x) = {})"
      then consider (a1) " y  (h_out M (q1', x)  h_out M (q2', x)) . True" | 
                    (a2) " y  (h_out M (q1', x) - h_out M (q2', x)) . True" |
                    (a3) " y  (h_out M (q2', x) - h_out M (q1', x)) . True"
        by blast
      then show "False" proof cases
        case a1
        then obtain y q1'' q2''  where "(y,q1'')  h M (q1',x)" and "(y,q2'')  h M (q2',x)" by auto
        then have "((q1',q2'),x,y,(q1'',q2''))  transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
          unfolding product_transitions_def h.simps using assms(2,3) by auto
        then have "(Inl (q1',q2'),x,y,Inl (q1'',q2''))  transitions ?C"  
          using (q1', q2')  states (product (from_FSM M q1) (from_FSM M q2))
                canonical_separator_transitions_def[OF assms(2,3)]  by fast
        
        then have "(Inl (q1',q2'),x,y,Inl (q1'',q2''))  {t  FSM.transitions (canonical_separator M q1 q2).
                                                             q1' q2' x . (Inl (q1', q2'), x)set cs 
                                                                t_source t = Inl (q1', q2') 
                                                                t_input t = x  t_target t  set (map fst cs)  {Inr q1, Inr q2}}"
          using state_separator_from_input_choices_target[OF assms(7) (Inl (q1',q2'),x,y,Inl (q1'',q2''))  transitions ?C]
          using (Inl (q1', q2'), x)  set cs by force 

        then have "(Inl (q1',q2'), x, y, Inl (q1'',q2''))  transitions ?S" 
          using state_separator_from_input_choices_simps(5)[OF assms(2,3,4,5,6)] by fastforce
        then show "False" 
          using deadlock_state ?S qq unfolding qq = Inl (q1',q2') by auto
      next
        case a2
        then obtain y where "y  (h_out M (q1', x) - h_out M (q2', x))" unfolding h_out.simps by blast
        then have "(q'. (q1', x, y, q')  FSM.transitions M)  (q'. (q2', x, y, q')  FSM.transitions M)" unfolding h_out.simps by blast
        then have "(Inl (q1',q2'), x, y, Inr q1)  distinguishing_transitions_left M q1 q2"
          unfolding distinguishing_transitions_left_def h.simps
          using (q1', q2')  states (product (from_FSM M q1) (from_FSM M q2)) by blast
        then have "(Inl (q1',q2'), x, y, Inr q1)  transitions ?C"
          unfolding canonical_separator_transitions_def[OF assms(2,3)] by blast
        moreover have "q1'' q2'' x' . (Inl (q1'', q2''), x')set cs  t_source (Inl (q1',q2'), x, y, Inr q1) = Inl (q1'', q2'')  t_input (Inl (q1',q2'), x, y, Inr q1) = x'"
          using (Inl (q1', q2'), x)  set cs by auto
        ultimately have "(Inl (q1',q2'), x, y, Inr q1)  transitions ?S" 
          using state_separator_from_input_choices_transitions_alt_def[OF assms(2,3,4,5,6,7)] by blast
        then show "False" 
          using deadlock_state ?S qq unfolding qq = Inl (q1',q2') by auto
      next
        case a3
        then obtain y where "y  (h_out M (q2', x) - h_out M (q1', x))" unfolding h_out.simps by blast
        then have "¬(q'. (q1', x, y, q')  FSM.transitions M)  (q'. (q2', x, y, q')  FSM.transitions M)" unfolding h_out.simps by blast
        then have "(Inl (q1',q2'), x, y, Inr q2)  distinguishing_transitions_right M q1 q2"
          unfolding distinguishing_transitions_right_def h.simps
          using (q1', q2')  states (product (from_FSM M q1) (from_FSM M q2)) by blast
        then have "(Inl (q1',q2'), x, y, Inr q2)  transitions ?C"
          unfolding canonical_separator_transitions_def[OF assms(2,3)] by blast
        moreover have "q1'' q2'' x' . (Inl (q1'', q2''), x')set cs  t_source (Inl (q1',q2'), x, y, Inr q2) = Inl (q1'', q2'')  t_input (Inl (q1',q2'), x, y, Inr q2) = x'"
          using (Inl (q1', q2'), x)  set cs by auto
        ultimately have "(Inl (q1',q2'), x, y, Inr q2)  transitions ?S" 
          using state_separator_from_input_choices_transitions_alt_def[OF assms(2,3,4,5,6,7)] by blast
        then show "False" 
          using deadlock_state ?S qq unfolding qq = Inl (q1',q2') by auto
      qed 
    qed
    then show ?thesis 
      using qq = Inl (q1', q2') x  FSM.inputs M by blast
  next
    case b
    then show ?thesis by simp
  qed
qed


lemma state_separator_from_input_choices_retains_io :
  assumes "distinct (map fst cs)"
      and "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
      and " i t . i < length cs
                     t  transitions (canonical_separator M q1 q2) 
                     t_source t = (fst (cs ! i))
                     t_input  t = snd (cs ! i)
                     t_target t  ((set (map fst (take i cs)))  {Inr q1, Inr q2})"
    shows "retains_outputs_for_states_and_inputs (canonical_separator M q1 q2) (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
  unfolding retains_outputs_for_states_and_inputs_def
  using state_separator_from_input_choices_transitions_alt_def[OF assms(2,3,4,5,6,7)] by fastforce


lemma state_separator_from_input_choices_is_state_separator :
  assumes "distinct (map fst cs)"
      and "q1  states M" 
      and "q2  states M"
      and " qq x . (qq,x)  set cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
      and "Inl (q1,q2)  set (map fst cs)"
      and " qq . qq  set (map fst cs)   q1' q2' . qq = Inl (q1',q2')"
      and " i t . i < length cs
                     t  transitions (canonical_separator M q1 q2) 
                     t_source t = (fst (cs ! i))
                     t_input  t = snd (cs ! i)
                     t_target t  ((set (map fst (take i cs)))  {Inr q1, Inr q2})"
      and "completely_specified M"
  shows "is_state_separator_from_canonical_separator
            (canonical_separator M q1 q2)
            q1
            q2
            (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
proof -
  let ?C = "(canonical_separator M q1 q2)"
  let ?S = "(state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"

  have submachine_prop:   "is_submachine ?S ?C"
    using state_separator_from_input_choices_submachine[OF assms(2,3,4,5,6)] by blast

  have single_input_prop: "single_input ?S"
    using state_separator_from_input_choices_single_input[OF assms(1,2,3,4,5,6)] by blast

  have acyclic_prop :     "acyclic ?S"
    using state_separator_from_input_choices_acyclic[OF assms(1,2,3,4,5,6,7)] by blast

  have i3:                " qq . qq  states ?S 
                                   deadlock_state ?S qq 
                                   qq  {Inr q1, Inr q2} 
                                         ( q1' q2' x . qq = Inl (q1',q2') 
                                             x  inputs M 
                                             h_out M (q1',x) = {} 
                                             h_out M (q2',x) = {})"
    using state_separator_from_input_choices_deadlock[OF assms(1,2,3,4,5,6,7)] by blast

  have i4:                "retains_outputs_for_states_and_inputs (canonical_separator M q1 q2) (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)"
    using state_separator_from_input_choices_retains_io[OF assms(1,2,3,4,5,6,7)] by blast



  have deadlock_prop_1: "deadlock_state ?S (Inr q1)"
    using submachine_deadlock[OF is_submachine ?S ?C canonical_separator_deadlock(1)[OF assms(2,3)]] by assumption

  have deadlock_prop_2: "deadlock_state ?S (Inr q2)"
    using submachine_deadlock[OF is_submachine ?S ?C canonical_separator_deadlock(2)[OF assms(2,3)]] by assumption

  have non_deadlock_prop': " qq . qq  states ?S  qq  Inr q1  qq  Inr q2  (isl qq  ¬ deadlock_state ?S qq)"
  proof -
    fix qq assume "qq  states ?S" and "qq  Inr q1" and "qq  Inr q2"
    then have "qq  set (map fst cs)"
      using state_separator_from_input_choices_simps(2)[OF assms(2,3,4,5,6)] by blast
    then obtain q1' q2' x where "qq = Inl (q1',q2')" and "(Inl (q1',q2'),x)  set cs"
      using assms(6) by fastforce
    then have "(Inl (q1',q2'))  states (canonical_separator M q1 q2)" and "x  inputs M"
      using assms(4) by blast+
    then have "(q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))"
      using canonical_separator_simps(2)[OF assms(2,3)] by fastforce
    then have "(q1',q2')  states (product (from_FSM M q1) (from_FSM M q2))"
      using reachable_state_is_state by fastforce
    then have "q1'  states M" and "q2'  states M"
      using assms(2,3) by auto

    obtain y q1'' where "(y,q1'')  h M (q1',x)"
      using completely_specified M q1'  states M x  inputs M
      unfolding completely_specified.simps h.simps by fastforce 

    consider (a) "y  h_out M (q2',x)" | (b) "y  h_out M (q2',x)" by blast
    then have "¬ deadlock_state ?S (Inl (q1',q2'))"
    proof cases
      case a 
      then obtain q2'' where "(y,q2'')  h M (q2',x)" by auto
      then have "((q1',q2'),x,y,(q1'',q2''))  transitions (product (from_FSM M q1) (from_FSM M q2))"
        using assms(2,3) (y,q1'')  h M (q1',x)
        unfolding h.simps product_transitions_def by fastforce
      then have "(Inl (q1',q2'),x,y,Inl (q1'',q2''))  transitions ?C"
        using canonical_separator_transitions_def[OF assms(2,3)]
        using (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2)) by fast
      then have "(Inl (q1',q2'),x,y,Inl (q1'',q2''))  transitions ?S"
        using state_separator_from_input_choices_transitions_alt_def[OF assms(2,3,4,5,6,7)] 
              (Inl (q1',q2'),x)  set cs by fastforce
      then show ?thesis 
        unfolding deadlock_state.simps by fastforce
    next
      case b
      then have "(Inl (q1',q2'),x,y,Inr q1)  distinguishing_transitions_left M q1 q2"
        using (y,q1'')  h M (q1',x) (q1',q2')  states (product (from_FSM M q1) (from_FSM M q2)) 
        unfolding h_simps h_out.simps distinguishing_transitions_left_def 
        by blast        
      then have "(Inl (q1',q2'),x,y,Inr q1)  transitions ?C"
        unfolding canonical_separator_transitions_def[OF assms(2,3)] by blast
      then have "(Inl (q1',q2'),x,y,Inr q1)  transitions ?S"
        using state_separator_from_input_choices_transitions_alt_def[OF assms(2,3,4,5,6,7)] 
              (Inl (q1',q2'),x)  set cs by fastforce
      then show ?thesis 
        unfolding deadlock_state.simps by fastforce
    qed
    then show "(isl qq  ¬ deadlock_state ?S qq)"
      unfolding qq = Inl (q1',q2') by simp
  qed
  then have non_deadlock_prop: "( q  reachable_states ?S . (q  Inr q1  q  Inr q2)  (isl q  ¬ deadlock_state ?S q))"
    using reachable_state_is_state by force
    

  (* Idea for reachable-deadlock proofs:
      - get longest path from initial to some non-deadlock state
      - that state can only target deadlock states
      - by assm, both Inr q1 and Inr q2 must be reached from that state
  *)
  define ndlps where ndlps_def: "ndlps = {p . path ?S (initial ?S) p  isl (target (initial ?S) p)}"
  

  obtain qdl where "qdl  reachable_states ?S" and "deadlock_state ?S qdl"
    using acyclic_deadlock_reachable[OF acyclic ?S] by blast
  
  have "qdl = Inr q1  qdl = Inr q2"
    using non_deadlock_prop'[OF reachable_state_is_state[OF qdl  reachable_states ?S]] deadlock_state ?S qdl by fastforce
  then have "Inr q1  reachable_states ?S  Inr q2  reachable_states ?S"
    using qdl  reachable_states ?S by blast

  have "isl (target (initial ?S) [])"
    using state_separator_from_input_choices_simps(1)[OF assms(2,3,4,5,6)] by auto
  then have "[]  ndlps"
    unfolding ndlps_def by auto
  then have "ndlps  {}"
    by blast
  moreover have "finite ndlps"
    using acyclic_finite_paths_from_reachable_state[OF acyclic ?S, of "[]"] unfolding ndlps_def by fastforce
  ultimately have " p  ndlps .  p'  ndlps . length p'  length p"
    by (meson max_length_elem not_le_imp_less) 
  then obtain mndlp where "path ?S (initial ?S) mndlp"
                      and "isl (target (initial ?S) mndlp)"
                      and " p . path ?S (initial ?S) p  isl (target (initial ?S) p)  length p  length mndlp"
    unfolding ndlps_def by blast
  then have "(target (initial ?S) mndlp)  reachable_states ?S"
    unfolding reachable_states_def by auto
  then have "(target (initial ?S) mndlp)  states ?S"
    using reachable_state_is_state by auto
  then have "(target (initial ?S) mndlp)  (set (map fst cs))"
    using isl (target (initial ?S) mndlp) state_separator_from_input_choices_simps(2)[OF assms(2,3,4,5,6)] by force
  then obtain q1' q2' x where "(Inl (q1',q2'),x)  set cs"
                          and "target (initial ?S) mndlp = Inl (q1',q2')"
    using assms(6) by fastforce
  then obtain i where "i < length cs" and "(cs ! i) = (Inl (q1',q2'),x)"
    by (metis in_set_conv_nth)

  have "Inl (q1', q2')  FSM.states (canonical_separator M q1 q2)" and "x  FSM.inputs M"
    using assms(4)[OF (Inl (q1',q2'),x)  set cs] by blast+
  then have "(q1',q2')  states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
    using canonical_separator_simps(2)[OF assms(2,3)] by blast

  have "q1'  states M" and "q2'  states M"
    using canonical_separator_states[OF Inl (q1', q2')  FSM.states (canonical_separator M q1 q2) assms(2,3)]
    unfolding product_simps using assms(2,3) by simp+

  have "¬(t'FSM.transitions (canonical_separator M q1 q2). t_source t' = target (initial ?S) mndlp  t_input t' = x  isl (t_target t'))"
  proof 
    assume "t'FSM.transitions (canonical_separator M q1 q2). t_source t' = target (initial ?S) mndlp  t_input t' = x  isl (t_target t')"
    then obtain t' where "t'FSM.transitions (canonical_separator M q1 q2)"
                     and "t_source t' = target (initial ?S) mndlp"
                     and "t_input t' = x"
                     and "isl (t_target t')" 
      by blast
    then have "q1' q2' x . (Inl (q1', q2'), x)set cs  t_source t' = Inl (q1', q2')  t_input t' = x"
      using (Inl (q1',q2'),x)  set cs unfolding target (initial ?S) mndlp = Inl (q1',q2') by fast
    then have "t'  transitions ?S"
      using t'FSM.transitions (canonical_separator M q1 q2) (Inl (q1',q2'),x)  set cs
      using state_separator_from_input_choices_transitions_alt_def[OF assms(2,3,4,5,6,7)] by blast

    then have "path ?S (initial ?S) (mndlp @ [t'])"
      using path ?S (initial ?S) mndlp t_source t' = target (initial ?S) mndlp by (metis path_append_transition)
    moreover have "isl (target (initial ?S) (mndlp @[t']))"
      using isl (t_target t') by auto
    ultimately show "False"
      using  p . path ?S (initial ?S) p  isl (target (initial ?S) p)  length p  length mndlp[of "mndlp@[t']"] by auto
  qed

  then obtain y1 y2 where "(Inl (q1',q2'),x,y1,Inr q1)  transitions (canonical_separator M q1 q2)"
                      and "(Inl (q1',q2'),x,y2,Inr q2)  transitions (canonical_separator M q1 q2)"
    using canonical_separator_isl_deadlock[OF Inl (q1', q2')  FSM.states (canonical_separator M q1 q2) x  FSM.inputs M completely_specified M _ assms(2,3)]
    unfolding target (initial ?S) mndlp = Inl (q1',q2') by blast


  have "(Inl (q1',q2'), x, y1, Inr q1)  transitions ?S"
    using (Inl (q1',q2'),x)  set cs state_separator_from_input_choices_transitions_alt_def[OF assms(2,3,4,5,6,7)] (Inl (q1',q2'),x,y1,Inr q1)  transitions (canonical_separator M q1 q2) by force

  have "(Inl (q1',q2'), x, y2, Inr q2)  transitions ?S"
    using (Inl (q1',q2'),x)  set cs state_separator_from_input_choices_transitions_alt_def[OF assms(2,3,4,5,6,7)] (Inl (q1',q2'),x,y2,Inr q2)  transitions (canonical_separator M q1 q2) by force

  have "path ?S (initial ?S) (mndlp@[(Inl (q1',q2'), x, y1, Inr q1)])"
    using target (initial ?S) mndlp = Inl (q1',q2') 
    using path_append_transition[OF path ?S (initial ?S) mndlp (Inl (q1',q2'), x, y1, Inr q1)  transitions ?S] by force
  moreover have "target (initial ?S) (mndlp@[(Inl (q1',q2'), x, y1, Inr q1)]) = Inr q1"
    by auto
  ultimately have reachable_prop_1: "Inr q1  reachable_states ?S"
    using reachable_states_intro by metis

   have "path ?S (initial ?S) (mndlp@[(Inl (q1',q2'), x, y2, Inr q2)])"
    using target (initial ?S) mndlp = Inl (q1',q2') 
    using path_append_transition[OF path ?S (initial ?S) mndlp (Inl (q1',q2'), x, y2, Inr q2)  transitions ?S] by force
  moreover have "target (initial ?S) (mndlp@[(Inl (q1',q2'), x, y2, Inr q2)]) = Inr q2"
    by auto
  ultimately have reachable_prop_2: "Inr q2  reachable_states ?S"
    using reachable_states_intro by metis


  have retainment_prop : " q x t' . q  reachable_states ?S
         x  FSM.inputs ?C 
         (tFSM.transitions ?S. t_source t = q  t_input t = x) 
         t'  FSM.transitions ?C
         t_source t' = q 
         t_input t' = x 
         t'  FSM.transitions ?S"
  proof -
    fix q x t' assume "q  reachable_states ?S"
                  and "x  FSM.inputs ?C"
                  and "(tFSM.transitions ?S. t_source t = q  t_input t = x)"
                  and "t'  FSM.transitions ?C"
                  and "t_source t' = q" 
                  and "t_input t' = x" 

    obtain t where "t  FSM.transitions ?S" and "t_source t = q" and "t_input t = x"
      using (tFSM.transitions ?S. t_source t = q  t_input t = x) by blast
    then have "t_source t = t_source t'  t_input t = t_input t'"
      using t_source t' = q t_input t' = x by auto

    
    show "t'  FSM.transitions ?S"
      using i4 unfolding retains_outputs_for_states_and_inputs_def
      using t  FSM.transitions ?S t'  FSM.transitions ?C t_source t = t_source t'  t_input t = t_input t' 
      by blast
  qed
    
  show ?thesis unfolding is_state_separator_from_canonical_separator_def
    using submachine_prop
          single_input_prop
          acyclic_prop
          deadlock_prop_1
          deadlock_prop_2
          reachable_prop_1
          reachable_prop_2
          non_deadlock_prop
          retainment_prop by blast 
qed
    
    

subsubsection ‹Calculating a State Separator by Backwards Reachability Analysis›

text ‹A state separator for states @{text "q1"} and @{text "q2"} can be calculated using backwards 
      reachability analysis starting from the two deadlock states of their canonical separator until
      @{text "Inl (q1.q2)"} is reached or it is not possible to reach @{text "(q1,q2)"}.›

definition s_states :: "('a::linorder,'b::linorder,'c) fsm  'a  'a  ((('a × 'a) + 'a) × 'b) list" where
  "s_states M q1 q2 = (let C = canonical_separator M q1 q2
   in select_inputs (h C) (initial C) (inputs_as_list C) (remove1 (Inl (q1,q2)) (remove1 (Inr q1) (remove1 (Inr q2) (states_as_list C)))) {Inr q1, Inr q2} [])"


definition state_separator_from_s_states :: "('a::linorder,'b::linorder,'c) fsm  'a  'a  (('a × 'a) + 'a, 'b, 'c) fsm option" 
  where
  "state_separator_from_s_states M q1 q2 = 
    (let cs = s_states M q1 q2 
      in (case length cs of
            0  None |
            _  if fst (last cs) = Inl (q1,q2)
                  then Some (state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 cs)
                  else None))"


lemma state_separator_from_s_states_code[code] :
  "state_separator_from_s_states M q1 q2 =
    (let C = canonical_separator M q1 q2;
         cs = select_inputs (h C) (initial C) (inputs_as_list C) (remove1 (Inl (q1,q2)) (remove1 (Inr q1) (remove1 (Inr q2) (states_as_list C)))) {Inr q1, Inr q2} []
      in (case length cs of
            0  None |
            _  if fst (last cs) = Inl (q1,q2)
                  then Some (state_separator_from_input_choices M C q1 q2 cs) 
                  else None))"
  unfolding s_states_def state_separator_from_s_states_def Let_def by simp


lemma s_states_properties : 
  assumes "q1  states M" and "q2  states M" 
  shows "distinct (map fst (s_states M q1 q2))"
    and " qq x . (qq,x)  set (s_states M q1 q2)  qq  states (canonical_separator M q1 q2)  x  inputs M"
    and " qq . qq  set (map fst (s_states M q1 q2))   q1' q2' . qq = Inl (q1',q2')"
    and " i t . i < length (s_states M q1 q2)
                   t  transitions (canonical_separator M q1 q2) 
                   t_source t = (fst ((s_states M q1 q2) ! i))
                   t_input  t = snd ((s_states M q1 q2) ! i)
                   t_target t  ((set (map fst (take i (s_states M q1 q2))))  {Inr q1, Inr q2})"
proof -
  let ?C = "canonical_separator M q1 q2"
  let ?nS = "{Inr q1, Inr q2}"
  let ?nL = "(remove1 (Inl (q1,q2)) (remove1 (Inr q1) (remove1 (Inr q2) (states_as_list ?C))))"
  let ?iL = "(inputs_as_list ?C)"
  let ?q0 = "(initial ?C)"
  let ?f  = "(h ?C)"
  let ?k  = "(size (canonical_separator M q1 q2))"

  let ?cs = "(s_states M q1 q2)"
  
  (* parameter properties required by lemmata for select_inputs *)
  have pp1: "distinct (map fst [])" by auto
  have pp2: "set (map fst [])  ?nS" by auto
  have pp3: "?nS = ?nS  set (map fst [])" by auto
  have pp4: "?q0  ?nS" unfolding canonical_separator_simps[OF assms] by auto
  have pp5 :"distinct ?nL" using states_as_list_distinct by simp 
  have pp6: "?q0  set ?nL" unfolding canonical_separator_simps[OF assms] by auto
  have pp7: "set ?nL  ?nS = {}" by auto

  (* index based properties *)

  have " i . length []  i" by auto

  have ip1: " i . i < length ?cs  fst (?cs ! i)  (insert ?q0 (set ?nL))" 
  and  ip2: " i . i < length ?cs  fst (?cs ! i)  ?nS0"
  and  ip3: " i . i < length ?cs  snd (?cs ! i)  set ?iL"
  and  ip4: " i . i < length ?cs  ( qx'  set (take i ?cs) . fst (?cs ! i)  fst qx')"
    using select_inputs_index_properties[OF _  i . length []  i pp1 pp3 pp4 pp5 pp6 pp7]
    unfolding s_states_def Let_def by blast+
  have ip5: " i . i < length ?cs  ( t  transitions ?C . t_source t = fst (?cs ! i)  t_input t = snd (?cs ! i))"
    using select_inputs_index_properties(5)[OF _  i . length []  i pp1 pp3 pp4 pp5 pp6 pp7]
    unfolding s_states_def Let_def by blast
  have ip6: " i t . i < length ?cs  t  transitions ?C  t_source t = fst (?cs ! i)  t_input t = snd (?cs ! i)  (t_target t  ?nS0  ( qx'  set (take i ?cs) . fst qx' = (t_target t)))"
    using select_inputs_index_properties(6)[OF _  i . length []  i pp1 pp3 pp4 pp5 pp6 pp7]
    unfolding s_states_def Let_def by blast


  show "distinct (map fst ?cs)" 
    using select_inputs_distinct[OF pp1 pp2 pp4 pp5 pp6 pp7]
    unfolding s_states_def Let_def by blast

  show " qq x . (qq,x)  set ?cs  qq  states (canonical_separator M q1 q2)  x  inputs M"
  proof -
    fix qq x assume "(qq,x)  set ?cs"
    then obtain i where "i < length ?cs" and "?cs ! i = (qq,x)"
      by (meson in_set_conv_nth) 
    show "qq  states (canonical_separator M q1 q2)  x  inputs M"
      using ip1[OF i < length ?cs] ip3[OF i < length ?cs] 
            states_as_list_set[of ?C] inputs_as_list_set[of ?C]
      unfolding ?cs ! i = (qq,x) fst_conv snd_conv canonical_separator_simps(3)[OF assms]
      by auto 
  qed

  show " qq . qq  set (map fst ?cs)   q1' q2' . qq = Inl (q1',q2')"
  proof -
    fix qq assume "qq  set (map fst ?cs)"
    then obtain i where "i < length ?cs" and "fst (?cs ! i) = qq"
      by (metis (no_types, lifting) in_set_conv_nth length_map nth_map)
    show " q1' q2' . qq = Inl (q1',q2')"
      using ip1[OF i < length ?cs] states_as_list_set[of ?C]
      unfolding fst (?cs ! i) = qq canonical_separator_simps[OF assms]
      by auto 
  qed

  show " i t . i < length ?cs
                   t  transitions (canonical_separator M q1 q2) 
                   t_source t = (fst (?cs ! i))
                   t_input  t = snd (?cs ! i)
                   t_target t  ((set (map fst (take i ?cs)))  {Inr q1, Inr q2})"
  proof -
    fix i t assume "i < length ?cs"
               and "t  transitions ?C"
               and "t_source t = (fst (?cs ! i))"
               and "t_input  t = snd (?cs ! i)"

    show "t_target t  ((set (map fst (take i ?cs)))  {Inr q1, Inr q2})"
      using ip6[OF i < length ?cs t  transitions ?C t_source t = (fst (?cs ! i)) t_input  t = snd (?cs ! i)] 
      by (metis Un_iff in_set_conv_nth length_map nth_map)
  qed
qed

     
lemma state_separator_from_s_states_soundness :
  assumes "state_separator_from_s_states M q1 q2 = Some A"
      and "q1  states M" and "q2  states M" and "completely_specified M"
  shows "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
proof -
  let ?cs = "s_states M q1 q2"

  have "length (s_states M q1 q2)  0  fst (last (s_states M q1 q2)) = Inl (q1,q2)"
  and  "A = state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 ?cs"
    using assms(1) unfolding state_separator_from_s_states_def Let_def
    by (cases "length (s_states M q1 q2)"; cases "fst (last (s_states M q1 q2)) = Inl (q1,q2)"; auto)+
  then have "Inl (q1,q2)  set (map fst ?cs)"
    by (metis last_in_set length_0_conv map_set)
     

  show ?thesis 
    using state_separator_from_input_choices_is_state_separator[
        OF _ assms(2,3) _ Inl (q1,q2)  set (map fst ?cs),
        OF s_states_properties[OF assms(2,3)] assms(4)] 
    unfolding A = state_separator_from_input_choices M (canonical_separator M q1 q2) q1 q2 ?cs[symmetric] by blast
qed
  

lemma state_separator_from_s_states_exhaustiveness :
  assumes " S . is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 S"
      and "q1  states M" and "q2  states M" and "completely_specified M" and "observable M"
  shows "state_separator_from_s_states M q1 q2  None"
proof -
  let ?CSep = "(canonical_separator M q1 q2)"

  obtain S where S_def: "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 S"
    using assms(1) by blast

  then have "is_submachine S ?CSep" 
       and  "single_input S"
       and  "acyclic S"
        and  *:" q . q  reachable_states S  q  Inr q1  q  Inr q2  (isl q  ¬ deadlock_state S q)"
       and  **:" q x t . q  reachable_states S  x  (inputs ?CSep)  ( t  transitions S . t_source t = q  t_input t = x)  t  transitions ?CSep  t_source t = q  t_input t = x  t  transitions S"
    using assms unfolding is_state_separator_from_canonical_separator_def by blast+

  have p1: "(q x. q  reachable_states S  h S (q, x)  {}  h S (q, x) = h ?CSep (q, x))"
  proof - 
    fix q x assume "q  reachable_states S" and "h S (q, x)  {}"

    then have "x  inputs ?CSep"
      using is_submachine S ?CSep fsm_transition_input by force
    have "( t  transitions S . t_source t = q  t_input t = x)"
      using h S (q, x)  {} by fastforce

    have " y q'' . (y,q'')  h S (q,x)  (y,q'')  h ?CSep (q,x)" 
      using is_submachine S ?CSep by force 
    moreover have " y q'' . (y,q'')  h ?CSep (q,x)  (y,q'')  h S (q,x)" 
      using **[OF q  reachable_states S x  inputs ?CSep ( t  transitions S . t_source t = q  t_input t = x)]
      unfolding h.simps by force
    ultimately show "h S (q, x) = h ?CSep (q, x)" 
      by force
  qed 

  have p2: "q'. q'  reachable_states S  deadlock_state S q'  q'  {Inr q1, Inr q2}  set (map fst [])"
    using * by fast

  have "initial S = Inl (q1,q2)"
    using is_state_separator_from_canonical_separator_initial[OF S_def assms(2,3)] by assumption
 
  have ***: "(set (remove1 (Inl (q1, q2)) (remove1 (Inr q1) (remove1 (Inr q2) (states_as_list ?CSep))))  {Inr q1, Inr q2}  set (map fst [])) = (states ?CSep - {Inl (q1,q2)})"
    using states_as_list_set[of ?CSep] states_as_list_distinct[of ?CSep] 
    unfolding 
              initial S = Inl (q1,q2) 
              canonical_separator_simps(2)[OF assms(2,3)]
    by auto 

  have "Inl (q1,q2)  reachable_states ?CSep"
    using reachable_states_initial[of S] unfolding initial S = Inl (q1,q2)
    using  submachine_reachable_subset[OF is_submachine S ?CSep] by blast
  then have p3: "states ?CSep = insert (FSM.initial S) (set (remove1 (Inl (q1,q2)) (remove1 (Inr q1) (remove1 (Inr q2) (states_as_list ?CSep))))  {Inr q1, Inr q2}  set (map fst []))"
    unfolding *** initial S = Inl (q1,q2)
    using reachable_state_is_state by fastforce
   
  have p4: "initial S  (set (remove1 (Inl (q1,q2)) (remove1 (Inr q1) (remove1 (Inr q2) (states_as_list ?CSep))))  {Inr q1, Inr q2}  set (map fst []))"
    using FSM.initial S = Inl (q1, q2) by auto 

  have "fst (last (s_states M q1 q2)) = Inl (q1,q2)" and "length (s_states M q1 q2) > 0"
    using select_inputs_from_submachine[OF single_input S acyclic S is_submachine S ?CSep p1 p2 p3 p4]
    unfolding s_states_def submachine_simps[OF is_submachine S ?CSep] Let_def canonical_separator_simps(1)[OF assms(2,3)]
    by auto 

  obtain k where"length (s_states M q1 q2) = Suc k" 
    using length (s_states M q1 q2) > 0 gr0_conv_Suc by blast 
  have "(fst (last (s_states M q1 q2)) = Inl (q1,q2)) = True"
    using fst (last (s_states M q1 q2)) = Inl (q1,q2) by simp

  show ?thesis                            
    unfolding state_separator_from_s_states_def Let_def length (s_states M q1 q2) = Suc k fst (last (s_states M q1 q2)) = Inl (q1,q2)
    by auto
qed



subsection ‹Generalizing State Separators›

text ‹State separators can be defined without reverence to the canonical separator:›

definition is_separator :: "('a,'b,'c) fsm  'a  'a  ('d,'b,'c) fsm  'd  'd  bool" where
  "is_separator M q1 q2 A t1 t2 = 
    (single_input A
      acyclic A
      observable A
      deadlock_state A t1 
      deadlock_state A t2
      t1  reachable_states A
      t2  reachable_states A
      ( t  reachable_states A . (t  t1  t  t2)  ¬ deadlock_state A t)
      ( io  L A . ( x yq yt . (io@[(x,yq)]  LS M q1  io@[(x,yt)]  L A)  (io@[(x,yq)]  L A))
                    ( x yq2 yt . (io@[(x,yq2)]  LS M q2  io@[(x,yt)]  L A)  (io@[(x,yq2)]  L A)))
      ( p . (path A (initial A) p  target (initial A) p = t1)  p_io p  LS M q1 - LS M q2)
      ( p . (path A (initial A) p  target (initial A) p = t2)  p_io p  LS M q2 - LS M q1)
      ( p . (path A (initial A) p  target (initial A) p  t1  target (initial A) p  t2)  p_io p  LS M q1  LS M q2)
      q1  q2
      t1  t2
      (inputs A)  (inputs M))"


lemma is_separator_simps :
  assumes "is_separator M q1 q2 A t1 t2"
shows "single_input A"
  and "acyclic A"
  and "observable A"
  and "deadlock_state A t1"
  and "deadlock_state A t2"
  and "t1  reachable_states A"
  and "t2  reachable_states A"
  and " t . t  reachable_states A  t  t1  t  t2  ¬ deadlock_state A t"
  and " io x yq yt . io@[(x,yq)]  LS M q1  io@[(x,yt)]  L A  (io@[(x,yq)]  L A)"
  and " io x yq yt . io@[(x,yq)]  LS M q2  io@[(x,yt)]  L A  (io@[(x,yq)]  L A)"
  and " p . path A (initial A) p  target (initial A) p = t1  p_io p  LS M q1 - LS M q2"
  and " p . path A (initial A) p  target (initial A) p = t2  p_io p  LS M q2 - LS M q1"
  and " p . path A (initial A) p  target (initial A) p  t1  target (initial A) p  t2  p_io p  LS M q1  LS M q2"
  and "q1  q2"
  and "t1  t2"
  and "(inputs A)  (inputs M)"
proof -
  have p01: "single_input A"
  and  p02: "acyclic A"
  and  p03: "observable A"
  and  p04: "deadlock_state A t1" 
  and  p05: "deadlock_state A t2"
  and  p06: "t1  reachable_states A"
  and  p07: "t2  reachable_states A"
  and  p08: "( t  reachable_states A . (t  t1  t  t2)  ¬ deadlock_state A t)"
  and  p09: "( io  L A . ( x yq yt . (io@[(x,yq)]  LS M q1  io@[(x,yt)]  L A)  (io@[(x,yq)]  L A))
                          ( x yq2 yt . (io@[(x,yq2)]  LS M q2  io@[(x,yt)]  L A)  (io@[(x,yq2)]  L A)))"
  and  p10: "( p . (path A (initial A) p  target (initial A) p = t1)  p_io p  LS M q1 - LS M q2)"
  and  p11: "( p . (path A (initial A) p  target (initial A) p = t2)  p_io p  LS M q2 - LS M q1)"
  and  p12: "( p . (path A (initial A) p  target (initial A) p  t1  target (initial A) p  t2)  p_io p  LS M q1  LS M q2)"
  and  p13: "q1  q2"
  and  p14: "t1  t2"
  and  p15: "(inputs A)  (inputs M)"
    using assms unfolding is_separator_def by presburger+

  show "single_input A" using p01 by assumption
  show "acyclic A" using p02 by assumption
  show "observable A" using p03 by assumption
  show "deadlock_state A t1" using p04 by assumption
  show "deadlock_state A t2" using p05 by assumption
  show "t1  reachable_states A" using p06 by assumption
  show "t2  reachable_states A" using p07 by assumption
  show " io x yq yt . io@[(x,yq)]  LS M q1  io@[(x,yt)]  L A  (io@[(x,yq)]  L A)" using p09 language_prefix[of _ _ A "initial A"] by blast
  show " io x yq yt . io@[(x,yq)]  LS M q2  io@[(x,yt)]  L A  (io@[(x,yq)]  L A)" using p09 language_prefix[of _ _ A "initial A"] by blast
  show " t . t  reachable_states A  t  t1  t  t2  ¬ deadlock_state A t" using p08 by blast
  show " p . path A (initial A) p  target (initial A) p = t1  p_io p  LS M q1 - LS M q2" using p10 by blast
  show " p . path A (initial A) p  target (initial A) p = t2  p_io p  LS M q2 - LS M q1" using p11 by blast
  show " p . path A (initial A) p  target (initial A) p  t1  target (initial A) p  t2  p_io p  LS M q1  LS M q2" using p12 by blast
  show "q1  q2" using p13 by assumption
  show "t1  t2" using p14 by assumption
  show "(inputs A)  (inputs M)" using p15 by assumption
qed


lemma separator_initial :
  assumes "is_separator M q1 q2 A t1 t2"
shows "initial A  t1"
and   "initial A  t2"
proof -
  show "initial A  t1"
  proof 
    assume "initial A = t1"
    then have "deadlock_state A (initial A)"
      using is_separator_simps(4)[OF assms] by auto
    then have "reachable_states A = {initial A}" 
      using states_initial_deadlock by blast
    then show "False"
      using is_separator_simps(7,15)[OF assms] initial A = t1 by auto
  qed

  show "initial A  t2"
  proof 
    assume "initial A = t2"
    then have "deadlock_state A (initial A)"
      using is_separator_simps(5)[OF assms] by auto
    then have "reachable_states A = {initial A}" 
      using states_initial_deadlock by blast
    then show "False"
      using is_separator_simps(6,15)[OF assms] initial A = t2 by auto
  qed
qed


lemma separator_path_targets :
  assumes "is_separator M q1 q2 A t1 t2"
  and     "path A (initial A) p"
shows "p_io p  LS M q1 - LS M q2  target (initial A) p = t1"
and   "p_io p  LS M q2 - LS M q1  target (initial A) p = t2"
and   "p_io p  LS M q1  LS M q2  (target (initial A) p  t1  target (initial A) p  t2)"
and   "p_io p  LS M q1  LS M q2"
proof -
  have pt1: " p . path A (initial A) p  target (initial A) p = t1  p_io p  LS M q1 - LS M q2" 
  and  pt2: " p . path A (initial A) p  target (initial A) p = t2  p_io p  LS M q2 - LS M q1" 
  and  pt3: " p . path A (initial A) p  target (initial A) p  t1  target (initial A) p  t2  p_io p  LS M q1  LS M q2" 
  and  "t1  t2"
  and  "observable A"
    using is_separator_simps[OF assms(1)] by blast+

  show "p_io p  LS M q1 - LS M q2  target (initial A) p = t1"
    using pt1[OF path A (initial A) p] pt2[OF path A (initial A) p] pt3[OF path A (initial A) p] t1  t2 by blast
  show "p_io p  LS M q2 - LS M q1  target (initial A) p = t2"
    using pt1[OF path A (initial A) p] pt2[OF path A (initial A) p] pt3[OF path A (initial A) p] t1  t2 by blast
  show "p_io p  LS M q1  LS M q2  (target (initial A) p  t1  target (initial A) p  t2)"
    using pt1[OF path A (initial A) p] pt2[OF path A (initial A) p] pt3[OF path A (initial A) p] t1  t2 by blast
  show "p_io p  LS M q1  LS M q2"
    using pt1[OF path A (initial A) p] pt2[OF path A (initial A) p] pt3[OF path A (initial A) p] t1  t2 by blast
qed


lemma separator_language :
  assumes "is_separator M q1 q2 A t1 t2"
  and     "io  L A"
shows "io  LS M q1 - LS M q2  io_targets A io (initial A) = {t1}"
and   "io  LS M q2 - LS M q1  io_targets A io (initial A) = {t2}"
and   "io  LS M q1  LS M q2  io_targets A io (initial A)  {t1,t2} = {}"
and   "io  LS M q1  LS M q2"
proof -

  obtain p where "path A (initial A) p" and "p_io p = io"
    using io  L A  by auto

  have pt1: " p . path A (initial A) p  target (initial A) p = t1  p_io p  LS M q1 - LS M q2" 
  and  pt2: " p . path A (initial A) p  target (initial A) p = t2  p_io p  LS M q2 - LS M q1" 
  and  pt3: " p . path A (initial A) p  target (initial A) p  t1  target (initial A) p  t2  p_io p  LS M q1  LS M q2" 
  and  "t1  t2"
  and  "observable A"
    using is_separator_simps[OF assms(1)] by blast+


  show "io  LS M q1 - LS M q2  io_targets A io (initial A) = {t1}"
  proof -
    assume "io  LS M q1 - LS M q2"
    
    then have "p_io p  LS M q1 - LS M q2"
      using p_io p = io by auto
    then have "target (initial A) p = t1"
      using pt1[OF path A (initial A) p] pt2[OF path A (initial A) p] pt3[OF path A (initial A) p] t1  t2
      by blast 
    then have "t1  io_targets A io (initial A)"
      using path A (initial A) p p_io p = io unfolding io_targets.simps by force
    then show "io_targets A io (initial A) = {t1}"
      using observable_io_targets[OF observable A]
      by (metis io  L A singletonD) 
  qed

  show "io  LS M q2 - LS M q1  io_targets A io (initial A) = {t2}"
  proof -
    assume "io  LS M q2 - LS M q1"
    
    then have "p_io p  LS M q2 - LS M q1"
      using p_io p = io by auto
    then have "target (initial A) p = t2"
      using pt1[OF path A (initial A) p] pt2[OF path A (initial A) p] pt3[OF path A (initial A) p] t1  t2
      by blast 
    then have "t2  io_targets A io (initial A)"
      using path A (initial A) p p_io p = io unfolding io_targets.simps by force
    then show "io_targets A io (initial A) = {t2}"
      using observable_io_targets[OF observable A]
      by (metis io  L A singletonD) 
  qed

  show "io  LS M q1  LS M q2  io_targets A io (initial A)  {t1,t2} = {}"
  proof -
    assume "io  LS M q1  LS M q2"
    
    then have "p_io p  LS M q1  LS M q2"
      using p_io p = io by auto
    then have "target (initial A) p  t1" and "target (initial A) p  t2"
      using pt1[OF path A (initial A) p] pt2[OF path A (initial A) p] pt3[OF path A (initial A) p] t1  t2
      by blast+ 
    moreover have "target (initial A) p  io_targets A io (initial A)"
      using path A (initial A) p p_io p = io unfolding io_targets.simps by force
    ultimately show "io_targets A io (initial A)  {t1,t2} = {}"
      using observable_io_targets[OF observable A io  L A]
      by (metis (no_types, opaque_lifting) inf_bot_left insert_disjoint(2) insert_iff singletonD) 
  qed

  show "io  LS M q1  LS M q2"
    using separator_path_targets(4)[OF assms(1) path A (initial A) p] p_io p = io by auto
qed


lemma is_separator_sym :
  "is_separator M q1 q2 A t1 t2  is_separator M q2 q1 A t2 t1"
  unfolding is_separator_def Int_commute[of "LS M q2" "LS M q1"] by meson 


lemma state_separator_from_canonical_separator_is_separator :
  assumes "is_state_separator_from_canonical_separator (canonical_separator M q1 q2) q1 q2 A"
  and     "observable M" 
  and     "q1  states M"
  and     "q2  states M"
  and     "q1  q2"
shows "is_separator M q1 q2 A (Inr q1) (Inr q2)"
proof -
  let ?C = "canonical_separator M q1 q2"
  have "observable ?C"
    using canonical_separator_observable[OF assms(2,3,4)] by assumption

  have "is_submachine A ?C" 
  and   p1: "single_input A"
  and   p2: "acyclic A"
  and   p4: "deadlock_state A (Inr q1)"
  and   p5: "deadlock_state A (Inr q2)"
  and   p6: "((Inr q1)  reachable_states A)"
  and   p7: "((Inr q2)  reachable_states A)"
  and   " q . q  reachable_states A  q  Inr q1  q  Inr q2  (isl q  ¬ deadlock_state A q)"
  and   compl: " q x t . q  reachable_states A  x  (inputs M)  ( t  transitions A . t_source t = q  t_input t = x)  t  transitions ?C  t_source t = q  t_input t = x  t  transitions A"
    using is_state_separator_from_canonical_separator_simps[OF assms(1)]
    unfolding canonical_separator_simps[OF assms(3,4)]
    by blast+

  have p3: "observable A" 
    using state_separator_from_canonical_separator_observable[OF assms(1-4)] by assumption

  have p8: "(treachable_states A. t  Inr q1  t  Inr q2  ¬ deadlock_state A t)"
    using  q . q  reachable_states A  q  Inr q1  q  Inr q2  (isl q  ¬ deadlock_state A q) by simp

  have " io . io  L A  
        (io  LS M q1 - LS M q2  io_targets A io (initial A) = {Inr q1}) 
        (io  LS M q2 - LS M q1  io_targets A io (initial A) = {Inr q2}) 
        (io  LS M q1  LS M q2  io_targets A io (initial A)  {Inr q1, Inr q2} = {}) 
        (x yq yt. io @ [(x, yq)]  LS M q1  io @ [(x, yt)]  LS A (initial A)  io @ [(x, yq)]  LS A (initial A)) 
        (x yq2 yt. io @ [(x, yq2)]  LS M q2  io @ [(x, yt)]  LS A (initial A)  io @ [(x, yq2)]  LS A (initial A))"
  proof -
    fix io assume "io  L A"

    have "io  LS M q1 - LS M q2  io_targets A io (initial A) = {Inr q1}"
      using state_separator_from_canonical_separator_language_target(1)[OF assms(1) io  L A assms(2,3,4,5)] by assumption
    moreover have "io  LS M q2 - LS M q1  io_targets A io (initial A) = {Inr q2}"
      using state_separator_from_canonical_separator_language_target(2)[OF assms(1) io  L A assms(2,3,4,5)] by assumption
    moreover have "io  LS M q1  LS M q2  io_targets A io (initial A)  {Inr q1, Inr q2} = {}"
      using state_separator_from_canonical_separator_language_target(3)[OF assms(1) io  L A assms(2,3,4,5)] by assumption
    moreover have " x yq yt. io @ [(x, yq)]  LS M q1  io @ [(x, yt)]  L A  io @ [(x, yq)]  L A"
    proof -
      fix x yq yt assume "io @ [(x, yq)]  LS M q1" and "io @ [(x, yt)]  L A"

      obtain pA tA where "path A (initial A) (pA@[tA])" and "p_io (pA@[tA]) = io @ [(x, yt)]"
        using language_initial_path_append_transition[OF io @ [(x, yt)]  L A] by blast
      then have "path A (initial A) pA" and "p_io pA = io"
        by auto
      then have "path ?C (initial ?C) pA"
        using submachine_path_initial[OF is_submachine A ?C] by auto

      obtain p1 t1 where "path M q1 (p1@[t1])" and "p_io (p1@[t1]) = io @ [(x, yq)]"
        using language_path_append_transition[OF io @ [(x, yq)]  LS M q1] by blast
      then have "path M q1 p1" and "p_io p1 = io" and "t1  transitions M" and "t_input t1 = x" and "t_output t1 = yq" and "t_source t1 = target q1 p1"
        by auto

      let ?q = "target (initial A) pA"
      have "?q  states A"
        using path_target_is_state path A (initial A) (pA@[tA]) by auto
      have "?q  reachable_states A"
        using path A (initial A) pA reachable_states_intro by blast

      have "tA  transitions A" and "t_input tA = x" and "t_output tA = yt" and "t_source tA = target (initial A) pA"
        using path A (initial A) (pA@[tA]) p_io (pA@[tA]) = io @ [(x, yt)] by auto
      then have "x  (inputs M)"
        using is_submachine A ?C 
        unfolding is_submachine.simps canonical_separator_simps[OF assms(3,4)] by auto
      
      have "t(transitions A). t_source t = target (initial A) pA  t_input t = x"
        using tA  transitions A t_input tA = x t_source tA = target (initial A) pA by blast

      have "io  LS M q2"
        using submachine_language[OF is_submachine A ?C] io @ [(x, yt)]  L A 
        using canonical_separator_language_prefix[OF _ assms(3,4,2,5), of io "(x,yt)"] by blast
      then obtain p2 where "path M q2 p2" and "p_io p2 = io"
        by auto
      


      show "io @ [(x, yq)]  L A" 
      proof (cases " t2  transitions M . t_source t2 = target q2 p2  t_input t2 = x  t_output t2 = yq")
        case True
        then obtain t2 where "t2  transitions M" and "t_source t2 = target q2 p2" and "t_input t2 = x" and "t_output t2 = yq"
          by blast
        then have "path M q2 (p2@[t2])" and "p_io (p2@[t2]) = io@[(x,yq)]"
          using path_append_transition[OF path M q2 p2] p_io p2 = io by auto
        then have "io @ [(x, yq)]  LS M q2"
          unfolding LS.simps by (metis (mono_tags, lifting) mem_Collect_eq) 
        then have "io@[(x,yq)]  L ?C"
          using  canonical_separator_language_intersection[OF io @ [(x, yq)]  LS M q1 _ assms(3,4)] by blast
        
        obtain pA' tA' where "path ?C (initial ?C) (pA'@[tA'])" and "p_io (pA'@[tA']) = io@[(x,yq)]"
          using language_initial_path_append_transition[OF io @ [(x, yq)]  L ?C] by blast
        then have "path ?C (initial ?C) pA'" and "p_io pA' = io" and "tA'  transitions ?C" and "t_source tA' = target (initial ?C) pA'" and "t_input tA' = x" and "t_output tA' = yq"
          by auto

        have "pA = pA'"
          using observable_path_unique[OF observable ?C path ?C (initial ?C) pA' path ?C (initial ?C) pA]
          using p_io pA' = io p_io pA = io by auto
        then have "t_source tA' = target (initial A) pA"
          using t_source tA' = target (initial ?C) pA'
          using is_state_separator_from_canonical_separator_initial[OF assms(1,3,4)]
          using canonical_separator_initial[OF assms(3,4)] by fastforce


        have "tA'  transitions A"
          using compl[OF ?q  reachable_states A x  (inputs M) t(transitions A). t_source t = target (initial A) pA  t_input t = x tA'  transitions ?C t_source tA' = target (initial A) pA t_input tA' = x] by assumption
        then have "path A (initial A) (pA@[tA'])" 
          using path A (initial A) pA t_source tA' = target (initial A) pA using path_append_transition by metis
        moreover have "p_io (pA@[tA']) = io@[(x,yq)]"
          using t_input tA' = x t_output tA' = yq p_io pA = io by auto
        
        ultimately show ?thesis 
          using language_state_containment
          by (metis (mono_tags, lifting)) 
          
      next
        case False

        let ?P = "product (from_FSM M q1) (from_FSM M q2)"
        let ?qq = "(target q1 p1, target q2 p2)"
        let ?tA = "(Inl (target q1 p1, target q2 p2), x, yq, Inr q1)"

        have "path (from_FSM M q1) (initial (from_FSM M q1)) p1" 
          using from_FSM_path_initial[OF q1  states M] path M q1 p1 by auto
        have "path (from_FSM M q2) (initial (from_FSM M q2)) p2" 
          using from_FSM_path_initial[OF q2  states M] path M q2 p2 by auto
        have "p_io p1 = p_io p2"
          using p_io p1 = io p_io p2 = io by auto
        
        have "?qq  states ?P" 
          using reachable_states_intro[OF product_path_from_paths(1)[OF path (from_FSM M q1) (initial (from_FSM M q1)) p1 path (from_FSM M q2) (initial (from_FSM M q2)) p2 p_io p1 = p_io p2]]
          unfolding product_path_from_paths(2)[OF path (from_FSM M q1) (initial (from_FSM M q1)) p1 path (from_FSM M q2) (initial (from_FSM M q2)) p2 p_io p1 = p_io p2] from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)] 
          using reachable_state_is_state
          by metis
        moreover have "q'. (target q1 p1, x, yq, q')  FSM.transitions M"
          using t1  FSM.transitions M t_input t1 = x t_output t1 = yq t_source t1 = target q1 p1
          by (metis prod.collapse) 
        moreover have "¬(q'. (target q2 p2, x, yq, q')  FSM.transitions M)"
          using t1  FSM.transitions M t_input t1 = x t_output t1 = yq t_source t1 = target q1 p1 False
          by fastforce
        ultimately have "?tA  (distinguishing_transitions_left M q1 q2)"
          unfolding distinguishing_transitions_left_def 
          by blast

        then have "(Inl (target q1 p1, target q2 p2), x, yq, Inr q1)  transitions ?C"
          using canonical_separator_distinguishing_transitions_left_containment[OF _ assms(3,4)] by metis

        let ?pP = "zip_path p1 p2"
        let ?pC = "map shift_Inl ?pP"
        have "path ?P (initial ?P) ?pP" 
        and  "target (initial ?P) ?pP = (target q1 p1, target q2 p2)"
          using  product_path_from_paths[OF path (from_FSM M q1) (initial (from_FSM M q1)) p1
                                            path (from_FSM M q2) (initial (from_FSM M q2)) p2
                                            p_io p1 = p_io p2]
          using assms(3,4) by auto

        have "length p1 = length p2"
          using p_io p1 = p_io p2 map_eq_imp_length_eq by blast 
        then have "p_io ?pP = io"
          using p_io p1 = io  by (induction p1 p2 arbitrary: io rule: list_induct2; auto)
        

        have "path ?C (initial ?C) ?pC"
          using canonical_separator_path_shift[OF assms(3,4)] path ?P (initial ?P) ?pP by simp

        have "target (initial ?C) ?pC = Inl (target q1 p1, target q2 p2)"
          using path_map_target[of Inl "initial ?P" Inl id id ?pP ]
          using target (initial ?P) ?pP = (target q1 p1, target q2 p2)
          unfolding canonical_separator_simps[OF assms(3,4)] product_simps from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)]
          by fastforce
        
        have "p_io ?pC = io"
          using p_io ?pP = io by auto
        have "p_io pA = p_io ?pC"
          unfolding p_io ?pC = io
          using p_io pA = io by assumption
  
        then have "?pC = pA"
          using observable_path_unique[OF observable ?C path ?C (initial ?C) pA path ?C (initial ?C) ?pC] by auto
        then have "t_source ?tA = target (initial A) pA"
          using target (initial ?C) ?pC = Inl (target q1 p1, target q2 p2)
          unfolding is_state_separator_from_canonical_separator_initial[OF assms(1,3,4)]
                    canonical_separator_simps[OF assms(3,4)] by force

        have "?tA  transitions A"
          using compl[OF ?q  reachable_states A x  (inputs M) t(transitions A). t_source t = target (initial A) pA  t_input t = x ?tA  transitions ?C t_source ?tA = target (initial A) pA ]
          unfolding snd_conv fst_conv by simp

        have *: "path A (initial A) (pA@[?tA])"
          using path_append_transition[OF path A (initial A) pA ?tA  transitions A  t_source ?tA = target (initial A) pA] by assumption

        have **: "p_io (pA@[?tA]) = io@[(x,yq)]"
          using p_io pA = io by auto

        show ?thesis 
          using language_state_containment[OF * **] by assumption
      qed
    qed

    
    moreover have " x yq yt. io @ [(x, yq)]  LS M q2  io @ [(x, yt)]  L A  io @ [(x, yq)]  L A"
    proof -
      fix x yq yt assume "io @ [(x, yq)]  LS M q2" and "io @ [(x, yt)]  L A"

      obtain pA tA where "path A (initial A) (pA@[tA])" and "p_io (pA@[tA]) = io @ [(x, yt)]"
        using language_initial_path_append_transition[OF io @ [(x, yt)]  L A] by blast
      then have "path A (initial A) pA" and "p_io pA = io"
        by auto
      then have "path ?C (initial ?C) pA"
        using submachine_path_initial[OF is_submachine A ?C] by auto

      obtain p2 t2 where "path M q2 (p2@[t2])" and "p_io (p2@[t2]) = io @ [(x, yq)]"
        using language_path_append_transition[OF io @ [(x, yq)]  LS M q2] by blast
      then have "path M q2 p2" and "p_io p2 = io" and "t2  transitions M" and "t_input t2 = x" and "t_output t2 = yq" and "t_source t2 = target q2 p2"
        by auto

      let ?q = "target (initial A) pA"
      have "?q  states A"
        using path_target_is_state path A (initial A) (pA@[tA]) by auto

      have "tA  transitions A" and "t_input tA = x" and "t_output tA = yt" and "t_source tA = target (initial A) pA"
        using path A (initial A) (pA@[tA]) p_io (pA@[tA]) = io @ [(x, yt)] by auto
      then have "x  (inputs M)"
        using is_submachine A ?C 
        unfolding is_submachine.simps canonical_separator_simps[OF assms(3,4)] by auto
      
      have "t(transitions A). t_source t = target (initial A) pA  t_input t = x"
        using tA  transitions A t_input tA = x t_source tA = target (initial A) pA by blast

      have "io  LS M q1"
        using submachine_language[OF is_submachine A ?C] io @ [(x, yt)]  L A 
        using canonical_separator_language_prefix[OF _ assms(3,4,2,5), of io "(x,yt)"] by blast
      then obtain p1 where "path M q1 p1" and "p_io p1 = io"
        by auto
      


      show "io @ [(x, yq)]  L A" 
      proof (cases " t1  transitions M . t_source t1 = target q1 p1  t_input t1 = x  t_output t1 = yq")
        case True
        then obtain t1 where "t1  transitions M" and "t_source t1 = target q1 p1" and "t_input t1 = x" and "t_output t1 = yq"
          by blast
        then have "path M q1 (p1@[t1])" and "p_io (p1@[t1]) = io@[(x,yq)]"
          using path_append_transition[OF path M q1 p1] p_io p1 = io by auto
        then have "io @ [(x, yq)]  LS M q1"
          unfolding LS.simps by (metis (mono_tags, lifting) mem_Collect_eq) 
        then have "io@[(x,yq)]  L ?C"
          using  canonical_separator_language_intersection[OF _ io @ [(x, yq)]  LS M q2 assms(3,4)] by blast
        
        obtain pA' tA' where "path ?C (initial ?C) (pA'@[tA'])" and "p_io (pA'@[tA']) = io@[(x,yq)]"
          using language_initial_path_append_transition[OF io @ [(x, yq)]  L ?C] by blast
        then have "path ?C (initial ?C) pA'" and "p_io pA' = io" and "tA'  transitions ?C" and "t_source tA' = target (initial ?C) pA'" and "t_input tA' = x" and "t_output tA' = yq"
          by auto

        have "pA = pA'"
          using observable_path_unique[OF observable ?C path ?C (initial ?C) pA' path ?C (initial ?C) pA]
          using p_io pA' = io p_io pA = io by auto
        then have "t_source tA' = target (initial A) pA"
          using t_source tA' = target (initial ?C) pA'
          using is_state_separator_from_canonical_separator_initial[OF assms(1,3,4)] 
          unfolding canonical_separator_simps[OF assms(3,4)] by auto

        have "?q  reachable_states A"
          using path A (initial A) pA reachable_states_intro by blast

        have "tA'  transitions A"
          using compl[OF ?q  reachable_states A x  (inputs M) t(transitions A). t_source t = target (initial A) pA  t_input t = x tA'  transitions ?C t_source tA' = target (initial A) pA t_input tA' = x] by assumption
        then have "path A (initial A) (pA@[tA'])" 
          using path A (initial A) pA t_source tA' = target (initial A) pA using path_append_transition by metis
        moreover have "p_io (pA@[tA']) = io@[(x,yq)]"
          using t_input tA' = x t_output tA' = yq p_io pA = io by auto
        
        ultimately show ?thesis 
          using language_state_containment
          by (metis (mono_tags, lifting)) 
          
      next
        case False

        let ?P = "product (from_FSM M q1) (from_FSM M q2)"
        let ?qq = "(target q1 p1, target q2 p2)"
        let ?tA = "(Inl (target q1 p1, target q2 p2), x, yq, Inr q2)"

        have "path (from_FSM M q1) (initial (from_FSM M q1)) p1" 
          using from_FSM_path_initial[OF q1  states M] path M q1 p1 by auto
        have "path (from_FSM M q2) (initial (from_FSM M q2)) p2" 
          using from_FSM_path_initial[OF q2  states M] path M q2 p2 by auto
        have "p_io p1 = p_io p2"
          using p_io p1 = io p_io p2 = io by auto

        have "?qq  states ?P"
          using reachable_states_intro[OF product_path_from_paths(1)[OF path (from_FSM M q1) (initial (from_FSM M q1)) p1 path (from_FSM M q2) (initial (from_FSM M q2)) p2 p_io p1 = p_io p2]]
          unfolding product_path_from_paths(2)[OF path (from_FSM M q1) (initial (from_FSM M q1)) p1 path (from_FSM M q2) (initial (from_FSM M q2)) p2 p_io p1 = p_io p2] from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)] 
          using reachable_state_is_state by metis
        moreover have "q'. (target q2 p2, x, yq, q')  FSM.transitions M"
          using t2  FSM.transitions M t_input t2 = x t_output t2 = yq t_source t2 = target q2 p2
          by (metis prod.collapse) 
        moreover have "¬(q'. (target q1 p1, x, yq, q')  FSM.transitions M)"
          using t2  FSM.transitions M t_input t2 = x t_output t2 = yq t_source t2 = target q2 p2 False
          by fastforce
        ultimately have "?tA  (distinguishing_transitions_right M q1 q2)"
          unfolding distinguishing_transitions_right_def 
          by blast

        then have "?tA  transitions ?C"
          using canonical_separator_distinguishing_transitions_right_containment[OF _ assms(3,4)] by metis

        let ?pP = "zip_path p1 p2"
        let ?pC = "map shift_Inl ?pP"
        have "path ?P (initial ?P) ?pP" 
        and  "target (initial ?P) ?pP = (target q1 p1, target q2 p2)"
          using  product_path_from_paths[OF path (from_FSM M q1) (initial (from_FSM M q1)) p1
                                            path (from_FSM M q2) (initial (from_FSM M q2)) p2
                                            p_io p1 = p_io p2]
          using assms(3,4) by auto

        have "length p1 = length p2"
          using p_io p1 = p_io p2 map_eq_imp_length_eq by blast 
        then have "p_io ?pP = io"
          using p_io p1 = io  by (induction p1 p2 arbitrary: io rule: list_induct2; auto)
        

        have "path ?C (initial ?C) ?pC"
          using canonical_separator_path_shift[OF assms(3,4)] path ?P (initial ?P) ?pP by simp

        have "target (initial ?C) ?pC = Inl (target q1 p1, target q2 p2)"
          using path_map_target[of Inl "initial ?P" Inl id id ?pP ]
          using target (initial ?P) ?pP = (target q1 p1, target q2 p2)
          unfolding canonical_separator_simps[OF assms(3,4)] product_simps from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)] by force
        
        have "p_io ?pC = io"
          using p_io ?pP = io by auto
        have "p_io pA = p_io ?pC"
          unfolding p_io ?pC = io
          using p_io pA = io by assumption
  
        then have "?pC = pA"
          using observable_path_unique[OF observable ?C path ?C (initial ?C) pA path ?C (initial ?C) ?pC] by auto
        then have "t_source ?tA = target (initial A) pA"
          using target (initial ?C) ?pC = Inl (target q1 p1, target q2 p2)
          unfolding is_state_separator_from_canonical_separator_initial[OF assms(1,3,4)]
                    canonical_separator_simps[OF assms(3,4)] by force

        have "?q  reachable_states A"
          using path A (initial A) pA reachable_states_intro by blast
        have "?tA  transitions A"
          using compl[OF ?q  reachable_states A x  (inputs M) t(transitions A). t_source t = target (initial A) pA  t_input t = x ?tA  transitions ?C t_source ?tA = target (initial A) pA ]
          unfolding snd_conv fst_conv by simp

        have *: "path A (initial A) (pA@[?tA])"
          using path_append_transition[OF path A (initial A) pA ?tA  transitions A  t_source ?tA = target (initial A) pA] by assumption

        have **: "p_io (pA@[?tA]) = io@[(x,yq)]"
          using p_io pA = io by auto

        show ?thesis 
          using language_state_containment[OF * **] by assumption
      qed
    qed


    ultimately show "(io  LS M q1 - LS M q2  io_targets A io (initial A) = {Inr q1}) 
        (io  LS M q2 - LS M q1  io_targets A io (initial A) = {Inr q2}) 
        (io  LS M q1  LS M q2  io_targets A io (initial A)  {Inr q1, Inr q2} = {}) 
        (x yq yt. io @ [(x, yq)]  LS M q1  io @ [(x, yt)]  LS A (initial A)  io @ [(x, yq)]  LS A (initial A)) 
        (x yq2 yt. io @ [(x, yq2)]  LS M q2  io @ [(x, yt)]  LS A (initial A)  io @ [(x, yq2)]  LS A (initial A))" 
      by blast 
  qed

  moreover have " p . path A (initial A) p  target (initial A) p = Inr q1  p_io p  LS M q1 - LS M q2"
    using canonical_separator_maximal_path_distinguishes_left[OF assms(1) _ _ observable M q1  states M q2  states M q1  q2] by blast
  moreover have " p . path A (initial A) p  target (initial A) p = Inr q2  p_io p  LS M q2 - LS M q1"
    using canonical_separator_maximal_path_distinguishes_right[OF assms(1) _ _ observable M q1  states M q2  states M q1  q2] by blast
  moreover have " p . path A (initial A) p  target (initial A) p  Inr q1  target (initial A) p  Inr q2  p_io p  LS M q1  LS M q2"
  proof -
    fix p assume "path A (initial A) p" and "target (initial A) p  Inr q1" and "target (initial A) p  Inr q2"

    have "path ?C (initial ?C) p"
      using submachine_path_initial[OF is_state_separator_from_canonical_separator_simps(1)[OF assms(1)] path A (initial A) p] by assumption

    have "target (initial ?C) p  Inr q1" and "target (initial ?C) p  Inr q2"
      using target (initial A) p  Inr q1 target (initial A) p  Inr q2
      unfolding is_state_separator_from_canonical_separator_initial[OF assms(1,3,4)] canonical_separator_initial[OF assms(3,4)] by blast+

    then have "isl (target (initial ?C) p)"
      using canonical_separator_path_initial(4)[OF path ?C (initial ?C) p q1  states M q2  states M observable M q1  q2]
      by auto 

    then show "p_io p  LS M q1  LS M q2"
      using path ?C (initial ?C) p canonical_separator_path_targets_language(1)[OF _ observable M q1  states M q2  states M q1  q2] 
      by auto
  qed

  moreover have "(inputs A)  (inputs M)"
    using is_submachine A ?C
    unfolding is_submachine.simps canonical_separator_simps[OF assms(3,4)] by auto

  ultimately show ?thesis
    unfolding is_separator_def
    using p1 p2 p3 p4 p5 p6 p7 p8 q1  q2
    by (meson sum.simps(2))
qed

  
lemma is_separator_separated_state_is_state :
  assumes "is_separator M q1 q2 A t1 t2"
  shows "q1  states M" and "q2  states M"
proof -
  have "initial A  t1"
    using separator_initial[OF assms(1)] by blast

  have "t1  reachable_states A"
  and  " p . path A (FSM.initial A) p  target (FSM.initial A) p = t1  p_io p  LS M q1 - LS M q2"
  and  "t2  reachable_states A"
  and  " p . path A (FSM.initial A) p  target (FSM.initial A) p = t2  p_io p  LS M q2 - LS M q1"
    using is_separator_simps[OF assms(1)] 
    by blast+

  obtain p1 where "path A (FSM.initial A) p1" and "target (FSM.initial A) p1 = t1"
    using t1  reachable_states A unfolding reachable_states_def by auto
  then have "p_io p1  LS M q1 - LS M q2"
    using  p . path A (FSM.initial A) p  target (FSM.initial A) p = t1  p_io p  LS M q1 - LS M q2 
    by blast
  then show "q1  states M" unfolding LS.simps
    using path_begin_state by fastforce 

  obtain p2 where "path A (FSM.initial A) p2" and "target (FSM.initial A) p2 = t2"
    using t2  reachable_states A unfolding reachable_states_def by auto
  then have "p_io p2  LS M q2 - LS M q1"
    using  p . path A (FSM.initial A) p  target (FSM.initial A) p = t2  p_io p  LS M q2 - LS M q1 
    by blast
  then show "q2  states M" unfolding LS.simps
    using path_begin_state by fastforce 
qed

end