[STATEMENT]
lemma cindexE_cong:
  assumes "finite s" and fg_eq:"\<And>x. \<lbrakk>a<x;x<b;x\<notin>s\<rbrakk> \<Longrightarrow> f x = g x"
  shows "cindexE a b f = cindexE a b g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
define left where 
      "left=(\<lambda>f. (\<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x)))"
[PROOF STATE]
proof (state)
this:
left = (\<lambda>f. \<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x))

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
define right where 
      "right=(\<lambda>f. (\<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x)))"
[PROOF STATE]
proof (state)
this:
right = (\<lambda>f. \<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x))

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
have "left f = left g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left f = left g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. left f = left g
[PROOF STEP]
have "jumpF f (at_left x) = jumpF g (at_left x)" when "a<x" "x\<le>b" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jumpF f (at_left x) = jumpF g (at_left x)
[PROOF STEP]
proof (rule jumpF_cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
define cs where "cs \<equiv> {y\<in>s. a<y \<and> y<x}"
[PROOF STATE]
proof (state)
this:
cs \<equiv> {y \<in> s. a < y \<and> y < x}

goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
define c where "c\<equiv> (if cs = {} then (x+a)/2 else Max cs)"
[PROOF STATE]
proof (state)
this:
c \<equiv> if cs = {} then (x + a) / 2 else Max cs

goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
have "finite cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite cs
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {y \<in> s. a < y \<and> y < x}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite s

goal (1 subgoal):
 1. finite {y \<in> s. a < y \<and> y < x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite cs

goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
have "c<x \<and> (\<forall>y. c<y \<and> y<x \<longrightarrow> f y=g y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
proof (cases "cs={}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
cs = {}

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs = {}
[PROOF STEP]
have "\<forall>y. c<y \<and> y<x \<longrightarrow> y \<notin> s"
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. \<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
[PROOF STEP]
unfolding cs_def c_def
[PROOF STATE]
proof (prove)
using this:
{y \<in> s. a < y \<and> y < x} = {}

goal (1 subgoal):
 1. \<forall>y. (if {y \<in> s. a < y \<and> y < x} = {} then (x + a) / 2 else Max {y \<in> s. a < y \<and> y < x}) < y \<and> y < x \<longrightarrow> y \<notin> s
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
have "c=(x+a)/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = (x + a) / 2
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. c = (x + a) / 2
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. (if cs = {} then (x + a) / 2 else Max cs) = (x + a) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c = (x + a) / 2

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
c = (x + a) / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
c = (x + a) / 2

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
using fg_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
c = (x + a) / 2
\<lbrakk>a < ?x; ?x < b; ?x \<notin> s\<rbrakk> \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
c = (x + a) / 2
\<lbrakk>a < ?x; ?x < b; ?x \<notin> s\<rbrakk> \<Longrightarrow> f ?x = g ?x
a < x
x \<le> b

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
cs \<noteq> {}

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs \<noteq> {}
[PROOF STEP]
have "c\<in>cs"
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}

goal (1 subgoal):
 1. c \<in> cs
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}

goal (1 subgoal):
 1. (if cs = {} then (x + a) / 2 else Max cs) \<in> cs
[PROOF STEP]
using False \<open>finite cs\<close>
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}
cs \<noteq> {}
finite cs

goal (1 subgoal):
 1. (if cs = {} then (x + a) / 2 else Max cs) \<in> cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> cs

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c \<in> cs

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
have "\<forall>y. c<y \<and> y<x \<longrightarrow> y \<notin> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) "
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s)

goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s)
[PROOF STEP]
obtain y' where "c<y'" "y'<x" "y'\<in>s"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s)

goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>c < y'; y' < x; y' \<in> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c < y'
y' < x
y' \<in> s

goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c < y'
y' < x
y' \<in> s
[PROOF STEP]
have "y'\<in>cs"
[PROOF STATE]
proof (prove)
using this:
c < y'
y' < x
y' \<in> s

goal (1 subgoal):
 1. y' \<in> cs
[PROOF STEP]
using \<open>c\<in>cs\<close>
[PROOF STATE]
proof (prove)
using this:
c < y'
y' < x
y' \<in> s
c \<in> cs

goal (1 subgoal):
 1. y' \<in> cs
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
using this:
c < y'
y' < x
y' \<in> s
c \<in> {y \<in> s. a < y \<and> y < x}

goal (1 subgoal):
 1. y' \<in> {y \<in> s. a < y \<and> y < x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y' \<in> cs

goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y' \<in> cs
[PROOF STEP]
have "y'\<le>c"
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs

goal (1 subgoal):
 1. y' \<le> c
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs

goal (1 subgoal):
 1. y' \<le> (if cs = {} then (x + a) / 2 else Max cs)
[PROOF STEP]
using False \<open>finite cs\<close>
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs
cs \<noteq> {}
finite cs

goal (1 subgoal):
 1. y' \<le> (if cs = {} then (x + a) / 2 else Max cs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y' \<le> c

goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y' \<le> c
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y' \<le> c

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>c<y'\<close>
[PROOF STATE]
proof (prove)
using this:
y' \<le> c
c < y'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c \<in> cs
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<in> cs
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
using this:
c \<in> {y \<in> s. a < y \<and> y < x}
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> {y \<in> s. a < y \<and> y < x}
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
a < x
x \<le> b

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
by (auto intro!:fg_eq)
[PROOF STATE]
proof (state)
this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
show "\<forall>\<^sub>F x in at_left x. f x = g x"
[PROOF STATE]
proof (prove)
using this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
unfolding eventually_at_left
[PROOF STATE]
proof (prove)
using this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. \<exists>b<x. \<forall>y>b. y < x \<longrightarrow> f y = g y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_left x. f x = g x

goal (1 subgoal):
 1. at_left x = at_left x
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>a < ?x; ?x \<le> b\<rbrakk> \<Longrightarrow> jumpF f (at_left ?x) = jumpF g (at_left ?x)

goal (1 subgoal):
 1. left f = left g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a < ?x; ?x \<le> b\<rbrakk> \<Longrightarrow> jumpF f (at_left ?x) = jumpF g (at_left ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < ?x; ?x \<le> b\<rbrakk> \<Longrightarrow> jumpF f (at_left ?x) = jumpF g (at_left ?x)

goal (1 subgoal):
 1. left f = left g
[PROOF STEP]
unfolding left_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < ?x; ?x \<le> b\<rbrakk> \<Longrightarrow> jumpF f (at_left ?x) = jumpF g (at_left ?x)

goal (1 subgoal):
 1. (\<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x)) = (\<Sum>x | jumpF g (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF g (at_left x))
[PROOF STEP]
by (auto intro: sum.cong)
[PROOF STATE]
proof (state)
this:
left f = left g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
left f = left g

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
left f = left g

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
have "right f = right g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right f = right g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. right f = right g
[PROOF STEP]
have "jumpF f (at_right x) = jumpF g (at_right x)" when "a\<le>x" "x<b" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jumpF f (at_right x) = jumpF g (at_right x)
[PROOF STEP]
proof (rule jumpF_cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
define cs where "cs \<equiv> {y\<in>s. x<y \<and> y<b}"
[PROOF STATE]
proof (state)
this:
cs \<equiv> {y \<in> s. x < y \<and> y < b}

goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
define c where "c\<equiv> (if cs = {} then (x+b)/2 else Min cs)"
[PROOF STATE]
proof (state)
this:
c \<equiv> if cs = {} then (x + b) / 2 else Min cs

goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
have "finite cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite cs
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {y \<in> s. x < y \<and> y < b}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite s

goal (1 subgoal):
 1. finite {y \<in> s. x < y \<and> y < b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite cs

goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
have "x<c \<and> (\<forall>y. x<y \<and> y<c \<longrightarrow> f y=g y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
proof (cases "cs={}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
cs = {}

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs = {}
[PROOF STEP]
have "\<forall>y. x<y \<and> y<c \<longrightarrow> y \<notin> s"
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. \<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
[PROOF STEP]
unfolding cs_def c_def
[PROOF STATE]
proof (prove)
using this:
{y \<in> s. x < y \<and> y < b} = {}

goal (1 subgoal):
 1. \<forall>y. x < y \<and> y < (if {y \<in> s. x < y \<and> y < b} = {} then (x + b) / 2 else Min {y \<in> s. x < y \<and> y < b}) \<longrightarrow> y \<notin> s
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
have "c=(x+b)/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = (x + b) / 2
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. c = (x + b) / 2
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) = (x + b) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c = (x + b) / 2

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
c = (x + b) / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
c = (x + b) / 2

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
using fg_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
c = (x + b) / 2
\<lbrakk>a < ?x; ?x < b; ?x \<notin> s\<rbrakk> \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
c = (x + b) / 2
\<lbrakk>a < ?x; ?x < b; ?x \<notin> s\<rbrakk> \<Longrightarrow> f ?x = g ?x
a \<le> x
x < b

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
cs \<noteq> {}

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs \<noteq> {}
[PROOF STEP]
have "c\<in>cs"
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}

goal (1 subgoal):
 1. c \<in> cs
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) \<in> cs
[PROOF STEP]
using False \<open>finite cs\<close>
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}
cs \<noteq> {}
finite cs

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) \<in> cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> cs

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c \<in> cs

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
have "\<forall>y. x<y \<and> y<c \<longrightarrow> y \<notin> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) "
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s)

goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s)
[PROOF STEP]
obtain y' where "x<y'" "y'<c" "y'\<in>s"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s)

goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>x < y'; y' < c; y' \<in> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y'
y' < c
y' \<in> s

goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < y'
y' < c
y' \<in> s
[PROOF STEP]
have "y'\<in>cs"
[PROOF STATE]
proof (prove)
using this:
x < y'
y' < c
y' \<in> s

goal (1 subgoal):
 1. y' \<in> cs
[PROOF STEP]
using \<open>c\<in>cs\<close>
[PROOF STATE]
proof (prove)
using this:
x < y'
y' < c
y' \<in> s
c \<in> cs

goal (1 subgoal):
 1. y' \<in> cs
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
using this:
x < y'
y' < c
y' \<in> s
c \<in> {y \<in> s. x < y \<and> y < b}

goal (1 subgoal):
 1. y' \<in> {y \<in> s. x < y \<and> y < b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y' \<in> cs

goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y' \<in> cs
[PROOF STEP]
have "y'\<ge>c"
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs

goal (1 subgoal):
 1. c \<le> y'
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) \<le> y'
[PROOF STEP]
using False \<open>finite cs\<close>
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs
cs \<noteq> {}
finite cs

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) \<le> y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<le> y'

goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<le> y'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
c \<le> y'

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>c>y'\<close>
[PROOF STATE]
proof (prove)
using this:
c \<le> y'
y' < c

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c \<in> cs
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<in> cs
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
using this:
c \<in> {y \<in> s. x < y \<and> y < b}
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> {y \<in> s. x < y \<and> y < b}
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
a \<le> x
x < b

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
by (auto intro!:fg_eq)
[PROOF STATE]
proof (state)
this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
show "\<forall>\<^sub>F x in at_right x. f x = g x"
[PROOF STATE]
proof (prove)
using this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
unfolding eventually_at_right
[PROOF STATE]
proof (prove)
using this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. \<exists>b>x. \<forall>y>x. y < b \<longrightarrow> f y = g y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_right x. f x = g x

goal (1 subgoal):
 1. at_right x = at_right x
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<le> ?x; ?x < b\<rbrakk> \<Longrightarrow> jumpF f (at_right ?x) = jumpF g (at_right ?x)

goal (1 subgoal):
 1. right f = right g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a \<le> ?x; ?x < b\<rbrakk> \<Longrightarrow> jumpF f (at_right ?x) = jumpF g (at_right ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> ?x; ?x < b\<rbrakk> \<Longrightarrow> jumpF f (at_right ?x) = jumpF g (at_right ?x)

goal (1 subgoal):
 1. right f = right g
[PROOF STEP]
unfolding right_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> ?x; ?x < b\<rbrakk> \<Longrightarrow> jumpF f (at_right ?x) = jumpF g (at_right ?x)

goal (1 subgoal):
 1. (\<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x)) = (\<Sum>x | jumpF g (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF g (at_right x))
[PROOF STEP]
by (auto intro: sum.cong)
[PROOF STATE]
proof (state)
this:
right f = right g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
right f = right g

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
left f = left g
right f = right g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
left f = left g
right f = right g

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
unfolding cindexE_def left_def right_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x)) = (\<Sum>x | jumpF g (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF g (at_left x))
(\<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x)) = (\<Sum>x | jumpF g (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF g (at_right x))

goal (1 subgoal):
 1. (\<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x)) - (\<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x)) = (\<Sum>x | jumpF g (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF g (at_right x)) - (\<Sum>x | jumpF g (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF g (at_left x))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
cindexE a b f = cindexE a b g

goal:
No subgoals!
[PROOF STEP]
qed