[STATEMENT]
lemma invar_last:
assumes "invar C" and "\<not>card C < k"
shows "card C = k" and "card C' > 0 \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card C = k &&& 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card C = k
 2. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
show "card C = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card C = k
[PROOF STEP]
using assms(1, 2)
[PROOF STATE]
proof (prove)
using this:
invar C
\<not> card C < k

goal (1 subgoal):
 1. card C = k
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
C \<noteq> {} \<and> card C \<le> k \<and> C \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C'))
\<not> card C < k

goal (1 subgoal):
 1. card C = k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card C = k

goal (1 subgoal):
 1. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
have C_props: "finite C \<and> C \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite C \<and> C \<noteq> {}
[PROOF STEP]
using finite_sites assms(1)
[PROOF STATE]
proof (prove)
using this:
finite S
invar C

goal (1 subgoal):
 1. finite C \<and> C \<noteq> {}
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
finite S
C \<noteq> {} \<and> card C \<le> k \<and> C \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C'))

goal (1 subgoal):
 1. finite C \<and> C \<noteq> {}
[PROOF STEP]
by (meson finite_subset)
[PROOF STATE]
proof (state)
this:
finite C \<and> C \<noteq> {}

goal (1 subgoal):
 1. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
show "card C' > 0 \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
proof (rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < card C' \<and> card C' \<le> k \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
assume C'_assms: "0 < card (C' :: 'a set) \<and> card C' \<le> k"
[PROOF STATE]
proof (state)
this:
0 < card C' \<and> card C' \<le> k

goal (1 subgoal):
 1. 0 < card C' \<and> card C' \<le> k \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
let ?r = "radius C'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < card C' \<and> card C' \<le> k \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
have "(\<forall>c\<^sub>1 \<in> C. \<forall>c\<^sub>2 \<in> C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s \<in> S. distance C s \<le> 2 * ?r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
invar C

goal (1 subgoal):
 1. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
C \<noteq> {} \<and> card C \<le> k \<and> C \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C'))

goal (1 subgoal):
 1. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')

goal (1 subgoal):
 1. 0 < card C' \<and> card C' \<le> k \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')
[PROOF STEP]
show "radius C \<le> 2 * ?r"
[PROOF STATE]
proof (prove)
using this:
(\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')

goal (1 subgoal):
 1. radius C \<le> 2 * radius C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2 \<Longrightarrow> radius C \<le> 2 * radius C'
 2. \<forall>s\<in>S. distance C s \<le> 2 * radius C' \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
assume case_assm: "\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2"
[PROOF STATE]
proof (state)
this:
\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2

goal (2 subgoals):
 1. \<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2 \<Longrightarrow> radius C \<le> 2 * radius C'
 2. \<forall>s\<in>S. distance C s \<le> 2 * radius C' \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
obtain s where s_def: "radius C = distance C s \<and> s \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. radius C = distance C s \<and> s \<in> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using radius_def2
[PROOF STATE]
proof (prove)
using this:
\<exists>s\<in>S. distance ?C s = radius ?C

goal (1 subgoal):
 1. (\<And>s. radius C = distance C s \<and> s \<in> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
radius C = distance C s \<and> s \<in> S

goal (2 subgoals):
 1. \<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2 \<Longrightarrow> radius C \<le> 2 * radius C'
 2. \<forall>s\<in>S. distance C s \<le> 2 * radius C' \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. radius C \<le> 2 * radius C'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
assume contr_assm: "\<not> radius C \<le> 2 * ?r"
[PROOF STATE]
proof (state)
this:
\<not> radius C \<le> 2 * radius C'

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> radius C \<le> 2 * radius C'
[PROOF STEP]
have s_prop: "distance C s > 2 * ?r"
[PROOF STATE]
proof (prove)
using this:
\<not> radius C \<le> 2 * radius C'

goal (1 subgoal):
 1. 2 * radius C' < distance C s
[PROOF STEP]
using s_def
[PROOF STATE]
proof (prove)
using this:
\<not> radius C \<le> 2 * radius C'
radius C = distance C s \<and> s \<in> S

goal (1 subgoal):
 1. 2 * radius C' < distance C s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * radius C' < distance C s

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 * radius C' < distance C s
[PROOF STEP]
have \<open>\<forall>c\<^sub>1 \<in> C \<union> {s}. \<forall>c\<^sub>2 \<in> C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> dist c\<^sub>1 c\<^sub>2 > 2 * ?r\<close>
[PROOF STATE]
proof (prove)
using this:
2 * radius C' < distance C s

goal (1 subgoal):
 1. \<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
using C_props dist_ins[of "C" "2*?r" "s"] case_assm
[PROOF STATE]
proof (prove)
using this:
2 * radius C' < distance C s
finite C \<and> C \<noteq> {}
\<lbrakk>\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2; 2 * radius C' < distance C s; finite C; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. \<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
have "s \<notin> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<notin> C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
assume "s \<in> C"
[PROOF STATE]
proof (state)
this:
s \<in> C

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> C
[PROOF STEP]
have "distance C s \<le> dist s s"
[PROOF STATE]
proof (prove)
using this:
s \<in> C

goal (1 subgoal):
 1. distance C s \<le> dist s s
[PROOF STEP]
using Min.coboundedI[of "distance C ` S" "dist s s"]
[PROOF STATE]
proof (prove)
using this:
s \<in> C
\<lbrakk>finite (distance C ` S); dist s s \<in> distance C ` S\<rbrakk> \<Longrightarrow> Min (distance C ` S) \<le> dist s s

goal (1 subgoal):
 1. distance C s \<le> dist s s
[PROOF STEP]
by (simp add: distance_def C_props)
[PROOF STATE]
proof (state)
this:
distance C s \<le> dist s s

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
distance C s \<le> dist s s

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
have " ... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist s s = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist s s = 0

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
distance C s \<le> 0
[PROOF STEP]
have "distance C s = 0"
[PROOF STATE]
proof (prove)
using this:
distance C s \<le> 0

goal (1 subgoal):
 1. distance C s = 0
[PROOF STEP]
using dist_lemmas(4)
[PROOF STATE]
proof (prove)
using this:
distance C s \<le> 0
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> 0 \<le> distance ?C ?s

goal (1 subgoal):
 1. distance C s = 0
[PROOF STEP]
by (smt C_props)
[PROOF STATE]
proof (state)
this:
distance C s = 0

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distance C s = 0
[PROOF STEP]
have radius_le_zero: "2 * ?r < 0"
[PROOF STATE]
proof (prove)
using this:
distance C s = 0

goal (1 subgoal):
 1. 2 * radius C' < 0
[PROOF STEP]
using contr_assm s_def
[PROOF STATE]
proof (prove)
using this:
distance C s = 0
\<not> radius C \<le> 2 * radius C'
radius C = distance C s \<and> s \<in> S

goal (1 subgoal):
 1. 2 * radius C' < 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * radius C' < 0

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
obtain x where x_def: "?r = distance C' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. radius C' = distance C' x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using radius_def2
[PROOF STATE]
proof (prove)
using this:
\<exists>s\<in>S. distance ?C s = radius ?C

goal (1 subgoal):
 1. (\<And>x. radius C' = distance C' x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
radius C' = distance C' x

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
obtain l where l_def: "distance C' x = dist x l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. distance C' x = dist x l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dist_lemmas(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>c\<in>?C. dist ?s c = distance ?C ?s

goal (1 subgoal):
 1. (\<And>l. distance C' x = dist x l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis C'_assms card_gt_0_iff)
[PROOF STATE]
proof (state)
this:
distance C' x = dist x l

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distance C' x = dist x l
[PROOF STEP]
have "dist x l = ?r"
[PROOF STATE]
proof (prove)
using this:
distance C' x = dist x l

goal (1 subgoal):
 1. dist x l = radius C'
[PROOF STEP]
by (simp add: x_def)
[PROOF STATE]
proof (state)
this:
dist x l = radius C'

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x l = radius C'

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
have "...  < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. radius C' < 0
[PROOF STEP]
using C'_assms radius_le_zero
[PROOF STATE]
proof (prove)
using this:
0 < card C' \<and> card C' \<le> k
2 * radius C' < 0

goal (1 subgoal):
 1. radius C' < 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
radius C' < 0

goal (1 subgoal):
 1. s \<in> C \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x l < 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
dist x l < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s \<notin> C

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<notin> C
[PROOF STEP]
have "card (C \<union> {s}) > k"
[PROOF STATE]
proof (prove)
using this:
s \<notin> C

goal (1 subgoal):
 1. k < card (C \<union> {s})
[PROOF STEP]
using assms(1,2) C_props
[PROOF STATE]
proof (prove)
using this:
s \<notin> C
invar C
\<not> card C < k
finite C \<and> C \<noteq> {}

goal (1 subgoal):
 1. k < card (C \<union> {s})
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
s \<notin> C
C \<noteq> {} \<and> card C \<le> k \<and> C \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C'))
\<not> card C < k
finite C \<and> C \<noteq> {}

goal (1 subgoal):
 1. k < card (C \<union> {s})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k < card (C \<union> {s})

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
k < card (C \<union> {s})

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < card (C \<union> {s})

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
have "C \<union> {s} \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<union> {s} \<subseteq> S
[PROOF STEP]
using assms(1) s_def
[PROOF STATE]
proof (prove)
using this:
invar C
radius C = distance C s \<and> s \<in> S

goal (1 subgoal):
 1. C \<union> {s} \<subseteq> S
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
C \<noteq> {} \<and> card C \<le> k \<and> C \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C'))
radius C = distance C s \<and> s \<in> S

goal (1 subgoal):
 1. C \<union> {s} \<subseteq> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C \<union> {s} \<subseteq> S

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C \<union> {s} \<subseteq> S

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
have "finite (C \<union> {s})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (C \<union> {s})
[PROOF STEP]
using calculation(3) finite_subset finite_sites
[PROOF STATE]
proof (prove)
using this:
C \<union> {s} \<subseteq> S
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
finite S

goal (1 subgoal):
 1. finite (C \<union> {s})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (C \<union> {s})

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
k < card (C \<union> {s})
C \<union> {s} \<subseteq> S
finite (C \<union> {s})
[PROOF STEP]
have "\<forall>C. card C \<le> k \<and> card C > 0 \<longrightarrow> radius C > ?r"
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
k < card (C \<union> {s})
C \<union> {s} \<subseteq> S
finite (C \<union> {s})

goal (1 subgoal):
 1. \<forall>C. card C \<le> k \<and> 0 < card C \<longrightarrow> radius C' < radius C
[PROOF STEP]
using inv_last_2
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
k < card (C \<union> {s})
C \<union> {s} \<subseteq> S
finite (C \<union> {s})
\<lbrakk>finite ?C; ?n < card ?C; ?C \<subseteq> S; \<forall>c\<^sub>1\<in>?C. \<forall>c\<^sub>2\<in>?C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2\<rbrakk> \<Longrightarrow> \<forall>C'. card C' \<le> ?n \<and> 0 < card C' \<longrightarrow> ?r < radius C'

goal (1 subgoal):
 1. \<forall>C. card C \<le> k \<and> 0 < card C \<longrightarrow> radius C' < radius C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>C. card C \<le> k \<and> 0 < card C \<longrightarrow> radius C' < radius C

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>C. card C \<le> k \<and> 0 < card C \<longrightarrow> radius C' < radius C
[PROOF STEP]
have "?r > ?r"
[PROOF STATE]
proof (prove)
using this:
\<forall>C. card C \<le> k \<and> 0 < card C \<longrightarrow> radius C' < radius C

goal (1 subgoal):
 1. radius C' < radius C'
[PROOF STEP]
using C'_assms
[PROOF STATE]
proof (prove)
using this:
\<forall>C. card C \<le> k \<and> 0 < card C \<longrightarrow> radius C' < radius C
0 < card C' \<and> card C' \<le> k

goal (1 subgoal):
 1. radius C' < radius C'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
radius C' < radius C'

goal (1 subgoal):
 1. \<not> radius C \<le> 2 * radius C' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
radius C' < radius C'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
radius C' < radius C'

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
radius C \<le> 2 * radius C'

goal (1 subgoal):
 1. \<forall>s\<in>S. distance C s \<le> 2 * radius C' \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s\<in>S. distance C s \<le> 2 * radius C' \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
assume "\<forall>s\<in>S. distance C s \<le> 2 * radius C'"
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>S. distance C s \<le> 2 * radius C'

goal (1 subgoal):
 1. \<forall>s\<in>S. distance C s \<le> 2 * radius C' \<Longrightarrow> radius C \<le> 2 * radius C'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>s\<in>S. distance C s \<le> 2 * radius C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>S. distance C s \<le> 2 * radius C'

goal (1 subgoal):
 1. radius C \<le> 2 * radius C'
[PROOF STEP]
by (metis image_iff radius_contained)
[PROOF STATE]
proof (state)
this:
radius C \<le> 2 * radius C'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
radius C \<le> 2 * radius C'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Center_Selection:
"VARS (C :: ('a :: metric_space) set) (s :: ('a :: metric_space))
  {k \<le> card S}
  C := {some S};
  WHILE card C < k INV {invar C} DO
    C := C \<union> {furthest_from C}
  OD
  {card C = k \<and> (\<forall>C'. card C' > 0 \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {k \<le> card S}
C := {SOME s. s \<in> S}; WHILE card C < k INV {invar C}  VAR {0}
DO C := C \<union> {furthest_from C} OD
{card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')}
[PROOF STEP]
proof (vcg, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C s. k \<le> card S \<Longrightarrow> invar {SOME s. s \<in> S}
 2. \<And>C s. invar C \<and> card C < k \<Longrightarrow> invar (C \<union> {furthest_from C})
 3. \<And>C s. invar C \<and> \<not> card C < k \<Longrightarrow> card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
case (1 C s)
[PROOF STATE]
proof (state)
this:
k \<le> card S

goal (3 subgoals):
 1. \<And>C s. k \<le> card S \<Longrightarrow> invar {SOME s. s \<in> S}
 2. \<And>C s. invar C \<and> card C < k \<Longrightarrow> invar (C \<union> {furthest_from C})
 3. \<And>C s. invar C \<and> \<not> card C < k \<Longrightarrow> card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
using invar_init
[PROOF STATE]
proof (prove)
using this:
invar {SOME s. s \<in> S}

goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invar {SOME s. s \<in> S}

goal (2 subgoals):
 1. \<And>C s. invar C \<and> card C < k \<Longrightarrow> invar (C \<union> {furthest_from C})
 2. \<And>C s. invar C \<and> \<not> card C < k \<Longrightarrow> card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C s. invar C \<and> card C < k \<Longrightarrow> invar (C \<union> {furthest_from C})
 2. \<And>C s. invar C \<and> \<not> card C < k \<Longrightarrow> card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
case (2 C s)
[PROOF STATE]
proof (state)
this:
invar C \<and> card C < k

goal (2 subgoals):
 1. \<And>C s. invar C \<and> card C < k \<Longrightarrow> invar (C \<union> {furthest_from C})
 2. \<And>C s. invar C \<and> \<not> card C < k \<Longrightarrow> card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar C \<and> card C < k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar C \<and> card C < k

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
using invar_step
[PROOF STATE]
proof (prove)
using this:
invar C \<and> card C < k
\<lbrakk>invar ?C; card ?C < k\<rbrakk> \<Longrightarrow> invar (?C \<union> {furthest_from ?C})

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invar (C \<union> {furthest_from C})

goal (1 subgoal):
 1. \<And>C s. invar C \<and> \<not> card C < k \<Longrightarrow> card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C s. invar C \<and> \<not> card C < k \<Longrightarrow> card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
case (3 C s)
[PROOF STATE]
proof (state)
this:
invar C \<and> \<not> card C < k

goal (1 subgoal):
 1. \<And>C s. invar C \<and> \<not> card C < k \<Longrightarrow> card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar C \<and> \<not> card C < k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar C \<and> \<not> card C < k

goal (1 subgoal):
 1. card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
using invar_last
[PROOF STATE]
proof (prove)
using this:
invar C \<and> \<not> card C < k
\<lbrakk>invar ?C; \<not> card ?C < k\<rbrakk> \<Longrightarrow> card ?C = k
\<lbrakk>invar ?C; \<not> card ?C < k\<rbrakk> \<Longrightarrow> 0 < card ?C' \<and> card ?C' \<le> k \<longrightarrow> radius ?C \<le> 2 * radius ?C'

goal (1 subgoal):
 1. card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card C = k \<and> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> radius C \<le> 2 * radius C')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_equiv_refl: "\<sigma> \<approx> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<approx> \<sigma>
[PROOF STEP]
unfolding stutter_equiv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<natural>\<sigma> = \<natural>\<sigma>
[PROOF STEP]
..


[STATEMENT]
lemma stutter_equiv_sym [sym]: "\<sigma> \<approx> \<tau> \<Longrightarrow> \<tau> \<approx> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<approx> \<tau> \<Longrightarrow> \<tau> \<approx> \<sigma>
[PROOF STEP]
unfolding stutter_equiv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<natural>\<sigma> = \<natural>\<tau> \<Longrightarrow> \<natural>\<tau> = \<natural>\<sigma>
[PROOF STEP]
by (rule sym)


[STATEMENT]
lemma stutter_equiv_trans [trans]: "\<rho> \<approx> \<sigma> \<Longrightarrow> \<sigma> \<approx> \<tau> \<Longrightarrow> \<rho> \<approx> \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<rho> \<approx> \<sigma>; \<sigma> \<approx> \<tau>\<rbrakk> \<Longrightarrow> \<rho> \<approx> \<tau>
[PROOF STEP]
unfolding stutter_equiv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<natural>\<rho> = \<natural>\<sigma>; \<natural>\<sigma> = \<natural>\<tau>\<rbrakk> \<Longrightarrow> \<natural>\<rho> = \<natural>\<tau>
[PROOF STEP]
by simp


[STATEMENT]
lemma sampled_stutter_equiv:
  assumes "stutter_sampler f \<sigma>"
  shows "\<sigma> \<circ> f \<approx> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<circ> f \<approx> \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>

goal (1 subgoal):
 1. \<sigma> \<circ> f \<approx> \<sigma>
[PROOF STEP]
unfolding stutter_equiv_def
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>

goal (1 subgoal):
 1. \<natural>(\<sigma> \<circ> f) = \<natural>\<sigma>
[PROOF STEP]
by (rule sample_max_sample)


[STATEMENT]
lemma stutter_reduced_equivalent: "\<natural>\<sigma> \<approx> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<natural>\<sigma> \<approx> \<sigma>
[PROOF STEP]
unfolding stutter_equiv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<natural>\<natural>\<sigma> = \<natural>\<sigma>
[PROOF STEP]
by (rule stutter_reduced_reduced)


[STATEMENT]
lemma stutter_equivI:
  assumes f: "stutter_sampler f \<sigma>" and g: "stutter_sampler g \<tau>"
      and eq: "\<sigma> \<circ> f = \<tau> \<circ> g"
  shows "\<sigma> \<approx> \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<approx> \<tau>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<approx> \<tau>
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler f \<sigma>
[PROOF STEP]
have "\<natural>\<sigma> = \<natural>(\<sigma> \<circ> f)"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>

goal (1 subgoal):
 1. \<natural>\<sigma> = \<natural>(\<sigma> \<circ> f)
[PROOF STEP]
by (rule sample_max_sample[THEN sym])
[PROOF STATE]
proof (state)
this:
\<natural>\<sigma> = \<natural>(\<sigma> \<circ> f)

goal (1 subgoal):
 1. \<sigma> \<approx> \<tau>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<natural>\<sigma> = \<natural>(\<sigma> \<circ> f)

goal (1 subgoal):
 1. \<sigma> \<approx> \<tau>
[PROOF STEP]
from eq
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<circ> f = \<tau> \<circ> g
[PROOF STEP]
have "... = \<natural>(\<tau> \<circ> g)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<circ> f = \<tau> \<circ> g

goal (1 subgoal):
 1. \<natural>(\<sigma> \<circ> f) = \<natural>(\<tau> \<circ> g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<natural>(\<sigma> \<circ> f) = \<natural>(\<tau> \<circ> g)

goal (1 subgoal):
 1. \<sigma> \<approx> \<tau>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<natural>(\<sigma> \<circ> f) = \<natural>(\<tau> \<circ> g)

goal (1 subgoal):
 1. \<sigma> \<approx> \<tau>
[PROOF STEP]
from g
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler g \<tau>
[PROOF STEP]
have "... = \<natural>\<tau>"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler g \<tau>

goal (1 subgoal):
 1. \<natural>(\<tau> \<circ> g) = \<natural>\<tau>
[PROOF STEP]
by (rule sample_max_sample)
[PROOF STATE]
proof (state)
this:
\<natural>(\<tau> \<circ> g) = \<natural>\<tau>

goal (1 subgoal):
 1. \<sigma> \<approx> \<tau>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<natural>\<sigma> = \<natural>\<tau>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<natural>\<sigma> = \<natural>\<tau>

goal (1 subgoal):
 1. \<sigma> \<approx> \<tau>
[PROOF STEP]
by (unfold stutter_equiv_def)
[PROOF STATE]
proof (state)
this:
\<sigma> \<approx> \<tau>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_equivE:
  assumes eq: "\<sigma> \<approx> \<tau>"
  and p: "\<And>f g. \<lbrakk> stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g \<rbrakk> \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof (rule p)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. stutter_sampler ?f \<sigma>
 2. stutter_sampler ?g \<tau>
 3. \<sigma> \<circ> ?f = \<tau> \<circ> ?g
[PROOF STEP]
from eq
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<approx> \<tau>
[PROOF STEP]
show "\<sigma> \<circ> (max_stutter_sampler \<sigma>) = \<tau> \<circ> (max_stutter_sampler \<tau>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<approx> \<tau>

goal (1 subgoal):
 1. \<sigma> \<circ> max_stutter_sampler \<sigma> = \<tau> \<circ> max_stutter_sampler \<tau>
[PROOF STEP]
by (unfold stutter_equiv_def stutter_reduced_def)
[PROOF STATE]
proof (state)
this:
\<sigma> \<circ> max_stutter_sampler \<sigma> = \<tau> \<circ> max_stutter_sampler \<tau>

goal (2 subgoals):
 1. stutter_sampler (max_stutter_sampler \<sigma>) \<sigma>
 2. stutter_sampler (max_stutter_sampler \<tau>) \<tau>
[PROOF STEP]
qed (rule max_stutter_sampler)+


[STATEMENT]
lemma stutter_equiv_eq:
  "\<sigma> \<approx> \<tau> = (\<exists>f g. stutter_sampler f \<sigma> \<and> stutter_sampler g \<tau> \<and> \<sigma> \<circ> f = \<tau> \<circ> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma> \<approx> \<tau>) = (\<exists>f g. stutter_sampler f \<sigma> \<and> stutter_sampler g \<tau> \<and> \<sigma> \<circ> f = \<tau> \<circ> g)
[PROOF STEP]
by (blast intro: stutter_equivI elim: stutter_equivE)


[STATEMENT]
lemma stutter_equiv_0:
  assumes "\<sigma> \<approx> \<tau>"
  shows "\<sigma> 0 = \<tau> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> 0 = \<tau> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> 0 = \<tau> 0
[PROOF STEP]
have "\<sigma> 0 = (\<natural>\<sigma>) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> 0 = (\<natural>\<sigma>) 0
[PROOF STEP]
by (rule stutter_reduced_0[THEN sym])
[PROOF STATE]
proof (state)
this:
\<sigma> 0 = (\<natural>\<sigma>) 0

goal (1 subgoal):
 1. \<sigma> 0 = \<tau> 0
[PROOF STEP]
with assms[unfolded stutter_equiv_def]
[PROOF STATE]
proof (chain)
picking this:
\<natural>\<sigma> = \<natural>\<tau>
\<sigma> 0 = (\<natural>\<sigma>) 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<natural>\<sigma> = \<natural>\<tau>
\<sigma> 0 = (\<natural>\<sigma>) 0

goal (1 subgoal):
 1. \<sigma> 0 = \<tau> 0
[PROOF STEP]
by (simp add: stutter_reduced_0)
[PROOF STATE]
proof (state)
this:
\<sigma> 0 = \<tau> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma suffix_stutter_equiv:
  assumes f: "stutter_sampler f \<sigma>"
  shows "suffix (f n) \<sigma> \<approx> suffix n (\<sigma> \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> [f n..] \<approx> \<sigma> \<circ> f [n..]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> [f n..] \<approx> \<sigma> \<circ> f [n..]
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler f \<sigma>
[PROOF STEP]
have "stutter_sampler (\<lambda>k. f (n+k) - f n) (\<sigma>[f n ..])"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>

goal (1 subgoal):
 1. stutter_sampler (\<lambda>k. f (n + k) - f n) \<sigma> [f n..]
[PROOF STEP]
by (rule stutter_sampler_suffix)
[PROOF STATE]
proof (state)
this:
stutter_sampler (\<lambda>k. f (n + k) - f n) \<sigma> [f n..]

goal (1 subgoal):
 1. \<sigma> [f n..] \<approx> \<sigma> \<circ> f [n..]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stutter_sampler (\<lambda>k. f (n + k) - f n) \<sigma> [f n..]

goal (1 subgoal):
 1. \<sigma> [f n..] \<approx> \<sigma> \<circ> f [n..]
[PROOF STEP]
have "stutter_sampler id ((\<sigma> \<circ> f)[n ..])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler id \<sigma> \<circ> f [n..]
[PROOF STEP]
by (rule id_stutter_sampler)
[PROOF STATE]
proof (state)
this:
stutter_sampler id \<sigma> \<circ> f [n..]

goal (1 subgoal):
 1. \<sigma> [f n..] \<approx> \<sigma> \<circ> f [n..]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stutter_sampler id \<sigma> \<circ> f [n..]

goal (1 subgoal):
 1. \<sigma> [f n..] \<approx> \<sigma> \<circ> f [n..]
[PROOF STEP]
have "(\<sigma>[f n ..]) \<circ> (\<lambda>k. f (n+k) - f n) = ((\<sigma> \<circ> f)[n ..]) \<circ> id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> [f n..] \<circ> (\<lambda>k. f (n + k) - f n) = \<sigma> \<circ> f [n..] \<circ> id
[PROOF STEP]
proof (rule ext, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<sigma> (f n + (f (n + x) - f n)) = \<sigma> (f (n + x))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<sigma> (f n + (f (n + x) - f n)) = \<sigma> (f (n + x))
[PROOF STEP]
from f[THEN stutter_sampler_mono, THEN strict_mono_mono]
[PROOF STATE]
proof (chain)
picking this:
mono f
[PROOF STEP]
have "f n \<le> f (n+i)"
[PROOF STATE]
proof (prove)
using this:
mono f

goal (1 subgoal):
 1. f n \<le> f (n + i)
[PROOF STEP]
by (rule monoD) simp
[PROOF STATE]
proof (state)
this:
f n \<le> f (n + i)

goal (1 subgoal):
 1. \<And>x. \<sigma> (f n + (f (n + x) - f n)) = \<sigma> (f (n + x))
[PROOF STEP]
thus "\<sigma> (f n + (f (n+i) - f n)) = \<sigma> (f (n+i))"
[PROOF STATE]
proof (prove)
using this:
f n \<le> f (n + i)

goal (1 subgoal):
 1. \<sigma> (f n + (f (n + i) - f n)) = \<sigma> (f (n + i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> (f n + (f (n + i) - f n)) = \<sigma> (f (n + i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma> [f n..] \<circ> (\<lambda>k. f (n + k) - f n) = \<sigma> \<circ> f [n..] \<circ> id

goal (1 subgoal):
 1. \<sigma> [f n..] \<approx> \<sigma> \<circ> f [n..]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler (\<lambda>k. f (n + k) - f n) \<sigma> [f n..]
stutter_sampler id \<sigma> \<circ> f [n..]
\<sigma> [f n..] \<circ> (\<lambda>k. f (n + k) - f n) = \<sigma> \<circ> f [n..] \<circ> id
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stutter_sampler (\<lambda>k. f (n + k) - f n) \<sigma> [f n..]
stutter_sampler id \<sigma> \<circ> f [n..]
\<sigma> [f n..] \<circ> (\<lambda>k. f (n + k) - f n) = \<sigma> \<circ> f [n..] \<circ> id

goal (1 subgoal):
 1. \<sigma> [f n..] \<approx> \<sigma> \<circ> f [n..]
[PROOF STEP]
by (rule stutter_equivI)
[PROOF STATE]
proof (state)
this:
\<sigma> [f n..] \<approx> \<sigma> \<circ> f [n..]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_equiv_within_interval:
  assumes f: "stutter_sampler f \<sigma>"
      and lo: "f k \<le> n" and hi: "n < f (Suc k)"
  shows "\<sigma>[n ..] \<approx> \<sigma>[f k ..]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> [n..] \<approx> \<sigma> [f k..]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> [n..] \<approx> \<sigma> [f k..]
[PROOF STEP]
have "stutter_sampler id (\<sigma>[n ..])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler id \<sigma> [n..]
[PROOF STEP]
by (rule id_stutter_sampler)
[PROOF STATE]
proof (state)
this:
stutter_sampler id \<sigma> [n..]

goal (1 subgoal):
 1. \<sigma> [n..] \<approx> \<sigma> [f k..]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stutter_sampler id \<sigma> [n..]

goal (1 subgoal):
 1. \<sigma> [n..] \<approx> \<sigma> [f k..]
[PROOF STEP]
from lo
[PROOF STATE]
proof (chain)
picking this:
f k \<le> n
[PROOF STEP]
have "stutter_sampler (\<lambda>i. if i=0 then 0 else n + i - f k) (\<sigma>[f k ..])"
    (is "stutter_sampler ?f _")
[PROOF STATE]
proof (prove)
using this:
f k \<le> n

goal (1 subgoal):
 1. stutter_sampler (\<lambda>i. if i = 0 then 0 else n + i - f k) \<sigma> [f k..]
[PROOF STEP]
proof (auto simp: stutter_sampler_def strict_mono_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>f k \<le> n; 0 < na; na < Suc n - f k\<rbrakk> \<Longrightarrow> \<sigma> (f k + na) = \<sigma> (f k)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>f k \<le> n; 0 < na; na < Suc n - f k\<rbrakk> \<Longrightarrow> \<sigma> (f k + na) = \<sigma> (f k)
[PROOF STEP]
assume i: "i < Suc n - f k"
[PROOF STATE]
proof (state)
this:
i < Suc n - f k

goal (1 subgoal):
 1. \<And>na. \<lbrakk>f k \<le> n; 0 < na; na < Suc n - f k\<rbrakk> \<Longrightarrow> \<sigma> (f k + na) = \<sigma> (f k)
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler f \<sigma>
[PROOF STEP]
show "\<sigma> (f k + i) = \<sigma> (f k)"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>

goal (1 subgoal):
 1. \<sigma> (f k + i) = \<sigma> (f k)
[PROOF STEP]
proof (rule stutter_sampler_between)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f k \<le> f k + i
 2. f k + i < f (Suc k)
[PROOF STEP]
from i hi
[PROOF STATE]
proof (chain)
picking this:
i < Suc n - f k
n < f (Suc k)
[PROOF STEP]
show "f k + i < f (Suc k)"
[PROOF STATE]
proof (prove)
using this:
i < Suc n - f k
n < f (Suc k)

goal (1 subgoal):
 1. f k + i < f (Suc k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f k + i < f (Suc k)

goal (1 subgoal):
 1. f k \<le> f k + i
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<sigma> (f k + i) = \<sigma> (f k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stutter_sampler (\<lambda>i. if i = 0 then 0 else n + i - f k) \<sigma> [f k..]

goal (1 subgoal):
 1. \<sigma> [n..] \<approx> \<sigma> [f k..]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stutter_sampler (\<lambda>i. if i = 0 then 0 else n + i - f k) \<sigma> [f k..]

goal (1 subgoal):
 1. \<sigma> [n..] \<approx> \<sigma> [f k..]
[PROOF STEP]
have "(\<sigma>[n ..]) \<circ> id = (\<sigma>[f k ..]) \<circ> ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> [n..] \<circ> id = \<sigma> [f k..] \<circ> (\<lambda>i. if i = 0 then 0 else n + i - f k)
[PROOF STEP]
proof (rule ext, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<sigma> n = \<sigma> (f k)
 2. \<And>x. 0 < x \<Longrightarrow> \<sigma> (n + x) = \<sigma> (f k + (n + x - f k))
[PROOF STEP]
from f lo hi
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler f \<sigma>
f k \<le> n
n < f (Suc k)
[PROOF STEP]
show "\<sigma> n = \<sigma> (f k)"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>
f k \<le> n
n < f (Suc k)

goal (1 subgoal):
 1. \<sigma> n = \<sigma> (f k)
[PROOF STEP]
by (rule stutter_sampler_between)
[PROOF STATE]
proof (state)
this:
\<sigma> n = \<sigma> (f k)

goal (1 subgoal):
 1. \<And>x. 0 < x \<Longrightarrow> \<sigma> (n + x) = \<sigma> (f k + (n + x - f k))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. 0 < x \<Longrightarrow> \<sigma> (n + x) = \<sigma> (f k + (n + x - f k))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. 0 < x \<Longrightarrow> \<sigma> (n + x) = \<sigma> (f k + (n + x - f k))
[PROOF STEP]
from lo
[PROOF STATE]
proof (chain)
picking this:
f k \<le> n
[PROOF STEP]
show "\<sigma> (n+i) = \<sigma> (f k + (n + i - f k))"
[PROOF STATE]
proof (prove)
using this:
f k \<le> n

goal (1 subgoal):
 1. \<sigma> (n + i) = \<sigma> (f k + (n + i - f k))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> (n + i) = \<sigma> (f k + (n + i - f k))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma> [n..] \<circ> id = \<sigma> [f k..] \<circ> (\<lambda>i. if i = 0 then 0 else n + i - f k)

goal (1 subgoal):
 1. \<sigma> [n..] \<approx> \<sigma> [f k..]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler id \<sigma> [n..]
stutter_sampler (\<lambda>i. if i = 0 then 0 else n + i - f k) \<sigma> [f k..]
\<sigma> [n..] \<circ> id = \<sigma> [f k..] \<circ> (\<lambda>i. if i = 0 then 0 else n + i - f k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stutter_sampler id \<sigma> [n..]
stutter_sampler (\<lambda>i. if i = 0 then 0 else n + i - f k) \<sigma> [f k..]
\<sigma> [n..] \<circ> id = \<sigma> [f k..] \<circ> (\<lambda>i. if i = 0 then 0 else n + i - f k)

goal (1 subgoal):
 1. \<sigma> [n..] \<approx> \<sigma> [f k..]
[PROOF STEP]
by (rule stutter_equivI)
[PROOF STATE]
proof (state)
this:
\<sigma> [n..] \<approx> \<sigma> [f k..]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem stutter_equiv_suffixes_left:
  assumes "\<sigma> \<approx> \<tau>"
  obtains m where "\<sigma>[m..] \<approx> \<tau>[n..]" and "\<forall>j<m. \<exists>k<n. \<sigma>[j..] \<approx> \<tau>[k..]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<approx> \<tau>

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule stutter_equivE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix f g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume f: "stutter_sampler f \<sigma>"
     and g: "stutter_sampler g \<tau>"
     and eq: "\<sigma> \<circ> f = \<tau> \<circ> g"
[PROOF STATE]
proof (state)
this:
stutter_sampler f \<sigma>
stutter_sampler g \<tau>
\<sigma> \<circ> f = \<tau> \<circ> g

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from g
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler g \<tau>
[PROOF STEP]
obtain i where i: "g i \<le> n" "n < g (Suc i)"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler g \<tau>

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>g i \<le> n; n < g (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule stutter_sampler_interval)
[PROOF STATE]
proof (state)
this:
g i \<le> n
n < g (Suc i)

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with g
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler g \<tau>
g i \<le> n
n < g (Suc i)
[PROOF STEP]
have "\<tau>[n..] \<approx> \<tau>[g i ..]"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler g \<tau>
g i \<le> n
n < g (Suc i)

goal (1 subgoal):
 1. \<tau> [n..] \<approx> \<tau> [g i..]
[PROOF STEP]
by (rule stutter_equiv_within_interval)
[PROOF STATE]
proof (state)
this:
\<tau> [n..] \<approx> \<tau> [g i..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<tau> [n..] \<approx> \<tau> [g i..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from g
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler g \<tau>
[PROOF STEP]
have "... \<approx> (\<tau> \<circ> g)[i ..]"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler g \<tau>

goal (1 subgoal):
 1. \<tau> [g i..] \<approx> \<tau> \<circ> g [i..]
[PROOF STEP]
by (rule suffix_stutter_equiv)
[PROOF STATE]
proof (state)
this:
\<tau> [g i..] \<approx> \<tau> \<circ> g [i..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<tau> [g i..] \<approx> \<tau> \<circ> g [i..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from eq
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<circ> f = \<tau> \<circ> g
[PROOF STEP]
have "... = (\<sigma> \<circ> f)[i ..]"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<circ> f = \<tau> \<circ> g

goal (1 subgoal):
 1. \<tau> \<circ> g [i..] = \<sigma> \<circ> f [i..]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<tau> \<circ> g [i..] = \<sigma> \<circ> f [i..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<tau> \<circ> g [i..] = \<sigma> \<circ> f [i..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler f \<sigma>
[PROOF STEP]
have "... \<approx> \<sigma>[f i ..]"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>

goal (1 subgoal):
 1. \<sigma> \<circ> f [i..] \<approx> \<sigma> [f i..]
[PROOF STEP]
by (rule suffix_stutter_equiv[THEN stutter_equiv_sym])
[PROOF STATE]
proof (state)
this:
\<sigma> \<circ> f [i..] \<approx> \<sigma> [f i..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<tau> [n..] \<approx> \<sigma> [f i..]
[PROOF STEP]
have "\<sigma>[f i ..] \<approx> \<tau>[n ..]"
[PROOF STATE]
proof (prove)
using this:
\<tau> [n..] \<approx> \<sigma> [f i..]

goal (1 subgoal):
 1. \<sigma> [f i..] \<approx> \<tau> [n..]
[PROOF STEP]
by (rule stutter_equiv_sym)
[PROOF STATE]
proof (state)
this:
\<sigma> [f i..] \<approx> \<tau> [n..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<sigma> [f i..] \<approx> \<tau> [n..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<sigma> [f i..] \<approx> \<tau> [n..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume j: "j < f i"
[PROOF STATE]
proof (state)
this:
j < f i

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler f \<sigma>
[PROOF STEP]
obtain a where a: "f a \<le> j" "j < f (Suc a)"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>f a \<le> j; j < f (Suc a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule stutter_sampler_interval)
[PROOF STATE]
proof (state)
this:
f a \<le> j
j < f (Suc a)

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from a j
[PROOF STATE]
proof (chain)
picking this:
f a \<le> j
j < f (Suc a)
j < f i
[PROOF STEP]
have "f a < f i"
[PROOF STATE]
proof (prove)
using this:
f a \<le> j
j < f (Suc a)
j < f i

goal (1 subgoal):
 1. f a < f i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f a < f i

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with f[THEN stutter_sampler_mono]
[PROOF STATE]
proof (chain)
picking this:
strict_mono f
f a < f i
[PROOF STEP]
have "a < i"
[PROOF STATE]
proof (prove)
using this:
strict_mono f
f a < f i

goal (1 subgoal):
 1. a < i
[PROOF STEP]
by (simp add: strict_mono_less)
[PROOF STATE]
proof (state)
this:
a < i

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with g[THEN stutter_sampler_mono]
[PROOF STATE]
proof (chain)
picking this:
strict_mono g
a < i
[PROOF STEP]
have "g a < g i"
[PROOF STATE]
proof (prove)
using this:
strict_mono g
a < i

goal (1 subgoal):
 1. g a < g i
[PROOF STEP]
by (simp add: strict_mono_less)
[PROOF STATE]
proof (state)
this:
g a < g i

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
g i \<le> n
n < g (Suc i)
g a < g i
[PROOF STEP]
have 1: "g a < n"
[PROOF STATE]
proof (prove)
using this:
g i \<le> n
n < g (Suc i)
g a < g i

goal (1 subgoal):
 1. g a < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g a < n

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from f a
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler f \<sigma>
f a \<le> j
j < f (Suc a)
[PROOF STEP]
have "\<sigma>[j..] \<approx> \<sigma>[f a ..]"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>
f a \<le> j
j < f (Suc a)

goal (1 subgoal):
 1. \<sigma> [j..] \<approx> \<sigma> [f a..]
[PROOF STEP]
by (rule stutter_equiv_within_interval)
[PROOF STATE]
proof (state)
this:
\<sigma> [j..] \<approx> \<sigma> [f a..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<sigma> [j..] \<approx> \<sigma> [f a..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler f \<sigma>
[PROOF STEP]
have "... \<approx> (\<sigma> \<circ> f)[a ..]"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f \<sigma>

goal (1 subgoal):
 1. \<sigma> [f a..] \<approx> \<sigma> \<circ> f [a..]
[PROOF STEP]
by (rule suffix_stutter_equiv)
[PROOF STATE]
proof (state)
this:
\<sigma> [f a..] \<approx> \<sigma> \<circ> f [a..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<sigma> [f a..] \<approx> \<sigma> \<circ> f [a..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from eq
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<circ> f = \<tau> \<circ> g
[PROOF STEP]
have "... = (\<tau> \<circ> g)[a ..]"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<circ> f = \<tau> \<circ> g

goal (1 subgoal):
 1. \<sigma> \<circ> f [a..] = \<tau> \<circ> g [a..]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> \<circ> f [a..] = \<tau> \<circ> g [a..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<sigma> \<circ> f [a..] = \<tau> \<circ> g [a..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from g
[PROOF STATE]
proof (chain)
picking this:
stutter_sampler g \<tau>
[PROOF STEP]
have "... \<approx> \<tau>[g a ..]"
[PROOF STATE]
proof (prove)
using this:
stutter_sampler g \<tau>

goal (1 subgoal):
 1. \<tau> \<circ> g [a..] \<approx> \<tau> [g a..]
[PROOF STEP]
by (rule suffix_stutter_equiv[THEN stutter_equiv_sym])
[PROOF STATE]
proof (state)
this:
\<tau> \<circ> g [a..] \<approx> \<tau> [g a..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<sigma> [j..] \<approx> \<tau> [g a..]
[PROOF STEP]
have "\<sigma>[j ..] \<approx> \<tau>[g a ..]"
[PROOF STATE]
proof (prove)
using this:
\<sigma> [j..] \<approx> \<tau> [g a..]

goal (1 subgoal):
 1. \<sigma> [j..] \<approx> \<tau> [g a..]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<sigma> [j..] \<approx> \<tau> [g a..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
g a < n
\<sigma> [j..] \<approx> \<tau> [g a..]
[PROOF STEP]
have "\<exists>k<n. \<sigma>[j..] \<approx> \<tau>[k ..]"
[PROOF STATE]
proof (prove)
using this:
g a < n
\<sigma> [j..] \<approx> \<tau> [g a..]

goal (1 subgoal):
 1. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?j2 < f i \<Longrightarrow> \<exists>k<n. \<sigma> [?j2..] \<approx> \<tau> [k..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?j2 < f i \<Longrightarrow> \<exists>k<n. \<sigma> [?j2..] \<approx> \<tau> [k..]

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note that
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<sigma> [?m..] \<approx> \<tau> [n..]; \<forall>j<?m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis; stutter_sampler f \<sigma>; stutter_sampler g \<tau>; \<sigma> \<circ> f = \<tau> \<circ> g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<sigma> [f i..] \<approx> \<tau> [n..]
?j2 < f i \<Longrightarrow> \<exists>k<n. \<sigma> [?j2..] \<approx> \<tau> [k..]
\<lbrakk>\<sigma> [?m..] \<approx> \<tau> [n..]; \<forall>j<?m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<sigma> [f i..] \<approx> \<tau> [n..]
?j2 < f i \<Longrightarrow> \<exists>k<n. \<sigma> [?j2..] \<approx> \<tau> [k..]
\<lbrakk>\<sigma> [?m..] \<approx> \<tau> [n..]; \<forall>j<?m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem stutter_equiv_suffixes_right:
  assumes "\<sigma> \<approx> \<tau>"
  obtains n where "\<sigma>[m..] \<approx> \<tau>[n..]" and "\<forall>j<n. \<exists>k<m. \<sigma>[k..] \<approx> \<tau>[j..]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<approx> \<tau>
[PROOF STEP]
have "\<tau> \<approx> \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<approx> \<tau>

goal (1 subgoal):
 1. \<tau> \<approx> \<sigma>
[PROOF STEP]
by (rule stutter_equiv_sym)
[PROOF STATE]
proof (state)
this:
\<tau> \<approx> \<sigma>

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<approx> \<sigma>
[PROOF STEP]
obtain n where "\<tau>[n..] \<approx> \<sigma>[m..]" "\<forall>j<n. \<exists>k<m. \<tau>[j..] \<approx> \<sigma>[k..]"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<approx> \<sigma>

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<tau> [n..] \<approx> \<sigma> [m..]; \<forall>j<n. \<exists>k<m. \<tau> [j..] \<approx> \<sigma> [k..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule stutter_equiv_suffixes_left)
[PROOF STATE]
proof (state)
this:
\<tau> [n..] \<approx> \<sigma> [m..]
\<forall>j<n. \<exists>k<m. \<tau> [j..] \<approx> \<sigma> [k..]

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<sigma> [m..] \<approx> \<tau> [?n..]; \<forall>j<?n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]\<rbrakk> \<Longrightarrow> thesis
\<tau> [n..] \<approx> \<sigma> [m..]
\<forall>j<n. \<exists>k<m. \<tau> [j..] \<approx> \<sigma> [k..]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<sigma> [m..] \<approx> \<tau> [?n..]; \<forall>j<?n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]\<rbrakk> \<Longrightarrow> thesis
\<tau> [n..] \<approx> \<sigma> [m..]
\<forall>j<n. \<exists>k<m. \<tau> [j..] \<approx> \<sigma> [k..]

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (blast dest: stutter_equiv_sym)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_equiv_element_left:
  assumes "\<sigma> \<approx> \<tau>"
  obtains m where "\<sigma> m = \<tau> n" and "\<forall>j<m. \<exists>k<n. \<sigma> j = \<tau> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>\<sigma> m = \<tau> n; \<forall>j<m. \<exists>k<n. \<sigma> j = \<tau> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>\<sigma> m = \<tau> n; \<forall>j<m. \<exists>k<n. \<sigma> j = \<tau> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<approx> \<tau>
[PROOF STEP]
obtain m where "\<sigma>[m..] \<approx> \<tau>[n..]" "\<forall>j<m. \<exists>k<n. \<sigma>[j..] \<approx> \<tau>[k..]"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<approx> \<tau>

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule stutter_equiv_suffixes_left)
[PROOF STATE]
proof (state)
this:
\<sigma> [m..] \<approx> \<tau> [n..]
\<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>\<sigma> m = \<tau> n; \<forall>j<m. \<exists>k<n. \<sigma> j = \<tau> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<sigma> ?m = \<tau> n; \<forall>j<?m. \<exists>k<n. \<sigma> j = \<tau> k\<rbrakk> \<Longrightarrow> thesis
\<sigma> [m..] \<approx> \<tau> [n..]
\<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<sigma> ?m = \<tau> n; \<forall>j<?m. \<exists>k<n. \<sigma> j = \<tau> k\<rbrakk> \<Longrightarrow> thesis
\<sigma> [m..] \<approx> \<tau> [n..]
\<forall>j<m. \<exists>k<n. \<sigma> [j..] \<approx> \<tau> [k..]

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (force dest: stutter_equiv_0)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_equiv_element_right:
  assumes "\<sigma> \<approx> \<tau>"
  obtains n where "\<sigma> m = \<tau> n" and "\<forall>j<n. \<exists>k<m. \<sigma> k = \<tau> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<sigma> m = \<tau> n; \<forall>j<n. \<exists>k<m. \<sigma> k = \<tau> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<sigma> m = \<tau> n; \<forall>j<n. \<exists>k<m. \<sigma> k = \<tau> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<approx> \<tau>
[PROOF STEP]
obtain n where "\<sigma>[m..] \<approx> \<tau>[n..]" "\<forall>j<n. \<exists>k<m. \<sigma>[k..] \<approx> \<tau>[j..]"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<approx> \<tau>

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>j<n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule stutter_equiv_suffixes_right)
[PROOF STATE]
proof (state)
this:
\<sigma> [m..] \<approx> \<tau> [n..]
\<forall>j<n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<sigma> m = \<tau> n; \<forall>j<n. \<exists>k<m. \<sigma> k = \<tau> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<sigma> m = \<tau> ?n; \<forall>j<?n. \<exists>k<m. \<sigma> k = \<tau> j\<rbrakk> \<Longrightarrow> thesis
\<sigma> [m..] \<approx> \<tau> [n..]
\<forall>j<n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<sigma> m = \<tau> ?n; \<forall>j<?n. \<exists>k<m. \<sigma> k = \<tau> j\<rbrakk> \<Longrightarrow> thesis
\<sigma> [m..] \<approx> \<tau> [n..]
\<forall>j<n. \<exists>k<m. \<sigma> [k..] \<approx> \<tau> [j..]

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (force dest: stutter_equiv_0)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma corrKey_Dom_keySetup [simp, intro]: "K \<in> corrKey \<Longrightarrow> K \<in> Domain keySetup"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K \<in> corrKey \<Longrightarrow> K \<in> Domain keySetup
[PROOF STEP]
by (auto simp add: corrKey_def)


[STATEMENT]
lemma keySetup_noSessionKeys [simp]: "(sesK K, A) \<notin> keySetup"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sesK K, A) \<notin> keySetup
[PROOF STEP]
by (simp add: keySetup_def)


[STATEMENT]
lemma corrKey_noSessionKeys [simp]: "sesK K \<notin> corrKey"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sesK K \<notin> corrKey
[PROOF STEP]
by (auto simp add: keySetup_def corrKey_def)


[STATEMENT]
lemma inner_prod_eq:
  fixes i::"'a::finite"
  shows "(\<lambda>(v::'a Rvec). v \<bullet> axis i 1) = (\<lambda>(v::'a Rvec). v $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. v \<bullet> axis i 1) = (\<lambda>v. v $ i)
[PROOF STEP]
unfolding cart_eq_inner_axis axis_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. v \<bullet> (\<chi>ia. if ia = i then 1 else 0)) = (\<lambda>v. v \<bullet> (\<chi>ia. if ia = i then 1 else 0))
[PROOF STEP]
by (simp add: eq_commute)


[STATEMENT]
theorem svar_deriv:
  fixes x:: "'sv::finite" and \<nu>:: "'sv Rvec" and F::"real filter"
  shows "((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi> i. if i = x then 1 else 0))) (at \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
let ?f = "(\<lambda>v. v)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
let ?f' = "(\<lambda>v'. v')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
let ?g = "(\<lambda>v. axis x 1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
let ?g' = "(\<lambda>v. 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
have id_deriv: "(?f has_derivative ?f') (at \<nu>) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>v. v) has_derivative (\<lambda>v'. v')) (at \<nu>)
[PROOF STEP]
by (rule has_derivative_ident)
[PROOF STATE]
proof (state)
this:
((\<lambda>v. v) has_derivative (\<lambda>v'. v')) (at \<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
have const_deriv: "(?g has_derivative ?g') (at \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>v. axis x (1::'a)) has_derivative (\<lambda>v. 0)) (at \<nu>)
[PROOF STEP]
by (rule has_derivative_const)
[PROOF STATE]
proof (state)
this:
((\<lambda>v. axis x (1::?'a10)) has_derivative (\<lambda>v. 0)) (at \<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
have inner_deriv:"((\<lambda>x. inner (?f x) (?g x)) has_derivative
                     (\<lambda>h. inner (?f \<nu>) (?g' h) + inner (?f' h) (?g \<nu>))) (at \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>xa. xa \<bullet> axis x 1) has_derivative (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)) (at \<nu>)
[PROOF STEP]
by (intro has_derivative_inner [OF id_deriv const_deriv])
[PROOF STATE]
proof (state)
this:
((\<lambda>xa. xa \<bullet> axis x 1) has_derivative (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)) (at \<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
from inner_prod_eq
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>v. v \<bullet> axis ?i 1) = (\<lambda>v. v $ ?i)
[PROOF STEP]
have left_eq: "(\<lambda>x. inner (?f x) (?g x)) = (\<lambda>v. vec_nth v x)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>v. v \<bullet> axis ?i 1) = (\<lambda>v. v $ ?i)

goal (1 subgoal):
 1. (\<lambda>xa. xa \<bullet> axis x 1) = (\<lambda>v. v $ x)
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>xa. xa \<bullet> axis x 1) = (\<lambda>v. v $ x)

goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
from inner_deriv and inner_prod_eq
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>xa. xa \<bullet> axis x 1) has_derivative (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)) (at \<nu>)
(\<lambda>v. v \<bullet> axis ?i 1) = (\<lambda>v. v $ ?i)
[PROOF STEP]
have better_deriv:"((\<lambda>v. vec_nth v x) has_derivative
                     (\<lambda>h. inner (?f \<nu>) (?g' h) + inner (?f' h) (?g \<nu>))) (at \<nu>)"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>xa. xa \<bullet> axis x 1) has_derivative (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)) (at \<nu>)
(\<lambda>v. v \<bullet> axis ?i 1) = (\<lambda>v. v $ ?i)

goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)) (at \<nu>)
[PROOF STEP]
by (metis (no_types, lifting) UNIV_I has_derivative_transform)
[PROOF STATE]
proof (state)
this:
((\<lambda>v. v $ x) has_derivative (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)) (at \<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
have vec_eq:"(\<chi> i. if i = x then 1 else 0) = (\<chi> i. if x = i then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. if i = x then 1::'a else (0::'a)) = (\<chi>i. if x = i then 1::'a else (0::'a))
[PROOF STEP]
by(rule vec_extensionality, auto)
[PROOF STATE]
proof (state)
this:
(\<chi>i. if i = x then 1::?'a11 else (0::?'a11)) = (\<chi>i. if x = i then 1::?'a11 else (0::?'a11))

goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
have deriv_eq:"(\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1) = (\<lambda>v'. v' \<bullet> (\<chi> i. if i = x then 1 else 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x (1::'a)) = (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1::'a else (0::'a)))
[PROOF STEP]
by(rule ext, auto simp add: axis_def vec_eq)
[PROOF STATE]
proof (state)
this:
(\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x (1::?'a12)) = (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1::?'a12 else (0::?'a12)))

goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)
[PROOF STEP]
apply(rule has_derivative_eq_rhs[where f'= "(\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)) (at \<nu>)
 2. (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1) = (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))
[PROOF STEP]
using better_deriv deriv_eq
[PROOF STATE]
proof (prove)
using this:
((\<lambda>v. v $ x) has_derivative (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)) (at \<nu>)
(\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x (1::?'a12)) = (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1::?'a12 else (0::?'a12)))

goal (2 subgoals):
 1. ((\<lambda>v. v $ x) has_derivative (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1)) (at \<nu>)
 2. (\<lambda>h. \<nu> \<bullet> 0 + h \<bullet> axis x 1) = (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>v. v $ x) has_derivative (\<lambda>v'. v' \<bullet> (\<chi>i. if i = x then 1 else 0))) (at \<nu>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma function_case_inner:
  assumes good_interp:
    "(\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x))"
  assumes IH:"((\<lambda>v. \<chi> i. sterm_sem I (args i) v)
             has_derivative (\<lambda> v. (\<chi> i. frechet I (args i) \<nu> v))) (at \<nu>)"
  shows  "((\<lambda>v. Functions I f (\<chi> i. sterm_sem I (args i) v))
            has_derivative (\<lambda>v. frechet I ($f f args) \<nu> v)) (at \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
let ?h = "(\<lambda>v. Functions I f (\<chi> i. sterm_sem I (args i) v))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
let ?h' = "frechet I ($f f args) \<nu>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
let ?g = "(\<lambda>v. \<chi> i. sterm_sem I (args i) v)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
let ?g' = "(\<lambda>v. \<chi> i. frechet I (args i) \<nu> v)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
let ?f = "(\<lambda>y. Functions I f y)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
let ?f' = "FunctionFrechet I f (?g \<nu>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
have hEqFG:  "?h  = ?f  o ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) = Functions I f \<circ> (\<lambda>v. \<chi>i. sterm_sem I (args i) v)
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) = Functions I f \<circ> (\<lambda>v. \<chi>i. sterm_sem I (args i) v)

goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
have hEqFG': "?h' = ?f' o ?g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet I ($f f args) \<nu> = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. frechet I ($f f args) \<nu> = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)
[PROOF STEP]
have frechet_def:"frechet I (Function f args) \<nu>
        = (\<lambda>v'. FunctionFrechet I f (?g \<nu>) (\<chi> i. frechet I (args i) \<nu> v'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet I ($f f args) \<nu> = (\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
frechet I ($f f args) \<nu> = (\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))

goal (1 subgoal):
 1. frechet I ($f f args) \<nu> = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)
[PROOF STEP]
have composition:
      "(\<lambda>v'. FunctionFrechet I f (?g \<nu>) (\<chi> i. frechet I (args i) \<nu> v'))
       = (FunctionFrechet I f (?g \<nu>)) o (\<lambda> v'. \<chi> i. frechet I (args i) \<nu> v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v')) = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v'. \<chi>i. frechet I (args i) \<nu> v')
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v')) = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v'. \<chi>i. frechet I (args i) \<nu> v')

goal (1 subgoal):
 1. frechet I ($f f args) \<nu> = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)
[PROOF STEP]
from frechet_def and composition
[PROOF STATE]
proof (chain)
picking this:
frechet I ($f f args) \<nu> = (\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))
(\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v')) = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v'. \<chi>i. frechet I (args i) \<nu> v')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
frechet I ($f f args) \<nu> = (\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))
(\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v')) = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v'. \<chi>i. frechet I (args i) \<nu> v')

goal (1 subgoal):
 1. frechet I ($f f args) \<nu> = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
frechet I ($f f args) \<nu> = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
frechet I ($f f args) \<nu> = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)

goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
have fDeriv: "(?f has_derivative ?f') (at (?g \<nu>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Functions I f has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>)) (at (\<chi>i. sterm_sem I (args i) \<nu>))
[PROOF STEP]
using good_interp is_interp_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x)
is_interp ?I \<equiv> \<forall>x i. (Functions ?I i has_derivative FunctionFrechet ?I i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet ?I i x))

goal (1 subgoal):
 1. (Functions I f has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>)) (at (\<chi>i. sterm_sem I (args i) \<nu>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(Functions I f has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>)) (at (\<chi>i. sterm_sem I (args i) \<nu>))

goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)
[PROOF STEP]
have gDeriv: "(?g has_derivative ?g') (at \<nu>)"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
((\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
from fDeriv and gDeriv
[PROOF STATE]
proof (chain)
picking this:
(Functions I f has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>)) (at (\<chi>i. sterm_sem I (args i) \<nu>))
((\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)
[PROOF STEP]
have composeDeriv: "((?f o ?g) has_derivative (?f' o ?g')) (at \<nu>)"
[PROOF STATE]
proof (prove)
using this:
(Functions I f has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>)) (at (\<chi>i. sterm_sem I (args i) \<nu>))
((\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)

goal (1 subgoal):
 1. (Functions I f \<circ> (\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)
[PROOF STEP]
using diff_chain_at good_interp
[PROOF STATE]
proof (prove)
using this:
(Functions I f has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>)) (at (\<chi>i. sterm_sem I (args i) \<nu>))
((\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)
\<lbrakk>(?f has_derivative ?f') (at ?x); (?g has_derivative ?g') (at (?f ?x))\<rbrakk> \<Longrightarrow> (?g \<circ> ?f has_derivative ?g' \<circ> ?f') (at ?x)
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x)

goal (1 subgoal):
 1. (Functions I f \<circ> (\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(Functions I f \<circ> (\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
from hEqFG hEqFG' composeDeriv
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) = Functions I f \<circ> (\<lambda>v. \<chi>i. sterm_sem I (args i) v)
frechet I ($f f args) \<nu> = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)
(Functions I f \<circ> (\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) = Functions I f \<circ> (\<lambda>v. \<chi>i. sterm_sem I (args i) v)
frechet I ($f f args) \<nu> = FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)
(Functions I f \<circ> (\<lambda>v. \<chi>i. sterm_sem I (args i) v) has_derivative FunctionFrechet I f (\<chi>i. sterm_sem I (args i) \<nu>) \<circ> (\<lambda>v. \<chi>i. frechet I (args i) \<nu> v)) (at \<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)

goal:
No subgoals!
[PROOF STEP]
qed