[STATEMENT]
lemma justified_with_add:
  assumes "justified_with C1 M N1"
    and   "justified C1 N1"
    and   "justified C2 N2"
    and   "\<forall>t. 0 \<le> zcount C1 t"
    and   "\<forall>t. 0 \<le> zcount C2 t"
  shows   "justified_with (C1+C2) M (N1+N2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (C1 + C2) M (N1 + N2)
[PROOF STEP]
proof (intro justified_with_leastI allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount M t; \<forall>t'<t. zcount M t' \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount M t; \<forall>t'<t. zcount M t' \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
assume count_t: "0 < zcount M t"
[PROOF STATE]
proof (state)
this:
0 < zcount M t

goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount M t; \<forall>t'<t. zcount M t' \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
assume least: "\<forall>t'<t. zcount M t' \<le> 0"
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. zcount M t' \<le> 0

goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount M t; \<forall>t'<t. zcount M t' \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
note assms(1)[unfolded justified_with_alt, rule_format, OF count_t]
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount N1 s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C1 s) \<or> zcount (M + N1) t < zcount C1 t

goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount M t; \<forall>t'<t. zcount M t' \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount N1 s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C1 s) \<or> zcount (M + N1) t < zcount C1 t
[PROOF STEP]
consider
    "\<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)" |
    "\<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)" |
    "\<exists>s<t. 0 < zcount C1 s" |
    "zcount (M + N1) t < zcount C1 t"
[PROOF STATE]
proof (prove)
using this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount N1 s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C1 s) \<or> zcount (M + N1) t < zcount C1 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 N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> thesis; zcount (M + N1) t < zcount C1 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 N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> ?thesis; zcount (M + N1) t < zcount C1 t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount M t; \<forall>t'<t. zcount M t' \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) 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 N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> ?thesis; zcount (M + N1) t < zcount C1 t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or>
         (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) 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 N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> ?thesis; zcount (M + N1) t < zcount C1 t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) 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 (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 4. zcount (M + N1) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) 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 (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 4. zcount (M + N1) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) 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 (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

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

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

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s < t; zcount N1 s < 0; \<forall>s'<s. 0 \<le> zcount N1 s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> \<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. 0 \<le> zcount N1 s')
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s < t; zcount N1 s < 0; \<forall>s'<s. zcount M s' \<le> 0\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. 0 \<le> zcount N1 s')
[PROOF STEP]
apply (drule order_zmset_exists_foundation_neg')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s < t; \<forall>s'<s. zcount M s' \<le> 0; \<exists>sa\<le>s. zcount N1 sa < 0 \<and> (\<forall>u<sa. 0 \<le> zcount N1 u)\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. 0 \<le> zcount N1 s')
[PROOF STEP]
using order.strict_trans order.strict_trans1
[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

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s < t; \<forall>s'<s. zcount M s' \<le> 0; \<exists>sa\<le>s. zcount N1 sa < 0 \<and> (\<forall>u<sa. 0 \<le> zcount N1 u)\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. 0 \<le> zcount N1 s')
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
s < t
zcount N1 s < 0
\<forall>s'<s. 0 \<le> zcount N1 s'

goal (3 subgoals):
 1. \<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. zcount (M + N1) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s < t
zcount N1 s < 0
\<forall>s'<s. 0 \<le> zcount N1 s'
[PROOF STEP]
consider
      "zcount (N1 + N2) s < 0" |
      "0 < zcount N2 s" "zcount (N1 + N2) s \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
s < t
zcount N1 s < 0
\<forall>s'<s. 0 \<le> zcount N1 s'

goal (1 subgoal):
 1. \<lbrakk>zcount (N1 + N2) s < 0 \<Longrightarrow> thesis; \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>zcount (N1 + N2) s < 0 \<Longrightarrow> ?thesis; \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (3 subgoals):
 1. \<exists>s<t. zcount N1 s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. zcount (M + N1) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>zcount (N1 + N2) s < 0 \<Longrightarrow> ?thesis; \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>zcount (N1 + N2) s < 0 \<Longrightarrow> ?thesis; \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. zcount (N1 + N2) s < 0 \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
zcount (N1 + N2) s < 0

goal (2 subgoals):
 1. zcount (N1 + N2) s < 0 \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (N1 + N2) s < 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount (N1 + N2) s < 0

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
using least order.strict_trans s(1)
[PROOF STATE]
proof (prove)
using this:
zcount (N1 + N2) s < 0
\<forall>t'<t. zcount M t' \<le> 0
\<lbrakk>?a < ?b; ?b < ?c\<rbrakk> \<Longrightarrow> ?a < ?c
s < t

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
0 < zcount N2 s
0 \<le> zcount (N1 + N2) s

goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
note assms(3)[unfolded justified_alt, rule_format, OF 2(1)]
[PROOF STATE]
proof (state)
this:
supported_strong N2 s \<or> (\<exists>t'<s. 0 < zcount C2 t') \<or> zcount N2 s < zcount C2 s

goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supported_strong N2 s \<or> (\<exists>t'<s. 0 < zcount C2 t') \<or> zcount N2 s < zcount C2 s
[PROOF STEP]
consider
        "supported_strong N2 s" "\<forall>t'<s. zcount C2 t' \<le> 0" "zcount N2 s \<ge> zcount C2 s" |
        "\<exists>t'<s. 0 < zcount C2 t'" |
        "zcount N2 s < zcount C2 s"
[PROOF STATE]
proof (prove)
using this:
supported_strong N2 s \<or> (\<exists>t'<s. 0 < zcount C2 t') \<or> zcount N2 s < zcount C2 s

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

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

goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 s; 0 \<le> zcount (N1 + N2) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk>supported_strong N2 s; \<forall>t'<s. zcount C2 t' \<le> 0; zcount C2 s \<le> zcount N2 s\<rbrakk> \<Longrightarrow> ?thesis; \<exists>t'<s. 0 < zcount C2 t' \<Longrightarrow> ?thesis; zcount N2 s < zcount C2 s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>supported_strong N2 s; \<forall>t'<s. zcount C2 t' \<le> 0; zcount C2 s \<le> zcount N2 s\<rbrakk> \<Longrightarrow> ?thesis; \<exists>t'<s. 0 < zcount C2 t' \<Longrightarrow> ?thesis; zcount N2 s < zcount C2 s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>supported_strong N2 s; \<forall>t'<s. zcount C2 t' \<le> 0; zcount C2 s \<le> zcount N2 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<exists>t'<s. 0 < zcount C2 t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. zcount N2 s < zcount C2 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
supported_strong N2 s
\<forall>t'<s. zcount C2 t' \<le> 0
zcount C2 s \<le> zcount N2 s

goal (3 subgoals):
 1. \<lbrakk>supported_strong N2 s; \<forall>t'<s. zcount C2 t' \<le> 0; zcount C2 s \<le> zcount N2 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<exists>t'<s. 0 < zcount C2 t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. zcount N2 s < zcount C2 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supported_strong N2 s
\<forall>t'<s. zcount C2 t' \<le> 0
zcount C2 s \<le> zcount N2 s
[PROOF STEP]
obtain s' where s': "s' < s" "zcount N2 s' < 0" "nonpos_upto N2 s'"
[PROOF STATE]
proof (prove)
using this:
supported_strong N2 s
\<forall>t'<s. zcount C2 t' \<le> 0
zcount C2 s \<le> zcount N2 s

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>s' < s; zcount N2 s' < 0; nonpos_upto N2 s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding supported_strong_def
[PROOF STATE]
proof (prove)
using this:
\<exists>sa<s. zcount N2 sa < 0 \<and> nonpos_upto N2 sa
\<forall>t'<s. zcount C2 t' \<le> 0
zcount C2 s \<le> zcount N2 s

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

goal (3 subgoals):
 1. \<lbrakk>supported_strong N2 s; \<forall>t'<s. zcount C2 t' \<le> 0; zcount C2 s \<le> zcount N2 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<exists>t'<s. 0 < zcount C2 t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. zcount N2 s < zcount C2 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
from s'(2)
[PROOF STATE]
proof (chain)
picking this:
zcount N2 s' < 0
[PROOF STEP]
have nonneg: "0 \<le> zcount (N1+N2) s' \<Longrightarrow> 0 < zcount N1 s'"
[PROOF STATE]
proof (prove)
using this:
zcount N2 s' < 0

goal (1 subgoal):
 1. 0 \<le> zcount (N1 + N2) s' \<Longrightarrow> 0 < zcount N1 s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> zcount (N1 + N2) s' \<Longrightarrow> 0 < zcount N1 s'

goal (3 subgoals):
 1. \<lbrakk>supported_strong N2 s; \<forall>t'<s. zcount C2 t' \<le> 0; zcount C2 s \<le> zcount N2 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<exists>t'<s. 0 < zcount C2 t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. zcount N2 s < zcount C2 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "zcount (N1 + N2) s' < 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. zcount (N1 + N2) s' < 0 \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<not> zcount (N1 + N2) s' < 0 \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (N1 + N2) s' < 0 \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
using least order.strict_trans s'(1) s(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. zcount M t' \<le> 0
\<lbrakk>?a < ?b; ?b < ?c\<rbrakk> \<Longrightarrow> ?a < ?c
s' < s
s < t

goal (1 subgoal):
 1. zcount (N1 + N2) s' < 0 \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by (intro disjI1) blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> zcount (N1 + N2) s' < 0 \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> zcount (N1 + N2) s' < 0 \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
unfolding not_less
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> zcount (N1 + N2) s' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule nonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount N1 s' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule assms(2)[unfolded justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>s<s'. zcount N1 s < 0 \<and> nonpos_upto N1 s) \<or> (\<exists>t'<s'. 0 < zcount C1 t') \<or> zcount N1 s' < zcount C1 s' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim disjE exE conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>s < s'; zcount N1 s < 0; nonpos_upto N1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<And>t'. \<lbrakk>t' < s'; 0 < zcount C1 t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. zcount N1 s' < zcount C1 s' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u < s'; zcount N1 u < 0; nonpos_upto N1 u\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by (meson local.order.strict_trans not_less s'(1) s(3))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t'. \<lbrakk>t' < s'; 0 < zcount C1 t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. zcount N1 s' < zcount C1 s' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u < s'; 0 < zcount C1 u\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by (metis add_strict_increasing assms(5) local.less_trans s'(1) s(1) zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount N1 s' < zcount C1 s' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount N1 s' < zcount C1 s' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by (smt (verit, ccfv_threshold) assms(5) local.dual_order.strict_trans s'(1) s(1) s(3) zcount_union)
[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:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal (2 subgoals):
 1. \<exists>t'<s. 0 < zcount C2 t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. zcount N2 s < zcount C2 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>t'<s. 0 < zcount C2 t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. zcount N2 s < zcount C2 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>t'<s. 0 < zcount C2 t'

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

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>t' < s; 0 < zcount C2 t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; 0 < zcount C2 s'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; 0 < zcount C2 s'\<rbrakk> \<Longrightarrow> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; 0 < zcount C2 s'\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount (C1 + C2) s
[PROOF STEP]
using assms(4)[rule_format, of s'] s(1)
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount C1 s'
s < t

goal (1 subgoal):
 1. \<lbrakk>s' < s; 0 < zcount C2 s'\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount (C1 + C2) s
[PROOF STEP]
apply (auto intro!: exI[of _ s'])
[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:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal (1 subgoal):
 1. zcount N2 s < zcount C2 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zcount N2 s < zcount C2 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
zcount N2 s < zcount C2 s

goal (1 subgoal):
 1. zcount N2 s < zcount C2 s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount N2 s < zcount C2 s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount N2 s < zcount C2 s

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by (smt (verit) "2"(1) assms(4) s(1) zcount_union)
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

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

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

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. 0 < zcount C1 s
\<forall>t. 0 \<le> zcount C2 t

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t. 0 < zcount C1 s; \<forall>t. 0 \<le> zcount C2 t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t. 0 < zcount C1 s; \<forall>t. 0 \<le> zcount C2 t\<rbrakk> \<Longrightarrow> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t. 0 < zcount C1 s; \<forall>t. 0 \<le> zcount C2 t\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount (C1 + C2) s
[PROOF STEP]
apply (metis add_strict_increasing zcount_union)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal (1 subgoal):
 1. zcount (M + N1) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zcount (M + N1) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
zcount (M + N1) t < zcount C1 t

goal (1 subgoal):
 1. zcount (M + N1) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (M + N1) t < zcount C1 t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount (M + N1) t < zcount C1 t

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
proof (cases "zcount (M + (N1 + N2)) t < zcount (C1 + C2) t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>zcount (M + N1) t < zcount C1 t; zcount (M + (N1 + N2)) t < zcount (C1 + C2) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<lbrakk>zcount (M + N1) t < zcount C1 t; \<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal (2 subgoals):
 1. \<lbrakk>zcount (M + N1) t < zcount C1 t; zcount (M + (N1 + N2)) t < zcount (C1 + C2) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<lbrakk>zcount (M + N1) t < zcount C1 t; \<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal (1 subgoal):
 1. \<lbrakk>zcount (M + N1) t < zcount C1 t; \<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>zcount (M + N1) t < zcount C1 t; \<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal (1 subgoal):
 1. \<lbrakk>zcount (M + N1) t < zcount C1 t; \<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
have N2t: "0 < zcount N2 t"
[PROOF STATE]
proof (prove)
using this:
\<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal (1 subgoal):
 1. 0 < zcount N2 t
[PROOF STEP]
using 4 assms(5)[rule_format, of t]
[PROOF STATE]
proof (prove)
using this:
\<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
zcount (M + N1) t < zcount C1 t
0 \<le> zcount C2 t

goal (1 subgoal):
 1. 0 < zcount N2 t
[PROOF STEP]
unfolding not_less zcount_union
[PROOF STATE]
proof (prove)
using this:
zcount C1 t + zcount C2 t \<le> zcount M t + (zcount N1 t + zcount N2 t)
zcount M t + zcount N1 t < zcount C1 t
0 \<le> zcount C2 t

goal (1 subgoal):
 1. 0 < zcount N2 t
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < zcount N2 t

goal (1 subgoal):
 1. \<lbrakk>zcount (M + N1) t < zcount C1 t; \<not> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount N2 t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < zcount N2 t

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
using assms(3)[unfolded justified_alt supported_strong_def, rule_format, OF N2t]
[PROOF STATE]
proof (prove)
using this:
0 < zcount N2 t
(\<exists>s<t. zcount N2 s < 0 \<and> nonpos_upto N2 s) \<or> (\<exists>t'<t. 0 < zcount C2 t') \<or> zcount N2 t < zcount C2 t

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim exE conjE disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<And>t'. \<lbrakk>0 < zcount N2 t; t' < t; 0 < zcount C2 t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. \<lbrakk>0 < zcount N2 t; zcount N2 t < zcount C2 t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "0 < zcount N1 s")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; 0 < zcount N1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; 0 < zcount N1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule assms(2)[unfolded justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; (\<exists>sa<s. zcount N1 sa < 0 \<and> nonpos_upto N1 sa) \<or> (\<exists>t'<s. 0 < zcount C1 t') \<or> zcount N1 s < zcount C1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim exE conjE disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; sa < s; zcount N1 sa < 0; nonpos_upto N1 sa\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<And>t'. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; t' < s; 0 < zcount C1 t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 3. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; zcount N1 s < zcount C1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; zcount N1 s' < 0; nonpos_upto N1 s'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; zcount N1 s' < 0; nonpos_upto N1 s'\<rbrakk> \<Longrightarrow> \<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)
[PROOF STEP]
apply (rule exI[of _ s'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; zcount N1 s' < 0; nonpos_upto N1 s'\<rbrakk> \<Longrightarrow> s' < t \<and> (zcount M s' < 0 \<or> zcount (N1 + N2) s' < 0) \<and> (\<forall>s'a<s'. zcount M s'a \<le> 0)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; zcount N1 s' < 0; nonpos_upto N1 s'\<rbrakk> \<Longrightarrow> s' < t
 2. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; zcount N1 s' < 0; nonpos_upto N1 s'\<rbrakk> \<Longrightarrow> zcount M s' < 0 \<or> zcount (N1 + N2) s' < 0
 3. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; zcount N1 s' < 0; nonpos_upto N1 s'\<rbrakk> \<Longrightarrow> \<forall>s'a<s'. zcount M s'a \<le> 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; zcount N1 s' < 0; nonpos_upto N1 s'\<rbrakk> \<Longrightarrow> zcount M s' < 0 \<or> zcount (N1 + N2) s' < 0
 2. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; zcount N1 s' < 0; nonpos_upto N1 s'\<rbrakk> \<Longrightarrow> \<forall>s'a<s'. zcount M s'a \<le> 0
[PROOF STEP]
apply (metis add_cancel_right_right add_neg_neg order.strict_implies_order nonpos_upto_def order_class.order.not_eq_order_implies_strict zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; zcount N1 s' < 0; nonpos_upto N1 s'\<rbrakk> \<Longrightarrow> \<forall>s'a<s'. zcount M s'a \<le> 0
[PROOF STEP]
apply (meson least less_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t'. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; t' < s; 0 < zcount C1 t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; zcount N1 s < zcount C1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; s' < s; 0 < zcount C1 s'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by (metis add_pos_nonneg assms(5) less_trans zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; zcount N1 s < zcount C1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; zcount N1 s < zcount C1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; zcount N1 s < zcount C1 s; \<not> ((\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp simp: not_le not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; zcount N1 s < zcount C1 s; \<forall>s<t. 0 \<le> zcount M s \<and> 0 \<le> zcount N1 s + zcount N2 s \<or> (\<exists>s'<s. 0 < zcount M s'); \<forall>s<t. zcount C1 s + zcount C2 s \<le> 0; zcount C1 t + zcount C2 t \<le> zcount M t + (zcount N1 t + zcount N2 t)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis (no_types, opaque_lifting) add_cancel_right_right add_neg_neg assms(4) assms(5) least less_trans not_less order_class.order.not_eq_order_implies_strict pos_add_strict)
[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 (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
apply (intro disjI1 exI[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> s < t \<and> (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)
[PROOF STEP]
apply (intro disjI2 conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> s < t
 2. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> zcount (N1 + N2) s < 0
 3. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> \<forall>s'<s. zcount M s' \<le> 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> zcount (N1 + N2) s < 0
 2. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> \<forall>s'<s. zcount M s' \<le> 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> \<forall>s'<s. zcount M s' \<le> 0
[PROOF STEP]
using least
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. zcount M t' \<le> 0

goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; zcount N2 s < 0; nonpos_upto N2 s; \<not> 0 < zcount N1 s\<rbrakk> \<Longrightarrow> \<forall>s'<s. zcount M s' \<le> 0
[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 (2 subgoals):
 1. \<And>t'. \<lbrakk>0 < zcount N2 t; t' < t; 0 < zcount C2 t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount N2 t; zcount N2 t < zcount C2 t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; s < t; 0 < zcount C2 s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by (metis add.comm_neutral add_mono_thms_linordered_field(4) assms(4) zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; zcount N2 t < zcount C2 t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; zcount N2 t < zcount C2 t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
zcount (M + N1) t < zcount C1 t

goal (1 subgoal):
 1. \<lbrakk>0 < zcount N2 t; zcount N2 t < zcount C2 t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t
[PROOF STEP]
by 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 (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N1 + N2) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + (N1 + N2)) t < zcount (C1 + C2) t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma justified_with_sum':
  assumes "finite X" "X\<noteq>{}"
    and   "\<forall>x\<in>X. 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> {}
\<forall>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> {}; \<forall>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>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<noteq> {}; \<forall>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 x F \<noteq> {}; \<forall>x\<in>insert x F. justified_with (C x) M (N x); \<forall>x\<in>insert x F. justified (C x) (N x); \<forall>x\<in>insert x F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert x F)) M (sum N (insert x F))
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<noteq> {}
\<forall>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> {}; \<forall>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>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<noteq> {}; \<forall>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 x F \<noteq> {}; \<forall>x\<in>insert x F. justified_with (C x) M (N x); \<forall>x\<in>insert x F. justified (C x) (N x); \<forall>x\<in>insert x F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert x F)) M (sum N (insert x F))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} \<noteq> {}
\<forall>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> {}
\<forall>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>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<noteq> {}; \<forall>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 x F \<noteq> {}; \<forall>x\<in>insert x F. justified_with (C x) M (N x); \<forall>x\<in>insert x F. justified (C x) (N x); \<forall>x\<in>insert x F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert x F)) M (sum N (insert x F))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<noteq> {}; \<forall>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 x F \<noteq> {}; \<forall>x\<in>insert x F. justified_with (C x) M (N x); \<forall>x\<in>insert x F. justified (C x) (N x); \<forall>x\<in>insert x F. \<forall>t. 0 \<le> zcount (C x) t\<rbrakk> \<Longrightarrow> justified_with (sum C (insert x F)) M (sum N (insert x F))
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
\<lbrakk>F \<noteq> {}; \<forall>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 x F \<noteq> {}
\<forall>x\<in>insert x F. justified_with (C x) M (N x)
\<forall>x\<in>insert x F. justified (C x) (N x)
\<forall>x\<in>insert x F. \<forall>t. 0 \<le> zcount (C x) t

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

goal (1 subgoal):
 1. F = {} \<Longrightarrow> justified_with (sum C (insert x F)) M (sum N (insert x F))
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> justified_with (sum C (insert x F)) M (sum N (insert x F))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> justified_with (sum C (insert x F)) M (sum N (insert x 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 x + sum C (F - {x})) M (N x + sum N (F - {x}))
[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 x + sum C (F - {x})) M (N x + sum N (F - {x}))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> justified_with (C x + sum C (F - {x})) M (N x + sum N (F - {x}))
[PROOF STEP]
using insert(2)
[PROOF STATE]
proof (prove)
using this:
x \<notin> F

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

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

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

goal (4 subgoals):
 1. \<lbrakk>F \<noteq> {}; x \<notin> F\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. justified (C x) (N x)
 2. \<lbrakk>F \<noteq> {}; x \<notin> F\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 3. \<lbrakk>F \<noteq> {}; x \<notin> F\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C x) t
 4. \<lbrakk>F \<noteq> {}; x \<notin> F\<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> {}; x \<notin> F\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 2. \<lbrakk>F \<noteq> {}; x \<notin> F\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C x) t
 3. \<lbrakk>F \<noteq> {}; x \<notin> F\<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 x F. \<forall>t. 0 \<le> zcount (C x) t

goal (3 subgoals):
 1. \<lbrakk>F \<noteq> {}; x \<notin> F\<rbrakk> \<Longrightarrow> \<forall>x\<in>F. \<forall>t. 0 \<le> zcount (C x) t
 2. \<lbrakk>F \<noteq> {}; x \<notin> F\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C x) t
 3. \<lbrakk>F \<noteq> {}; x \<notin> F\<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> {}; x \<notin> F\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C x) t
 2. \<lbrakk>F \<noteq> {}; x \<notin> F\<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 x F. \<forall>t. 0 \<le> zcount (C x) t

goal (2 subgoals):
 1. \<lbrakk>F \<noteq> {}; x \<notin> F\<rbrakk> \<Longrightarrow> \<forall>t. 0 \<le> zcount (C x) t
 2. \<lbrakk>F \<noteq> {}; x \<notin> F\<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> {}; x \<notin> F\<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> {}; x \<notin> F\<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> {}; x \<notin> F\<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> {}; x \<notin> F; xa \<in> F\<rbrakk> \<Longrightarrow> 0 \<le> zcount (C xa) t
[PROOF STEP]
using insert(7)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert x F. \<forall>t. 0 \<le> zcount (C x) t

goal (1 subgoal):
 1. \<And>t xa. \<lbrakk>F \<noteq> {}; x \<notin> F; 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:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
justified_with (sum C (insert x F)) M (sum N (insert x F))

goal:
No subgoals!
[PROOF STEP]
qed