[STATEMENT]
lemma interleave_filter:
  assumes "xs \<in> filter P ys \<otimes> filter P zs"
  obtains xs' where "xs' \<in> ys \<otimes> zs" and "xs = filter P xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs'. \<lbrakk>xs' \<in> ys \<otimes> zs; xs = filter P xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<in> filter P ys \<otimes> filter P zs

goal (1 subgoal):
 1. (\<And>xs'. \<lbrakk>xs' \<in> ys \<otimes> zs; xs = filter P xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> filter P ys \<otimes> filter P zs \<Longrightarrow> \<exists>xs'. xs' \<in> ys \<otimes> zs \<and> xs = filter P xs'
[PROOF STEP]
proof(induction ys zs arbitrary: xs rule: list_induct2'')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>xs. xs \<in> filter P [] \<otimes> filter P [] \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> [] \<and> xs = filter P xs'
 2. \<And>xs xsa. xsa \<in> filter P xs \<otimes> filter P [] \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> [] \<and> xsa = filter P xs'
 3. \<And>ys xs. xs \<in> filter P [] \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> ys \<and> xs = filter P xs'
 4. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
case NilNil
[PROOF STATE]
proof (state)
this:
xs \<in> filter P [] \<otimes> filter P []

goal (4 subgoals):
 1. \<And>xs. xs \<in> filter P [] \<otimes> filter P [] \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> [] \<and> xs = filter P xs'
 2. \<And>xs xsa. xsa \<in> filter P xs \<otimes> filter P [] \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> [] \<and> xsa = filter P xs'
 3. \<And>ys xs. xs \<in> filter P [] \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> ys \<and> xs = filter P xs'
 4. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
xs \<in> filter P [] \<otimes> filter P []

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> [] \<otimes> [] \<and> xs = filter P xs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> [] \<otimes> [] \<and> xs = filter P xs'

goal (3 subgoals):
 1. \<And>xs xsa. xsa \<in> filter P xs \<otimes> filter P [] \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> [] \<and> xsa = filter P xs'
 2. \<And>ys xs. xs \<in> filter P [] \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> ys \<and> xs = filter P xs'
 3. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xs xsa. xsa \<in> filter P xs \<otimes> filter P [] \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> [] \<and> xsa = filter P xs'
 2. \<And>ys xs. xs \<in> filter P [] \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> ys \<and> xs = filter P xs'
 3. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
case (ConsNil ys xs)
[PROOF STATE]
proof (state)
this:
xs \<in> filter P ys \<otimes> filter P []

goal (3 subgoals):
 1. \<And>xs xsa. xsa \<in> filter P xs \<otimes> filter P [] \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> [] \<and> xsa = filter P xs'
 2. \<And>ys xs. xs \<in> filter P [] \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> ys \<and> xs = filter P xs'
 3. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
xs \<in> filter P ys \<otimes> filter P []

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> ys \<otimes> [] \<and> xs = filter P xs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> ys \<otimes> [] \<and> xs = filter P xs'

goal (2 subgoals):
 1. \<And>ys xs. xs \<in> filter P [] \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> ys \<and> xs = filter P xs'
 2. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys xs. xs \<in> filter P [] \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> ys \<and> xs = filter P xs'
 2. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
case (NilCons zs xs)
[PROOF STATE]
proof (state)
this:
xs \<in> filter P [] \<otimes> filter P zs

goal (2 subgoals):
 1. \<And>ys xs. xs \<in> filter P [] \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> [] \<otimes> ys \<and> xs = filter P xs'
 2. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
xs \<in> filter P [] \<otimes> filter P zs

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> [] \<otimes> zs \<and> xs = filter P xs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> [] \<otimes> zs \<and> xs = filter P xs'

goal (1 subgoal):
 1. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
case (ConsCons y ys z zs xs)
[PROOF STATE]
proof (state)
this:
?xs \<in> filter P ys \<otimes> filter P (z # zs) \<Longrightarrow> \<exists>xs'. xs' \<in> ys \<otimes> z # zs \<and> ?xs = filter P xs'
?xs \<in> filter P (y # ys) \<otimes> filter P zs \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> zs \<and> ?xs = filter P xs'
xs \<in> filter P (y # ys) \<otimes> filter P (z # zs)

goal (1 subgoal):
 1. \<And>x xs y ys xsa. \<lbrakk>\<And>xsa. xsa \<in> filter P xs \<otimes> filter P (y # ys) \<Longrightarrow> \<exists>xs'. xs' \<in> xs \<otimes> y # ys \<and> xsa = filter P xs'; \<And>xsa. xsa \<in> filter P (x # xs) \<otimes> filter P ys \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> ys \<and> xsa = filter P xs'; xsa \<in> filter P (x # xs) \<otimes> filter P (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> x # xs \<otimes> y # ys \<and> xsa = filter P xs'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
proof(cases "P y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> P y

goal (2 subgoals):
 1. P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
with ConsCons.prems(1)
[PROOF STATE]
proof (chain)
picking this:
xs \<in> filter P (y # ys) \<otimes> filter P (z # zs)
\<not> P y
[PROOF STEP]
have "xs \<in> filter P ys \<otimes> filter P (z#zs)"
[PROOF STATE]
proof (prove)
using this:
xs \<in> filter P (y # ys) \<otimes> filter P (z # zs)
\<not> P y

goal (1 subgoal):
 1. xs \<in> filter P ys \<otimes> filter P (z # zs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs \<in> filter P ys \<otimes> filter P (z # zs)

goal (2 subgoals):
 1. P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
from ConsCons.IH(1)[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs'. xs' \<in> ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
obtain xs' where "xs' \<in> ys \<otimes> (z # zs)" "xs = filter P xs'"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs'. xs' \<in> ys \<otimes> z # zs \<and> xs = filter P xs'

goal (1 subgoal):
 1. (\<And>xs'. \<lbrakk>xs' \<in> ys \<otimes> z # zs; xs = filter P xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs' \<in> ys \<otimes> z # zs
xs = filter P xs'

goal (2 subgoals):
 1. P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
hence "y#xs' \<in> y#ys \<otimes> z#zs" and "xs = filter P (y#xs')"
[PROOF STATE]
proof (prove)
using this:
xs' \<in> ys \<otimes> z # zs
xs = filter P xs'

goal (1 subgoal):
 1. y # xs' \<in> y # ys \<otimes> z # zs &&& xs = filter P (y # xs')
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
xs' \<in> ys \<otimes> z # zs
xs = filter P xs'
\<not> P y

goal (1 subgoal):
 1. y # xs' \<in> y # ys \<otimes> z # zs &&& xs = filter P (y # xs')
[PROOF STEP]
by (auto intro: interleave_intros)
[PROOF STATE]
proof (state)
this:
y # xs' \<in> y # ys \<otimes> z # zs
xs = filter P (y # xs')

goal (2 subgoals):
 1. P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y # xs' \<in> y # ys \<otimes> z # zs
xs = filter P (y # xs')

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'

goal (1 subgoal):
 1. P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
P y

goal (1 subgoal):
 1. P y \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
proof(cases "P z")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> P z

goal (2 subgoals):
 1. P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
with ConsCons.prems(1)
[PROOF STATE]
proof (chain)
picking this:
xs \<in> filter P (y # ys) \<otimes> filter P (z # zs)
\<not> P z
[PROOF STEP]
have "xs \<in> filter P (y#ys) \<otimes> filter P zs"
[PROOF STATE]
proof (prove)
using this:
xs \<in> filter P (y # ys) \<otimes> filter P (z # zs)
\<not> P z

goal (1 subgoal):
 1. xs \<in> filter P (y # ys) \<otimes> filter P zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs \<in> filter P (y # ys) \<otimes> filter P zs

goal (2 subgoals):
 1. P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
from ConsCons.IH(2)[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs'. xs' \<in> y # ys \<otimes> zs \<and> xs = filter P xs'
[PROOF STEP]
obtain xs' where "xs' \<in> y#ys \<otimes> zs" "xs = filter P xs'"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs'. xs' \<in> y # ys \<otimes> zs \<and> xs = filter P xs'

goal (1 subgoal):
 1. (\<And>xs'. \<lbrakk>xs' \<in> y # ys \<otimes> zs; xs = filter P xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs' \<in> y # ys \<otimes> zs
xs = filter P xs'

goal (2 subgoals):
 1. P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
hence "z#xs' \<in> y#ys \<otimes> z#zs" and "xs = filter P (z#xs')"
[PROOF STATE]
proof (prove)
using this:
xs' \<in> y # ys \<otimes> zs
xs = filter P xs'

goal (1 subgoal):
 1. z # xs' \<in> y # ys \<otimes> z # zs &&& xs = filter P (z # xs')
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
xs' \<in> y # ys \<otimes> zs
xs = filter P xs'
\<not> P z

goal (1 subgoal):
 1. z # xs' \<in> y # ys \<otimes> z # zs &&& xs = filter P (z # xs')
[PROOF STEP]
by (auto intro: interleave_intros)
[PROOF STATE]
proof (state)
this:
z # xs' \<in> y # ys \<otimes> z # zs
xs = filter P (z # xs')

goal (2 subgoals):
 1. P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<not> P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z # xs' \<in> y # ys \<otimes> z # zs
xs = filter P (z # xs')

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'

goal (1 subgoal):
 1. P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
P z

goal (1 subgoal):
 1. P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
from ConsCons.prems(1) \<open>P y\<close> \<open>P z\<close>
[PROOF STATE]
proof (chain)
picking this:
xs \<in> filter P (y # ys) \<otimes> filter P (z # zs)
P y
P z
[PROOF STEP]
have "xs \<in> y # filter P ys  \<otimes> z # filter P zs"
[PROOF STATE]
proof (prove)
using this:
xs \<in> filter P (y # ys) \<otimes> filter P (z # zs)
P y
P z

goal (1 subgoal):
 1. xs \<in> y # filter P ys \<otimes> z # filter P zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs \<in> y # filter P ys \<otimes> z # filter P zs

goal (1 subgoal):
 1. P z \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xs \<in> y # filter P ys \<otimes> z # filter P zs

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
proof(rule interleave_ConsConsE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>zs. \<lbrakk>xs = y # zs; zs \<in> filter P ys \<otimes> z # filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
fix xs'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>zs. \<lbrakk>xs = y # zs; zs \<in> filter P ys \<otimes> z # filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
assume "xs = y # xs'" and "xs' \<in> interleave (filter P ys) (z # filter P zs)"
[PROOF STATE]
proof (state)
this:
xs = y # xs'
xs' \<in> filter P ys \<otimes> z # filter P zs

goal (2 subgoals):
 1. \<And>zs. \<lbrakk>xs = y # zs; zs \<in> filter P ys \<otimes> z # filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
hence "xs' \<in> filter P ys  \<otimes> filter P (z#zs)"
[PROOF STATE]
proof (prove)
using this:
xs = y # xs'
xs' \<in> filter P ys \<otimes> z # filter P zs

goal (1 subgoal):
 1. xs' \<in> filter P ys \<otimes> filter P (z # zs)
[PROOF STEP]
using \<open>P z\<close>
[PROOF STATE]
proof (prove)
using this:
xs = y # xs'
xs' \<in> filter P ys \<otimes> z # filter P zs
P z

goal (1 subgoal):
 1. xs' \<in> filter P ys \<otimes> filter P (z # zs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs' \<in> filter P ys \<otimes> filter P (z # zs)

goal (2 subgoals):
 1. \<And>zs. \<lbrakk>xs = y # zs; zs \<in> filter P ys \<otimes> z # filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
from ConsCons.IH(1)[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs'a. xs'a \<in> ys \<otimes> z # zs \<and> xs' = filter P xs'a
[PROOF STEP]
obtain xs'' where "xs'' \<in> ys \<otimes> (z # zs)" and "xs' = filter P xs''"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs'a. xs'a \<in> ys \<otimes> z # zs \<and> xs' = filter P xs'a

goal (1 subgoal):
 1. (\<And>xs''. \<lbrakk>xs'' \<in> ys \<otimes> z # zs; xs' = filter P xs''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs'' \<in> ys \<otimes> z # zs
xs' = filter P xs''

goal (2 subgoals):
 1. \<And>zs. \<lbrakk>xs = y # zs; zs \<in> filter P ys \<otimes> z # filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
hence "y#xs'' \<in> y#ys  \<otimes> z#zs" and "y#xs' = filter P (y#xs'')"
[PROOF STATE]
proof (prove)
using this:
xs'' \<in> ys \<otimes> z # zs
xs' = filter P xs''

goal (1 subgoal):
 1. y # xs'' \<in> y # ys \<otimes> z # zs &&& y # xs' = filter P (y # xs'')
[PROOF STEP]
using \<open>P y\<close>
[PROOF STATE]
proof (prove)
using this:
xs'' \<in> ys \<otimes> z # zs
xs' = filter P xs''
P y

goal (1 subgoal):
 1. y # xs'' \<in> y # ys \<otimes> z # zs &&& y # xs' = filter P (y # xs'')
[PROOF STEP]
by (auto intro: interleave_intros)
[PROOF STATE]
proof (state)
this:
y # xs'' \<in> y # ys \<otimes> z # zs
y # xs' = filter P (y # xs'')

goal (2 subgoals):
 1. \<And>zs. \<lbrakk>xs = y # zs; zs \<in> filter P ys \<otimes> z # filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
 2. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y # xs'' \<in> y # ys \<otimes> z # zs
y # xs' = filter P (y # xs'')

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
using \<open>xs = _\<close>
[PROOF STATE]
proof (prove)
using this:
y # xs'' \<in> y # ys \<otimes> z # zs
y # xs' = filter P (y # xs'')
xs = y # xs'

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'

goal (1 subgoal):
 1. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
fix xs'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
assume "xs = z # xs'" and "xs' \<in> y # filter P ys  \<otimes> filter P zs"
[PROOF STATE]
proof (state)
this:
xs = z # xs'
xs' \<in> y # filter P ys \<otimes> filter P zs

goal (1 subgoal):
 1. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
hence "xs' \<in> filter P (y#ys) \<otimes> filter P zs"
[PROOF STATE]
proof (prove)
using this:
xs = z # xs'
xs' \<in> y # filter P ys \<otimes> filter P zs

goal (1 subgoal):
 1. xs' \<in> filter P (y # ys) \<otimes> filter P zs
[PROOF STEP]
using \<open>P y\<close>
[PROOF STATE]
proof (prove)
using this:
xs = z # xs'
xs' \<in> y # filter P ys \<otimes> filter P zs
P y

goal (1 subgoal):
 1. xs' \<in> filter P (y # ys) \<otimes> filter P zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs' \<in> filter P (y # ys) \<otimes> filter P zs

goal (1 subgoal):
 1. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
from ConsCons.IH(2)[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs'a. xs'a \<in> y # ys \<otimes> zs \<and> xs' = filter P xs'a
[PROOF STEP]
obtain xs'' where "xs'' \<in> y#ys \<otimes> zs" and "xs' = filter P xs''"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs'a. xs'a \<in> y # ys \<otimes> zs \<and> xs' = filter P xs'a

goal (1 subgoal):
 1. (\<And>xs''. \<lbrakk>xs'' \<in> y # ys \<otimes> zs; xs' = filter P xs''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs'' \<in> y # ys \<otimes> zs
xs' = filter P xs''

goal (1 subgoal):
 1. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
hence "z#xs'' \<in> y#ys \<otimes> z#zs" and "z#xs' = filter P (z#xs'')"
[PROOF STATE]
proof (prove)
using this:
xs'' \<in> y # ys \<otimes> zs
xs' = filter P xs''

goal (1 subgoal):
 1. z # xs'' \<in> y # ys \<otimes> z # zs &&& z # xs' = filter P (z # xs'')
[PROOF STEP]
using \<open>P z\<close>
[PROOF STATE]
proof (prove)
using this:
xs'' \<in> y # ys \<otimes> zs
xs' = filter P xs''
P z

goal (1 subgoal):
 1. z # xs'' \<in> y # ys \<otimes> z # zs &&& z # xs' = filter P (z # xs'')
[PROOF STEP]
by (auto intro: interleave_intros)
[PROOF STATE]
proof (state)
this:
z # xs'' \<in> y # ys \<otimes> z # zs
z # xs' = filter P (z # xs'')

goal (1 subgoal):
 1. \<And>zs. \<lbrakk>xs = z # zs; zs \<in> y # filter P ys \<otimes> filter P zs\<rbrakk> \<Longrightarrow> \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z # xs'' \<in> y # ys \<otimes> z # zs
z # xs' = filter P (z # xs'')

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
using \<open>xs = _\<close>
[PROOF STATE]
proof (prove)
using this:
z # xs'' \<in> y # ys \<otimes> z # zs
z # xs' = filter P (z # xs'')
xs = z # xs'

goal (1 subgoal):
 1. \<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs'. xs' \<in> y # ys \<otimes> z # zs \<and> xs = filter P xs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma verifies_io_pair_handled:
  assumes "verifies_io_pair f M1 M2 cg_insert cg_lookup"
shows "handles_io_pair f M1 M2 cg_insert cg_lookup"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. handles_io_pair f M1 M2 cg_insert cg_lookup
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. handles_io_pair f M1 M2 cg_insert cg_lookup
[PROOF STEP]
have *:"\<And> V T G q x y . set T \<subseteq> set (fst (f M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V T G q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
verifies_io_pair f M1 M2 cg_insert cg_lookup

goal (1 subgoal):
 1. \<And>V T G q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
unfolding verifies_io_pair_def
[PROOF STATE]
proof (prove)
using this:
\<forall>V T G q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1 \<longrightarrow> q \<in> reachable_states M1 \<longrightarrow> x \<in> FSM.inputs M1 \<longrightarrow> y \<in> FSM.outputs M1 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup G \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y)))

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

goal (1 subgoal):
 1. handles_io_pair f M1 M2 cg_insert cg_lookup
[PROOF STEP]
have ***:"\<And> V T G q x y . finite_tree T \<longrightarrow> finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V T G q x y. finite_tree T \<longrightarrow> finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
verifies_io_pair f M1 M2 cg_insert cg_lookup

goal (1 subgoal):
 1. \<And>V T G q x y. finite_tree T \<longrightarrow> finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
unfolding verifies_io_pair_def
[PROOF STATE]
proof (prove)
using this:
\<forall>V T G q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1 \<longrightarrow> q \<in> reachable_states M1 \<longrightarrow> x \<in> FSM.inputs M1 \<longrightarrow> y \<in> FSM.outputs M1 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup G \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y)))

goal (1 subgoal):
 1. \<And>V T G q x y. finite_tree T \<longrightarrow> finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite_tree ?T \<longrightarrow> finite_tree (fst (f M1 ?V ?T ?G cg_insert cg_lookup ?q ?x ?y))

goal (1 subgoal):
 1. handles_io_pair f M1 M2 cg_insert cg_lookup
[PROOF STEP]
have **:"\<And> V T G q x y.
        observable M1 \<Longrightarrow>
        observable M2 \<Longrightarrow>
        minimal M1 \<Longrightarrow>
        minimal M2 \<Longrightarrow>
        FSM.inputs M2 = FSM.inputs M1 \<Longrightarrow>
        FSM.outputs M2 = FSM.outputs M1 \<Longrightarrow>
        is_state_cover_assignment M1 V \<Longrightarrow>
        L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1 \<Longrightarrow>
        q \<in> reachable_states M1 \<Longrightarrow>
        x \<in> inputs M1 \<Longrightarrow>
        y \<in> outputs M1 \<Longrightarrow>
        convergence_graph_lookup_invar M1 M2 cg_lookup G \<Longrightarrow>
        convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<Longrightarrow>
        L M1 \<inter> set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<Longrightarrow>
        ( L M1 \<inter> {(V q)@[(x,y)]} = L M2 \<inter> {(V q)@[(x,y)]} )
        \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
fix V T G q x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a01: "observable M1"
[PROOF STATE]
proof (state)
this:
observable M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
observable M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a02: "observable M2"
[PROOF STATE]
proof (state)
this:
observable M2

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
observable M2

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a03: "minimal M1"
[PROOF STATE]
proof (state)
this:
minimal M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
minimal M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a04: "minimal M2"
[PROOF STATE]
proof (state)
this:
minimal M2

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
minimal M2

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a05: "FSM.inputs M2 = FSM.inputs M1"
[PROOF STATE]
proof (state)
this:
FSM.inputs M2 = FSM.inputs M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
FSM.inputs M2 = FSM.inputs M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a06: "FSM.outputs M2 = FSM.outputs M1"
[PROOF STATE]
proof (state)
this:
FSM.outputs M2 = FSM.outputs M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
FSM.outputs M2 = FSM.outputs M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a07: "is_state_cover_assignment M1 V"
[PROOF STATE]
proof (state)
this:
is_state_cover_assignment M1 V

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_state_cover_assignment M1 V

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a09: "L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1"
[PROOF STATE]
proof (state)
this:
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a10: "q \<in> reachable_states M1"
[PROOF STATE]
proof (state)
this:
q \<in> reachable_states M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
q \<in> reachable_states M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a11: "x \<in> inputs M1"
[PROOF STATE]
proof (state)
this:
x \<in> FSM.inputs M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> FSM.inputs M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a12: "y \<in> outputs M1"
[PROOF STATE]
proof (state)
this:
y \<in> FSM.outputs M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> FSM.outputs M1

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a13: "convergence_graph_lookup_invar M1 M2 cg_lookup G"
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup G

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup G

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a14: "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
[PROOF STATE]
proof (state)
this:
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a15: "L M1 \<inter> set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> set (fst (f M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
observable M1
observable M2
minimal M1
minimal M2
FSM.inputs M2 = FSM.inputs M1
FSM.outputs M2 = FSM.outputs M1
is_state_cover_assignment M1 V
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1
q \<in> reachable_states M1
x \<in> FSM.inputs M1
y \<in> FSM.outputs M1
convergence_graph_lookup_invar M1 M2 cg_lookup G
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert
L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
have *:"(\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and>
                          converge M2 \<alpha> (V q) \<and>
                          \<alpha> \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)))"
               and **: "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
using this:
observable M1
observable M2
minimal M1
minimal M2
FSM.inputs M2 = FSM.inputs M1
FSM.outputs M2 = FSM.outputs M1
is_state_cover_assignment M1 V
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1
q \<in> reachable_states M1
x \<in> FSM.inputs M1
y \<in> FSM.outputs M1
convergence_graph_lookup_invar M1 M2 cg_lookup G
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert
L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))

goal (1 subgoal):
 1. \<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) &&& convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
observable M1
observable M2
minimal M1
minimal M2
FSM.inputs M2 = FSM.inputs M1
FSM.outputs M2 = FSM.outputs M1
is_state_cover_assignment M1 V
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1
q \<in> reachable_states M1
x \<in> FSM.inputs M1
y \<in> FSM.outputs M1
convergence_graph_lookup_invar M1 M2 cg_lookup G
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert
L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))
verifies_io_pair f M1 M2 cg_insert cg_lookup

goal (1 subgoal):
 1. \<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) &&& convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
unfolding verifies_io_pair_def
[PROOF STATE]
proof (prove)
using this:
observable M1
observable M2
minimal M1
minimal M2
FSM.inputs M2 = FSM.inputs M1
FSM.outputs M2 = FSM.outputs M1
is_state_cover_assignment M1 V
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1
q \<in> reachable_states M1
x \<in> FSM.inputs M1
y \<in> FSM.outputs M1
convergence_graph_lookup_invar M1 M2 cg_lookup G
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert
L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))
\<forall>V T G q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1 \<longrightarrow> q \<in> reachable_states M1 \<longrightarrow> x \<in> FSM.inputs M1 \<longrightarrow> y \<in> FSM.outputs M1 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup G \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y)))

goal (1 subgoal):
 1. \<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) &&& convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
by presburger+
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
have "( L M1 \<inter> {(V q)@[(x,y)]} = L M2 \<inter> {(V q)@[(x,y)]} )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
obtain \<alpha> where "converge M1 \<alpha> (V q)" and "converge M2 \<alpha> (V q)" and "\<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>converge M1 \<alpha> (V q); converge M2 \<alpha> (V q); \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))

goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>converge M1 \<alpha> (V q); converge M2 \<alpha> (V q); \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
converge M1 \<alpha> (V q)
converge M2 \<alpha> (V q)
\<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))

goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
have "(V q)@[(x,y)] \<in> L M1 = (\<alpha>@[(x,y)] \<in> L M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V q @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M1)
[PROOF STEP]
using \<open>converge M1 \<alpha> (V q)\<close>
[PROOF STATE]
proof (prove)
using this:
converge M1 \<alpha> (V q)

goal (1 subgoal):
 1. (V q @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M1)
[PROOF STEP]
using a01 a07
[PROOF STATE]
proof (prove)
using this:
converge M1 \<alpha> (V q)
observable M1
is_state_cover_assignment M1 V

goal (1 subgoal):
 1. (V q @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M1)
[PROOF STEP]
by (meson converge_append_language_iff)
[PROOF STATE]
proof (state)
this:
(V q @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M1)

goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(V q @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M1)

goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
have "(V q)@[(x,y)] \<in> L M2 = (\<alpha>@[(x,y)] \<in> L M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V q @ [(x, y)] \<in> L M2) = (\<alpha> @ [(x, y)] \<in> L M2)
[PROOF STEP]
using \<open>converge M2 \<alpha> (V q)\<close>
[PROOF STATE]
proof (prove)
using this:
converge M2 \<alpha> (V q)

goal (1 subgoal):
 1. (V q @ [(x, y)] \<in> L M2) = (\<alpha> @ [(x, y)] \<in> L M2)
[PROOF STEP]
using a02 a07
[PROOF STATE]
proof (prove)
using this:
converge M2 \<alpha> (V q)
observable M2
is_state_cover_assignment M1 V

goal (1 subgoal):
 1. (V q @ [(x, y)] \<in> L M2) = (\<alpha> @ [(x, y)] \<in> L M2)
[PROOF STEP]
by (meson converge_append_language_iff)
[PROOF STATE]
proof (state)
this:
(V q @ [(x, y)] \<in> L M2) = (\<alpha> @ [(x, y)] \<in> L M2)

goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(V q @ [(x, y)] \<in> L M2) = (\<alpha> @ [(x, y)] \<in> L M2)

goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
have "\<alpha> @ [(x, y)] \<in> L M1 = (\<alpha> @ [(x, y)] \<in> L M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<alpha> @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M2)
[PROOF STEP]
using \<open>\<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<close> a15
[PROOF STATE]
proof (prove)
using this:
\<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))
L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))

goal (1 subgoal):
 1. (\<alpha> @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<alpha> @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M2)

goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(V q @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M1)
(V q @ [(x, y)] \<in> L M2) = (\<alpha> @ [(x, y)] \<in> L M2)
(\<alpha> @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(V q @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M1)
(V q @ [(x, y)] \<in> L M2) = (\<alpha> @ [(x, y)] \<in> L M2)
(\<alpha> @ [(x, y)] \<in> L M1) = (\<alpha> @ [(x, y)] \<in> L M2)

goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}

goal (1 subgoal):
 1. \<And>V T G q x y. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 V; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
[PROOF STEP]
show "( L M1 \<inter> {(V q)@[(x,y)]} = L M2 \<inter> {(V q)@[(x,y)]} ) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}

goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]}
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))

goal (1 subgoal):
 1. L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 ?V; L M1 \<inter> ?V ` reachable_states M1 = L M2 \<inter> ?V ` reachable_states M1; ?q \<in> reachable_states M1; ?x \<in> FSM.inputs M1; ?y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup ?G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 ?V ?T ?G cg_insert cg_lookup ?q ?x ?y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 ?V ?T ?G cg_insert cg_lookup ?q ?x ?y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {?V ?q @ [(?x, ?y)]} = L M2 \<inter> {?V ?q @ [(?x, ?y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 ?V ?T ?G cg_insert cg_lookup ?q ?x ?y))

goal (1 subgoal):
 1. handles_io_pair f M1 M2 cg_insert cg_lookup
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. handles_io_pair f M1 M2 cg_insert cg_lookup
[PROOF STEP]
unfolding handles_io_pair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>V T G q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1 \<longrightarrow> q \<in> reachable_states M1 \<longrightarrow> x \<in> FSM.inputs M1 \<longrightarrow> y \<in> FSM.outputs M1 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup G \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y)))
[PROOF STEP]
using * *** **
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (f M1 ?V ?T ?G cg_insert cg_lookup ?q ?x ?y))
finite_tree ?T \<longrightarrow> finite_tree (fst (f M1 ?V ?T ?G cg_insert cg_lookup ?q ?x ?y))
\<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1; is_state_cover_assignment M1 ?V; L M1 \<inter> ?V ` reachable_states M1 = L M2 \<inter> ?V ` reachable_states M1; ?q \<in> reachable_states M1; ?x \<in> FSM.inputs M1; ?y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup ?G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (f M1 ?V ?T ?G cg_insert cg_lookup ?q ?x ?y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 ?V ?T ?G cg_insert cg_lookup ?q ?x ?y))\<rbrakk> \<Longrightarrow> L M1 \<inter> {?V ?q @ [(?x, ?y)]} = L M2 \<inter> {?V ?q @ [(?x, ?y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 ?V ?T ?G cg_insert cg_lookup ?q ?x ?y))

goal (1 subgoal):
 1. \<forall>V T G q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y))) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1 \<longrightarrow> q \<in> reachable_states M1 \<longrightarrow> x \<in> FSM.inputs M1 \<longrightarrow> y \<in> FSM.outputs M1 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup G \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (f M1 V T G cg_insert cg_lookup q x y)) \<longrightarrow> L M1 \<inter> {V q @ [(x, y)]} = L M2 \<inter> {V q @ [(x, y)]} \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
handles_io_pair f M1 M2 cg_insert cg_lookup

goal:
No subgoals!
[PROOF STEP]
qed