[STATEMENT]
lemma justified_with_sum:
  assumes "finite X" "X\<noteq>{}"
    and   "x \<in> X"
    and   "justified_with (C x) M (N x)"
    and   "\<forall>x\<in>X. justified (C x) (N x)"
    and   "\<forall>x\<in>X. \<forall>t. 0 \<le> zcount (C x) t"
  shows   "justified_with (\<Sum>x\<in>X. C x) M (\<Sum>x\<in>X. N x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (sum C X) M (sum N X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
X \<noteq> {}
x \<in> X
justified_with (C x) M (N x)
\<forall>x\<in>X. justified (C x) (N x)
\<forall>x\<in>X. \<forall>t. 0 \<le> zcount (C x) t

goal (1 subgoal):
 1. justified_with (sum C X) M (sum N X)
[PROOF STEP]
proof (induct X rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>{} \<noteq> {}; x \<in> {}; justified_with (C x) M (N x); \<forall>x\<in>{}. justified (C x) (N x); \<forall>x\<in>{}. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C {}) M (sum N {})
 2. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; \<lbrakk>F \<noteq> {}; x \<in> F; justified_with (C x) M (N x); \<forall>x\<in>F. justified (C x) (N x); \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F); insert xa F \<noteq> {}; x \<in> insert xa F; justified_with (C x) M (N x); \<forall>x\<in>insert xa F. justified (C x) (N x); \<forall>x\<in>insert xa F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert xa F)) M (sum N (insert xa F))
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<noteq> {}
x \<in> {}
justified_with (C x) M (N x)
\<forall>x\<in>{}. justified (C x) (N x)
\<forall>x\<in>{}. \<forall>t. 0 \<le> zcount (C x) t

goal (2 subgoals):
 1. \<lbrakk>{} \<noteq> {}; x \<in> {}; justified_with (C x) M (N x); \<forall>x\<in>{}. justified (C x) (N x); \<forall>x\<in>{}. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C {}) M (sum N {})
 2. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; \<lbrakk>F \<noteq> {}; x \<in> F; justified_with (C x) M (N x); \<forall>x\<in>F. justified (C x) (N x); \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F); insert xa F \<noteq> {}; x \<in> insert xa F; justified_with (C x) M (N x); \<forall>x\<in>insert xa F. justified (C x) (N x); \<forall>x\<in>insert xa F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert xa F)) M (sum N (insert xa F))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} \<noteq> {}
x \<in> {}
justified_with (C x) M (N x)
\<forall>x\<in>{}. justified (C x) (N x)
\<forall>x\<in>{}. \<forall>t. 0 \<le> zcount (C x) t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{} \<noteq> {}
x \<in> {}
justified_with (C x) M (N x)
\<forall>x\<in>{}. justified (C x) (N x)
\<forall>x\<in>{}. \<forall>t. 0 \<le> zcount (C x) t

goal (1 subgoal):
 1. justified_with (sum C {}) M (sum N {})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
justified_with (sum C {}) M (sum N {})

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; \<lbrakk>F \<noteq> {}; x \<in> F; justified_with (C x) M (N x); \<forall>x\<in>F. justified (C x) (N x); \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F); insert xa F \<noteq> {}; x \<in> insert xa F; justified_with (C x) M (N x); \<forall>x\<in>insert xa F. justified (C x) (N x); \<forall>x\<in>insert xa F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert xa F)) M (sum N (insert xa F))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; \<lbrakk>F \<noteq> {}; x \<in> F; justified_with (C x) M (N x); \<forall>x\<in>F. justified (C x) (N x); \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F); insert xa F \<noteq> {}; x \<in> insert xa F; justified_with (C x) M (N x); \<forall>x\<in>insert xa F. justified (C x) (N x); \<forall>x\<in>insert xa F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert xa F)) M (sum N (insert xa F))
[PROOF STEP]
case (insert y F)
[PROOF STATE]
proof (state)
this:
finite F
y \<notin> F
\<lbrakk>F \<noteq> {}; x \<in> F; justified_with (C x) M (N x); \<forall>x\<in>F. justified (C x) (N x); \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F)
insert y F \<noteq> {}
x \<in> insert y F
justified_with (C x) M (N x)
\<forall>x\<in>insert y F. justified (C x) (N x)
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; \<lbrakk>F \<noteq> {}; x \<in> F; justified_with (C x) M (N x); \<forall>x\<in>F. justified (C x) (N x); \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F); insert xa F \<noteq> {}; x \<in> insert xa F; justified_with (C x) M (N x); \<forall>x\<in>insert xa F. justified (C x) (N x); \<forall>x\<in>insert xa F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert xa F)) M (sum N (insert xa F))
[PROOF STEP]
thm insert
[PROOF STATE]
proof (state)
this:
finite F
y \<notin> F
\<lbrakk>F \<noteq> {}; x \<in> F; justified_with (C x) M (N x); \<forall>x\<in>F. justified (C x) (N x); \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F)
insert y F \<noteq> {}
x \<in> insert y F
justified_with (C x) M (N x)
\<forall>x\<in>insert y F. justified (C x) (N x)
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; \<lbrakk>F \<noteq> {}; x \<in> F; justified_with (C x) M (N x); \<forall>x\<in>F. justified (C x) (N x); \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F); insert xa F \<noteq> {}; x \<in> insert xa F; justified_with (C x) M (N x); \<forall>x\<in>insert xa F. justified (C x) (N x); \<forall>x\<in>insert xa F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert xa F)) M (sum N (insert xa F))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (sum C (insert y F)) M (sum N (insert y F))
[PROOF STEP]
apply (cases "F={}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. F = {} \<Longrightarrow> justified_with (sum C (insert y F)) M (sum N (insert y F))
 2. F \<noteq> {} \<Longrightarrow> justified_with (sum C (insert y F)) M (sum N (insert y F))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = {} \<Longrightarrow> justified_with (sum C (insert y F)) M (sum N (insert y F))
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
y \<notin> F
\<lbrakk>F \<noteq> {}; x \<in> F; justified_with (C x) M (N x); \<forall>x\<in>F. justified (C x) (N x); \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F)
insert y F \<noteq> {}
x \<in> insert y F
justified_with (C x) M (N x)
\<forall>x\<in>insert y F. justified (C x) (N x)
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (1 subgoal):
 1. F = {} \<Longrightarrow> justified_with (sum C (insert y F)) M (sum N (insert y F))
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> justified_with (sum C (insert y F)) M (sum N (insert y F))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> justified_with (sum C (insert y F)) M (sum N (insert y F))
[PROOF STEP]
apply (subst (1 2) sum.insert_remove)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. F \<noteq> {} \<Longrightarrow> finite F
 2. F \<noteq> {} \<Longrightarrow> justified_with (C y + sum C (F - {y})) M (N y + sum N (F - {y}))
[PROOF STEP]
using insert(1)
[PROOF STATE]
proof (prove)
using this:
finite F

goal (2 subgoals):
 1. F \<noteq> {} \<Longrightarrow> finite F
 2. F \<noteq> {} \<Longrightarrow> justified_with (C y + sum C (F - {y})) M (N y + sum N (F - {y}))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> justified_with (C y + sum C (F - {y})) M (N y + sum N (F - {y}))
[PROOF STEP]
using insert(2)
[PROOF STATE]
proof (prove)
using this:
y \<notin> F

goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> justified_with (C y + sum C (F - {y})) M (N y + sum N (F - {y}))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F\<rbrakk> \<Longrightarrow> justified_with (C y + sum C F) M (N y + sum N F)
[PROOF STEP]
apply (cases "y=x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified_with (C y + sum C F) M (N y + sum N F)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (C y + sum C F) M (N y + sum N F)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified_with (C y + sum C F) M (N y + sum N F)
[PROOF STEP]
apply (rule justified_with_add)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified_with (C y) M (N y)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
using insert(6)
[PROOF STATE]
proof (prove)
using this:
justified_with (C x) M (N x)

goal (5 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified_with (C y) M (N y)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
using insert(7)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. justified (C x) (N x)

goal (4 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
apply (rule justified_sum)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
using insert(7)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. justified (C x) (N x)

goal (4 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
using insert(8)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (3 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
using insert(8)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (2 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
[PROOF STEP]
apply (intro allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> 0 \<le> zcount (sum C F) t
[PROOF STEP]
unfolding zcount_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>M\<in>F. zcount (C M) t)
[PROOF STEP]
apply (rule sum_nonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t xa. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x; xa \<in> F\<rbrakk> \<Longrightarrow> 0 \<le> zcount (C xa) t
[PROOF STEP]
using insert(8)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (1 subgoal):
 1. \<And>t xa. \<lbrakk>F \<noteq> {}; y \<notin> F; y = x; xa \<in> F\<rbrakk> \<Longrightarrow> 0 \<le> zcount (C xa) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (C y + sum C F) M (N y + sum N F)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (C y + sum C F) M (N y + sum N F)
[PROOF STEP]
apply (subst (1 2) add.commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (sum C F + C y) M (sum N F + N y)
[PROOF STEP]
apply (rule justified_with_add)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (sum C F) M (sum N F)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply (rule insert(3))
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> F \<noteq> {}
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> F
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (C x) M (N x)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 6. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 7. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 8. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 9. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> F
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (C x) M (N x)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 6. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 7. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 8. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
using insert(5)
[PROOF STATE]
proof (prove)
using this:
x \<in> insert y F

goal (8 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> F
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (C x) M (N x)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 6. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 7. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 8. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (C x) M (N x)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 6. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 7. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
using insert(6)
[PROOF STATE]
proof (prove)
using this:
justified_with (C x) M (N x)

goal (7 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified_with (C x) M (N x)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 6. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 7. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 6. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
using insert(7)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. justified (C x) (N x)

goal (6 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 6. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
using insert(8)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (5 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (sum C F) (sum N F)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply (rule justified_sum)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>p\<in>F. justified (C p) (N p)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>p\<in>F. \<forall>t. 0 \<le> zcount (C p) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
using insert(7)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. justified (C x) (N x)

goal (5 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>p\<in>F. justified (C p) (N p)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>p\<in>F. \<forall>t. 0 \<le> zcount (C p) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 5. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>p\<in>F. \<forall>t. 0 \<le> zcount (C p) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
using insert(8)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (4 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>p\<in>F. \<forall>t. 0 \<le> zcount (C p) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 4. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
using insert(7)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. justified (C x) (N x)

goal (3 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> justified (C y) (N y)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 3. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum C F) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply (intro allI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> 0 \<le> zcount (sum C F) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
unfolding zcount_sum
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>M\<in>F. zcount (C M) t)
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply (rule sum_nonneg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t xa. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x; xa \<in> F\<rbrakk> \<Longrightarrow> 0 \<le> zcount (C xa) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
using insert(8)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (2 subgoals):
 1. \<And>t xa. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x; xa \<in> F\<rbrakk> \<Longrightarrow> 0 \<le> zcount (C xa) t
 2. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
using insert(8)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert y F. \<forall>t. 0 \<le> zcount (C x) t

goal (1 subgoal):
 1. \<lbrakk>F \<noteq> {}; y \<notin> F; y \<noteq> x\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C y) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
justified_with (sum C (insert y F)) M (sum N (insert y F))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma justified_with_add_same:
  assumes "justified_with C M N"
    and   "\<forall>t. 0 \<le> zcount C t"
  shows   "justified_with (C + zmset_of \<Delta>) M (N + zmset_of \<Delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (C + zmset_of \<Delta>) M (N + zmset_of \<Delta>)
[PROOF STEP]
unfolding justified_with_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
assume Mt: "0 < zcount M t"
[PROOF STATE]
proof (state)
this:
0 < zcount M t

goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
note assms(1)[unfolded justified_with_alt, rule_format, OF Mt]
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t

goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
with Mt
[PROOF STATE]
proof (chain)
picking this:
0 < zcount M t
(\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
consider
    "\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)" |
    "\<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)" |
    "\<exists>s<t. 0 < zcount C s" |
    "zcount (M + N) t < zcount C t"
[PROOF STATE]
proof (prove)
using this:
0 < zcount M t
(\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t

goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> thesis; zcount (M + N) t < zcount C t \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using not_less
[PROOF STATE]
proof (prove)
using this:
0 < zcount M t
(\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> thesis; zcount (M + N) t < zcount C t \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> ?thesis; zcount (M + N) t < zcount C t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> ?thesis; zcount (M + N) t < zcount C t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "(\<exists>s<t. (zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0)) \<or>
         (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> ?thesis; zcount (M + N) t < zcount C t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 2. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 3. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 4. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)

goal (4 subgoals):
 1. \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 2. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 3. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 4. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t

goal (3 subgoals):
 1. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 2. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 3. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 2. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 3. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)

goal (3 subgoals):
 1. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 2. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 3. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
by (metis add_less_same_cancel2 assms(2) not_less preorder_class.le_less_trans zcount_union)
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t

goal (2 subgoals):
 1. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 2. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 2. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
\<exists>s<t. 0 < zcount C s

goal (2 subgoals):
 1. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
 2. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t. 0 < zcount C s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. 0 < zcount C s

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t

goal (1 subgoal):
 1. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
zcount (M + N) t < zcount C t

goal (1 subgoal):
 1. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (M + N) t < zcount C t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount (M + N) t < zcount C t

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + zmset_of \<Delta>) s < 0) \<or> (\<exists>s<t. 0 < zcount (C + zmset_of \<Delta>) s) \<or> zcount (M + (N + zmset_of \<Delta>)) t < zcount (C + zmset_of \<Delta>) t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma justified_with_add_msg_delta:
  assumes "justified_with C M N"
    and   "minting_msg C \<Delta>"
    and   "\<forall>t. 0 \<le> zcount C t"
  shows   "justified_with C M (N + timestamps (zmset_of \<Delta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with C M (N + timestamps (zmset_of \<Delta>))
[PROOF STEP]
unfolding justified_with_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
assume Mt: "0 < zcount M t"
[PROOF STATE]
proof (state)
this:
0 < zcount M t

goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
note assms(1)[unfolded justified_with_alt, rule_format, OF Mt]
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t

goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
with Mt
[PROOF STATE]
proof (chain)
picking this:
0 < zcount M t
(\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
consider
    "\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)" |
    "\<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)" |
    "\<exists>s<t. 0 < zcount C s" |
    "zcount (M + N) t < zcount C t"
[PROOF STATE]
proof (prove)
using this:
0 < zcount M t
(\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t

goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> thesis; zcount (M + N) t < zcount C t \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using not_less
[PROOF STATE]
proof (prove)
using this:
0 < zcount M t
(\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> thesis; zcount (M + N) t < zcount C t \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> ?thesis; zcount (M + N) t < zcount C t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> ?thesis; zcount (M + N) t < zcount C t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "(\<exists>s<t. (zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0)) \<or>
         (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. 0 < zcount C s \<Longrightarrow> ?thesis; zcount (M + N) t < zcount C t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 3. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 4. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)

goal (4 subgoals):
 1. \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 3. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 4. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t

goal (3 subgoals):
 1. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 3. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 3. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)

goal (3 subgoals):
 1. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 3. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)
[PROOF STEP]
obtain s where s: "s < t" "zcount N s < 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)

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

goal (3 subgoals):
 1. \<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 3. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s < t
zcount N s < 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s < t
zcount N s < 0

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
proof (cases "\<exists>(p,s')\<in>#\<Delta>. s' \<le> s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>s < t; zcount N s < 0; \<exists>(p, s')\<in>#\<Delta>. s' \<le> s\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. \<lbrakk>s < t; zcount N s < 0; \<not> (\<exists>(p, s')\<in>#\<Delta>. s' \<le> s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>(p, s')\<in>#\<Delta>. s' \<le> s

goal (2 subgoals):
 1. \<lbrakk>s < t; zcount N s < 0; \<exists>(p, s')\<in>#\<Delta>. s' \<le> s\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. \<lbrakk>s < t; zcount N s < 0; \<not> (\<exists>(p, s')\<in>#\<Delta>. s' \<le> s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>(p, s')\<in>#\<Delta>. s' \<le> s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>(p, s')\<in>#\<Delta>. s' \<le> s

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>(p, s')\<in>#\<Delta>. s' \<le> s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in># \<Delta>; b \<le> s; \<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s + int (count {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>#} s) < 0; \<not> zcount M t + (zcount N t + int (count {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>#} t)) < zcount C t\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
apply (drule assms(2)[unfolded minting_msg_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<le> s; \<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s + int (count {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>#} s) < 0; \<not> zcount M t + (zcount N t + int (count {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>#} t)) < zcount C t; case (a, b) of (p, t) \<Rightarrow> \<exists>t'<t. 0 < zcount C t'\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
using order.strict_trans order.strict_trans1 s(1) not_less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < ?b; ?b < ?c\<rbrakk> \<Longrightarrow> ?a < ?c
\<lbrakk>?a \<le> ?b; ?b < ?c\<rbrakk> \<Longrightarrow> ?a < ?c
s < t
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<le> s; \<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s + int (count {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>#} s) < 0; \<not> zcount M t + (zcount N t + int (count {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>#} t)) < zcount C t; case (a, b) of (p, t) \<Rightarrow> \<exists>t'<t. 0 < zcount C t'\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t

goal (1 subgoal):
 1. \<lbrakk>s < t; zcount N s < 0; \<not> (\<exists>(p, s')\<in>#\<Delta>. s' \<le> s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>s < t; zcount N s < 0; \<not> (\<exists>(p, s')\<in>#\<Delta>. s' \<le> s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>(p, s')\<in>#\<Delta>. s' \<le> s)

goal (1 subgoal):
 1. \<lbrakk>s < t; zcount N s < 0; \<not> (\<exists>(p, s')\<in>#\<Delta>. s' \<le> s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>(p, s')\<in>#\<Delta>. s' \<le> s)
[PROOF STEP]
have "zcount (timestamps (zmset_of \<Delta>)) s = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>(p, s')\<in>#\<Delta>. s' \<le> s)

goal (1 subgoal):
 1. zcount (timestamps (zmset_of \<Delta>)) s = 0
[PROOF STEP]
by (force intro: ccontr dest: pos_image_zmset_obtain_pre[rotated])
[PROOF STATE]
proof (state)
this:
zcount (timestamps (zmset_of \<Delta>)) s = 0

goal (1 subgoal):
 1. \<lbrakk>s < t; zcount N s < 0; \<not> (\<exists>(p, s')\<in>#\<Delta>. s' \<le> s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (timestamps (zmset_of \<Delta>)) s = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount (timestamps (zmset_of \<Delta>)) s = 0

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
by (metis plus_int_code(1) s(1,2) zcount_union)
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t

goal (2 subgoals):
 1. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
\<exists>s<t. 0 < zcount C s

goal (2 subgoals):
 1. \<exists>s<t. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t. 0 < zcount C s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. 0 < zcount C s

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t

goal (1 subgoal):
 1. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
zcount (M + N) t < zcount C t

goal (1 subgoal):
 1. zcount (M + N) t < zcount C t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (M + N) t < zcount C t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount (M + N) t < zcount C t

goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
apply (cases "zcount (timestamps (zmset_of \<Delta>)) t > 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>zcount (M + N) t < zcount C t; 0 < zcount (timestamps (zmset_of \<Delta>)) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
 2. \<lbrakk>zcount (M + N) t < zcount C t; \<not> 0 < zcount (timestamps (zmset_of \<Delta>)) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
apply (auto dest: pos_image_zmset_obtain_pre[rotated] assms(2)[unfolded minting_msg_def, rule_format]) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>zcount (M + N) t < zcount C t; \<not> 0 < zcount (timestamps (zmset_of \<Delta>)) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
unfolding not_less
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>zcount (M + N) t < zcount C t; zcount (timestamps (zmset_of \<Delta>)) t \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. zcount M s < 0 \<or> zcount (N + timestamps (zmset_of \<Delta>)) s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + (N + timestamps (zmset_of \<Delta>))) t < zcount C t

goal:
No subgoals!
[PROOF STEP]
qed