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