[STATEMENT]
lemma append_heuristic_io_in :
  "fst (append_heuristic_io T w (uBest,lBest) u') \<in> {u',uBest}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (append_heuristic_io T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
unfolding append_heuristic_io.simps Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (if maximum_prefix (Prefix_Tree.after T u') w = w then (u', 0) else if is_maximal_in (Prefix_Tree.after T u') (maximum_prefix (Prefix_Tree.after T u') w) \<and> (lBest < int (length (maximum_prefix (Prefix_Tree.after T u') w)) \<or> int (length (maximum_prefix (Prefix_Tree.after T u') w)) = lBest \<and> length u' < length uBest) then (u', int (length (maximum_prefix (Prefix_Tree.after T u') w))) else (uBest, lBest)) \<in> {u', uBest}
[PROOF STEP]
by auto


[STATEMENT]
lemma append_heuristic_input_in :
  "fst (append_heuristic_input M T w (uBest,lBest) u') \<in> {u',uBest}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
define ws where ws: "ws = maximum_fst_prefixes (after T u') (map fst w) (outputs_as_list M)"
[PROOF STATE]
proof (state)
this:
ws = maximum_fst_prefixes (Prefix_Tree.after T u') (map fst w) (outputs_as_list M)

goal (1 subgoal):
 1. fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
define f where f: "f = (\<lambda> w' (uBest',lBest'::int) .
                                                if w' = w
                                                  then (u',0::int)
                                                  else if (int (length w') > lBest' \<or> (int (length w') = lBest' \<and> length u' < length uBest'))
                                                    then (u',int (length w'))
                                                    else (uBest',lBest'))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>w' (uBest', lBest'). if w' = w then (u', 0) else if lBest' < int (length w') \<or> int (length w') = lBest' \<and> length u' < length uBest' then (u', int (length w')) else (uBest', lBest'))

goal (1 subgoal):
 1. fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
have "\<And> w' b' . fst b' \<in> {u',uBest} \<Longrightarrow> fst (f w' b') \<in> {u',uBest}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w' b'. fst b' \<in> {u', uBest} \<Longrightarrow> fst (f w' b') \<in> {u', uBest}
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w' b'. fst b' \<in> {u', uBest} \<Longrightarrow> fst (case b' of (uBest', lBest') \<Rightarrow> if w' = w then (u', 0) else if lBest' < int (length w') \<or> int (length w') = lBest' \<and> length u' < length uBest' then (u', int (length w')) else (uBest', lBest')) \<in> {u', uBest}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst ?b' \<in> {u', uBest} \<Longrightarrow> fst (f ?w' ?b') \<in> {u', uBest}

goal (1 subgoal):
 1. fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst ?b' \<in> {u', uBest} \<Longrightarrow> fst (f ?w' ?b') \<in> {u', uBest}
[PROOF STEP]
have "fst (foldr f ws (uBest,lBest)) \<in> {u',uBest}"
[PROOF STATE]
proof (prove)
using this:
fst ?b' \<in> {u', uBest} \<Longrightarrow> fst (f ?w' ?b') \<in> {u', uBest}

goal (1 subgoal):
 1. fst (foldr f ws (uBest, lBest)) \<in> {u', uBest}
[PROOF STEP]
by (induction ws; auto)
[PROOF STATE]
proof (state)
this:
fst (foldr f ws (uBest, lBest)) \<in> {u', uBest}

goal (1 subgoal):
 1. fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst (foldr f ws (uBest, lBest)) \<in> {u', uBest}

goal (1 subgoal):
 1. fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
have "append_heuristic_input M T w (uBest,lBest) u' = foldr f ws (uBest,lBest)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. append_heuristic_input M T w (uBest, lBest) u' = foldr f ws (uBest, lBest)
[PROOF STEP]
unfolding append_heuristic_input.simps Let_def ws f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>w' (uBest', lBest'). if w' = w then (u', 0) else if lBest' < int (length w') \<or> int (length w') = lBest' \<and> length u' < length uBest' then (u', int (length w')) else (uBest', lBest')) (maximum_fst_prefixes (Prefix_Tree.after T u') (map fst w) (outputs_as_list M)) (uBest, lBest) = foldr (\<lambda>w' (uBest', lBest'). if w' = w then (u', 0) else if lBest' < int (length w') \<or> int (length w') = lBest' \<and> length u' < length uBest' then (u', int (length w')) else (uBest', lBest')) (maximum_fst_prefixes (Prefix_Tree.after T u') (map fst w) (outputs_as_list M)) (uBest, lBest)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
append_heuristic_input M T w (uBest, lBest) u' = foldr f ws (uBest, lBest)

goal (1 subgoal):
 1. fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst (foldr f ws (uBest, lBest)) \<in> {u', uBest}
append_heuristic_input M T w (uBest, lBest) u' = foldr f ws (uBest, lBest)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst (foldr f ws (uBest, lBest)) \<in> {u', uBest}
append_heuristic_input M T w (uBest, lBest) u' = foldr f ws (uBest, lBest)

goal (1 subgoal):
 1. fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (append_heuristic_input M T w (uBest, lBest) u') \<in> {u', uBest}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distribute_extension_subset :
  "set T \<subseteq> set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define u0 where u0: "u0 = shortest_list_in_tree_or_default (cg_lookup G u) T u"
[PROOF STATE]
proof (state)
this:
u0 = shortest_list_in_tree_or_default (cg_lookup G u) T u

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define l0 where l0: "l0 = (-1::int)"
[PROOF STATE]
proof (state)
this:
l0 = - 1

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define u' where u': "u' = fst (foldl (heuristic T w) (u0,l0) (filter (isin T) (cg_lookup G u)))"
[PROOF STATE]
proof (state)
this:
u' = fst (foldl (heuristic T w) (u0, l0) (filter (isin T) (cg_lookup G u)))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define T' where T': "T' = insert T (u'@w)"
[PROOF STATE]
proof (state)
this:
T' = Prefix_Tree.insert T (u' @ w)

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define G' where G': "G' = cg_insert G (maximal_prefix_in_language M (initial M) (u'@w))"
[PROOF STATE]
proof (state)
this:
G' = cg_insert G (maximal_prefix_in_language M (FSM.initial M) (u' @ w))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "set T \<subseteq> set T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set T'
[PROOF STEP]
unfolding T' insert_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set T \<union> {xs'. \<exists>xs''. u' @ w = xs' @ xs''}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set T'

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
proof (cases b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
 2. \<not> b \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b

goal (2 subgoals):
 1. b \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
 2. \<not> b \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
using \<open>set T \<subseteq> set T'\<close>
[PROOF STATE]
proof (prove)
using this:
b
Prefix_Tree.set T \<subseteq> Prefix_Tree.set T'

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
unfolding distribute_extension.simps u0 l0 u' T' G' Let_def
[PROOF STATE]
proof (prove)
using this:
b
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (if b then (combine (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)) (complete_inputs_to_tree M (FSM.initial M) (outputs_as_list M) (map fst (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))) else (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))))
[PROOF STEP]
using combine_set
[PROOF STATE]
proof (prove)
using this:
b
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))
Prefix_Tree.set (combine ?t1.0 ?t2.0) = Prefix_Tree.set ?t1.0 \<union> Prefix_Tree.set ?t2.0

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (if b then (combine (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)) (complete_inputs_to_tree M (FSM.initial M) (outputs_as_list M) (map fst (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))) else (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> b \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> b
[PROOF STEP]
have "fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'"
[PROOF STATE]
proof (prove)
using this:
\<not> b

goal (1 subgoal):
 1. fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'
[PROOF STEP]
unfolding distribute_extension.simps u0 l0 u' T' G' Let_def
[PROOF STATE]
proof (prove)
using this:
\<not> b

goal (1 subgoal):
 1. fst (if b then (combine (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)) (complete_inputs_to_tree M (FSM.initial M) (outputs_as_list M) (map fst (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))) else (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))) = Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
using \<open>set T \<subseteq> set T'\<close>
[PROOF STATE]
proof (prove)
using this:
fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'
Prefix_Tree.set T \<subseteq> Prefix_Tree.set T'

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distribute_extension_finite :
  assumes "finite_tree T"
  shows "finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define u0 where u0: "u0 = shortest_list_in_tree_or_default (cg_lookup G u) T u"
[PROOF STATE]
proof (state)
this:
u0 = shortest_list_in_tree_or_default (cg_lookup G u) T u

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define l0 where l0: "l0 = (-1::int)"
[PROOF STATE]
proof (state)
this:
l0 = - 1

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define u' where u': "u' = fst (foldl (heuristic T w) (u0,l0) (filter (isin T) (cg_lookup G u)))"
[PROOF STATE]
proof (state)
this:
u' = fst (foldl (heuristic T w) (u0, l0) (filter (isin T) (cg_lookup G u)))

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define T' where T': "T' = insert T (u'@w)"
[PROOF STATE]
proof (state)
this:
T' = Prefix_Tree.insert T (u' @ w)

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define G' where G': "G' = cg_insert G (maximal_prefix_in_language M (initial M) (u'@w))"
[PROOF STATE]
proof (state)
this:
G' = cg_insert G (maximal_prefix_in_language M (FSM.initial M) (u' @ w))

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "finite_tree T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree T'
[PROOF STEP]
unfolding T'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (Prefix_Tree.insert T (u' @ w))
[PROOF STEP]
using insert_finite_tree[OF assms]
[PROOF STATE]
proof (prove)
using this:
finite_tree (Prefix_Tree.insert T ?xs)

goal (1 subgoal):
 1. finite_tree (Prefix_Tree.insert T (u' @ w))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite_tree T'

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
proof (cases b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b \<Longrightarrow> finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
 2. \<not> b \<Longrightarrow> finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b

goal (2 subgoals):
 1. b \<Longrightarrow> finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
 2. \<not> b \<Longrightarrow> finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
using \<open>finite_tree T'\<close>
[PROOF STATE]
proof (prove)
using this:
b
finite_tree T'

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
unfolding distribute_extension.simps u0 l0 u' T' G' Let_def
[PROOF STATE]
proof (prove)
using this:
b
finite_tree (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))

goal (1 subgoal):
 1. finite_tree (fst (if b then (combine (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)) (complete_inputs_to_tree M (FSM.initial M) (outputs_as_list M) (map fst (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))) else (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))))
[PROOF STEP]
by (simp add: combine_finite_tree complete_inputs_to_tree_finite_tree)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> b \<Longrightarrow> finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> b
[PROOF STEP]
have "fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'"
[PROOF STATE]
proof (prove)
using this:
\<not> b

goal (1 subgoal):
 1. fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'
[PROOF STEP]
unfolding distribute_extension.simps u0 l0 u' T' G' Let_def
[PROOF STATE]
proof (prove)
using this:
\<not> b

goal (1 subgoal):
 1. fst (if b then (combine (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)) (complete_inputs_to_tree M (FSM.initial M) (outputs_as_list M) (map fst (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))) else (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w), cg_insert G (maximal_prefix_in_language M (FSM.initial M) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))) = Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
using \<open>finite_tree T'\<close>
[PROOF STATE]
proof (prove)
using this:
fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic) = T'
finite_tree T'

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u w b heuristic))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distribute_extension_adds_sequence :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  assumes "observable M1"
  and     "minimal M1"
  and     "u \<in> L M1" and "u \<in> L M2"
  and     "convergence_graph_lookup_invar M1 M2 cg_lookup G"
  and     "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
  and     "(L M1 \<inter> set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) = L M2 \<inter> set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)))"
  and     "\<And> u' uBest lBest . fst (heuristic T w (uBest,lBest) u') \<in> {u',uBest}"
shows "\<exists> u' . converge M1 u u' \<and> u'@w \<in> set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'"
and   "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u' &&& convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define u0 where u0: "u0 = shortest_list_in_tree_or_default (cg_lookup G u) T u"
[PROOF STATE]
proof (state)
this:
u0 = shortest_list_in_tree_or_default (cg_lookup G u) T u

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define l0 where l0: "l0 = (-1::int)"
[PROOF STATE]
proof (state)
this:
l0 = - 1

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define u' where u': "u' = fst (foldl (heuristic T w) (u0,l0) (filter (isin T) (cg_lookup G u)))"
[PROOF STATE]
proof (state)
this:
u' = fst (foldl (heuristic T w) (u0, l0) (filter (isin T) (cg_lookup G u)))

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define T' where T': "T' = insert T (u'@w)"
[PROOF STATE]
proof (state)
this:
T' = Prefix_Tree.insert T (u' @ w)

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define G' where G': "G' = cg_insert G (maximal_prefix_in_language M1 (initial M1) (u'@w))"
[PROOF STATE]
proof (state)
this:
G' = cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w))

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define TC where TC: "TC = complete_inputs_to_tree M1 (initial M1) (outputs_as_list M1) (map fst (u'@w))"
[PROOF STATE]
proof (state)
this:
TC = complete_inputs_to_tree M1 (FSM.initial M1) (outputs_as_list M1) (map fst (u' @ w))

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
define T'' where T'': "T'' = Prefix_Tree.combine T' TC"
[PROOF STATE]
proof (state)
this:
T'' = combine T' TC

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T',G') \<or>
        distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T'',G')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T', G') \<or> distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T'', G')
[PROOF STEP]
unfolding distribute_extension.simps u0 l0 u' T' G' TC T'' Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if b then (combine (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)) (complete_inputs_to_tree M1 (FSM.initial M1) (outputs_as_list M1) (map fst (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))), cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))) else (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w), cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))) = (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w), cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))) \<or> (if b then (combine (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)) (complete_inputs_to_tree M1 (FSM.initial M1) (outputs_as_list M1) (map fst (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))), cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))) else (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w), cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))) = (combine (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)) (complete_inputs_to_tree M1 (FSM.initial M1) (outputs_as_list M1) (map fst (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))), cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T', G') \<or> distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T'', G')

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T', G') \<or> distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T'', G')

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "set T' \<subseteq> set T''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T' \<subseteq> Prefix_Tree.set T''
[PROOF STEP]
unfolding T'' combine_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T' \<subseteq> Prefix_Tree.set T' \<union> Prefix_Tree.set TC
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set T''

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T', G') \<or> distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T'', G')
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set T''
[PROOF STEP]
have "set T' \<subseteq> set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))"
[PROOF STATE]
proof (prove)
using this:
distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T', G') \<or> distribute_extension M1 T G cg_lookup cg_insert u w b heuristic = (T'', G')
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set T''

goal (1 subgoal):
 1. Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "\<And> xs . fst (foldl (heuristic T w) (u0,l0) xs) \<in> Set.insert u0 (list.set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs)
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs)
[PROOF STEP]
show "fst (foldl (heuristic T w) (u0,l0) xs) \<in> Set.insert u0 (list.set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs)
[PROOF STEP]
proof (induction xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst (foldl (heuristic T w) (u0, l0) []) \<in> Set.insert u0 (list.set [])
 2. \<And>x xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs) \<Longrightarrow> fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. fst (foldl (heuristic T w) (u0, l0) []) \<in> Set.insert u0 (list.set [])
 2. \<And>x xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs) \<Longrightarrow> fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (foldl (heuristic T w) (u0, l0) []) \<in> Set.insert u0 (list.set [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (foldl (heuristic T w) (u0, l0) []) \<in> Set.insert u0 (list.set [])

goal (1 subgoal):
 1. \<And>x xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs) \<Longrightarrow> fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs) \<Longrightarrow> fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs)

goal (1 subgoal):
 1. \<And>x xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs) \<Longrightarrow> fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))
[PROOF STEP]
have "\<And> u' uBest lBest . (fst ((heuristic T w) (uBest,lBest) u')) = u' \<or> (fst ((heuristic T w) (uBest,lBest) u')) = uBest"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u' uBest lBest. fst (heuristic T w (uBest, lBest) u') = u' \<or> fst (heuristic T w (uBest, lBest) u') = uBest
[PROOF STEP]
using assms(8)
[PROOF STATE]
proof (prove)
using this:
fst (heuristic T w (?uBest, ?lBest) ?u') \<in> {?u', ?uBest}

goal (1 subgoal):
 1. \<And>u' uBest lBest. fst (heuristic T w (uBest, lBest) u') = u' \<or> fst (heuristic T w (uBest, lBest) u') = uBest
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst (heuristic T w (?uBest, ?lBest) ?u') = ?u' \<or> fst (heuristic T w (?uBest, ?lBest) ?u') = ?uBest

goal (1 subgoal):
 1. \<And>x xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs) \<Longrightarrow> fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (heuristic T w (?uBest, ?lBest) ?u') = ?u' \<or> fst (heuristic T w (?uBest, ?lBest) ?u') = ?uBest
[PROOF STEP]
have "(fst ((heuristic T w) (foldl (heuristic T w) (u0, l0) xs) x)) = x \<or> (fst ((heuristic T w) (foldl (heuristic T w) (u0, l0) xs) x)) = fst (foldl (heuristic T w) (u0, l0) xs)"
[PROOF STATE]
proof (prove)
using this:
fst (heuristic T w (?uBest, ?lBest) ?u') = ?u' \<or> fst (heuristic T w (?uBest, ?lBest) ?u') = ?uBest

goal (1 subgoal):
 1. fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = x \<or> fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = fst (foldl (heuristic T w) (u0, l0) xs)
[PROOF STEP]
by (metis prod.exhaust_sel)
[PROOF STATE]
proof (state)
this:
fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = x \<or> fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = fst (foldl (heuristic T w) (u0, l0) xs)

goal (1 subgoal):
 1. \<And>x xs. fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs) \<Longrightarrow> fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = x \<or> fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = fst (foldl (heuristic T w) (u0, l0) xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = x \<or> fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = fst (foldl (heuristic T w) (u0, l0) xs)

goal (1 subgoal):
 1. fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))
[PROOF STEP]
using snoc.IH
[PROOF STATE]
proof (prove)
using this:
fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = x \<or> fst (heuristic T w (foldl (heuristic T w) (u0, l0) xs) x) = fst (foldl (heuristic T w) (u0, l0) xs)
fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs)

goal (1 subgoal):
 1. fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (foldl (heuristic T w) (u0, l0) (xs @ [x])) \<in> Set.insert u0 (list.set (xs @ [x]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst (foldl (heuristic T w) (u0, l0) xs) \<in> Set.insert u0 (list.set xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst (foldl (heuristic T w) (u0, l0) ?xs) \<in> Set.insert u0 (list.set ?xs)

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (foldl (heuristic T w) (u0, l0) ?xs) \<in> Set.insert u0 (list.set ?xs)
[PROOF STEP]
have "u' \<in> Set.insert u0 (list.set (filter (isin T) (cg_lookup G u)))"
[PROOF STATE]
proof (prove)
using this:
fst (foldl (heuristic T w) (u0, l0) ?xs) \<in> Set.insert u0 (list.set ?xs)

goal (1 subgoal):
 1. u' \<in> Set.insert u0 (list.set (filter (isin T) (cg_lookup G u)))
[PROOF STEP]
unfolding u'
[PROOF STATE]
proof (prove)
using this:
fst (foldl (heuristic T w) (u0, l0) ?xs) \<in> Set.insert u0 (list.set ?xs)

goal (1 subgoal):
 1. fst (foldl (heuristic T w) (u0, l0) (filter (isin T) (cg_lookup G u))) \<in> Set.insert u0 (list.set (filter (isin T) (cg_lookup G u)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' \<in> Set.insert u0 (list.set (filter (isin T) (cg_lookup G u)))

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u' \<in> Set.insert u0 (list.set (filter (isin T) (cg_lookup G u)))
[PROOF STEP]
have "u' \<in> Set.insert u0 (list.set (cg_lookup G u))"
[PROOF STATE]
proof (prove)
using this:
u' \<in> Set.insert u0 (list.set (filter (isin T) (cg_lookup G u)))

goal (1 subgoal):
 1. u' \<in> Set.insert u0 (list.set (cg_lookup G u))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' \<in> Set.insert u0 (list.set (cg_lookup G u))

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u' \<in> Set.insert u0 (list.set (cg_lookup G u))

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "converge M1 u u0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M1 u u0
[PROOF STEP]
unfolding u'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M1 u u0
[PROOF STEP]
using shortest_list_in_tree_or_default_elem[of "cg_lookup G u" T u]
[PROOF STATE]
proof (prove)
using this:
shortest_list_in_tree_or_default (cg_lookup G u) T u \<in> Set.insert u (list.set (cg_lookup G u))

goal (1 subgoal):
 1. converge M1 u u0
[PROOF STEP]
by (metis assms(1-5) convergence_graph_lookup_invar_def convergence_minimal insert_iff u0)
[PROOF STATE]
proof (state)
this:
converge M1 u u0

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
converge M1 u u0

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "\<And> u' . u' \<in> list.set (cg_lookup G u) \<Longrightarrow> converge M1 u u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u'. u' \<in> list.set (cg_lookup G u) \<Longrightarrow> converge M1 u u'
[PROOF STEP]
using assms(3,4,5)
[PROOF STATE]
proof (prove)
using this:
u \<in> L M1
u \<in> L M2
convergence_graph_lookup_invar M1 M2 cg_lookup G

goal (1 subgoal):
 1. \<And>u'. u' \<in> list.set (cg_lookup G u) \<Longrightarrow> converge M1 u u'
[PROOF STEP]
by (metis convergence_graph_lookup_invar_def)
[PROOF STATE]
proof (state)
this:
?u' \<in> list.set (cg_lookup G u) \<Longrightarrow> converge M1 u ?u'

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u' \<in> Set.insert u0 (list.set (cg_lookup G u))
converge M1 u u0
?u' \<in> list.set (cg_lookup G u) \<Longrightarrow> converge M1 u ?u'
[PROOF STEP]
have "converge M1 u u'"
[PROOF STATE]
proof (prove)
using this:
u' \<in> Set.insert u0 (list.set (cg_lookup G u))
converge M1 u u0
?u' \<in> list.set (cg_lookup G u) \<Longrightarrow> converge M1 u ?u'

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

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
converge M1 u u'

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "u'@w \<in> set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
using \<open>set T' \<subseteq> set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))\<close>
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))

goal (1 subgoal):
 1. u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
unfolding T' insert_set fst_conv
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T \<union> {xs'. \<exists>xs''. u' @ w = xs' @ xs''} \<subseteq> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))

goal (1 subgoal):
 1. u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "converge M2 u u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M2 u u'
[PROOF STEP]
by (metis \<open>u' \<in> Set.insert u0 (list.set (cg_lookup G u))\<close> assms(3) assms(4) assms(5) converge.elims(3) convergence_graph_lookup_invar_def insertE shortest_list_in_tree_or_default_elem u0)
[PROOF STATE]
proof (state)
this:
converge M2 u u'

goal (2 subgoals):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
 2. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
converge M1 u u'
u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
converge M2 u u'
[PROOF STEP]
show "\<exists> u' . converge M1 u u' \<and> u'@w \<in> set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'"
[PROOF STATE]
proof (prove)
using this:
converge M1 u u'
u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
converge M2 u u'

goal (1 subgoal):
 1. \<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>u'. converge M1 u u' \<and> u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) \<and> converge M2 u u'

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "(maximal_prefix_in_language M1 (initial M1) (u'@w)) \<in> L M1"
  and  "(maximal_prefix_in_language M1 (initial M1) (u'@w)) \<in> list.set (prefixes (u'@w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M1 &&& maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> list.set (prefixes (u' @ w))
[PROOF STEP]
using maximal_prefix_in_language_properties[OF assms(1) fsm_initial]
[PROOF STATE]
proof (prove)
using this:
maximal_prefix_in_language M1 (FSM.initial M1) ?io \<in> L M1
maximal_prefix_in_language M1 (FSM.initial M1) ?io \<in> list.set (prefixes ?io)

goal (1 subgoal):
 1. maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M1 &&& maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> list.set (prefixes (u' @ w))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M1
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> list.set (prefixes (u' @ w))

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M1
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> list.set (prefixes (u' @ w))

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "(maximal_prefix_in_language M1 (initial M1) (u'@w)) \<in> set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
using \<open>u'@w \<in> set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))\<close> set_prefix
[PROOF STATE]
proof (prove)
using this:
u' @ w \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
?xs @ ?ys \<in> Prefix_Tree.set ?T \<Longrightarrow> ?xs \<in> Prefix_Tree.set ?T

goal (1 subgoal):
 1. maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
by (metis (no_types, lifting) \<open>maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> list.set (prefixes (u' @ w))\<close> prefixes_set_ob)
[PROOF STATE]
proof (state)
this:
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M1
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> list.set (prefixes (u' @ w))
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "(maximal_prefix_in_language M1 (initial M1) (u'@w)) \<in> L M2"
[PROOF STATE]
proof (prove)
using this:
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M1
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> list.set (prefixes (u' @ w))
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))

goal (1 subgoal):
 1. maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M2
[PROOF STEP]
using assms(7)
[PROOF STATE]
proof (prove)
using this:
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M1
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> list.set (prefixes (u' @ w))
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
L M1 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic)) = L M2 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))

goal (1 subgoal):
 1. maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M2

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
have "convergence_graph_lookup_invar M1 M2 cg_lookup G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup G'
[PROOF STEP]
using assms(5,6) \<open>(maximal_prefix_in_language M1 (initial M1) (u'@w)) \<in> L M1\<close> \<open>(maximal_prefix_in_language M1 (initial M1) (u'@w)) \<in> L M2\<close>
[PROOF STATE]
proof (prove)
using this:
convergence_graph_lookup_invar M1 M2 cg_lookup G
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M1
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M2

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup G'
[PROOF STEP]
unfolding G' convergence_graph_insert_invar_def
[PROOF STATE]
proof (prove)
using this:
convergence_graph_lookup_invar M1 M2 cg_lookup G
\<forall>G \<gamma>. \<gamma> \<in> L M1 \<longrightarrow> \<gamma> \<in> L M2 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup G \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (cg_insert G \<gamma>)
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M1
maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w) \<in> L M2

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (u' @ w)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup G'

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
show "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
using \<open>convergence_graph_lookup_invar M1 M2 cg_lookup G'\<close>
[PROOF STATE]
proof (prove)
using this:
convergence_graph_lookup_invar M1 M2 cg_lookup G'

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))
[PROOF STEP]
unfolding distribute_extension.simps u0 l0 u' T' G' Let_def
[PROOF STATE]
proof (prove)
using this:
convergence_graph_lookup_invar M1 M2 cg_lookup (cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd (if b then (combine (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)) (complete_inputs_to_tree M1 (FSM.initial M1) (outputs_as_list M1) (map fst (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))), cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w))) else (Prefix_Tree.insert T (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w), cg_insert G (maximal_prefix_in_language M1 (FSM.initial M1) (fst (foldl (heuristic T w) (shortest_list_in_tree_or_default (cg_lookup G u) T u, - 1) (filter (isin T) (cg_lookup G u))) @ w)))))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert u w b heuristic))

goal:
No subgoals!
[PROOF STEP]
qed