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 "(∃tR∈FSM.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) "*" ‹∃qx∈set 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 
        ⟹ (∃t∈FSM.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 "(∃t∈FSM.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 ‹(∃t∈FSM.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: "(∀t∈reachable_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