[STATEMENT]
lemma establish_convergence_static_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 "t \<in> transitions M1"
      and "t_source t \<in> reachable_states M1"
      and "is_state_cover_assignment M1 V"
      and "V (t_source t) @ [(t_input t, t_output t)] \<in> L M2"
      and "V ` reachable_states M1 \<subseteq> set T"
      and "preserves_divergence M1 M2 (V ` reachable_states M1)"
      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> \<exists> io . \<forall> k1 k2 . io \<in> set (dist_fun k1 q1) \<inter> set (dist_fun k2 q2) \<and> distinguishes M1 q1 q2 io"
      and "\<And> q . q \<in> reachable_states M1 \<Longrightarrow> set (dist_fun 0 q) \<subseteq> set (after T (V q))"
      and "\<And> q k . q \<in> states M1 \<Longrightarrow> finite_tree (dist_fun k q)"
      and "L M1 \<inter> set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))"
shows "converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))"
(is "converge M2 ?u ?v")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[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})"
[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 (V (t_source t) @ [(t_input t, t_output t)])); 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> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<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> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))})) &&& preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)})
[PROOF STEP]
using establish_convergence_static_properties(1,2)[OF assms(1-4,7-20)]
[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; \<And>q. q \<in> reachable_states M1 \<Longrightarrow> q \<in> reachable_states M1; \<And>q k. q \<in> FSM.states M1 \<Longrightarrow> q \<in> FSM.states M1\<rbrakk> \<Longrightarrow> \<forall>\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> m - size_r M1 \<longrightarrow> \<gamma> \<in> LS M1 (after_initial M1 (V (t_source t) @ [(t_input t, t_output t)])) \<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> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<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> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))})
\<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; \<And>q. q \<in> reachable_states M1 \<Longrightarrow> q \<in> reachable_states M1; \<And>q k. q \<in> FSM.states M1 \<Longrightarrow> q \<in> FSM.states M1\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)})

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 (V (t_source t) @ [(t_input t, t_output t)])); 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> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<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> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<and> \<omega>' \<in> list.set (prefixes (\<gamma> @ [(x, y)]))})) &&& preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)})
[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 (V (t_source t) @ [(t_input t, t_output t)])); ?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> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))}) = L M2 \<inter> (V ` reachable_states M1 \<union> {\<omega> @ \<omega>' |\<omega> \<omega>'. \<omega> \<in> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<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> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)} \<and> \<omega>' \<in> list.set (prefixes (?\<gamma> @ [(?x, ?y)]))})
preserves_divergence M1 M2 (V ` reachable_states M1 \<union> {V (t_source t) @ [(t_input t, t_output t)], V (t_target t)})

goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[PROOF STEP]
have "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 assms(13,20)
[PROOF STATE]
proof (prove)
using this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set T
L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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]
using establish_convergence_static_subset[of T dist_fun 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_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static 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. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target 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 "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]
by (metis Int_iff assms(10) assms(11) assms(9) imageI is_state_cover_assignment_language reachable_states_next)
[PROOF STATE]
proof (state)
this:
V (t_target t) \<in> L M2

goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[PROOF STEP]
have "converge M1 ?u ?v"
[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 assms(1,11,9,10)]
[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. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[PROOF STEP]
using establish_convergence_from_pass[OF assms(1-8,11) \<open>L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1\<close> \<open>converge M1 ?u ?v\<close> \<open>V (t_source t) @ [(t_input t, t_output t)] \<in> L M2\<close> \<open>V (t_target t) \<in> L M2\<close> 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 (V (t_source t) @ [(t_input t, t_output t)])); 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 (V (t_source t) @ [(t_input t, t_output t)])); x \<in> FSM.inputs M1; y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> \<gamma> \<in> LS M1 (after_initial M1 (V (t_source t) @ [(t_input t, t_output t)])); \<And>\<gamma> x y. \<lbrakk>length (\<gamma> @ [(x, y)]) \<le> m - size_r M1; \<gamma> \<in> LS M1 (after_initial M1 (V (t_source t) @ [(t_input t, t_output t)])); 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 (V (t_source t) @ [(t_input t, t_output t)])); x \<in> FSM.inputs M1; y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> y \<in> FSM.outputs M1\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma establish_convergence_static_verifies_transition :
  assumes "\<And> q1 q2 . q1 \<in> states M1 \<Longrightarrow> q2 \<in> states M1 \<Longrightarrow> q1 \<noteq> q2 \<Longrightarrow> \<exists> io . \<forall> k1 k2 . io \<in> set (dist_fun k1 q1) \<inter> set (dist_fun k2 q2) \<and> distinguishes M1 q1 q2 io"
      and "\<And> q k . q \<in> states M1 \<Longrightarrow> finite_tree (dist_fun k q)"
shows "verifies_transition (establish_convergence_static dist_fun) M1 M2 V (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) cg_insert cg_lookup"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verifies_transition (establish_convergence_static dist_fun) M1 M2 V (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) cg_insert cg_lookup
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. verifies_transition (establish_convergence_static dist_fun) M1 M2 V (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) cg_insert cg_lookup
[PROOF STEP]
have *:"\<And> V T (G::'d) m t. set T \<subseteq> set (fst ((establish_convergence_static dist_fun) M1 V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V T G m t. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
using establish_convergence_static_subset
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static ?dist_fun ?M ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))

goal (1 subgoal):
 1. \<And>V T G m t. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 ?V ?T ?G cg_insert cg_lookup ?m ?t))

goal (1 subgoal):
 1. verifies_transition (establish_convergence_static dist_fun) M1 M2 V (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) cg_insert cg_lookup
[PROOF STEP]
have ***:"\<And> V T (G::'d) m t. finite_tree T \<longrightarrow> finite_tree (fst ((establish_convergence_static dist_fun) M1 V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V T G m t. finite_tree T \<longrightarrow> finite_tree (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
using establish_convergence_static_finite
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (establish_convergence_static ?dist_fun ?M ?V ?T ?G ?cg_insert ?cg_lookup ?m ?t))

goal (1 subgoal):
 1. \<And>V T G m t. finite_tree T \<longrightarrow> finite_tree (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite_tree ?T \<longrightarrow> finite_tree (fst (establish_convergence_static dist_fun M1 ?V ?T ?G cg_insert cg_lookup ?m ?t))

goal (1 subgoal):
 1. verifies_transition (establish_convergence_static dist_fun) M1 M2 V (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) cg_insert cg_lookup
[PROOF STEP]
let ?distinguish_traces = "(\<lambda> \<alpha> t' q' \<beta> t'' g'' . dist_fun 0 q')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. verifies_transition (establish_convergence_static dist_fun) M1 M2 V (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) cg_insert cg_lookup
[PROOF STEP]
have **:"\<And> T (G::'d) 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)] \<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>
        set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> set T \<Longrightarrow>
        L M1 \<inter> Prefix_Tree.set (fst ((establish_convergence_static dist_fun) M1 V T G cg_insert cg_lookup m t)) =
        L M2 \<inter> Prefix_Tree.set (fst ((establish_convergence_static 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_static dist_fun) M1 V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
fix G :: 'd
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
fix T m t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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_static dist_fun) M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst ((establish_convergence_static 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_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))

goal (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
assume a18: "set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> set T"
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T

goal (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
have "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 *
[PROOF STATE]
proof (prove)
using this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set T
L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static 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 (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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 d2: "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 blast
[PROOF STATE]
proof (state)
this:
V (t_target t) \<in> L M2

goal (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
have d1: "\<And> q . q \<in> reachable_states M1 \<Longrightarrow> set (dist_fun 0 q) \<subseteq> set (after T (V q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. q \<in> reachable_states M1 \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
using handle_state_cover_static_applies_dist_sets[of _ M1 dist_fun V cg_initial cg_insert cg_lookup] a18
[PROOF STATE]
proof (prove)
using this:
?q \<in> reachable_states M1 \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) (V ?q))
Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T

goal (1 subgoal):
 1. \<And>q. q \<in> reachable_states M1 \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
by (meson in_mono subsetI subset_after_subset)
[PROOF STATE]
proof (state)
this:
?q1 \<in> reachable_states M1 \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q1) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V ?q1))

goal (2 subgoals):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static 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))
 2. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[PROOF STEP]
using establish_convergence_static_establishes_convergence[where dist_fun=dist_fun, OF a01 a02 a03 a04 a05 a06 a07 a08 a12 a13 a09 a14 a11 a10 a15 a16 assms(1) d1 assms(2) a17]
[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; \<And>q. q \<in> reachable_states M1 \<Longrightarrow> q \<in> reachable_states M1; \<And>q k. q \<in> FSM.states M1 \<Longrightarrow> q \<in> FSM.states M1\<rbrakk> \<Longrightarrow> converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))

goal (1 subgoal):
 1. converge M2 (V (t_source t) @ [(t_input t, t_output t)]) (V (t_target t))
[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))

goal (1 subgoal):
 1. \<And>T G 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)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set T; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
show "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
using establish_convergence_static_properties(3)[where dist_fun=dist_fun, OF a01 a02 a03 a04 a07 a08 a12 a13 a09 a14 a11 a10 a15 a16 assms(1) d1 assms(2) a17]
[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; \<And>q. q \<in> reachable_states M1 \<Longrightarrow> q \<in> reachable_states M1; \<And>q k. q \<in> FSM.states M1 \<Longrightarrow> q \<in> FSM.states M1\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static 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> ?m1; FSM.size M2 \<le> ?m1; 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 ?T1; ?t1 \<in> FSM.transitions M1; t_source ?t1 \<in> reachable_states M1; V (t_source ?t1) @ [(t_input ?t1, t_output ?t1)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup ?G1; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set ?T1; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V ?T1 ?G1 cg_insert cg_lookup ?m1 ?t1)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V ?T1 ?G1 cg_insert cg_lookup ?m1 ?t1))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source ?t1) @ [(t_input ?t1, t_output ?t1)]) (V (t_target ?t1)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V ?T1 ?G1 cg_insert cg_lookup ?m1 ?t1))

goal (1 subgoal):
 1. verifies_transition (establish_convergence_static dist_fun) M1 M2 V (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) cg_insert cg_lookup
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verifies_transition (establish_convergence_static dist_fun) M1 M2 V (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) 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_static dist_fun M1 V T G cg_insert cg_lookup m t)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (establish_convergence_static 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_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) \<longrightarrow> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<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_static 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_static dist_fun M1 ?V ?T ?G cg_insert cg_lookup ?m ?t))
finite_tree ?T \<longrightarrow> finite_tree (fst (establish_convergence_static dist_fun M1 ?V ?T ?G cg_insert cg_lookup ?m ?t))
\<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> ?m1; FSM.size M2 \<le> ?m1; 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 ?T1; ?t1 \<in> FSM.transitions M1; t_source ?t1 \<in> reachable_states M1; V (t_source ?t1) @ [(t_input ?t1, t_output ?t1)] \<in> L M2; convergence_graph_lookup_invar M1 M2 cg_lookup ?G1; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<subseteq> Prefix_Tree.set ?T1; L M1 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V ?T1 ?G1 cg_insert cg_lookup ?m1 ?t1)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V ?T1 ?G1 cg_insert cg_lookup ?m1 ?t1))\<rbrakk> \<Longrightarrow> converge M2 (V (t_source ?t1) @ [(t_input ?t1, t_output ?t1)]) (V (t_target ?t1)) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (establish_convergence_static dist_fun M1 V ?T1 ?G1 cg_insert cg_lookup ?m1 ?t1))

goal (1 subgoal):
 1. \<forall>T G m t. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (establish_convergence_static 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_static dist_fun M1 V T G cg_insert cg_lookup m t)) = L M2 \<inter> Prefix_Tree.set (fst (establish_convergence_static dist_fun M1 V T G cg_insert cg_lookup m t)) \<longrightarrow> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<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_static 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_static dist_fun) M1 M2 V (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) cg_insert cg_lookup

goal:
No subgoals!
[PROOF STEP]
qed