[STATEMENT]
lemma traces_to_check_set :
  fixes M :: "('a,'b::linorder,'c::linorder) fsm"
  assumes "observable M"
  and     "q \<in> states M"
shows "list.set (traces_to_check M q k) = {(\<gamma> @ [(x, y)]) | \<gamma> x y . length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> inputs M \<and> y \<in> outputs M}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
q \<in> FSM.states M

goal (1 subgoal):
 1. list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
proof (induction k arbitrary: q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q 0) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> 0 \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
 2. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
q \<in> FSM.states M

goal (2 subgoals):
 1. \<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q 0) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> 0 \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
 2. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> FSM.states M
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q \<in> FSM.states M

goal (1 subgoal):
 1. list.set (traces_to_check M q 0) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> 0 \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list.set (traces_to_check M q 0) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> 0 \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
?q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M ?q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M ?q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
q \<in> FSM.states M

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
define ios where ios: "ios  = List.product (inputs_as_list M) (outputs_as_list M)"
[PROOF STATE]
proof (state)
this:
ios = List.product (inputs_as_list M) (outputs_as_list M)

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
define f where f: "f = (\<lambda>(x,y) . case h_obs M q x y of None \<Rightarrow> [[(x,y)]] | Some q' \<Rightarrow> [(x,y)] # (map ((#) (x,y)) (traces_to_check M q' k)))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>(x, y). case FSM.h_obs M q x y of None \<Rightarrow> [[(x, y)]] | Some q' \<Rightarrow> [(x, y)] # map ((#) (x, y)) (traces_to_check M q' k))

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
have "list.set ios = inputs M \<times> outputs M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set ios = FSM.inputs M \<times> FSM.outputs M
[PROOF STEP]
using inputs_as_list_set outputs_as_list_set
[PROOF STATE]
proof (prove)
using this:
list.set (inputs_as_list ?M) = FSM.inputs ?M
list.set (outputs_as_list ?M) = FSM.outputs ?M

goal (1 subgoal):
 1. list.set ios = FSM.inputs M \<times> FSM.outputs M
[PROOF STEP]
unfolding ios
[PROOF STATE]
proof (prove)
using this:
list.set (inputs_as_list ?M) = FSM.inputs ?M
list.set (outputs_as_list ?M) = FSM.outputs ?M

goal (1 subgoal):
 1. list.set (List.product (inputs_as_list M) (outputs_as_list M)) = FSM.inputs M \<times> FSM.outputs M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list.set ios = FSM.inputs M \<times> FSM.outputs M

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list.set ios = FSM.inputs M \<times> FSM.outputs M

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
have "traces_to_check M q (Suc k) = concat (map f ios)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. traces_to_check M q (Suc k) = concat (map f ios)
[PROOF STEP]
unfolding f ios
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. traces_to_check M q (Suc k) = concat (map (\<lambda>(x, y). case FSM.h_obs M q x y of None \<Rightarrow> [[(x, y)]] | Some q' \<Rightarrow> [(x, y)] # map ((#) (x, y)) (traces_to_check M q' k)) (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
traces_to_check M q (Suc k) = concat (map f ios)

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list.set ios = FSM.inputs M \<times> FSM.outputs M
traces_to_check M q (Suc k) = concat (map f ios)
[PROOF STEP]
have in_ex : "\<And> io . io \<in> list.set (traces_to_check M q (Suc k)) \<longleftrightarrow> (\<exists> x y . x \<in> inputs M \<and> y \<in> outputs M \<and> io \<in> list.set (f (x,y)))"
[PROOF STATE]
proof (prove)
using this:
list.set ios = FSM.inputs M \<times> FSM.outputs M
traces_to_check M q (Suc k) = concat (map f ios)

goal (1 subgoal):
 1. \<And>io. (io \<in> list.set (traces_to_check M q (Suc k))) = (\<exists>x y. x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M \<and> io \<in> list.set (f (x, y)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(?io \<in> list.set (traces_to_check M q (Suc k))) = (\<exists>x y. x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M \<and> ?io \<in> list.set (f (x, y)))

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> list.set (traces_to_check M q k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}; q \<in> FSM.states M\<rbrakk> \<Longrightarrow> list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. list.set (traces_to_check M q (Suc k)) \<subseteq> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
 2. {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
show "list.set (traces_to_check M q (Suc k)) \<subseteq> {(\<gamma> @ [(x, y)]) | \<gamma> x y . length (\<gamma> @ [(x, y)]) \<le> (Suc k) \<and> \<gamma> \<in> LS M q \<and> x \<in> inputs M \<and> y \<in> outputs M}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (traces_to_check M q (Suc k)) \<subseteq> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> list.set (traces_to_check M q (Suc k)) \<Longrightarrow> x \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> list.set (traces_to_check M q (Suc k)) \<Longrightarrow> x \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
assume "io \<in> list.set (traces_to_check M q (Suc k))"
[PROOF STATE]
proof (state)
this:
io \<in> list.set (traces_to_check M q (Suc k))

goal (1 subgoal):
 1. \<And>x. x \<in> list.set (traces_to_check M q (Suc k)) \<Longrightarrow> x \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
obtain x y where "x \<in> inputs M" and "y \<in> outputs M"
                        and "io \<in> list.set (f (x,y))"
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (traces_to_check M q (Suc k))

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> FSM.inputs M; y \<in> FSM.outputs M; io \<in> list.set (f (x, y))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using in_ex
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (traces_to_check M q (Suc k))
(?io \<in> list.set (traces_to_check M q (Suc k))) = (\<exists>x y. x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M \<and> ?io \<in> list.set (f (x, y)))

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> FSM.inputs M; y \<in> FSM.outputs M; io \<in> list.set (f (x, y))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> FSM.inputs M
y \<in> FSM.outputs M
io \<in> list.set (f (x, y))

goal (1 subgoal):
 1. \<And>x. x \<in> list.set (traces_to_check M q (Suc k)) \<Longrightarrow> x \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
have "[(x,y)] \<in> {(\<gamma> @ [(x, y)]) | \<gamma> x y . length (\<gamma> @ [(x, y)]) \<le> (Suc k) \<and> \<gamma> \<in> LS M q \<and> x \<in> inputs M \<and> y \<in> outputs M}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
have "length ([] @ [(x, y)]) \<le> Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ([] @ [(x, y)]) \<le> Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ([] @ [(x, y)]) \<le> Suc k

goal (1 subgoal):
 1. [(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length ([] @ [(x, y)]) \<le> Suc k

goal (1 subgoal):
 1. [(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
have "[] \<in> LS M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<in> LS M q
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
q \<in> FSM.states M

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

goal (1 subgoal):
 1. [(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length ([] @ [(x, y)]) \<le> Suc k
[] \<in> LS M q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length ([] @ [(x, y)]) \<le> Suc k
[] \<in> LS M q

goal (1 subgoal):
 1. [(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
using \<open>x \<in> inputs M\<close> \<open>y \<in> outputs M\<close>
[PROOF STATE]
proof (prove)
using this:
length ([] @ [(x, y)]) \<le> Suc k
[] \<in> LS M q
x \<in> FSM.inputs M
y \<in> FSM.outputs M

goal (1 subgoal):
 1. [(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. \<And>x. x \<in> list.set (traces_to_check M q (Suc k)) \<Longrightarrow> x \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
show "io \<in> {(\<gamma> @ [(x, y)]) | \<gamma> x y . length (\<gamma> @ [(x, y)]) \<le> (Suc k) \<and> \<gamma> \<in> LS M q \<and> x \<in> inputs M \<and> y \<in> outputs M}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
proof (cases "h_obs M q x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q x y = None \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
 2. \<And>a. FSM.h_obs M q x y = Some a \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q x y = None

goal (2 subgoals):
 1. FSM.h_obs M q x y = None \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
 2. \<And>a. FSM.h_obs M q x y = Some a \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q x y = None
[PROOF STEP]
have "io = [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q x y = None

goal (1 subgoal):
 1. io = [(x, y)]
[PROOF STEP]
using \<open>io \<in> list.set (f (x,y))\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q x y = None
io \<in> list.set (f (x, y))

goal (1 subgoal):
 1. io = [(x, y)]
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q x y = None
io \<in> list.set (case (x, y) of (x, y) \<Rightarrow> case FSM.h_obs M q x y of None \<Rightarrow> [[(x, y)]] | Some q' \<Rightarrow> [(x, y)] # map ((#) (x, y)) (traces_to_check M q' k))

goal (1 subgoal):
 1. io = [(x, y)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io = [(x, y)]

goal (2 subgoals):
 1. FSM.h_obs M q x y = None \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
 2. \<And>a. FSM.h_obs M q x y = Some a \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io = [(x, y)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io = [(x, y)]

goal (1 subgoal):
 1. io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
using \<open>[(x,y)] \<in> {(\<gamma> @ [(x, y)]) | \<gamma> x y . length (\<gamma> @ [(x, y)]) \<le> (Suc k) \<and> \<gamma> \<in> LS M q \<and> x \<in> inputs M \<and> y \<in> outputs M}\<close>
[PROOF STATE]
proof (prove)
using this:
io = [(x, y)]
[(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q x y = Some a \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q x y = Some a \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
case (Some q')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q x y = Some q'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q x y = Some a \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q x y = Some q'
[PROOF STEP]
consider "io = [(x,y)]" | "io \<in> list.set (map ((#) (x,y)) (traces_to_check M q' k))"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q x y = Some q'

goal (1 subgoal):
 1. \<lbrakk>io = [(x, y)] \<Longrightarrow> thesis; io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using \<open>io \<in> list.set (f (x,y))\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q x y = Some q'
io \<in> list.set (f (x, y))

goal (1 subgoal):
 1. \<lbrakk>io = [(x, y)] \<Longrightarrow> thesis; io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q x y = Some q'
io \<in> list.set (case (x, y) of (x, y) \<Rightarrow> case FSM.h_obs M q x y of None \<Rightarrow> [[(x, y)]] | Some q' \<Rightarrow> [(x, y)] # map ((#) (x, y)) (traces_to_check M q' k))

goal (1 subgoal):
 1. \<lbrakk>io = [(x, y)] \<Longrightarrow> thesis; io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>io = [(x, y)] \<Longrightarrow> ?thesis; io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q x y = Some a \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>io = [(x, y)] \<Longrightarrow> ?thesis; io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>io = [(x, y)] \<Longrightarrow> ?thesis; io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. io = [(x, y)] \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
 2. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
io = [(x, y)]

goal (2 subgoals):
 1. io = [(x, y)] \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
 2. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io = [(x, y)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io = [(x, y)]

goal (1 subgoal):
 1. io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
using \<open>[(x,y)] \<in> {(\<gamma> @ [(x, y)]) | \<gamma> x y . length (\<gamma> @ [(x, y)]) \<le> (Suc k) \<and> \<gamma> \<in> LS M q \<and> x \<in> inputs M \<and> y \<in> outputs M}\<close>
[PROOF STATE]
proof (prove)
using this:
io = [(x, y)]
[(x, y)] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k))

goal (1 subgoal):
 1. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k))
[PROOF STEP]
obtain io' where "io = (x,y)#io'" and "io' \<in> list.set (traces_to_check M q' k)"
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k))

goal (1 subgoal):
 1. (\<And>io'. \<lbrakk>io = (x, y) # io'; io' \<in> list.set (traces_to_check M q' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io = (x, y) # io'
io' \<in> list.set (traces_to_check M q' k)

goal (1 subgoal):
 1. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io = (x, y) # io'
io' \<in> list.set (traces_to_check M q' k)
[PROOF STEP]
have "io' \<in> {(\<gamma> @ [(x, y)]) | \<gamma> x y . length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> inputs M \<and> y \<in> outputs M}"
[PROOF STATE]
proof (prove)
using this:
io = (x, y) # io'
io' \<in> list.set (traces_to_check M q' k)

goal (1 subgoal):
 1. io' \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
using Suc.IH[OF h_obs_state[OF Some]]
[PROOF STATE]
proof (prove)
using this:
io = (x, y) # io'
io' \<in> list.set (traces_to_check M q' k)
list.set (traces_to_check M q' k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. io' \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io' \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io' \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
obtain \<gamma> x' y' where "io' = (\<gamma> @ [(x', y')])" and "length (\<gamma> @ [(x', y')]) \<le> k" and "\<gamma> \<in> LS M q'" and "x' \<in> inputs M" and "y' \<in> outputs M"
[PROOF STATE]
proof (prove)
using this:
io' \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. (\<And>\<gamma> x' y'. \<lbrakk>io' = \<gamma> @ [(x', y')]; length (\<gamma> @ [(x', y')]) \<le> k; \<gamma> \<in> LS M q'; x' \<in> FSM.inputs M; y' \<in> FSM.outputs M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io' = \<gamma> @ [(x', y')]
length (\<gamma> @ [(x', y')]) \<le> k
\<gamma> \<in> LS M q'
x' \<in> FSM.inputs M
y' \<in> FSM.outputs M

goal (1 subgoal):
 1. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
have "length (((x,y)#\<gamma>) @ [(x', y')]) \<le> Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (((x, y) # \<gamma>) @ [(x', y')]) \<le> Suc k
[PROOF STEP]
using \<open>length (\<gamma> @ [(x', y')]) \<le> k\<close>
[PROOF STATE]
proof (prove)
using this:
length (\<gamma> @ [(x', y')]) \<le> k

goal (1 subgoal):
 1. length (((x, y) # \<gamma>) @ [(x', y')]) \<le> Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (((x, y) # \<gamma>) @ [(x', y')]) \<le> Suc k

goal (1 subgoal):
 1. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (((x, y) # \<gamma>) @ [(x', y')]) \<le> Suc k

goal (1 subgoal):
 1. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
have "((x,y)#\<gamma>) \<in> LS M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) # \<gamma> \<in> LS M q
[PROOF STEP]
using \<open>\<gamma> \<in> LS M q'\<close> Some assms(1)
[PROOF STATE]
proof (prove)
using this:
\<gamma> \<in> LS M q'
FSM.h_obs M q x y = Some q'
observable M

goal (1 subgoal):
 1. (x, y) # \<gamma> \<in> LS M q
[PROOF STEP]
by (meson h_obs_language_iff)
[PROOF STATE]
proof (state)
this:
(x, y) # \<gamma> \<in> LS M q

goal (1 subgoal):
 1. io \<in> list.set (map ((#) (x, y)) (traces_to_check M q' k)) \<Longrightarrow> io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (((x, y) # \<gamma>) @ [(x', y')]) \<le> Suc k
(x, y) # \<gamma> \<in> LS M q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (((x, y) # \<gamma>) @ [(x', y')]) \<le> Suc k
(x, y) # \<gamma> \<in> LS M q

goal (1 subgoal):
 1. io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
using \<open>x' \<in> inputs M\<close> \<open>y' \<in> outputs M\<close>
[PROOF STATE]
proof (prove)
using this:
length (((x, y) # \<gamma>) @ [(x', y')]) \<le> Suc k
(x, y) # \<gamma> \<in> LS M q
x' \<in> FSM.inputs M
y' \<in> FSM.outputs M

goal (1 subgoal):
 1. io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
unfolding \<open>io = (x,y)#io'\<close> \<open>io' = (\<gamma> @ [(x', y')])\<close>
[PROOF STATE]
proof (prove)
using this:
length (((x, y) # \<gamma>) @ [(x', y')]) \<le> Suc k
(x, y) # \<gamma> \<in> LS M q
x' \<in> FSM.inputs M
y' \<in> FSM.outputs M

goal (1 subgoal):
 1. (x, y) # \<gamma> @ [(x', y')] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list.set (traces_to_check M q (Suc k)) \<subseteq> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
show "{\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> list.set (traces_to_check M q (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<Longrightarrow> x \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<Longrightarrow> x \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
assume "io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}"
[PROOF STATE]
proof (state)
this:
io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. \<And>x. x \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<Longrightarrow> x \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
obtain \<gamma> x' y' where "io = (\<gamma> @ [(x', y')])" and "length (\<gamma> @ [(x', y')]) \<le> Suc k" and "\<gamma> \<in> LS M q" and "x' \<in> inputs M" and "y' \<in> outputs M"
[PROOF STATE]
proof (prove)
using this:
io \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. (\<And>\<gamma> x' y'. \<lbrakk>io = \<gamma> @ [(x', y')]; length (\<gamma> @ [(x', y')]) \<le> Suc k; \<gamma> \<in> LS M q; x' \<in> FSM.inputs M; y' \<in> FSM.outputs M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io = \<gamma> @ [(x', y')]
length (\<gamma> @ [(x', y')]) \<le> Suc k
\<gamma> \<in> LS M q
x' \<in> FSM.inputs M
y' \<in> FSM.outputs M

goal (1 subgoal):
 1. \<And>x. x \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<Longrightarrow> x \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
show "io \<in> list.set (traces_to_check M q (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
proof (cases \<gamma>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<gamma> = [] \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
 2. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<gamma> = []

goal (2 subgoals):
 1. \<gamma> = [] \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
 2. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<gamma> = []
[PROOF STEP]
have "io = [(x',y')]"
[PROOF STATE]
proof (prove)
using this:
\<gamma> = []

goal (1 subgoal):
 1. io = [(x', y')]
[PROOF STEP]
using \<open>io = (\<gamma> @ [(x', y')])\<close>
[PROOF STATE]
proof (prove)
using this:
\<gamma> = []
io = \<gamma> @ [(x', y')]

goal (1 subgoal):
 1. io = [(x', y')]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io = [(x', y')]

goal (2 subgoals):
 1. \<gamma> = [] \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
 2. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
have "io \<in> list.set (f (x',y'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<in> list.set (f (x', y'))
[PROOF STEP]
unfolding f case_prod_conv \<open>io = [(x',y')]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x', y')] \<in> list.set (case FSM.h_obs M q x' y' of None \<Rightarrow> [[(x', y')]] | Some q' \<Rightarrow> [(x', y')] # map ((#) (x', y')) (traces_to_check M q' k))
[PROOF STEP]
by (cases "FSM.h_obs M q x' y'"; auto)
[PROOF STATE]
proof (state)
this:
io \<in> list.set (f (x', y'))

goal (2 subgoals):
 1. \<gamma> = [] \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
 2. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> list.set (f (x', y'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (f (x', y'))

goal (1 subgoal):
 1. io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
using in_ex[of io] \<open>x' \<in> inputs M\<close> \<open>y' \<in> outputs M\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (f (x', y'))
(io \<in> list.set (traces_to_check M q (Suc k))) = (\<exists>x y. x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M \<and> io \<in> list.set (f (x, y)))
x' \<in> FSM.inputs M
y' \<in> FSM.outputs M

goal (1 subgoal):
 1. io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> list.set (traces_to_check M q (Suc k))

goal (1 subgoal):
 1. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
case (Cons xy \<gamma>')
[PROOF STATE]
proof (state)
this:
\<gamma> = xy # \<gamma>'

goal (1 subgoal):
 1. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
obtain x y where "xy = (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. xy = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = (x1, x2) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>x y. xy = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
xy = (x, y)

goal (1 subgoal):
 1. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
obtain q' where "h_obs M q x y = Some q'"  and "x \<in> inputs M" and "y \<in> outputs M" and "\<gamma>' \<in> LS M q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>FSM.h_obs M q x y = Some q'; x \<in> FSM.inputs M; y \<in> FSM.outputs M; \<gamma>' \<in> LS M q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<gamma> \<in> LS M q\<close>
[PROOF STATE]
proof (prove)
using this:
\<gamma> \<in> LS M q

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>FSM.h_obs M q x y = Some q'; x \<in> FSM.inputs M; y \<in> FSM.outputs M; \<gamma>' \<in> LS M q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Cons \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
(x, y) # \<gamma>' \<in> LS M q

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>FSM.h_obs M q x y = Some q'; x \<in> FSM.inputs M; y \<in> FSM.outputs M; \<gamma>' \<in> LS M q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms(1) h_obs_language_iff language_io(1) language_io(2) list.set_intros(1))
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q x y = Some q'
x \<in> FSM.inputs M
y \<in> FSM.outputs M
\<gamma>' \<in> LS M q'

goal (1 subgoal):
 1. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q x y = Some q'
x \<in> FSM.inputs M
y \<in> FSM.outputs M
\<gamma>' \<in> LS M q'
[PROOF STEP]
have "\<gamma>'@[(x',y')] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q x y = Some q'
x \<in> FSM.inputs M
y \<in> FSM.outputs M
\<gamma>' \<in> LS M q'

goal (1 subgoal):
 1. \<gamma>' @ [(x', y')] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
using \<open>length (\<gamma> @ [(x', y')]) \<le> Suc k\<close> \<open>x' \<in> inputs M\<close> \<open>y' \<in> outputs M\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q x y = Some q'
x \<in> FSM.inputs M
y \<in> FSM.outputs M
\<gamma>' \<in> LS M q'
length (\<gamma> @ [(x', y')]) \<le> Suc k
x' \<in> FSM.inputs M
y' \<in> FSM.outputs M

goal (1 subgoal):
 1. \<gamma>' @ [(x', y')] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
unfolding Cons
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q x y = Some q'
x \<in> FSM.inputs M
y \<in> FSM.outputs M
\<gamma>' \<in> LS M q'
length ((xy # \<gamma>') @ [(x', y')]) \<le> Suc k
x' \<in> FSM.inputs M
y' \<in> FSM.outputs M

goal (1 subgoal):
 1. \<gamma>' @ [(x', y')] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<gamma>' @ [(x', y')] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<gamma>' @ [(x', y')] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
have "\<gamma>'@[(x',y')] \<in> list.set (traces_to_check M q' k)"
[PROOF STATE]
proof (prove)
using this:
\<gamma>' @ [(x', y')] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. \<gamma>' @ [(x', y')] \<in> list.set (traces_to_check M q' k)
[PROOF STEP]
using Suc.IH[OF h_obs_state[OF \<open>h_obs M q x y = Some q'\<close>]]
[PROOF STATE]
proof (prove)
using this:
\<gamma>' @ [(x', y')] \<in> {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
list.set (traces_to_check M q' k) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> k \<and> \<gamma> \<in> LS M q' \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. \<gamma>' @ [(x', y')] \<in> list.set (traces_to_check M q' k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma>' @ [(x', y')] \<in> list.set (traces_to_check M q' k)

goal (1 subgoal):
 1. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<gamma>' @ [(x', y')] \<in> list.set (traces_to_check M q' k)
[PROOF STEP]
have "io \<in> list.set (f (x,y))"
[PROOF STATE]
proof (prove)
using this:
\<gamma>' @ [(x', y')] \<in> list.set (traces_to_check M q' k)

goal (1 subgoal):
 1. io \<in> list.set (f (x, y))
[PROOF STEP]
unfolding f case_prod_conv \<open>h_obs M q x y = Some q'\<close>
[PROOF STATE]
proof (prove)
using this:
\<gamma>' @ [(x', y')] \<in> list.set (traces_to_check M q' k)

goal (1 subgoal):
 1. io \<in> list.set (case Some q' of None \<Rightarrow> [[(x, y)]] | Some q' \<Rightarrow> [(x, y)] # map ((#) (x, y)) (traces_to_check M q' k))
[PROOF STEP]
unfolding \<open>io = (\<gamma> @ [(x', y')])\<close> Cons \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
\<gamma>' @ [(x', y')] \<in> list.set (traces_to_check M q' k)

goal (1 subgoal):
 1. ((x, y) # \<gamma>') @ [(x', y')] \<in> list.set (case Some q' of None \<Rightarrow> [[(x, y)]] | Some q' \<Rightarrow> [(x, y)] # map ((#) (x, y)) (traces_to_check M q' k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io \<in> list.set (f (x, y))

goal (1 subgoal):
 1. \<And>a list. \<gamma> = a # list \<Longrightarrow> io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> list.set (f (x, y))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (f (x, y))

goal (1 subgoal):
 1. io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
using in_ex[of io] \<open>x \<in> inputs M\<close> \<open>y \<in> outputs M\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (f (x, y))
(io \<in> list.set (traces_to_check M q (Suc k))) = (\<exists>x y. x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M \<and> io \<in> list.set (f (x, y)))
x \<in> FSM.inputs M
y \<in> FSM.outputs M

goal (1 subgoal):
 1. io \<in> list.set (traces_to_check M q (Suc k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> list.set (traces_to_check M q (Suc k))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io \<in> list.set (traces_to_check M q (Suc k))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> list.set (traces_to_check M q (Suc k))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list.set (traces_to_check M q (Suc k)) = {\<gamma> @ [(x, y)] |\<gamma> x y. length (\<gamma> @ [(x, y)]) \<le> Suc k \<and> \<gamma> \<in> LS M q \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma appendDistTrace_subset_helper :
  assumes "appendDistTrace = (\<lambda> (T,G) w . let
                                            (T',G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u@w) False (append_heuristic_input M)
                                            in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u@w) False (append_heuristic_input M))"
shows "set T \<subseteq> set (fst (appendDistTrace (T,G) w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (appendDistTrace (T, G) w))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (appendDistTrace (T, G) w))
[PROOF STEP]
obtain T' G' where ***: "distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u@w) False (append_heuristic_input M) = (T',G')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T' G'. distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) = (T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = (x1, x2) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>T' G'. distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) = (T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) = (T', G')

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (appendDistTrace (T, G) w))
[PROOF STEP]
show "set T \<subseteq> set (fst (appendDistTrace (T,G) w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (appendDistTrace (T, G) w))
[PROOF STEP]
using distribute_extension_subset[of T M G cg_lookup cg_insert \<alpha> "xy#u@w" False "(append_heuristic_input M)"]
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M)))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (appendDistTrace (T, G) w))
[PROOF STEP]
using distribute_extension_subset[of T' M G' cg_lookup cg_insert \<beta> "u@w" False "(append_heuristic_input M)"]
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M)))
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (appendDistTrace (T, G) w))
[PROOF STEP]
unfolding assms case_prod_conv *** Let_def fst_conv
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set T'
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (appendDistTrace (T, G) w))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma handleTrace_subset_helper :
  assumes "handleTrace = (\<lambda> (T,G) u .
          if is_in_language M qTarget u
            then let
                qu = FSM.after M qTarget u;
                ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu);
                appendDistTrace = (\<lambda> (T,G) w . let
                                                  (T',G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u@w) False (append_heuristic_input M)
                                                in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u@w) False (append_heuristic_input M))
                in foldl appendDistTrace (T,G) ws
            else let
                (T',G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u) False (append_heuristic_input M)
                in distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M))"
shows "set T \<subseteq> set (fst (handleTrace (T,G) u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
proof (cases "is_in_language M qTarget u")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_in_language M qTarget u

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
define qu where qu: "qu = FSM.after M qTarget u"
[PROOF STATE]
proof (state)
this:
qu = FSM.after M qTarget u

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
define ws where ws: "ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu)"
[PROOF STATE]
proof (state)
this:
ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu)

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
define appendDistTrace where appendDistTrace: "appendDistTrace = (\<lambda> (T,G) w . let
                                            (T',G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u@w) False (append_heuristic_input M)
                                            in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u@w) False (append_heuristic_input M))"
[PROOF STATE]
proof (state)
this:
appendDistTrace = (\<lambda>(T, G) w. let (T', G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M))

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
have **: "handleTrace (T,G) u = foldl appendDistTrace (T,G) ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. handleTrace (T, G) u = foldl appendDistTrace (T, G) ws
[PROOF STEP]
unfolding qu ws appendDistTrace Let_def case_prod_conv assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if is_in_language M qTarget u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u))) else case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)) = foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u)))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
is_in_language M qTarget u

goal (1 subgoal):
 1. (if is_in_language M qTarget u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u))) else case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)) = foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
handleTrace (T, G) u = foldl appendDistTrace (T, G) ws

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
using appendDistTrace_subset_helper[OF appendDistTrace]
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (appendDistTrace (?T, ?G) ?w))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
unfolding **
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (appendDistTrace (?T, ?G) ?w))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl appendDistTrace (T, G) ws))
[PROOF STEP]
apply (induction ws rule: rev_induct; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>Collect (isin T) \<subseteq> Collect (isin (fst (foldl appendDistTrace (T, G) xs))); \<And>T G w. Collect (isin T) \<subseteq> Collect (isin (fst (appendDistTrace (T, G) w)))\<rbrakk> \<Longrightarrow> Collect (isin T) \<subseteq> Collect (isin (fst (appendDistTrace (foldl appendDistTrace (T, G) xs) x)))
[PROOF STEP]
by (metis (no_types, opaque_lifting) Collect_mono_iff fst_conv old.prod.exhaust)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))

goal (1 subgoal):
 1. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_in_language M qTarget u

goal (1 subgoal):
 1. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
obtain T' G' where ***: "distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u) False (append_heuristic_input M) = (T',G')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T' G'. distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) = (T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = (x1, x2) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>T' G'. distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) = (T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) = (T', G')

goal (1 subgoal):
 1. \<not> is_in_language M qTarget u \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
show "set T \<subseteq> set (fst (handleTrace (T, G) u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
using distribute_extension_subset[of T M G cg_lookup cg_insert \<alpha> "xy#u" False "(append_heuristic_input M)"]
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M)))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
using distribute_extension_subset[of T' M G' cg_lookup cg_insert \<beta> "u" False "(append_heuristic_input M)"]
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M)))
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M)))
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)))
\<not> is_in_language M qTarget u

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
unfolding case_prod_conv *** Let_def fst_conv assms
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set T'
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)))
\<not> is_in_language M qTarget u

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (if is_in_language M qTarget u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u))) else distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma establish_convergence_static_finite :
  fixes M :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  assumes "finite_tree T"
shows "finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define \<alpha> where \<alpha>: "\<alpha> = V (t_source t)"
[PROOF STATE]
proof (state)
this:
\<alpha> = V (t_source t)

goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define xy where xy: "xy = (t_input t, t_output t)"
[PROOF STATE]
proof (state)
this:
xy = (t_input t, t_output t)

goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define \<beta> where \<beta>: "\<beta> = V (t_target t)"
[PROOF STATE]
proof (state)
this:
\<beta> = V (t_target t)

goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define qSource where qSource: "qSource = (after_initial M (V (t_source t)))"
[PROOF STATE]
proof (state)
this:
qSource = after_initial M (V (t_source t))

goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define qTarget where qTarget: "qTarget = (after_initial M (V (t_target t)))"
[PROOF STATE]
proof (state)
this:
qTarget = after_initial M (V (t_target t))

goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define k where k: "k = m - size_r M"
[PROOF STATE]
proof (state)
this:
k = m - size_r M

goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define ttc where ttc : "ttc = [] # traces_to_check M qTarget k"
[PROOF STATE]
proof (state)
this:
ttc = [] # traces_to_check M qTarget k

goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define handleTrace where handleTrace: "handleTrace = (\<lambda> (T,G) u .
          if is_in_language M qTarget u
            then let
                qu = FSM.after M qTarget u;
                ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu);
                appendDistTrace = (\<lambda> (T,G) w . let
                                                  (T',G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u@w) False (append_heuristic_input M)
                                                in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u@w) False (append_heuristic_input M))
                in foldl appendDistTrace (T,G) ws
            else let
                (T',G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u) False (append_heuristic_input M)
                in distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M))"
[PROOF STATE]
proof (state)
this:
handleTrace = (\<lambda>(T, G) u. if is_in_language M qTarget u then let qu = FSM.after M qTarget u; ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu); appendDistTrace = \<lambda>(T, G) w. let (T', G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M) in foldl appendDistTrace (T, G) ws else let (T', G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M))

goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
have *:"establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t = foldl handleTrace (T,G) ttc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t = foldl handleTrace (T, G) ttc
[PROOF STEP]
unfolding establish_convergence_static.simps \<alpha> xy \<beta> qSource qTarget k ttc handleTrace Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>(T, G) u. if is_in_language M (after_initial M (V (t_target t))) u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M (after_initial M (V (t_target t))) u))) else case distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) u False (append_heuristic_input M)) (T, G) ([] # traces_to_check M (after_initial M (V (t_target t))) (m - size_r M)) = foldl (\<lambda>(T, G) u. if is_in_language M (after_initial M (V (t_target t))) u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M (after_initial M (V (t_target t))) u))) else case distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) u False (append_heuristic_input M)) (T, G) ([] # traces_to_check M (after_initial M (V (t_target t))) (m - size_r M))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t = foldl handleTrace (T, G) ttc

goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (foldl handleTrace (T, G) ttc))
[PROOF STEP]
proof (induction ttc rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite_tree (fst (foldl handleTrace (T, G) []))
 2. \<And>x xs. finite_tree (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> finite_tree (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite_tree (fst (foldl handleTrace (T, G) []))
 2. \<And>x xs. finite_tree (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> finite_tree (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (foldl handleTrace (T, G) []))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite_tree T

goal (1 subgoal):
 1. finite_tree (fst (foldl handleTrace (T, G) []))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (fst (foldl handleTrace (T, G) []))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> finite_tree (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> finite_tree (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
case (snoc io ttc)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (foldl handleTrace (T, G) ttc))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> finite_tree (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
have *:"foldl handleTrace (T, G) (ttc@[io]) = handleTrace (foldl handleTrace (T,G) ttc) io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl handleTrace (T, G) (ttc @ [io]) = handleTrace (foldl handleTrace (T, G) ttc) io
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl handleTrace (T, G) (ttc @ [io]) = handleTrace (foldl handleTrace (T, G) ttc) io

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> finite_tree (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
have "\<And> u T G . finite_tree T \<Longrightarrow> finite_tree (fst (handleTrace (T,G) u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
fix T :: "('b\<times>'c) prefix_tree"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
fix u G
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
assume "finite_tree T"
[PROOF STATE]
proof (state)
this:
finite_tree T

goal (1 subgoal):
 1. \<And>u T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
show "finite_tree (fst (handleTrace (T,G) u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
proof (cases "is_in_language M qTarget u")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_in_language M qTarget u

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
define qu where qu: "qu = FSM.after M qTarget u"
[PROOF STATE]
proof (state)
this:
qu = FSM.after M qTarget u

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
define ws where ws: "ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu)"
[PROOF STATE]
proof (state)
this:
ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu)

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
define appendDistTrace where appendDistTrace: "appendDistTrace = (\<lambda> (T,G) w . let
                                                  (T',G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u@w) False (append_heuristic_input M)
                                                  in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u@w) False (append_heuristic_input M))"
[PROOF STATE]
proof (state)
this:
appendDistTrace = (\<lambda>(T, G) w. let (T', G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M))

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
have **: "handleTrace (T,G) u = foldl appendDistTrace (T,G) ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. handleTrace (T, G) u = foldl appendDistTrace (T, G) ws
[PROOF STEP]
unfolding handleTrace qu ws appendDistTrace Let_def case_prod_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if is_in_language M qTarget u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u))) else case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)) = foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u)))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
is_in_language M qTarget u

goal (1 subgoal):
 1. (if is_in_language M qTarget u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u))) else case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)) = foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
handleTrace (T, G) u = foldl appendDistTrace (T, G) ws

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
have "\<And> w T G . finite_tree T \<Longrightarrow> finite_tree (fst (appendDistTrace (T,G) w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w T G. finite_tree T \<Longrightarrow> finite_tree (fst (appendDistTrace (T, G) w))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w T G. finite_tree T \<Longrightarrow> finite_tree (fst (appendDistTrace (T, G) w))
[PROOF STEP]
fix T :: "('b\<times>'c) prefix_tree"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w T G. finite_tree T \<Longrightarrow> finite_tree (fst (appendDistTrace (T, G) w))
[PROOF STEP]
fix w G
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w T G. finite_tree T \<Longrightarrow> finite_tree (fst (appendDistTrace (T, G) w))
[PROOF STEP]
assume "finite_tree T"
[PROOF STATE]
proof (state)
this:
finite_tree T

goal (1 subgoal):
 1. \<And>w T G. finite_tree T \<Longrightarrow> finite_tree (fst (appendDistTrace (T, G) w))
[PROOF STEP]
obtain T' G' where ***: "distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u@w) False (append_heuristic_input M) = (T',G')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T' G'. distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) = (T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = (x1, x2) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>T' G'. distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) = (T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) = (T', G')

goal (1 subgoal):
 1. \<And>w T G. finite_tree T \<Longrightarrow> finite_tree (fst (appendDistTrace (T, G) w))
[PROOF STEP]
show "finite_tree (fst (appendDistTrace (T,G) w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (appendDistTrace (T, G) w))
[PROOF STEP]
using distribute_extension_finite[of T M G cg_lookup cg_insert \<alpha> "xy#u@w" False "(append_heuristic_input M)", OF \<open>finite_tree T\<close>]
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M)))

goal (1 subgoal):
 1. finite_tree (fst (appendDistTrace (T, G) w))
[PROOF STEP]
using distribute_extension_finite[of T' M G' cg_lookup cg_insert \<beta> "u@w" False "(append_heuristic_input M)"]
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M)))
finite_tree T' \<Longrightarrow> finite_tree (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)))

goal (1 subgoal):
 1. finite_tree (fst (appendDistTrace (T, G) w))
[PROOF STEP]
unfolding appendDistTrace case_prod_conv *** Let_def fst_conv
[PROOF STATE]
proof (prove)
using this:
finite_tree T'
finite_tree T' \<Longrightarrow> finite_tree (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)))

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite_tree (fst (appendDistTrace (T, G) w))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (appendDistTrace (?T, ?G) ?w))

goal (2 subgoals):
 1. is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
 2. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (appendDistTrace (?T, ?G) ?w))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (appendDistTrace (?T, ?G) ?w))

goal (1 subgoal):
 1. finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
unfolding **
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (appendDistTrace (?T, ?G) ?w))

goal (1 subgoal):
 1. finite_tree (fst (foldl appendDistTrace (T, G) ws))
[PROOF STEP]
using \<open>finite_tree T\<close>
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (appendDistTrace (?T, ?G) ?w))
finite_tree T

goal (1 subgoal):
 1. finite_tree (fst (foldl appendDistTrace (T, G) ws))
[PROOF STEP]
apply (induction ws rule: rev_induct; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>finite_tree (fst (foldl appendDistTrace (T, G) xs)); \<And>T G w. finite_tree T \<Longrightarrow> finite_tree (fst (appendDistTrace (T, G) w)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (appendDistTrace (foldl appendDistTrace (T, G) xs) x))
[PROOF STEP]
by (metis (no_types, opaque_lifting) fst_conv old.prod.exhaust)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (handleTrace (T, G) u))

goal (1 subgoal):
 1. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_in_language M qTarget u

goal (1 subgoal):
 1. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
obtain T' G' where ***: "distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u) False (append_heuristic_input M) = (T',G')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T' G'. distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) = (T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = (x1, x2) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>T' G'. distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) = (T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) = (T', G')

goal (1 subgoal):
 1. \<not> is_in_language M qTarget u \<Longrightarrow> finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
show "finite_tree (fst (handleTrace (T, G) u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
using distribute_extension_finite[of T M G cg_lookup cg_insert \<alpha> "xy#u" False "(append_heuristic_input M)", OF \<open>finite_tree T\<close>]
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M)))

goal (1 subgoal):
 1. finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
using distribute_extension_finite[of T' M G' cg_lookup cg_insert \<beta> "u" False "(append_heuristic_input M)"]
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M)))
finite_tree T' \<Longrightarrow> finite_tree (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)))

goal (1 subgoal):
 1. finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M)))
finite_tree T' \<Longrightarrow> finite_tree (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)))
\<not> is_in_language M qTarget u

goal (1 subgoal):
 1. finite_tree (fst (handleTrace (T, G) u))
[PROOF STEP]
unfolding case_prod_conv *** Let_def fst_conv handleTrace
[PROOF STATE]
proof (prove)
using this:
finite_tree T'
finite_tree T' \<Longrightarrow> finite_tree (fst (distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)))
\<not> is_in_language M qTarget u

goal (1 subgoal):
 1. finite_tree (fst (if is_in_language M qTarget u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M qTarget u))) else distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite_tree (fst (handleTrace (T, G) u))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree (fst (handleTrace (T, G) u))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (handleTrace (?T, ?G) ?u))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> finite_tree (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (handleTrace (?T, ?G) ?u))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (handleTrace (?T, ?G) ?u))

goal (1 subgoal):
 1. finite_tree (fst (foldl handleTrace (T, G) (ttc @ [io])))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (handleTrace (?T, ?G) ?u))

goal (1 subgoal):
 1. finite_tree (fst (handleTrace (foldl handleTrace (T, G) ttc) io))
[PROOF STEP]
by (metis (no_types, opaque_lifting) snoc.IH fst_conv old.prod.exhaust)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (foldl handleTrace (T, G) (ttc @ [io])))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))

goal:
No subgoals!
[PROOF STEP]
qed