[STATEMENT]
lemma distinguish_from_set_establishes_convergence :
  assumes "observable M1"
      and "observable M2"
      and "minimal M1"
      and "minimal M2"
      and "size_r M1 \<le> m"
      and "size M2 \<le> m"
      and "inputs M2 = inputs M1"
      and "outputs M2 = outputs M1"
      and "is_state_cover_assignment M1 V"
      and "preserves_divergence M1 M2 (V ` reachable_states M1)"
      and "L M1 \<inter> (V ` reachable_states M1) = L M2 \<inter> V ` reachable_states M1"
      and "converge M1 u v"
      and "u \<in> L M2"
      and "v \<in> L M2"
      and "convergence_graph_lookup_invar M1 M2 cg_lookup G"
      and "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
      and "\<And> q1 q2 . q1 \<in> states M1 \<Longrightarrow> q2 \<in> states M1 \<Longrightarrow> q1 \<noteq> q2 \<Longrightarrow> distinguishes M1 q1 q2 (get_distinguishing_trace q1 q2)"
      and "L M1 \<inter> set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u=v))) = L M2 \<inter> set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u=v)))"
      and "\<And> T w u' uBest lBest . fst (append_heuristic T w (uBest,lBest) u') \<in> {u',uBest}"
shows "converge M2 u v"
  and "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u=v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M2 u v &&& convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. converge M2 u v
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
have d1: "V ` reachable_states M1 \<subseteq> list.set (map V (reachable_states_as_list M1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> list.set (map V (reachable_states_as_list M1))
[PROOF STEP]
using reachable_states_as_list_set
[PROOF STATE]
proof (prove)
using this:
list.set (reachable_states_as_list ?M) = reachable_states ?M

goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> list.set (map V (reachable_states_as_list M1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V ` reachable_states M1 \<subseteq> list.set (map V (reachable_states_as_list M1))

goal (2 subgoals):
 1. converge M2 u v
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
have d2: "preserves_divergence M1 M2 (list.set (map V (reachable_states_as_list M1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set (map V (reachable_states_as_list M1)))
[PROOF STEP]
using assms(10) reachable_states_as_list_set
[PROOF STATE]
proof (prove)
using this:
preserves_divergence M1 M2 (V ` reachable_states M1)
list.set (reachable_states_as_list ?M) = reachable_states ?M

goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set (map V (reachable_states_as_list M1)))
[PROOF STEP]
by (metis image_set)
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (list.set (map V (reachable_states_as_list M1)))

goal (2 subgoals):
 1. converge M2 u v
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
have d3: "(\<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
assume "w \<in> list.set (map V (reachable_states_as_list M1))"
[PROOF STATE]
proof (state)
this:
w \<in> list.set (map V (reachable_states_as_list M1))

goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> list.set (map V (reachable_states_as_list M1))
[PROOF STEP]
have "w \<in> V ` reachable_states M1"
[PROOF STATE]
proof (prove)
using this:
w \<in> list.set (map V (reachable_states_as_list M1))

goal (1 subgoal):
 1. w \<in> V ` reachable_states M1
[PROOF STEP]
using reachable_states_as_list_set
[PROOF STATE]
proof (prove)
using this:
w \<in> list.set (map V (reachable_states_as_list M1))
list.set (reachable_states_as_list ?M) = reachable_states ?M

goal (1 subgoal):
 1. w \<in> V ` reachable_states M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> V ` reachable_states M1

goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w \<in> V ` reachable_states M1

goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
have "w \<in> L M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> L M1
[PROOF STEP]
by (metis assms(1) assms(9) calculation image_iff state_cover_assignment_after(1))
[PROOF STATE]
proof (state)
this:
w \<in> L M1

goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w \<in> V ` reachable_states M1
w \<in> L M1
[PROOF STEP]
have "w \<in> L M2"
[PROOF STATE]
proof (prove)
using this:
w \<in> V ` reachable_states M1
w \<in> L M1

goal (1 subgoal):
 1. w \<in> L M2
[PROOF STEP]
using assms(11)
[PROOF STATE]
proof (prove)
using this:
w \<in> V ` reachable_states M1
w \<in> L M1
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1

goal (1 subgoal):
 1. w \<in> L M2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<in> L M2

goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
have "converge M1 w w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M1 w w
[PROOF STEP]
using \<open>w \<in> L M1\<close>
[PROOF STATE]
proof (prove)
using this:
w \<in> L M1

goal (1 subgoal):
 1. converge M1 w w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
converge M1 w w

goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
converge M1 w w

goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
have "converge M2 w w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M2 w w
[PROOF STEP]
using \<open>w \<in> L M2\<close>
[PROOF STATE]
proof (prove)
using this:
w \<in> L M2

goal (1 subgoal):
 1. converge M2 w w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
converge M2 w w

goal (1 subgoal):
 1. \<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
converge M1 w w
converge M2 w w
[PROOF STEP]
show "\<exists>w'. converge M1 w w' \<and> converge M2 w w'"
[PROOF STATE]
proof (prove)
using this:
converge M1 w w
converge M2 w w

goal (1 subgoal):
 1. \<exists>w'. converge M1 w w' \<and> converge M2 w w'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>w'. converge M1 w w' \<and> converge M2 w w'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> \<exists>w'. converge M1 ?w w' \<and> converge M2 ?w w'

goal (2 subgoals):
 1. converge M2 u v
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
have "list.set (map V (reachable_states_as_list M1)) = V ` reachable_states M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (map V (reachable_states_as_list M1)) = V ` reachable_states M1
[PROOF STEP]
using reachable_states_as_list_set
[PROOF STATE]
proof (prove)
using this:
list.set (reachable_states_as_list ?M) = reachable_states ?M

goal (1 subgoal):
 1. list.set (map V (reachable_states_as_list M1)) = V ` reachable_states M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list.set (map V (reachable_states_as_list M1)) = V ` reachable_states M1

goal (2 subgoals):
 1. converge M2 u v
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
have prop1: "\<And>\<gamma> x y.
     length (\<gamma> @ [(x, y)]) \<le> (m - size_r M1) \<Longrightarrow>
     \<gamma> \<in> LS M1 (after_initial M1 u) \<Longrightarrow>
     x \<in> FSM.inputs M1 \<Longrightarrow>
     y \<in> FSM.outputs M1 \<Longrightarrow>
     L M1 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) =
     L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) \<and>
     preserves_divergence M1 M2
      (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))})"
  and prop2: "preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {u, v})"
  and prop3: "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u=v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<gamma> x y. \<lbrakk>length (\<gamma> @ [(x, y)]) \<le> m - size_r M1; \<gamma> \<in> LS M1 (after_initial M1 u); x \<in> FSM.inputs M1; y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> L M1 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) \<and> preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))})) &&& preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {u, v}) &&& convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
using distinguish_from_set_properties[OF assms(1-4,7,8,9) d1 d2 d3 assms(12-19)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> w \<in> list.set (map V (reachable_states_as_list M1)); \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> \<forall>\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> m - size_r M1 \<longrightarrow> \<gamma> \<in> LS M1 (after_initial M1 u) \<longrightarrow> x \<in> FSM.inputs M1 \<longrightarrow> y \<in> FSM.outputs M1 \<longrightarrow> L M1 \<inter> (list.set (map V (reachable_states_as_list M1)) \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) = L M2 \<inter> (list.set (map V (reachable_states_as_list M1)) \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) \<and> preserves_divergence M1 M2 (list.set (map V (reachable_states_as_list M1)) \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))})
\<lbrakk>\<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> w \<in> list.set (map V (reachable_states_as_list M1)); \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (map V (reachable_states_as_list M1)) \<union> {u, v})
\<lbrakk>\<And>w. w \<in> list.set (map V (reachable_states_as_list M1)) \<Longrightarrow> w \<in> list.set (map V (reachable_states_as_list M1)); \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))

goal (1 subgoal):
 1. (\<And>\<gamma> x y. \<lbrakk>length (\<gamma> @ [(x, y)]) \<le> m - size_r M1; \<gamma> \<in> LS M1 (after_initial M1 u); x \<in> FSM.inputs M1; y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> L M1 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) \<and> preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))})) &&& preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {u, v}) &&& convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
unfolding \<open>list.set (map V (reachable_states_as_list M1)) = V ` reachable_states M1\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>w. w \<in> V ` reachable_states M1 \<Longrightarrow> w \<in> V ` reachable_states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> \<forall>\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> m - size_r M1 \<longrightarrow> \<gamma> \<in> LS M1 (after_initial M1 u) \<longrightarrow> x \<in> FSM.inputs M1 \<longrightarrow> y \<in> FSM.outputs M1 \<longrightarrow> L M1 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) \<and> preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))})
\<lbrakk>\<And>w. w \<in> V ` reachable_states M1 \<Longrightarrow> w \<in> V ` reachable_states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {u, v})
\<lbrakk>\<And>w. w \<in> V ` reachable_states M1 \<Longrightarrow> w \<in> V ` reachable_states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))

goal (1 subgoal):
 1. (\<And>\<gamma> x y. \<lbrakk>length (\<gamma> @ [(x, y)]) \<le> m - size_r M1; \<gamma> \<in> LS M1 (after_initial M1 u); x \<in> FSM.inputs M1; y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> L M1 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) \<and> preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))})) &&& preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {u, v}) &&& convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
by presburger+
[PROOF STATE]
proof (state)
this:
\<lbrakk>length (?\<gamma> @ [(?x, ?y)]) \<le> m - size_r M1; ?\<gamma> \<in> LS M1 (after_initial M1 u); ?x \<in> FSM.inputs M1; ?y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> L M1 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))}) \<and> preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))})
preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {u, v})
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))

goal (2 subgoals):
 1. converge M2 u v
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length (?\<gamma> @ [(?x, ?y)]) \<le> m - size_r M1; ?\<gamma> \<in> LS M1 (after_initial M1 u); ?x \<in> FSM.inputs M1; ?y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> L M1 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))}) \<and> preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))})
preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {u, v})
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
show "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u=v)))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length (?\<gamma> @ [(?x, ?y)]) \<le> m - size_r M1; ?\<gamma> \<in> LS M1 (after_initial M1 u); ?x \<in> FSM.inputs M1; ?y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> L M1 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))}) \<and> preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {u, v} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))})
preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {u, v})
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert get_distinguishing_trace u v (map V (reachable_states_as_list M1)) k (m - size_r M1) completeInputTraces append_heuristic (u = v)))

goal (1 subgoal):
 1. converge M2 u v
[PROOF STEP]
show "converge M2 u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M2 u v
[PROOF STEP]
using establish_convergence_from_pass[OF assms(1-9,11-14) prop1 prop2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<gamma> x y. \<lbrakk>length (\<gamma> @ [(x, y)]) \<le> m - size_r M1; \<gamma> \<in> LS M1 (after_initial M1 u); x \<in> FSM.inputs M1; y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> length (\<gamma> @ [(x, y)]) \<le> m - size_r M1; \<And>\<gamma> x y. \<lbrakk>length (\<gamma> @ [(x, y)]) \<le> m - size_r M1; \<gamma> \<in> LS M1 (after_initial M1 u); x \<in> FSM.inputs M1; y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> \<gamma> \<in> LS M1 (after_initial M1 u); \<And>\<gamma> x y. \<lbrakk>length (\<gamma> @ [(x, y)]) \<le> m - size_r M1; \<gamma> \<in> LS M1 (after_initial M1 u); x \<in> FSM.inputs M1; y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> x \<in> FSM.inputs M1; \<And>\<gamma> x y. \<lbrakk>length (\<gamma> @ [(x, y)]) \<le> m - size_r M1; \<gamma> \<in> LS M1 (after_initial M1 u); x \<in> FSM.inputs M1; y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> converge M2 u v

goal (1 subgoal):
 1. converge M2 u v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
converge M2 u v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma establish_convergence_dynamic_verifies_transition :
  assumes "\<And> q1 q2 . q1 \<in> states M1 \<Longrightarrow> q2 \<in> states M1 \<Longrightarrow> q1 \<noteq> q2 \<Longrightarrow> distinguishes M1 q1 q2 (dist_fun q1 q2)"
  shows "verifies_transition (establish_convergence_dynamic b c dist_fun) M1 M2 V T0 cg_insert cg_lookup"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verifies_transition (establish_convergence_dynamic b c dist_fun) M1 M2 V T0 cg_insert cg_lookup
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. verifies_transition (establish_convergence_dynamic b c dist_fun) M1 M2 V T0 cg_insert cg_lookup
[PROOF STEP]
have *:"\<And> (M1::('a::linorder,'b::linorder,'c::linorder) fsm) V T (G::'d) cg_insert cg_lookup m t. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup m t. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
using distinguish_from_set_subset
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (distinguish_from_set ?M ?V ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?v ?X ?k ?depth ?completeInputTraces ?append_heuristic ?u_is_v))

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup m t. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
unfolding establish_convergence_dynamic_def
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (distinguish_from_set ?M ?V ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?v ?X ?k ?depth ?completeInputTraces ?append_heuristic ?u_is_v))

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup m t. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) False))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))

goal (1 subgoal):
 1. verifies_transition (establish_convergence_dynamic b c dist_fun) M1 M2 V T0 cg_insert cg_lookup
[PROOF STEP]
have ***:"\<And> (M1::('a::linorder,'b::linorder,'c::linorder) fsm) V T (G::'d) cg_insert cg_lookup m t. finite_tree T \<longrightarrow> finite_tree (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup m t. finite_tree T \<longrightarrow> finite_tree (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
using distinguish_from_set_finite
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (distinguish_from_set ?M ?V ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?v ?X ?k ?depth ?completeInputTraces ?append_heuristic ?u_is_v))

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup m t. finite_tree T \<longrightarrow> finite_tree (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
unfolding establish_convergence_dynamic_def
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (distinguish_from_set ?M ?V ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?v ?X ?k ?depth ?completeInputTraces ?append_heuristic ?u_is_v))

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup m t. finite_tree T \<longrightarrow> finite_tree (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) False))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite_tree ?T \<longrightarrow> finite_tree (fst (establish_convergence_dynamic b c dist_fun ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))

goal (1 subgoal):
 1. verifies_transition (establish_convergence_dynamic b c dist_fun) M1 M2 V T0 cg_insert cg_lookup
[PROOF STEP]
have **:"\<And> V T (G::'d) cg_insert cg_lookup m t.
        observable M1 \<Longrightarrow>
        observable M2 \<Longrightarrow>
        minimal M1 \<Longrightarrow>
        minimal M2 \<Longrightarrow>
        size_r M1 \<le> m \<Longrightarrow>
        FSM.size M2 \<le> m \<Longrightarrow>
        FSM.inputs M2 = FSM.inputs M1 \<Longrightarrow>
        FSM.outputs M2 = FSM.outputs M1 \<Longrightarrow>
        is_state_cover_assignment M1 V \<Longrightarrow>
        preserves_divergence M1 M2 (V ` reachable_states M1) \<Longrightarrow>
        V ` reachable_states M1 \<subseteq> set T \<Longrightarrow>
        t \<in> FSM.transitions M1 \<Longrightarrow>
        t_source t \<in> reachable_states M1 \<Longrightarrow>
        ((V (t_source t)) @ [(t_input t,t_output t)]) \<noteq> (V (t_target t)) \<Longrightarrow>
        V (t_source t) @ [(t_input t, t_output t)] \<in> L M2 \<Longrightarrow>
        convergence_graph_lookup_invar M1 M2 cg_lookup G \<Longrightarrow>
        convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<Longrightarrow>
        L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) =
        L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) \<Longrightarrow>
        converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and>
        convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
fix G :: 'd
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
fix V T cg_insert cg_lookup m t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a01: "observable M1"
[PROOF STATE]
proof (state)
this:
observable M1

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a02: "observable M2"
[PROOF STATE]
proof (state)
this:
observable M2

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a03: "minimal M1"
[PROOF STATE]
proof (state)
this:
minimal M1

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a04: "minimal M2"
[PROOF STATE]
proof (state)
this:
minimal M2

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a05: "size_r M1 \<le> m"
[PROOF STATE]
proof (state)
this:
size_r M1 \<le> m

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a06: "FSM.size M2 \<le> m"
[PROOF STATE]
proof (state)
this:
FSM.size M2 \<le> m

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a07: "FSM.inputs M2 = FSM.inputs M1"
[PROOF STATE]
proof (state)
this:
FSM.inputs M2 = FSM.inputs M1

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a08: "FSM.outputs M2 = FSM.outputs M1"
[PROOF STATE]
proof (state)
this:
FSM.outputs M2 = FSM.outputs M1

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a09: "is_state_cover_assignment M1 V"
[PROOF STATE]
proof (state)
this:
is_state_cover_assignment M1 V

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a10: "preserves_divergence M1 M2 (V ` reachable_states M1)"
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (V ` reachable_states M1)

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a11: "V ` reachable_states M1 \<subseteq> set T"
[PROOF STATE]
proof (state)
this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set T

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a12: "t \<in> FSM.transitions M1"
[PROOF STATE]
proof (state)
this:
t \<in> FSM.transitions M1

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a13: "t_source t \<in> reachable_states M1"
[PROOF STATE]
proof (state)
this:
t_source t \<in> reachable_states M1

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a14: "V (t_source t) @ [(t_input t, t_output t)] \<in> L M2"
[PROOF STATE]
proof (state)
this:
V (t_source t) @ [(t_input t, t_output t)] \<in> L M2

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a15: "convergence_graph_lookup_invar M1 M2 cg_lookup G"
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup G

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a16: "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
[PROOF STATE]
proof (state)
this:
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a17: "L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a18: "((V (t_source t)) @ [(t_input t,t_output t)]) \<noteq> (V (t_target t))"
[PROOF STATE]
proof (state)
this:
V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t)

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
let ?heuristic = "(if c then append_heuristic_input M1 else append_heuristic_io)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
have d2: "converge M1 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M1 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[PROOF STEP]
using state_cover_transition_converges[OF a01 a09 a12 a13]
[PROOF STATE]
proof (prove)
using this:
converge M1 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))

goal (1 subgoal):
 1. converge M1 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
converge M1 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
have d1: "L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1
[PROOF STEP]
using a11 a17 *[of T M1 V G cg_insert cg_lookup m t]
[PROOF STATE]
proof (prove)
using this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set T
L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))

goal (1 subgoal):
 1. L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1
[PROOF STEP]
have d3: "V (t_target t) \<in> L M2"
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1

goal (1 subgoal):
 1. V (t_target t) \<in> L M2
[PROOF STEP]
using a11 is_state_cover_assignment_language[OF a09, of "t_target t"] reachable_states_next[OF a13 a12]
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1
V ` reachable_states M1 \<subseteq> Prefix_Tree.set T
t_target t \<in> reachable_states M1 \<Longrightarrow> V (t_target t) \<in> L M1
t_source t = t_source t \<Longrightarrow> t_target t \<in> reachable_states M1

goal (1 subgoal):
 1. V (t_target t) \<in> L M2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V (t_target t) \<in> L M2

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
have d5: "L M1 \<inter> Prefix_Tree.set  (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * size M1) (m - size_r M1) b ?heuristic (((V (t_source t)) @ [(t_input t,t_output t)]) = (V (t_target t))))) = L M2 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * size M1) (m - size_r M1) b ?heuristic (((V (t_source t)) @ [(t_input t,t_output t)]) = (V (t_target t)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)))) = L M2 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t))))
[PROOF STEP]
using a17 a18
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t)

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)))) = L M2 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t))))
[PROOF STEP]
unfolding establish_convergence_dynamic_def
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) False)) = L M2 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) False))
V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t)

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)))) = L M2 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t))))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)))) = L M2 \<inter> Prefix_Tree.set (fst (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t))))

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
have d6: "(\<And>T w u' uBest lBest. fst (?heuristic T w (uBest, lBest) u') \<in> {u', uBest})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T w u' uBest lBest. fst ((if c then append_heuristic_input M1 else append_heuristic_io) T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
using append_heuristic_input_in[of M1] append_heuristic_io_in
[PROOF STATE]
proof (prove)
using this:
fst (append_heuristic_input M1 ?T ?w (?uBest, ?lBest) ?u') \<in> {?u', ?uBest}
fst (append_heuristic_io ?T ?w (?uBest, ?lBest) ?u') \<in> {?u', ?uBest}

goal (1 subgoal):
 1. \<And>T w u' uBest lBest. fst ((if c then append_heuristic_input M1 else append_heuristic_io) T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
fst ((if c then append_heuristic_input M1 else append_heuristic_io) ?T ?w (?uBest, ?lBest) ?u') \<in> {?u', ?uBest}

goal (1 subgoal):
 1. \<And>V T G cg_insert cg_lookup m t. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; preserves_divergence M1 M2 (V ` reachable_states M1); V ` reachable_states M1 \<subseteq> Prefix_Tree.set T; t \<in> FSM.transitions M1; t_source t \<in> reachable_states M1; V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t); V (t_source t) @ [(t_input t, t_output t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
show "converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and>
          convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
using distinguish_from_set_establishes_convergence[OF a01 a02 a03 a04 a05 a06 a07 a08 a09 a10 d1 d2 a14 d3 a15 a16 assms d5 d6] a18
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
\<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t))))
V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t)

goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
unfolding establish_convergence_dynamic_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
\<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) (V (t_source t) @ [(t_input t, t_output t)] = V (t_target t))))
V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t)

goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distinguish_from_set M1 V T G cg_lookup cg_insert dist_fun (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) (map V (reachable_states_as_list M1)) (2 * FSM.size M1) (m - size_r M1) b (if c then append_heuristic_input M1 else append_heuristic_io) False))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> ?m; FSM.size M2 \<le> ?m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 ?V; preserves_divergence M1 M2 (?V ` reachable_states M1); ?V ` reachable_states M1 \<subseteq> Prefix_Tree.set ?T; ?t \<in> FSM.transitions M1; t_source ?t \<in> reachable_states M1; ?V (t_source ?t) @ [(t_input ?t, t_output ?t)] \<noteq> ?V (t_target ?t); ?V (t_source ?t) @ [(t_input ?t, t_output ?t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 ?cg_lookup ?G; convergence_graph_insert_invar M1 M2 ?cg_lookup ?cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))\<rbrakk> \<Longrightarrow> converge M2 (?V (t_source ?t) @ [(t_input ?t, t_output ?t)]) (?V (t_target ?t)) \<and> convergence_graph_lookup_invar M1 M2 ?cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))

goal (1 subgoal):
 1. verifies_transition (establish_convergence_dynamic b c dist_fun) M1 M2 V T0 cg_insert cg_lookup
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verifies_transition (establish_convergence_dynamic b c dist_fun) M1 M2 V T0 cg_insert cg_lookup
[PROOF STEP]
unfolding verifies_transition_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>T G m t. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> size_r M1 \<le> m \<longrightarrow> FSM.size M2 \<le> m \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<longrightarrow> V ` reachable_states M1 \<subseteq> Prefix_Tree.set T \<longrightarrow> t \<in> FSM.transitions M1 \<longrightarrow> t_source t \<in> reachable_states M1 \<longrightarrow> V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t) \<longrightarrow> V (t_source t) @ [(t_input t, t_output t)] \<in> L M2 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup G \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) \<longrightarrow> Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set T \<longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)))
[PROOF STEP]
using * *** **
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))
finite_tree ?T \<longrightarrow> finite_tree (fst (establish_convergence_dynamic b c dist_fun ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))
\<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> ?m; FSM.size M2 \<le> ?m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 ?V; preserves_divergence M1 M2 (?V ` reachable_states M1); ?V ` reachable_states M1 \<subseteq> Prefix_Tree.set ?T; ?t \<in> FSM.transitions M1; t_source ?t \<in> reachable_states M1; ?V (t_source ?t) @ [(t_input ?t, t_output ?t)] \<noteq> ?V (t_target ?t); ?V (t_source ?t) @ [(t_input ?t, t_output ?t)] \<in> L M2; convergence_graph_lookup_invar M1 M2 ?cg_lookup ?G; convergence_graph_insert_invar M1 M2 ?cg_lookup ?cg_insert; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))\<rbrakk> \<Longrightarrow> converge M2 (?V (t_source ?t) @ [(t_input ?t, t_output ?t)]) (?V (t_target ?t)) \<and> convergence_graph_lookup_invar M1 M2 ?cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))

goal (1 subgoal):
 1. \<forall>T G m t. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t))) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> size_r M1 \<le> m \<longrightarrow> FSM.size M2 \<le> m \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<longrightarrow> V ` reachable_states M1 \<subseteq> Prefix_Tree.set T \<longrightarrow> t \<in> FSM.transitions M1 \<longrightarrow> t_source t \<in> reachable_states M1 \<longrightarrow> V (t_source t) @ [(t_input t, t_output t)] \<noteq> V (t_target t) \<longrightarrow> V (t_source t) @ [(t_input t, t_output t)] \<in> L M2 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup G \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)) \<longrightarrow> Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set T \<longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_dynamic b c dist_fun M1 V T G cg_insert cg_lookup m t)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
verifies_transition (establish_convergence_dynamic b c dist_fun) M1 M2 V T0 cg_insert cg_lookup

goal:
No subgoals!
[PROOF STEP]
qed