[STATEMENT]
lemma estimate_growth_result :
  assumes "observable M"
  and     "minimal M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  and     "estimate_growth M dist_fun q1 q2 x y errorValue < errorValue"
shows "\<exists> \<gamma> . distinguishes M q1 q2 ([(x,y)]@\<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
proof (cases "h_obs M q1 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
proof (cases "h_obs M q2 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None

goal (1 subgoal):
 1. \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
using \<open>h_obs M q1 x y = None\<close> assms(5)
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = None
estimate_growth M dist_fun q1 q2 x y errorValue < errorValue

goal (1 subgoal):
 1. \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
case (Some a)
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = Some a

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = Some a
[PROOF STEP]
have "distinguishes M q1 q2 [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = Some a

goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
using h_obs_distinguishes[OF assms(1) _ None] distinguishes_sym
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = Some a
FSM.h_obs M ?q1.0 x y = Some ?q1' \<Longrightarrow> distinguishes M ?q1.0 q1 [(x, y)]
distinguishes ?M ?q1.0 ?q2.0 ?io \<Longrightarrow> distinguishes ?M ?q2.0 ?q1.0 ?io

goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distinguishes M q1 q2 [(x, y)]

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 [(x, y)]

goal (1 subgoal):
 1. \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
case (Some q1')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
proof (cases "h_obs M q2 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = None
[PROOF STEP]
have "distinguishes M q1 q2 [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None

goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
using h_obs_distinguishes[OF assms(1) Some]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M ?q2.0 x y = None \<Longrightarrow> distinguishes M q1 ?q2.0 [(x, y)]

goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distinguishes M q1 q2 [(x, y)]

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 [(x, y)]

goal (1 subgoal):
 1. \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
case (Some q2')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
have "q1' \<noteq> q2'"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. q1' \<noteq> q2'
[PROOF STEP]
using \<open>h_obs M q1 x y = Some q1'\<close> assms(5)
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = Some q2'
FSM.h_obs M q1 x y = Some q1'
estimate_growth M dist_fun q1 q2 x y errorValue < errorValue

goal (1 subgoal):
 1. q1' \<noteq> q2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q1' \<noteq> q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q1' \<noteq> q2'
[PROOF STEP]
obtain \<gamma> where "distinguishes M q1' q2' \<gamma>"
[PROOF STATE]
proof (prove)
using this:
q1' \<noteq> q2'

goal (1 subgoal):
 1. (\<And>\<gamma>. distinguishes M q1' q2' \<gamma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using h_obs_state[OF \<open>h_obs M q1 x y = Some q1'\<close>]
[PROOF STATE]
proof (prove)
using this:
q1' \<noteq> q2'
q1' \<in> FSM.states M

goal (1 subgoal):
 1. (\<And>\<gamma>. distinguishes M q1' q2' \<gamma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using h_obs_state[OF Some]
[PROOF STATE]
proof (prove)
using this:
q1' \<noteq> q2'
q1' \<in> FSM.states M
q2' \<in> FSM.states M

goal (1 subgoal):
 1. (\<And>\<gamma>. distinguishes M q1' q2' \<gamma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>minimal M\<close>
[PROOF STATE]
proof (prove)
using this:
q1' \<noteq> q2'
q1' \<in> FSM.states M
q2' \<in> FSM.states M
minimal M

goal (1 subgoal):
 1. (\<And>\<gamma>. distinguishes M q1' q2' \<gamma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding minimal.simps distinguishes_def
[PROOF STATE]
proof (prove)
using this:
q1' \<noteq> q2'
q1' \<in> FSM.states M
q2' \<in> FSM.states M
\<forall>q\<in>FSM.states M. \<forall>q'\<in>FSM.states M. q \<noteq> q' \<longrightarrow> LS M q \<noteq> LS M q'

goal (1 subgoal):
 1. (\<And>\<gamma>. \<gamma> \<in> LS M q1' \<union> LS M q2' \<and> \<gamma> \<notin> LS M q1' \<inter> LS M q2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinguishes M q1' q2' \<gamma>

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinguishes M q1' q2' \<gamma>
[PROOF STEP]
have "distinguishes M q1 q2 ([(x,y)]@\<gamma>)"
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1' q2' \<gamma>

goal (1 subgoal):
 1. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
using h_obs_language_iff[OF assms(1), of x y \<gamma>]
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1' q2' \<gamma>
((x, y) # \<gamma> \<in> LS M ?q) = (\<exists>q'. FSM.h_obs M ?q x y = Some q' \<and> \<gamma> \<in> LS M q')

goal (1 subgoal):
 1. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
using \<open>h_obs M q1 x y = Some q1'\<close> Some
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1' q2' \<gamma>
((x, y) # \<gamma> \<in> LS M ?q) = (\<exists>q'. FSM.h_obs M ?q x y = Some q' \<and> \<gamma> \<in> LS M q')
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
\<gamma> \<in> LS M q1' \<union> LS M q2' \<and> \<gamma> \<notin> LS M q1' \<inter> LS M q2'
((x, y) # \<gamma> \<in> LS M ?q) = (\<exists>q'. FSM.h_obs M ?q x y = Some q' \<and> \<gamma> \<in> LS M q')
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. [(x, y)] @ \<gamma> \<in> LS M q1 \<union> LS M q2 \<and> [(x, y)] @ \<gamma> \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
distinguishes M q1 q2 ([(x, y)] @ \<gamma>)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinguishes M q1 q2 ([(x, y)] @ \<gamma>)

goal (1 subgoal):
 1. \<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>\<gamma>. distinguishes M q1 q2 ([(x, y)] @ \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shortest_list_or_default_elem :
  "shortest_list_or_default xs x \<in> Set.insert x (list.set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_list_or_default xs x \<in> Set.insert x (list.set xs)
[PROOF STEP]
by (induction xs rule: rev_induct; auto)


[STATEMENT]
lemma shortest_list_elem :
  assumes "xs \<noteq> []"
shows "shortest_list xs \<in> list.set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_list xs \<in> list.set xs
[PROOF STEP]
using assms shortest_list_or_default_elem
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
shortest_list_or_default ?xs ?x \<in> Set.insert ?x (list.set ?xs)

goal (1 subgoal):
 1. shortest_list xs \<in> list.set xs
[PROOF STEP]
by (metis list.simps(15) shortest_list.elims)


[STATEMENT]
lemma shortest_list_in_tree_or_default_elem :
  "shortest_list_in_tree_or_default xs T x \<in> Set.insert x (list.set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_list_in_tree_or_default xs T x \<in> Set.insert x (list.set xs)
[PROOF STEP]
by (induction xs rule: rev_induct; auto)


[STATEMENT]
lemma estimate_growth_Suc :
  assumes "errorValue > 0"
  shows "estimate_growth M get_distinguishing_trace q1 q2 x y errorValue > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < estimate_growth M get_distinguishing_trace q1 q2 x y errorValue
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < errorValue

goal (1 subgoal):
 1. 0 < estimate_growth M get_distinguishing_trace q1 q2 x y errorValue
[PROOF STEP]
unfolding estimate_growth.simps
[PROOF STATE]
proof (prove)
using this:
0 < errorValue

goal (1 subgoal):
 1. 0 < (case FSM.h_obs M q1 x y of None \<Rightarrow> case FSM.h_obs M q1 x y of None \<Rightarrow> errorValue | Some q2' \<Rightarrow> 1 | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> 1 | Some q2' \<Rightarrow> if q1' = q2' \<or> {q1', q2'} = {q1, q2} then errorValue else 1 + 2 * length (get_distinguishing_trace q1 q2))
[PROOF STEP]
by (cases "FSM.h_obs M q1 x y"; cases "FSM.h_obs M q2 x y"; fastforce)


[STATEMENT]
lemma get_extension_result:
  assumes "u \<in> L M1" and "u \<in> L M2"
  and     "convergence_graph_lookup_invar M1 M2 cg_lookup G"
  and     "get_extension T G cg_lookup u x y = Some u'"
shows "converge M1 u u'" and "u' \<in> L M2 \<Longrightarrow> converge M2 u u'" and "u'@[(x,y)] \<in> set T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converge M1 u u' &&& (u' \<in> L M2 \<Longrightarrow> converge M2 u u') &&& u' @ [(x, y)] \<in> Prefix_Tree.set T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. converge M1 u u'
 2. u' \<in> L M2 \<Longrightarrow> converge M2 u u'
 3. u' @ [(x, y)] \<in> Prefix_Tree.set T
[PROOF STEP]
have "find (\<lambda> \<beta> . isin T (\<beta>@[(x,y)])) (u # cg_lookup G u) = Some u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find (\<lambda>\<beta>. isin T (\<beta> @ [(x, y)])) (u # cg_lookup G u) = Some u'
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
get_extension T G cg_lookup u x y = Some u'

goal (1 subgoal):
 1. find (\<lambda>\<beta>. isin T (\<beta> @ [(x, y)])) (u # cg_lookup G u) = Some u'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
find (\<lambda>\<beta>. isin T (\<beta> @ [(x, y)])) (u # cg_lookup G u) = Some u'

goal (3 subgoals):
 1. converge M1 u u'
 2. u' \<in> L M2 \<Longrightarrow> converge M2 u u'
 3. u' @ [(x, y)] \<in> Prefix_Tree.set T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
find (\<lambda>\<beta>. isin T (\<beta> @ [(x, y)])) (u # cg_lookup G u) = Some u'
[PROOF STEP]
have "isin T (u'@[(x,y)])"
[PROOF STATE]
proof (prove)
using this:
find (\<lambda>\<beta>. isin T (\<beta> @ [(x, y)])) (u # cg_lookup G u) = Some u'

goal (1 subgoal):
 1. isin T (u' @ [(x, y)])
[PROOF STEP]
using find_condition
[PROOF STATE]
proof (prove)
using this:
find (\<lambda>\<beta>. isin T (\<beta> @ [(x, y)])) (u # cg_lookup G u) = Some u'
find ?P ?xs = Some ?x \<Longrightarrow> ?P ?x

goal (1 subgoal):
 1. isin T (u' @ [(x, y)])
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
isin T (u' @ [(x, y)])

goal (3 subgoals):
 1. converge M1 u u'
 2. u' \<in> L M2 \<Longrightarrow> converge M2 u u'
 3. u' @ [(x, y)] \<in> Prefix_Tree.set T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isin T (u' @ [(x, y)])
[PROOF STEP]
show "u'@[(x,y)] \<in> set T"
[PROOF STATE]
proof (prove)
using this:
isin T (u' @ [(x, y)])

goal (1 subgoal):
 1. u' @ [(x, y)] \<in> Prefix_Tree.set T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' @ [(x, y)] \<in> Prefix_Tree.set T

goal (2 subgoals):
 1. converge M1 u u'
 2. u' \<in> L M2 \<Longrightarrow> converge M2 u u'
[PROOF STEP]
have "u' \<in> Set.insert u (list.set (cg_lookup G u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' \<in> Set.insert u (list.set (cg_lookup G u))
[PROOF STEP]
using \<open>find (\<lambda> \<beta> . isin T (\<beta>@[(x,y)])) (u # cg_lookup G u) = Some u'\<close>
[PROOF STATE]
proof (prove)
using this:
find (\<lambda>\<beta>. isin T (\<beta> @ [(x, y)])) (u # cg_lookup G u) = Some u'

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

goal (2 subgoals):
 1. converge M1 u u'
 2. u' \<in> L M2 \<Longrightarrow> converge M2 u u'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u' \<in> Set.insert u (list.set (cg_lookup G u))
[PROOF STEP]
show "converge M1 u u'" and "u' \<in> L M2 \<Longrightarrow> converge M2 u u'"
[PROOF STATE]
proof (prove)
using this:
u' \<in> Set.insert u (list.set (cg_lookup G u))

goal (1 subgoal):
 1. converge M1 u u' &&& (u' \<in> L M2 \<Longrightarrow> converge M2 u u')
[PROOF STEP]
using assms(1,2,3)
[PROOF STATE]
proof (prove)
using this:
u' \<in> Set.insert u (list.set (cg_lookup G u))
u \<in> L M1
u \<in> L M2
convergence_graph_lookup_invar M1 M2 cg_lookup G

goal (1 subgoal):
 1. converge M1 u u' &&& (u' \<in> L M2 \<Longrightarrow> converge M2 u u')
[PROOF STEP]
by (metis converge.elims(3) convergence_graph_lookup_invar_def insert_iff)+
[PROOF STATE]
proof (state)
this:
converge M1 u u'
u' \<in> L M2 \<Longrightarrow> converge M2 u u'

goal:
No subgoals!
[PROOF STEP]
qed