Theory Pair_Framework

section ‹Pair-Framework›

text ‹This theory defines the Pair-Framework and provides completeness properties.›


theory Pair_Framework
  imports H_Framework 
begin

subsection ‹Classical H-Condition›

definition satisfies_h_condition :: "('a,'b,'c) fsm  ('a,'b,'c) state_cover_assignment  ('b ×'c) list set  nat  bool" where
  "satisfies_h_condition M V T m = (let
      Π = (V ` reachable_states M);
      n = card (reachable_states M);
      𝒳 = λ q . {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M}; 
      A = Π × Π;
      B = Π × { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q};
      C = ( q  reachable_states M .  τ  𝒳 q . { (V q) @ τ' | τ' . τ'  list.set (prefixes τ)} × {(V q)@τ}) 
    in 
      is_state_cover_assignment M V
       Π  T
       { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}  T
       ( (α,β)  A  B  C . α  L M  
                                β  L M  
                                after_initial M α  after_initial M β  
                                ( ω . α@ω  T 
                                       β@ω  T 
                                       distinguishes M (after_initial M α) (after_initial M β) ω)))"

lemma h_condition_satisfies_abstract_h_condition :
  assumes "observable M"
  and     "observable I"
  and     "minimal M"
  and     "size I  m"
  and     "m  size_r M"
  and     "inputs I = inputs M"
  and     "outputs I = outputs M"
  and     "satisfies_h_condition M V T m"
  and     "(L M  T = L I  T)"
shows "satisfies_abstract_h_condition M I V m"
proof -

  define Π where Π: "Π = (V ` reachable_states M)"
  define n where n: "n = size_r M"
  define 𝒳 where 𝒳: "𝒳 = (λ q . {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M})"
  define A where A: "A = Π × Π"
  define B where B: "B = Π × { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}"
  define C where C: "C = ( q  reachable_states M .  τ  𝒳 q . { (V q) @ τ' | τ' . τ'  list.set (prefixes τ)} × {(V q)@τ})"


  have "satisfies_h_condition M V T m = (is_state_cover_assignment M V
     Π  T
     { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}  T
     ( (α,β)  A  B  C . α  L M  
                              β  L M  
                              after_initial M α  after_initial M β  
                              ( ω . α@ω  T 
                                     β@ω  T 
                                     distinguishes M (after_initial M α) (after_initial M β) ω)))"
    unfolding satisfies_h_condition_def Let_def Π n 𝒳 A B C  
    by auto

  then have "is_state_cover_assignment M V" 
        and "Π  T" 
        and "{ (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}  T"
        and distinguishing_tests: " α β . (α,β)  A  B  C  
                            α  L M  
                            β  L M  
                            after_initial M α  after_initial M β  
                            ( ω . α@ω  T 
                                   β@ω  T 
                                   distinguishes M (after_initial M α) (after_initial M β) ω)"
    using satisfies_h_condition M V T m by blast+

  have "Π  L I" and "Π  L M"
    using Π  T Π = (V ` reachable_states M) L M  T = L I  T 
          state_cover_assignment_language[OF is_state_cover_assignment M V] by blast+

  have "( q γ . q  reachable_states M  length γ  Suc (m-size_r M)  list.set γ  inputs M × outputs M   butlast γ  LS M q   (L M  (V ` reachable_states M  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}) = L I  (V ` reachable_states M  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))  (preserves_divergence M I (V ` reachable_states M  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))) 
        satisfies_abstract_h_condition M I V m"
    unfolding satisfies_abstract_h_condition_def Let_def 
    by blast
  moreover have "( q γ . q  reachable_states M  length γ  Suc (m-size_r M)  list.set γ  inputs M × outputs M   butlast γ  LS M q   (L M  (V ` reachable_states M  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}) = L I  (V ` reachable_states M  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))  (preserves_divergence M I (V ` reachable_states M  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})))"
  proof -
    fix q γ 
    assume a1: "q  reachable_states M" 
       and a2: "length γ  Suc (m-size_r M)" 
       and a3: "list.set γ  inputs M × outputs M"
       and a4: "butlast γ  LS M q" 


    have "{V q @ ω' |ω'. ω'  list.set (prefixes γ)}  {V q}  {V q @ τ | τ. τ  𝒳 q}"
    proof 
      fix v assume "v  {V q @ ω' |ω'. ω'  list.set (prefixes γ)}"
      then obtain w where "v = V q @ w" and "w  list.set (prefixes γ)"
        by blast

      show "v  {V q}  {V q @ τ | τ. τ  𝒳 q}"
      proof (cases w rule: rev_cases)
        case Nil
        show ?thesis unfolding v = V q @ w Nil Π using a1 by auto
      next
        case (snoc w' xy)

        obtain w'' where "γ = w'@[xy]@w''"
          using w  list.set (prefixes γ) 
          unfolding prefixes_set snoc by auto

        obtain w''' x y where "γ = (w'@w''')@[(x,y)]"
        proof (cases w'' rule: rev_cases)
          case Nil
          show ?thesis 
            using that[of "[]" "fst xy" "snd xy"] 
            unfolding γ = w'@[xy]@w'' Nil by auto
        next
          case (snoc w''' xy')
          show ?thesis 
            using that[of "[xy]@w'''" "fst xy'" "snd xy'"]
            unfolding γ = w'@[xy]@w'' snoc by auto              
        qed
        then have "butlast γ = w'@w'''"
          using butlast_snoc by metis

        have "w'  LS M q"
          using a4 unfolding v = V q @ w butlast γ = w'@w''' 
          using language_prefix by metis
        moreover have "length w'  m - size_r M"
          using a2 unfolding v = V q @ w γ = (w'@w''')@[(x,y)] by auto
        moreover have "fst xy  FSM.inputs M  snd xy  FSM.outputs M"
          using a3 unfolding v = V q @ w γ = w'@[xy]@w'' by auto
        ultimately have "w'@[(fst xy, snd xy)]  𝒳 q"
          unfolding snoc 𝒳 n by blast
        then have "w  𝒳 q"
          unfolding snoc by auto
        then show ?thesis
          unfolding v = V q @ w using a1 by blast
      qed
    qed


    have "preserves_divergence M I (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})"
    proof -
      have " α β . α  L M  α  (Π  {V q @ ω' |ω'. ω'  list.set (prefixes γ)})  β  L M  β   (Π  {V q @ ω' |ω'. ω'  list.set (prefixes γ)}) 
          ¬ converge M α β  ¬ converge I α β"
      proof -
        fix α β 
        assume "α  L M"
           and "α  (Π  {V q @ ω' |ω'. ω'  list.set (prefixes γ)})"
           and "β  L M"
           and "β   (Π  {V q @ ω' |ω'. ω'  list.set (prefixes γ)})"
           and "¬ converge M α β"
        then have "after_initial M α  after_initial M β"
          by auto
        then have "α  β"
          by auto

        obtain v w where "{v,w} = {α,β}" and *:"(v  Π  w  Π)
                                                (v  Π  w  {V q @ ω' |ω'. ω'  list.set (prefixes γ)})
                                                (v  {V q @ ω' |ω'. ω'  list.set (prefixes γ)}  w  {V q @ ω' |ω'. ω'  list.set (prefixes γ)})"
          using α  (Π  {V q @ ω' |ω'. ω'  list.set (prefixes γ)})
                β  (Π  {V q @ ω' |ω'. ω'  list.set (prefixes γ)})
          by blast

        from * consider "(v  Π  w  Π)" |
                        "(v  Π  w  {V q @ ω' |ω'. ω'  list.set (prefixes γ)})" |
                        "(v  {V q @ ω' |ω'. ω'  list.set (prefixes γ)}  w  {V q @ ω' |ω'. ω'  list.set (prefixes γ)})"
          by blast
        then have "(v,w)  A  B  C  (w,v)  A  B  C"
        proof cases
          case 1
          then show ?thesis unfolding A by blast
        next
          case 2
          then show ?thesis
            using {V q @ ω' |ω'. ω'  list.set (prefixes γ)}  {V q}  {V q @ τ | τ. τ  𝒳 q} a1
            unfolding A B Π
            by blast
        next
          case 3

          then obtain io io' where "v = V q @ io" and "io  list.set (prefixes γ)"
                               and "w = V q @ io'" and "io'  list.set (prefixes γ)"
            by auto
          
          have "v  w"
            using {v,w} = {α,β} α  β by force 
          then have "length io  length io'" 
            using io  list.set (prefixes γ) io'  list.set (prefixes γ)
            unfolding v = V q @ io w = V q @ io' prefixes_set 
            by force
          
          have "io  list.set (prefixes io')  io'  list.set (prefixes io)"
            using prefixes_prefixes[OF io  list.set (prefixes γ) io'  list.set (prefixes γ)] .
          then obtain u u' where "{u,u@u'} = {io,io'}"
                             and "u  list.set (prefixes (u@u'))"
            unfolding prefixes_set by auto

          have "(u,u@u') = (io,io')  (u,u@u') = (io',io)"
            using {u,u@u'} = {io,io'}
            by (metis empty_iff insert_iff) 

          have "u  u@u'"
            using length io  length io' {u,u@u'} = {io,io'} by force
          then have "u@u'  []"
            by auto
          moreover have " w . w  []  w  list.set (prefixes γ)  w  𝒳 q"
            using {V q @ ω' |ω'. ω'  list.set (prefixes γ)}  {V q}  {V q @ τ | τ. τ  𝒳 q}
            by auto
          moreover have "u@u'  list.set (prefixes γ)"
            using (u,u@u') = (io,io')  (u,u@u') = (io',io) io  list.set (prefixes γ) io'  list.set (prefixes γ) by auto
          ultimately have "u@u'  𝒳 q"
            by blast
          then have "(V q @ u, V q @ (u@u'))  C"
            unfolding C
            using a1 u  list.set (prefixes (u@u')) by blast
          moreover have "(V q @ u, V q @ (u@u'))  {(v,w), (w,v)}"
            unfolding v = V q @ io w = V q @ io' 
            using (u,u@u') = (io,io')  (u,u@u') = (io',io) by auto
          ultimately show ?thesis
            by blast
        qed
        moreover have "(α,β) = (v,w)  (α,β) = (w,v)"
          using {v,w} = {α,β} 
          by (metis empty_iff insert_iff) 
        ultimately consider "(α,β)  A  B  C" | "(β,α)  A  B  C" 
          by blast

        then obtain ω where "α@ω  T" and "β@ω  T" and "distinguishes M (after_initial M α) (after_initial M β) ω"
          using distinguishing_tests[OF _ α  L M β  L M after_initial M α  after_initial M β]
          using distinguishing_tests[OF _ β  L M α  L M ] after_initial M α  after_initial M β
          by (metis distinguishes_sym)

        show "¬ converge I α β"
          using distinguish_diverge[OF assms(1,2) distinguishes M (after_initial M α) (after_initial M β) ω α@ω  T β@ω  T α  L M β  L M assms(9)] .
      qed
      then show ?thesis
        unfolding preserves_divergence.simps by blast
    qed

    moreover have "(L M  (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}) = L I  (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))"
    proof -
      have "L M  Π = L I  Π"
        using Π  L I Π  L M 
        by blast
      moreover have "L M  { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q} = L I  { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}"
        using { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}  T 
        using assms(9)
        by blast
      ultimately have *:"L M  (Π  { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}) = L I  (Π  { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q})"
        by blast
      have **:"(Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})  Π  { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}"
        using {V q @ ω' |ω'. ω'  list.set (prefixes γ)}  {V q}  {V q @ τ | τ. τ  𝒳 q} 
        using a1 unfolding Π by blast
      
      have scheme: " A B C D . A  C = B  C  D  C  A  D = B  D"
        by (metis (no_types, opaque_lifting) Int_absorb1 inf_assoc) 
      show ?thesis 
        using scheme[OF * **] .
    qed

    ultimately show "(L M  (V ` reachable_states M  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}) = L I  (V ` reachable_states M  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))  (preserves_divergence M I (V ` reachable_states M  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))"
      unfolding Π by blast
  qed
  ultimately show ?thesis
    by blast
qed

lemma h_condition_completeness :
  assumes "observable M"
  and     "observable I"
  and     "minimal M"
  and     "size I  m"
  and     "m  size_r M"
  and     "inputs I = inputs M"
  and     "outputs I = outputs M"
  and     "satisfies_h_condition M V T m"
shows "(L M = L I)  (L M  T = L I  T)"
proof -
  have "is_state_cover_assignment M V" using assms(8) unfolding satisfies_h_condition_def Let_def by blast
  then show ?thesis
    using h_condition_satisfies_abstract_h_condition[OF assms]
    using abstract_h_condition_completeness[OF assms(1-7)]
    by blast
qed



subsection ‹Helper Functions›

fun language_up_to_length_with_extensions :: "'a  ('a  'b  (('c×'a) list))  'b list  ('b×'c) list list  nat  ('b ×'c) list list" 
  where
  "language_up_to_length_with_extensions q hM iM ex 0 = ex" |
  "language_up_to_length_with_extensions q hM iM ex (Suc k) = 
    ex @ concat (map (λx .concat (map (λ(y,q') . (map (λp . (x,y) # p)
                                                (language_up_to_length_with_extensions q' hM iM ex k)))
                            (hM q x))) 
                iM)"

lemma language_up_to_length_with_extensions_set :
  assumes "q  states M"
  shows "List.set (language_up_to_length_with_extensions q (λ q x . sorted_list_of_set (h M (q,x))) (inputs_as_list M) ex k) 
          = {io@xy | io xy . io  LS M q  length io  k  xy  List.set ex}"
  (is "?S1 q k = ?S2 q k")
proof 
  let ?hM = "(λ q x . sorted_list_of_set (h M (q,x)))"
  let ?iM = "inputs_as_list M"

  show "?S1 q k  ?S2 q k"
  proof 
    fix io assume "io  ?S1 q k"
    then show "io  ?S2 q k"
      using assms proof (induction k arbitrary: q io)
      case 0
      then obtain xy where "io = []@xy"
                       and "xy  List.set ex"
                       and "[]  LS M q"
        by auto
      then show ?case by force
    next
      case (Suc k)     

      show ?case proof (cases "io  List.set ex")
        case True
        then have "io = []@io"
              and "io  List.set ex"
              and "[]  LS M q"
          using Suc.prems(2) by auto
        then show ?thesis by force
      next
        case False
        then obtain x where "x  List.set ?iM"
                        and *: "io  List.set (concat (map (λ(y,q') . map (λp . (x,y) # p)
                                                                           (language_up_to_length_with_extensions q' ?hM ?iM ex k))
                                                       (?hM q x)))"
          using Suc.prems(1) 
          unfolding language_up_to_length_with_extensions.simps 
          by fastforce
        
        have "x  inputs M"
          using x  List.set ?iM inputs_as_list_set by auto
  
        obtain yq' where "(yq')  List.set (?hM q x)"
                     and "io  List.set ((λ(y,q') . (map (λp . (x,y) # p)
                                                      (language_up_to_length_with_extensions q' ?hM ?iM ex k))) yq')"
          using concat_map_elem[OF *] by blast
        moreover obtain y q' where "yq' = (y,q')"
          using prod.exhaust_sel by blast
        ultimately have "(y,q')  List.set (?hM q x)"
                    and "io  List.set ((map (λp . (x,y) # p) (language_up_to_length_with_extensions q' ?hM ?iM ex k)))"
          by auto
  
        
        have "(y,q')  h M (q,x)"
          using (y,q')  List.set (?hM q x)
          by (metis empty_iff empty_set sorted_list_of_set.fold_insort_key.infinite sorted_list_of_set.set_sorted_key_list_of_set)           
        then have "q'  states M" 
              and "y  outputs M"
              and "(q,x,y,q')  transitions M"
          unfolding h_simps using fsm_transition_target fsm_transition_output by auto
  
        obtain p where "io = (x,y) # p"
                   and "p  List.set (language_up_to_length_with_extensions q' ?hM ?iM ex k)"
          using io  List.set ((map (λp . (x,y) # p) (language_up_to_length_with_extensions q' ?hM ?iM ex k)))
          by force
        then have "p  {io @ xy |io xy. io  LS M q'  length io  k  xy  list.set ex}"
          using Suc.IH[OF _ q'  states M] 
          by auto
        then obtain ioP xy where "p = ioP@xy"
                             and "ioP  LS M q'" 
                             and "length ioP  k" 
                             and "xy  list.set ex"
          by blast
  
        have "io = ((x,y)#ioP)@xy"
          using io = (x,y) # p p = ioP@xy by auto
        moreover have "((x,y)#ioP)  LS M q"
          using LS_prepend_transition[OF (q,x,y,q')  transitions M] ioP  LS M q'
          by auto
        moreover have "length ((x,y)#ioP)  Suc k"
          using length ioP  k
          by simp
        ultimately show ?thesis
          using xy  list.set ex by blast
      qed
    qed
  qed
        
  show "?S2 q k  ?S1 q k"
  proof 
    fix io' assume "io'  ?S2 q k"
    then show "io'  ?S1 q k"
      using assms proof (induction k arbitrary: q io')
      case 0
      then show ?case by auto
    next
      case (Suc k)

      then obtain io xy where "io' = io@xy"
                           and "io  LS M q" 
                           and "length io  Suc k" 
                           and "xy  list.set ex"
        by blast

      show ?case proof (cases io)
        case Nil
        then show ?thesis 
          using io  LS M q xy  list.set ex
          unfolding io' = io@xy 
          by auto
      next
        case (Cons a io'')
        
        obtain p where "path M q p" and "p_io p = io"
          using io  LS M q by auto
        then obtain t p' where "p = t#p'"
          using Cons
          by blast 

        then have "t  transitions M"
              and "t_source t = q"
              and "path M (t_target t) p'"
          using path M q p by auto

        have "a = (t_input t, t_output t)"
         and "p_io p' = io''"
          using p_io p = io Cons p = t#p' 
          by auto

        have "io''  LS M (t_target t)" 
          using p_io p' = io'' path M (t_target t) p' by auto
        moreover have "length io''  k"
          using length io  Suc k Cons by auto
        ultimately have "io''@xy  {io @ xy |io xy. io  LS M (t_target t)  length io  k  xy  list.set ex}"
          using xy  list.set ex by blast

        moreover define f where f_def: "f = (λ q . (language_up_to_length_with_extensions q ?hM ?iM ex k))"
        ultimately have "io''@xy  list.set (f (t_target t))"
          using Suc.IH[OF _ fsm_transition_target[OF t  transitions M]]
          by auto
        moreover have "(t_output t, t_target t)  list.set (?hM q (t_input t))"
        proof -
          have "(h M (q,t_input t))  image (snd  snd) (transitions M)"
            unfolding h_simps by force
          then have "finite (h M (q,t_input t))"
            using fsm_transitions_finite
            using finite_surj by blast 
          moreover have "(t_output t, t_target t)  h M (q,t_input t)"
            using t  transitions M t_source t = q 
            by auto
          ultimately show ?thesis 
            by simp
        qed
        ultimately have "a#(io''@xy)  list.set (concat (map (λ(y,q') . (map (λp . ((t_input t),y) # p)
                                                (f q')))
                            (?hM q (t_input t))))"
          unfolding a = (t_input t, t_output t) 
          by force 
        moreover have "t_input t  list.set ?iM"
          using fsm_transition_input[OF t  transitions M] inputs_as_list_set by auto
        ultimately have "a#(io''@xy)  list.set (concat (map (λx .concat (map (λ(y,q') . (map (λp . (x,y) # p)
                                                (f q')))
                            (?hM q x))) 
                ?iM))"
          by force
        then have "a#(io''@xy)  ?S1 q (Suc k)"
          unfolding language_up_to_length_with_extensions.simps
          unfolding f_def by force
        then show ?thesis
          unfolding io' = io@xy Cons by simp
      qed
    qed
  qed
qed



fun h_extensions :: "('a::linorder,'b::linorder,'c::linorder) fsm  'a  nat  ('b ×'c) list list" where
  "h_extensions M q k = (let 
    iM = inputs_as_list M;
    ex = map (λxy . [xy]) (List.product iM (outputs_as_list M));
    hM = (λ q x . sorted_list_of_set (h M (q,x)))
  in
    language_up_to_length_with_extensions q hM iM ex k)"


lemma h_extensions_set :
  assumes "q  states M"
shows "List.set (h_extensions M q k) = {io@[(x,y)] | io x y . io  LS M q  length io  k  x  inputs M  y  outputs M}"
proof -

  define ex where ex: "ex = map (λxy . [xy]) (List.product (inputs_as_list M) (outputs_as_list M))"
  then have "List.set ex = {[xy] | xy . xy  list.set (List.product (inputs_as_list M) (outputs_as_list M))}"
    by auto
  then have *: "List.set ex = {[(x,y)] | x y . x  inputs M  y  outputs M}"
    using inputs_as_list_set[of M] outputs_as_list_set[of M]
    by auto

  have "h_extensions M q k = language_up_to_length_with_extensions q (λ q x . sorted_list_of_set (h M (q,x))) (inputs_as_list M) ex k"
    unfolding ex h_extensions.simps Let_def 
    by auto
  then have "List.set (h_extensions M q k) = {io @ xy |io xy. io  LS M q  length io  k  xy  list.set ex}"
    using language_up_to_length_with_extensions_set[OF assms] 
    by auto
  then show ?thesis
    unfolding * by blast
qed



fun paths_up_to_length_with_targets :: "'a  ('a  'b  (('a,'b,'c) transition list))  'b list  nat  (('a,'b,'c) path × 'a) list" 
  where
  "paths_up_to_length_with_targets q hM iM 0 = [([],q)]" |
  "paths_up_to_length_with_targets q hM iM (Suc k) = 
    ([],q) # (concat (map (λx .concat (map (λt . (map (λ(p,q). (t # p,q))
                                                (paths_up_to_length_with_targets (t_target t) hM iM k)))
                            (hM q x))) 
                iM))"

lemma paths_up_to_length_with_targets_set :
  assumes "q  states M"
  shows "List.set (paths_up_to_length_with_targets q (λ q x . map (λ(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x)))) (inputs_as_list M) k) 
          = {(p, target q p) | p . path M q p  length p  k}"
  (is "?S1 q k = ?S2 q k")
proof 
  let ?hM = "(λ q x . map (λ(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x))))"
  let ?iM = "inputs_as_list M"

  have hM: " q x . list.set (?hM q x) = {(q,x,y,q') | y q' . (q,x,y,q')  transitions M}"
  proof -
    fix q x show "list.set (?hM q x) = {(q,x,y,q') | y q' . (q,x,y,q')  transitions M}"
    proof 
      show "list.set (?hM q x)  {(q,x,y,q') | y q' . (q,x,y,q')  transitions M}"
      proof 
        fix t assume "t  list.set (?hM q x)"
        then obtain y q' where "t = (q,x,y,q')" and "(y,q')  list.set (sorted_list_of_set (h M (q,x)))"
          by auto
        then have "(y,q')  h M (q,x)"
          by (metis empty_iff empty_set sorted_list_of_set.fold_insort_key.infinite sorted_list_of_set.set_sorted_key_list_of_set)
        then show "t  {(q,x,y,q') | y q' . (q,x,y,q')  transitions M}"
          unfolding h_simps t = (q,x,y,q') by blast
      qed

      show "{(q,x,y,q') | y q' . (q,x,y,q')  transitions M}  list.set (?hM q x)"
      proof 
        fix t assume "t  {(q,x,y,q') | y q' . (q,x,y,q')  transitions M}"
        then obtain y q' where "t = (q,x,y,q')" and "(q,x,y,q')  {(q,x,y,q') | y q' . (q,x,y,q')  transitions M}"
          by auto
        then have "(y,q')  h M (q,x)"
          by auto

        have "(h M (q,x))  image (snd  snd) (transitions M)"
          unfolding h_simps by force
        then have "finite (h M (q,x))"
          using fsm_transitions_finite
          using finite_surj by blast 
        then have "(y,q')  list.set (sorted_list_of_set (h M (q,x)))"
          using (y,q')  h M (q,x) by auto
        then show "t  list.set (?hM q x)"
          unfolding t = (q,x,y,q') by auto
      qed
    qed
  qed

  show "?S1 q k  ?S2 q k"
  proof 
    fix pq assume "pq  ?S1 q k"
    then show "pq  ?S2 q k"
    using assms proof (induction k arbitrary: q pq)
      case 0
      then show ?case by force
    next
      case (Suc k)     

      obtain p q' where "pq = (p,q')"
        by fastforce

      show ?case proof (cases p)
        case Nil
        have "q' = q"
          using Suc.prems(1) 
          unfolding pq = (p,q') Nil paths_up_to_length_with_targets.simps 
          by force
        then show ?thesis 
          unfolding pq = (p,q') Nil using Suc.prems(2) by auto
      next
        case (Cons t p')

        obtain x where "x  list.set ?iM"
                   and *:"(t#p',q')  list.set (concat (map (λt . (map (λ(p,q). (t # p,q))
                                                        (paths_up_to_length_with_targets (t_target t) ?hM ?iM k)))
                                                (?hM q x)))"
          using Suc.prems(1) unfolding pq = (p,q') Cons paths_up_to_length_with_targets.simps 
          by fastforce

        have "x  inputs M"
          using x  List.set ?iM inputs_as_list_set by auto

        have "t  list.set (?hM q x)"
         and **:"(p',q')  list.set (paths_up_to_length_with_targets (t_target t) ?hM ?iM k)"
          using * by auto

        have "t  transitions M" and "t_source t = q"
          using t  list.set (?hM q x) hM by auto

        have "q' = target (t_target t) p'"
         and "path M (t_target t) p'"
         and "length p'  k"
          using Suc.IH[OF ** fsm_transition_target[OF t  transitions M]]
          by auto

        have "q' = target q p"
          unfolding Cons using q' = target (t_target t) p' by auto
        moreover have "path M q p"
          unfolding Cons using path M (t_target t) p' t  transitions M t_source t = q by auto
        moreover have "length p  Suc k"
          unfolding Cons using length p'  k by auto
        ultimately show ?thesis 
          unfolding pq = (p,q') by blast
      qed
    qed
  qed     

  show "?S2 q k  ?S1 q k"
  proof 
    fix pq assume "pq  ?S2 q k"

    obtain p q' where "pq = (p,q')"
      by fastforce

    show "pq  ?S1 q k"
    using assms pq  ?S2 q k unfolding pq = (p,q') proof (induction k arbitrary: q p q')
      case 0
      then show ?case by force
    next
      case (Suc k)  
      then have "q' = target q p"
            and "path M q p"
            and "length p  Suc k"
        by auto

      show ?case proof (cases p)
        case Nil
        then have "q' = q"
          using Suc.prems(2) by auto
        then show ?thesis unfolding Nil by auto
      next
        case (Cons t p')

        then have "q' = target q (t#p')"
            and "path M q (t#p')"
            and "length (t#p')  Suc k"
          using Suc.prems(2)
          by auto 

        have "t  transitions M" and "t_source t = q"
          using path M q (t#p') by auto
        then have "t  list.set (?hM q (t_input t))"
          unfolding hM
          by (metis (mono_tags, lifting) mem_Collect_eq prod.exhaust_sel) 

        have "t_input t  list.set ?iM"
          using fsm_transition_input[OF t  transitions M] inputs_as_list_set by auto


        have "q' = target (t_target t) p'"
          using q' = target q (t#p') by auto
        moreover have "path M (t_target t) p'"
          using path M q (t#p') by auto
        moreover have "length p'  k"
          using length (t#p')  Suc k by auto
        ultimately have "(p',q')  ?S2 (t_target t) k"
          by blast
        moreover define f where f_def: "f = (λq . (paths_up_to_length_with_targets q ?hM ?iM k))"
        ultimately have "(p',q')  list.set (f (t_target t))"
          using Suc.IH[OF fsm_transition_target[OF t  transitions M]]
          by blast
        then have **: "(t#p',q')  list.set ((map (λ(p,q). (t # p,q)) (f (t_target t))))"
          by auto

        have scheme: " x y ys f . x  list.set (f y)  y  list.set ys  x  list.set (concat (map f ys))"
          by auto

        have "(t#p',q')  list.set (concat (map (λt . (map (λ(p,q). (t # p,q))
                                                (f (t_target t))))
                                          (?hM q (t_input t))))"
          using scheme[of "(t#p',q')" "λ t. (map (λ(p,q). (t # p,q)) (f (t_target t)))", OF ** t  list.set (?hM q (t_input t))]
          .

        then have "(t#p',q')  list.set (concat
          (map (λx. concat
                     (map (λt. map (λ(p, y). (t # p, y))
                                (f (t_target t)))
                       (map (λ(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))))))
            (inputs_as_list M)))"
          using t_input t  list.set ?iM by force

        then show ?thesis
          unfolding paths_up_to_length_with_targets.simps f_def Cons by auto
      qed
    qed
  qed
qed



fun pairs_to_distinguish :: "('a::linorder,'b::linorder,'c::linorder) fsm  ('a,'b,'c) state_cover_assignment  ('a  (('a,'b,'c) path × 'a) list)  'a list  ((('b × 'c) list × 'a) × (('b × 'c) list × 'a)) list" where
  "pairs_to_distinguish M V 𝒳' rstates = (let 
    Π = map (λq . (V q,q)) rstates;
    A = List.product Π Π;
    B = List.product Π (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates));
    C = concat (map (λq . concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q))) rstates) 
  in 
    filter (λ((α,q'),(β,q'')) . q'  q'') (A@B@C))"

lemma pairs_to_distinguish_elems :
  assumes "observable M"
  and     "is_state_cover_assignment M V"
  and     "list.set rstates = reachable_states M"
  and     " q p q' . q  reachable_states M  (p,q')  list.set (𝒳' q)  path M q p  target q p = q'  length p  m-n+1"
  and     "((α,q1),(β,q2))  list.set (pairs_to_distinguish M V 𝒳' rstates)"
  
shows "q1  states M" and "q2  states M" and "q1  q2"
  and "α  L M" and "β  L M" and "q1 = after_initial M α" and "q2 = after_initial M β"
proof -

  define Π where Π: "Π = map (λq . (V q,q)) rstates"
  moreover define A where A: "A = List.product Π Π"
  moreover define B where B: "B = List.product Π (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates))"
  moreover define C where C: "C = concat (map (λq . concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q))) rstates)"
  ultimately have pairs_def: "pairs_to_distinguish M V 𝒳' rstates = filter (λ((α,q'),(β,q'')) . q'  q'') (A@B@C)"
    unfolding pairs_to_distinguish.simps Let_def by force

  show "q1  q2"
    using assms(5) unfolding pairs_def by auto

  consider "((α,q1),(β,q2))  list.set A" | "((α,q1),(β,q2))  list.set B" | "((α,q1),(β,q2))  list.set C"
    using assms(5) unfolding pairs_def by auto
  then have "q1  states M  q2  states M  α  L M  β  L M  q1 = after_initial M α  q2 = after_initial M β"
  proof cases
    case 1
    then have "(α,q1)  list.set Π" and "(β,q2)  list.set Π"
      unfolding A by auto
    then show ?thesis unfolding Π using assms(3)
      using reachable_state_is_state 
      using state_cover_assignment_after[OF assms(1,2)]
      by force
  next
    case 2
    then have "(α,q1)  list.set Π" and "(β,q2)  list.set (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates))"
      unfolding B by auto
     
    then obtain q where "q  reachable_states M"
                    and "(β,q2)  list.set (map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q))"
      unfolding assms(3)[symmetric] by (meson concat_map_elem)
    then obtain τ where "(τ,q2)  list.set (𝒳' q)" and "β = (V q)@ p_io τ"
      by force
    then have "path M q τ" and "target q τ = q2" 
      unfolding assms(4)[OF q  reachable_states M] by auto
    moreover obtain p where "path M (initial M) p" and "p_io p = V q" and "target (initial M) p = q"
      using state_cover_assignment_after[OF assms(1,2) q  reachable_states M]
            after_path[OF assms(1)]
      by auto
    ultimately have "path M (initial M) (p@τ)" and "target (initial M) (p@τ) = q2" and "p_io (p@τ) = β"
      unfolding β = (V q)@ p_io τ by auto
    then have "q2 = after_initial M β"
      by (metis (mono_tags, lifting) after_path assms(1))
    moreover have "β  L M"
      using path M (initial M) (p@τ) p_io (p@τ) = β
      by (metis (mono_tags, lifting) language_state_containment) 
    moreover have "q2  states M"
      by (metis path M q τ target q τ = q2 path_target_is_state)
    moreover have "q1  states M"
      using (α,q1)  list.set Π assms(3) reachable_state_is_state unfolding Π by fastforce
    moreover have "α  L M" and "q1 = after_initial M α"
      using (α,q1)  list.set Π assms(3) state_cover_assignment_after[OF assms(1,2)] unfolding Π by auto
    ultimately show ?thesis 
      by blast
  next
    case 3
    then obtain q where "q  reachable_states M"
                    and "((α,q1),(β,q2))  list.set  (concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q)))"
      unfolding assms(3)[symmetric] C by force
    then obtain τ' where "(τ',q2)  list.set (𝒳' q)" and "β = V q @ p_io τ'"
                     and "((α,q1),(β,q2))  list.set (map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q2))) (prefixes τ'))"
      by force
    then obtain τ'' where "τ''  list.set (prefixes τ')" and "α = V q @ p_io τ''"
                      and "((α,q1),(β,q2)) = (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q2))"
      by auto
    then have "q1 = target q τ''"
      by auto

    have "path M q τ'" and "target q τ' = q2"
      using (τ',q2)  list.set (𝒳' q) unfolding assms(4)[OF q  reachable_states M] by simp+
    then have "path M q τ''"
      using τ''  list.set (prefixes τ')
      using prefixes_set_ob by force 
    then have "q1  states M"
      using path_target_is_state unfolding q1 = target q τ'' by force
    moreover have "α  L M" 
      unfolding α = V q @ p_io τ'' 
      using state_cover_assignment_after[OF assms(1,2)]
      by (metis (mono_tags, lifting) path M q τ'' q  reachable_states M assms(1) language_state_containment observable_after_language_append)
    moreover have "q1 = after_initial M α"
      unfolding α = V q @ p_io τ'' 
      using state_cover_assignment_after[OF assms(1,2) q  reachable_states M]
      by (metis (mono_tags, lifting) α = V q @ p_io τ'' path M q τ''  q1 = target q τ'' after_path after_split assms(1) calculation(2))
    moreover have "q2  states M"
      using path M q τ' target q τ' = q2 path_target_is_state by force
    moreover have "β  L M"
      by (metis (mono_tags, lifting) α = V q @ p_io τ'' β = V q @ p_io τ' path M q τ' q  reachable_states M assms(1) assms(2) calculation(2) is_state_cover_assignment_observable_after language_prefix language_state_containment observable_after_language_append)
    moreover have "q2 = after_initial M β"
      unfolding β = V q @ p_io τ'
      using state_cover_assignment_after[OF assms(1,2) q  reachable_states M]
      by (metis (mono_tags, lifting) β = V q @ p_io τ' path M q τ' target q τ' = q2 after_path after_split assms(1) calculation(5))
    ultimately show ?thesis 
      by blast
  qed
  then show "q1  states M" and "q2  states M" and "α  L M" and "β  L M" and "q1 = after_initial M α" and "q2 = after_initial M β"
    by auto
qed


lemma pairs_to_distinguish_containment :
  assumes "observable M"
  and     "is_state_cover_assignment M V"
  and     "list.set rstates = reachable_states M"
  and     " q p q' . q  reachable_states M  (p,q')  list.set (𝒳' q)  path M q p  target q p = q'  length p  m-n+1"
  and     "(α,β)  (V ` reachable_states M) × (V ` reachable_states M)
                   (V ` reachable_states M) × { (V q) @ τ | q τ . q  reachable_states M  τ  {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M}}
                   ( q  reachable_states M .  τ  {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M} . { (V q) @ τ' | τ' . τ'  list.set (prefixes τ)} × {(V q)@τ})"
  and     "α  L M"
  and     "β  L M"
  and     "after_initial M α  after_initial M β"
shows "((α,after_initial M α),(β,after_initial M β))  list.set (pairs_to_distinguish M V 𝒳' rstates)"
proof -

  let ?𝒳 = "λ q . {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M}"

  define Π where Π: "Π = map (λq . (V q,q)) rstates"
  moreover define A where A: "A = List.product Π Π"
  moreover define B where B: "B =List.product Π (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates))"
  moreover define C where C: "C = concat (map (λq . concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q))) rstates)"
  ultimately have pairs_def: "pairs_to_distinguish M V 𝒳' rstates = filter (λ((α,q'),(β,q'')) . q'  q'') (A@B@C)"
    unfolding pairs_to_distinguish.simps Let_def by force


  have V_target: "q . q  reachable_states M  after_initial M (V q) = q"
  proof -
    fix q assume "q  reachable_states M"
    then have "q  io_targets M (V q) (initial M)"
      using assms(2) by auto
    then have "V q  L M"
      unfolding io_targets.simps
      by force 
    
    show "after_initial M (V q) = q"
      by (meson q  reachable_states M assms(1) assms(2) is_state_cover_assignment_observable_after)
  qed

  have V_path: " io q . q  reachable_states M  io  LS M q   p . path M q p  p_io p = io  target q p = after_initial M ((V q)@io)"
  proof -
    fix io q assume "q  reachable_states M" and "io  LS M q"
    then have "after_initial M (V q) = q" 
      using V_target by auto
    then have "((V q)@io)  L M"
      using io  LS M q
      by (meson q  reachable_states M assms(2) is_state_cover_assignment.simps language_io_target_append) 
    then obtain p where "path M (initial M) p" and "p_io p = ((V q)@io)"
      by auto
    moreover have "target (initial M) p  io_targets M ((V q)@io) (initial M)"
      using calculation unfolding io_targets.simps by force
    ultimately have "target (initial M) p = after_initial M ((V q)@io)"
      using observable_io_targets[OF observable M ((V q)@io)  L M] 
      unfolding io_targets.simps
      by (metis (mono_tags, lifting) after_path assms(1)) 

    have "path M (FSM.initial M) (take (length (V q)) p)"
     and "p_io (take (length (V q)) p) = V q"
     and "path M (target (FSM.initial M) (take (length (V q)) p)) (drop (length (V q)) p)"
     and "p_io (drop (length (V q)) p) = io"
      using path_io_split[OF path M (initial M) p p_io p = ((V q)@io)]
      by auto

    have "target (initial M) p = target (target (FSM.initial M) (take (length (V q)) p)) (drop (length (V q)) p)"
      by (metis append_take_drop_id path_append_target)
    moreover have "(target (FSM.initial M) (take (length (V q)) p)) = q"
      using p_io (take (length (V q)) p) = V q after_initial M (V q) = q
      using path M (FSM.initial M) (take (length (V q)) p) after_path assms(1) by fastforce 
    ultimately have "target q (drop (length (V q)) p) = after_initial M ((V q)@io)"
      using target (initial M) p = after_initial M ((V q)@io)
      by presburger
    then show " p . path M q p  p_io p = io  target q p = after_initial M ((V q)@io)"
      using path M (target (FSM.initial M) (take (length (V q)) p)) (drop (length (V q)) p) p_io (drop (length (V q)) p) = io
      unfolding (target (FSM.initial M) (take (length (V q)) p)) = q
      by blast
  qed
      


  consider "(α,β)  (V ` reachable_states M) × (V ` reachable_states M)" |
           "(α,β)  (V ` reachable_states M) × { (V q) @ τ | q τ . q  reachable_states M  τ  {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M}}" |
           "(α,β)  ( q  reachable_states M .  τ  {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M} . { (V q) @ τ' | τ' . τ'  list.set (prefixes τ)} × {(V q)@τ})"
    using assms(5) by blast
  then show ?thesis proof cases
    case 1
    then have "α  V ` reachable_states M"
          and "β  V ` reachable_states M"
      by auto
    
    have "(α,after_initial M α)  list.set (map (λq . (V q,q)) rstates)"
      using α  V ` reachable_states M V_target assms(3) by force
    moreover have "(β,after_initial M β)  list.set (map (λq . (V q,q)) rstates)"
      using β  V ` reachable_states M V_target assms(3) by force
    ultimately have "((α,after_initial M α),(β,after_initial M β))  list.set A"
      unfolding Π A by auto
    then show ?thesis
      using after_initial M α  after_initial M β
      unfolding pairs_def by auto
  next
    case 2
    then have "α  V ` reachable_states M"
          and "β  { (V q) @ τ | q τ . q  reachable_states M  τ  {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M}}"
      by auto

    have "(α,after_initial M α)  list.set (map (λq . (V q,q)) rstates)"
      using α  V ` reachable_states M V_target assms(3) by force

    obtain q io x y where "β = (V q) @ (io@[(x,y)])"
                 and "q  reachable_states M"
                 and "length io  m-n"
      using β  { (V q) @ τ | q τ . q  reachable_states M  τ  {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M}}
      by blast

    have "(V q) @ (io@[(x,y)])  L M"
      using β  L M unfolding β = (V q) @ (io@[(x,y)]) by simp


    have "q  io_targets M (V q) (initial M)"
      using q  reachable_states M assms(2) by auto 
    then have "io@[(x,y)]  LS M q"
      unfolding β = (V q) @ (io@[(x,y)])
      using observable_io_targets_language[OF (V q) @ (io@[(x,y)])  L M observable M]
      by auto
    then obtain p where "path M q p" 
                    and "p_io p = io@[(x,y)]"
                    and "target q p = after_initial M β"
      using V_path[OF q  reachable_states M]
      unfolding β = (V q) @ (io@[(x,y)])
      by blast
    moreover have "length p  m-n+1"
      using calculation length io  m-n
      by (metis (no_types, lifting) Suc_le_mono add.commute length_append_singleton length_map plus_1_eq_Suc) 
    ultimately have "(p,after_initial M β)  list.set (𝒳' q)"
      using assms(4)[OF q  reachable_states M] 
      by auto
    then have "(β,after_initial M β)  list.set (map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q))"
      unfolding β = (V q) @ (io@[(x,y)]) using p_io p = io@[(x,y)] by force
    moreover have "q  list.set rstates"
      using q  reachable_states M assms(3) by auto
    ultimately have "(β,after_initial M β)  list.set (concat (map (λq . map (λ (τ,q') . ((V q)@ p_io τ,q')) (𝒳' q)) rstates))"
      by force
    then have "((α,after_initial M α),(β,after_initial M β))  list.set B"
      using (α,after_initial M α)  list.set (map (λq . (V q,q)) rstates)
      unfolding B Π 
      by auto
    then show ?thesis
      using after_initial M α  after_initial M β
      unfolding pairs_def by auto
  next
    case 3
    then obtain q τ' io x y where "q  reachable_states M"
                                and "io  LS M q" 
                                and "length io  m - n" 
                                and "x  FSM.inputs M" 
                                and "y  FSM.outputs M"
                                and "α = V q @ τ'" 
                                and "τ'  list.set (prefixes ( io @ [(x, y)]))"
                                and "β = V q @ io @ [(x, y)]"
      by blast



    have "(V q) @ (io@[(x,y)])  L M"
      using β  L M unfolding β = (V q) @ (io@[(x,y)]) by simp
    

    have "q  io_targets M (V q) (initial M)"
      using q  reachable_states M assms(2) by auto 
    then have "io@[(x,y)]  LS M q"
      unfolding β = (V q) @ (io@[(x,y)])
      using observable_io_targets_language[OF (V q) @ (io@[(x,y)])  L M observable M]
      by auto
    then obtain p where "path M q p" 
                    and "p_io p = io@[(x,y)]"
                    and "target q p = after_initial M β"
      using V_path[OF q  reachable_states M]
      unfolding β = (V q) @ (io@[(x,y)])
      by blast
    moreover have "length p  m-n+1"
      using calculation length io  m-n
      by (metis (no_types, lifting) Suc_le_mono add.commute length_append_singleton length_map plus_1_eq_Suc) 
    ultimately have "(p,after_initial M β)  list.set (𝒳' q)"
      using assms(4)[OF q  reachable_states M] 
      by auto
    
    have "q  list.set rstates"
      using q  reachable_states M assms(3) by auto

    let  = "take (length τ') (io@[(x,y)])"
    obtain τ'' where "io @ [(x, y)] = τ' @ τ''"
      using τ'  list.set (prefixes ( io @ [(x, y)]))
      using prefixes_set_ob by blast 
    then have "τ' = "
      by auto
    then have "io@[(x,y)] = τ' @ (drop (length τ') (io@[(x,y)]))"
      by (metis append_take_drop_id)
    then have "p_io p = τ' @ (drop (length τ') (io@[(x,y)]))"
      using p_io p = io@[(x,y)]
      by simp
    
    have "path M q (take (length τ') p)"
     and "p_io (take (length τ') p) = τ'"
      using path_io_split(1,2)[OF path M q p p_io p = τ' @ (drop (length τ') (io@[(x,y)]))]
      by auto
    then have "τ'  LS M q"
      using language_intro by fastforce

    have "(V q) @ τ'  L M"
      using (V q) @ (io@[(x,y)])  L M unfolding io @ [(x, y)] = τ' @ τ'' 
      using language_prefix[of "V q @ τ'" τ'' M "initial M"] 
      by auto 
      
      
    have "(FSM.after M (FSM.initial M) (V q)) = q"
      using V_target q  reachable_states M by blast
    have "target q (take (length τ') p) = after_initial M α"
      using observable_after_target[OF observable M (V q) @ τ'  L M _ p_io (take (length τ') p) = τ'] 
      using path M q (take (length τ') p)
      unfolding (FSM.after M (FSM.initial M) (V q)) = q α = V q @ τ'
      by auto

    have "p = (take (length τ') p)@(drop (length τ') p)"
      by simp
    then have "(take (length τ') p)  list.set (prefixes p)"
      unfolding prefixes_set
      by (metis (mono_tags, lifting) mem_Collect_eq) 


    have "(((V q)@ p_io (take (length τ') p), target q (take (length τ') p)),((V q)@ p_io p,after_initial M β))  list.set ( (λ(τ', q'). map (λτ''. ((V q @ p_io τ'', target q τ''), V q @ p_io τ', q')) (prefixes τ')) (p,after_initial M β))"
      using (take (length τ') p)  list.set (prefixes p)
      by auto
    then have *: "((α, after_initial M α),(β,after_initial M β))  list.set ( (λ(τ', q'). map (λτ''. ((V q @ p_io τ'', target q τ''), V q @ p_io τ', q')) (prefixes τ')) (p,after_initial M β))"
      unfolding α = V q @ τ' 
                β = V q @ io @ [(x, y)] 
                target q (take (length τ') p) = after_initial M α 
                p_io (take (length τ') p) = τ'
                p_io p = io@[(x,y)] .

    have scheme: " x y ys f . x  list.set (f y)  y  list.set ys  x  list.set (concat (map f ys))"
      by auto


    have **: "((α, after_initial M α),(β,after_initial M β))  list.set (concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q)))"
      using scheme[of _ "(λ(τ', q'). map (λτ''. ((V q @ p_io τ'', target q τ''), V q @ p_io τ', q')) (prefixes τ'))", OF * (p,after_initial M β)  list.set (𝒳' q)]
      .

    have "((α, after_initial M α),(β,after_initial M β))  list.set C"
      unfolding C 
      using scheme[of _ "(λq . concat (map (λ (τ',q'). map (λτ'' . (((V q)@ p_io τ'', target q τ''),((V q)@ p_io τ',q'))) (prefixes τ')) (𝒳' q)))", OF ** q  list.set rstates]
      .

    then show ?thesis
      using after_initial M α  after_initial M β
      unfolding pairs_def by auto
  qed
qed


subsection ‹Definition of the Pair-Framework›

definition pair_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm 
                              nat 
                              (('a,'b,'c) fsm  nat  ('b×'c) prefix_tree) 
                              (('a,'b,'c) fsm  nat  ((('b × 'c) list × 'a) × (('b × 'c) list × 'a)) list) 
                              (('a,'b,'c) fsm  (('b × 'c) list × 'a) × ('b × 'c) list × 'a  ('b × 'c) prefix_tree  ('b × 'c) prefix_tree) 
                              ('b×'c) prefix_tree" 
where
  "pair_framework M m get_initial_test_suite get_pairs get_separating_traces =   
    (let 
      TS = get_initial_test_suite M m;
      D  = get_pairs M m;
      dist_extension = (λ t ((α,q'),(β,q'')) . let tDist = get_separating_traces M ((α,q'),(β,q'')) t
                                                in combine_after (combine_after t α tDist) β tDist)
    in 
      foldl dist_extension TS D)"



lemma pair_framework_completeness :
  assumes "observable M"
  and     "observable I"
  and     "minimal M"
  and     "size I  m"
  and     "m  size_r M"
  and     "inputs I = inputs M"
  and     "outputs I = outputs M"
  and     "is_state_cover_assignment M V"
  and     "{(V q)@io@[(x,y)] | q io x y . q  reachable_states M  io  LS M q  length io  m - size_r M  x  inputs M  y  outputs M}  set (get_initial_test_suite M m)"
  and     " α β . (α,β)  (V ` reachable_states M) × (V ` reachable_states M)
                       (V ` reachable_states M) × { (V q) @ τ | q τ . q  reachable_states M  τ  {io@[(x,y)] | io x y . io  LS M q  length io  m-size_r M  x  inputs M  y  outputs M}}
                       ( q  reachable_states M .  τ  {io@[(x,y)] | io x y . io  LS M q  length io  m-size_r M  x  inputs M  y  outputs M} . { (V q) @ τ' | τ' . τ'  list.set (prefixes τ)} × {(V q)@τ}) 
                    α  L M  β  L M  after_initial M α  after_initial M β 
                    ((α,after_initial M α),(β,after_initial M β))  list.set (get_pairs M m)"
  and     " α β t . α  L M  β  L M  after_initial M α  after_initial M β   io  set (get_separating_traces M ((α,after_initial M α),(β,after_initial M β)) t)  (set (after t α)  set (after t β)) . distinguishes M (after_initial M α) (after_initial M β) io"
shows "(L M = L I)  (L M  set (pair_framework M m get_initial_test_suite get_pairs get_separating_traces) = L I  set (pair_framework M m get_initial_test_suite get_pairs get_separating_traces))"
proof (cases "inputs M = {}  outputs M = {}")
  case True (* handle case of empty input or outputs *)
  then consider "inputs M = {}" | "outputs M = {}" by blast
  then show ?thesis proof cases
    case 1
    have "L M = {[]}"
      using "1" language_empty_IO by blast
    moreover have "L I = {[]}"
      by (metis "1" assms(6) language_empty_IO)
    ultimately show ?thesis by blast
  next
    case 2
    have "L M = {[]}"
      using language_io(2)[of _ M "initial M"] unfolding 2
      by (metis (no_types, opaque_lifting) ex_in_conv is_singletonI' is_singleton_the_elem language_contains_empty_sequence set_empty2 singleton_iff surj_pair) 
    moreover have "L I = {[]}"
      using language_io(2)[of _ I "initial I"] unfolding 2 outputs I = outputs M
      by (metis (no_types, opaque_lifting) ex_in_conv is_singletonI' is_singleton_the_elem language_contains_empty_sequence set_empty2 singleton_iff surj_pair)
    ultimately show ?thesis by blast
  qed
next
  case False


  define T where T: "T = get_initial_test_suite M m"
  moreover define pairs where pairs: "pairs  = get_pairs M m"
  moreover define distExtension where distExtension: "distExtension = (λ t ((α,q'),(β,q'')) . let tDist = get_separating_traces M ((α,q'),(β,q'')) t
                                                                       in combine_after (combine_after t α tDist) β tDist)"
  ultimately have res_def: "pair_framework M m get_initial_test_suite get_pairs get_separating_traces = foldl distExtension T pairs"
    unfolding pair_framework_def Let_def by auto

  define T' where T': "T' = set (foldl distExtension T pairs)"
  then have T'r: "T' = set (foldr (λ x y . distExtension y x) (rev pairs) T)"
    by (simp add: foldl_conv_foldr) 

  define Π where Π: "Π = (V ` reachable_states M)"
  define n where n: "n = size_r M"
  define 𝒳 where 𝒳: "𝒳 = (λ q . {io@[(x,y)] | io x y . io  LS M q  length io  m-n  x  inputs M  y  outputs M})"
  define A where A: "A = Π × Π"
  define B where B: "B = Π × { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}"
  define C where C: "C = ( q  reachable_states M .  τ  𝒳 q . { (V q) @ τ' | τ' . τ'  list.set (prefixes τ)} × {(V q)@τ})"
  

  have satisfaction_conditions: "is_state_cover_assignment M V 
    Π  T' 
    { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}  T' 
    ( α β . (α,β)  A  B  C  
              α  L M 
              β  L M 
              after_initial M α  after_initial M β 
              ( ω . α@ω  T' 
                     β@ω  T' 
                     distinguishes M (after_initial M α) (after_initial M β) ω)) 
    satisfies_h_condition M V T' m"
    unfolding satisfies_h_condition_def Let_def Π n 𝒳 A B C  
    by force

  have c1: "is_state_cover_assignment M V"
    using assms(8) .

  have c2: "Π  T'" and c3: "{ (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}  T'"
  proof -
    have "set T  T'"
      unfolding T' 
    proof (induction pairs rule: rev_induct)
      case Nil
      then show ?case by auto
    next
      case (snoc a pairs)

      obtain α q' β q'' where "a = ((α,q'),(β,q''))"
        by (metis prod.collapse) 

      have "foldl distExtension T (pairs @ [a]) = distExtension (foldl distExtension T pairs) a"
        by simp 
      moreover have " t . set t  set (distExtension t a)" 
      proof -
        fix t
        have "distExtension t a = combine_after (combine_after t α (get_separating_traces M ((α,q'),(β,q'')) t)) β (get_separating_traces M ((α,q'),(β,q'')) t)"
          unfolding distExtension a = ((α,q'),(β,q'')) Let_def by auto
        moreover have " t' . set t  set (combine_after (combine_after t α t') β t')"
          unfolding combine_after_set by blast
        ultimately show "set t  set (distExtension t a)" 
          by simp
      qed
      ultimately show ?case
        using snoc.IH by auto
    qed

    have "Π  set T"
    proof 
      fix io assume "io  Π"
      then obtain q where "io = (V q)"
                      and "q  reachable_states M"                      
        unfolding Π
        by blast

      obtain x y where "x  inputs M" and "y  outputs M" 
        using False by blast
      moreover have "[]  LS M q"
        using reachable_state_is_state[OF q  reachable_states M] by auto
      ultimately have "(V q) @ [(x,y)]  set T"
        using assms(9) q  reachable_states M
        unfolding T[symmetric] by force
      then show "io  set T"
        unfolding Π
        using io = V q set_prefix by auto 
    qed
    then show "Π  T'"
      using set T  T' by blast


    have "{ (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}  set T" 
      using assms(9)
      unfolding 𝒳 T[symmetric] n[symmetric] by force
    then show "{ (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}  T'"
      using set T  T' by blast
  qed

  have c4: "( α β . (α,β)  A  B  C  
              α  L M 
              β  L M 
              after_initial M α  after_initial M β 
              ( ω . α@ω  T' 
                     β@ω  T' 
                     distinguishes M (after_initial M α) (after_initial M β) ω))"    
  proof -
    fix α β assume "(α,β)  A  B  C"
               and "α  L M"
               and "β  L M"
               and "after_initial M α  after_initial M β"


    have "((α, FSM.after M (FSM.initial M) α), β, FSM.after M (FSM.initial M) β)  list.set pairs"
      using (α,β)  A  B  C
      unfolding A B C Π 𝒳 pairs
      using α  L M β  L M after_initial M α  after_initial M β assms(10) n by force
    moreover note α  L M β  L M after_initial M α  after_initial M β
    moreover have " α β . ((α,after_initial M α),(β,after_initial M β))  list.set pairs  α  L M  β  L M  after_initial M α  after_initial M β   io . io  (LS M (after_initial M α) - LS M (after_initial M β))  (LS M (after_initial M β) - LS M (after_initial M α))  α@io  T'  β@io  T'"
      unfolding T' proof (induction pairs rule: rev_induct)
      case Nil
      then show ?case by auto
    next
      case (snoc a pairs)

      obtain αa q'a βa q''a where "a = ((αa,q'a),(βa,q''a))"
        by (metis prod.collapse) 

      have "foldl distExtension T (pairs @ [a]) = distExtension (foldl distExtension T pairs) a"
        by simp 
      moreover have " t . set t  set (distExtension t a)"
      proof -
        fix t
        have "distExtension t a = combine_after (combine_after t αa (get_separating_traces M ((αa,q'a),(βa,q''a)) t)) βa (get_separating_traces M ((αa,q'a),(βa,q''a)) t)"
          unfolding distExtension a = ((αa,q'a),(βa,q''a)) Let_def by auto
        moreover have " t' . set t  set (combine_after (combine_after t αa t') βa t')"
          unfolding combine_after_set by blast
        ultimately show "set t  set (distExtension t a)" 
          by simp
      qed
      ultimately have "set (foldl distExtension T pairs)  set (foldl distExtension T (pairs@[a]))"
        by auto

      let ?q' = "after_initial M α"
      let ?q'' = "after_initial M β"

      show ?case proof (cases "a = ((α,?q'),(β,?q''))")
        case True
        then have "foldl distExtension T (pairs @ [a]) = distExtension (foldl distExtension T pairs) ((α,?q'),(β,?q''))"
          by auto 
        also have " = combine_after (combine_after (foldl distExtension T pairs) α (get_separating_traces M ((α, ?q'), (β, ?q'')) (foldl distExtension T pairs))) β (get_separating_traces M ((α, ?q'), (β, ?q'')) (foldl distExtension T pairs))"
          using distExtension 
          by (metis (no_types, lifting) case_prod_conv)
        finally have "foldl distExtension T (pairs @ [a]) = combine_after (combine_after (foldl distExtension T pairs) α (get_separating_traces M ((α, ?q'), (β, ?q'')) (foldl distExtension T pairs))) β (get_separating_traces M ((α, ?q'), (β, ?q'')) (foldl distExtension T pairs))"
          .
        moreover define dist where dist: "dist = (get_separating_traces M ((α,?q'),(β,?q'')) (foldl distExtension T pairs))"
        ultimately have *: "foldl distExtension T (pairs @ [a]) = combine_after (combine_after (foldl distExtension T pairs) α dist) β dist"
          by auto

        define ta where "ta = (after (foldl distExtension T pairs) α)"
        define tb where "tb = (after (foldl distExtension T pairs) β)"
        obtain io where "io  set dist  (set ta  set tb)" and "io  (LS M ?q' - LS M ?q'')  (LS M ?q'' - LS M ?q')"
          using assms(11)[OF snoc.prems(2,3,4), of "(foldl distExtension T pairs)"]
          unfolding dist distinguishes_def ta_def tb_def by blast 
        then consider "io  set dist" | "io  (set ta  set tb)"
          by blast

        then show ?thesis proof cases
          case 1
          then have "α@io  set (foldl distExtension T (pairs @ [a]))" and "β@io  set (foldl distExtension T (pairs @ [a]))"
            unfolding * using combine_after_set by blast+
          then show ?thesis 
            using io  (LS M ?q' - LS M ?q'')  (LS M ?q'' - LS M ?q') by auto
        next
          case 2
          moreover have "io  []"
            using io  (LS M ?q' - LS M ?q'')  (LS M ?q'' - LS M ?q')
                  after_is_state[OF assms(1) snoc.prems(2)]
                  after_is_state[OF assms(1) snoc.prems(3)]
            by auto
          ultimately have "α@io  set (foldl distExtension T pairs)" and "β@io  set (foldl distExtension T pairs)"
            unfolding ta_def tb_def after_set by blast+
          then show ?thesis
            using io  (LS M ?q' - LS M ?q'')  (LS M ?q'' - LS M ?q')
                  set (foldl distExtension T pairs)  set (foldl distExtension T (pairs @ [a]))
            by auto
        qed
      next
        case False
        then have "((α,?q'),(β,?q''))  list.set pairs"
          using snoc.prems(1) by auto

        show ?thesis 
          using snoc.IH[OF ((α,?q'),(β,?q''))  list.set pairs snoc.prems(2,3,4)]
                set (foldl distExtension T pairs)  set (foldl distExtension T (pairs @ [a]))
          by auto
      qed
    qed
    ultimately show "( ω . α@ω  T'  β@ω  T'  distinguishes M (after_initial M α) (after_initial M β) ω)"
      unfolding distinguishes_def  by blast
  qed

  have "satisfies_h_condition M V T' m"
    using satisfaction_conditions[OF c1 c2 c3 c4]
    by blast
  then have "satisfies_h_condition M V (set (pair_framework M m get_initial_test_suite get_pairs get_separating_traces)) m"
    unfolding res_def T' .
  then show ?thesis
    using h_condition_completeness[OF assms(1-7)]
    by blast
qed



lemma pair_framework_finiteness :
  assumes " α β t . α  L M  β  L M  after_initial M α  after_initial M β  finite_tree (get_separating_traces M ((α,after_initial M α),(β,after_initial M β)) t)"
  and     "finite_tree (get_initial_test_suite M m)"
  and     " α q' β q'' . ((α,q'),(β,q''))  list.set (get_pairs M m)  α  L M  β  L M  after_initial M α  after_initial M β  q' = after_initial M α  q'' = after_initial M β"
shows "finite_tree (pair_framework M m get_initial_test_suite get_pairs get_separating_traces)"
proof -
  
  define T where T: "T = get_initial_test_suite M m"
  moreover define pairs where pairs: "pairs  = get_pairs M m"
  moreover define distExtension where distExtension: "distExtension = (λ t ((α,q'),(β,q'')) . let tDist = get_separating_traces M ((α,q'),(β,q'')) t
                                                                       in combine_after (combine_after t α tDist) β tDist)"
  ultimately have res_def: "pair_framework M m get_initial_test_suite get_pairs get_separating_traces = foldl distExtension T pairs"
    unfolding pair_framework_def Let_def by auto

  have " α q' β q'' . ((α,q'),(β,q''))  list.set pairs  α  L M  β  L M  after_initial M α  after_initial M β  q' = after_initial M α  q'' = after_initial M β"
    using assms(3) unfolding pairs by auto
  then show ?thesis
  unfolding res_def proof (induction pairs rule: rev_induct)
    case Nil
    then show ?case 
      using from_list_finite_tree assms(2)
      unfolding T 
      by auto
  next
    case (snoc a pairs)
    then have p1: " α q' β q'' . ((α,q'),(β,q''))  list.set pairs  α  L M  β  L M  after_initial M α  after_initial M β  q' = after_initial M α  q'' = after_initial M β"
      by (metis butlast_snoc in_set_butlastD)

    obtain α q' β q'' where "a = ((α,q'),(β,q''))"
      by (metis prod.collapse) 
    then have "foldl distExtension T (pairs @ [a]) = distExtension (foldl distExtension T pairs) ((α,q'),(β,q'')) "
      by auto
    also have " = combine_after (combine_after (foldl distExtension T pairs) α (get_separating_traces M ((α,q'),(β,q'')) (foldl distExtension T pairs))) β (get_separating_traces M ((α,q'),(β,q'')) (foldl distExtension T pairs))"
      using distExtension 
      by (metis (no_types, lifting) case_prod_conv)
    finally have "foldl distExtension T (pairs @ [a]) = combine_after (combine_after (foldl distExtension T pairs) α (get_separating_traces M ((α,q'),(β,q'')) (foldl distExtension T pairs))) β (get_separating_traces M ((α,q'),(β,q'')) (foldl distExtension T pairs))"
      .
    moreover define ta where ta: "ta = (after (foldl distExtension T pairs) α)"
    moreover define tb where tb: "tb = (after (foldl distExtension T pairs) β)"
    moreover define dist where dist: "dist = (get_separating_traces M ((α,q'),(β,q'')) (foldl distExtension T pairs))"
        ultimately have *: "foldl distExtension T (pairs @ [a]) = combine_after (combine_after (foldl distExtension T pairs) α dist) β dist"
          by auto

    have "((α,q'),(β,q''))  list.set (a#pairs)"
      unfolding a = ((α,q'),(β,q'')) by auto
    then have "α  L M  β  L M  after_initial M α  after_initial M β  q' = after_initial M α  q'' = after_initial M β"
      using snoc.prems
      by auto 
    then have "finite_tree dist"
      using assms(1) unfolding dist by auto
    moreover have "finite_tree (foldl distExtension T pairs)"
      using snoc.IH[OF p1] by auto
    ultimately show ?case
      unfolding * 
      using combine_after_finite_tree by blast
  qed
qed


end