[STATEMENT]
lemma succ_ex:
  assumes "R \<in> \<R>"
  shows "succ \<R> R \<in> \<R>" (is "?G1") and "succ \<R> R \<in> Succ \<R> R" (is "?G2")
  and "\<forall> u \<in> R. \<forall> t \<ge> 0. (u \<oplus> t) \<notin> R \<longrightarrow> (\<exists> t' \<le> t. (u \<oplus> t') \<in> succ \<R> R \<and> 0 \<le> t')" (is "?G3")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ \<R> R \<in> \<R> &&& succ \<R> R \<in> Succ \<R> R &&& \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. succ \<R> R \<in> \<R>
 2. succ \<R> R \<in> Succ \<R> R
 3. \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')
[PROOF STEP]
from \<open>R \<in> \<R>\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<in> \<R>
[PROOF STEP]
obtain I r where R: "R = region X I r" "valid_region X k I r"
[PROOF STATE]
proof (prove)
using this:
R \<in> \<R>

goal (1 subgoal):
 1. (\<And>I r. \<lbrakk>R = Regions.region X I r; Regions.valid_region X k I r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<R>_def
[PROOF STATE]
proof (prove)
using this:
R \<in> {Regions.region X I r |I r. Regions.valid_region X k I r}

goal (1 subgoal):
 1. (\<And>I r. \<lbrakk>R = Regions.region X I r; Regions.valid_region X k I r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R = Regions.region X I r
Regions.valid_region X k I r

goal (3 subgoals):
 1. succ \<R> R \<in> \<R>
 2. succ \<R> R \<in> Succ \<R> R
 3. \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')
[PROOF STEP]
from region_not_empty[OF finite] R
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
R = Regions.region X I r
Regions.valid_region X k I r
[PROOF STEP]
obtain u where u: "u \<in> R"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
R = Regions.region X I r
Regions.valid_region X k I r

goal (1 subgoal):
 1. (\<And>u. u \<in> R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<in> R

goal (3 subgoals):
 1. succ \<R> R \<in> \<R>
 2. succ \<R> R \<in> Succ \<R> R
 3. \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')
[PROOF STEP]
let ?Z = "{x \<in> X . \<exists> c. I x = Const c}"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. succ \<R> R \<in> \<R>
 2. succ \<R> R \<in> Succ \<R> R
 3. \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')
[PROOF STEP]
let ?succ =
    "\<lambda> R'. R' \<noteq> R \<and> R' \<in> Succ \<R> R
     \<and> (\<forall> u \<in> R. \<forall> t \<ge> 0. (u \<oplus> t) \<notin> R \<longrightarrow> (\<exists> t' \<le> t. (u \<oplus> t') \<in> R' \<and> 0 \<le> t'))"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. succ \<R> R \<in> \<R>
 2. succ \<R> R \<in> Succ \<R> R
 3. \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')
[PROOF STEP]
consider (upper_right) "\<forall> x \<in> X. isGreater (I x)" | (intv) "\<exists> x \<in> X. \<exists> d. I x = Intv d \<and> ?Z = {}"
         | (const) "?Z \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "\<forall> x \<in> X. isGreater (I x)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; \<forall>x\<in>X. Regions.isGreater (I x)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; \<not> (\<forall>x\<in>X. Regions.isGreater (I x))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; \<not> (\<forall>x\<in>X. Regions.isGreater (I x))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "?Z = {}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; \<not> (\<forall>x\<in>X. Regions.isGreater (I x)); {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; \<not> (\<forall>x\<in>X. Regions.isGreater (I x)); {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {}\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}; \<not> thesis; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
 2. \<And>x xa c. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; \<not> thesis; x \<in> X; \<not> Regions.isGreater (I x); xa \<in> X; I xa = Regions.intv.Const c\<rbrakk> \<Longrightarrow> xa \<in> {}
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}; \<not> thesis; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
 2. \<And>x xa c. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; \<not> thesis; x \<in> X; \<not> Regions.isGreater (I x); xa \<in> X; I xa = Regions.intv.Const c\<rbrakk> \<Longrightarrow> xa \<in> {}
[PROOF STEP]
apply (case_tac "I x")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x x1. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}; \<not> thesis; x \<in> X; I x = Regions.intv.Const x1\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
 2. \<And>x x2. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}; \<not> thesis; x \<in> X; I x = Regions.intv.Intv x2\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
 3. \<And>x x3. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}; \<not> thesis; x \<in> X; I x = Regions.intv.Greater x3\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
 4. \<And>x xa c. \<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> thesis; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> thesis; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> thesis; \<not> thesis; x \<in> X; \<not> Regions.isGreater (I x); xa \<in> X; I xa = Regions.intv.Const c\<rbrakk> \<Longrightarrow> xa \<in> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> ?thesis2; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> ?thesis2; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> ?thesis2\<rbrakk> \<Longrightarrow> ?thesis2

goal (3 subgoals):
 1. succ \<R> R \<in> \<R>
 2. succ \<R> R \<in> Succ \<R> R
 3. \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> ?thesis2; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> ?thesis2; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> ?thesis2\<rbrakk> \<Longrightarrow> ?thesis2
[PROOF STEP]
have "?G1 \<and> ?G2 \<and> ?G3"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> ?thesis2; \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> ?thesis2; {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> ?thesis2\<rbrakk> \<Longrightarrow> ?thesis2

goal (1 subgoal):
 1. succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
case const
[PROOF STATE]
proof (state)
this:
{x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {}

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with upper_right_eq[OF finite R(2)]
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
{x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {}
[PROOF STEP]
have "\<not> is_upper_right R"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
{x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {}

goal (1 subgoal):
 1. \<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)
[PROOF STEP]
by (auto simp: R(1))
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
from closest_prestable_1(1,2)[OF const finite R(2)] closest_valid_1[OF const finite R(2)] R(1)
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>Regions.region X I r. \<forall>t>0. \<exists>t'\<le>t. v \<oplus> t' \<in> Regions.region X (\<lambda>x. if x \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I x else if intv_const (I x) = k x then Regions.intv.Greater (k x) else Regions.intv.Intv (intv_const (I x))) (r \<union> {(x, y). x \<in> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<and> y \<in> X \<and> intv_const (I x) < k x \<and> Regions.isIntv (if y \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I y else if intv_const (I y) = k y then Regions.intv.Greater (k y) else Regions.intv.Intv (intv_const (I y)))}) \<and> 0 \<le> t'
\<forall>v\<in>Regions.region X (\<lambda>x. if x \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I x else if intv_const (I x) = k x then Regions.intv.Greater (k x) else Regions.intv.Intv (intv_const (I x))) (r \<union> {(x, y). x \<in> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<and> y \<in> X \<and> intv_const (I x) < k x \<and> Regions.isIntv (if y \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I y else if intv_const (I y) = k y then Regions.intv.Greater (k y) else Regions.intv.Intv (intv_const (I y)))}). \<forall>t\<ge>0. v \<oplus> t \<notin> Regions.region X I r
Regions.valid_region X k (\<lambda>x. if x \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I x else if intv_const (I x) = k x then Regions.intv.Greater (k x) else Regions.intv.Intv (intv_const (I x))) (r \<union> {(x, y). x \<in> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<and> y \<in> X \<and> intv_const (I x) < k x \<and> Regions.isIntv (if y \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I y else if intv_const (I y) = k y then Regions.intv.Greater (k y) else Regions.intv.Intv (intv_const (I y)))})
R = Regions.region X I r
[PROOF STEP]
obtain R' where R':
      "\<forall> u \<in> R. \<forall> t>0. \<exists>t'\<le>t. (u \<oplus> t') \<in> R' \<and> t' \<ge> 0" "R' \<in> \<R>" "\<forall> u \<in> R'. \<forall> t\<ge>0. (u \<oplus> t) \<notin> R"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>Regions.region X I r. \<forall>t>0. \<exists>t'\<le>t. v \<oplus> t' \<in> Regions.region X (\<lambda>x. if x \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I x else if intv_const (I x) = k x then Regions.intv.Greater (k x) else Regions.intv.Intv (intv_const (I x))) (r \<union> {(x, y). x \<in> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<and> y \<in> X \<and> intv_const (I x) < k x \<and> Regions.isIntv (if y \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I y else if intv_const (I y) = k y then Regions.intv.Greater (k y) else Regions.intv.Intv (intv_const (I y)))}) \<and> 0 \<le> t'
\<forall>v\<in>Regions.region X (\<lambda>x. if x \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I x else if intv_const (I x) = k x then Regions.intv.Greater (k x) else Regions.intv.Intv (intv_const (I x))) (r \<union> {(x, y). x \<in> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<and> y \<in> X \<and> intv_const (I x) < k x \<and> Regions.isIntv (if y \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I y else if intv_const (I y) = k y then Regions.intv.Greater (k y) else Regions.intv.Intv (intv_const (I y)))}). \<forall>t\<ge>0. v \<oplus> t \<notin> Regions.region X I r
Regions.valid_region X k (\<lambda>x. if x \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I x else if intv_const (I x) = k x then Regions.intv.Greater (k x) else Regions.intv.Intv (intv_const (I x))) (r \<union> {(x, y). x \<in> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<and> y \<in> X \<and> intv_const (I x) < k x \<and> Regions.isIntv (if y \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I y else if intv_const (I y) = k y then Regions.intv.Greater (k y) else Regions.intv.Intv (intv_const (I y)))})
R = Regions.region X I r

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'; R' \<in> \<R>; \<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<R>_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>Regions.region X I r. \<forall>t>0. \<exists>t'\<le>t. v \<oplus> t' \<in> Regions.region X (\<lambda>x. if x \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I x else if intv_const (I x) = k x then Regions.intv.Greater (k x) else Regions.intv.Intv (intv_const (I x))) (r \<union> {(x, y). x \<in> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<and> y \<in> X \<and> intv_const (I x) < k x \<and> Regions.isIntv (if y \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I y else if intv_const (I y) = k y then Regions.intv.Greater (k y) else Regions.intv.Intv (intv_const (I y)))}) \<and> 0 \<le> t'
\<forall>v\<in>Regions.region X (\<lambda>x. if x \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I x else if intv_const (I x) = k x then Regions.intv.Greater (k x) else Regions.intv.Intv (intv_const (I x))) (r \<union> {(x, y). x \<in> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<and> y \<in> X \<and> intv_const (I x) < k x \<and> Regions.isIntv (if y \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I y else if intv_const (I y) = k y then Regions.intv.Greater (k y) else Regions.intv.Intv (intv_const (I y)))}). \<forall>t\<ge>0. v \<oplus> t \<notin> Regions.region X I r
Regions.valid_region X k (\<lambda>x. if x \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I x else if intv_const (I x) = k x then Regions.intv.Greater (k x) else Regions.intv.Intv (intv_const (I x))) (r \<union> {(x, y). x \<in> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<and> y \<in> X \<and> intv_const (I x) < k x \<and> Regions.isIntv (if y \<notin> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} then I y else if intv_const (I y) = k y then Regions.intv.Greater (k y) else Regions.intv.Intv (intv_const (I y)))})
R = Regions.region X I r

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'; R' \<in> {Regions.region X I r |I r. Regions.valid_region X k I r}; \<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with region_not_empty[OF finite]
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
[PROOF STEP]
obtain u' where "u' \<in> R'"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R

goal (1 subgoal):
 1. (\<And>u'. u' \<in> R' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<R>_def
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'
R' \<in> {Regions.region X I r |I r. Regions.valid_region X k I r}
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R

goal (1 subgoal):
 1. (\<And>u'. u' \<in> R' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' \<in> R'

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with R'(3)
[PROOF STATE]
proof (chain)
picking this:
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
u' \<in> R'
[PROOF STEP]
have neq: "R' \<noteq> R"
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
u' \<in> R'

goal (1 subgoal):
 1. R' \<noteq> R
[PROOF STEP]
by (fastforce simp: cval_add_def)
[PROOF STATE]
proof (state)
this:
R' \<noteq> R

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
obtain t:: real where "t > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. 0 < t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: that[of 1])
[PROOF STATE]
proof (state)
this:
0 < t

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with R'(1,2) \<open>u \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'
R' \<in> \<R>
u \<in> R
0 < t
[PROOF STEP]
obtain t where "t \<ge> 0" "u \<oplus> t \<in> R'"
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'
R' \<in> \<R>
u \<in> R
0 < t

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>0 \<le> t; u \<oplus> t \<in> R'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> t
u \<oplus> t \<in> R'

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with \<open>R \<in> \<R>\<close> \<open>R' \<in> \<R>\<close> \<open>u \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<in> \<R>
R' \<in> \<R>
u \<in> R
0 \<le> t
u \<oplus> t \<in> R'
[PROOF STEP]
have "R' \<in> Succ \<R> R"
[PROOF STATE]
proof (prove)
using this:
R \<in> \<R>
R' \<in> \<R>
u \<in> R
0 \<le> t
u \<oplus> t \<in> R'

goal (1 subgoal):
 1. R' \<in> Succ \<R> R
[PROOF STEP]
by (intro SuccI3)
[PROOF STATE]
proof (state)
this:
R' \<in> Succ \<R> R

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
R' \<in> Succ \<R> R

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
have "(\<forall> u \<in> R. \<forall> t \<ge> 0. (u \<oplus> t) \<notin> R \<longrightarrow> (\<exists> t' \<le> t. (u \<oplus> t') \<in> R' \<and> 0 \<le> t'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
[PROOF STEP]
using R'(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'

goal (1 subgoal):
 1. \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
[PROOF STEP]
unfolding cval_add_def
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. (\<lambda>x. u x + t') \<in> R' \<and> 0 \<le> t'

goal (1 subgoal):
 1. \<forall>u\<in>R. \<forall>t\<ge>0. (\<lambda>x. u x + t) \<notin> R \<longrightarrow> (\<exists>t'\<le>t. (\<lambda>x. u x + t') \<in> R' \<and> 0 \<le> t')
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u t. \<lbrakk>\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. (\<lambda>x. u x + t') \<in> R' \<and> 0 \<le> t'; u \<in> R; 0 \<le> t; (\<lambda>x. u x + t) \<notin> R\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. (\<lambda>x. u x + t') \<in> R' \<and> 0 \<le> t'
[PROOF STEP]
subgoal for u t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. (\<lambda>x. u x + t') \<in> R' \<and> 0 \<le> t'; u \<in> R; 0 \<le> t; (\<lambda>x. u x + t) \<notin> R\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. (\<lambda>x. u x + t') \<in> R' \<and> 0 \<le> t'
[PROOF STEP]
by (cases "t = 0") auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R' \<in> Succ \<R> R
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
[PROOF STEP]
have *: "?succ R'"
[PROOF STATE]
proof (prove)
using this:
R' \<in> Succ \<R> R
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')

goal (1 subgoal):
 1. R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
[PROOF STEP]
using neq
[PROOF STATE]
proof (prove)
using this:
R' \<in> Succ \<R> R
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
R' \<noteq> R

goal (1 subgoal):
 1. R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
have "succ \<R> R = R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ \<R> R = R'
[PROOF STEP]
unfolding succ_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R then R else THE R'. R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))) = R'
[PROOF STEP]
proof (simp add: \<open>\<not> is_upper_right R\<close>, intro the_equality, rule *, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
case prems: (1 R'')
[PROOF STATE]
proof (state)
this:
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))
[PROOF STEP]
obtain t' u' where R'':
        "R'' \<in> \<R>" "R'' \<noteq> R" "t' \<ge> 0" "R'' = [u' \<oplus> t']\<^sub>\<R>" "u' \<in> R"
[PROOF STATE]
proof (prove)
using this:
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))

goal (1 subgoal):
 1. (\<And>t' u'. \<lbrakk>R'' \<in> \<R>; R'' \<noteq> R; 0 \<le> t'; R'' = [u' \<oplus> t']\<^sub>\<R>; u' \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R'(1)
[PROOF STATE]
proof (prove)
using this:
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'

goal (1 subgoal):
 1. (\<And>t' u'. \<lbrakk>R'' \<in> \<R>; R'' \<noteq> R; 0 \<le> t'; R'' = [u' \<oplus> t']\<^sub>\<R>; u' \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
R'' \<in> \<R>
[PROOF STEP]
obtain I r where R''2:
        "R'' = region X I r" "valid_region X k I r"
[PROOF STATE]
proof (prove)
using this:
R'' \<in> \<R>

goal (1 subgoal):
 1. (\<And>I r. \<lbrakk>R'' = Regions.region X I r; Regions.valid_region X k I r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: \<R>_def)
[PROOF STATE]
proof (state)
this:
R'' = Regions.region X I r
Regions.valid_region X k I r

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
from R''
[PROOF STATE]
proof (chain)
picking this:
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R
[PROOF STEP]
have "u' \<oplus> t' \<notin> R"
[PROOF STATE]
proof (prove)
using this:
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R

goal (1 subgoal):
 1. u' \<oplus> t' \<notin> R
[PROOF STEP]
using assms region_unique_spec
[PROOF STATE]
proof (prove)
using this:
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R
R \<in> \<R>
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R

goal (1 subgoal):
 1. u' \<oplus> t' \<notin> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' \<oplus> t' \<notin> R

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
with * \<open>t' \<ge> 0\<close> \<open>u' \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
0 \<le> t'
u' \<in> R
u' \<oplus> t' \<notin> R
[PROOF STEP]
obtain t'' where t'': "t'' \<le> t'" "u' \<oplus> t'' \<in> R'" "t'' \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
0 \<le> t'
u' \<in> R
u' \<oplus> t' \<notin> R

goal (1 subgoal):
 1. (\<And>t''. \<lbrakk>t'' \<le> t'; u' \<oplus> t'' \<in> R'; 0 \<le> t''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
from this(2) neq
[PROOF STATE]
proof (chain)
picking this:
u' \<oplus> t'' \<in> R'
R' \<noteq> R
[PROOF STEP]
have "u' \<oplus> t'' \<notin> R"
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t'' \<in> R'
R' \<noteq> R

goal (1 subgoal):
 1. u' \<oplus> t'' \<notin> R
[PROOF STEP]
using R'(2) assms region_unique_spec
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t'' \<in> R'
R' \<noteq> R
R' \<in> \<R>
R \<in> \<R>
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R

goal (1 subgoal):
 1. u' \<oplus> t'' \<notin> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' \<oplus> t'' \<notin> R

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
with t'' prems \<open>u' \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))
u' \<in> R
u' \<oplus> t'' \<notin> R
[PROOF STEP]
obtain t''' where t''':
        "t''' \<le> t''" "u' \<oplus> t''' \<in> R''" "t''' \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))
u' \<in> R
u' \<oplus> t'' \<notin> R

goal (1 subgoal):
 1. (\<And>t'''. \<lbrakk>t''' \<le> t''; u' \<oplus> t''' \<in> R''; 0 \<le> t'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t''' \<le> t''
u' \<oplus> t''' \<in> R''
0 \<le> t'''

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
with region_continuous[OF R''2(2) _ _ t'''(2)[unfolded R''2(1)], of "t'' - t'''" "t' - t'''"]
           t'' R'' regions_closed'_spec[OF \<open>R \<in> \<R>\<close> R''(5,3)]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 \<le> t'' - t'''; t'' - t''' \<le> t' - t'''; (u' \<oplus> t''') \<oplus> t' - t''' \<in> Regions.region X I r\<rbrakk> \<Longrightarrow> (u' \<oplus> t''') \<oplus> t'' - t''' \<in> Regions.region X I r
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R
u' \<oplus> t' \<in> [u' \<oplus> t']\<^sub>\<R>
t''' \<le> t''
u' \<oplus> t''' \<in> R''
0 \<le> t'''
[PROOF STEP]
have "u' \<oplus> t'' \<in> R''"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> t'' - t'''; t'' - t''' \<le> t' - t'''; (u' \<oplus> t''') \<oplus> t' - t''' \<in> Regions.region X I r\<rbrakk> \<Longrightarrow> (u' \<oplus> t''') \<oplus> t'' - t''' \<in> Regions.region X I r
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R
u' \<oplus> t' \<in> [u' \<oplus> t']\<^sub>\<R>
t''' \<le> t''
u' \<oplus> t''' \<in> R''
0 \<le> t'''

goal (1 subgoal):
 1. u' \<oplus> t'' \<in> R''
[PROOF STEP]
by (auto simp: R''2 cval_add_def)
[PROOF STATE]
proof (state)
this:
u' \<oplus> t'' \<in> R''

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
with t''(2)
[PROOF STATE]
proof (chain)
picking this:
u' \<oplus> t'' \<in> R'
u' \<oplus> t'' \<in> R''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t'' \<in> R'
u' \<oplus> t'' \<in> R''

goal (1 subgoal):
 1. R'' = R'
[PROOF STEP]
using R''(1) R'(2) region_unique_spec
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t'' \<in> R'
u' \<oplus> t'' \<in> R''
R'' \<in> \<R>
R' \<in> \<R>
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
succ \<R> R = R'

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 3. {x \<in> X. \<exists>c. I x = Regions.intv.Const c} \<noteq> {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with R' *
[PROOF STATE]
proof (chain)
picking this:
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
succ \<R> R = R'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R. \<forall>t>0. \<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
succ \<R> R = R'

goal (1 subgoal):
 1. succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
case intv
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}
[PROOF STEP]
have *: "\<forall>x\<in>X. \<not> Regions.isConst (I x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}

goal (1 subgoal):
 1. \<forall>x\<in>X. \<not> Regions.isConst (I x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. \<not> Regions.isConst (I x)

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
let ?X\<^sub>0 = "{x \<in> X. isIntv (I x)}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
let ?M = "{x \<in> ?X\<^sub>0. \<forall>y\<in>?X\<^sub>0. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
from intv
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}
[PROOF STEP]
obtain x c where x: "x \<in> X" "\<not> isGreater (I x)" and c: "I x = Intv c"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {}

goal (1 subgoal):
 1. (\<And>x c. \<lbrakk>x \<in> X; \<not> Regions.isGreater (I x); I x = Regions.intv.Intv c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
\<not> Regions.isGreater (I x)
I x = Regions.intv.Intv c

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with \<open>x \<in> X\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
x \<in> X
\<not> Regions.isGreater (I x)
I x = Regions.intv.Intv c
[PROOF STEP]
have "?X\<^sub>0 \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
x \<in> X
\<not> Regions.isGreater (I x)
I x = Regions.intv.Intv c

goal (1 subgoal):
 1. {x \<in> X. Regions.isIntv (I x)} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> X. Regions.isIntv (I x)} \<noteq> {}

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
have "?X\<^sub>0 = {x \<in> X. \<exists>d. I x = Intv d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> X. Regions.isIntv (I x)} = {x \<in> X. \<exists>d. I x = Regions.intv.Intv d}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> X. Regions.isIntv (I x)} = {x \<in> X. \<exists>d. I x = Regions.intv.Intv d}

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with R(2)
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_region X k I r
{x \<in> X. Regions.isIntv (I x)} = {x \<in> X. \<exists>d. I x = Regions.intv.Intv d}
[PROOF STEP]
have r: "total_on ?X\<^sub>0 r" "trans r"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X k I r
{x \<in> X. Regions.isIntv (I x)} = {x \<in> X. \<exists>d. I x = Regions.intv.Intv d}

goal (1 subgoal):
 1. total_on {x \<in> X. Regions.isIntv (I x)} r &&& trans r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
total_on {x \<in> X. Regions.isIntv (I x)} r
trans r

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
from total_finite_trans_max[OF \<open>?X\<^sub>0 \<noteq> {}\<close> _ this] finite
[PROOF STATE]
proof (chain)
picking this:
finite {x \<in> X. Regions.isIntv (I x)} \<Longrightarrow> \<exists>x\<in>{x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. x \<noteq> y \<longrightarrow> (y, x) \<in> r
finite X
[PROOF STEP]
obtain x' where x': "x' \<in> ?X\<^sub>0" "\<forall> y \<in> ?X\<^sub>0. x' \<noteq> y \<longrightarrow> (y, x') \<in> r"
[PROOF STATE]
proof (prove)
using this:
finite {x \<in> X. Regions.isIntv (I x)} \<Longrightarrow> \<exists>x\<in>{x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. x \<noteq> y \<longrightarrow> (y, x) \<in> r
finite X

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> {x \<in> X. Regions.isIntv (I x)}; \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. x' \<noteq> y \<longrightarrow> (y, x') \<in> r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x' \<in> {x \<in> X. Regions.isIntv (I x)}
\<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. x' \<noteq> y \<longrightarrow> (y, x') \<in> r

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. x' \<noteq> y \<longrightarrow> (y, x') \<in> r
[PROOF STEP]
have "\<forall>y\<in>?X\<^sub>0. (x', y) \<in> r \<longrightarrow> (y, x') \<in> r"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. x' \<noteq> y \<longrightarrow> (y, x') \<in> r

goal (1 subgoal):
 1. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x', y) \<in> r \<longrightarrow> (y, x') \<in> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x', y) \<in> r \<longrightarrow> (y, x') \<in> r

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with x'(1)
[PROOF STATE]
proof (chain)
picking this:
x' \<in> {x \<in> X. Regions.isIntv (I x)}
\<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x', y) \<in> r \<longrightarrow> (y, x') \<in> r
[PROOF STEP]
have **: "?M \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
x' \<in> {x \<in> X. Regions.isIntv (I x)}
\<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x', y) \<in> r \<longrightarrow> (y, x') \<in> r

goal (1 subgoal):
 1. {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<noteq> {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<noteq> {}

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with upper_right_eq[OF finite R(2)]
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
{x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<noteq> {}
[PROOF STEP]
have "\<not> is_upper_right R"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
{x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<noteq> {}

goal (1 subgoal):
 1. \<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)
[PROOF STEP]
by (auto simp: R(1))
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
from closest_prestable_2(1,2)[OF * finite R(2) **] closest_valid_2[OF * finite R(2) **] R(1)
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>Regions.region X I r. \<forall>t\<ge>0. v \<oplus> t \<notin> Regions.region X I r \<longrightarrow> (\<exists>t'\<le>t. v \<oplus> t' \<in> Regions.region X (\<lambda>x. if x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} then I x else Regions.intv.Const (intv_const (I x) + 1)) {(x, y). (x, y) \<in> r \<and> x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<and> y \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}} \<and> 0 \<le> t')
\<forall>v\<in>Regions.region X (\<lambda>x. if x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} then I x else Regions.intv.Const (intv_const (I x) + 1)) {(x, y). (x, y) \<in> r \<and> x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<and> y \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}}. \<forall>t\<ge>0. v \<oplus> t \<notin> Regions.region X I r
Regions.valid_region X k (\<lambda>x. if x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} then I x else Regions.intv.Const (intv_const (I x) + 1)) {(x, y). (x, y) \<in> r \<and> x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<and> y \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}}
R = Regions.region X I r
[PROOF STEP]
obtain R' where R':
      "(\<forall> u \<in> R. \<forall> t \<ge> 0. (u \<oplus> t) \<notin> R \<longrightarrow> (\<exists> t' \<le> t. (u \<oplus> t') \<in> R' \<and> 0 \<le> t'))" "R' \<in> \<R>"
      "\<forall> u \<in> R'. \<forall> t\<ge>0. (u \<oplus> t) \<notin> R"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>Regions.region X I r. \<forall>t\<ge>0. v \<oplus> t \<notin> Regions.region X I r \<longrightarrow> (\<exists>t'\<le>t. v \<oplus> t' \<in> Regions.region X (\<lambda>x. if x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} then I x else Regions.intv.Const (intv_const (I x) + 1)) {(x, y). (x, y) \<in> r \<and> x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<and> y \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}} \<and> 0 \<le> t')
\<forall>v\<in>Regions.region X (\<lambda>x. if x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} then I x else Regions.intv.Const (intv_const (I x) + 1)) {(x, y). (x, y) \<in> r \<and> x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<and> y \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}}. \<forall>t\<ge>0. v \<oplus> t \<notin> Regions.region X I r
Regions.valid_region X k (\<lambda>x. if x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} then I x else Regions.intv.Const (intv_const (I x) + 1)) {(x, y). (x, y) \<in> r \<and> x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<and> y \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}}
R = Regions.region X I r

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'); R' \<in> \<R>; \<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<R>_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>Regions.region X I r. \<forall>t\<ge>0. v \<oplus> t \<notin> Regions.region X I r \<longrightarrow> (\<exists>t'\<le>t. v \<oplus> t' \<in> Regions.region X (\<lambda>x. if x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} then I x else Regions.intv.Const (intv_const (I x) + 1)) {(x, y). (x, y) \<in> r \<and> x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<and> y \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}} \<and> 0 \<le> t')
\<forall>v\<in>Regions.region X (\<lambda>x. if x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} then I x else Regions.intv.Const (intv_const (I x) + 1)) {(x, y). (x, y) \<in> r \<and> x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<and> y \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}}. \<forall>t\<ge>0. v \<oplus> t \<notin> Regions.region X I r
Regions.valid_region X k (\<lambda>x. if x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} then I x else Regions.intv.Const (intv_const (I x) + 1)) {(x, y). (x, y) \<in> r \<and> x \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r} \<and> y \<notin> {x \<in> {x \<in> X. Regions.isIntv (I x)}. \<forall>y\<in>{x \<in> X. Regions.isIntv (I x)}. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r}}
R = Regions.region X I r

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'); R' \<in> {Regions.region X I r |I r. Regions.valid_region X k I r}; \<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with region_not_empty[OF finite]
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
[PROOF STEP]
obtain u' where "u' \<in> R'"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R

goal (1 subgoal):
 1. (\<And>u'. u' \<in> R' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<R>_def
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
R' \<in> {Regions.region X I r |I r. Regions.valid_region X k I r}
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R

goal (1 subgoal):
 1. (\<And>u'. u' \<in> R' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' \<in> R'

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with R'(3)
[PROOF STATE]
proof (chain)
picking this:
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
u' \<in> R'
[PROOF STEP]
have neq: "R' \<noteq> R"
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
u' \<in> R'

goal (1 subgoal):
 1. R' \<noteq> R
[PROOF STEP]
by (fastforce simp: cval_add_def)
[PROOF STATE]
proof (state)
this:
R' \<noteq> R

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
from bounded_region[OF finite R(2), folded R(1), OF \<open>\<not> is_upper_right R\<close> u]
[PROOF STATE]
proof (chain)
picking this:
u \<oplus> 1 \<notin> R
[PROOF STEP]
have
      "u \<oplus> (1 :: t) \<notin> R" "(1 :: t) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
u \<oplus> 1 \<notin> R

goal (1 subgoal):
 1. u \<oplus> 1 \<notin> R &&& 0 \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<oplus> 1 \<notin> R
0 \<le> 1

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with R'(1) u
[PROOF STATE]
proof (chain)
picking this:
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
u \<in> R
u \<oplus> 1 \<notin> R
0 \<le> 1
[PROOF STEP]
obtain t' where "t' \<le> (1 :: t)" "(u \<oplus> t') \<in> R'" "0 \<le> t'"
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
u \<in> R
u \<oplus> 1 \<notin> R
0 \<le> 1

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<le> 1; u \<oplus> t' \<in> R'; 0 \<le> t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
t' \<le> 1
u \<oplus> t' \<in> R'
0 \<le> t'

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with \<open>R \<in> \<R>\<close> \<open>R' \<in> \<R>\<close> \<open>u \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<in> \<R>
R' \<in> \<R>
u \<in> R
t' \<le> 1
u \<oplus> t' \<in> R'
0 \<le> t'
[PROOF STEP]
have "R' \<in> Succ \<R> R"
[PROOF STATE]
proof (prove)
using this:
R \<in> \<R>
R' \<in> \<R>
u \<in> R
t' \<le> 1
u \<oplus> t' \<in> R'
0 \<le> t'

goal (1 subgoal):
 1. R' \<in> Succ \<R> R
[PROOF STEP]
by (intro SuccI3)
[PROOF STATE]
proof (state)
this:
R' \<in> Succ \<R> R

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with R'(1) neq
[PROOF STATE]
proof (chain)
picking this:
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
R' \<noteq> R
R' \<in> Succ \<R> R
[PROOF STEP]
have *: "?succ R'"
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
R' \<noteq> R
R' \<in> Succ \<R> R

goal (1 subgoal):
 1. R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
have "succ \<R> R = R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ \<R> R = R'
[PROOF STEP]
unfolding succ_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R then R else THE R'. R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))) = R'
[PROOF STEP]
proof (simp add: \<open>\<not> is_upper_right R\<close>, intro the_equality, rule *, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
case prems: (1 R'')
[PROOF STATE]
proof (state)
this:
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))
[PROOF STEP]
obtain t' u' where R'':
        "R'' \<in> \<R>" "R'' \<noteq> R" "t' \<ge> 0" "R'' = [u' \<oplus> t']\<^sub>\<R>" "u' \<in> R"
[PROOF STATE]
proof (prove)
using this:
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))

goal (1 subgoal):
 1. (\<And>t' u'. \<lbrakk>R'' \<in> \<R>; R'' \<noteq> R; 0 \<le> t'; R'' = [u' \<oplus> t']\<^sub>\<R>; u' \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R'(1)
[PROOF STATE]
proof (prove)
using this:
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')

goal (1 subgoal):
 1. (\<And>t' u'. \<lbrakk>R'' \<in> \<R>; R'' \<noteq> R; 0 \<le> t'; R'' = [u' \<oplus> t']\<^sub>\<R>; u' \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
R'' \<in> \<R>
[PROOF STEP]
obtain I r where R''2:
        "R'' = region X I r" "valid_region X k I r"
[PROOF STATE]
proof (prove)
using this:
R'' \<in> \<R>

goal (1 subgoal):
 1. (\<And>I r. \<lbrakk>R'' = Regions.region X I r; Regions.valid_region X k I r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: \<R>_def)
[PROOF STATE]
proof (state)
this:
R'' = Regions.region X I r
Regions.valid_region X k I r

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
from R''
[PROOF STATE]
proof (chain)
picking this:
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R
[PROOF STEP]
have "u' \<oplus> t' \<notin> R"
[PROOF STATE]
proof (prove)
using this:
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R

goal (1 subgoal):
 1. u' \<oplus> t' \<notin> R
[PROOF STEP]
using assms region_unique_spec
[PROOF STATE]
proof (prove)
using this:
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R
R \<in> \<R>
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R

goal (1 subgoal):
 1. u' \<oplus> t' \<notin> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' \<oplus> t' \<notin> R

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
with * \<open>t' \<ge> 0\<close> \<open>u' \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
0 \<le> t'
u' \<in> R
u' \<oplus> t' \<notin> R
[PROOF STEP]
obtain t'' where t'': "t'' \<le> t'" "u' \<oplus> t'' \<in> R'" "t'' \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
0 \<le> t'
u' \<in> R
u' \<oplus> t' \<notin> R

goal (1 subgoal):
 1. (\<And>t''. \<lbrakk>t'' \<le> t'; u' \<oplus> t'' \<in> R'; 0 \<le> t''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
from this(2) neq
[PROOF STATE]
proof (chain)
picking this:
u' \<oplus> t'' \<in> R'
R' \<noteq> R
[PROOF STEP]
have "u' \<oplus> t'' \<notin> R"
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t'' \<in> R'
R' \<noteq> R

goal (1 subgoal):
 1. u' \<oplus> t'' \<notin> R
[PROOF STEP]
using R'(2) assms region_unique_spec
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t'' \<in> R'
R' \<noteq> R
R' \<in> \<R>
R \<in> \<R>
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R

goal (1 subgoal):
 1. u' \<oplus> t'' \<notin> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' \<oplus> t'' \<notin> R

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
with t'' prems \<open>u' \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))
u' \<in> R
u' \<oplus> t'' \<notin> R
[PROOF STEP]
obtain t''' where t''':
        "t''' \<le> t''" "u' \<oplus> t''' \<in> R''" "t''' \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''
R'' \<noteq> R \<and> R'' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'' \<and> 0 \<le> t'))
u' \<in> R
u' \<oplus> t'' \<notin> R

goal (1 subgoal):
 1. (\<And>t'''. \<lbrakk>t''' \<le> t''; u' \<oplus> t''' \<in> R''; 0 \<le> t'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t''' \<le> t''
u' \<oplus> t''' \<in> R''
0 \<le> t'''

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
with region_continuous[OF R''2(2) _ _ t'''(2)[unfolded R''2(1)], of "t'' - t'''" "t' - t'''"]
           t'' R'' regions_closed'_spec[OF \<open>R \<in> \<R>\<close> R''(5,3)]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 \<le> t'' - t'''; t'' - t''' \<le> t' - t'''; (u' \<oplus> t''') \<oplus> t' - t''' \<in> Regions.region X I r\<rbrakk> \<Longrightarrow> (u' \<oplus> t''') \<oplus> t'' - t''' \<in> Regions.region X I r
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R
u' \<oplus> t' \<in> [u' \<oplus> t']\<^sub>\<R>
t''' \<le> t''
u' \<oplus> t''' \<in> R''
0 \<le> t'''
[PROOF STEP]
have "u' \<oplus> t'' \<in> R''"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> t'' - t'''; t'' - t''' \<le> t' - t'''; (u' \<oplus> t''') \<oplus> t' - t''' \<in> Regions.region X I r\<rbrakk> \<Longrightarrow> (u' \<oplus> t''') \<oplus> t'' - t''' \<in> Regions.region X I r
t'' \<le> t'
u' \<oplus> t'' \<in> R'
0 \<le> t''
R'' \<in> \<R>
R'' \<noteq> R
0 \<le> t'
R'' = [u' \<oplus> t']\<^sub>\<R>
u' \<in> R
u' \<oplus> t' \<in> [u' \<oplus> t']\<^sub>\<R>
t''' \<le> t''
u' \<oplus> t''' \<in> R''
0 \<le> t'''

goal (1 subgoal):
 1. u' \<oplus> t'' \<in> R''
[PROOF STEP]
by (auto simp: cval_add_def R''2)
[PROOF STATE]
proof (state)
this:
u' \<oplus> t'' \<in> R''

goal (1 subgoal):
 1. \<And>R'a. R'a \<noteq> R \<and> R'a \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R'a \<and> 0 \<le> t')) \<Longrightarrow> R'a = R'
[PROOF STEP]
with t''(2)
[PROOF STATE]
proof (chain)
picking this:
u' \<oplus> t'' \<in> R'
u' \<oplus> t'' \<in> R''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t'' \<in> R'
u' \<oplus> t'' \<in> R''

goal (1 subgoal):
 1. R'' = R'
[PROOF STEP]
using R''(1) R'(2) region_unique_spec
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t'' \<in> R'
u' \<oplus> t'' \<in> R''
R'' \<in> \<R>
R' \<in> \<R>
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
succ \<R> R = R'

goal (2 subgoals):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
 2. \<exists>x\<in>X. \<exists>d. I x = Regions.intv.Intv d \<and> {x \<in> X. \<exists>c. I x = Regions.intv.Const c} = {} \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with R' *
[PROOF STATE]
proof (chain)
picking this:
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
succ \<R> R = R'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t')
R' \<in> \<R>
\<forall>u\<in>R'. \<forall>t\<ge>0. u \<oplus> t \<notin> R
R' \<noteq> R \<and> R' \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> R' \<and> 0 \<le> t'))
succ \<R> R = R'

goal (1 subgoal):
 1. succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))

goal (1 subgoal):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
case upper_right
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. Regions.isGreater (I x)

goal (1 subgoal):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with upper_right_eq[OF finite R(2)]
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
\<forall>x\<in>X. Regions.isGreater (I x)
[PROOF STEP]
have "succ \<R> R = R"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
\<forall>x\<in>X. Regions.isGreater (I x)

goal (1 subgoal):
 1. succ \<R> R = R
[PROOF STEP]
by (auto simp: R succ_def)
[PROOF STATE]
proof (state)
this:
succ \<R> R = R

goal (1 subgoal):
 1. \<forall>x\<in>X. Regions.isGreater (I x) \<Longrightarrow> succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
with \<open>R \<in> \<R>\<close> u
[PROOF STATE]
proof (chain)
picking this:
R \<in> \<R>
u \<in> R
succ \<R> R = R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R \<in> \<R>
u \<in> R
succ \<R> R = R

goal (1 subgoal):
 1. succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
by (fastforce simp: cval_add_def intro: SuccI3)
[PROOF STATE]
proof (state)
this:
succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))

goal (3 subgoals):
 1. succ \<R> R \<in> \<R>
 2. succ \<R> R \<in> Succ \<R> R
 3. \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))
[PROOF STEP]
show ?G1 ?G2 ?G3
[PROOF STATE]
proof (prove)
using this:
succ \<R> R \<in> \<R> \<and> succ \<R> R \<in> Succ \<R> R \<and> (\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t'))

goal (1 subgoal):
 1. succ \<R> R \<in> \<R> &&& succ \<R> R \<in> Succ \<R> R &&& \<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succ \<R> R \<in> \<R>
succ \<R> R \<in> Succ \<R> R
\<forall>u\<in>R. \<forall>t\<ge>0. u \<oplus> t \<notin> R \<longrightarrow> (\<exists>t'\<le>t. u \<oplus> t' \<in> succ \<R> R \<and> 0 \<le> t')

goal:
No subgoals!
[PROOF STEP]
qed