# Theory Convergence

section ‹Convergence of Traces›

text ‹This theory defines convergence of traces in observable FSMs and provides results on
sufficient conditions to establish that two traces converge.
Furthermore it is shown how convergence can be employed in proving language equivalence.›

theory Convergence
imports
begin

subsection ‹Basic Definitions›

(* two traces converge if they are both in the language of the FSM and reach the same state *)
fun converge :: "('a,'b,'c) fsm  ('b × 'c) list   ('b × 'c) list  bool" where
"converge M π τ = (π  L M  τ  L M  (LS M (after_initial M π) = LS M (after_initial M τ)))"

fun preserves_divergence :: "('a,'b,'c) fsm  ('d,'b,'c) fsm  ('b × 'c) list set  bool" where
"preserves_divergence M1 M2 A = ( α  L M1  A .  β  L M1  A . ¬ converge M1 α β  ¬ converge M2 α β)"

fun preserves_convergence :: "('a,'b,'c) fsm  ('d,'b,'c) fsm  ('b × 'c) list set  bool" where
"preserves_convergence M1 M2 A = ( α  L M1  A .  β  L M1  A . converge M1 α β  converge M2 α β)"

lemma converge_refl :
assumes "α  L M"
shows "converge M α α"
using assms by auto

lemma convergence_minimal :
assumes "minimal M"
and     "observable M"
and     "α  L M"
and     "β  L M"
shows "converge M α β = ((after_initial M α) = (after_initial M β))"
proof
have *:"(after_initial M α)  states M"
using α  L M by (meson after_is_state assms(2))
have **:"(after_initial M β)  states M"
using β  L M by (meson after_is_state assms(2))

show "converge M α β  ((after_initial M α) = (after_initial M β))"
using * ** minimal M unfolding minimal.simps converge.simps
by blast

show "((after_initial M α) = (after_initial M β))  converge M α β"
unfolding converge.simps using assms(3,4) by simp
qed

lemma state_cover_assignment_diverges :
assumes "observable M"
and     "minimal M"
and
and     "q1  reachable_states M"
and     "q2  reachable_states M"
and     "q1  q2"
shows "¬ converge M (f q1) (f q2)"
proof -
have "f q1  L M"
using assms(3,4)
by (metis from_FSM_language is_state_cover_assignment.simps language_contains_empty_sequence language_io_target_append language_prefix reachable_state_is_state)
moreover have "q1  io_targets M (f q1) (initial M)"
using assms(3,4) unfolding is_state_cover_assignment.simps by blast
ultimately have "(after_initial M (f q1)) = q1"
using assms(1)
by (metis (no_types, lifting) observable_after_path observable_path_io_target singletonD)

have "f q2  L M"
using assms(3,5)
by (metis from_FSM_language is_state_cover_assignment.simps language_contains_empty_sequence language_io_target_append language_prefix reachable_state_is_state)
moreover have "q2  io_targets M (f q2) (initial M)"
using assms(3,5) unfolding is_state_cover_assignment.simps by blast
ultimately have "(after_initial M (f q2)) = q2"
using assms(1)
by (metis (no_types, lifting) observable_after_path observable_path_io_target singletonD)

show ?thesis
using convergence_minimal[OF assms(2,1) f q1  L M f q2  L M] q1  q2
unfolding (after_initial M (f q1)) = q1 (after_initial M (f q2)) = q2
by simp
qed

lemma converge_extend :
assumes "observable M"
and     "converge M α β"
and     "α@γ  L M"
and     "β  L M"
shows "β@γ  L M"
by (metis after_io_targets assms(1) assms(2) assms(3) assms(4) converge.simps language_io_target_append language_prefix observable_io_targets observable_io_targets_language singletonI the_elem_eq)

lemma converge_append :
assumes "observable M"
and     "converge M α β"
and     "α@γ  L M"
and     "β  L M"
shows "converge M (α@γ) (β@γ)"
using after_language_append_iff[OF assms(1,3)]
using after_language_append_iff[OF assms(1) converge_extend[OF assms]]
using assms converge_extend
unfolding converge.simps
by blast

lemma non_initialized_state_cover_assignment_diverges :
assumes "observable M"
and     "minimal M"
and     " q . q  reachable_states M  q  io_targets M (f q) (initial M)"
and     " q . q  reachable_states M  f q  L M   SC"
and     "q1  reachable_states M"
and     "q2  reachable_states M"
and     "q1  q2"
shows "¬ converge M (f q1) (f q2)"
proof -

have "f q1  L M"
using assms(4,5) by blast
moreover have "q1  io_targets M (f q1) (initial M)"
using assms(3,5) by blast
ultimately have "(after_initial M (f q1)) = q1"
using assms(1)
by (metis (no_types, lifting) observable_after_path observable_path_io_target singletonD)

have "f q2  L M"
using assms(4,6) by blast
moreover have "q2  io_targets M (f q2) (initial M)"
using assms(3,6) by blast
ultimately have "(after_initial M (f q2)) = q2"
using assms(1)
by (metis (no_types, lifting) observable_after_path observable_path_io_target singletonD)

show ?thesis
using convergence_minimal[OF assms(2,1) f q1  L M f q2  L M] q1  q2
unfolding (after_initial M (f q1)) = q1 (after_initial M (f q2)) = q2
by simp
qed

lemma converge_trans_2 :
assumes "observable M" and "minimal M" and "converge M u v"
shows "converge M (u@w1) (u@w2) = converge M (v@w1) (v@w2)"
"converge M (u@w1) (u@w2) = converge M (u@w1) (v@w2)"
"converge M (u@w1) (u@w2) = converge M (v@w1) (u@w2)"
proof -
have "converge M (u@w1) (u@w2) = converge M (v@w1) (v@w2)  converge M (u@w1) (u@w2) = converge M (u@w1) (v@w2)  converge M (u@w1) (u@w2) = converge M (v@w1) (u@w2)"
proof (cases "u@w1  L M  u@w2  L M")
case False
then consider "u@w1  L M" | "u@w2  L M"
by blast
then have "v@w1  L M  v@w2  L M"
using after_language_iff[OF assms(1), of u "initial M" w1]
after_language_iff[OF assms(1), of u "initial M" w2]
after_language_iff[OF assms(1), of v "initial M" w1]
after_language_iff[OF assms(1), of v "initial M" w2]
by (metis assms(3) converge.elims(2))
then show ?thesis
by (meson assms(1) assms(3) converge.elims(2) converge_extend)
next
case True
then have "u@w1  L M" and "u@w2  L M" by auto
then have "v@w1  L M" and "v@w2  L M"
by (meson assms(1) assms(3) converge.simps converge_extend)+

have "u  L M" using u@w1  L M language_prefix by metis
have "v  L M" using v@w1  L M language_prefix by metis

have
using u  L M v  L M assms(1) assms(2) assms(3) convergence_minimal by blast
moreover have "after_initial M (u @ w1) = after_initial M (v @ w1)"
by (metis calculation True v @ w1  L M after_split assms(1))
ultimately have "after_initial M (u @ w2) = after_initial M (v @ w2)"
by (metis (no_types) True v @ w2  L M after_split assms(1))

have "converge M (u@w1) (u@w2) = converge M (v@w1) (v@w2)"
using True after_initial M (u @ w1) = after_initial M (v @ w1) after_initial M (u @ w2) = after_initial M (v @ w2) v @ w1  L M v @ w2  L M
by auto
moreover have "converge M (u@w1) (u@w2) = converge M (u@w1) (v@w2)"
using True after_initial M (u @ w2) = after_initial M (v @ w2) v @ w2  L M by auto
moreover have "converge M (u@w1) (u@w2) = converge M (v@w1) (u@w2)"
using True after_initial M (u @ w1) = after_initial M (v @ w1) v @ w1  L M by auto
ultimately show ?thesis
by blast
qed
then show "converge M (u@w1) (u@w2) = converge M (v@w1) (v@w2)"
"converge M (u@w1) (u@w2) = converge M (u@w1) (v@w2)"
"converge M (u@w1) (u@w2) = converge M (v@w1) (u@w2)"
by blast+
qed

lemma preserves_divergence_converge_insert :
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "converge M1 u v"
and "converge M2 u v"
and "preserves_divergence M1 M2 X"
and "u  X"
shows "preserves_divergence M1 M2 (Set.insert v X)"
proof -
have " w . w  L M1  X  ¬converge M1 v w  ¬converge M2 v w"
proof -
fix w
assume "w  L M1  X" and "¬converge M1 v w"

then have "¬converge M1 u w"
using assms(5)
using converge.simps by blast
then have "¬converge M2 u w"
using assms(5-8)
by (meson IntI w  L M1  X converge.elims(2) preserves_divergence.simps)
then show "¬converge M2 v w"
using assms(6) converge.simps by blast
qed
then show ?thesis
using assms(7)
unfolding preserves_divergence.simps
by (metis (no_types, lifting) Int_insert_right_if1 assms(1) assms(2) assms(3) assms(4) assms(5) converge.elims(2) convergence_minimal insert_iff)
qed

lemma preserves_divergence_converge_replace :
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "converge M1 u v"
and "converge M2 u v"
and "preserves_divergence M1 M2 (Set.insert u X)"
shows "preserves_divergence M1 M2 (Set.insert v X)"
proof -
have "u  L M1" and "v  L M1"
using assms(5) by auto
then have "after_initial M1 u = after_initial M1 v"
using assms(1) assms(3) assms(5) convergence_minimal by blast

have " w . w  L M1  X  ¬converge M1 v w  ¬converge M2 v w"
proof -
fix w
assume "w  L M1  X" and "¬converge M1 v w"

then have "¬converge M1 u w"
using assms(5)
using converge.simps by blast
then have "¬converge M2 u w"
using assms(5-7)
by (meson IntD1 IntD2 IntI w  L M1  X converge.elims(2) insertCI preserves_divergence.elims(1))
then show "¬converge M2 v w"
using assms(6) converge.simps by blast
qed

have " α β . α  L M1  α  insert v X  β  L M1  β  insert v X  ¬ converge M1 α β  ¬ converge M2 α β"
proof -
fix α β  assume "α  L M1" "α  insert v X" "β  L M1" "β  insert v X" "¬ converge M1 α β"

then consider "α = v  β = v" |
"α = v  β  X" |
"α  X  β = v" |
"α  X  β  X"
by blast
then show "¬ converge M2 α β"
proof cases
case 1
then show ?thesis
using α  L M1 β  L M1 ¬ converge M1 α β by auto
next
case 2
then show ?thesis
by (metis IntI w. w  L M1  X; ¬ converge M1 v w  ¬ converge M2 v w β  L M1 ¬ converge M1 α β)
next
case 3
then show ?thesis
by (metis IntI w. w  L M1  X; ¬ converge M1 v w  ¬ converge M2 v w α  L M1 ¬ converge M1 α β converge.simps)
next
case 4
then show ?thesis
using assms(7) unfolding preserves_divergence.simps
using α  L M1 β  L M1 ¬ converge M1 α β by blast
qed
qed
then show ?thesis
unfolding preserves_divergence.simps by blast
qed

lemma preserves_divergence_converge_replace_iff :
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "converge M1 u v"
and "converge M2 u v"
shows "preserves_divergence M1 M2 (Set.insert u X) = preserves_divergence M1 M2 (Set.insert v X)"
proof -
have *: "converge M1 v u" using assms(5) by auto
have **: "converge M2 v u" using assms(6) by auto

show ?thesis
using preserves_divergence_converge_replace[OF assms]
preserves_divergence_converge_replace[OF assms(1-4) * **]
by blast
qed

lemma preserves_divergence_subset :
assumes "preserves_divergence M1 M2 B"
and     "A  B"
shows "preserves_divergence M1 M2 A"
using assms unfolding preserves_divergence.simps by blast

lemma preserves_divergence_insertI :
assumes "preserves_divergence M1 M2 X"
and     " α . α  L M1  X  β  L M1  ¬converge M1 α β  ¬converge M2 α β"
shows "preserves_divergence M1 M2 (Set.insert β X)"
using assms unfolding preserves_divergence.simps
by (metis Int_insert_right converge.elims(2) converge.elims(3) insertE)

lemma preserves_divergence_insertE :
assumes "preserves_divergence M1 M2 (Set.insert β X)"
shows "preserves_divergence M1 M2 X"
and   " α . α  L M1  X  β  L M1  ¬converge M1 α β  ¬converge M2 α β"
using assms unfolding preserves_divergence.simps
by blast+

lemma distinguishes_diverge_prefix :
assumes "observable M"
and     "distinguishes M (after_initial M u) (after_initial M v) w"
and     "u  L M"
and     "v  L M"
and     "w'  set (prefixes w)"
and     "w'  LS M (after_initial M u)"
and     "w'  LS M (after_initial M v)"
shows "¬converge M (u@w') (v@w')"
proof
assume "converge M (u @ w') (v @ w')"

obtain w'' where "w = w'@w''"
using assms(5)
using prefixes_set_ob by auto

have "u@w'  L M"
using assms(3,6) after_language_iff[OF assms(1)]
by blast
then have *:"(w  LS M (after_initial M u)) = (w''  LS M (after_initial M (u@w')))"
using after_language_append_iff[OF assms(1)]
unfolding w = w'@w''
by blast

have "v@w'  L M"
using assms(4,7) after_language_iff[OF assms(1)]
by blast
then have **:"(w  LS M (after_initial M v)) = (w''  LS M (after_initial M (v@w')))"
using after_language_append_iff[OF assms(1)]
unfolding w = w'@w''
by blast

have "(w  LS M (after_initial M u)) = (w  LS M (after_initial M v))"
unfolding * **
using converge M (u @ w') (v @ w')
by (metis converge.elims(2))
then show False
using distinguishes M (after_initial M u) (after_initial M v) w
unfolding distinguishes_def
by blast
qed

lemma converge_distinguishable_helper :
assumes "observable M1"
and     "observable M2"
and     "minimal M1"
and     "minimal M2"
and "converge M1 π α"
and "converge M2 π α"
and "converge M1 τ β"
and "converge M2 τ β"
and "distinguishes M2 (after_initial M2 π) (after_initial M2 τ) v"
and "L M1  {α@v,β@v} = L M2  {α@v,β@v}"
shows "(after_initial M1 π)  (after_initial M1 τ)"
proof -
have "LS M1 (after_initial M1 π) = LS M1 (after_initial M1 α)"
by (meson assms(5) converge.elims(2))
have "LS M1 (after_initial M1 τ) = LS M1 (after_initial M1 β)"
by (meson assms(7) converge.elims(2))
have "LS M2 (after_initial M2 π) = LS M2 (after_initial M2 α)"
by (meson assms(6) converge.elims(2))
have "LS M2 (after_initial M2 τ) = LS M2 (after_initial M2 β)"
by (meson assms(8) converge.elims(2))

have "v  LS M2 (after_initial M2 π)  v  LS M2 (after_initial M2 τ)"
using assms(9) unfolding distinguishes_def by blast
then have "v  LS M2 (after_initial M2 α)  v  LS M2 (after_initial M2 β)"
using LS M2 (after_initial M2 π) = LS M2 (after_initial M2 α) LS M2 (after_initial M2 τ) = LS M2 (after_initial M2 β) by blast
then have "α@v  L M2  β@v  L M2"
by (meson after_language_iff assms(2) assms(6) assms(8) converge.elims(2))
then have "α@v  L M1  β@v  L M1"
using assms(10)
by (metis (no_types, lifting) Int_insert_right inf_sup_ord(1) insert_subset)
then have "v  LS M1 (after_initial M1 α)  v  LS M1 (after_initial M1 β)"
by (meson after_language_iff assms(1) assms(5) assms(7) converge.elims(2))
then have "v  LS M1 (after_initial M1 π)  v  LS M1 (after_initial M1 τ)"
using LS M1 (after_initial M1 π) = LS M1 (after_initial M1 α) LS M1 (after_initial M1 τ) = LS M1 (after_initial M1 β) by blast
then show ?thesis
by metis
qed

lemma converge_append_language_iff :
assumes "observable M"
and     "converge M α β"
shows "(α@γ  L M) = (β@γ  L M)"
by (metis (no_types) assms(1) assms(2) converge.simps converge_extend)

lemma converge_append_iff :
assumes "observable M"
and     "converge M α β"
shows "converge M γ (α@ω) = converge M γ (β@ω)"
proof (cases "(α@ω)  L M")
case True
then show ?thesis
using converge_append_language_iff[OF assms] language_prefix[of β ω M "initial M"]
using converge_append[OF assms True]
by auto
next
case False
then show ?thesis
using converge_append_language_iff[OF assms]
using converge.simps by blast
qed

lemma after_distinguishes_language :
assumes "observable M1"
and     "α  L M1"
and     "β  L M1"
and     "distinguishes M1 (after_initial M1 α) (after_initial M1 β) γ"
shows "(α@γ  L M1)  (β@γ  L M1)"
unfolding after_language_iff[OF assms(1,2),symmetric]
after_language_iff[OF assms(1,3),symmetric]
using assms(4)
unfolding distinguishes_def
by blast

lemma distinguish_diverge :
assumes "observable M1"
and     "observable M2"
and     "distinguishes M1 (after_initial M1 u) (after_initial M1 v) γ"
and     "u @ γ  T"
and     "v @ γ  T"
and     "u  L M1"
and     "v  L M1"
and     "L M1  T = L M2  T"
shows "¬ converge M2 u v"
proof
assume "converge M2 u v"
then have "u@γ  L M2  v@γ  L M2"
using assms(2) converge_append_language_iff by blast
moreover have "u@γ  L M1  v@γ  L M1"
using assms(1,3,6,7)
using after_distinguishes_language
by blast
ultimately show False
using assms(4,5,8) by blast
qed

lemma distinguish_converge_diverge :
assumes "observable M1"
and     "observable M2"
and     "minimal M1"
and     "u'  L M1"
and     "v'  L M1"
and     "converge M1 u u'"
and     "converge M1 v v'"
and     "converge M2 u u'"
and     "converge M2 v v'"
and     "distinguishes M1 (after_initial M1 u) (after_initial M1 v) γ"
and     "u' @ γ  T"
and     "v' @ γ  T"
and     "L M1  T = L M2  T"
shows "¬ converge M2 u v"
proof -
have *:"distinguishes M1 (after_initial M1 u') (after_initial M1 v') γ"
by (metis (mono_tags, opaque_lifting) assms(1) assms(10) assms(3) assms(6) assms(7) converge.simps convergence_minimal)

show ?thesis
using distinguish_diverge[OF assms(1-2) *]
by (metis (mono_tags, lifting) assms(9) assms(11) assms(12) assms(13) assms(4) assms(5) assms(8) converge.simps)
qed

lemma diverge_prefix :
assumes "observable M"
and     "α@γ  L M"
and     "β@γ  L M"
and     "¬ converge M (α@γ) (β@γ)"
shows "¬ converge M α β"
by (meson assms converge_append language_prefix)

lemma converge_sym: "converge M u v = converge M v u"
by auto

lemma state_cover_transition_converges :
assumes "observable M"
and
and     "t  transitions M"
and
shows "converge M ((V (t_source t)) @ [(t_input t,t_output t)]) (V (t_target t))"
proof -
have
using assms(3,4) reachable_states_next
by metis

have "V (t_source t)  L M" and "after_initial M (V (t_source t)) = (t_source t)"
using state_cover_assignment_after[OF assms(1,2,4)]
by simp+

have "((V (t_source t)) @ [(t_input t,t_output t)])  L M"
using after_language_iff[OF assms(1) V (t_source t)  L M, of "[(t_input t,t_output t)]"]
assms(3)
unfolding LS_single_transition after_initial M (V (t_source t)) = (t_source t)
by force

have "FSM.after M (t_source t) [(t_input t, t_output t)] = t_target t"
using after_transition[OF assms(1)] assms(3)
by auto
then have "after_initial M ((V (t_source t)) @ [(t_input t,t_output t)]) = t_target t"
using after_initial M (V (t_source t)) = (t_source t)
using after_split[OF assms(1) ((V (t_source t)) @ [(t_input t,t_output t)])  L M]
by force
then show ?thesis
using ((V (t_source t)) @ [(t_input t,t_output t)])  L M
using state_cover_assignment_after[OF assms(1,2) ]
by auto
qed

lemma equivalence_preserves_divergence :
assumes "observable M"
and     "observable I"
and     "L M = L I"
shows "preserves_divergence M I A"
proof -
have " α β . α  L M  A  β  L M  A  ¬ converge M α β  ¬ converge I α β"
proof -
fix  α β assume "α  L M  A" and "β  L M  A" and "¬ converge M α β"
then have "after_initial M α  states M" and "after_initial M β  states M" and "LS M (after_initial M α)  LS M (after_initial M β)"
using after_is_state[OF assms(1)]  unfolding converge.simps
by auto
then obtain γ where "(γ  LS M (after_initial M α))  (γ  LS M (after_initial M β))"
by blast
then have "(α@γ  L M)  (β@γ  L M)"
using after_language_iff[OF assms(1)] α  L M  A β  L M  A by blast
then have "(α@γ  L I)  (β@γ  L I)"
using assms(3) by blast
then show "¬ converge I α β"
using assms(2) converge_append_language_iff by blast
qed
then show ?thesis
unfolding preserves_divergence.simps by blast
qed

subsection ‹Sufficient Conditions for Convergence›

text ‹The following lemma provides a condition for convergence that assumes the existence
of a single state cover covering all extensions of length up to (m - |M1|).
This is too restrictive for the SPYH method but could be used in the SPY method.
The proof idea has been developed by Wen-ling Huang and adapted by the author to
avoid requiring the SC to cover traces that contain a proper prefix already not
in the language of FSM M1.›
lemma sufficient_condition_for_convergence_in_SPY_method :
fixes M1 :: "('a,'b,'c) fsm"
fixes M2 :: "('d,'b,'c) fsm"
assumes "observable M1"
and     "observable M2"
and     "minimal M1"
and     "minimal M2"
and     "size_r M1  m"
and     "size M2  m"
and     "L M1  T = L M2  T"
and     "π  L M1  T"
and     "τ  L M1  T"
and     "converge M1 π τ"
and     "SC  T"
and     " q . q  reachable_states M1   io  L M1  SC . q  io_targets M1 io (initial M1)"
and     "preserves_divergence M1 M2 SC"
and     " γ x y . length γ < m - size_r M1
γ  LS M1 (after_initial M1 π)
x  inputs M1
y  outputs M1
α β . converge M1 α (π@γ)
converge M2 α (π@γ)
converge M1 β (τ@γ)
converge M2 β (τ@γ)
α  SC
α@[(x,y)]  SC
β  SC
β@[(x,y)]  SC"
and     " α β . converge M1 α π
converge M2 α π
converge M1 β τ
converge M2 β τ
α  SC
β  SC"
and    "inputs M2 = inputs M1"
and    "outputs M2 = outputs M1"
shows "converge M2 π τ"
proof -

obtain f where f1: " q . q  reachable_states M1  q  io_targets M1 (f q) (initial M1)"
and f2: " q . q  reachable_states M1  f q  L M1  SC"
using non_initialized_state_cover_assignment_from_non_initialized_state_cover[OF  q . q  reachable_states M1   io  L M1  SC . q  io_targets M1 io (initial M1)]
by blast

define A where A: "A = (λ q . Set.filter (converge M1 (f q)) (L M1  SC))"

define Q where Q: "Q = (λ q .  α  A q . io_targets M2 α (initial M2))"

have " q . q  reachable_states M1  Q q  {}"
proof -
fix q assume "q  reachable_states M1"
then have "f q  A q"
using A
using f2 by auto
moreover have "f q  L M2"
proof -
have "f q  L M1  SC"
using q  reachable_states M1 f2 by blast
then show ?thesis
using SC  T L M1  T = L M2  T by blast
qed
ultimately show "Q q  {}"
unfolding Q
by auto
qed

have "states M2 = ( q  reachable_states M1 . Q q)  (states M2 - ( q  reachable_states M1 . Q q))"
proof -
have "( q  reachable_states M1 . Q q)  reachable_states M2"
proof
fix q assume "q  ( q  reachable_states M1 . Q q)"
then obtain α where "q  io_targets M2 α (initial M2)"
unfolding Q by blast
then show "q  reachable_states M2"
unfolding io_targets.simps reachable_states_def by blast
qed
then show ?thesis
by (metis Diff_partition reachable_state_is_state subset_iff)
qed

have " q1 q2 . q1  reachable_states M1  q2  reachable_states M1  q1  q2  Q q1  Q q2 = {}"
proof -
fix q1 q2
assume "q1  reachable_states M1" and "q2  reachable_states M1" and "q1  q2"

have " α β . α  A q1  β  A q2  io_targets M2 α (initial M2)  io_targets M2 β (initial M2) = {}"
proof -
fix α β assume "α  A q1" and "β  A q2"

then have "converge M1 (f q1) α" and "converge M1 (f q2) β"
unfolding A
by (meson member_filter)+
moreover have "¬ converge M1 (f q1) (f q2)"
using non_initialized_state_cover_assignment_diverges[OF assms(1,3) f1 f2 q1  reachable_states M1 q2  reachable_states M1 q1  q2] .
ultimately have "¬ converge M1 α β"
unfolding converge.simps by blast
moreover have "αL M1  SC"
using α  A q1 unfolding A
by (meson member_filter)
moreover have "βL M1  SC"
using β  A q2 unfolding A
by (meson member_filter)
ultimately have "¬ converge M2 α β"
using preserves_divergence M1 M2 SC
unfolding preserves_divergence.simps
by blast

have "α  L M2" and "β  L M2"
using αL M1  SC βL M1  SC SC  T L M1  T = L M2  T by blast+

have "io_targets M2 α (initial M2) = {after_initial M2 α}"
using observable_io_targets[OF observable M2 α  L M2]
unfolding after_io_targets[OF observable M2 α  L M2]
by (metis the_elem_eq)
moreover have "io_targets M2 β (initial M2) = {after_initial M2 β}"
using observable_io_targets[OF observable M2 β  L M2]
unfolding after_io_targets[OF observable M2 β  L M2]
by (metis the_elem_eq)
ultimately show "io_targets M2 α (initial M2)  io_targets M2 β (initial M2) = {}"
using ¬ converge M2 α β unfolding convergence_minimal[OF assms(4,2) α  L M2 β  L M2]
by (metis Int_insert_right_if0 inf_bot_right singletonD)
qed

then show "Q q1  Q q2 = {}"
unfolding Q by blast
qed
then have " q . Uniq (λq' .  q'  reachable_states M1  q  Q q')"
unfolding Uniq_def
by blast

(* we can partition states of M2 via the Q-classes they belong to (using a single separate class for
all states not contained in any Q-class *)
define partition where partition: "partition = (λ q . if  q'  reachable_states M1 . q  Q q'
then Q (THE q' . q'  reachable_states M1  q  Q q')
else (states M2 - ( q  reachable_states M1 . Q q)))"

have is_eq: "equivalence_relation_on_states M2 partition"
proof-
let ?r = "{(q1,q2) | q1 q2 . q1  states M2  q2  partition q1}"

have " q .partition q  states M2"
proof -
fix q show "partition q  states M2"
proof (cases " q'  reachable_states M1 . q  Q q'")
case True
then have "partition q = Q (THE q' . q'  reachable_states M1  q  Q q')"
unfolding partition by simp
then show ?thesis
using True  q . Uniq (λq' .  q'  reachable_states M1  q  Q q')
by (metis (no_types, lifting) Q SUP_least io_targets_states)
next
case False
then show ?thesis unfolding partition
by auto
qed
qed

have " q . q  states M2  q  partition q"
proof -
fix q assume "q  states M2"
show "q  partition q"
proof (cases " q'  reachable_states M1 . q  Q q'")
case True
then have "partition q = Q (THE q' . q'  reachable_states M1  q  Q q')"
unfolding partition by simp
then show ?thesis
using True  q . Uniq (λq' .  q'  reachable_states M1  q  Q q')
using the1_equality' by fastforce
next
case False
then show ?thesis unfolding partition
using q  states M2
by simp
qed
qed

have " q q' . q  states M2  q'  partition q  q  partition q'"
proof -
fix q q' assume "q  states M2" and "q'  partition q"
show "q  partition q'"
proof (cases " q'  reachable_states M1 . q  Q q'")
case True
then have "partition q = Q (THE q' . q'  reachable_states M1  q  Q q')"
unfolding partition by simp
then obtain q1 where "partition q = Q q1" and "q1  reachable_states M1" and "q  Q q1"
using True  q . Uniq (λq' .  q'  reachable_states M1  q  Q q')
using the1_equality' by fastforce
then have "q'  Q q1"
using q'  partition q by auto
then have "partition q' = Q q1"
using q1  reachable_states M1
using the1_equality'[OF  q . Uniq (λq' .  q'  reachable_states M1  q  Q q')]
unfolding partition
by auto
then show ?thesis
using q  Q q1 q'  partition q partition q = Q q1 by blast
next
case False
then show ?thesis
using q  states M2 q'  partition q
qed
qed

have " q q' q'' . q  states M2  q'  partition q  q''  partition q'  q''  partition q"
proof -
fix q q' q''
assume "q  states M2" and "q'  partition q" and "q''  partition q'"
show "q''  partition q"
proof (cases " q'  reachable_states M1 . q  Q q'")
case True
then have "partition q = Q (THE q' . q'  reachable_states M1  q  Q q')"
unfolding partition by simp
then obtain q1 where "partition q = Q q1" and "q1  reachable_states M1" and "q  Q q1"
using True  q . Uniq (λq' .  q'  reachable_states M1  q  Q q')
using the1_equality' by fastforce
then have "q'  Q q1"
using q'  partition q by auto
then have "partition q' = Q q1"
using q1  reachable_states M1
using the1_equality'[OF  q . Uniq (λq' .  q'  reachable_states M1  q  Q q')]
unfolding partition
by auto
then have "q''  Q q1"
using q''  partition q' by auto
then have "partition q'' = Q q1"
using q1  reachable_states M1
using the1_equality'[OF  q . Uniq (λq' .  q'  reachable_states M1  q  Q q')]
unfolding partition
by auto
then show ?thesis
unfolding partition q = Q q1
using q''  Q q1 by blast
next
case False
then show ?thesis
using q  states M2 q'  partition q q''  partition q'
qed
qed

have "refl_on (states M2) ?r" unfolding refl_on_def
proof
show "{(q1, q2) |q1 q2. q1  FSM.states M2  q2  partition q1}  FSM.states M2 × FSM.states M2"
using  q .partition q  states M2 by blast
show "xFSM.states M2. (x, x)  {(q1, q2) |q1 q2. q1  FSM.states M2  q2  partition q1}"
proof
fix q assume "q  states M2"
then show "(q,q)  {(q1, q2) |q1 q2. q1  FSM.states M2  q2  partition q1}"
using  q . q  states M2  q  partition q
by blast
qed
qed
moreover have "sym ?r"
unfolding sym_def
using  q q' . q  states M2  q'  partition q  q  partition q'   q .partition q  states M2
by blast
moreover have "trans ?r"
unfolding trans_def
using  q q' q'' . q  states M2  q'  partition q  q''  partition q'  q''  partition q
by blast
ultimately show ?thesis
unfolding equivalence_relation_on_states_def equiv_def
using  q .partition q  states M2 by blast
qed

(* the partitioning results in at most n+1 classes *)
define n0 where n0: "n0 = card (partition ` states M2)"
have "n0  Suc (size_r M1)" and "n0  size_r M1"
proof -
have "partition ` states M2  insert (states M2 - ( q  reachable_states M1 . Q q)) (Q ` reachable_states M1)"
proof
fix X assume "X  partition ` states M2"
then obtain q where "q  states M2" and "X = partition q"
by blast

show "X  insert (states M2 - ( q  reachable_states M1 . Q q)) (Q ` reachable_states M1)"
proof (cases "q'reachable_states M1. q  Q q'")
case True
then show ?thesis
unfolding X = partition q  partition
using the1_equality'[OF  q . Uniq (λq' .  q'  reachable_states M1  q  Q q')]
by auto
next
case False
then show ?thesis
unfolding X = partition q  partition
by auto
qed
qed
moreover have "card (insert (states M2 - ( q  reachable_states M1 . Q q)) (Q ` reachable_states M1))  Suc (size_r M1)"
and  "finite (insert (states M2 - ( q  reachable_states M1 . Q q)) (Q ` reachable_states M1))"
and  "card (insert (states M2 - ( q  reachable_states M1 . Q q)) (Q ` reachable_states M1))  size_r M1"
proof -
have "finite (Q ` reachable_states M1)"
using fsm_states_finite[of M1]
by (metis finite_imageI fsm_states_finite restrict_to_reachable_states_simps(2))
moreover have "card (Q ` reachable_states M1) = size_r M1"
proof -
have "card (Q ` reachable_states M1)  size_r M1"
by (metis card_image_le fsm_states_finite restrict_to_reachable_states_simps(2))
moreover have "card (Q ` reachable_states M1)  size_r M1"
using finite (Q ` reachable_states M1)
by (metis (full_types) q. q  reachable_states M1  Q q  {} q2 q1. q1  reachable_states M1; q2  reachable_states M1; q1  q2  Q q1  Q q2 = {} calculation card_eq_0_iff card_union_of_distinct le_0_eq)
ultimately show ?thesis
by simp
qed
ultimately show "card (insert (states M2 - ( q  reachable_states M1 . Q q)) (Q ` reachable_states M1))  Suc (size_r M1)"
and "card (insert (states M2 - ( q  reachable_states M1 . Q q)) (Q ` reachable_states M1))  size_r M1"
show "finite (insert (states M2 - ( q  reachable_states M1 . Q q)) (Q ` reachable_states M1))"
using finite (Q ` reachable_states M1)
by blast
qed
ultimately show "n0  Suc (size_r M1)" unfolding n0
by (meson card_mono le_trans)

have "(Q ` reachable_states M1)  partition ` states M2"
proof
fix x assume "x  (Q ` reachable_states M1)"
then obtain q' where "q'  reachable_states M1" and "x = Q q'"
by blast
then obtain q where "q  Q q'"
using  q . q  reachable_states M1  Q q  {} by blast
then obtain α where "α  A q'" and "q  io_targets M2 α (initial M2)"
unfolding Q by blast
then have "q  states M2"
by (meson io_targets_states subset_iff)

have "q'reachable_states M1. q  Q q'"
using q'  reachable_states M1 q  Q q' by blast
then have "partition q = Q q'"
unfolding partition
using the1_equality'[OF  q . Uniq (λq' .  q'  reachable_states M1  q  Q q'), of q' q] q  Q q' q'  reachable_states M1
by auto
then show "x  partition ` states M2"
using q  states M2 x = Q q'
by blast
qed
then show "n0  size_r M1"
unfolding n0
using finite (insert (states M2 - ( q  reachable_states M1 . Q q)) (Q ` reachable_states M1))
by (metis (full_types) q. q  reachable_states M1  Q q  {} q2 q1. q1  reachable_states M1; q2  reachable_states M1; q1  q2  Q q1  Q q2 = {} partition ` FSM.states M2  insert (FSM.states M2 -  (Q ` reachable_states M1)) (Q ` reachable_states M1) card_mono card_union_of_distinct finite_subset fsm_states_finite restrict_to_reachable_states_simps(2))
qed

moreover have "after_initial M2 τ  ofsm_table M2 partition (m - size_r M1) (after_initial M2 π)"
proof -

define q1 where q1: "q1 = (after_initial M2 π)"
define q2 where q2: "q2 = (after_initial M2 τ)"

have "π  L M2" and "τ  L M2"
using assms(7,8,9) by blast+

have "q1  states M2"
using π  L M2 after_is_state[OF observable M2] unfolding q1 by blast
have "q2  states M2"
using τ  L M2 after_is_state[OF observable M2] unfolding q2 by blast

moreover have " γ . length γ  m - size_r M1  (γ  LS M2 q1) = (γ  LS M2 q2)  (γ  LS M2 q1  after M2 q2 γ  partition (after M2 q1 γ))"
proof -
fix γ :: "('b×'c) list"
assume "length γ  m - size_r M1"

then show "((γ  LS M2 q1) = (γ  LS M2 q2))  (γ  LS M2 q1  after M2 q2 γ  partition (after M2 q1 γ))"
proof (induction γ rule: rev_induct)
case Nil

show ?case
proof

have "([]  LS M2 q1)" and "([]  LS M2 q2)"
using q1  states M2 q2  states M2
by auto
then have "after M2 q1 [] = q1" and "after M2 q2 [] = q2"
unfolding Nil
by auto

obtain α β where "converge M1 α π"
"converge M2 α π"
"converge M1 β τ"
"converge M2 β τ"
"α  SC"
"β  SC"
using assms(15) by blast
then have "α  L M1" and "β  L M1"
by auto

have "α  L M2"
using α  L M1 α  SC L M1  T = L M2  T SC  T by blast
have "β  L M2"
using β  L M1 β  SC L M1  T = L M2  T SC  T by blast

have "([]  LS M2 q1) = ([]  LS M2 (after_initial M2 α))"
using converge M2 α π unfolding q1 converge.simps by simp
also have " = ([]  LS M1 (after_initial M1 α))"
using α  SC L M1  T = L M2  T SC  T
unfolding after_language_iff[OF observable M1 α  L M1]
unfolding after_language_iff[OF observable M2 α  L M2]
unfolding Nil
by auto
also have " = ([]  LS M1 (after_initial M1 β))"
using converge M1 π τ converge M1 α π converge M1 β τ
unfolding converge.simps by blast
also have " = ([]  LS M2 (after_initial M2 β))"
using β  SC L M1  T = L M2  T SC  T
unfolding after_language_iff[OF observable M1 β  L M1]
unfolding after_language_iff[OF observable M2 β  L M2]
unfolding Nil
by auto
also have " = ([]  LS M2 q2)"
using converge M2 β τ unfolding q2 converge.simps by simp
finally show "([]  LS M2 q1) = ([]  LS M2 q2)" .

show "([]  LS M2 q1  after M2 q2 []  partition (after M2 q1 []))"
proof
assume "[]  LS M2 q1"
then have "[]  LS M1 (after_initial M1 α)"
and "[]  LS M1 (after_initial M1 β)"
unfolding ([]  LS M2 q1) = ([]  LS M2 (after_initial M2 α))
([]  LS M2 (after M2 (FSM.initial M2) α)) = ([]  LS M1 (after M1 (FSM.initial M1) α))
([]  LS M1 (after M1 (FSM.initial M1) α)) = ([]  LS M1 (after M1 (FSM.initial M1) β))
by simp+

have "α@[]  L M1"
using []  LS M1 (after_initial M1 α) unfolding after_language_iff[OF observable M1 α  L M1] .
moreover have "β@[]  L M1"
using []  LS M1 (after_initial M1 β) unfolding after_language_iff[OF observable M1 β  L M1] .
moreover have "converge M1 α β"
using converge M1 π τ converge M1 α π converge M1 β τ
unfolding converge.simps by blast
ultimately have "converge M1 (α@[]) (β@[])"
using converge_append[OF observable M1] language_prefix[of β "[]" M1 "initial M1"] by blast

have "(α @ [])  L M2" and "(β @ [])  L M2"
using α@[]  L M1 α  SC β@[]  L M1 β  SCL M1  T = L M2  T SC  T by auto
have "after_initial M1 (α@[])  reachable_states M1"
using observable_after_path[OF observable M1 ]
unfolding reachable_states_def
proof -
have "ps. after M1 (FSM.initial M1) α = target (FSM.initial M1) ps  path M1 (FSM.initial M1) ps"
by (metis (no_types) thesis q io. io  LS M1 q; p. path M1 q p; p_io p = io; target q p = after M1 q io  thesis  thesis α  L M1)
then show "after M1 (FSM.initial M1) (α @ [])  {target (FSM.initial M1) ps |ps. path M1 (FSM.initial M1) ps}"
by auto
qed
have "(α@[])  A (after_initial M1 (α@[]))"
unfolding A
using convergence_minimal[OF assms(3,1) _ α@[]  L M1, of "f (after_initial M1 (α@[]))"]
using f2[OF after_initial M1 (α@[])  reachable_states M1]
using α  SC
unfolding Nil
by (metis (no_types, lifting) Int_iff α  L M1 after M1 (FSM.initial M1) (α @ [])  reachable_states M1 append_Nil2 assms(1) f1 member_filter observable_after_path observable_path_io_target singletonD)
then have "after M2 (FSM.initial M2) (α @ [])  Q (after_initial M1 (α@[]))"
unfolding Q
using observable_io_targets[OF observable M2 (α @ [])  L M2]
unfolding after_io_targets[OF observable M2 (α @ [])  L M2]
by (metis UN_iff insertCI the_elem_eq)
then have "q'reachable_states M1. after M2 (FSM.initial M2) (α @ [])  Q q'"
using after_initial M1 (α@[])  reachable_states M1 by blast
moreover have "(THE q'. q'  reachable_states M1  after M2 (FSM.initial M2) (α @ [])  Q q') = (after_initial M1 (α@[]))"
using after_initial M1 (α@[])  reachable_states M1
using after M2 (FSM.initial M2) (α @ [])  Q (after_initial M1 (α@[]))
by (simp add: q. 1 q'. q'  reachable_states M1  q  Q q' the1_equality')
moreover have "after M2 (FSM.initial M2) (β @ [])  Q (after_initial M1 (α@[]))"
proof -
have "(β@[])  A (after_initial M1 (α@[]))"
using A α @ []  A (after M1 (FSM.initial M1) (α @ [])) β @ []  L M1 β  SC converge M1 (α @ []) (β @ []) unfolding Nil by auto
then show ?thesis
unfolding Q
using observable_io_targets[OF observable M2 (β @ [])  L M2]
unfolding after_io_targets[OF observable M2 (β @ [])  L M2]
by (metis UN_iff insertCI the_elem_eq)
qed
ultimately have "after_initial M2 (β@[])  partition (after_initial M2 (α@[]))"
unfolding partition
by presburger
moreover have "after_initial M2 (α@[]) = after_initial M2 (π@[])"
using converge_append[OF assms(2) converge M2 α π (α @ [])  L M2 π  L M2]
unfolding convergence_minimal[OF assms(4,2) (α @ [])  L M2 converge_extend[OF assms(2) converge M2 α π (α @ [])  L M2 π  L M2]]
.
moreover have "after_initial M2 (β@[]) = after_initial M2 (τ@[])"
using converge_append[OF assms(2) converge M2 β τ (β @ [])  L M2 τ  L M2]
unfolding convergence_minimal[OF assms(4,2) (β @ [])  L M2 converge_extend[OF assms(2) converge M2 β τ (β @ [])  L M2 τ  L M2]]
.
ultimately show "after M2 q2 []  partition (after M2 q1 [])"
unfolding q1 q2
unfolding after_split[OF assms(2) converge_extend[OF assms(2) converge M2 α π (α @ [])  L M2 π  L M2]]
unfolding after_split[OF assms(2) converge_extend[OF assms(2) converge M2 β τ (β @ [])  L M2 τ  L M2]]
by simp
qed
qed
next
case (snoc xy γ)

obtain x y where "xy = (x,y)"
by fastforce

show ?case proof (cases " x' y' . (x',y')  set (γ@[(x,y)])  x'  inputs M1  y'  outputs M1")
case False

have "γ@[(x,y)]  LS M2 q1" and "γ@[(x,y)]  LS M2 q2"
using language_io[of "γ[(x,y)]" M2 _ ] False
unfolding inputs M2 = inputs M1 outputs M2 = outputs M1
by blast+
then show ?thesis
unfolding xy = (x,y)
by blast
next
case True

define s1 where s1: "s1 = (after_initial M1 π)"
define s2 where s2: "s2 = (after_initial M1 τ)"

have "s1  states M1"
using π  L M1  T after_is_state[OF observable M1] unfolding s1 by blast
have "s2  states M1"
using τ  L M1  T after_is_state[OF observable M1] unfolding s2 by blast

show ?thesis proof (cases "γ  LS M1 s1")
case False  (* if γ is not contained in the language of s1, then by application
of the SC it is also not contained in the languages of q1 or q2 *)

obtain io' x' y' io'' where "γ = io' @ [(x', y')] @ io''"
and "io'  LS M1 s1"
and "io' @ [(x', y')]  LS M1 s1"
using language_maximal_contained_prefix_ob[OF False s1  states M1 observable M1]
by blast

have *: "length io' < m - size_r M1"
using length (γ @ [xy])  m - size_r M1
unfolding γ = io' @ [(x', y')] @ io''
by auto
have **: "io'  LS M1 (after M1 (FSM.initial M1) π)"
using io'  LS M1 s1 unfolding s1 .
have "x'  inputs M1" and "y'  outputs M1"
using True
unfolding γ = io' @ [(x', y')] @ io''
by auto

obtain α β where "converge M1 α (π @ io')"
"converge M2 α (π @ io')"
"converge M1 β (τ @ io')"
"converge M2 β (τ @ io')"
"α  SC"
"α @ [(x', y')]  SC"
"β  SC"
"β @ [(x', y')]  SC"
using assms(14)[OF * ** x'  inputs M1 y'  outputs M1]
by blast
then have "α  L M1" and "β  L M1"
by auto

have "π@io'  L M1"
using io'  LS M1 s1 π  L M1  T
using after_language_iff[OF observable M1, of π "initial M1" io']
unfolding s1
by blast
have "converge M1 (π @ io') (τ @ io')"
using converge_append[OF observable M1 converge M1 π τ π@io'  L M1 ]
using τ  L M1  T
by blast

have "(π @ io') @ [(x', y')]  L M1"
using io' @ [(x', y')]  LS M1 s1
using π  L M1  T
using after_language_iff[OF observable M1, of π "initial M1" "io'@[(x',y')]"]
unfolding s1
by auto
then have "[(x',y')]  LS M1 (after_initial M1 α)"
using after_language_iff[OF observable M1 π@io'  L M1, of "[(x',y')]"]
using converge M1 α (π @ io')
unfolding converge.simps
by blast
then have "[(x',y')]  LS M1 (after_initial M1 β)"
using converge M1 (π @ io') (τ @ io') converge M1 α (π @ io') converge M1 β (τ @ io')
unfolding converge.simps
by blast

have "α  L M2"
using α  L M1 α  SC L M1  T = L M2  T SC  T by blast
have "β  L M2"
using β  L M1 β  SC L M1  T = L M2  T SC  T by blast

have "[(x',y')]  LS M2 (after_initial M2 α)"
using α @ [(x', y')]  SC L M1  T = L M2  T SC  T
[(x',y')]  LS M1 (after_initial M1 α)
unfolding after_language_iff[OF observable M1 α  L M1]
unfolding after_language_iff[OF observable M2 α  L M2]
by blast
then have "io'@[(x',y')]  LS M2 q1"
using converge M2 α (π @ io')
unfolding q1 converge.simps
using after_language_append_iff assms(2) by blast
then have "γ@[xy]  LS M2 q1"
unfolding γ = io' @ [(x', y')] @ io''
using language_prefix
by (metis append_assoc)

have "[(x',y')]  LS M2 (after_initial M2 β)"
using β @ [(x', y')]  SC L M1  T = L M2  T SC  T
[(x',y')]  LS M1 (after_initial M1 β)
unfolding after_language_iff[OF observable M1 β  L M1]
unfolding after_language_iff[OF observable M2 β  L M2]
by blast
then have "io'@[(x',y')]  LS M2 q2"
using converge M2 β (τ @ io')
unfolding q2 converge.simps
using after_language_append_iff assms(2) by blast
then have "γ@[xy]  LS M2 q2"
unfolding γ = io' @ [(x', y')] @ io''
using language_prefix
by (metis append_assoc)

then show ?thesis
using γ@[xy]  LS M2 q1
by blast
next
case True

have *: "length γ < m - size_r M1"
using length (γ @ [xy])  m - size_r M1
by auto
have **: "γ  LS M1 (after M1 (FSM.initial M1) π)"
using True unfolding s1 .
have "x  inputs M1" and "y  outputs M1"
using  x' y' . (x',y')  set (γ@[(x,y)])  x'  inputs M1  y'  outputs M1
by auto

obtain α β where "converge M1 α (π @ γ)"
"converge M2 α (π @ γ)"
"converge M1 β (τ @ γ)"
"converge M2 β (τ @ γ)"
"α  SC"
"α @ [xy]  SC"
"β  SC"
"β @ [xy]  SC"
using assms(14)[OF * ** x  inputs M1 y  outputs M1]
unfolding xy = (x,y)
by blast
then have "α  L M1" and "β  L M1"
by auto

have "α  L M2"
using α  L M1 α  SC L M1  T = L M2  T SC  T by blast
have "β  L M2"
using β  L M1 β  SC L M1  T = L M2  T SC  T by blast

have "(π @ γ)  L M2"
using converge M2 α (π @ γ) by auto
have "(τ @ γ)  L M2"
using converge M2 β (τ @ γ) by auto

have "converge M1 (π @ γ) (τ @ γ)"
using converge_append[OF observable M1 converge M1 π τ, of γ]
using converge M1 α (π @ γ) τ  L M1  T
by auto

have "(γ@[xy]  LS M2 q1) = ([xy]  LS M2 (after_initial M2 (π@γ)))"
unfolding q1
using after_language_append_iff[OF observable M2 (π @ γ)  L M2] by auto
also have " = ([xy]  LS M2 (after_initial M2 α))"
using converge M2 α (π @ γ) unfolding q1 converge.simps
by blast
also have " = ([xy]  LS M1 (after_initial M1 α))"
using α@[xy]  SC L M1  T = L M2  T SC  T
unfolding after_language_iff[OF observable M1 α  L M1]
unfolding after_language_iff[OF observable M2 α  L M2]
by blast
also have " = ([xy]  LS M1 (after_initial M1 β))"
using converge M1 (π @ γ) (τ @ γ) converge M1 α (π @ γ) converge M1 β (τ @ γ)
unfolding converge.simps
by blast
also have " = ([xy]  LS M2 (after_initial M2 β))"
using β@[xy]  SC L M1  T = L M2  T SC  T
unfolding after_language_iff[OF observable M1 β  L M1]
unfolding after_language_iff[OF observable M2 β  L M2]
by blast
also have " = ([xy]  LS M2 (after_initial M2 (τ@γ)))"
using converge M2 β (τ @ γ) unfolding q1 converge.simps
by blast
also have " = (γ@[xy]  LS M2 q2)"
unfolding q2
using after_language_append_iff[OF observable M2 (τ @ γ)  L M2] by auto
finally have p1: "(γ@[xy]  LS M2 q1) = (γ@[xy]  LS M2 q2)"
.

moreover have "(γ@[xy]  LS M2 q1  after M2 q2 (γ@[xy])  partition (after M2 q1 (γ@[xy])))"
proof
assume "γ@[xy]  LS M2 q1"
then have "[xy]  LS M1 (after_initial M1 α)"
and "[xy]  LS M1 (after_initial M1 β)"
unfolding (γ@[xy]  LS M2 q1) = ([xy]  LS M2 (after_initial M2 (π@γ)))
([xy]  LS M2 (after_initial M2 (π@γ))) = ([xy]  LS M2 (after_initial M2 α))
([xy]  LS M2 (after M2 (FSM.initial M2) α)) = ([xy]  LS M1 (after M1 (FSM.initial M1) α))
([xy]  LS M1 (after M1 (FSM.initial M1) α)) = ([xy]  LS M1 (after M1 (FSM.initial M1) β))
by simp+

have "α@[xy]  L M1"
using [xy]  LS M1 (after_initial M1 α) unfolding after_language_iff[OF observable M1 α  L M1] .
moreover have "β@[xy]  L M1"
using [xy]  LS M1 (after_initial M1 β) unfolding after_language_iff[OF observable M1 β  L M1] .
moreover have "converge M1 α β"
using converge M1 (π @ γ) (τ @ γ) converge M1 α (π @ γ) converge M1 β (τ @ γ)
unfolding converge.simps
by blast
ultimately have "converge M1 (α@[xy]) (β@[xy])"
using converge_append[OF observable M1] language_prefix[of β "[xy]" M1 "initial M1"] by blast

have "(α @ [xy])  L M2" and "(β @ [xy])  L M2"
using α@[xy]  L M1 α@[xy]  SC β@[xy]  L M1 β@[xy]  SCL M1  T = L M2  T SC  T  by blast+
have "after_initial M1 (α@[xy])  reachable_states M1"
using observable_after_path[OF observable M1 α@[xy]  L M1]
unfolding reachable_states_def
by (metis (mono_tags, lifting) mem_Collect_eq)
have "(α@[xy])  A (after_initial M1 (α@[xy]))"
unfolding A
using convergence_minimal[OF assms(3,1) _ α@[xy]  L M1, of "f (after_initial M1 (α@[xy]))"]
using f2[OF after_initial M1 (α@[xy])  reachable_states M1]
using α@[xy]  SC
by (metis (no_types, lifting) Int_iff α @ [xy]  L M1 after M1 (FSM.initial M1) (α @ [xy])  reachable_states M1 assms(1) f1 member_filter observable_after_path observable_path_io_target singletonD)
then have "after M2 (FSM.initial M2) (α @ [xy])  Q (after_initial M1 (α@[xy]))"
unfolding Q
using observable_io_targets[OF observable M2 (α @ [xy])  L M2]
unfolding after_io_targets[OF observable M2 (α @ [xy])  L M2]
by (metis UN_iff insertCI the_elem_eq)
then have "q'reachable_states M1. after M2 (FSM.initial M2) (α @ [xy])  Q q'"
using after_initial M1 (α@[xy])  reachable_states M1 by blast
moreover have "(THE q'. q'  reachable_states M1  after M2 (FSM.initial M2) (α @ [xy])  Q q') = (after_initial M1 (α@[xy]))"
using after_initial M1 (α@[xy])  reachable_states M1
using after M2 (FSM.initial M2) (α @ [xy])  Q (after_initial M1 (α@[xy]))
by (simp add: q. 1 q'. q'  reachable_states M1  q  Q q' the1_equality')
moreover have "after M2 (FSM.initial M2) (β @ [xy])  Q (after_initial M1 (α@[xy]))"
proof -
have "(β@[xy])  A (after_initial M1 (α@[xy]))"
using A α @ [xy]  A (after M1 (FSM.initial M1) (α @ [xy])) β @ [xy]  L M1 β @ [xy]  SC converge M1 (α @ [xy]) (β @ [xy]) by auto
then show ?thesis
unfolding Q
using observable_io_targets[OF observable M2 (β @ [xy])  L M2]
unfolding after_io_targets[OF observable M2 (β @ [xy])  L M2]
by (metis UN_iff insertCI the_elem_eq)
qed
ultimately have "after_initial M2 (β@[xy])  partition (after_initial M2 (α@[xy]))"
unfolding partition
by presburger
moreover have "after_initial M2 (α@[xy]) = after_initial M2 ((π@γ)@[xy])"
using converge_append[OF assms(2) converge M2 α (π@γ) (α @ [xy])  L M2 (π@γ)  L M2]
unfolding convergence_minimal[OF assms(4,2) (α @ [xy])  L M2 converge_extend[OF assms(2) converge M2 α (π@γ) (α @ [xy])  L M2 (π@γ)  L M2]]
.
moreover have "after_initial M2 (β@[xy]) = after_initial M2 ((τ@γ)@[xy])"
using converge_append[OF assms(2) converge M2 β (τ@γ) (β @ [xy])  L M2 (τ@γ)  L M2]
unfolding convergence_minimal[OF assms(4,2) (β @ [xy])  L M2 converge_extend[OF assms(2) converge M2 β (τ@γ) (β @ [xy])  L M2 (τ@γ)  L M2]]
.
ultimately show "after M2 q2 (γ@[xy])  partition (after M2 q1 (γ@[xy]))"
unfolding q1 q2
unfolding after_split[OF assms(2) converge_extend[OF assms(2) converge M2 α (π@γ) (α @ [xy])  L M2 (π@γ)  L M2]]
unfolding after_split[OF assms(2) converge_extend[OF assms(2) converge M2 β (τ@γ) (β @ [xy])  L M2 (τ@γ)  L M2]]
by (metis γ @ [xy]  LS M2 q1 π @ γ  L M2 τ @ γ  L M2 after M2 (after M2 (FSM.initial M2) (π @ γ)) [xy] = after M2 (FSM.initial M2) ((π @ γ) @ [xy]) after M2 (after M2 (FSM.initial M2) (τ @ γ)) [xy] = after M2 (FSM.initial M2) ((τ @ γ) @ [xy]) after_split assms(2) p1 q1 q2)
qed

ultimately show ?thesis
by blast
qed
qed
qed
qed

ultimately show ?thesis
using ofsm_table_set_observable[OF observable M2 q1  states M2 is_eq, of "m - size_r M1"]
unfolding q1 q2
by blast
qed

ultimately have "after M2 (FSM.initial M2) τ  ofsm_table M2 partition (m - n0) (after M2 (FSM.initial M2) π)"
using ofsm_table_subset[OF size_r M1  n0, of M2 partition "initial M2"]
by (meson diff_le_mono2 in_mono ofsm_table_subset)

moreover have "after M2 (FSM.initial M2) π  states M2"
by (metis IntD1 after_is_state assms(2) assms(7) assms(8))

ultimately have "after M2 (FSM.initial M2) τ  ofsm_table_fix M2 partition 0 (after M2 (FSM.initial M2) π)"
using ofsm_table_fix_partition_fixpoint[OF equivalence_relation_on_states M2 partition size M2  m, of "after M2 (FSM.initial M2) π"]
unfolding n0
by blast

then have "LS M2 (after_initial M2 τ)