[STATEMENT]
lemma justified_add_same:
  assumes "justified C M"
    and   "minting_self C \<Delta>"
    and   "\<forall>t. 0 \<le> zcount C t"
  shows   "justified (C + zmset_of \<Delta>) (M + zmset_of \<Delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified (C + zmset_of \<Delta>) (M + zmset_of \<Delta>)
[PROOF STEP]
proof (intro allI impI justified_leastI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount (M + zmset_of \<Delta>) t; \<forall>t'<t. zcount (M + zmset_of \<Delta>) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + 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 + zmset_of \<Delta>) t; \<forall>t'<t. zcount (M + zmset_of \<Delta>) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
assume t: "0 < zcount (M + zmset_of \<Delta>) t"
[PROOF STATE]
proof (state)
this:
0 < zcount (M + zmset_of \<Delta>) t

goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount (M + zmset_of \<Delta>) t; \<forall>t'<t. zcount (M + zmset_of \<Delta>) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
assume least: "\<forall>t'<t. zcount (M + zmset_of \<Delta>) t' \<le> 0"
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. zcount (M + zmset_of \<Delta>) t' \<le> 0

goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount (M + zmset_of \<Delta>) t; \<forall>t'<t. zcount (M + zmset_of \<Delta>) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
from t
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (M + zmset_of \<Delta>) t
[PROOF STEP]
consider
    "0 < zcount M t" |
    "0 < zcount (zmset_of \<Delta>) t" "zcount M t \<le> 0"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (M + zmset_of \<Delta>) t

goal (1 subgoal):
 1. \<lbrakk>0 < zcount M t \<Longrightarrow> thesis; \<lbrakk>0 < zcount (zmset_of \<Delta>) t; zcount M t \<le> 0\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim (auto simp: not_less count_inI)
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < zcount M t \<Longrightarrow> ?thesis; \<lbrakk>0 < zcount (zmset_of \<Delta>) t; zcount M t \<le> 0\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < zcount M t \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
 2. \<lbrakk>0 < zcount (zmset_of \<Delta>) t; zcount M t \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
0 < zcount M t

goal (2 subgoals):
 1. 0 < zcount M t \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
 2. \<lbrakk>0 < zcount (zmset_of \<Delta>) t; zcount M t \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
note assms(1)[unfolded justified_alt, rule_format, OF 1]
[PROOF STATE]
proof (state)
this:
supported_strong M t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t

goal (2 subgoals):
 1. 0 < zcount M t \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
 2. \<lbrakk>0 < zcount (zmset_of \<Delta>) t; zcount M t \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supported_strong M t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
[PROOF STEP]
consider
      "supported_strong M t" |
      "\<exists>t'<t. 0 < zcount C t'" |
      "zcount M t < zcount C t"
[PROOF STATE]
proof (prove)
using this:
supported_strong M t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t

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

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

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

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

goal (1 subgoal):
 1. supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
unfolding supported_strong_def
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s

goal (1 subgoal):
 1. (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + 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>s. \<lbrakk>s < t; zcount M s < 0; nonpos_upto M s\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
subgoal for t'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
apply (cases "\<exists>s\<le>t'. zcount (zmset_of \<Delta>) s > 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
 2. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; s \<le> t'; 0 < zcount (zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
 2. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; s \<le> t'; 0 < zcount (zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; s \<le> t'; s \<in># \<Delta>\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s + int (count \<Delta> s) < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount C t' + int (count \<Delta> t')) \<or> zcount M t < zcount C t
[PROOF STEP]
apply (drule assms(2)[unfolded minting_self_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; s \<le> t'; \<exists>t'\<le>s. 0 < zcount C t'\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s + int (count \<Delta> s) < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount C t' + int (count \<Delta> t')) \<or> zcount M t < zcount C t
[PROOF STEP]
apply (smt (z3) order.strict_trans1 of_nat_0_le_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M + zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M + zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
apply (intro disjI1 exI[of _ t'] conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> t' < t
 2. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> zcount (M + zmset_of \<Delta>) t' < 0
 3. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> nonpos_upto (M + zmset_of \<Delta>) t'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> zcount (M + zmset_of \<Delta>) t' < 0
 2. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> nonpos_upto (M + zmset_of \<Delta>) t'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<forall>s\<le>t'. s \<notin># \<Delta>\<rbrakk> \<Longrightarrow> zcount M t' + int (count \<Delta> t') < 0
 2. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> nonpos_upto (M + zmset_of \<Delta>) t'
[PROOF STEP]
apply (metis add_cancel_right_left add_mono_thms_linordered_field(1) count_eq_zero_iff order.order_iff_strict of_nat_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> nonpos_upto (M + zmset_of \<Delta>) t'
[PROOF STEP]
using least nonpos_upto_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. zcount (M + zmset_of \<Delta>) t' \<le> 0
nonpos_upto ?a ?t = (\<forall>s\<le>?t. zcount ?a s \<le> 0)

goal (1 subgoal):
 1. \<lbrakk>t' < t; zcount M t' < 0; nonpos_upto M t'; \<not> (\<exists>s\<le>t'. 0 < zcount (zmset_of \<Delta>) s)\<rbrakk> \<Longrightarrow> nonpos_upto (M + zmset_of \<Delta>) t'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>0 < zcount (zmset_of \<Delta>) t; zcount M t \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (zmset_of \<Delta>) t; zcount M t \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
0 < zcount (zmset_of \<Delta>) t
zcount M t \<le> 0

goal (1 subgoal):
 1. \<lbrakk>0 < zcount (zmset_of \<Delta>) t; zcount M t \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (zmset_of \<Delta>) t
zcount M t \<le> 0
[PROOF STEP]
obtain t' where t': "t' \<le> t" "0 < zcount C t'"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (zmset_of \<Delta>) t
zcount M t \<le> 0

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<le> t; 0 < zcount C t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)[unfolded minting_self_def]
[PROOF STATE]
proof (prove)
using this:
0 < zcount (zmset_of \<Delta>) t
zcount M t \<le> 0
\<forall>t\<in>#\<Delta>. \<exists>t'\<le>t. 0 < zcount C t'

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

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

goal (1 subgoal):
 1. supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
apply (cases "t'=t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t' \<le> t; 0 < zcount C t'; t' = t\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
 2. \<lbrakk>t' \<le> t; 0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<le> t; 0 < zcount C t'; t' = t\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
using 2(2)
[PROOF STATE]
proof (prove)
using this:
zcount M t \<le> 0

goal (1 subgoal):
 1. \<lbrakk>t' \<le> t; 0 < zcount C t'; t' = t\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<le> t; 0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<le> t; 0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t
[PROOF STEP]
apply (rule disjI2, rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<le> t; 0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t'
[PROOF STEP]
using assms(3) order.not_eq_order_implies_strict
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount C t
\<lbrakk>?a \<noteq> ?b; ?a \<le> ?b\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. \<lbrakk>t' \<le> t; 0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t'
[PROOF STEP]
apply fastforce
[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:
supported_strong (M + zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C + zmset_of \<Delta>) t') \<or> zcount (M + zmset_of \<Delta>) t < zcount (C + zmset_of \<Delta>) t

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma justified_with_add_records:
  assumes "justified_with C1 M N"
    and   "\<forall>t. 0 \<le> zcount C2 t"
  shows   "justified_with (C1+C2) M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (C1 + C2) 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 (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) 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 (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule assms(1)[unfolded justified_with_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C1 s) \<or> zcount (M + N) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<exists>s<t. zcount M s < 0 \<or> zcount N s < 0 \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
 2. \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
 3. zcount (M + N) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s<t. zcount M s < 0 \<or> zcount N s < 0 \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
 2. zcount (M + N) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s<t. 0 < zcount C1 s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s < t \<and> 0 < zcount C1 s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < t \<and> 0 < zcount C1 s \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI2, rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < t \<and> 0 < zcount C1 s \<Longrightarrow> \<exists>s<t. 0 < zcount (C1 + C2) s
[PROOF STEP]
using assms(2)[rule_format, of s]
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount C2 s

goal (1 subgoal):
 1. s < t \<and> 0 < zcount C1 s \<Longrightarrow> \<exists>s<t. 0 < zcount (C1 + C2) s
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (M + N) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (M + N) t < zcount C1 t \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount (C1 + C2) s) \<or> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
apply (intro disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (M + N) t < zcount C1 t \<Longrightarrow> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
using assms(2)[rule_format, of t]
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount C2 t

goal (1 subgoal):
 1. zcount (M + N) t < zcount C1 t \<Longrightarrow> zcount (M + N) t < zcount (C1 + C2) t
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma justified_with_leastI:
  assumes
    "(\<forall>t. 0 < zcount M t \<longrightarrow> (\<forall>t'<t. zcount M t' \<le> 0) \<longrightarrow>
       (\<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)"
  shows   "justified_with C M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with C M N
[PROOF STEP]
unfolding justified_with_alt
[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) \<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]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N 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]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N 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]
assume t: "0 < zcount M t"
[PROOF STATE]
proof (state)
this:
0 < zcount M t

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

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<le> t; 0 < zcount M t'; \<forall>s<t'. zcount M s \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim (drule order_zmset_exists_foundation')
[PROOF STATE]
proof (state)
this:
t' \<le> t
0 < zcount M t'
\<forall>s<t'. zcount M s \<le> 0

goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<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]
note assms[rule_format, OF t'(2)]
[PROOF STATE]
proof (state)
this:
(\<And>t'a. t'a < t' \<Longrightarrow> zcount M t'a \<le> 0) \<Longrightarrow> (\<exists>s<t'. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t'. 0 < zcount C s) \<or> zcount (M + N) t' < zcount C t'

goal (1 subgoal):
 1. \<And>t. 0 < zcount M t \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N 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]
with t'(3)
[PROOF STATE]
proof (chain)
picking this:
\<forall>s<t'. zcount M s \<le> 0
(\<And>t'a. t'a < t' \<Longrightarrow> zcount M t'a \<le> 0) \<Longrightarrow> (\<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 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)" |
    "\<exists>s<t'. 0 < zcount C s" |
    "zcount (M+N) t' < zcount C t'"
[PROOF STATE]
proof (prove)
using this:
\<forall>s<t'. zcount M s \<le> 0
(\<And>t'a. t'a < t' \<Longrightarrow> zcount M t'a \<le> 0) \<Longrightarrow> (\<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 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t'. 0 < zcount C s \<Longrightarrow> thesis; zcount (M + N) t' < zcount C t' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using not_less
[PROOF STATE]
proof (prove)
using this:
\<forall>s<t'. zcount M s \<le> 0
(\<And>t'a. t'a < t' \<Longrightarrow> zcount M t'a \<le> 0) \<Longrightarrow> (\<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 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> thesis; \<exists>s<t'. 0 < zcount C s \<Longrightarrow> thesis; zcount (M + N) t' < zcount C t' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>s<t'. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> ?thesis; \<exists>s<t'. 0 < zcount C s \<Longrightarrow> ?thesis; zcount (M + N) t' < zcount C t' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount N 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]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<exists>s<t'. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<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
 2. \<exists>s<t'. 0 < zcount C s \<Longrightarrow> (\<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
 3. zcount (M + N) t' < zcount C t' \<Longrightarrow> (\<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]
case 1
[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)

goal (3 subgoals):
 1. \<exists>s<t'. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0) \<Longrightarrow> (\<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
 2. \<exists>s<t'. 0 < zcount C s \<Longrightarrow> (\<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
 3. zcount (M + N) t' < zcount C t' \<Longrightarrow> (\<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]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t'. (zcount M s < 0 \<or> 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 M s < 0 \<or> 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 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]
using order.strict_trans2 t'(1)
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t'. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c
t' \<le> t

goal (1 subgoal):
 1. (\<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]
by blast
[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 (2 subgoals):
 1. \<exists>s<t'. 0 < zcount C s \<Longrightarrow> (\<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
 2. zcount (M + N) t' < zcount C t' \<Longrightarrow> (\<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]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>s<t'. 0 < zcount C s \<Longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N 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
 2. zcount (M + N) t' < zcount C t' \<Longrightarrow> (\<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]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>s<t'. 0 < zcount C s

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

goal (1 subgoal):
 1. (\<exists>s<t. (zcount M s < 0 \<or> zcount N 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]
using order.strict_trans2 t'(1)
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t'. 0 < zcount C s
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c
t' \<le> t

goal (1 subgoal):
 1. (\<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]
by blast
[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. zcount (M + N) t' < zcount C t' \<Longrightarrow> (\<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]
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 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]
case 3
[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 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]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (M + N) t' < zcount C t'
[PROOF STEP]
consider
      "zcount (M+N) t' < 0" |
      "zcount C t' > 0"
[PROOF STATE]
proof (prove)
using this:
zcount (M + N) t' < zcount C t'

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

goal (1 subgoal):
 1. zcount (M + N) t' < zcount C t' \<Longrightarrow> (\<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]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>zcount (M + N) t' < 0 \<Longrightarrow> ?thesis; 0 < zcount C t' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>zcount (M + N) t' < 0 \<Longrightarrow> ?thesis; 0 < zcount C t' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<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]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. zcount (M + N) t' < 0 \<Longrightarrow> (\<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
 2. 0 < zcount C t' \<Longrightarrow> (\<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]
case 1
[PROOF STATE]
proof (state)
this:
zcount (M + N) t' < 0

goal (2 subgoals):
 1. zcount (M + N) t' < 0 \<Longrightarrow> (\<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
 2. 0 < zcount C t' \<Longrightarrow> (\<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]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (M + N) t' < 0
[PROOF STEP]
have "zcount N t' < 0"
[PROOF STATE]
proof (prove)
using this:
zcount (M + N) t' < 0

goal (1 subgoal):
 1. zcount N t' < 0
[PROOF STEP]
using t'(2)
[PROOF STATE]
proof (prove)
using this:
zcount (M + N) t' < 0
0 < zcount M t'

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

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

goal (1 subgoal):
 1. (\<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]
apply (cases "t'=t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>s<t'. zcount M s \<le> 0; zcount N t' < 0; t' = t\<rbrakk> \<Longrightarrow> (\<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
 2. \<lbrakk>\<forall>s<t'. zcount M s \<le> 0; zcount N t' < 0; t' \<noteq> t\<rbrakk> \<Longrightarrow> (\<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]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t'. zcount M s \<le> 0; zcount N t' < 0; t' = t\<rbrakk> \<Longrightarrow> (\<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]
using 3(1)
[PROOF STATE]
proof (prove)
using this:
zcount (M + N) t' < zcount C t'

goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t'. zcount M s \<le> 0; zcount N t' < 0; t' = t\<rbrakk> \<Longrightarrow> (\<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]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t'. zcount M s \<le> 0; zcount N t' < 0; t' \<noteq> t\<rbrakk> \<Longrightarrow> (\<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]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t'. zcount M s \<le> 0; zcount N t' < 0; t' \<noteq> t\<rbrakk> \<Longrightarrow> (\<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]
using t'(1)
[PROOF STATE]
proof (prove)
using this:
t' \<le> t

goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t'. zcount M s \<le> 0; zcount N t' < 0; t' \<noteq> t\<rbrakk> \<Longrightarrow> (\<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]
by (auto intro: exI[of _ t'])
[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 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. 0 < zcount C t' \<Longrightarrow> (\<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]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < zcount C t' \<Longrightarrow> (\<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]
case 2
[PROOF STATE]
proof (state)
this:
0 < zcount C t'

goal (1 subgoal):
 1. 0 < zcount C t' \<Longrightarrow> (\<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]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount C t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < zcount C t'

goal (1 subgoal):
 1. (\<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]
apply (cases "t'=t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount C t'; t' = t\<rbrakk> \<Longrightarrow> (\<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
 2. \<lbrakk>0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> (\<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]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount C t'; t' = t\<rbrakk> \<Longrightarrow> (\<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]
apply (intro disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount C t'; t' = t\<rbrakk> \<Longrightarrow> zcount (M + N) t < zcount C t
[PROOF STEP]
using 3(1)
[PROOF STATE]
proof (prove)
using this:
zcount (M + N) t' < zcount C t'

goal (1 subgoal):
 1. \<lbrakk>0 < zcount C t'; t' = t\<rbrakk> \<Longrightarrow> zcount (M + N) t < zcount C t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> (\<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]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> (\<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]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
using order.not_eq_order_implies_strict t'(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<noteq> ?b; ?a \<le> ?b\<rbrakk> \<Longrightarrow> ?a < ?b
t' \<le> t

goal (1 subgoal):
 1. \<lbrakk>0 < zcount C t'; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[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:
No subgoals!
[PROOF STEP]
qed
[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:
No subgoals!
[PROOF STEP]
qed
[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:
No subgoals!
[PROOF STEP]
qed