[STATEMENT]
lemma delayedR_correct:
  fixes I r
  defines "R' \<equiv> region \<X> I r"
  assumes "u \<in> R" "R \<in> \<R>" "valid_region \<X> k I r" "\<forall> c \<in> \<X>. \<not> isConst (I c)" "R' \<in> Succ \<R> R"
  shows
    "delayedR R' u \<in> R'"
    "\<exists> t \<ge> 0. delayedR R' u = u \<oplus> t
            \<and> t \<ge> (1 - Max ({frac (u c) | c. c \<in> \<X> \<and> isIntv (I c)} \<union> {0})) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delayedR R' u \<in> R' &&& \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
let ?u = "SOME u. u \<in> R"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
let ?I = "SOME I. \<exists> r. valid_region \<X> k I r \<and> R' = region \<X> I r"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
let ?S = "{frac (u c) | c. c \<in> \<X> \<and> isIntv (I c)}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
let ?m = "1 - Max (?S \<union> {0})"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
let ?t = "SOME t. u \<oplus> t \<in> R' \<and> t \<ge> ?m / 2"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
have "Max (?S \<union> {0}) \<ge> 0" "?m \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) &&& 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1
[PROOF STEP]
using finite(1)
[PROOF STATE]
proof (prove)
using this:
finite \<X>

goal (1 subgoal):
 1. 0 \<le> Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) &&& 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1

goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
have "Max (?S \<union> {0}) \<in> ?S \<union> {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<in> {frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}
[PROOF STEP]
using finite(1)
[PROOF STATE]
proof (prove)
using this:
finite \<X>

goal (1 subgoal):
 1. Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<in> {frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}
[PROOF STEP]
by - (rule Max_in; auto)
[PROOF STATE]
proof (state)
this:
Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<in> {frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}

goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
with frac_lt_1
[PROOF STATE]
proof (chain)
picking this:
frac ?x < (1::?'a)
Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<in> {frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}
[PROOF STEP]
have "Max (?S \<union> {0}) \<le> 1" "?m \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
frac ?x < (1::?'a)
Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<in> {frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}

goal (1 subgoal):
 1. Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1 &&& 0 \<le> 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1
0 \<le> 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})

goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
from assms(3, 6) \<open>u \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<in> \<R>
R' \<in> Succ \<R> R
u \<in> R
[PROOF STEP]
obtain t where t:
    "u \<oplus> t \<in> R'" "t \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
R \<in> \<R>
R' \<in> Succ \<R> R
u \<in> R

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

goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
have I_cong: "\<forall> c \<in> \<X>. I' c = I c" if "valid_region \<X> k I' r'" "R' = region \<X> I' r'" for I' r'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>\<X>. I' c = I c
[PROOF STEP]
using valid_regions_intv_distinct assms(4) t(1) that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Regions.valid_region ?X k ?I ?r; Regions.valid_region ?X k ?I' ?r'; ?u \<in> Regions.region ?X ?I ?r; ?u \<in> Regions.region ?X ?I' ?r'; ?x \<in> ?X\<rbrakk> \<Longrightarrow> ?I ?x = ?I' ?x
Regions.valid_region \<X> k I r
u \<oplus> t \<in> R'
Regions.valid_region \<X> k I' r'
R' = Regions.region \<X> I' r'

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. I' c = I c
[PROOF STEP]
unfolding R'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Regions.valid_region ?X k ?I ?r; Regions.valid_region ?X k ?I' ?r'; ?u \<in> Regions.region ?X ?I ?r; ?u \<in> Regions.region ?X ?I' ?r'; ?x \<in> ?X\<rbrakk> \<Longrightarrow> ?I ?x = ?I' ?x
Regions.valid_region \<X> k I r
u \<oplus> t \<in> Regions.region \<X> I r
Regions.valid_region \<X> k I' r'
Regions.region \<X> I r = Regions.region \<X> I' r'

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

goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
have I_cong: "?I c = I c" if "c \<in> \<X>" for c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) c = I c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) c = I c
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
R' \<equiv> Regions.region \<X> I r
u \<in> R
R \<in> \<R>
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
R' \<in> Succ \<R> R
[PROOF STEP]
have
      "\<exists> r. valid_region \<X> k ?I r \<and> R' = region \<X> ?I r"
[PROOF STATE]
proof (prove)
using this:
R' \<equiv> Regions.region \<X> I r
u \<in> R
R \<in> \<R>
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
R' \<in> Succ \<R> R

goal (1 subgoal):
 1. \<exists>r. Regions.valid_region \<X> k (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) r \<and> R' = Regions.region \<X> (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) r
[PROOF STEP]
by - (rule someI[where P = "\<lambda> I. \<exists> r. valid_region \<X> k I r \<and> R' = region \<X> I r"]; auto)
[PROOF STATE]
proof (state)
this:
\<exists>r. Regions.valid_region \<X> k (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) r \<and> R' = Regions.region \<X> (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) r

goal (1 subgoal):
 1. (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) c = I c
[PROOF STEP]
with I_cong that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Regions.valid_region \<X> k ?I'5 ?r'5; R' = Regions.region \<X> ?I'5 ?r'5\<rbrakk> \<Longrightarrow> \<forall>c\<in>\<X>. ?I'5 c = I c
c \<in> \<X>
\<exists>r. Regions.valid_region \<X> k (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) r \<and> R' = Regions.region \<X> (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Regions.valid_region \<X> k ?I'5 ?r'5; R' = Regions.region \<X> ?I'5 ?r'5\<rbrakk> \<Longrightarrow> \<forall>c\<in>\<X>. ?I'5 c = I c
c \<in> \<X>
\<exists>r. Regions.valid_region \<X> k (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) r \<and> R' = Regions.region \<X> (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) r

goal (1 subgoal):
 1. (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) c = I c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) c = I c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?c5 \<in> \<X> \<Longrightarrow> (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) ?c5 = I ?c5

goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?c5 \<in> \<X> \<Longrightarrow> (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) ?c5 = I ?c5
[PROOF STEP]
have "?S = {frac (u c) | c. c \<in> \<X> \<and> isIntv (?I c)}"
[PROOF STATE]
proof (prove)
using this:
?c5 \<in> \<X> \<Longrightarrow> (SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) ?c5 = I ?c5

goal (1 subgoal):
 1. {frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} = {frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv ((SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) c)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} = {frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv ((SOME I. \<exists>r. Regions.valid_region \<X> k I r \<and> R' = Regions.region \<X> I r) c)}

goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
have upper_bound: "(u \<oplus> ?m / 2) c < intv_const (I c) + 1" if "c \<in> \<X>" "isIntv (I c)" for c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
proof (cases "u c > intv_const (I c)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
real (intv_const (I c)) < u c

goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
from t that assms
[PROOF STATE]
proof (chain)
picking this:
u \<oplus> t \<in> R'
0 \<le> t
c \<in> \<X>
Regions.isIntv (I c)
R' \<equiv> Regions.region \<X> I r
u \<in> R
R \<in> \<R>
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
R' \<in> Succ \<R> R
[PROOF STEP]
have "u c + t < intv_const (I c) + 1"
[PROOF STATE]
proof (prove)
using this:
u \<oplus> t \<in> R'
0 \<le> t
c \<in> \<X>
Regions.isIntv (I c)
R' \<equiv> Regions.region \<X> I r
u \<in> R
R \<in> \<R>
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
R' \<in> Succ \<R> R

goal (1 subgoal):
 1. u c + t < real (intv_const (I c) + 1)
[PROOF STEP]
unfolding cval_add_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. u x + t) \<in> R'
0 \<le> t
c \<in> \<X>
Regions.isIntv (I c)
R' \<equiv> Regions.region \<X> I r
u \<in> R
R \<in> \<R>
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
R' \<in> Succ \<R> R

goal (1 subgoal):
 1. u c + t < real (intv_const (I c) + 1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
u c + t < real (intv_const (I c) + 1)

goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
with \<open>t \<ge> 0\<close> True
[PROOF STATE]
proof (chain)
picking this:
0 \<le> t
real (intv_const (I c)) < u c
u c + t < real (intv_const (I c) + 1)
[PROOF STEP]
have *: "intv_const (I c) < u c" "u c < intv_const (I c) + 1"
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
real (intv_const (I c)) < u c
u c + t < real (intv_const (I c) + 1)

goal (1 subgoal):
 1. real (intv_const (I c)) < u c &&& u c < real (intv_const (I c) + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (intv_const (I c)) < u c
u c < real (intv_const (I c) + 1)

goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
have "frac (u c) \<le> Max (?S \<union> {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frac (u c) \<le> Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
[PROOF STEP]
using finite(1) that
[PROOF STATE]
proof (prove)
using this:
finite \<X>
c \<in> \<X>
Regions.isIntv (I c)

goal (1 subgoal):
 1. frac (u c) \<le> Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
[PROOF STEP]
by - (rule Max_ge; auto)
[PROOF STATE]
proof (state)
this:
frac (u c) \<le> Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})

goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
frac (u c) \<le> Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
[PROOF STEP]
have "?m \<le> 1 - frac (u c)"
[PROOF STATE]
proof (prove)
using this:
frac (u c) \<le> Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})

goal (1 subgoal):
 1. 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1 - frac (u c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1 - frac (u c)

goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1 - frac (u c)
[PROOF STEP]
have "?m / 2 < 1 - frac (u c)"
[PROOF STATE]
proof (prove)
using this:
1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1 - frac (u c)

goal (1 subgoal):
 1. (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1 - frac (u c)
[PROOF STEP]
using * nat_intv_frac_decomp
[PROOF STATE]
proof (prove)
using this:
1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1 - frac (u c)
real (intv_const (I c)) < u c
u c < real (intv_const (I c) + 1)
\<lbrakk>real ?c < ?d; ?d < real (?c + 1)\<rbrakk> \<Longrightarrow> ?d = real ?c + frac ?d

goal (1 subgoal):
 1. (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1 - frac (u c)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1 - frac (u c)

goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1 - frac (u c)
[PROOF STEP]
have "(u \<oplus> ?m / 2) c < u c + 1 - frac (u c)"
[PROOF STATE]
proof (prove)
using this:
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1 - frac (u c)

goal (1 subgoal):
 1. (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < u c + 1 - frac (u c)
[PROOF STEP]
unfolding cval_add_def
[PROOF STATE]
proof (prove)
using this:
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1 - frac (u c)

goal (1 subgoal):
 1. u c + (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < u c + 1 - frac (u c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < u c + 1 - frac (u c)

goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < u c + 1 - frac (u c)

goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
real (intv_const (I c)) < u c
u c < real (intv_const (I c) + 1)
[PROOF STEP]
have
      "\<dots> = intv_const (I c) + 1"
[PROOF STATE]
proof (prove)
using this:
real (intv_const (I c)) < u c
u c < real (intv_const (I c) + 1)

goal (1 subgoal):
 1. u c + 1 - frac (u c) = real (intv_const (I c) + 1)
[PROOF STEP]
using nat_intv_frac_decomp of_nat_1 of_nat_add
[PROOF STATE]
proof (prove)
using this:
real (intv_const (I c)) < u c
u c < real (intv_const (I c) + 1)
\<lbrakk>real ?c < ?d; ?d < real (?c + 1)\<rbrakk> \<Longrightarrow> ?d = real ?c + frac ?d
of_nat 1 = (1::?'a)
of_nat (?m + ?n) = of_nat ?m + of_nat ?n

goal (1 subgoal):
 1. u c + 1 - frac (u c) = real (intv_const (I c) + 1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
u c + 1 - frac (u c) = real (intv_const (I c) + 1)

goal (2 subgoals):
 1. real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)

goal (1 subgoal):
 1. (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)

goal (1 subgoal):
 1. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> real (intv_const (I c)) < u c

goal (1 subgoal):
 1. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> real (intv_const (I c)) < u c
[PROOF STEP]
have "u c \<le> intv_const (I c)"
[PROOF STATE]
proof (prove)
using this:
\<not> real (intv_const (I c)) < u c

goal (1 subgoal):
 1. u c \<le> real (intv_const (I c))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u c \<le> real (intv_const (I c))

goal (1 subgoal):
 1. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u c \<le> real (intv_const (I c))

goal (1 subgoal):
 1. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
from \<open>0 \<le> ?m\<close> \<open>?m \<le> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1
[PROOF STEP]
have "?m / 2 < 1"
[PROOF STATE]
proof (prove)
using this:
0 \<le> 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1

goal (1 subgoal):
 1. (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1

goal (1 subgoal):
 1. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u c \<le> real (intv_const (I c))
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1
[PROOF STEP]
have "u c + ?m / 2 < intv_const (I c) + 1"
[PROOF STATE]
proof (prove)
using this:
u c \<le> real (intv_const (I c))
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < 1

goal (1 subgoal):
 1. u c + (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < real (intv_const (I c) + 1)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
u c + (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < real (intv_const (I c) + 1)

goal (1 subgoal):
 1. \<not> real (intv_const (I c)) < u c \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u c + (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < real (intv_const (I c) + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u c + (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 < real (intv_const (I c) + 1)

goal (1 subgoal):
 1. (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
[PROOF STEP]
by (simp add: cval_add_def)
[PROOF STATE]
proof (state)
this:
(u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c5 \<in> \<X>; Regions.isIntv (I ?c5)\<rbrakk> \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) ?c5 < real (intv_const (I ?c5) + 1)

goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
have "?t \<ge> 0 \<and> u \<oplus> ?t \<in> R' \<and> ?t \<ge> ?m / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
proof (cases "t \<ge> ?m / 2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
 2. \<not> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t

goal (2 subgoals):
 1. (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
 2. \<not> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
from \<open>t \<ge> ?m / 2\<close> t \<open>Max (?S \<union> {0}) \<le> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
u \<oplus> t \<in> R'
0 \<le> t
Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1
[PROOF STEP]
have "u \<oplus> ?t \<in> R' \<and> ?t \<ge> ?m / 2"
[PROOF STATE]
proof (prove)
using this:
(1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
u \<oplus> t \<in> R'
0 \<le> t
Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0}) \<le> 1

goal (1 subgoal):
 1. u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
by - (rule someI; auto)
[PROOF STATE]
proof (state)
this:
u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)

goal (2 subgoals):
 1. (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
 2. \<not> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
with \<open>?m \<ge> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)

goal (1 subgoal):
 1. 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)

goal (1 subgoal):
 1. \<not> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t

goal (1 subgoal):
 1. \<not> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
have "u \<oplus> ?m / 2 \<in> R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<in> R'
[PROOF STEP]
unfolding R'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<in> Regions.region \<X> I r
[PROOF STEP]
apply (rule delayedR_correct_aux')
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. u \<oplus> ?t1.0 \<in> Regions.region \<X> I r
 2. Regions.valid_region \<X> k I r
 3. \<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
 4. \<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 5. ?t1.0 \<le> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2
[PROOF STEP]
apply (rule t[unfolded R'_def])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Regions.valid_region \<X> k I r
 2. \<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
 3. \<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 4. t \<le> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2
[PROOF STEP]
apply (rule assms)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. t \<le> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2
[PROOF STEP]
using upper_bound False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c5 \<in> \<X>; Regions.isIntv (I ?c5)\<rbrakk> \<Longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) ?c5 < real (intv_const (I ?c5) + 1)
\<not> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2) c < real (intv_const (I c) + 1)
 2. t \<le> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<in> R'

goal (1 subgoal):
 1. \<not> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t \<Longrightarrow> 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
with \<open>?m \<ge> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<in> R'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> 1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})
u \<oplus> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<in> R'

goal (1 subgoal):
 1. 0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
by - (rule someI2; fastforce)
[PROOF STATE]
proof (state)
this:
0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)

goal (2 subgoals):
 1. delayedR R' u \<in> R'
 2. \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)
[PROOF STEP]
show "delayedR R' u \<in> R'" "\<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> t \<ge> ?m / 2"
[PROOF STATE]
proof (prove)
using this:
0 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<and> u \<oplus> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t) \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> (SOME t. u \<oplus> t \<in> R' \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t)

goal (1 subgoal):
 1. delayedR R' u \<in> R' &&& \<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
[PROOF STEP]
by (auto simp: delayedR_def \<open>?S = _\<close>)
[PROOF STATE]
proof (state)
this:
delayedR R' u \<in> R'
\<exists>t\<ge>0. delayedR R' u = u \<oplus> t \<and> (1 - Max ({frac (u c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<S>_L:
  "l \<in> L" if "(l, R) \<in> \<S>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> L
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(l, R) \<in> \<S>

goal (1 subgoal):
 1. l \<in> L
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
using this:
(l, R) \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}

goal (1 subgoal):
 1. l \<in> L
[PROOF STEP]
by auto


[STATEMENT]
lemma \<S>_inv:
  "(l, R) \<in> \<S> \<Longrightarrow> R \<subseteq> \<lbrace>inv_of A l\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, R) \<in> \<S> \<Longrightarrow> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, R) \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<Longrightarrow> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[PROOF STEP]
by auto


[STATEMENT]
lemma upper_right_closed:
  assumes "\<forall>c\<in>\<X>. real (k c) < u c" "u \<in> R" "R \<in> \<R>" "t \<ge> 0"
  shows "u \<oplus> t \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> t \<in> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<oplus> t \<in> R
[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 (1 subgoal):
 1. u \<oplus> t \<in> R
[PROOF STEP]
from assms \<R>_V
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<in>\<X>. real (k c) < u c
u \<in> R
R \<in> \<R>
0 \<le> t
\<Union> \<R> = V
[PROOF STEP]
have "u \<in> V"
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>\<X>. real (k c) < u c
u \<in> R
R \<in> \<R>
0 \<le> t
\<Union> \<R> = V

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

goal (1 subgoal):
 1. u \<oplus> t \<in> R
[PROOF STEP]
from assms R
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<in>\<X>. real (k c) < u c
u \<in> R
R \<in> \<R>
0 \<le> t
R = Regions.region \<X> I r
Regions.valid_region \<X> k I r
[PROOF STEP]
have "\<forall> c \<in> \<X>. I c = Greater (k c)"
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>\<X>. real (k c) < u c
u \<in> R
R \<in> \<R>
0 \<le> t
R = Regions.region \<X> I r
Regions.valid_region \<X> k I r

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. I c = Regions.intv.Greater (k c)
[PROOF STEP]
by safe (case_tac "I c"; fastforce)
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>\<X>. I c = Regions.intv.Greater (k c)

goal (1 subgoal):
 1. u \<oplus> t \<in> R
[PROOF STEP]
with R \<open>u \<in> V\<close> assms
[PROOF STATE]
proof (chain)
picking this:
R = Regions.region \<X> I r
Regions.valid_region \<X> k I r
u \<in> V
\<forall>c\<in>\<X>. real (k c) < u c
u \<in> R
R \<in> \<R>
0 \<le> t
\<forall>c\<in>\<X>. I c = Regions.intv.Greater (k c)
[PROOF STEP]
show
    "u \<oplus> t \<in> R"
[PROOF STATE]
proof (prove)
using this:
R = Regions.region \<X> I r
Regions.valid_region \<X> k I r
u \<in> V
\<forall>c\<in>\<X>. real (k c) < u c
u \<in> R
R \<in> \<R>
0 \<le> t
\<forall>c\<in>\<X>. I c = Regions.intv.Greater (k c)

goal (1 subgoal):
 1. u \<oplus> t \<in> R
[PROOF STEP]
unfolding V_def
[PROOF STATE]
proof (prove)
using this:
R = Regions.region \<X> I r
Regions.valid_region \<X> k I r
u \<in> {v. \<forall>x\<in>\<X>. 0 \<le> v x}
\<forall>c\<in>\<X>. real (k c) < u c
u \<in> R
R \<in> \<R>
0 \<le> t
\<forall>c\<in>\<X>. I c = Regions.intv.Greater (k c)

goal (1 subgoal):
 1. u \<oplus> t \<in> R
[PROOF STEP]
by safe (rule; force simp: cval_add_def)
[PROOF STATE]
proof (state)
this:
u \<oplus> t \<in> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma S_I[intro]:
  "(l, u) \<in> S" if "l \<in> L" "u \<in> V" "u \<turnstile> inv_of A l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, u) \<in> S
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
l \<in> L
u \<in> V
u \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. (l, u) \<in> S
[PROOF STEP]
by (auto simp: S_def V_def)