[STATEMENT]
lemma handle_state_cover_static_applies_dist_sets:
  assumes "q \<in> reachable_states M1"
  shows "set (dist_fun 0 q) \<subseteq> set (after (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) (V q))"
  (is "set (dist_fun 0 q) \<subseteq> set (after ?T (V q))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 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))
[PROOF STEP]
define k where "k = 2 * size M1"
[PROOF STATE]
proof (state)
this:
k = 2 * FSM.size M1

goal (1 subgoal):
 1. 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))
[PROOF STEP]
define separate_state where "separate_state = (\<lambda> T q . combine_after T (V q) (dist_fun 0 q))"
[PROOF STATE]
proof (state)
this:
separate_state = (\<lambda>T q. combine_after T (V q) (dist_fun 0 q))

goal (1 subgoal):
 1. 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))
[PROOF STEP]
define rstates where "rstates = reachable_states_as_list M1"
[PROOF STATE]
proof (state)
this:
rstates = reachable_states_as_list M1

goal (1 subgoal):
 1. 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))
[PROOF STEP]
define T where "T = foldl separate_state empty rstates"
[PROOF STATE]
proof (state)
this:
T = foldl separate_state Prefix_Tree.empty rstates

goal (1 subgoal):
 1. 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))
[PROOF STEP]
define G where "G = cg_initial M1 T"
[PROOF STATE]
proof (state)
this:
G = cg_initial M1 T

goal (1 subgoal):
 1. 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))
[PROOF STEP]
have *:"?T = T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup) = T
[PROOF STEP]
unfolding k_def separate_state_def rstates_def T_def G_def handle_state_cover_static.simps Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (foldl (\<lambda>T q. combine_after T (V q) (dist_fun 0 q)) Prefix_Tree.empty (reachable_states_as_list M1), cg_initial M1 (foldl (\<lambda>T q. combine_after T (V q) (dist_fun 0 q)) Prefix_Tree.empty (reachable_states_as_list M1))) = foldl (\<lambda>T q. combine_after T (V q) (dist_fun 0 q)) Prefix_Tree.empty (reachable_states_as_list M1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup) = T

goal (1 subgoal):
 1. 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))
[PROOF STEP]
have separate_state_subset : "\<And> q T . set T \<subseteq> set (separate_state T q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q T. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (separate_state T q)
[PROOF STEP]
unfolding separate_state_def combine_after_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q T. Prefix_Tree.set T \<subseteq> Prefix_Tree.set T \<union> {xs'. \<exists>xs''. V q = xs' @ xs''} \<union> {V q @ xs' |xs'. xs' \<in> Prefix_Tree.set (dist_fun 0 q)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (separate_state ?T ?q)

goal (1 subgoal):
 1. 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))
[PROOF STEP]
have "\<And> q . q \<in> list.set rstates \<Longrightarrow> set (dist_fun 0 q) \<subseteq> set (after T (V q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. q \<in> list.set rstates \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q. q \<in> list.set rstates \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q. q \<in> list.set rstates \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
assume "q \<in> list.set rstates"
[PROOF STATE]
proof (state)
this:
q \<in> list.set rstates

goal (1 subgoal):
 1. \<And>q. q \<in> list.set rstates \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> list.set rstates
[PROOF STEP]
show "set (dist_fun 0 q) \<subseteq> set (after T (V q))"
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set rstates

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set rstates

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q))
[PROOF STEP]
proof (induction rstates arbitrary: q rule: rev_induct )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q. q \<in> list.set [] \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty []) (V q))
 2. \<And>x xs q. \<lbrakk>\<And>q. q \<in> list.set xs \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty xs) (V q)); q \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (xs @ [x])) (V q))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
q \<in> list.set []

goal (2 subgoals):
 1. \<And>q. q \<in> list.set [] \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty []) (V q))
 2. \<And>x xs q. \<lbrakk>\<And>q. q \<in> list.set xs \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty xs) (V q)); q \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (xs @ [x])) (V q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> list.set []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set []

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty []) (V q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty []) (V q))

goal (1 subgoal):
 1. \<And>x xs q. \<lbrakk>\<And>q. q \<in> list.set xs \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty xs) (V q)); q \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (xs @ [x])) (V q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs q. \<lbrakk>\<And>q. q \<in> list.set xs \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty xs) (V q)); q \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (xs @ [x])) (V q))
[PROOF STEP]
case (snoc a rstates)
[PROOF STATE]
proof (state)
this:
?q \<in> list.set rstates \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V ?q))
q \<in> list.set (rstates @ [a])

goal (1 subgoal):
 1. \<And>x xs q. \<lbrakk>\<And>q. q \<in> list.set xs \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty xs) (V q)); q \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (xs @ [x])) (V q))
[PROOF STEP]
have *: "foldl separate_state empty (rstates@[a]) = separate_state (foldl separate_state empty rstates) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl separate_state Prefix_Tree.empty (rstates @ [a]) = separate_state (foldl separate_state Prefix_Tree.empty rstates) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl separate_state Prefix_Tree.empty (rstates @ [a]) = separate_state (foldl separate_state Prefix_Tree.empty rstates) a

goal (1 subgoal):
 1. \<And>x xs q. \<lbrakk>\<And>q. q \<in> list.set xs \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty xs) (V q)); q \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (xs @ [x])) (V q))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
proof (cases "q = a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q = a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
 2. q \<noteq> a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
q = a

goal (2 subgoals):
 1. q = a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
 2. q \<noteq> a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 a) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V a))
[PROOF STEP]
using separate_state_def combine_after_after_subset
[PROOF STATE]
proof (prove)
using this:
separate_state = (\<lambda>T q. combine_after T (V q) (dist_fun 0 q))
Prefix_Tree.set ?T2.0 \<subseteq> Prefix_Tree.set (Prefix_Tree.after (combine_after ?T1.0 ?xs ?T2.0) ?xs)

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 a) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V a))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))

goal (1 subgoal):
 1. q \<noteq> a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<noteq> a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
q \<noteq> a

goal (1 subgoal):
 1. q \<noteq> a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> a
[PROOF STEP]
have \<open>q \<in> list.set rstates\<close>
[PROOF STATE]
proof (prove)
using this:
q \<noteq> a

goal (1 subgoal):
 1. q \<in> list.set rstates
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
q \<noteq> a
q \<in> list.set (rstates @ [a])

goal (1 subgoal):
 1. q \<in> list.set rstates
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> list.set rstates

goal (1 subgoal):
 1. q \<noteq> a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> list.set rstates
[PROOF STEP]
have "set (dist_fun 0 q) \<subseteq> set (after (foldl separate_state empty rstates) (V q))"
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set rstates

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q))
[PROOF STEP]
using snoc.IH
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set rstates
?q \<in> list.set rstates \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V ?q))

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q))

goal (1 subgoal):
 1. q \<noteq> a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q))

goal (1 subgoal):
 1. q \<noteq> a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
have "set (after (foldl separate_state empty rstates) (V q)) \<subseteq> set (after (foldl separate_state empty (rstates@[a])) (V q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q)) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q)) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (separate_state (foldl separate_state Prefix_Tree.empty rstates) a) (V q))
[PROOF STEP]
using subset_after_subset[OF separate_state_subset]
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (Prefix_Tree.after ?T2.0 ?xs) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (separate_state ?T2.0 ?q1) ?xs)

goal (1 subgoal):
 1. Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q)) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (separate_state (foldl separate_state Prefix_Tree.empty rstates) a) (V q))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q)) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))

goal (1 subgoal):
 1. q \<noteq> a \<Longrightarrow> Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q))
Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q)) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q))
Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty rstates) (V q)) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (foldl separate_state Prefix_Tree.empty (rstates @ [a])) (V q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?q \<in> list.set rstates \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V ?q))

goal (1 subgoal):
 1. 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))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?q \<in> list.set rstates \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V ?q))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?q \<in> list.set rstates \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V ?q))

goal (1 subgoal):
 1. 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))
[PROOF STEP]
unfolding rstates_def \<open>?T = T\<close>
[PROOF STATE]
proof (prove)
using this:
?q \<in> list.set (reachable_states_as_list M1) \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V ?q))

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?q \<in> list.set (reachable_states_as_list M1) \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V ?q))
q \<in> reachable_states M1

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
using reachable_states_as_list_set
[PROOF STATE]
proof (prove)
using this:
?q \<in> list.set (reachable_states_as_list M1) \<Longrightarrow> Prefix_Tree.set (dist_fun 0 ?q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V ?q))
q \<in> reachable_states M1
list.set (reachable_states_as_list ?M) = reachable_states ?M

goal (1 subgoal):
 1. Prefix_Tree.set (dist_fun 0 q) \<subseteq> Prefix_Tree.set (Prefix_Tree.after T (V q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
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))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma handle_state_cover_static_separates_state_cover:
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('e,'b,'c) fsm"
  fixes cg_insert :: "('d \<Rightarrow> ('b\<times>'c) list \<Rightarrow> 'd)"
  assumes "observable M1 \<Longrightarrow> minimal M1 \<Longrightarrow> (\<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> k q . q \<in> states M1 \<Longrightarrow> finite_tree (dist_fun k q)"
shows "separates_state_cover (handle_state_cover_static dist_fun) M1 M2 cg_initial cg_insert cg_lookup"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_static dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_static dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
let ?f = "(handle_state_cover_static dist_fun)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_static dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
have "\<And> (V :: ('a,'b,'c) state_cover_assignment) .
          (V ` reachable_states M1 \<subseteq> set (fst (?f M1 V cg_initial cg_insert cg_lookup)))
            \<and> finite_tree (fst (?f M1 V cg_initial cg_insert cg_lookup))
            \<and> (observable M1 \<longrightarrow>
                observable M2 \<longrightarrow>
                minimal M1 \<longrightarrow>
                minimal M2 \<longrightarrow>
                inputs M2 = inputs M1 \<longrightarrow>
                outputs M2 = outputs M1 \<longrightarrow>
                is_state_cover_assignment M1 V \<longrightarrow>
                convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow>
                convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow>
                L M1 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow>
                (preserves_divergence M1 M2 (V ` reachable_states M1)
                \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (?f M1 V cg_initial cg_insert cg_lookup))))" (is "\<And> V . ?P V")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
fix V :: "('a,'b,'c) state_cover_assignment"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define k where "k = 2 * size M1"
[PROOF STATE]
proof (state)
this:
k = 2 * FSM.size M1

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define separate_state where "separate_state = (\<lambda> T q . combine_after T (V q) (dist_fun 0 q))"
[PROOF STATE]
proof (state)
this:
separate_state = (\<lambda>T q. combine_after T (V q) (dist_fun 0 q))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define rstates where "rstates = reachable_states_as_list M1"
[PROOF STATE]
proof (state)
this:
rstates = reachable_states_as_list M1

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define T where "T = foldl separate_state empty rstates"
[PROOF STATE]
proof (state)
this:
T = foldl separate_state Prefix_Tree.empty rstates

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define G where "G = cg_initial M1 T"
[PROOF STATE]
proof (state)
this:
G = cg_initial M1 T

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have *:"(?f M1 V cg_initial cg_insert cg_lookup) = (T,G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup = (T, G)
[PROOF STEP]
unfolding k_def separate_state_def rstates_def T_def G_def handle_state_cover_static.simps Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (foldl (\<lambda>T q. combine_after T (V q) (dist_fun 0 q)) Prefix_Tree.empty (reachable_states_as_list M1), cg_initial M1 (foldl (\<lambda>T q. combine_after T (V q) (dist_fun 0 q)) Prefix_Tree.empty (reachable_states_as_list M1))) = (foldl (\<lambda>T q. combine_after T (V q) (dist_fun 0 q)) Prefix_Tree.empty (reachable_states_as_list M1), cg_initial M1 (foldl (\<lambda>T q. combine_after T (V q) (dist_fun 0 q)) Prefix_Tree.empty (reachable_states_as_list M1)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup = (T, G)

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have separate_state_subset : "\<And> q T . set T \<subseteq> set (separate_state T q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q T. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (separate_state T q)
[PROOF STEP]
unfolding separate_state_def combine_after_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q T. Prefix_Tree.set T \<subseteq> Prefix_Tree.set T \<union> {xs'. \<exists>xs''. V q = xs' @ xs''} \<union> {V q @ xs' |xs'. xs' \<in> Prefix_Tree.set (dist_fun 0 q)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (separate_state ?T1 ?q1)

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have "V ` (list.set rstates) \<subseteq> set T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ` list.set rstates \<subseteq> Prefix_Tree.set T
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ` list.set rstates \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty rstates)
[PROOF STEP]
proof (induction rstates rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. V ` list.set [] \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty [])
 2. \<And>x xs. V ` list.set xs \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty xs) \<Longrightarrow> V ` list.set (xs @ [x]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. V ` list.set [] \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty [])
 2. \<And>x xs. V ` list.set xs \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty xs) \<Longrightarrow> V ` list.set (xs @ [x]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ` list.set [] \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V ` list.set [] \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty [])

goal (1 subgoal):
 1. \<And>x xs. V ` list.set xs \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty xs) \<Longrightarrow> V ` list.set (xs @ [x]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. V ` list.set xs \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty xs) \<Longrightarrow> V ` list.set (xs @ [x]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
case (snoc a rstates)
[PROOF STATE]
proof (state)
this:
V ` list.set rstates \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty rstates)

goal (1 subgoal):
 1. \<And>x xs. V ` list.set xs \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty xs) \<Longrightarrow> V ` list.set (xs @ [x]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
have *: "foldl separate_state empty (rstates@[a]) = separate_state (foldl separate_state empty rstates) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl separate_state Prefix_Tree.empty (rstates @ [a]) = separate_state (foldl separate_state Prefix_Tree.empty rstates) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl separate_state Prefix_Tree.empty (rstates @ [a]) = separate_state (foldl separate_state Prefix_Tree.empty rstates) a

goal (1 subgoal):
 1. \<And>x xs. V ` list.set xs \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty xs) \<Longrightarrow> V ` list.set (xs @ [x]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
have "V ` (list.set rstates) \<subseteq> set (foldl separate_state empty (rstates@[a]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ` list.set rstates \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (rstates @ [a]))
[PROOF STEP]
using snoc separate_state_subset
[PROOF STATE]
proof (prove)
using this:
V ` list.set rstates \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty rstates)
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (separate_state ?T1 ?q1)

goal (1 subgoal):
 1. V ` list.set rstates \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (rstates @ [a]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V ` list.set rstates \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (rstates @ [a]))

goal (1 subgoal):
 1. \<And>x xs. V ` list.set xs \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty xs) \<Longrightarrow> V ` list.set (xs @ [x]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V ` list.set rstates \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (rstates @ [a]))

goal (1 subgoal):
 1. \<And>x xs. V ` list.set xs \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty xs) \<Longrightarrow> V ` list.set (xs @ [x]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
have "V a \<in> set (separate_state (foldl separate_state empty rstates) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V a \<in> Prefix_Tree.set (separate_state (foldl separate_state Prefix_Tree.empty rstates) a)
[PROOF STEP]
unfolding separate_state_def combine_after_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V a \<in> Prefix_Tree.set (foldl (\<lambda>T q. combine_after T (V q) (dist_fun 0 q)) Prefix_Tree.empty rstates) \<union> {xs'. \<exists>xs''. V a = xs' @ xs''} \<union> {V a @ xs' |xs'. xs' \<in> Prefix_Tree.set (dist_fun 0 a)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V a \<in> Prefix_Tree.set (separate_state (foldl separate_state Prefix_Tree.empty rstates) a)

goal (1 subgoal):
 1. \<And>x xs. V ` list.set xs \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty xs) \<Longrightarrow> V ` list.set (xs @ [x]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V ` list.set rstates \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (rstates @ [a]))
V a \<in> Prefix_Tree.set (separate_state (foldl separate_state Prefix_Tree.empty rstates) a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
V ` list.set rstates \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (rstates @ [a]))
V a \<in> Prefix_Tree.set (separate_state (foldl separate_state Prefix_Tree.empty rstates) a)

goal (1 subgoal):
 1. V ` list.set (rstates @ [a]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (rstates @ [a]))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
V ` list.set rstates \<subseteq> Prefix_Tree.set (separate_state (foldl separate_state Prefix_Tree.empty rstates) a)
V a \<in> Prefix_Tree.set (separate_state (foldl separate_state Prefix_Tree.empty rstates) a)

goal (1 subgoal):
 1. V ` list.set (rstates @ [a]) \<subseteq> Prefix_Tree.set (separate_state (foldl separate_state Prefix_Tree.empty rstates) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V ` list.set (rstates @ [a]) \<subseteq> Prefix_Tree.set (foldl separate_state Prefix_Tree.empty (rstates @ [a]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
V ` list.set rstates \<subseteq> Prefix_Tree.set T

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V ` list.set rstates \<subseteq> Prefix_Tree.set T
[PROOF STEP]
have p1: "(V ` reachable_states M1 \<subseteq> set (fst (?f M1 V cg_initial cg_insert cg_lookup)))"
[PROOF STATE]
proof (prove)
using this:
V ` list.set rstates \<subseteq> Prefix_Tree.set T

goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
unfolding rstates_def *
[PROOF STATE]
proof (prove)
using this:
V ` list.set (reachable_states_as_list M1) \<subseteq> Prefix_Tree.set T

goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (T, G))
[PROOF STEP]
using reachable_states_as_list_set
[PROOF STATE]
proof (prove)
using this:
V ` list.set (reachable_states_as_list M1) \<subseteq> Prefix_Tree.set T
list.set (reachable_states_as_list ?M) = reachable_states ?M

goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (T, G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have separate_state_finite : "\<And> q X T G . q \<in> states M1 \<Longrightarrow> finite_tree T \<Longrightarrow> finite_tree (separate_state T q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q X T G. \<lbrakk>q \<in> FSM.states M1; finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (separate_state T q)
[PROOF STEP]
unfolding separate_state_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q X T G. \<lbrakk>q \<in> FSM.states M1; finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (combine_after T (V q) (dist_fun 0 q))
[PROOF STEP]
using combine_after_finite_tree[OF _ assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite_tree ?t1.0; ?q1 \<in> FSM.states M1\<rbrakk> \<Longrightarrow> finite_tree (combine_after ?t1.0 ?\<alpha> (dist_fun ?k1 ?q1))

goal (1 subgoal):
 1. \<And>q X T G. \<lbrakk>q \<in> FSM.states M1; finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (combine_after T (V q) (dist_fun 0 q))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q1 \<in> FSM.states M1; finite_tree ?T1\<rbrakk> \<Longrightarrow> finite_tree (separate_state ?T1 ?q1)

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q1 \<in> FSM.states M1; finite_tree ?T1\<rbrakk> \<Longrightarrow> finite_tree (separate_state ?T1 ?q1)

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have "\<And> q . q \<in> list.set rstates \<Longrightarrow> q \<in> states M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. q \<in> list.set rstates \<Longrightarrow> q \<in> FSM.states M1
[PROOF STEP]
unfolding rstates_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. q \<in> list.set (reachable_states_as_list M1) \<Longrightarrow> q \<in> FSM.states M1
[PROOF STEP]
by (metis reachable_state_is_state reachable_states_as_list_set)
[PROOF STATE]
proof (state)
this:
?q2 \<in> list.set rstates \<Longrightarrow> ?q2 \<in> FSM.states M1

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?q1 \<in> FSM.states M1; finite_tree ?T1\<rbrakk> \<Longrightarrow> finite_tree (separate_state ?T1 ?q1)
?q2 \<in> list.set rstates \<Longrightarrow> ?q2 \<in> FSM.states M1
[PROOF STEP]
have p2: "finite_tree (fst (?f M1 V cg_initial cg_insert cg_lookup))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q1 \<in> FSM.states M1; finite_tree ?T1\<rbrakk> \<Longrightarrow> finite_tree (separate_state ?T1 ?q1)
?q2 \<in> list.set rstates \<Longrightarrow> ?q2 \<in> FSM.states M1

goal (1 subgoal):
 1. finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
unfolding *  fst_conv T_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q1 \<in> FSM.states M1; finite_tree ?T1\<rbrakk> \<Longrightarrow> finite_tree (separate_state ?T1 ?q1)
?q2 \<in> list.set rstates \<Longrightarrow> ?q2 \<in> FSM.states M1

goal (1 subgoal):
 1. finite_tree (foldl separate_state Prefix_Tree.empty rstates)
[PROOF STEP]
using empty_finite_tree
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q1 \<in> FSM.states M1; finite_tree ?T1\<rbrakk> \<Longrightarrow> finite_tree (separate_state ?T1 ?q1)
?q2 \<in> list.set rstates \<Longrightarrow> ?q2 \<in> FSM.states M1
finite_tree Prefix_Tree.empty

goal (1 subgoal):
 1. finite_tree (foldl separate_state Prefix_Tree.empty rstates)
[PROOF STEP]
by (induction rstates rule: rev_induct; auto)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have p3: "observable M1 \<Longrightarrow>
                observable M2 \<Longrightarrow>
                minimal M1 \<Longrightarrow>
                minimal M2 \<Longrightarrow>
                inputs M2 = inputs M1 \<Longrightarrow>
                outputs M2 = outputs M1 \<Longrightarrow>
                is_state_cover_assignment M1 V \<Longrightarrow>
                convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<Longrightarrow>
                convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<Longrightarrow>
                L M1 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) \<Longrightarrow>
                (preserves_divergence M1 M2 (V ` reachable_states M1)
                \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (?f M1 V cg_initial cg_insert cg_lookup)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; convergence_graph_initial_invar M1 M2 cg_lookup cg_initial; L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; convergence_graph_initial_invar M1 M2 cg_lookup cg_initial; L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
assume a0: "observable M1"
         and a1: "observable M2"
         and a2: "minimal M1"
         and a3: "minimal M2"
         and a4: "inputs M2 = inputs M1"
         and a5: "outputs M2 = outputs M1"
         and a6: "is_state_cover_assignment M1 V"
         and a7: "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
         and a8: "convergence_graph_initial_invar M1 M2 cg_lookup cg_initial"
         and a9: "L M1 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup))"
[PROOF STATE]
proof (state)
this:
observable M1
observable M2
minimal M1
minimal M2
FSM.inputs M2 = FSM.inputs M1
FSM.outputs M2 = FSM.outputs M1
is_state_cover_assignment M1 V
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert
convergence_graph_initial_invar M1 M2 cg_lookup cg_initial
L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; convergence_graph_initial_invar M1 M2 cg_lookup cg_initial; L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
have "L M1 \<inter> set T = L M2 \<inter> set T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T
[PROOF STEP]
using a9
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set (fst (T, G)) = L M2 \<inter> Prefix_Tree.set (fst (T, G))

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; convergence_graph_initial_invar M1 M2 cg_lookup cg_initial; L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T
[PROOF STEP]
have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (?f M1 V cg_initial cg_insert cg_lookup))"
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
using a8 p2
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T
convergence_graph_initial_invar M1 M2 cg_lookup cg_initial
finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
unfolding * fst_conv snd_conv G_def convergence_graph_initial_invar_def
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T
\<forall>T. L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T \<longrightarrow> finite_tree T \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (cg_initial M1 T)
finite_tree T

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (cg_initial M1 T)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; convergence_graph_initial_invar M1 M2 cg_lookup cg_initial; L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; convergence_graph_initial_invar M1 M2 cg_lookup cg_initial; L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
have "preserves_divergence M1 M2 (V ` reachable_states M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preserves_divergence M1 M2 (V ` reachable_states M1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. preserves_divergence M1 M2 (V ` reachable_states M1)
[PROOF STEP]
have "\<And> u v . u\<in>L M1 \<inter> V ` reachable_states M1 \<Longrightarrow> v\<in>L M1 \<inter> V ` reachable_states M1 \<Longrightarrow> \<not> converge M1 u v \<Longrightarrow> \<not> converge M2 u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
fix u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
assume "u\<in>L M1 \<inter> V ` reachable_states M1" and "v\<in>L M1 \<inter> V ` reachable_states M1" and "\<not> converge M1 u v"
[PROOF STATE]
proof (state)
this:
u \<in> L M1 \<inter> V ` reachable_states M1
v \<in> L M1 \<inter> V ` reachable_states M1
\<not> converge M1 u v

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> L M1 \<inter> V ` reachable_states M1
v \<in> L M1 \<inter> V ` reachable_states M1
\<not> converge M1 u v
[PROOF STEP]
obtain qv qu where "qu \<in> reachable_states M1" and "u = V qu"
                                  "qv \<in> reachable_states M1" and "v = V qv"
[PROOF STATE]
proof (prove)
using this:
u \<in> L M1 \<inter> V ` reachable_states M1
v \<in> L M1 \<inter> V ` reachable_states M1
\<not> converge M1 u v

goal (1 subgoal):
 1. (\<And>qu qv. \<lbrakk>qu \<in> reachable_states M1; u = V qu; qv \<in> reachable_states M1; v = V qv\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qu \<in> reachable_states M1
u = V qu
qv \<in> reachable_states M1
v = V qv

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qu \<in> reachable_states M1
u = V qu
qv \<in> reachable_states M1
v = V qv
[PROOF STEP]
have "u \<in> L M1" and "v \<in> L M1"
[PROOF STATE]
proof (prove)
using this:
qu \<in> reachable_states M1
u = V qu
qv \<in> reachable_states M1
v = V qv

goal (1 subgoal):
 1. u \<in> L M1 &&& v \<in> L M1
[PROOF STEP]
using a6
[PROOF STATE]
proof (prove)
using this:
qu \<in> reachable_states M1
u = V qu
qv \<in> reachable_states M1
v = V qv
is_state_cover_assignment M1 V

goal (1 subgoal):
 1. u \<in> L M1 &&& v \<in> L M1
[PROOF STEP]
by (meson is_state_cover_assignment_language)+
[PROOF STATE]
proof (state)
this:
u \<in> L M1
v \<in> L M1

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> L M1
v \<in> L M1
[PROOF STEP]
have "qu \<noteq> qv"
[PROOF STATE]
proof (prove)
using this:
u \<in> L M1
v \<in> L M1

goal (1 subgoal):
 1. qu \<noteq> qv
[PROOF STEP]
using a6 \<open>\<not> converge M1 u v\<close>
[PROOF STATE]
proof (prove)
using this:
u \<in> L M1
v \<in> L M1
is_state_cover_assignment M1 V
\<not> converge M1 u v

goal (1 subgoal):
 1. qu \<noteq> qv
[PROOF STEP]
using \<open>u = V qu\<close> \<open>v = V qv\<close> a0 a2 convergence_minimal
[PROOF STATE]
proof (prove)
using this:
u \<in> L M1
v \<in> L M1
is_state_cover_assignment M1 V
\<not> converge M1 u v
u = V qu
v = V qv
observable M1
minimal M1
\<lbrakk>minimal ?M; observable ?M; ?\<alpha> \<in> L ?M; ?\<beta> \<in> L ?M\<rbrakk> \<Longrightarrow> converge ?M ?\<alpha> ?\<beta> = (after_initial ?M ?\<alpha> = after_initial ?M ?\<beta>)

goal (1 subgoal):
 1. qu \<noteq> qv
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qu \<noteq> qv

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qu \<noteq> qv

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
have "qu \<in> states M1" and "qv \<in> states M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qu \<in> FSM.states M1 &&& qv \<in> FSM.states M1
[PROOF STEP]
using \<open>qu \<in> reachable_states M1\<close> \<open>qv \<in> reachable_states M1\<close>
[PROOF STATE]
proof (prove)
using this:
qu \<in> reachable_states M1
qv \<in> reachable_states M1

goal (1 subgoal):
 1. qu \<in> FSM.states M1 &&& qv \<in> FSM.states M1
[PROOF STEP]
by (simp add: reachable_state_is_state)+
[PROOF STATE]
proof (state)
this:
qu \<in> FSM.states M1
qv \<in> FSM.states M1

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qu \<noteq> qv
qu \<in> FSM.states M1
qv \<in> FSM.states M1
[PROOF STEP]
obtain w where "distinguishes M1 qu qv w" and "w \<in> set (dist_fun 0 qu)" and "w \<in> set (dist_fun 0 qv)"
[PROOF STATE]
proof (prove)
using this:
qu \<noteq> qv
qu \<in> FSM.states M1
qv \<in> FSM.states M1

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>distinguishes M1 qu qv w; w \<in> Prefix_Tree.set (dist_fun 0 qu); w \<in> Prefix_Tree.set (dist_fun 0 qv)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)[OF a0 a2]
[PROOF STATE]
proof (prove)
using this:
qu \<noteq> qv
qu \<in> FSM.states M1
qv \<in> FSM.states M1
\<lbrakk>?q1.0 \<in> FSM.states M1; ?q2.0 \<in> FSM.states M1; ?q1.0 \<noteq> ?q2.0\<rbrakk> \<Longrightarrow> \<exists>io. \<forall>k1 k2. io \<in> Prefix_Tree.set (dist_fun k1 ?q1.0) \<inter> Prefix_Tree.set (dist_fun k2 ?q2.0) \<and> distinguishes M1 ?q1.0 ?q2.0 io

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>distinguishes M1 qu qv w; w \<in> Prefix_Tree.set (dist_fun 0 qu); w \<in> Prefix_Tree.set (dist_fun 0 qv)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Int_iff)
[PROOF STATE]
proof (state)
this:
distinguishes M1 qu qv w
w \<in> Prefix_Tree.set (dist_fun 0 qu)
w \<in> Prefix_Tree.set (dist_fun 0 qv)

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinguishes M1 qu qv w
w \<in> Prefix_Tree.set (dist_fun 0 qu)
w \<in> Prefix_Tree.set (dist_fun 0 qv)
[PROOF STEP]
have "w \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
distinguishes M1 qu qv w
w \<in> Prefix_Tree.set (dist_fun 0 qu)
w \<in> Prefix_Tree.set (dist_fun 0 qv)

goal (1 subgoal):
 1. w \<noteq> []
[PROOF STEP]
by (meson \<open>qu \<in> FSM.states M1\<close> \<open>qv \<in> FSM.states M1\<close> distinguishes_not_Nil)
[PROOF STATE]
proof (state)
this:
w \<noteq> []

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
have "(u@w \<in> L M1) \<noteq> (v@w \<in> L M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u @ w \<in> L M1) \<noteq> (v @ w \<in> L M1)
[PROOF STEP]
unfolding \<open>u = V qu\<close> \<open>v = V qv\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V qu @ w \<in> L M1) \<noteq> (V qv @ w \<in> L M1)
[PROOF STEP]
using state_cover_assignment_after[OF a0 a6 \<open>qu \<in> reachable_states M1\<close>]
[PROOF STATE]
proof (prove)
using this:
V qu \<in> L M1
after_initial M1 (V qu) = qu

goal (1 subgoal):
 1. (V qu @ w \<in> L M1) \<noteq> (V qv @ w \<in> L M1)
[PROOF STEP]
using state_cover_assignment_after[OF a0 a6 \<open>qv \<in> reachable_states M1\<close>]
[PROOF STATE]
proof (prove)
using this:
V qu \<in> L M1
after_initial M1 (V qu) = qu
V qv \<in> L M1
after_initial M1 (V qv) = qv

goal (1 subgoal):
 1. (V qu @ w \<in> L M1) \<noteq> (V qv @ w \<in> L M1)
[PROOF STEP]
by (metis \<open>distinguishes M1 qu qv w\<close> a0 after_distinguishes_language)
[PROOF STATE]
proof (state)
this:
(u @ w \<in> L M1) \<noteq> (v @ w \<in> L M1)

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(u @ w \<in> L M1) \<noteq> (v @ w \<in> L M1)

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
have "u@w \<in> set T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u @ w \<in> Prefix_Tree.set T
[PROOF STEP]
using handle_state_cover_static_applies_dist_sets[OF \<open>qu \<in> reachable_states M1\<close>, of dist_fun V cg_initial cg_insert cg_lookup] \<open>w \<in> set (dist_fun 0 qu)\<close> \<open>w \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (dist_fun 0 qu) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) (V qu))
w \<in> Prefix_Tree.set (dist_fun 0 qu)
w \<noteq> []

goal (1 subgoal):
 1. u @ w \<in> Prefix_Tree.set T
[PROOF STEP]
unfolding * fst_conv after_set \<open>u = V qu\<close>
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (dist_fun 0 qu) \<subseteq> Set.insert [] {xs'. V qu @ xs' \<in> Prefix_Tree.set T}
w \<in> Prefix_Tree.set (dist_fun 0 qu)
w \<noteq> []

goal (1 subgoal):
 1. V qu @ w \<in> Prefix_Tree.set T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u @ w \<in> Prefix_Tree.set T

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u @ w \<in> Prefix_Tree.set T

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
have "v@w \<in> set T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v @ w \<in> Prefix_Tree.set T
[PROOF STEP]
using handle_state_cover_static_applies_dist_sets[OF \<open>qv \<in> reachable_states M1\<close>, of dist_fun V cg_initial cg_insert cg_lookup] \<open>w \<in> set (dist_fun 0 qv)\<close> \<open>w \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (dist_fun 0 qv) \<subseteq> Prefix_Tree.set (Prefix_Tree.after (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) (V qv))
w \<in> Prefix_Tree.set (dist_fun 0 qv)
w \<noteq> []

goal (1 subgoal):
 1. v @ w \<in> Prefix_Tree.set T
[PROOF STEP]
unfolding * fst_conv after_set \<open>v = V qv\<close>
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (dist_fun 0 qv) \<subseteq> Set.insert [] {xs'. V qv @ xs' \<in> Prefix_Tree.set T}
w \<in> Prefix_Tree.set (dist_fun 0 qv)
w \<noteq> []

goal (1 subgoal):
 1. V qv @ w \<in> Prefix_Tree.set T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v @ w \<in> Prefix_Tree.set T

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(u @ w \<in> L M1) \<noteq> (v @ w \<in> L M1)
u @ w \<in> Prefix_Tree.set T
v @ w \<in> Prefix_Tree.set T
[PROOF STEP]
have "(u@w \<in> L M2) \<noteq> (v@w \<in> L M2)"
[PROOF STATE]
proof (prove)
using this:
(u @ w \<in> L M1) \<noteq> (v @ w \<in> L M1)
u @ w \<in> Prefix_Tree.set T
v @ w \<in> Prefix_Tree.set T

goal (1 subgoal):
 1. (u @ w \<in> L M2) \<noteq> (v @ w \<in> L M2)
[PROOF STEP]
using \<open>L M1 \<inter> set T = L M2 \<inter> set T\<close>
[PROOF STATE]
proof (prove)
using this:
(u @ w \<in> L M1) \<noteq> (v @ w \<in> L M1)
u @ w \<in> Prefix_Tree.set T
v @ w \<in> Prefix_Tree.set T
L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T

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

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> L M1 \<inter> V ` reachable_states M1; v \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 u v\<rbrakk> \<Longrightarrow> \<not> converge M2 u v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(u @ w \<in> L M2) \<noteq> (v @ w \<in> L M2)
[PROOF STEP]
show "\<not> converge M2 u v"
[PROOF STATE]
proof (prove)
using this:
(u @ w \<in> L M2) \<noteq> (v @ w \<in> L M2)

goal (1 subgoal):
 1. \<not> converge M2 u v
[PROOF STEP]
using a1 converge_append_language_iff
[PROOF STATE]
proof (prove)
using this:
(u @ w \<in> L M2) \<noteq> (v @ w \<in> L M2)
observable M2
\<lbrakk>observable ?M; converge ?M ?\<alpha> ?\<beta>\<rbrakk> \<Longrightarrow> (?\<alpha> @ ?\<gamma> \<in> L ?M) = (?\<beta> @ ?\<gamma> \<in> L ?M)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?u2 \<in> L M1 \<inter> V ` reachable_states M1; ?v2 \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 ?u2 ?v2\<rbrakk> \<Longrightarrow> \<not> converge M2 ?u2 ?v2

goal (1 subgoal):
 1. preserves_divergence M1 M2 (V ` reachable_states M1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?u2 \<in> L M1 \<inter> V ` reachable_states M1; ?v2 \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 ?u2 ?v2\<rbrakk> \<Longrightarrow> \<not> converge M2 ?u2 ?v2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u2 \<in> L M1 \<inter> V ` reachable_states M1; ?v2 \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 ?u2 ?v2\<rbrakk> \<Longrightarrow> \<not> converge M2 ?u2 ?v2

goal (1 subgoal):
 1. preserves_divergence M1 M2 (V ` reachable_states M1)
[PROOF STEP]
unfolding preserves_divergence.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u2 \<in> L M1 \<inter> V ` reachable_states M1; ?v2 \<in> L M1 \<inter> V ` reachable_states M1; \<not> converge M1 ?u2 ?v2\<rbrakk> \<Longrightarrow> \<not> converge M2 ?u2 ?v2

goal (1 subgoal):
 1. \<forall>\<alpha>\<in>L M1 \<inter> V ` reachable_states M1. \<forall>\<beta>\<in>L M1 \<inter> V ` reachable_states M1. \<not> converge M1 \<alpha> \<beta> \<longrightarrow> \<not> converge M2 \<alpha> \<beta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (V ` reachable_states M1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (V ` reachable_states M1)

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; convergence_graph_initial_invar M1 M2 cg_lookup cg_initial; L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
preserves_divergence M1 M2 (V ` reachable_states M1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
preserves_divergence M1 M2 (V ` reachable_states M1)

goal (1 subgoal):
 1. preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; convergence_graph_initial_invar M1 M2 cg_lookup cg_initial; L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
show "?P V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
using p1 p2 p3
[PROOF STATE]
proof (prove)
using this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))
\<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; convergence_graph_initial_invar M1 M2 cg_lookup cg_initial; L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?V1 ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 ?V1 \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (?V1 ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)))

goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_static dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?V1 ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 ?V1 \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (?V1 ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?V1 ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 ?V1 \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (?V1 ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)))

goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_static dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
unfolding separates_state_cover_def
[PROOF STATE]
proof (prove)
using this:
?V1 ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 ?V1 \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (?V1 ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)))

goal (1 subgoal):
 1. \<forall>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_static dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
separates_state_cover (handle_state_cover_static dist_fun) M1 M2 cg_initial cg_insert cg_lookup

goal:
No subgoals!
[PROOF STEP]
qed