[STATEMENT]
lemma justified_with_diff:
  assumes "justified_with C M N"
    and   "\<forall>t. 0 \<le> zcount C t"
    and   "\<forall>t. count \<Delta> t \<le> zcount C t"
    and   "justified C N"
  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]
proof (intro allI impI justified_with_leastI)
[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 (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>0 < zcount M t; \<forall>t'<t. zcount M t' \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>0 < zcount M t; \<forall>t'<t. zcount M t' \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 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 (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>0 < zcount M t; \<forall>t'<t. zcount M t' \<le> 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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" "\<forall>s<t. zcount M s \<ge> 0 \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0)" "\<forall>s<t. zcount N s \<ge> 0 \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0)" "zcount (M + N) t \<ge> zcount C t"  |
    "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; \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<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; \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<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; \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> ?thesis; zcount (M + N) t < zcount C 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 (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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; \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<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) \<and> (\<forall>s'<s. zcount M s' \<le> 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; \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
using diff_add_cancel zcount_union zcount_zmset_of_nonneg
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. zcount N s < 0 \<and> (\<forall>s'<s. zcount M s' \<le> 0)
?a - ?b + ?b = ?a
zcount (?M + ?N) ?a = zcount ?M ?a + zcount ?N ?a
0 \<le> zcount (zmset_of ?M) ?t

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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
\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0)
\<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0)
zcount C t \<le> zcount (M + N) t

goal (2 subgoals):
 1. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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
\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0)
\<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0)
zcount C t \<le> zcount (M + N) t
[PROOF STEP]
obtain s where s: "s < t" "0 < zcount C s" "\<forall>s'<s. zcount C s' = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. 0 < zcount C s
\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0)
\<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0)
zcount C t \<le> zcount (M + N) t

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s < t; 0 < zcount C s; \<forall>s'<s. zcount C s' = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s \<and> (\<forall>s'<s. zcount C s' = 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; s < t; 0 < zcount C s\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s \<and> (\<forall>s'<s. zcount C s' = 0)
[PROOF STEP]
apply (drule order_zmset_exists_foundation')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; s < t; \<exists>sa\<le>s. 0 < zcount C sa \<and> (\<forall>u<sa. zcount C u \<le> 0)\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s \<and> (\<forall>s'<s. zcount C s' = 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; s < t; sa \<le> s; 0 < zcount C sa; \<forall>u<sa. zcount C u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s \<and> (\<forall>s'<s. zcount C s' = 0)
[PROOF STEP]
subgoal for t' s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s \<and> (\<forall>s'<s. zcount C s' = 0)
[PROOF STEP]
apply (rule exI[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0\<rbrakk> \<Longrightarrow> s < t \<and> 0 < zcount C s \<and> (\<forall>s'<s. zcount C s' = 0)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0\<rbrakk> \<Longrightarrow> s < t
 2. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0\<rbrakk> \<Longrightarrow> 0 < zcount C s
 3. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0\<rbrakk> \<Longrightarrow> \<forall>s'<s. zcount C s' = 0
[PROOF STEP]
apply auto [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0\<rbrakk> \<Longrightarrow> \<forall>s'<s. zcount C s' = 0
[PROOF STEP]
apply (intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0; s' < s\<rbrakk> \<Longrightarrow> zcount C s' = 0
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0; s' < s\<rbrakk> \<Longrightarrow> zcount C s' = 0
[PROOF STEP]
using assms(2)[rule_format, of s']
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount C s'

goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t; t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0; s' < s\<rbrakk> \<Longrightarrow> zcount C s' = 0
[PROOF STEP]
by auto
[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:
s < t
0 < zcount C s
\<forall>s'<s. zcount C s' = 0

goal (2 subgoals):
 1. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
s < t
0 < zcount C s
\<forall>s'<s. zcount C s' = 0
[PROOF STEP]
consider
      "0 < zcount (C - zmset_of \<Delta>) s" |
      "zcount (C - zmset_of \<Delta>) s = 0" "zcount (N - zmset_of \<Delta>) s < 0" |
      "zcount (C - zmset_of \<Delta>) s = 0" "zcount (N - zmset_of \<Delta>) s = 0" |
      "zcount (C - zmset_of \<Delta>) s = 0" "zcount (N - zmset_of \<Delta>) s > 0"
[PROOF STATE]
proof (prove)
using this:
s < t
0 < zcount C s
\<forall>s'<s. zcount C s' = 0

goal (1 subgoal):
 1. \<lbrakk>0 < zcount (C - zmset_of \<Delta>) s \<Longrightarrow> thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms(3)[rule_format, of s]
[PROOF STATE]
proof (prove)
using this:
s < t
0 < zcount C s
\<forall>s'<s. zcount C s' = 0
int (count \<Delta> s) \<le> zcount C s

goal (1 subgoal):
 1. \<lbrakk>0 < zcount (C - zmset_of \<Delta>) s \<Longrightarrow> thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < zcount (C - zmset_of \<Delta>) s \<Longrightarrow> ?thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. \<lbrakk>\<exists>s<t. 0 < zcount C s; \<forall>s<t. 0 \<le> zcount M s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); \<forall>s<t. 0 \<le> zcount N s \<or> \<not> (\<forall>s'<s. zcount M s' \<le> 0); zcount C t \<le> zcount (M + N) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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>0 < zcount (C - zmset_of \<Delta>) s \<Longrightarrow> ?thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < zcount (C - zmset_of \<Delta>) s \<Longrightarrow> ?thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. 0 < zcount (C - zmset_of \<Delta>) s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
0 < zcount (C - zmset_of \<Delta>) s

goal (4 subgoals):
 1. 0 < zcount (C - zmset_of \<Delta>) s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
0 < zcount (C - zmset_of \<Delta>) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < zcount (C - zmset_of \<Delta>) s

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
using s
[PROOF STATE]
proof (prove)
using this:
0 < zcount (C - zmset_of \<Delta>) s
s < t
0 < zcount C s
\<forall>s'<s. zcount C s' = 0

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
zcount (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s < 0

goal (3 subgoals):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s < 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s < 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s < 0

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
using s least
[PROOF STATE]
proof (prove)
using this:
zcount (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s < 0
s < t
0 < zcount C s
\<forall>s'<s. zcount C s' = 0
\<forall>t'<t. zcount M t' \<le> 0

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 simp: nonpos_upto_def)
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
zcount (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s = 0

goal (2 subgoals):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 case3 = 3
[PROOF STATE]
proof (state)
this:
zcount (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s = 0

goal (2 subgoals):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 s(2)
[PROOF STATE]
proof (chain)
picking this:
0 < zcount C s
zcount (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s = 0
[PROOF STEP]
have Ns: "0 < zcount N s"
[PROOF STATE]
proof (prove)
using this:
0 < zcount C s
zcount (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s = 0

goal (1 subgoal):
 1. 0 < zcount N s
[PROOF STEP]
by (auto intro: ccontr simp: not_less)
[PROOF STATE]
proof (state)
this:
0 < zcount N s

goal (2 subgoals):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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(4)[unfolded justified_alt, rule_format, OF Ns]
[PROOF STATE]
proof (state)
this:
supported_strong N s \<or> (\<exists>t'<s. 0 < zcount C t') \<or> zcount N s < zcount C s

goal (2 subgoals):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
supported_strong N s \<or> (\<exists>t'<s. 0 < zcount C t') \<or> zcount N s < zcount C s
[PROOF STEP]
consider "supported_strong N s" | "\<exists>t'<s. 0 < zcount C t'" | "zcount N s < zcount C s"
[PROOF STATE]
proof (prove)
using this:
supported_strong N s \<or> (\<exists>t'<s. 0 < zcount C t') \<or> zcount N s < zcount C s

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

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

goal (2 subgoals):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (N - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>supported_strong N s \<Longrightarrow> ?thesis; \<exists>t'<s. 0 < zcount C t' \<Longrightarrow> ?thesis; zcount N s < zcount C s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>supported_strong N s \<Longrightarrow> ?thesis; \<exists>t'<s. 0 < zcount C t' \<Longrightarrow> ?thesis; zcount N s < zcount C s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 (3 subgoals):
 1. supported_strong N s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
supported_strong N s

goal (3 subgoals):
 1. supported_strong N s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
supported_strong N s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
supported_strong N s

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
unfolding supported_strong_def
[PROOF STATE]
proof (prove)
using this:
\<exists>sa<s. zcount N sa < 0 \<and> nonpos_upto N sa

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>sa < s; zcount N sa < 0; nonpos_upto N sa\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; zcount N s' < 0; nonpos_upto N s'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
using s(1,2) least
[PROOF STATE]
proof (prove)
using this:
s < t
0 < zcount C s
\<forall>t'<t. zcount M t' \<le> 0

goal (1 subgoal):
 1. \<lbrakk>s' < s; zcount N s' < 0; nonpos_upto N s'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 intro: exI[of _ s'] simp: nonpos_upto_def)
[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 - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t'

goal (2 subgoals):
 1. \<exists>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>t'<s. 0 < zcount C t'

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
using s(3)
[PROOF STATE]
proof (prove)
using this:
\<exists>t'<s. 0 < zcount C t'
\<forall>s'<s. zcount C s' = 0

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
zcount N s < zcount C s

goal (1 subgoal):
 1. zcount N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
from case3
[PROOF STATE]
proof (chain)
picking this:
zcount (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s = 0
[PROOF STEP]
have "zcount C s = zcount N s"
[PROOF STATE]
proof (prove)
using this:
zcount (C - zmset_of \<Delta>) s = 0
zcount (N - zmset_of \<Delta>) s = 0

goal (1 subgoal):
 1. zcount C s = zcount N s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zcount C s = zcount N s

goal (1 subgoal):
 1. zcount N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 3
[PROOF STATE]
proof (chain)
picking this:
zcount N s < zcount C s
zcount C s = zcount N s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount N s < zcount C s
zcount C s = zcount N s

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 linarith
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 (C - zmset_of \<Delta>) s = 0
0 < zcount (N - zmset_of \<Delta>) s

goal (1 subgoal):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 (C - zmset_of \<Delta>) s = 0
0 < zcount (N - zmset_of \<Delta>) s
[PROOF STEP]
have Ns: "0 < zcount N s"
[PROOF STATE]
proof (prove)
using this:
zcount (C - zmset_of \<Delta>) s = 0
0 < zcount (N - zmset_of \<Delta>) s

goal (1 subgoal):
 1. 0 < zcount N s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < zcount N s

goal (1 subgoal):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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(4)[unfolded justified_alt, rule_format, OF Ns]
[PROOF STATE]
proof (state)
this:
supported_strong N s \<or> (\<exists>t'<s. 0 < zcount C t') \<or> zcount N s < zcount C s

goal (1 subgoal):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
supported_strong N s \<or> (\<exists>t'<s. 0 < zcount C t') \<or> zcount N s < zcount C s
[PROOF STEP]
consider "supported_strong N s" | "\<exists>t'<s. 0 < zcount C t'" | "zcount N s < zcount C s"
[PROOF STATE]
proof (prove)
using this:
supported_strong N s \<or> (\<exists>t'<s. 0 < zcount C t') \<or> zcount N s < zcount C s

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

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

goal (1 subgoal):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (N - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>supported_strong N s \<Longrightarrow> ?thesis; \<exists>t'<s. 0 < zcount C t' \<Longrightarrow> ?thesis; zcount N s < zcount C s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>supported_strong N s \<Longrightarrow> ?thesis; \<exists>t'<s. 0 < zcount C t' \<Longrightarrow> ?thesis; zcount N s < zcount C s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 (3 subgoals):
 1. supported_strong N s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
supported_strong N s

goal (3 subgoals):
 1. supported_strong N s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
supported_strong N s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
supported_strong N s

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
unfolding supported_strong_def
[PROOF STATE]
proof (prove)
using this:
\<exists>sa<s. zcount N sa < 0 \<and> nonpos_upto N sa

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>sa < s; zcount N sa < 0; nonpos_upto N sa\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; zcount N s' < 0; nonpos_upto N s'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
using s(1,2) least
[PROOF STATE]
proof (prove)
using this:
s < t
0 < zcount C s
\<forall>t'<t. zcount M t' \<le> 0

goal (1 subgoal):
 1. \<lbrakk>s' < s; zcount N s' < 0; nonpos_upto N s'\<rbrakk> \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 intro: exI[of _ s'] simp: nonpos_upto_def)
[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 - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t'

goal (2 subgoals):
 1. \<exists>t'<s. 0 < zcount C t' \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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>t'<s. 0 < zcount C t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>t'<s. 0 < zcount C t'

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
using s(3)
[PROOF STATE]
proof (prove)
using this:
\<exists>t'<s. 0 < zcount C t'
\<forall>s'<s. zcount C s' = 0

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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:
zcount N s < zcount C s

goal (1 subgoal):
 1. zcount N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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]
have "zcount C s = zcount N s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount C s = zcount N s
[PROOF STEP]
using 3 4(1,2)
[PROOF STATE]
proof (prove)
using this:
zcount N s < zcount C s
zcount (C - zmset_of \<Delta>) s = 0
0 < zcount (N - zmset_of \<Delta>) s

goal (1 subgoal):
 1. zcount C s = zcount N s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zcount C s = zcount N s

goal (1 subgoal):
 1. zcount N s < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 3
[PROOF STATE]
proof (chain)
picking this:
zcount N s < zcount C s
zcount C s = zcount N s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount N s < zcount C s
zcount C s = zcount N s

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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 linarith
[PROOF STATE]
proof (state)
this:
(\<exists>s<t. (zcount M s < 0 \<or> zcount (N - zmset_of \<Delta>) s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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) \<and> (\<forall>s'<s. zcount M s' \<le> 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 PositiveImplies_justified_with:
  assumes "justified C (M+N)"
    and   "PositiveImplies M (M+N)"
  shows   "justified_with C M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with C M N
[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 s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply (intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply (drule assms(2)[unfolded PositiveImplies_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. 0 < zcount (M + N) t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply (frule assms(1)[unfolded justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount (M + N) t; (\<exists>s<t. zcount (M + N) s < 0 \<and> nonpos_upto (M + N) s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + N) t < zcount C t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>0 < zcount (M + N) t; \<exists>s<t. zcount (M + N) s < 0 \<and> nonpos_upto (M + N) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
 2. \<And>t. \<lbrakk>0 < zcount (M + N) t; \<exists>t'<t. 0 < zcount C t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
 3. \<And>t. \<lbrakk>0 < zcount (M + N) t; zcount (M + N) t < zcount C t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
subgoal for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M + N) t; \<exists>s<t. zcount (M + N) s < 0 \<and> nonpos_upto (M + N) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply (intro disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M + N) t; \<exists>s<t. zcount (M + N) s < 0 \<and> nonpos_upto (M + N) s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<or> zcount N s < 0
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < zcount (M + N) t; s < t \<and> zcount (M + N) s < 0 \<and> nonpos_upto (M + N) s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<or> zcount N s < 0
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M + N) t; s < t \<and> zcount (M + N) s < 0 \<and> nonpos_upto (M + N) s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<or> zcount N s < 0
[PROOF STEP]
apply (clarsimp 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 (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>0 < zcount (M + N) t; \<exists>t'<t. 0 < zcount C t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
 2. \<And>t. \<lbrakk>0 < zcount (M + N) t; zcount (M + N) t < zcount C t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
subgoal for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M + N) t; \<exists>t'<t. 0 < zcount C t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
using less_imp_le
[PROOF STATE]
proof (prove)
using this:
?x < ?y \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M + N) t; \<exists>t'<t. 0 < zcount C t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount (M + N) t; zcount (M + N) t < zcount C t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
subgoal for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M + N) t; zcount (M + N) t < zcount C t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
by (intro disjI2 exI[of _ t]) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma justified_with_add_zmset[simp]:
  assumes "justified_with C M N"
  shows   "justified_with (add_zmset c C) M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (add_zmset c C) M N
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
justified_with C M N

goal (1 subgoal):
 1. justified_with (add_zmset c C) M N
[PROOF STEP]
apply (subst add_zmset_add_single)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with C M N \<Longrightarrow> justified_with (C + {#c#}\<^sub>z) M N
[PROOF STEP]
apply (rule justified_with_add_records)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. justified_with C M N \<Longrightarrow> justified_with C M N
 2. justified_with C M N \<Longrightarrow> \<forall>t. 0 \<le> zcount {#c#}\<^sub>z t
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma next_performop'_preserves_justified_with:
  assumes "justified_with (c_caps c0 p) M N"
    and   "next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self"
    and   "\<forall>t. 0 \<le> zcount (c_caps c0 p) t"
    and   "justified (c_caps c0 p) N"
  shows   "justified_with (c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) M (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg) - zmset_of \<Delta>neg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) M (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg) - zmset_of \<Delta>neg)
[PROOF STEP]
apply (rule justified_with_diff)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. justified_with (c_caps c0 p + zmset_of \<Delta>mint_self) M (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 3. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply (rule justified_with_add_msg_delta)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. justified_with (c_caps c0 p + zmset_of \<Delta>mint_self) M (N + zmset_of \<Delta>mint_self)
 2. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 5. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 6. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply (rule justified_with_add_same)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. justified_with (c_caps c0 p) M N
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 3. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 4. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 5. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 6. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 7. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
justified_with (c_caps c0 p) M N

goal (7 subgoals):
 1. justified_with (c_caps c0 p) M N
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 3. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 4. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 5. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 6. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 7. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 2. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 5. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 6. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount (c_caps c0 p) t

goal (6 subgoals):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 2. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 5. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 6. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 5. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply (rule minting_msg_add_records)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. minting_msg (c_caps c0 p) \<Delta>mint_msg
 2. \<forall>t. 0 \<le> zcount (zmset_of \<Delta>mint_self) t
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 5. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 6. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
using next_performopD(4)[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
minting_msg (c_caps c0 p) \<Delta>mint_msg

goal (6 subgoals):
 1. minting_msg (c_caps c0 p) \<Delta>mint_msg
 2. \<forall>t. 0 \<le> zcount (zmset_of \<Delta>mint_self) t
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 5. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 6. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<forall>t. 0 \<le> zcount (zmset_of \<Delta>mint_self) t
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 5. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 3. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount (c_caps c0 p) t

goal (4 subgoals):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 3. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 4. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 2. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 3. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount (c_caps c0 p) t

goal (3 subgoals):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 2. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 3. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 2. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
using next_performopD(2)[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t

goal (2 subgoals):
 1. \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
 2. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply (simp add: add.commute add_increasing)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg))
[PROOF STEP]
apply (rule justified_add_msg_delta)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. justified (c_caps c0 p + zmset_of \<Delta>mint_self) (N + zmset_of \<Delta>mint_self)
 2. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
apply (rule justified_add_same)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. justified (c_caps c0 p) N
 2. minting_self (c_caps c0 p) \<Delta>mint_self
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 4. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 5. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
justified (c_caps c0 p) N

goal (5 subgoals):
 1. justified (c_caps c0 p) N
 2. minting_self (c_caps c0 p) \<Delta>mint_self
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 4. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 5. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. minting_self (c_caps c0 p) \<Delta>mint_self
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 3. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 4. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
using next_performopD(3)[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
minting_self (c_caps c0 p) \<Delta>mint_self

goal (4 subgoals):
 1. minting_self (c_caps c0 p) \<Delta>mint_self
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 3. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 4. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 2. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount (c_caps c0 p) t

goal (3 subgoals):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 2. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. minting_msg (c_caps c0 p + zmset_of \<Delta>mint_self) \<Delta>mint_msg
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
apply (rule minting_msg_add_records)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. minting_msg (c_caps c0 p) \<Delta>mint_msg
 2. \<forall>t. 0 \<le> zcount (zmset_of \<Delta>mint_self) t
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
using next_performopD(4)[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
minting_msg (c_caps c0 p) \<Delta>mint_msg

goal (3 subgoals):
 1. minting_msg (c_caps c0 p) \<Delta>mint_msg
 2. \<forall>t. 0 \<le> zcount (zmset_of \<Delta>mint_self) t
 3. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>t. 0 \<le> zcount (zmset_of \<Delta>mint_self) t
 2. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount (c_caps c0 p) t

goal (1 subgoal):
 1. \<forall>t. 0 \<le> zcount (c_caps c0 p + zmset_of \<Delta>mint_self) t
[PROOF STEP]
apply (simp add: add.commute add_increasing)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma init_config_implies_InvRecordCount: "init_config c \<Longrightarrow> InvRecordCount c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init_config c \<Longrightarrow> InvRecordCount c
[PROOF STEP]
by (simp add: InvRecordCount_def init_config_def GlobalIncomingInfo_def IncomingInfo_def)