[STATEMENT]
lemma justified_leastI:
  assumes "\<forall>t. 0 < zcount M t \<longrightarrow> (\<forall>t'<t. zcount M t' \<le> 0) \<longrightarrow> supported_strong M t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> (zcount M t < zcount C t)"
  shows   "justified C M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified C M
[PROOF STEP]
unfolding justified_alt supported_strong_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M 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 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
[PROOF STEP]
apply (drule order_zmset_exists_foundation)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s) \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t s. \<lbrakk>s \<le> t; 0 < zcount M s; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
[PROOF STEP]
subgoal for t' s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> t'; 0 < zcount M s; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
apply (drule assms(1)[unfolded supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t'a. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; t'a < s\<rbrakk> \<Longrightarrow> zcount M t'a \<le> 0
 2. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa) \<or> (\<exists>t'<s. 0 < zcount C t') \<or> zcount M s < zcount C s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
apply (auto intro: ccontr) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa) \<or> (\<exists>t'<s. 0 < zcount C t') \<or> zcount M s < zcount C s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
apply (elim disj3_split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
 2. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa) \<and> (\<exists>t'<s. 0 < zcount C t')\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
 3. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa); \<not> (\<exists>t'<s. 0 < zcount C t'); zcount M s < zcount C s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa\<rbrakk> \<Longrightarrow> \<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s
 2. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa) \<and> (\<exists>t'<s. 0 < zcount C t')\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
 3. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa); \<not> (\<exists>t'<s. 0 < zcount C t'); zcount M s < zcount C s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
using order.strict_trans2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c

goal (3 subgoals):
 1. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa\<rbrakk> \<Longrightarrow> \<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s
 2. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa) \<and> (\<exists>t'<s. 0 < zcount C t')\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
 3. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa); \<not> (\<exists>t'<s. 0 < zcount C t'); zcount M s < zcount C s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa) \<and> (\<exists>t'<s. 0 < zcount C t')\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
 2. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa); \<not> (\<exists>t'<s. 0 < zcount C t'); zcount M s < zcount C s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
apply (rule disjI2, rule disjI1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa) \<and> (\<exists>t'<s. 0 < zcount C t')\<rbrakk> \<Longrightarrow> \<exists>t'a<t'. 0 < zcount C t'a
 2. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa); \<not> (\<exists>t'<s. 0 < zcount C t'); zcount M s < zcount C s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
using order.strict_trans2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c

goal (2 subgoals):
 1. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa) \<and> (\<exists>t'<s. 0 < zcount C t')\<rbrakk> \<Longrightarrow> \<exists>t'a<t'. 0 < zcount C t'a
 2. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa); \<not> (\<exists>t'<s. 0 < zcount C t'); zcount M s < zcount C s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<not> (\<exists>sa<s. zcount M sa < 0 \<and> nonpos_upto M sa); \<not> (\<exists>t'<s. 0 < zcount C t'); zcount M s < zcount C s\<rbrakk> \<Longrightarrow> (\<exists>s<t'. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'a<t'. 0 < zcount C t'a) \<or> zcount M t' < zcount C t'
[PROOF STEP]
apply (clarsimp simp: nonpos_upto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> t'; \<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s; \<forall>t'<s. \<not> 0 < zcount C t'; zcount M s < zcount C s; \<forall>s. zcount M s < 0 \<longrightarrow> s < t' \<longrightarrow> (\<exists>sa\<le>s. \<not> zcount M sa \<le> 0); \<not> zcount M t' < zcount C t'\<rbrakk> \<Longrightarrow> \<exists>t'a<t'. 0 < zcount C t'a
[PROOF STEP]
apply (metis le_less_linear linear le_imp_less_or_eq preorder_class.le_less_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma justified_add:
  assumes "justified C1 M1"
    and   "justified C2 M2"
    and   "\<forall>t. 0 \<le> zcount C1 t"
    and   "\<forall>t. 0 \<le> zcount C2 t"
  shows   "justified (C1+C2) (M1+M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified (C1 + C2) (M1 + M2)
[PROOF STEP]
apply (rule justified_leastI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 < zcount (M1 + M2) t \<longrightarrow> (\<forall>t'<t. zcount (M1 + M2) t' \<le> 0) \<longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "0 < zcount M1 t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; 0 < zcount M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
(* symmetric cases *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; 0 < zcount M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; 0 < zcount M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule assms(1)[unfolded justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s) \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim disj3_split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s) \<and> (\<exists>t'<t. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 3. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; zcount M1 s < 0; nonpos_upto M1 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule order_zmset_exists_foundation_neg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; \<exists>sa\<le>s. zcount M1 sa < 0 \<and> (\<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < sa)\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; sa \<le> s; zcount M1 sa < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < sa\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for s s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
(* anything less than s' is 0 in M1 *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "zcount (M1 + M2) s' < 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
apply (auto intro!: exI[of _ s'] simp: nonpos_upto_def supported_strong_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (subst (asm) not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "0 < zcount M2 s'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; 0 < zcount M2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> 0 < zcount M2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> 0 < zcount M2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; 0 < zcount M2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> 0 < zcount M2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; 0 < zcount M2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
(* trivial contradiction *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; 0 < zcount M2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; 0 < zcount M2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule assms(2)[unfolded justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s) \<or> (\<exists>t'<s'. 0 < zcount C2 t') \<or> zcount M2 s' < zcount C2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim disj3_split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s) \<and> (\<exists>t'<s'. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 3. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<s'. 0 < zcount C2 t'); zcount M2 s' < zcount C2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; sa < s' \<and> zcount M2 sa < 0 \<and> nonpos_upto M2 sa\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
subgoal for s''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; s'' < s' \<and> zcount M2 s'' < 0 \<and> nonpos_upto M2 s''\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
by (auto intro!: exI[of _ s''] simp: nonpos_upto_def supported_strong_def add_nonpos_neg)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s) \<and> (\<exists>t'<s'. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<s'. 0 < zcount C2 t'); zcount M2 s' < zcount C2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s) \<and> (\<exists>t'<s'. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI2, rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s) \<and> (\<exists>t'<s'. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C1 + C2) t'
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s); t' < s'; 0 < zcount C2 t'\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C1 + C2) t'
[PROOF STEP]
subgoal for s''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s); s'' < s'; 0 < zcount C2 s''\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C1 + C2) t'
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount C1 t

goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s); s'' < s'; 0 < zcount C2 s''\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C1 + C2) t'
[PROOF STEP]
by (auto simp: add_nonneg_pos intro!: exI[of _ s''])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<s'. 0 < zcount C2 t'); zcount M2 s' < zcount C2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; s < t; nonpos_upto M1 s; s' \<le> s; zcount M1 s' < 0; \<forall>u. zcount M1 u < 0 \<longrightarrow> \<not> u < s'; 0 \<le> zcount (M1 + M2) s'; \<not> (\<exists>s<s'. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<s'. 0 < zcount C2 t'); zcount M2 s' < zcount C2 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
by (metis add.right_neutral add_strict_increasing2 assms(3) less_add_same_cancel1 order.strict_trans1 pos_add_strict zcount_union)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (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. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s) \<and> (\<exists>t'<t. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s) \<and> (\<exists>t'<t. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
by (metis add.commute add_mono_thms_linordered_field(4) assms(4) add_0 zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "supported_strong M2 t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; supported_strong M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<not> supported_strong M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; supported_strong M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; supported_strong M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
using assms(1)[unfolded justified_alt]
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t

goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; supported_strong M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
apply (subst supported_strong_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; supported_strong M2 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount (M1 + M2) s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply (subst (asm) supported_strong_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount (M1 + M2) s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount (M1 + M2) s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
unfolding not_ex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<forall>x. \<not> (x < t \<and> zcount M1 x < 0 \<and> nonpos_upto M1 x); \<forall>x. \<not> (x < t \<and> 0 < zcount C1 x); zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount (M1 + M2) s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<forall>x. \<not> (x < t \<and> zcount M1 x < 0 \<and> nonpos_upto M1 x); \<forall>x. \<not> (x < t \<and> 0 < zcount C1 x); zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount (M1 + M2) s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M1 s + zcount M2 s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply (rule exI[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> s < t \<and> zcount M1 s + zcount M2 s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> s < t
 2. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> zcount M1 s + zcount M2 s < 0
 3. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> zcount M1 s + zcount M2 s < 0
 2. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply (rule add_nonpos_neg)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> zcount M1 s \<le> 0
 2. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> zcount M2 s < 0
 3. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply (metis assms(3) le_less_linear less_trans order_class.le_less supported_strong_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> zcount M2 s < 0
 2. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>x. zcount M1 x < 0 \<longrightarrow> x < t \<longrightarrow> \<not> nonpos_upto M1 x; \<forall>x<t. \<not> 0 < zcount C1 x; zcount M1 t < zcount C1 t; \<forall>t. 0 < zcount M1 t \<longrightarrow> supported_strong M1 t \<or> (\<exists>t'<t. 0 < zcount C1 t') \<or> zcount M1 t < zcount C1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply (clarsimp simp: nonpos_upto_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<not> supported_strong M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<not> supported_strong M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "\<exists>t'<t. 0 < zcount C2 t'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<not> supported_strong M2 t; \<exists>t'<t. 0 < zcount C2 t'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<not> supported_strong M2 t; \<not> (\<exists>t'<t. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<not> supported_strong M2 t; \<exists>t'<t. 0 < zcount C2 t'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
by (metis add_cancel_left_left assms(3) order_class.order.not_eq_order_implies_strict zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<not> supported_strong M2 t; \<not> (\<exists>t'<t. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<not> supported_strong M2 t; \<not> (\<exists>t'<t. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (intro disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> (\<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<t. 0 < zcount C1 t'); zcount M1 t < zcount C1 t; \<not> supported_strong M2 t; \<not> (\<exists>t'<t. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>s. zcount M1 s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M1 s; \<forall>t'<t. \<not> 0 < zcount C1 t'; zcount M1 t < zcount C1 t; \<not> supported_strong M2 t; \<forall>t'<t. \<not> 0 < zcount C2 t'\<rbrakk> \<Longrightarrow> zcount M1 t + zcount M2 t < zcount C1 t + zcount C2 t
[PROOF STEP]
using assms(2)[unfolded justified_alt, rule_format, of t]
[PROOF STATE]
proof (prove)
using this:
0 < zcount M2 t \<Longrightarrow> supported_strong M2 t \<or> (\<exists>t'<t. 0 < zcount C2 t') \<or> zcount M2 t < zcount C2 t

goal (1 subgoal):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<forall>s. zcount M1 s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M1 s; \<forall>t'<t. \<not> 0 < zcount C1 t'; zcount M1 t < zcount C1 t; \<not> supported_strong M2 t; \<forall>t'<t. \<not> 0 < zcount C2 t'\<rbrakk> \<Longrightarrow> zcount M1 t + zcount M2 t < zcount C1 t + zcount C2 t
[PROOF STEP]
apply (metis add.commute add_cancel_left_right add_mono_thms_linordered_field(5) add_strict_increasing2 assms(4) nonzero_lt_gtD)
[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 (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "0 < zcount M2 t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; 0 < zcount M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> 0 < zcount M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
(* symmetric case *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; 0 < zcount M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> 0 < zcount M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> 0 < zcount M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; 0 < zcount M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> 0 < zcount M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; 0 < zcount M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; 0 < zcount M2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule assms(2)[unfolded justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s) \<or> (\<exists>t'<t. 0 < zcount C2 t') \<or> zcount M2 t < zcount C2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim disj3_split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s) \<and> (\<exists>t'<t. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 3. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; zcount M2 s < 0; nonpos_upto M2 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule order_zmset_exists_foundation_neg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; \<exists>sa\<le>s. zcount M2 sa < 0 \<and> (\<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < sa)\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; sa \<le> s; zcount M2 sa < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < sa\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal for s s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
(* anything less than s' is 0 in M1 *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "zcount (M1 + M2) s' < 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
apply (auto intro!: exI[of _ s'] simp: nonpos_upto_def supported_strong_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (subst (asm) not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "0 < zcount M1 s'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; 0 < zcount M1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> 0 < zcount M1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> 0 < zcount M1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; 0 < zcount M1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> 0 < zcount M1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; 0 < zcount M1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
(* trivial contradiction *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; 0 < zcount M1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; 0 < zcount M1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (drule assms(1)[unfolded justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s) \<or> (\<exists>t'<s'. 0 < zcount C1 t') \<or> zcount M1 s' < zcount C1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (elim disj3_split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s) \<and> (\<exists>t'<s'. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 3. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<s'. 0 < zcount C1 t'); zcount M1 s' < zcount C1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; sa < s' \<and> zcount M1 sa < 0 \<and> nonpos_upto M1 sa\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
subgoal for s''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; s'' < s' \<and> zcount M1 s'' < 0 \<and> nonpos_upto M1 s''\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
by (auto intro!: exI[of _ s''] simp: nonpos_upto_def supported_strong_def add_neg_nonpos)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s) \<and> (\<exists>t'<s'. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<s'. 0 < zcount C1 t'); zcount M1 s' < zcount C1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s) \<and> (\<exists>t'<s'. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI2, rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s) \<and> (\<exists>t'<s'. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C1 + C2) t'
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); t' < s'; 0 < zcount C1 t'\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C1 + C2) t'
[PROOF STEP]
subgoal for s''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); s'' < s'; 0 < zcount C1 s''\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C1 + C2) t'
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount C2 t

goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); s'' < s'; 0 < zcount C1 s''\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount (C1 + C2) t'
[PROOF STEP]
by (auto simp: add_pos_nonneg intro!: exI[of _ s''])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<s'. 0 < zcount C1 t'); zcount M1 s' < zcount C1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<s'. 0 < zcount C1 t'); zcount M1 s' < zcount C1 s'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI2, rule disjI1, rule exI[of _ s'], rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<s'. 0 < zcount C1 t'); zcount M1 s' < zcount C1 s'\<rbrakk> \<Longrightarrow> s' < t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<s'. 0 < zcount C1 t'); zcount M1 s' < zcount C1 s'\<rbrakk> \<Longrightarrow> 0 < zcount (C1 + C2) s'
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount C2 t

goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<s'. 0 < zcount C1 t'); zcount M1 s' < zcount C1 s'\<rbrakk> \<Longrightarrow> s' < t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; zcount M1 t \<le> 0; s < t; nonpos_upto M2 s; s' \<le> s; zcount M2 s' < 0; \<forall>u. zcount M2 u < 0 \<longrightarrow> \<not> u < s'; \<not> zcount (M1 + M2) s' < 0; \<not> (\<exists>s<s'. zcount M1 s < 0 \<and> nonpos_upto M1 s); \<not> (\<exists>t'<s'. 0 < zcount C1 t'); zcount M1 s' < zcount C1 s'\<rbrakk> \<Longrightarrow> 0 < zcount (C1 + C2) s'
[PROOF STEP]
by (auto intro!: add_pos_nonneg)
[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 (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s) \<and> (\<exists>t'<t. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s) \<and> (\<exists>t'<t. 0 < zcount C2 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
by (metis add_mono_thms_linordered_field(4) assms(3) add_0 zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "supported_strong M1 t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; supported_strong M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<not> supported_strong M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; supported_strong M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; supported_strong M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t
[PROOF STEP]
apply (simp only: supported_strong_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<exists>s<t. zcount M1 s < 0 \<and> nonpos_upto M1 s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount (M1 + M2) s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; s < t \<and> zcount M1 s < 0 \<and> nonpos_upto M1 s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount (M1 + M2) s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; s < t \<and> zcount M1 s < 0 \<and> nonpos_upto M1 s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount (M1 + M2) s < 0 \<and> nonpos_upto (M1 + M2) s
[PROOF STEP]
apply (clarsimp simp: nonpos_upto_def intro!: exI[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<not> 0 < zcount M1 t; \<forall>s. zcount M2 s < 0 \<longrightarrow> s < t \<longrightarrow> (\<exists>sa\<le>s. \<not> zcount M2 sa \<le> 0); \<forall>t'<t. \<not> 0 < zcount C2 t'; zcount M2 t < zcount C2 t; s < t; zcount M1 s < 0; \<forall>sa\<le>s. zcount M1 sa \<le> 0\<rbrakk> \<Longrightarrow> zcount M1 s + zcount M2 s < 0
[PROOF STEP]
using assms(2)[unfolded justified_alt nonpos_upto_def supported_strong_def, rule_format, of s]
                assms(4)[rule_format, of s]
[PROOF STATE]
proof (prove)
using this:
0 < zcount M2 s \<Longrightarrow> (\<exists>sa<s. zcount M2 sa < 0 \<and> (\<forall>s\<le>sa. zcount M2 s \<le> 0)) \<or> (\<exists>t'<s. 0 < zcount C2 t') \<or> zcount M2 s < zcount C2 s
0 \<le> zcount C2 s

goal (1 subgoal):
 1. \<lbrakk>0 < zcount M1 t + zcount M2 t; \<forall>t'<t. zcount M1 t' + zcount M2 t' \<le> 0; \<not> 0 < zcount M1 t; \<forall>s. zcount M2 s < 0 \<longrightarrow> s < t \<longrightarrow> (\<exists>sa\<le>s. \<not> zcount M2 sa \<le> 0); \<forall>t'<t. \<not> 0 < zcount C2 t'; zcount M2 t < zcount C2 t; s < t; zcount M1 s < 0; \<forall>sa\<le>s. zcount M1 sa \<le> 0\<rbrakk> \<Longrightarrow> zcount M1 s + zcount M2 s < 0
[PROOF STEP]
apply (smt (verit, best) dual_order.strict_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<not> supported_strong M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<not> supported_strong M1 t\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (cases "\<exists>t'<t. 0 < zcount C1 t'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<not> supported_strong M1 t; \<exists>t'<t. 0 < zcount C1 t'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
 2. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<not> supported_strong M1 t; \<not> (\<exists>t'<t. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<not> supported_strong M1 t; \<exists>t'<t. 0 < zcount C1 t'\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
by (metis add.commute add_cancel_left_left assms(4) order_class.order.not_eq_order_implies_strict zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<not> supported_strong M1 t; \<not> (\<exists>t'<t. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<not> supported_strong M1 t; \<not> (\<exists>t'<t. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> supported_strong (M1 + M2) t \<or> (\<exists>t'<t. 0 < zcount (C1 + C2) t') \<or> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (intro disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (M1 + M2) t; \<forall>t'<t. zcount (M1 + M2) t' \<le> 0; \<not> 0 < zcount M1 t; \<not> (\<exists>s<t. zcount M2 s < 0 \<and> nonpos_upto M2 s); \<not> (\<exists>t'<t. 0 < zcount C2 t'); zcount M2 t < zcount C2 t; \<not> supported_strong M1 t; \<not> (\<exists>t'<t. 0 < zcount C1 t')\<rbrakk> \<Longrightarrow> zcount (M1 + M2) t < zcount (C1 + C2) t
[PROOF STEP]
apply (metis add.commute add_strict_increasing2 assms(3) not_le sublist_order.add_less zcount_union)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (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 (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma justified_sum:
  assumes "\<forall>p\<in>P. justified (f p) (g p)"
    and   "\<forall>p\<in>P. \<forall>t. 0 \<le> zcount (f p) t"
  shows   "justified (\<Sum>p\<in>P. f p) (\<Sum>p\<in>P. g p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified (sum f P) (sum g P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>P. justified (f p) (g p)
\<forall>p\<in>P. \<forall>t. 0 \<le> zcount (f p) t

goal (1 subgoal):
 1. justified (sum f P) (sum g P)
[PROOF STEP]
by (induct P rule: infinite_finite_induct)
    (auto intro!: justified_add sum_nonneg simp: zcount_sum)


[STATEMENT]
lemma justified_add_records:
  assumes "justified C M"
    and   "\<forall>t. 0 \<le> zcount C' t"
  shows   "justified (C+C') M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified (C + C') M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
justified C M
\<forall>t. 0 \<le> zcount C' t

goal (1 subgoal):
 1. justified (C + C') M
[PROOF STEP]
unfolding justified_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 < zcount M t \<longrightarrow> supported M t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
\<forall>t. 0 \<le> zcount C' t

goal (1 subgoal):
 1. \<forall>t. 0 < zcount M t \<longrightarrow> supported M t \<or> (\<exists>t'<t. 0 < zcount (C + C') t') \<or> zcount M t < zcount (C + C') t
[PROOF STEP]
apply (clarsimp intro: add_pos_nonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<forall>t. 0 < zcount M t \<longrightarrow> supported M t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t; \<forall>t. 0 \<le> zcount C' t; 0 < zcount M t; \<not> supported M t; \<not> zcount M t < zcount C t + zcount C' t\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t' + zcount C' t'
[PROOF STEP]
apply (metis add.commute add_strict_increasing2 assms(2))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma justified_add_zmset_records:
  assumes "justified C M"
  shows   "justified (add_zmset t C) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified (add_zmset t C) M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
justified C M

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