[STATEMENT]
lemma betaupright_upright_vut:
  assumes "beta_upright va vb"
    and     "upright vb"
    and     "vacant_upto (va + vb) t"
  shows   "vacant_upto va t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
assume s: "s \<le> t" "zcount va s > 0"
[PROOF STATE]
proof (state)
this:
s \<le> t
0 < zcount va s

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
[PROOF STEP]
obtain x where x: "x < s" "zcount va x < 0 \<or> zcount vb x < 0" "nonpos_upto va x"
[PROOF STATE]
proof (prove)
using this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using betaupright_obtain_support
[PROOF STATE]
proof (prove)
using this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
\<lbrakk>beta_upright ?va ?vb; 0 < zcount ?va ?t; \<And>s. \<lbrakk>s < ?t; zcount ?va s < 0 \<or> zcount ?vb s < 0; nonpos_upto ?va s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x

goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "zcount va x < 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; zcount va x < 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
zcount va x < 0

goal (2 subgoals):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; zcount va x < 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms(2,3) s x(1,3)
[PROOF STATE]
proof (chain)
picking this:
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
nonpos_upto va x
zcount va x < 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
nonpos_upto va x
zcount va x < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
upright vb
\<forall>s\<le>t. zcount (va + vb) s = 0
s \<le> t
0 < zcount va s
x < s
nonpos_upto va x
zcount va x < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>upright vb; \<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t; 0 < zcount va s; x < s; nonpos_upto va x; zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule upright_obtain_support[of vb x])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t; 0 < zcount va s; x < s; nonpos_upto va x; zcount va x < 0\<rbrakk> \<Longrightarrow> 0 < zcount vb x
 2. \<And>sa. \<lbrakk>\<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t; 0 < zcount va s; x < s; nonpos_upto va x; zcount va x < 0; sa < x; zcount vb sa < 0; nonpos_upto vb sa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis add_less_same_cancel2 order.trans order.strict_implies_order)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t; 0 < zcount va s; x < s; nonpos_upto va x; zcount va x < 0; sa < x; zcount vb sa < 0; nonpos_upto vb sa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis add_less_same_cancel1 add_neg_neg order.order_iff_strict order.trans less_irrefl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> zcount va x < 0

goal (1 subgoal):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms s x
[PROOF STATE]
proof (chain)
picking this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
\<not> zcount va x < 0
[PROOF STEP]
have "x \<le> t" "zcount va x > 0"
[PROOF STATE]
proof (prove)
using this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
\<not> zcount va x < 0

goal (1 subgoal):
 1. x \<le> t &&& 0 < zcount va x
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>beta_upright va vb; upright vb; vacant_upto (va + vb) t; s \<le> t; 0 < zcount va s; x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> x \<le> t
 2. \<lbrakk>beta_upright va vb; upright vb; vacant_upto (va + vb) t; s \<le> t; 0 < zcount va s; x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> 0 < zcount va x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>beta_upright va vb; upright vb; vacant_upto (va + vb) t; s \<le> t; 0 < zcount va s; x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> 0 < zcount va x
[PROOF STEP]
apply (metis (no_types, opaque_lifting) add.left_neutral order.order_iff_strict order.trans vacant_upto_def zcount_union)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
x \<le> t
0 < zcount va x

goal (1 subgoal):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms(2,3) s x
[PROOF STATE]
proof (chain)
picking this:
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
x \<le> t
0 < zcount va x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
x \<le> t
0 < zcount va x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s2 \<le> t; 0 < zcount va ?s2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
note r = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s2 \<le> t; 0 < zcount va ?s2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
from assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
upright vb
vacant_upto (va + vb) t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
upright vb
vacant_upto (va + vb) t

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
unfolding vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
upright vb
\<forall>s\<le>t. zcount (va + vb) s = 0

goal (1 subgoal):
 1. \<forall>s\<le>t. zcount va s = 0
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>upright vb; \<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t\<rbrakk> \<Longrightarrow> zcount va s = 0
[PROOF STEP]
apply (metis (no_types, opaque_lifting) r add_cancel_right_left order.order_iff_strict order.trans le_less_linear less_add_same_cancel2 upright_obtain_support)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
vacant_upto va t

goal:
No subgoals!
[PROOF STEP]
qed