Theory H_Framework

section ‹H-Framework›

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

theory H_Framework
imports Convergence_Graph "../Prefix_Tree" "../State_Cover"
begin


subsection ‹Abstract H-Condition›

(* assumes that V is a state cover assignment *)
definition satisfies_abstract_h_condition :: "('a,'b,'c) fsm  ('e,'b,'c) fsm  ('a,'b,'c) state_cover_assignment  nat  bool" where
  "satisfies_abstract_h_condition M1 M2 V m = ( q γ . 
    q  reachable_states M1  
    length γ  Suc (m-size_r M1)  
    list.set γ  inputs M1 × outputs M1   
    butlast γ  LS M1 q  
    (let traces = (V ` reachable_states M1)
                   {V q @ ω' | ω'. ω'  list.set (prefixes γ)} 
      in (L M1  traces = L M2  traces)
          preserves_divergence M1 M2 traces))"



lemma abstract_h_condition_exhaustiveness :
  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     "satisfies_abstract_h_condition M I V m"
shows "L M = L I"
proof (rule ccontr)
  assume "L M  L I"

  (* unfold the sufficient condition for easier reference *)

  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})"

  have pass_prop: " q γ . q  reachable_states M  length γ  Suc (m-n)  list.set γ  inputs M × outputs M   butlast γ  LS M q 
                    (L M  (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})
                     = L I  (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))"
  and dist_prop: " q γ . q  reachable_states M  length γ  Suc (m-n)  list.set γ  inputs M × outputs M   butlast γ  LS M q 
                     preserves_divergence M I (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})"
    using satisfies_abstract_h_condition M I V m 
    unfolding satisfies_abstract_h_condition_def Let_def Π n  by blast+

  have pass_prop_𝒳 : " q γ . q  reachable_states M  γ  𝒳 q 
                           (L M  (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})
                            = L I  (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))"
   and dist_prop_𝒳 : " q γ . q  reachable_states M  γ  𝒳 q 
                           preserves_divergence M I (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})"
  proof -
    fix q γ assume *: "q  reachable_states M" and "γ  𝒳 q"
    then obtain io x y where "γ = io@[(x,y)]" and "io  LS M q" and "length io  m-n" and "x  inputs M" and "y  outputs M"
      unfolding 𝒳 by blast

    have **:"length γ  Suc (m-n)"
      using γ = io@[(x,y)] length io  m-n by auto
    have ***:"list.set γ  inputs M × outputs M"
      using language_io[OF io  LS M q] x  inputs M y  outputs M
      unfolding γ = io@[(x,y)] by auto
    have ****:"butlast γ  LS M q"
      unfolding γ = io@[(x,y)] using io  LS M q by auto
    
    show "(L M  (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})
                            = L I  (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))"
      using pass_prop[OF * ** *** ****] .
    show "preserves_divergence M I (Π  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})"
      using dist_prop[OF * ** *** ****] .
  qed


  (* obtain minimal trace that
      - extends some sequence of the state cover (which contains the empty sequence), and
      - is contained in either L M or L I *)
 
  have "(L M  Π) = (L I  Π)"
    using pass_prop[OF reachable_states_initial, of "[]"] language_contains_empty_sequence[of M] by auto
  moreover have "Π  L M"
    unfolding Π using state_cover_assignment_after(1)[OF assms(1) is_state_cover_assignment M V]
    by blast
  ultimately have "Π  L I"
    using Π = (V ` reachable_states M) by blast

  obtain π τ' where "π  Π"
                and "π @ τ'  (L M - L I)  (L I - L M)"
                and " io q . q  reachable_states M  (V q)@io  (L M - L I)  (L I - L M)  length τ'  length io"
    using (L M  Π) = (L I  Π)
    using minimal_sequence_to_failure_from_state_cover_assignment_ob[OF L M  L I is_state_cover_assignment M V] 
    unfolding Π
    by blast

  obtain q where "q  reachable_states M" and "π = V q"
    using π  Π unfolding Π by blast
  then have "π  L M" and "after_initial M π = q"
    using state_cover_assignment_after[OF assms(1) is_state_cover_assignment M V]
    by blast+
  

  have τ'_min: " π' io . π'  Π  π'@io  (L M - L I)  (L I - L M)  length τ'  length io"
  proof -
    fix π' io
    assume "π'  Π" and "π'@io  (L M - L I)  (L I - L M)"
    then obtain q where "q  reachable_states M" and "π' = V q"
      unfolding Π by blast
    then show "length τ'  length io"
      using  io q . q  reachable_states M  (V q)@io  (L M - L I)  (L I - L M)  length τ'  length io
            π'@io  (L M - L I)  (L I - L M) by auto
  qed


  

  obtain πτ xy τ'' where "π @ τ' = πτ @ [xy] @ τ''"
                      and "πτ  L M  L I"
                      and "πτ@[xy]  (L I - L M)  (L M - L I)"
    using minimal_failure_prefix_ob[OF observable M observable I fsm_initial fsm_initial, of "π @ τ'"]
    using minimal_failure_prefix_ob[OF observable I observable M fsm_initial fsm_initial, of "π @ τ'"]
    using π @ τ'  (L M - L I)  (L I - L M)
    by (metis Int_commute Un_iff)

  moreover obtain x y where "xy = (x,y)"
    using surjective_pairing by blast

  moreover have "πτ = π @ butlast τ'"
  proof -
    have "length πτ  length π"
    proof (rule ccontr) 
      assume "¬ length π  length πτ"
      then have "length (πτ@[xy])  length π"
        by auto
      then have "take (length (πτ@[xy])) π = πτ@[xy]"
        using π @ τ' = πτ @ [xy] @ τ''
        by (metis append_assoc append_eq_append_conv_if) 
      then have "π = (πτ@[xy]) @ (drop (length (πτ@[xy])) π)"
        by (metis append_take_drop_id)          
      then have "πτ@[xy]  L M  L I"
        using π  Π Π  L I Π  L M 
        using language_prefix[of "(πτ@[xy])" "drop (length (πτ@[xy])) π", of M "initial M"]
        using language_prefix[of "(πτ@[xy])" "drop (length (πτ@[xy])) π", of I "initial I"]
        by auto
      then show "False"
        using πτ@[xy]  (L I - L M)  (L M - L I) by blast
    qed

    then have "πτ = π @ (take (length πτ - length π) τ')"
      using π @ τ' = πτ @ [xy] @ τ''
      by (metis dual_order.refl take_all take_append take_le) 
    then have "π @ ((take (length πτ - length π) τ')@[xy])  (L I - L M)  (L M - L I)"
      using πτ@[xy]  (L I - L M)  (L M - L I)
      by (metis append_assoc)        
    then have "length τ'  Suc (length (take (length πτ - length π) τ'))"
      using τ'_min[OF π  Π]
      by (metis Un_commute length_append_singleton)
    moreover have "length τ'  Suc (length (take (length πτ - length π) τ'))"
      using π @ τ' = πτ @ [xy] @ τ'' πτ = π @ take (length πτ - length π) τ' not_less_eq_eq by fastforce
    ultimately have "length τ' = Suc (length (take (length πτ - length π) τ'))"
      by simp
    then show ?thesis
    proof -
      have "π @ τ' = (π @ take (length πτ - length π) τ') @ [xy] @ τ''"
        using π @ τ' = πτ @ [xy] @ τ'' πτ = π @ take (length πτ - length π) τ' by presburger
      then have "take (length πτ - length π) τ' = butlast τ'"
        by (metis (no_types) length τ' = Suc (length (take (length πτ - length π) τ')) append_assoc append_butlast_last_id append_eq_append_conv diff_Suc_1 length_butlast length_greater_0_conv zero_less_Suc)
      then show ?thesis
        using πτ = π @ take (length πτ - length π) τ' by fastforce
    qed 
  qed

  ultimately have "π @ (butlast τ')  L M  L I"
              and "(π @ (butlast τ'))@[(x,y)]  (L I - L M)  (L M - L I)"
    by auto

  have "τ' = (butlast τ')@[(x,y)]"
    using π @ τ' = πτ @ [xy] @ τ'' xy = (x,y) 
    unfolding πτ = π @ butlast τ'
    by (metis (no_types, opaque_lifting) append_Cons append_butlast_last_id butlast.simps(1) butlast_append last_appendR list.distinct(1) self_append_conv)


  have "x  inputs M" and "y  outputs M"
  proof -
    have *: "(x,y)  list.set ((π @ (butlast τ'))@[(x,y)])"
      by auto

    show "x  inputs M"
      using (π @ (butlast τ'))@[(x,y)]  (L I - L M)  (L M - L I) 
            language_io(1)[OF _ *, of I]
            language_io(1)[OF _ *, of M]
            inputs I = inputs M
      by blast

    show "y  outputs M"
      using (π @ (butlast τ'))@[(x,y)]  (L I - L M)  (L M - L I) 
            language_io(2)[OF _ *, of I]
            language_io(2)[OF _ *, of M]
            outputs I = outputs M
      by blast
  qed

  have "π @ (butlast τ')  L M"
    using  π @ (butlast τ')  L M  L I by auto
  have "list.set (π @ τ')  inputs M × outputs M"
    using π @ τ'  (L M - L I)  (L I - L M)
    using language_io[of π @ τ' M "initial M"]
    using language_io[of π @ τ' I "initial I"]
    unfolding assms(6,7) by fast 
  then have "list.set τ'  inputs M × outputs M"
    by auto
  have "list.set (butlast τ')  inputs M × outputs M"
    using language_io[OF π @ (butlast τ')  L M] by force
  have "butlast τ'  LS M q"
    using after_language_iff[OF assms(1) π  L M] π @ (butlast τ')  L M
    unfolding after_initial M π = q
    by blast

  have "length τ' > m - n + 1"
  proof (rule ccontr)
    assume "¬ m - n + 1 < length τ'"
    then have "length τ'  Suc (m - n)"
      by auto

    have "π @ τ'  (Π  {V q @ ω' |ω'. ω'  list.set (prefixes τ')})"
      unfolding π = V q using q  reachable_states M  unfolding prefixes_set by auto
    then have "L M  {π @ τ'} = L I  {π @ τ'}"
      using pass_prop[OF q  reachable_states M length τ'  Suc (m - n) list.set τ'  inputs M × outputs M butlast τ'  LS M q]
      by blast
    then show False
      using π @ τ'  (L M - L I)  (L I - L M) by blast
  qed



  define τ where τ_def: "τ = (λi . take i (butlast τ'))"

  have " i . i > 0  i  m - n + 1  (τ i)  𝒳 q"
  proof -
    fix i assume "i > 0" and "i  m - n + 1"
    
    then have "τ i = (butlast (τ i)) @ [last (τ i)]"
      using τ_def length τ' > m - n + 1
      by (metis add_less_same_cancel2 append_butlast_last_id length_butlast less_diff_conv list.size(3) not_add_less2 take_eq_Nil) 

    have "length (butlast (τ i))  m - n" 
      using τ_def length τ' > m - n + 1 i  m - n + 1 by auto


    have "q  io_targets M π (initial M)"
      using is_state_cover_assignment M V q  reachable_states M π = V q
      by simp 
    then have "(butlast τ')  LS M q"
      using π @ (butlast τ')  L M  L I 
      using observable_io_targets_language[OF _ observable M] 
      by force
    then have "τ i @ (drop i (butlast τ'))  LS M q"
      using τ_def by auto
    then have "τ i  LS M q"
      using language_prefix
      by fastforce 
    then have "butlast (τ i)  LS M q"
      using language_prefix τ i = (butlast (τ i)) @ [last (τ i)]
      by metis 

    have "(fst (last (τ i)), snd (last (τ i)))  list.set ((butlast (τ i)) @ [last (τ i)])"
      using τ i = (butlast (τ i)) @ [last (τ i)]
      using in_set_conv_decomp by fastforce
    then have "fst (last (τ i))  inputs M" 
          and "snd (last (τ i))  outputs M"
      using τ i  LS M q τ i = (butlast (τ i)) @ [last (τ i)] language_io[of "(butlast (τ i)) @ [last (τ i)]" M q "fst (last (τ i))" "snd (last (τ i))"] 
      by auto
      
    then show "τ i  𝒳 q"
      unfolding 𝒳 
      using length (butlast (τ i))  m - n τ i = (butlast (τ i)) @ [last (τ i)]
            butlast (τ i)  LS M q
      by (metis (mono_tags, lifting) mem_Collect_eq surjective_pairing)
  qed

  have " i . i  m-n+1  π @ (τ i)  L M  L I"
  proof -
    fix i assume "i  m-n+1"

    have "butlast τ' = τ i @ (drop i (butlast τ'))"
      unfolding τ_def by auto
    then have (π @ τ i) @ (drop i (butlast τ'))  L M  L I
      using π @ (butlast τ')  L M  L I
      by auto
    then show "π @ (τ i)  L M  L I"
      using language_prefix[of "(π @ τ i)" "(drop i (butlast τ'))", of M "initial M"]
      using language_prefix[of "(π @ τ i)" "(drop i (butlast τ'))", of I "initial I"]
      by blast
  qed

  have B_diff: "Π  (λi . π @ (τ i)) ` {1 .. m-n+1} = {}"
  proof -
    have " io1 io2 . io1  Π  io2  (λi . π @ (τ i)) ` {1 .. m-n+1}  io1  io2"
    proof (rule ccontr)
      fix io1 io2 assume "io1  Π" "io2  (λi . π @ (τ i)) ` {1 .. m-n+1}" "¬ io1  io2"

      then obtain i where "io2 = π @ (τ i)" and "i  1" and "i  m - n + 1" and "π @ (τ i)  Π"
        by auto
      then have "π @ (τ i)  L M"
        using  i . i  m-n+1  π @ (τ i)  L M  L I by auto
      
      obtain q where "q  reachable_states M" and "V q = π @ (τ i)"
        using π @ (τ i)  Π Π
        by auto 
      moreover have "(π @ (τ i))@(drop i τ')  (L M - L I)  (L I - L M)"
        using τ_def π @ τ'  (L M - L I)  (L I - L M) length τ' > m - n + 1 i  m - n + 1
        by (metis append_assoc append_take_drop_id le_iff_sup sup.strict_boundedE take_butlast) 
      ultimately have "length τ'  length (drop i τ')"
        using  io q . q  reachable_states M  (V q)@io  (L M - L I)  (L I - L M)  length τ'  length io
        by presburger
      then show "False"
        using length τ' > m - n + 1 i  1
        by (metis One_nat_def i  m - n + 1 diff_diff_cancel diff_is_0_eq' le_trans length_drop less_Suc_eq nat_less_le) 
    qed
    then show ?thesis 
      by blast
  qed


  have same_targets_in_I: " α β . 
                    α  Π  (λi . π @ (τ i)) ` {1 .. m-n+1}
                     β  Π  (λi . π @ (τ i)) ` {1 .. m-n+1}
                     α  β  (after_initial I α = after_initial I β)"
  proof - 
    have "after_initial I ` (Π  (λi . π @ (τ i)) ` {1 .. m-n+1})  states I"
    proof 
      fix q assume "q  after_initial I ` (Π  (λi . π @ (τ i)) ` {1 .. m-n+1})"
      then obtain io where "io  (Π  (λi . π @ (τ i)) ` {1 .. m-n+1})" and "q = after_initial I io"
        by blast
      then have "io  L I"
        using  i . i  m-n+1  π @ (τ i)  L M  L I Π  L I by auto
      then show "q  states I"
        unfolding q = after_initial I io 
        using observable_after_path[OF observable I, of io "initial I"] path_target_is_state[of I "initial I"]
        by metis 
    qed
    then have "card (after_initial I ` (Π  (λi . π @ (τ i)) ` {1 .. m-n+1}))  m"
      using size I  m fsm_states_finite[of I] unfolding FSM.size_def
      by (meson card_mono le_trans) 
    moreover have "card (Π  (λi . π @ (τ i)) ` {1 .. m-n+1}) = m+1"
    proof -
      have *: "card Π = n"
        using state_cover_assignment_card[OF is_state_cover_assignment M V observable M] unfolding Π n .
      have **: "card ((λi . π @ (τ i)) ` {1 .. m-n+1}) = m-n+1"
      proof -
        have "finite ((λi . π @ (τ i)) ` {1 .. m-n+1})"
          by auto
        moreover have "inj_on (λi . π @ (τ i)) {1 .. m-n+1}" 
        proof 
          fix x y assume "x  {1..m - n + 1}" "y  {1..m - n + 1}" "π @ τ x = π @ τ y"

          then have "take x τ' = take y τ'"
            unfolding τ_def length τ' > m - n + 1
            by (metis (no_types, lifting) m - n + 1 < length τ' atLeastAtMost_iff diff_is_0_eq le_trans nat_less_le same_append_eq take_butlast zero_less_diff)
          moreover have "x  length τ'"
            using x  {1..m - n + 1} length τ' > m - n + 1 by auto
          moreover have "y  length τ'"
            using y  {1..m - n + 1} length τ' > m - n + 1 by auto
          ultimately show "x=y"
            by (metis length_take min.absorb2) 
        qed
        moreover have "card {1..m - n + 1} = m - n + 1"
          by auto
        ultimately show ?thesis
          by (simp add: card_image) 
      qed

      have ***: "n + (m - n + 1) = m+1"
        unfolding n using m  size_r M by auto

      have "finite Π"
        unfolding Π using fsm_states_finite restrict_to_reachable_states_simps(2)
        by (metis finite_imageI) 
      have "finite ((λi . π @ (τ i)) ` {1 .. m-n+1})"
        by auto
      
      show ?thesis
        using card_Un_disjoint[OF finite Π finite ((λi. π @ τ i) ` {1..m - n + 1}) Π  (λi . π @ (τ i)) ` {1 .. m-n+1} = {}]
        unfolding * ** *** .
    qed
    ultimately have *: "card (after_initial I ` (Π  (λi . π @ (τ i)) ` {1 .. m-n+1})) < card (Π  (λi . π @ (τ i)) ` {1 .. m-n+1})"
      by simp
    
    show ?thesis
      using pigeonhole[OF *] unfolding inj_on_def by blast
  qed

  (* covered converging traces in I must also converge in M *)
  have same_targets_in_M: " α β . 
                    α  Π  (λi . π @ (τ i)) ` {1 .. m-n+1} 
                    β  Π  (λi . π @ (τ i)) ` {1 .. m-n+1} 
                    α  β  
                    (after_initial I α = after_initial I β) 
                    (after_initial M α = after_initial M β)"
  proof (rule ccontr)
    fix α β assume "α  Π  (λi . π @ (τ i)) ` {1 .. m-n+1}"
               and "β  Π  (λi . π @ (τ i)) ` {1 .. m-n+1}"
               and "α  β"
               and "(after_initial I α = after_initial I β)"
               and "(after_initial M α  after_initial M β)"


    have *: "(λi . π @ (τ i)) ` {1 .. m-n+1}  { (V q) @ τ | q τ . q  reachable_states M  τ  𝒳 q}"
      using  i . i > 0  i  m - n + 1  (τ i)  𝒳 q q  reachable_states M π = V q
      by force

    have "α  L M" and "β  L M" and "α  L I" and "β  L I"
      using α  Π  (λi . π @ (τ i)) ` {1 .. m-n+1} 
            β  Π  (λi . π @ (τ i)) ` {1 .. m-n+1}
             i . i  m-n+1  π @ (τ i)  L M  L I 
            Π  L M Π  L I 
      by auto
    then have "¬ converge M α β" and "converge I α β"
      using after_initial M α  after_initial M β 
      using minimal M 
      using after_is_state[OF assms(1) α  L M]
      using after_is_state[OF assms(1) β  L M]
      unfolding converge.simps minimal.simps after_initial I α = after_initial I β by auto
    then have "¬ converge M β α" and "converge I β α"
      using converge_sym by blast+

    
    have split_helper: " (P :: nat  nat  bool) . ( i j . P i j  i  j) = (( i j . P i j  i < j)  ( i j . P i j  i > j))"
    proof 
      show " (P :: nat  nat  bool) . i j. P i j  i  j  (i j. P i j  i < j)  (i j. P i j  j < i)" 
      proof -
        fix P :: "nat  nat  bool" 
        assume "i j. P i j  i  j"
        then obtain i j where "P i j" and "i  j" by auto
        then have "i < j  i > j" by auto
        then show "(i j. P i j  i < j)  (i j. P i j  j < i)" using P i j by auto
      qed
      show " (P :: nat  nat  bool) . (i j. P i j  i < j)  (i j. P i j  j < i)  i j. P i j  i  j" by auto
    qed
    have split_scheme:"( i j . i  {1 .. m-n+1}  j  {1 .. m-n+1}  α = π @ (τ i)  β = π @ (τ j))
          = (( i j . i  {1 .. m-n+1}  j  {1 .. m-n+1}  i < j  α = π @ (τ i)  β = π @ (τ j))
               ( i j . i  {1 .. m-n+1}  j  {1 .. m-n+1}  i > j  α = π @ (τ i)  β = π @ (τ j)))"
      using α  β  
      using split_helper[of "λ i j . i  {1 .. m-n+1}  j  {1 .. m-n+1}  α = π @ (τ i)  β = π @ (τ j)"]
      by blast

    consider "(α  Π  β  Π)" |
             "( i . i  {1 .. m-n+1}  α  Π  β = π @ (τ i))" |
             "( i . i  {1 .. m-n+1}  β  Π  α = π @ (τ i))" |
             "( i j . i  {1 .. m-n+1}  j  {1 .. m-n+1}  i < j  α = π @ (τ i)  β = π @ (τ j))" |
             "( i j . i  {1 .. m-n+1}  j  {1 .. m-n+1}  i > j  α = π @ (τ i)  β = π @ (τ j))"
      using α  Π  (λi . π @ (τ i)) ` {1 .. m-n+1}
            β  Π  (λi . π @ (τ i)) ` {1 .. m-n+1}
      using split_scheme 
      by blast

    then have " α' β' . α'  L M  β'  L M  ¬converge M α' β'  converge I α' β' 
            ( (α'  Π  β'  Π) 
               ( i . i  {1 .. m-n+1}  α'  Π  β' = π @ (τ i))
               ( i j . i < j  i  {1 .. m-n+1}  j  {1 .. m-n+1}  α' = π @ (τ i)  β' = π @ (τ j)))"
      using α  L M β  L M ¬ converge M α β converge I α β ¬ converge M β α converge I β α 
      by metis

    then obtain α' β' where "α'  L M" and "β'  L M" and "¬converge M α' β'" and "converge I α' β' "
                        and "(α'  Π  β'  Π) 
                               ( i . i  {1 .. m-n+1}  α'  Π  β' = π @ (τ i))
                               ( i j . i < j  i  {1 .. m-n+1}  j  {1 .. m-n+1}  α' = π @ (τ i)  β' = π @ (τ j))"
      by blast
    then consider "α'  Π  β'  Π"
      | " i . i  {1 .. m-n+1}  α'  Π  β' = π @ (τ i)"
      | " i j . i < j  i  {1 .. m-n+1}  j  {1 .. m-n+1}  α' = π @ (τ i)  β' = π @ (τ j)"
      by blast

    then show False proof cases
      case 1
      moreover have "preserves_divergence M I Π"
        using dist_prop[OF reachable_states_initial, of "[]"] language_contains_empty_sequence[of M] by auto
      ultimately show ?thesis 
        using ¬converge M α' β' converge I α' β' α'  L M β'  L M
        unfolding preserves_divergence.simps 
        by blast
    next
      case 2
      then obtain i where "i  {1 .. m-n+1}" and "α'  Π" and "β' = π @ (τ i)"
        by blast
      then have "τ i  𝒳 q" 
        using  i . i > 0  i  m - n + 1  (τ i)  𝒳 q
        by force 

      have "β'  {V q @ ω' |ω'. ω'  list.set (prefixes (τ i))}"
        unfolding β' = π @ (τ i) π = V q prefixes_set by auto 
      then have "¬converge I α' β'"
        using α'  Π ¬converge M α' β' α'  L M β'  L M
        using dist_prop_𝒳[OF q  reachable_states M τ i  𝒳 q]
        unfolding preserves_divergence.simps by blast
      then show False
        using converge I α' β' by blast
    next
      case 3
      then obtain i j where "i  {1 .. m-n+1}" and "j  {1 .. m-n+1}" and "α' = π @ (τ i)" and "β' = π @ (τ j)" and "i < j" by blast
      then have "τ j  𝒳 q" 
        using  i . i > 0  i  m - n + 1  (τ i)  𝒳 q
        by force 

      have "(τ i) = take i (τ j)"
        using i < j unfolding τ_def
        by simp
      then have "(τ i)  list.set (prefixes (τ j))"
        unfolding prefixes_set
        by (metis (mono_tags) append_take_drop_id mem_Collect_eq)
      then have "α'  {V q @ ω' |ω'. ω'  list.set (prefixes (τ j))}"
        unfolding α' = π @ (τ i) π = V q
        by simp
      moreover have "β'  {V q @ ω' |ω'. ω'  list.set (prefixes (τ j))}"
        unfolding β' = π @ (τ j) π = V q prefixes_set by auto 
      ultimately have "¬converge I α' β'"
        using ¬converge M α' β' α'  L M β'  L M
        using dist_prop_𝒳[OF q  reachable_states M τ j  𝒳 q]
        unfolding preserves_divergence.simps by blast
      then show False
        using converge I α' β' by blast
    qed
  qed


  have case_helper: " A B P . ( x y . P x y = P y x)  
                                ( x y . x  A  B  y  A  B  P x y) =
                                          (( x y . x  A  y  A  P x y)
                                             ( x y . x  A  y  B  P x y)
                                             ( x y . x  B  y  B  P x y))"
    by auto
  have *: "(x y. (x  y  FSM.after I (FSM.initial I) x = FSM.after I (FSM.initial I) y) =
          (y  x  FSM.after I (FSM.initial I) y = FSM.after I (FSM.initial I) x))"
    by auto
    
  consider (a) " α β . α  Π  β  Π  α  β  (after_initial I α = after_initial I β)" | 
           (b) " α β . α  Π  β  (λi . π @ (τ i)) ` {1 .. m-n+1}  α  β  (after_initial I α = after_initial I β)" |
           (c) " α β . α  (λi . π @ (τ i)) ` {1 .. m-n+1}  β  (λi . π @ (τ i)) ` {1 .. m-n+1}  α  β  (after_initial I α = after_initial I β)" 
    using same_targets_in_I
    unfolding case_helper[of "λ x y . x  y  (after_initial I x = after_initial I y)" Π "(λi . π @ (τ i)) ` {1 .. m-n+1}", OF *] 
    by blast
  then show "False" proof cases
    case a (* elements of the state cover cannot coincide *)
    then obtain α β  where "α  Π" and "β  Π" and "α  β" and "(after_initial I α = after_initial I β)" by blast
    then have "(after_initial M α = after_initial M β)"
      using same_targets_in_M by blast

    obtain q1 q2 where "q1  reachable_states M" and "α = V q1"
                   and "q2  reachable_states M" and "β = V q2"
      using α  Π β  Π α  β
      unfolding Π by blast
    then have "q1  q2"
      using α  β by auto

    have "α  L M" 
      using Π  L M α  Π by blast
    have "q1 = after_initial M α"
      using is_state_cover_assignment M V q1  reachable_states M observable_io_targets[OF observable M α  L M] 
      unfolding is_state_cover_assignment.simps α = V q1
      by (metis is_state_cover_assignment M V assms(1) is_state_cover_assignment_observable_after)

    have "β  L M" 
      using Π  L M β  Π by blast
    have "q2 = after_initial M β"
      using is_state_cover_assignment M V q2  reachable_states M observable_io_targets[OF observable M β  L M] 
      unfolding is_state_cover_assignment.simps β = V q2
      by (metis is_state_cover_assignment M V assms(1) is_state_cover_assignment_observable_after)

    show "False"
      using q1  q2 (after_initial M α = after_initial M β)
      unfolding q1 = after_initial M α q2 = after_initial M β 
      by simp
  next
    case b (* state cover and π@(τ i) cannot coincide due to minimality of π@τ' *)
    then obtain α β where "α  Π"
                      and "β  (λi. π @ τ i) ` {1..m - n + 1}"
                      and "α  β" 
                      and "FSM.after I (FSM.initial I) α = FSM.after I (FSM.initial I) β"
      by blast
    then have "FSM.after M (FSM.initial M) α = FSM.after M (FSM.initial M) β"
      using same_targets_in_M by blast

    obtain i where "β = π@(τ i)" and "i  {1..m - n + 1}"
      using β  (λi. π @ τ i) ` {1..m - n + 1} by auto

    have "α  L M" and "α  L I" 
      using Π  L M  Π  L I α  Π by blast+
    have "β  L M" and "β  L I" 
      using β  (λi. π @ τ i) ` {1..m - n + 1}  i . i  m-n+1  π @ (τ i)  L M  L I 
      by auto

    let ?io = "drop i τ'"

    have "τ' = (τ i) @ ?io"
      using i  {1..m - n + 1} length τ' > m-n+1 
      unfolding τ_def
      by (metis (no_types, lifting) antisym_conv append_take_drop_id atLeastAtMost_iff less_or_eq_imp_le linorder_neqE_nat order.trans take_butlast)
    then have "β@?io  (L M - L I)  (L I - L M)"
      using β = π@(τ i)  π @ τ'  (L M - L I)  (L I - L M)
      by auto
    then have "α@?io  (L M - L I)  (L I - L M)"
      using observable_after_eq[OF observable M FSM.after M (FSM.initial M) α = FSM.after M (FSM.initial M) β α  L M β  L M]
            observable_after_eq[OF observable I FSM.after I (FSM.initial I) α = FSM.after I (FSM.initial I) β α  L I β  L I]
      by blast
    then show "False"
      using τ'_min[OF α  Π, of ?io] length τ' > m - n + 1 i  {1..m - n + 1}
      by (metis One_nat_def add_diff_cancel_left' atLeastAtMost_iff diff_diff_cancel diff_is_0_eq' length_drop less_Suc_eq nat_le_linear not_add_less2)
  next
    case c (* π@(τ i) and π@(τ j) cannot coincide due to minimality of π@τ' *)
    then have " i j  . i  j  i  {1..m - n + 1}  j  {1..m - n + 1}  (after_initial I (π@(τ i)) = after_initial I (π@(τ j)))"
      by force
    then have " i j  . i < j  i  {1..m - n + 1}  j  {1..m - n + 1}  (after_initial I (π@(τ i)) = after_initial I (π@(τ j)))"
      by (metis linorder_neqE_nat)
    then obtain i j  where "i  {1..m - n + 1}"
                       and "j  {1..m - n + 1}"
                       and "i < j"
                       and "FSM.after I (FSM.initial I) (π@(τ i)) = FSM.after I (FSM.initial I) (π@(τ j))"
      by force

    have "(π@(τ i))  (λi. π @ τ i) ` {1..m - n + 1}" and "(π@(τ j))  (λi. π @ τ i) ` {1..m - n + 1}"
      using i  {1..m - n + 1} j  {1..m - n + 1}
      by auto
    moreover have "(π@(τ i))  (π@(τ j))"
    proof -
      have "j  length (butlast τ')"
        using j  {1..m - n + 1} length τ' > m - n + 1 by auto
      moreover have " xs . j  length xs  i < j  take j xs  take i xs"
        by (metis dual_order.strict_implies_not_eq length_take min.absorb2 min_less_iff_conj)
      ultimately show ?thesis
        using i < j unfolding τ_def
        by fastforce 
    qed
    ultimately have "FSM.after M (FSM.initial M) (π@(τ i)) = FSM.after M (FSM.initial M) (π@(τ j))"
      using FSM.after I (FSM.initial I) (π@(τ i)) = FSM.after I (FSM.initial I) (π@(τ j))
            same_targets_in_M 
      by blast

    have "(π@(τ i))  L M" and "(π@(τ i))  L I" and "(π@(τ j))  L M" and "(π@(τ j))  L I" 
      using  i . i  m-n+1  π @ (τ i)  L M  L I i  {1..m - n + 1} j  {1..m - n + 1} 
      by auto

    let ?io = "drop j τ'"
    have "τ' = (τ j) @ ?io"
      using j  {1..m - n + 1} length τ' > m-n+1 
      unfolding τ_def
      by (metis (no_types, lifting) antisym_conv append_take_drop_id atLeastAtMost_iff less_or_eq_imp_le linorder_neqE_nat order.trans take_butlast)
    then have "(π@(τ j))@?io  (L M - L I)  (L I - L M)"
      using π @ τ'  (L M - L I)  (L I - L M)
      by (simp add: τ_def)
    then have "(π@(τ i))@?io  (L M - L I)  (L I - L M)"
      using observable_after_eq[OF observable M FSM.after M (FSM.initial M) (π@(τ i)) = FSM.after M (FSM.initial M) (π@(τ j)) (π@(τ i))  L M (π@(τ j))  L M]
            observable_after_eq[OF observable I FSM.after I (FSM.initial I) (π@(τ i)) = FSM.after I (FSM.initial I) (π@(τ j)) (π@(τ i))  L I (π@(τ j))  L I]
      by blast
    then have "π@(τ i)@?io  (L M - L I)  (L I - L M)"
      by auto
    moreover have "length τ' > length (τ i @ drop j τ')"
      using length τ' > m - n + 1 j  {1..m - n + 1} i < j unfolding τ_def by force
    ultimately show "False"
      using τ'_min[OF π  Π, of "(τ i) @ ?io"] 
      by simp
  qed
qed



lemma abstract_h_condition_soundness :
  assumes "observable M"
  and     "observable I"
  and     "is_state_cover_assignment M V"
  and     "L M = L I"
shows "satisfies_abstract_h_condition M I V m"
  using assms(3,4) equivalence_preserves_divergence[OF assms(1,2,4)]
  unfolding satisfies_abstract_h_condition_def Let_def by blast
  


lemma abstract_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     "is_state_cover_assignment M V"
shows "satisfies_abstract_h_condition M I V m  (L M = L I)"
  using abstract_h_condition_soundness[OF assms(1,2,8)]
  using abstract_h_condition_exhaustiveness[OF assms]
  by blast


    
subsection ‹Definition of the Framework›


definition h_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm  
                              (('a,'b,'c) fsm  ('a,'b,'c) state_cover_assignment)                         
                              (('a,'b,'c) fsm  ('a,'b,'c) state_cover_assignment  (('a,'b,'c) fsm  ('b×'c) prefix_tree  'd)  ('d  ('b×'c) list  'd)  ('d  ('b×'c) list  ('b×'c) list list)  (('b×'c) prefix_tree × 'd)) 
                              (('a,'b,'c) fsm  ('a,'b,'c) state_cover_assignment  ('a,'b,'c) transition list  ('a,'b,'c) transition list)                               
                              (('a,'b,'c) fsm  ('a,'b,'c) state_cover_assignment  ('b×'c) prefix_tree  'd  ('d  ('b×'c) list  'd)  ('d  ('b×'c) list  ('b×'c) list list)  ('d  ('b×'c) list  ('b×'c) list  'd)  nat  ('a,'b,'c) transition   ('a,'b,'c) transition list  ( ('a,'b,'c) transition list × ('b×'c) prefix_tree × 'd))  
                              (('a,'b,'c) fsm  ('a,'b,'c) state_cover_assignment  ('b×'c) prefix_tree  'd  ('d  ('b×'c) list  'd)  ('d  ('b×'c) list  ('b×'c) list list)  'a  'b  'c  (('b×'c) prefix_tree) × 'd)  
                              (('a,'b,'c) fsm  ('b×'c) prefix_tree  'd) 
                              ('d  ('b×'c) list  'd) 
                              ('d  ('b×'c) list  ('b×'c) list list) 
                              ('d  ('b×'c) list  ('b×'c) list  'd) 
                              nat 
                              ('b×'c) prefix_tree" 
  where
  "h_framework M 
               get_state_cover 
               handle_state_cover
               sort_transitions
               handle_unverified_transition
               handle_unverified_io_pair
               cg_initial
               cg_insert
               cg_lookup
               cg_merge
               m
  = (let
      rstates_set = reachable_states M;
      rstates     = reachable_states_as_list M;
      rstates_io  = List.product rstates (List.product (inputs_as_list M) (outputs_as_list M));
      undefined_io_pairs = List.filter (λ (q,(x,y)) . h_obs M q x y = None) rstates_io;
      V           = get_state_cover M;
      TG1         = handle_state_cover M V cg_initial cg_insert cg_lookup;
      sc_covered_transitions = ( q  rstates_set . covered_transitions M V (V q));
      unverified_transitions = sort_transitions M V (filter (λt . t_source t  rstates_set  t  sc_covered_transitions) (transitions_as_list M));
      verify_transition = (λ (X,T,G) t . handle_unverified_transition M V T G cg_insert cg_lookup cg_merge m t X);
      TG2         = snd (foldl verify_transition (unverified_transitions, TG1) unverified_transitions);
      verify_undefined_io_pair = (λ T (q,(x,y)) . fst (handle_unverified_io_pair M V T (snd TG2) cg_insert cg_lookup q x y))
    in
      foldl verify_undefined_io_pair (fst TG2) undefined_io_pairs)"


subsection ‹Required Conditions on Procedural Parameters›

definition separates_state_cover :: "(('a::linorder,'b::linorder,'c::linorder) fsm  ('a,'b,'c) state_cover_assignment  (('a,'b,'c) fsm  ('b×'c) prefix_tree  'd)  ('d  ('b×'c) list  'd)  ('d  ('b×'c) list  ('b×'c) list list)  (('b×'c) prefix_tree × 'd)) 
                                  ('a,'b,'c) fsm 
                                  ('e,'b,'c) fsm 
                                  (('a,'b,'c) fsm  ('b×'c) prefix_tree  'd) 
                                  ('d  ('b×'c) list  'd) 
                                  ('d  ('b×'c) list  ('b×'c) list list)  
                                  bool"
  where 
  "separates_state_cover f M1 M2 cg_initial cg_insert cg_lookup = 
    ( V .
        (V ` reachable_states M1  set (fst (f M1 V cg_initial cg_insert cg_lookup)))
         finite_tree (fst (f M1 V cg_initial cg_insert cg_lookup))
         (observable M1 
            observable M2 
            minimal M1 
            minimal M2 
            inputs M2 = inputs M1 
            outputs M2 = outputs M1 
            is_state_cover_assignment M1 V 
            convergence_graph_insert_invar M1 M2 cg_lookup cg_insert 
            convergence_graph_initial_invar M1 M2 cg_lookup cg_initial 
            L M1  set (fst (f M1 V cg_initial cg_insert cg_lookup)) = L M2  set (fst (f M1 V cg_initial cg_insert cg_lookup)) 
            (preserves_divergence M1 M2 (V ` reachable_states M1)
             convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V cg_initial cg_insert cg_lookup)))))"


definition handles_transition :: "(('a::linorder,'b::linorder,'c::linorder) fsm 
                                    ('a,'b,'c) state_cover_assignment 
                                    ('b×'c) prefix_tree  
                                    'd 
                                    ('d  ('b×'c) list  'd) 
                                    ('d  ('b×'c) list  ('b×'c) list list) 
                                    ('d  ('b×'c) list  ('b×'c) list  'd)  
                                    nat 
                                    ('a,'b,'c) transition  
                                    ('a,'b,'c) transition list    
                                    (('a,'b,'c) transition list × ('b×'c) prefix_tree × 'd))    
                                  ('a::linorder,'b::linorder,'c::linorder) fsm 
                                  ('e,'b,'c) fsm 
                                  ('a,'b,'c) state_cover_assignment     
                                  ('b×'c) prefix_tree 
                                  ('d  ('b×'c) list  'd) 
                                  ('d  ('b×'c) list  ('b×'c) list list)  
                                  ('d  ('b×'c) list  ('b×'c) list  'd) 
                                  bool"
  where 
  "handles_transition f M1 M2 V T0 cg_insert cg_lookup cg_merge = 
    ( T G m t X .
        (set T  set (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))))
         (finite_tree T  finite_tree (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))))
         (observable M1 
            observable M2 
            minimal M1 
            minimal M2 
            size_r M1  m 
            size M2  m 
            inputs M2 = inputs M1 
            outputs M2 = outputs M1 
            is_state_cover_assignment M1 V 
            preserves_divergence M1 M2 (V ` reachable_states M1) 
            V ` reachable_states M1  set T 
            t  transitions M1 
            t_source t  reachable_states M1 
            ((V (t_source t)) @ [(t_input t,t_output t)])  (V (t_target t))   
            convergence_graph_lookup_invar M1 M2 cg_lookup G 
            convergence_graph_insert_invar M1 M2 cg_lookup cg_insert 
            convergence_graph_merge_invar M1 M2 cg_lookup cg_merge 
            L M1  set (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))) = L M2  set (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))) 
            (set T0  set T) 
            ( γ . (length γ  (m-size_r M1)  list.set γ  inputs M1 × outputs M1  butlast γ  LS M1 (t_target t))
                     ((L M1  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)})
                          = L M2  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))
                          preserves_divergence M1 M2 (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)})))   
             convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X)))))"


definition handles_io_pair :: "(('a::linorder,'b::linorder,'c::linorder) fsm 
                                            ('a,'b,'c) state_cover_assignment 
                                            ('b×'c) prefix_tree  
                                            'd 
                                            ('d  ('b×'c) list  'd)  
                                            ('d  ('b×'c) list  ('b×'c) list list)  
                                            'a  'b  'c   
                                            (('b×'c) prefix_tree × 'd)) 
                                          ('a::linorder,'b::linorder,'c::linorder) fsm 
                                          ('e,'b,'c) fsm 
                                          ('d  ('b×'c) list  'd) 
                                          ('d  ('b×'c) list  ('b×'c) list list)                                      
                                          bool"
  where 
  "handles_io_pair f M1 M2 cg_insert cg_lookup = 
    ( V T G q x y .
        (set T  set (fst (f M1 V T G cg_insert cg_lookup q x y)))
         (finite_tree T  finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y)))
         (observable M1 
            observable M2 
            minimal M1 
            minimal M2 
            inputs M2 = inputs M1 
            outputs M2 = outputs M1 
            is_state_cover_assignment M1 V 
            L M1  (V ` reachable_states M1) = L M2  V ` reachable_states M1 
            q  reachable_states M1 
            x  inputs M1  
            y  outputs M1  
            convergence_graph_lookup_invar M1 M2 cg_lookup G    
            convergence_graph_insert_invar M1 M2 cg_lookup cg_insert 
            L M1  set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2  set (fst (f M1 V T G cg_insert cg_lookup q x y)) 
            ( L M1  {(V q)@[(x,y)]} = L M2  {(V q)@[(x,y)]} )
             convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))))"



subsection ‹Completeness and Finiteness of the Scheme›


lemma unverified_transitions_handle_all_transitions :
  assumes "observable M1"
  and     "is_state_cover_assignment M1 V"
  and     "L M1  V ` reachable_states M1 = L M2  V ` reachable_states M1"
  and     "preserves_divergence M1 M2 (V ` reachable_states M1)"
  and     handles_unverified_transitions: " t γ . t  transitions M1 
                                            t_source t  reachable_states M1 
                                            length γ  k  
                                            list.set γ  inputs M1 × outputs M1  
                                            butlast γ  LS M1 (t_target t) 
                                            (V (t_target t)  (V (t_source t))@[(t_input t, t_output t)]) 
                                            ((L M1  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)})
                                               = L M2  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))
                                              preserves_divergence M1 M2 (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))"
  and     handles_undefined_io_pairs: " q x y . q  reachable_states M1  x  inputs M1  y  outputs M1  h_obs M1 q x y = None  L M1  {V q @ [(x,y)]} = L M2  {V q @ [(x,y)]}"
  and     "t  transitions M1"
  and     "t_source t  reachable_states M1"
  and     "length γ  k"
  and     "list.set γ  inputs M1 × outputs M1"
  and     "butlast γ  LS M1 (t_target t)"
shows "(L M1  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)})
         = L M2  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))
         preserves_divergence M1 M2 (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)})"
proof (cases "V (t_target t)  V (t_source t) @ [(t_input t, t_output t)]")
  case True
  then show ?thesis 
    using handles_unverified_transitions[OF assms(7-11)] 
    by blast
next
  case False
  then have "V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)"
    by simp
  have " γ . length γ  k 
             list.set γ  inputs M1 × outputs M1  
             butlast γ  LS M1 (t_target t) 
             L M1  (V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes γ)}) =
               L M2  (V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes γ)}) 
             preserves_divergence M1 M2 (V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes γ)})"
  proof -
    fix γ assume "length γ  k" and "list.set γ  inputs M1 × outputs M1" and "butlast γ  LS M1 (t_target t)"
    then show "L M1  (V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes γ)}) =
                 L M2  (V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes γ)}) 
               preserves_divergence M1 M2 (V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes γ)})"
      using t  transitions M1 t_source t  reachable_states M1 V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)
    proof (induction γ arbitrary: t)
      case Nil
      have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes [])} = {V (t_target t)}"
        unfolding Nil by auto
      then have *: "(V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes [])}) = V ` reachable_states M1"
        using reachable_states_next[OF Nil.prems(5,4)] by blast
      show ?case 
        unfolding *
        using assms(3,4) 
        by blast
    next
      case (Cons xy γ)
      then obtain x y where "xy = (x,y)" by auto
      then have "x  inputs M1" and "y  outputs M1"
        using Cons.prems(2) by auto

      have "t_target t  reachable_states M1"
        using reachable_states_next[OF Cons.prems(5,4)] by blast
      then have "after_initial M1 (V (t_target t)) = t_target t"
        using is_state_cover_assignment M1 V 
        by (metis assms(1) is_state_cover_assignment_observable_after)

      show ?case proof (cases "[xy]  LS M1 (t_target t)")
        case False
        then have "h_obs M1 (t_target t) x y = None"
          using Cons.prems(4,5) x  inputs M1 y  outputs M1 unfolding xy = (x,y)
          by (meson assms(1) h_obs_language_single_transition_iff) 
        then have "L M1  {V (t_target t) @ [(x, y)]} = L M2  {V (t_target t) @ [(x, y)]}"
          using handles_undefined_io_pairs[OF t_target t  reachable_states M1 x  inputs M1 y  outputs M1] by blast      
        
        have "V (t_target t) @ [(x, y)]  L M1"
          using False after_initial M1 (V (t_target t)) = t_target t 
          unfolding xy = (x,y)
          by (metis assms(1) language_prefix observable_after_language_none) 
        then have "preserves_divergence M1 M2 (V ` reachable_states M1  {V (t_target t) @ [(x, y)]})"
          using assms(4)
          unfolding preserves_divergence.simps
          by blast 

        have "γ = []"
          using False Cons.prems(3) 
          by (metis (no_types, lifting) LS_single_transition xy = (x, y) butlast.simps(2) language_next_transition_ob)
        then have "list.set (prefixes (xy#γ)) = {[], [(x,y)]}"
          unfolding xy = (x,y)
          by force 
        then have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes (xy # γ))} = {V (t_target t), V (t_target t) @ [(x, y)]}"
          unfolding Cons by auto
        then have *:"(V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes (xy # γ))}) = (V ` reachable_states M1  {V (t_target t) @ [(x, y)]})"
          using reachable_states_next[OF Cons.prems(5,4)] by blast

        

        show ?thesis 
          unfolding *
          using assms(3)
                L M1  {V (t_target t) @ [(x, y)]} = L M2  {V (t_target t) @ [(x, y)]}
                preserves_divergence M1 M2 (V ` reachable_states M1  {V (t_target t) @ [(x, y)]})    
          by blast
      next
        case True

        then obtain t' where "t_source t' = t_target t" and "t_input t' = x" and "t_output t' = y" and "t'  transitions M1"
          unfolding xy = (x,y)
          by auto 
        then have "t_target t'  reachable_states M1" and "t_source t'  reachable_states M1"
          using reachable_states_next[OF t_target t  reachable_states M1, of t'] t_target t  reachable_states M1 by auto

        have *: "length γ  k"
          using Cons.prems(1) by auto
        have **: "list.set γ  inputs M1 × outputs M1"
          using Cons.prems(2) by auto
        have ***: "butlast γ  LS M1 (t_target t')"
          using Cons.prems(3)
          by (metis True t'  FSM.transitions M1 t_input t' = x t_output t' = y t_source t' = t_target t xy = (x, y) assms(1) butlast.simps(1) butlast.simps(2) observable_language_transition_target)                
        
        have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes (xy # γ))} = {((V (t_source t) @ [(t_input t, t_output t)]) @ [xy]) @ ω' |ω'. ω'  list.set (prefixes γ)}  {V (t_source t) @ [(t_input t, t_output t)]}"
          by (induction γ; auto) 
        moreover have "{((V (t_source t) @ [(t_input t, t_output t)]) @ [xy]) @ ω' |ω'. ω'  list.set (prefixes γ)} = {(V (t_source t') @ [(t_input t', t_output t')]) @ ω' |ω'. ω'  list.set (prefixes γ)}"
          unfolding t_source t' = t_target t t_input t' = x t_output t' = y xy = (x,y)[symmetric] Cons.prems(6)[symmetric] by simp
        ultimately have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes (xy # γ))} = {(V (t_source t') @ [(t_input t', t_output t')]) @ ω' |ω'. ω'  list.set (prefixes γ)}  {V (t_target t)}"
          unfolding Cons by force
        then have ****: "V ` reachable_states M1  {(V (t_source t') @ [(t_input t', t_output t')]) @ ω' |ω'. ω'  list.set (prefixes γ)}
                          = V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes (xy # γ))}"
          using t_source t' = t_target t t_source t'  reachable_states M1 by force

      

        show ?thesis proof (cases "V (t_source t') @ [(t_input t', t_output t')] = V (t_target t')")
          case True
          show ?thesis
            using Cons.IH[OF * ** *** t'  transitions M1 t_source t'  reachable_states M1 True]
            unfolding **** .
        next
          case False
          then show ?thesis
            using handles_unverified_transitions[OF t'  transitions M1 t_source t'  reachable_states M1 * ** ***]
            unfolding ****
            by presburger
        qed
      qed
    qed
  qed
  then show ?thesis
    using assms(9-11)
    by blast
qed

lemma abstract_h_condition_by_transition_and_io_pair_coverage :
  assumes "observable M1"
  and     "is_state_cover_assignment M1 V"
  and     "L M1  V ` reachable_states M1 = L M2  V ` reachable_states M1"
  and     "preserves_divergence M1 M2 (V ` reachable_states M1)"
  and     handles_unverified_transitions: " t γ . t  transitions M1 
                                            t_source t  reachable_states M1 
                                            length γ  k  
                                            list.set γ  inputs M1 × outputs M1  
                                            butlast γ  LS M1 (t_target t) 
                                            ((L M1  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)})
                                               = L M2  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))
                                              preserves_divergence M1 M2 (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))"
  and     handles_undefined_io_pairs: " q x y . q  reachable_states M1  x  inputs M1  y  outputs M1  h_obs M1 q x y = None  L M1  {V q @ [(x,y)]} = L M2  {V q @ [(x,y)]}"  
  and     "q  reachable_states M1"
  and     "length γ  Suc k"
  and     "list.set γ  inputs M1 × outputs M1"
  and     "butlast γ  LS M1 q"
shows "(L M1  (V ` reachable_states M1  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})
         = L M2  (V ` reachable_states M1  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))
         preserves_divergence M1 M2 (V ` reachable_states M1  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})"   
proof (cases γ)
  case Nil 
  show ?thesis 
    using assms(3,4,7) unfolding Nil by auto
next
  case (Cons xy γ')
  then obtain x y where "xy = (x,y)" using prod.exhaust by metis
  then have "x  inputs M1" and "y  outputs M1"
    using assms(9) Cons by auto

  show ?thesis proof (cases "[xy]  LS M1 q")
    case False
    then have "h_obs M1 q x y = None"
      using assms(7) x  inputs M1 y  outputs M1 unfolding xy = (x,y)
      by (meson assms(1) h_obs_language_single_transition_iff) 
    then have "L M1  {V q @ [(x,y)]} = L M2  {V q @ [(x,y)]}"
      using handles_undefined_io_pairs[OF assms(7) x  inputs M1 y  outputs M1] by blast

    have "V q @ [(x, y)]  L M1"
      using observable_after_language_none[OF assms(1), of "V q" "initial M1" "[(x,y)]"]
      using state_cover_assignment_after[OF assms(1,2,7)]
      by (metis False xy = (x, y)) 
    then have "preserves_divergence M1 M2 (V ` reachable_states M1  {V q @ [(x, y)]})"
      using assms(4)
      unfolding preserves_divergence.simps
      by blast 


    have "γ' = []"
      using False assms(10) language_prefix[of "[xy]" γ' M1 q]
      unfolding Cons 
      by (metis (no_types, lifting) LS_single_transition xy = (x, y) butlast.simps(2) language_next_transition_ob)
    then have "γ = [(x,y)]"
      unfolding Cons xy = (x,y) by auto
    then have *: "(V ` reachable_states M1  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}) = V ` reachable_states M1  {V q @ [(x,y)]}"
      using assms(7) by auto

    show ?thesis
      unfolding *
      using assms(3) L M1  {V q @ [(x,y)]} = L M2  {V q @ [(x,y)]} preserves_divergence M1 M2 (V ` reachable_states M1  {V q @ [(x, y)]})
      by blast
  next
    case True
    moreover have "butlast ((x,y)#γ')  LS M1 q"
      using assms(10) unfolding Cons xy = (x,y) .
    ultimately have "(x,y) # (butlast γ')  LS M1 q" 
      unfolding  xy = (x,y) by (cases γ'; auto)
    then obtain q' where "h_obs M1 q x y = Some q'" and "butlast γ'  LS M1 q'"
      using h_obs_language_iff[OF assms(1), of x y "butlast γ'" q]
      by blast
    then have "(q,x,y,q')  transitions M1"
      unfolding h_obs_Some[OF assms(1)] by blast

    

    have "length γ'  k"
      using assms(8) unfolding Cons by auto
    have "list.set γ'  inputs M1 × outputs M1"    
      using assms(9) unfolding Cons by auto
    
    have *:"(L M1  (V ` reachable_states M1  {(V q @ [(x,y)]) @ ω' | ω'. ω'  list.set (prefixes γ')})
         = L M2  (V ` reachable_states M1  {(V q @ [(x,y)]) @ ω' | ω'. ω'  list.set (prefixes γ')}))
         preserves_divergence M1 M2 (V ` reachable_states M1  {(V q @ [(x,y)]) @ ω' | ω'. ω'  list.set (prefixes γ')})"
      using handles_unverified_transitions[OF (q,x,y,q')  transitions M1 _ length γ'  k list.set γ'  inputs M1 × outputs M1]
            assms(7) butlast γ'  LS M1 q'
      unfolding fst_conv snd_conv 
      by blast

    have "{V q @ ω' |ω'. ω'  list.set (prefixes γ)} = {(V q @ [(x, y)]) @ ω' |ω'. ω'  list.set (prefixes γ')}  {V q}"
      unfolding Cons xy = (x,y) by auto 
    then have **: "V ` reachable_states M1  {V q @ ω' |ω'. ω'  list.set (prefixes γ)} 
                    = V ` reachable_states M1  {(V q @ [(x, y)]) @ ω' |ω'. ω'  list.set (prefixes γ')}"
      using assms(7) by blast

    show ?thesis
      using * unfolding ** .
  qed
qed


lemma abstract_h_condition_by_unverified_transition_and_io_pair_coverage :
  assumes "observable M1"
  and     "is_state_cover_assignment M1 V"
  and     "L M1  V ` reachable_states M1 = L M2  V ` reachable_states M1"
  and     "preserves_divergence M1 M2 (V ` reachable_states M1)"
  and     handles_unverified_transitions: " t γ . t  transitions M1 
                                            t_source t  reachable_states M1 
                                            length γ  k  
                                            list.set γ  inputs M1 × outputs M1  
                                            butlast γ  LS M1 (t_target t) 
                                            (V (t_target t)  (V (t_source t))@[(t_input t, t_output t)])  
                                            ((L M1  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)})
                                               = L M2  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))
                                              preserves_divergence M1 M2 (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))"
  and     handles_undefined_io_pairs: " q x y . q  reachable_states M1  x  inputs M1  y  outputs M1  h_obs M1 q x y = None  L M1  {V q @ [(x,y)]} = L M2  {V q @ [(x,y)]}"  
  and     "q  reachable_states M1"
  and     "length γ  Suc k"
  and     "list.set γ  inputs M1 × outputs M1"
  and     "butlast γ  LS M1 q"
shows "(L M1  (V ` reachable_states M1  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})
         = L M2  (V ` reachable_states M1  {V q @ ω' | ω'. ω'  list.set (prefixes γ)}))
         preserves_divergence M1 M2 (V ` reachable_states M1  {V q @ ω' | ω'. ω'  list.set (prefixes γ)})"   
  using unverified_transitions_handle_all_transitions[OF assms(1-6), of k]
  using abstract_h_condition_by_transition_and_io_pair_coverage[OF assms(1-4) _ assms(6-10)]
  by presburger


lemma h_framework_completeness_and_finiteness :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('e,'b,'c) fsm"
  fixes cg_insert :: "('d  ('b×'c) list  'd)"
  assumes "observable M1"
  and     "observable M2"
  and     "minimal M1"
  and     "minimal M2"
  and     "size_r M1  m"
  and     "size M2  m"
  and     "inputs M2 = inputs M1"
  and     "outputs M2 = outputs M1"
  and     "is_state_cover_assignment M1 (get_state_cover M1)"
  and     " xs . List.set xs = List.set (sort_transitions M1 (get_state_cover M1) xs)"
  and     "convergence_graph_initial_invar M1 M2 cg_lookup cg_initial"
  and     "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
  and     "convergence_graph_merge_invar M1 M2 cg_lookup cg_merge"
  and     "separates_state_cover handle_state_cover M1 M2 cg_initial cg_insert cg_lookup"
  and     "handles_transition handle_unverified_transition M1 M2 (get_state_cover M1) (fst (handle_state_cover M1 (get_state_cover M1) cg_initial cg_insert cg_lookup)) cg_insert cg_lookup cg_merge"
  and     "handles_io_pair handle_unverified_io_pair M1 M2 cg_insert cg_lookup"
shows "(L M1 = L M2)  ((L M1  set (h_framework M1 get_state_cover handle_state_cover sort_transitions handle_unverified_transition handle_unverified_io_pair cg_initial cg_insert cg_lookup cg_merge m))
                          = (L M2  set (h_framework M1 get_state_cover handle_state_cover sort_transitions handle_unverified_transition handle_unverified_io_pair cg_initial cg_insert cg_lookup cg_merge m)))"
  (is "(L M1 = L M2)  ((L M1  set ?TS) = (L M2  set ?TS))")
and "finite_tree (h_framework M1 get_state_cover handle_state_cover sort_transitions handle_unverified_transition handle_unverified_io_pair cg_initial cg_insert cg_lookup cg_merge m)"
proof 
  show "(L M1 = L M2)  ((L M1  set ?TS) = (L M2  set ?TS))"
    by blast


  define rstates where rstates: "rstates = reachable_states_as_list M1"
  define rstates_io where rstates_io: "rstates_io = List.product rstates (List.product (inputs_as_list M1) (outputs_as_list M1))"
  define undefined_io_pairs where undefined_io_pairs: "undefined_io_pairs = List.filter (λ (q,(x,y)) . h_obs M1 q x y = None) rstates_io"
  define V where V: "V             = get_state_cover M1"
  define n where n: "n             = size_r M1"
  define TG1 where TG1: "TG1 = handle_state_cover M1 V cg_initial cg_insert cg_lookup"

  define sc_covered_transitions where sc_covered_transitions: "sc_covered_transitions = ( q  reachable_states M1 . covered_transitions M1 V (V q))"
  define unverified_transitions where unverified_transitions: "unverified_transitions = sort_transitions M1 V (filter (λt . t_source t  reachable_states M1  t  sc_covered_transitions) (transitions_as_list M1))"
  define verify_transition where verify_transition: "verify_transition = (λ (X,T,G) t . handle_unverified_transition M1 V T G cg_insert cg_lookup cg_merge m t X)"
  define TG2 where TG2: "TG2 = snd (foldl verify_transition (unverified_transitions, TG1) unverified_transitions)"
  define verify_undefined_io_pair where verify_undefined_io_pair: "verify_undefined_io_pair = (λ T (q,(x,y)) . fst (handle_unverified_io_pair M1 V T (snd TG2) cg_insert cg_lookup q x y))" 
  define T3 where T3: "T3 = foldl verify_undefined_io_pair (fst TG2) undefined_io_pairs"

  have "?TS = T3"
    unfolding rstates rstates_io undefined_io_pairs V TG1 sc_covered_transitions unverified_transitions verify_transition TG2 verify_undefined_io_pair T3
    unfolding h_framework_def Let_def
    by force
  then have "((L M1  set ?TS) = (L M2  set ?TS))  L M1  set T3 = L M2  set T3"
    by simp

  have "is_state_cover_assignment M1 V"
    unfolding V using assms(9) .

  (* basic properties of T1 and G1 *)

  define T1 where T1: "T1 = fst TG1"
  moreover define G1 where G1: "G1 = snd TG1"
  ultimately have "TG1 = (T1,G1)" 
    by auto 

  have T1_state_cover: "V ` reachable_states M1  set T1"
  and  T1_finite: "finite_tree T1"
    using separates_state_cover handle_state_cover M1 M2 cg_initial cg_insert cg_lookup
    unfolding T1 TG1 separates_state_cover_def
    by blast+
  

  have T1_V_div: "(L M1  set T1 = (L M2  set T1))  preserves_divergence M1 M2 (V ` reachable_states M1)"
   and G1_invar: "(L M1  set T1 = (L M2  set T1))  convergence_graph_lookup_invar M1 M2 cg_lookup G1" 
    using separates_state_cover handle_state_cover M1 M2 cg_initial cg_insert cg_lookup
    unfolding T1 G1 TG1 separates_state_cover_def
    using assms(1-4,7,8) is_state_cover_assignment M1 V assms(12,11) 
    by blast+

  

  (* properties of transition filtering and sorting *)

  have sc_covered_transitions_alt_def: "sc_covered_transitions = {t . t  transitions M1  t_source t  reachable_states M1  (V (t_target t) = (V (t_source t))@[(t_input t, t_output t)])}"
    (is "?A = ?B")
  proof 
    show "?A  ?B"
    proof 
      fix t assume "t  ?A"
      then obtain q where "t  covered_transitions M1 V (V q)" and "q  reachable_states M1"
        unfolding sc_covered_transitions 
        by blast
      then have "V q  L M1" and "after_initial M1 (V q) = q"
        using state_cover_assignment_after[OF assms(1) is_state_cover_assignment M1 V]
        by blast+

      then obtain p where "path M1 (initial M1) p" and "p_io p = V q"
        by auto
      then have *: "the_elem (paths_for_io M1 (initial M1) (V q)) = p"
        using observable_paths_for_io[OF assms(1) V q  L M1]
        unfolding paths_for_io_def
        by (metis (mono_tags, lifting) assms(1) mem_Collect_eq observable_path_unique singletonI the_elem_eq)
      
      have "t  list.set p" and "V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)"
        using t  covered_transitions M1 V (V q) 
        unfolding covered_transitions_def Let_def * 
        by auto

      have "t  transitions M1"
        using t  list.set p path M1 (initial M1) p
        by (meson path_transitions subsetD) 
      moreover have "t_source t  reachable_states M1"
        using reachable_states_path[OF reachable_states_initial path M1 (initial M1) p t  list.set p] .
      ultimately show "t  ?B"
        using V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)
        by auto
    qed

    show "?B  ?A"
    proof 
      fix t assume "t  ?B"
      then have "t  transitions M1" 
                "t_source t  reachable_states M1" 
                "(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)"
        by auto
      then have "t_target t  reachable_states M1"
        using reachable_states_next[of "t_source t" M1 t] 
        by blast
      then have "V (t_target t)  L M1" and "after_initial M1 (V (t_target t)) = (t_target t)"
        using state_cover_assignment_after[OF assms(1) is_state_cover_assignment M1 V]
        by blast+
      then obtain p where "path M1 (initial M1) p" and "p_io p = V (t_target t)"
        by auto
      then have *: "the_elem (paths_for_io M1 (initial M1) (V (t_target t))) = p"
        using observable_paths_for_io[OF assms(1) V (t_target t)  L M1]
        unfolding paths_for_io_def
        by (metis (mono_tags, lifting) assms(1) mem_Collect_eq observable_path_unique singletonI the_elem_eq)

      
      have "V (t_source t)  L M1" and "after_initial M1 (V (t_source t)) = (t_source t)"
        using t_source t  reachable_states M1
        using state_cover_assignment_after[OF assms(1) is_state_cover_assignment M1 V]
        by blast+
      then obtain p' where "path M1 (initial M1) p'" and "p_io p' = V (t_source t)"
        by auto
      
      have "path M1 (initial M1) (p'@[t])"
        using after_path[OF assms(1) path M1 (initial M1) p'] path M1 (initial M1) p' ttransitions M1
        unfolding p_io p' = V (t_source t)
        unfolding after_initial M1 (V (t_source t)) = (t_source t)
        by (metis path_append single_transition_path)
      moreover have "p_io (p'@[t]) = p_io p"
        using p_io p' = V (t_source t) 
        unfolding p_io p = V (t_target t)  (V (t_source t))@[(t_input t, t_output t)] = V (t_target t)[symmetric]
        by auto
      ultimately have "p'@[t] = p"
        using observable_path_unique[OF assms(1) _ path M1 (initial M1) p]
        by force
      then have "t  list.set p"
        by auto
      then have "t  covered_transitions M1 V (V (t_target t))"
        using (V (t_source t))@[(t_input t, t_output t)] = V (t_target t)
        unfolding covered_transitions_def Let_def *
        by auto
      then show "t  ?A"
        using t_target t  reachable_states M1
        unfolding sc_covered_transitions 
        by blast
    qed
  qed

  have T1_covered_transitions_conv: " t . (L M1  set T1 = (L M2  set T1))  t  sc_covered_transitions  converge M2 (V (t_target t)) ((V (t_source t))@[(t_input t, t_output t)])"
  proof -
    fix t assume "(L M1  set T1 = (L M2  set T1))"
                 "t  sc_covered_transitions"

    then have "t  transitions M1" 
              "t_source t  reachable_states M1" 
              "(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)"
      unfolding sc_covered_transitions_alt_def
      by auto
    then have "t_target t  reachable_states M1"
      using reachable_states_next[of "t_source t" M1 t] 
      by blast
    then have "V (t_target t)  L M1"
      using state_cover_assignment_after[OF assms(1) is_state_cover_assignment M1 V]
      by blast   
    moreover have "V (t_target t)  set T1"
      using T1_state_cover t_target t  reachable_states M1
      by blast
    ultimately have "V (t_target t)  L M2"
      using (L M1  set T1 = (L M2  set T1))
      by blast
    then show "converge M2 (V (t_target t)) ((V (t_source t))@[(t_input t, t_output t)])"
      unfolding (V (t_source t))@[(t_input t, t_output t)] = V (t_target t)
      by auto
  qed


  have unverified_transitions_alt_def : "list.set unverified_transitions = {t . t  transitions M1  t_source t  reachable_states M1  (V (t_target t)  (V (t_source t))@[(t_input t, t_output t)])}"
    unfolding unverified_transitions sc_covered_transitions_alt_def V
    unfolding assms(10)[symmetric] 
    using transitions_as_list_set[of M1]
    by auto


  (* remaining properties before the computation of TG2 *)

  have cg_insert_invar : " G γ . γ  L M1  γ  L M2  convergence_graph_lookup_invar M1 M2 cg_lookup G  convergence_graph_lookup_invar M1 M2 cg_lookup (cg_insert G γ)"
    using assms(12)
    unfolding convergence_graph_insert_invar_def
    by blast

  have cg_merge_invar : " G γ γ'. convergence_graph_lookup_invar M1 M2 cg_lookup G  converge M1 γ γ'  converge M2 γ γ'  convergence_graph_lookup_invar M1 M2 cg_lookup (cg_merge G γ γ')"
    using assms(13)
    unfolding convergence_graph_merge_invar_def
    by blast


  (* properties of the computation of TG2 *)

  define T2 where T2: "T2 = fst TG2"
  define G2 where G2: "G2 = snd TG2"

  (* idea: in each application of verify_transition, a further transition of unverified_transitions
           (q,x,y,q') is covered - that is
            - traces α.(x/y), β are added to the test suite such that
              - α converges with V s in both M1 and M2
              - β converges with V s' in both M1 and M2
              - α.(x/y) converges with β in both M1 and M2 
            - the test suite is added as required to establish this convergence
            - the convergence graph is updated, respecting the lookup-invariants due to convergence (in merge)
  *)

  have "handles_transition handle_unverified_transition M1 M2 V T1 cg_insert cg_lookup cg_merge"
    using assms(15)
    unfolding T1 TG1 V .
  then have verify_transition_retains_testsuite: " t T G X . set T  set (fst (snd (verify_transition (X,T,G) t)))"
       and  verify_transition_retains_finiteness: " t T G X . finite_tree T  finite_tree (fst (snd (verify_transition (X,T,G) t)))"
    unfolding verify_transition case_prod_conv handles_transition_def 
    by presburger+


  define handles_unverified_transition 
    where handles_unverified_transition: "handles_unverified_transition  = (λt .
                                                ( γ . (length γ  (m-size_r M1)  list.set γ  inputs M1 × outputs M1  butlast γ  LS M1 (t_target t))
                                                           ((L M1  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)})
                                                                = L M2  (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))
                                                                preserves_divergence M1 M2 (V ` reachable_states M1  {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω'  list.set (prefixes γ)}))))"


  have verify_transition_cover_prop: " t T G X . (L M1  (set (fst (snd (verify_transition (X,T,G) t)))) = L M2  (set (fst (snd (verify_transition (X,T,G) t)))))
                                           convergence_graph_lookup_invar M1 M2 cg_lookup G
                                           t  transitions M1
                                           t_source t  reachable_states M1
                                           set T1  set T
                                           ((V (t_source t)) @ [(t_input t,t_output t)])  (V (t_target t))
                                           handles_unverified_transition t  convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (verify_transition (X,T,G) t)))"
  proof -
    fix t T G X
    assume a1: "(L M1  (set (fst (snd (verify_transition (X,T,G) t)))) = L M2  (set (fst (snd (verify_transition (X,T,G) t)))))"
    assume a2: "convergence_graph_lookup_invar M1 M2 cg_lookup G"
    assume a3: "t  transitions M1"
    assume a4: "t_source t  reachable_states M1"
    assume a5: "set T1  set T"
    assume a6: "((V (t_source t)) @ [(t_input t,t_output t)])  (V (t_target t))"

    

    obtain X' T' G' where TG': "(X',T',G') = handle_unverified_transition M1 V T G cg_insert cg_lookup cg_merge m t X"
      using prod.exhaust by metis
    have T':  "T'  = fst (snd (handle_unverified_transition M1 V T G cg_insert cg_lookup cg_merge m t X))"
     and G':  "G'  = snd (snd (handle_unverified_transition M1 V T G cg_insert cg_lookup cg_merge m t X))"
      unfolding TG'[symmetric] by auto

    have "verify_transition (X,T,G) t = (X',T',G')"
      using TG'[symmetric]
      unfolding verify_transition G' Let_def case_prod_conv 
      by force
    then have "set T  set T'"
      using verify_transition_retains_testsuite[of T X G t] unfolding T' 
      by auto
    then have "set T1  set T'"
      using a5 by blast
    then have "(L M1  (set T1) = L M2  (set T1))"
      using a1 unfolding verify_transition (X,T,G) t = (X',T',G') fst_conv snd_conv
      by blast
    then have *: "preserves_divergence M1 M2 (V ` reachable_states M1)"
      using T1_V_div
      by auto

    have "L M1  set T' = L M2  set T'"
      using a1 set T  set T' unfolding T' verify_transition (X,T,G) t = (X',T',G') fst_conv snd_conv
      by blast

    have **: "V ` reachable_states M1  set T"
      using a5 T1_state_cover by blast

    show "handles_unverified_transition t  convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (verify_transition (X,T,G) t)))"
      unfolding verify_transition (X,T,G) t = (X',T',G') snd_conv 
      unfolding G'
      using handles_transition handle_unverified_transition M1 M2 V T1 cg_insert cg_lookup cg_merge
      unfolding handles_transition_def 

      using assms(1-8) is_state_cover_assignment M1 V * ** a3 a4 a2 a6 convergence_graph_insert_invar M1 M2 cg_lookup cg_insert convergence_graph_merge_invar M1 M2 cg_lookup cg_merge L M1  set T' = L M2  set T' a5
      unfolding T'
      unfolding handles_unverified_transition 
      by blast
  qed

  have verify_transition_foldl_invar_1: " X ts . list.set ts  list.set unverified_transitions  
                set T1  set (fst (snd (foldl verify_transition (X, T1, G1) ts)))  finite_tree (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
  proof -
    fix X ts assume "list.set ts  list.set unverified_transitions" 
    then show "set T1  set (fst (snd (foldl verify_transition (X, T1, G1) ts)))  finite_tree (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
    proof (induction ts rule: rev_induct)
      case Nil
      then show ?case 
        using T1_finite by auto
    next
      case (snoc t ts)
      then have "t  transitions M1" and "t_source t  reachable_states M1"
        unfolding unverified_transitions_alt_def 
        by force+

      have p1: "list.set ts  list.set unverified_transitions"
        using snoc.prems(1) by auto

      have "set (fst (snd (foldl verify_transition (X, T1, G1) ts)))  set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using verify_transition_retains_testsuite 
        unfolding foldl_append
        unfolding foldl.simps 
        by (metis prod.collapse) 

      have **: "Prefix_Tree.set T1  Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"  
       and ***: "finite_tree (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
        using snoc.IH[OF p1] 
        by auto          
    
      have "Prefix_Tree.set T1  Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using ** verify_transition_retains_testsuite set (fst (snd (foldl verify_transition (X, T1, G1) ts)))  set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t])))) 
        by auto 
      moreover have "finite_tree (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using verify_transition_retains_finiteness[OF ***, of "fst (foldl verify_transition (X, T1, G1) ts)" "snd (snd (foldl verify_transition (X, T1, G1) ts))"] 
        by auto
      ultimately show ?case 
        by simp
    qed
  qed 
  then have T2_invar_1: "set T1  set T2"
        and T2_finite : "finite_tree T2"
    unfolding TG2 G2 T2 TG1 = (T1,G1)
    by auto

  have verify_transition_foldl_invar_2: " X ts . list.set ts  list.set unverified_transitions  
                L M1  set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2  set (fst (snd (foldl verify_transition (X, T1, G1) ts)))  
                convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) ts)))"
  proof -
    fix X ts assume "list.set ts  list.set unverified_transitions" 
              and "L M1  set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2  set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
    then show "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) ts)))"
    proof (induction ts rule: rev_induct)
      case Nil
      then show ?case 
        using G1_invar by auto
    next
      case (snoc t ts)
      then have "t  transitions M1" and "t_source t  reachable_states M1"
        unfolding unverified_transitions_alt_def 
        by force+

      have p1: "list.set ts  list.set unverified_transitions"
        using snoc.prems(1) by auto

      have "set (fst (snd (foldl verify_transition (X, T1, G1) ts)))  set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using verify_transition_retains_testsuite unfolding foldl_append foldl.simps
        by (metis fst_conv prod_eq_iff snd_conv)
      then have p2: "L M1  set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2  set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
        using snoc.prems(2)
        by blast 

      have *:"convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) ts)))"                                                           
        using snoc.IH[OF p1 p2] 
        by auto          

      have **: "Prefix_Tree.set T1  Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
        using verify_transition_foldl_invar_1[OF p1] by blast

      have ***: "((V (t_source t)) @ [(t_input t,t_output t)])  (V (t_target t))"
        using snoc.prems(1) unfolding unverified_transitions_alt_def by force
    
      have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (verify_transition ((fst (foldl verify_transition (X, T1, G1) ts)), fst (snd (foldl verify_transition (X, T1, G1) ts)), snd (snd (foldl verify_transition (X, T1, G1) ts))) t)))"          
        using verify_transition_cover_prop[OF _ * t  transitions M1 t_source t  reachable_states M1 ** ***, of "(fst (foldl verify_transition (X, T1, G1) ts))"] snoc.prems(2)
        unfolding prod.collapse
        by auto
      then have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        by auto
      moreover have "Prefix_Tree.set T1  Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using ** verify_transition_retains_testsuite
        using snoc.prems(1) verify_transition_foldl_invar_1 by blast 
      ultimately show ?case 
        by simp
    qed
  qed 
  then have T2_invar_2: "L M1  set T2 = L M2  set T2  convergence_graph_lookup_invar M1 M2 cg_lookup G2"
    unfolding TG2 G2 T2 TG1 = (T1,G1) by auto

  have T2_cover: " t . L M1  set T2 = L M2  set T2  t  list.set unverified_transitions  handles_unverified_transition t"
  proof -
    have " X t ts . t  list.set ts  list.set ts  list.set unverified_transitions  L M1  set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2  set (fst (snd (foldl verify_transition (X, T1, G1) ts)))  handles_unverified_transition t"
    proof -
      fix X t ts
      assume "t  list.set ts" and "list.set ts  list.set unverified_transitions" and "L M1  set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2  set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"

      then show "handles_unverified_transition t"
      proof (induction ts rule: rev_induct)
        case Nil
        then show ?case by auto
      next
        case (snoc t' ts)

        then have "t  transitions M1" and "t_source t  reachable_states M1"
          unfolding unverified_transitions_alt_def 
          by blast+

        have "t'  transitions M1" and "t_source t'  reachable_states M1"
          using snoc.prems(2)
          unfolding unverified_transitions_alt_def 
          by auto

        have "set (fst (snd (foldl verify_transition (X, T1, G1) ts)))  set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t']))))"
          using verify_transition_retains_testsuite unfolding foldl_append foldl.simps
          by (metis fst_conv prod_eq_iff snd_conv)
        then have "L M1  set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2  set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
          using snoc.prems(3) 
          by blast

        have *: "L M1  Prefix_Tree.set (fst (snd (verify_transition (foldl verify_transition (X, T1, G1) ts) t'))) = L M2  Prefix_Tree.set (fst (snd (verify_transition (foldl verify_transition (X, T1, G1) ts) t')))"               
          using snoc.prems(3) by auto

        have **: "V (t_source t') @ [(t_input t', t_output t')]  V (t_target t')"
          using snoc.prems(2) unfolding unverified_transitions_alt_def by force

        have "L M1  Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2  Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
          using set (fst (snd (foldl verify_transition (X, T1, G1) ts)))  set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t'])))) snoc.prems(3)
          by auto
        then have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) ts)))  Prefix_Tree.set T1  Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
          using snoc.prems(2) verify_transition_foldl_invar_1[of ts] verify_transition_foldl_invar_2[of ts]
          by auto
        then have covers_t': "handles_unverified_transition t'"
          by (metis "*" "**" t'  FSM.transitions M1 t_source t'  reachable_states M1 prod.collapse verify_transition_cover_prop) 

        show ?case proof (cases "t = t'")
          case True
          then show ?thesis 
            using covers_t' by auto
        next
          case False
          then have "t  list.set ts"
            using snoc.prems(1) by auto

          show "handles_unverified_transition t"
            using snoc.IH[OF t  list.set ts] snoc.prems(2) L M1  Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2  Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))
            by auto
        qed
      qed
    qed

    then show " t . L M1  set T2 = L M2  set T2  t  list.set unverified_transitions  handles_unverified_transition t"
      unfolding TG2 T2 G2 TG1 = (T1,G1)
      by simp
  qed


  (* properties of T3 derived from those of T1 and T2 and the assumption that T3 is passed by M2 *)

  have verify_undefined_io_pair_retains_testsuite: " qxy T . set T  set (verify_undefined_io_pair T qxy)"
  proof -
    fix qxy :: "('a × 'b × 'c)"
    fix T
    obtain q x y where "qxy = (q,x,y)"
      using prod.exhaust by metis
    show set T  set (verify_undefined_io_pair T qxy)
      unfolding qxy = (q,x,y)
      using handles_io_pair handle_unverified_io_pair M1 M2 cg_insert cg_lookup
      unfolding handles_io_pair_def verify_undefined_io_pair case_prod_conv
      by blast
  qed
  have verify_undefined_io_pair_folding_retains_testsuite: " qxys T . set T  set (foldl verify_undefined_io_pair T qxys)"
  proof -
    fix qxys T
    show "set T  set (foldl verify_undefined_io_pair T qxys)"
      using verify_undefined_io_pair_retains_testsuite
      by (induction qxys rule: rev_induct; force) 
  qed

  have verify_undefined_io_pair_retains_finiteness: " qxy T . finite_tree T  finite_tree (verify_undefined_io_pair T qxy)"
  proof -
    fix qxy :: "('a × 'b × 'c)"
    fix T :: "('b×'c) prefix_tree"
    assume "finite_tree T"
    obtain q x y where "qxy = (q,x,y)"
      using prod.exhaust by metis
    show finite_tree (verify_undefined_io_pair T qxy)
      unfolding qxy = (q,x,y)
      using handles_io_pair handle_unverified_io_pair M1 M2 cg_insert cg_lookup finite_tree T
      unfolding handles_io_pair_def verify_undefined_io_pair case_prod_conv
      by blast
  qed
  have verify_undefined_io_pair_folding_retains_finiteness: " qxys T . finite_tree T  finite_tree (foldl verify_undefined_io_pair T qxys)"
  proof -
    fix qxys 
    fix T :: "('b×'c) prefix_tree"
    assume "finite_tree T"
    then show "finite_tree (foldl verify_undefined_io_pair T qxys)"
      using verify_undefined_io_pair_retains_finiteness
      by (induction qxys rule: rev_induct; force) 
  qed

  show "finite_tree ?TS"
    using T2 T2_finite T3 h_framework M1 get_state_cover handle_state_cover sort_transitions handle_unverified_transition handle_unverified_io_pair cg_initial cg_insert cg_lookup cg_merge m = T3 verify_undefined_io_pair_folding_retains_finiteness 
    by auto


  (* having finished all but one goal, we may finally assume that M2 passes the test suite *)
  assume "((L M1  set ?TS) = (L M2  set ?TS))"
  
  have "set T2  set T3"
    unfolding T3 T2
  proof (induction undefined_io_pairs rule: rev_induct)
    case Nil
    then show ?case by auto
  next
    case (snoc x xs)
    then show ?case 
      using verify_undefined_io_pair_retains_testsuite[of "(foldl verify_undefined_io_pair (fst TG2) xs)" x]
      by force
  qed
  then have passes_T2: "L M1  set T2 = L M2  set T2"
    using ((L M1  set ?TS) = (L M2  set ?TS))  (L M1  set T3 = L M2  set T3) ((L M1  set ?TS) = (L M2  set ?TS))
    by blast


  have "set T1  set T3"
  and  G2_invar: "((L M1  set ?TS) = (L M2  set ?TS))  convergence_graph_lookup_invar M1 M2 cg_lookup G2"
    using T2_invar_1 T2_invar_2[OF passes_T2] set T2  set T3 
    by auto
  then have passes_T1: "L M1  set T1 = L M2  set T1"
    using ((L M1  set ?TS) = (L M2  set ?TS))  L M1  set T3 = L M2  set T3 ((L M1  set ?TS) = (L M2  set ?TS))
    by blast

  have T3_preserves_divergence : "preserves_divergence M1 M2 (V ` reachable_states M1)"
    using T1_V_div[OF passes_T1] .

  have T3_state_cover : "V ` reachable_states M1  set T3"
    using T1_state_cover set T1  set T3
    by blast
  then have T3_passes_state_cover : "L M1  V ` reachable_states M1 = L M2  V ` reachable_states M1"
    using T1_state_cover passes_T1 by blast 


  (* properties of T3 w.r.t. undefined io pairs *)

  have rstates_io_set : "list.set rstates_io = {(q,(x,y)) . q  reachable_states M1  x  inputs M1  y  outputs M1}"
    unfolding rstates_io rstates 
    using reachable_states_as_list_set[of M1] inputs_as_list_set[of M1] outputs_as_list_set[of M1] 
    by force
  then have undefined_io_pairs_set : "list.set undefined_io_pairs = {(q,(x,y)) . q  reachable_states M1  x  inputs M1  y  outputs M1  h_obs M1 q x y = None}"
    unfolding undefined_io_pairs 
    by auto

  have verify_undefined_io_pair_prop : "((L M1  set ?TS) = (L M2  set ?TS))  ( q x y T . L M1  set (verify_undefined_io_pair T (q,(x,y))) = L M2  set (verify_undefined_io_pair T (q,(x,y)))  
                                                    q  reachable_states M1  x  inputs M1  y  outputs M1 
                                                    V ` reachable_states M1  set T 
                                                    ( L M1  {(V q)@[(x,y)]} = L M2  {(V q)@[(x,y)]} ))"
  proof -
    fix q x y T
    assume "L M1  set (verify_undefined_io_pair T (q,(x,y))) = L M2  set (verify_undefined_io_pair T (q,(x,y)))"
       and "q  reachable_states M1" and "x  inputs M1" and "y  outputs M1"
       and "V ` reachable_states M1  set T"
       and "((L M1  set ?TS) = (L M2  set ?TS))"

    have " L M1  V ` reachable_states M1 = L M2  V ` reachable_states M1"
      using T3_state_cover ((L M1  set ?TS) = (L M2  set ?TS))  L M1  Prefix_Tree.set T3 = L M2  Prefix_Tree.set T3 ((L M1  set ?TS) = (L M2  set ?TS)) 
      by blast

    have "L M1  set (fst (handle_unverified_io_pair M1 V T G2 cg_insert cg_lookup q x y)) = L M2  set (fst (handle_unverified_io_pair M1 V T G2 cg_insert cg_lookup q x y))"
      using L M1  set (verify_undefined_io_pair T (q,(x,y))) = L M2  set (verify_undefined_io_pair T (q,(x,y)))
      unfolding verify_undefined_io_pair case_prod_conv combine_set G2
      by blast


    show "( L M1  {(V q)@[(x,y)]} = L M2  {(V q)@[(x,y)]} )"
      using assms(16)
      unfolding handles_io_pair_def 
      using assms(1-4,7,8) is_state_cover_assignment M1 V L M1  V ` reachable_states M1 = L M2  V ` reachable_states M1
            q  reachable_states M1 x  inputs M1 y  outputs M1
            G2_invar[OF ((L M1  set ?TS) = (L M2  set ?TS))] convergence_graph_insert_invar M1 M2 cg_lookup cg_insert
            L M1  set (fst (handle_unverified_io_pair M1 V T G2 cg_insert cg_lookup q x y)) = L M2  set (fst (handle_unverified_io_pair M1 V T G2 cg_insert cg_lookup q x y)) 
      by blast
  qed

  have T3_covers_undefined_io_pairs : "( q x y . q  reachable_states M1  x  inputs M1  y  outputs M1  h_obs M1 q x y = None 
          ( L M1  {(V q)@[(x,y)]} = L M2  {(V q)@[(x,y)]} ))" 
  proof -
    fix q x y assume "q  reachable_states M1" and "x  inputs M1" and "y  outputs M1" and "h_obs M1 q x y = None" 

    have " q x y qxys T . L M1  set (foldl verify_undefined_io_pair T qxys) = L M2  set (foldl verify_undefined_io_pair T qxys)  (V ` reachable_states M1)  set T  (q,(x,y))  list.set qxys  list.set qxys  list.set undefined_io_pairs  
              ( L M1  {(V q)@[(x,y)]} = L M2  {(V q)@[(x,y)]} )"
      (is " q x y qxys T . ?P1 qxys T  (V ` reachable_states M1)  set T  (q,(x,y))  list.set qxys  list.set qxys  list.set undefined_io_pairs  ?P2 q x y qxys T")
    proof -
      fix q x y qxys T
      assume "?P1 qxys T" and "(q,(x,y))  list.set qxys" and "list.set qxys  list.set undefined_io_pairs" and "(V ` reachable_states M1)  set T"
      then show "?P2 q x y qxys T"
      proof (induction qxys rule: rev_induct)
        case Nil
        then show ?case by auto
      next
        case (snoc a qxys)

        have "set (foldl verify_undefined_io_pair T qxys)  set (foldl verify_undefined_io_pair T (qxys@[a]))"
          using verify_undefined_io_pair_retains_testsuite 
          by auto
        then have *:"L M1  Prefix_Tree.set (foldl verify_undefined_io_pair T qxys) = L M2  Prefix_Tree.set (foldl verify_undefined_io_pair T qxys)"
          using snoc.prems(1)
          by blast

        have **: "V ` reachable_states M1  Prefix_Tree.set (foldl verify_undefined_io_pair T qxys)"
          using snoc.prems(4) verify_undefined_io_pair_folding_retains_testsuite
          by blast

        show ?case proof (cases "a = (q,(x,y))")
          case True
          then have ***: "q  reachable_states M1"
            using snoc.prems(3) 
            unfolding undefined_io_pairs_set
            by auto 

          have "x  inputs M1" and "y  outputs M1"
            using snoc.prems(2,3) unfolding undefined_io_pairs_set by auto

          have ****: "L M1  set (verify_undefined_io_pair (foldl verify_undefined_io_pair T qxys) (q,(x,y))) = L M2  set (verify_undefined_io_pair (foldl verify_undefined_io_pair T qxys) (q,(x,y)))"
            using snoc.prems(1) unfolding True by auto
            
          show ?thesis
            using verify_undefined_io_pair_prop[OF ((L M1  set ?TS) = (L M2  set ?TS)) **** *** x  inputs M1 y  outputs M1 **]
            unfolding True 
            by auto
        next
          case False
          then have "(q, x, y)  list.set qxys" and "list.set qxys  list.set undefined_io_pairs"
            using snoc.prems(2,3) by auto
          then show ?thesis 
            using snoc.IH[OF * _ _  snoc.prems(4)]
            using set (foldl verify_undefined_io_pair T qxys)  set (foldl verify_undefined_io_pair T (qxys@[a]))
            by blast
        qed
      qed
    qed
    moreover have "L M1  set (foldl verify_undefined_io_pair T2 undefined_io_pairs) = L M2  set (foldl verify_undefined_io_pair T2 undefined_io_pairs)"
      using ((L M1  set ?TS) = (L M2  set ?TS))  L M1  set T3 = L M2  set T3  ((L M1  set ?TS) = (L M2  set ?TS))
      unfolding T3 T2 .
    moreover have "(V ` reachable_states M1)  set T2"
      using T1_state_cover T2 T2_invar_1 passes_T2 by fastforce
    moreover have "(q,(x,y))  list.set undefined_io_pairs"
      unfolding undefined_io_pairs_set
      using q  reachable_states M1 x  inputs M1 y  outputs M1 h_obs M1 q x y = None
      by blast
    ultimately show "( L M1  {(V q)@[(x,y)]} = L M2  {(V q)@[(x,y)]} )"
      unfolding T3 T2 
      by blast
  qed


  have handles_unverified_transitions: " 
            (t γ. t  FSM.transitions M1 
              t_source t  reachable_states M1 
              length γ  m-n 
              list.set γ  FSM.inputs M1 × FSM.outputs M1 
              butlast γ  LS M1 (t_target t) 
              V (t_target t)  V (t_source t) @ [(t_input t, t_output t)] 
              L M1  (V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes γ)}) =
              L M2  (V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes γ)}) 
              preserves_divergence M1 M2 (V ` reachable_states M1  {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω'  list.set (prefixes γ)}))"
    using T2_cover[OF passes_T2]
    unfolding unverified_transitions_alt_def
    unfolding handles_unverified_transition
    unfolding ?TS = T3 n by blast



  have "satisfies_abstract_h_condition M1 M2 V m"
    unfolding satisfies_abstract_h_condition_def Let_def
    using abstract_h_condition_by_unverified_transition_and_io_pair_coverage[where k="m-n",OF assms(1) is_state_cover_assignment M1 V T3_passes_state_cover T3_preserves_divergence handles_unverified_transitions T3_covers_undefined_io_pairs]
    unfolding ?TS = T3 n by blast

  then show "L M1 = L M2"
    using abstract_h_condition_completeness[OF assms(1,2,3,6,5,7,8) is_state_cover_assignment M1 V]
    by blast  
qed

end