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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<exists>s<t. zcount (M - zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M - zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s < t \<and> zcount M s < 0 \<and> nonpos_upto M s \<Longrightarrow> (\<exists>s<t. zcount (M - zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M - zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < t \<and> zcount M s < 0 \<and> nonpos_upto M s \<Longrightarrow> (\<exists>s<t. zcount (M - zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M - zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
by (auto intro!: disjI1 exI[of _ s] simp: nonpos_upto_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t

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

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

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

goal (1 subgoal):
 1. \<lbrakk>t' < t; s \<le> t'; 0 < zcount C s; \<forall>u<s. zcount C u \<le> 0; s' < s\<rbrakk> \<Longrightarrow> zcount C s' = 0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
s < t
0 < zcount C s
\<forall>s'<s. zcount C s' = 0

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

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

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

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

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

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

goal (1 subgoal):
 1. supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
0 < zcount (C - zmset_of \<Delta>) s
s < t
0 < zcount C s
\<forall>s'<s. zcount C s' = 0

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

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

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

goal (1 subgoal):
 1. supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
using s least
[PROOF STATE]
proof (prove)
using this:
zcount (C - zmset_of \<Delta>) s = 0
zcount (M - zmset_of \<Delta>) s < 0
s < t
0 < zcount C s
\<forall>s'<s. zcount C s' = 0
\<forall>t'<t. zcount (M - zmset_of \<Delta>) t' \<le> 0

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

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

goal (2 subgoals):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (M - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
 2. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (M - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
note case3 = 3
[PROOF STATE]
proof (state)
this:
zcount (C - zmset_of \<Delta>) s = 0
zcount (M - zmset_of \<Delta>) s = 0

goal (2 subgoals):
 1. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; zcount (M - zmset_of \<Delta>) s = 0\<rbrakk> \<Longrightarrow> supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
 2. \<lbrakk>zcount (C - zmset_of \<Delta>) s = 0; 0 < zcount (M - zmset_of \<Delta>) s\<rbrakk> \<Longrightarrow> supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
with s(2)
[PROOF STATE]
proof (chain)
picking this:
0 < zcount C s
zcount (C - zmset_of \<Delta>) s = 0
zcount (M - zmset_of \<Delta>) s = 0
[PROOF STEP]
have Ms: "0 < zcount M s"
[PROOF STATE]
proof (prove)
using this:
0 < zcount C s
zcount (C - zmset_of \<Delta>) s = 0
zcount (M - zmset_of \<Delta>) s = 0

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<exists>s<t. zcount (M - zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M - zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>sa < s; zcount M sa < 0; nonpos_upto M sa\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M - zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M - zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; zcount M s' < 0; nonpos_upto M s'\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (M - zmset_of \<Delta>) s < 0 \<and> nonpos_upto (M - zmset_of \<Delta>) s) \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
apply (intro disjI1 exI[of _ s'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; zcount M s' < 0; nonpos_upto M s'\<rbrakk> \<Longrightarrow> s' < t \<and> zcount (M - zmset_of \<Delta>) s' < 0 \<and> nonpos_upto (M - zmset_of \<Delta>) s'
[PROOF STEP]
using s(1,2)
[PROOF STATE]
proof (prove)
using this:
s < t
0 < zcount C s

goal (1 subgoal):
 1. \<lbrakk>s' < s; zcount M s' < 0; nonpos_upto M s'\<rbrakk> \<Longrightarrow> s' < t \<and> zcount (M - zmset_of \<Delta>) s' < 0 \<and> nonpos_upto (M - zmset_of \<Delta>) s'
[PROOF STEP]
apply (auto intro: exI[of _ s'] 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 (state)
this:
supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t

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

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

goal (1 subgoal):
 1. supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
using s(3)
[PROOF STATE]
proof (prove)
using this:
\<exists>t'<s. 0 < zcount C t'
\<forall>s'<s. zcount C s' = 0

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

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

goal (1 subgoal):
 1. zcount M s < zcount C s \<Longrightarrow> supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
from case3
[PROOF STATE]
proof (chain)
picking this:
zcount (C - zmset_of \<Delta>) s = 0
zcount (M - zmset_of \<Delta>) s = 0
[PROOF STEP]
have "zcount C s = zcount M s"
[PROOF STATE]
proof (prove)
using this:
zcount (C - zmset_of \<Delta>) s = 0
zcount (M - zmset_of \<Delta>) s = 0

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

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

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

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

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

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

goal (1 subgoal):
 1. supported_strong (M - zmset_of \<Delta>) t \<or> (\<exists>t'<t. 0 < zcount (C - zmset_of \<Delta>) t') \<or> zcount (M - zmset_of \<Delta>) t < zcount (C - zmset_of \<Delta>) t
[PROOF STEP]
using least s(1)
[PROOF STATE]
proof (prove)
using this:
zcount (C - zmset_of \<Delta>) s = 0
0 < zcount (M - zmset_of \<Delta>) s
\<forall>t'<t. zcount (M - zmset_of \<Delta>) t' \<le> 0
s < t

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. \<And>t. \<lbrakk>0 < zcount (M + timestamps (zmset_of \<Delta>)) t; \<forall>t'<t. zcount (M + timestamps (zmset_of \<Delta>)) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
have \<Delta>t: "0 < zcount (timestamps (zmset_of \<Delta>)) t \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>)) t \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
by (auto dest: pos_image_zmset_obtain_pre[rotated] assms(2)[unfolded minting_msg_def, rule_format])
[PROOF STATE]
proof (state)
this:
0 < zcount (timestamps (zmset_of \<Delta>)) t \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s; \<forall>t'<t. zcount C t' = 0; zcount C t \<le> zcount M t\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t'<t. zcount C t' = 0; zcount C t \<le> zcount M t; s < t; zcount M s < 0; nonpos_upto M s\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
apply (drule order_zmset_exists_foundation_neg')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t'<t. zcount C t' = 0; zcount C t \<le> zcount M t; s < t; nonpos_upto M s; \<exists>sa\<le>s. zcount M sa < 0 \<and> (\<forall>u<sa. 0 \<le> zcount M u)\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>\<forall>t'<t. zcount C t' = 0; zcount C t \<le> zcount M t; s < t; nonpos_upto M s; sa \<le> s; zcount M sa < 0; \<forall>u<sa. 0 \<le> zcount M u\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
subgoal for s s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t'<t. zcount C t' = 0; zcount C t \<le> zcount M t; s < t; nonpos_upto M s; s' \<le> s; zcount M s' < 0; \<forall>u<s'. 0 \<le> zcount M u\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
by (auto intro!: exI[of _ s'] simp: nonpos_upto_def order_class.order_antisym)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
s < t
zcount M s < 0
\<forall>s'<s. zcount M s' = 0

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

goal (1 subgoal):
 1. supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
apply (cases "\<exists>s'\<le>s. zcount (timestamps (zmset_of \<Delta>)) s' > 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; \<exists>s'\<le>s. 0 < zcount (timestamps (zmset_of \<Delta>)) s'\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
 2. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; \<not> (\<exists>s'\<le>s. 0 < zcount (timestamps (zmset_of \<Delta>)) s')\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; s' \<le> s; 0 < zcount (timestamps (zmset_of \<Delta>)) s'\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
 2. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; \<not> (\<exists>s'\<le>s. 0 < zcount (timestamps (zmset_of \<Delta>)) s')\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; s' \<le> s; 0 < zcount (timestamps (zmset_of \<Delta>)) s'\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
apply (drule pos_image_zmset_obtain_pre[rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ta. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; s' \<le> s\<rbrakk> \<Longrightarrow> 0 \<le> zcount (zmset_of \<Delta>) ta
 2. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; s' \<le> s; \<exists>m. 0 < zcount (zmset_of \<Delta>) m \<and> (case m of (x, t) \<Rightarrow> t) = s'\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; s' \<le> s; \<exists>m. 0 < zcount (zmset_of \<Delta>) m \<and> (case m of (x, t) \<Rightarrow> t) = s'\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; s' \<le> s; 0 < zcount (zmset_of \<Delta>) m; (case m of (x, t) \<Rightarrow> t) = s'\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; s' \<le> s; m \<in># \<Delta>; (case m of (x, t) \<Rightarrow> t) = s'\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>#}) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t + int (count {#t. (p, t) \<in># \<Delta>#} t) < zcount C t
[PROOF STEP]
apply (drule assms(2)[unfolded minting_msg_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; s' \<le> s; (case m of (x, t) \<Rightarrow> t) = s'; case m of (p, t) \<Rightarrow> \<exists>t'<t. 0 < zcount C t'\<rbrakk> \<Longrightarrow> supported_strong (M + zmset_of {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>#}) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t + int (count {#t. (p, t) \<in># \<Delta>#} t) < zcount C t
[PROOF STEP]
apply (auto simp: supported_strong_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; \<not> (\<exists>s'\<le>s. 0 < zcount (timestamps (zmset_of \<Delta>)) s')\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; \<not> (\<exists>s'\<le>s. 0 < zcount (timestamps (zmset_of \<Delta>)) s')\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t
[PROOF STEP]
apply (intro disjI1 exI[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; \<not> (\<exists>s'\<le>s. 0 < zcount (timestamps (zmset_of \<Delta>)) s')\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t
[PROOF STEP]
unfolding not_less
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s < t; zcount M s < 0; \<forall>s'<s. zcount M s' = 0; \<not> (\<exists>s'\<le>s. 0 < zcount (timestamps (zmset_of \<Delta>)) s')\<rbrakk> \<Longrightarrow> supported_strong (M + timestamps (zmset_of \<Delta>)) t
[PROOF STEP]
apply (metis (full_types) le_less_linear least eq_refl order.strict_trans1 nonpos_upto_def supported_strong_def 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 (state)
this:
supported_strong (M + timestamps (zmset_of \<Delta>)) t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount (M + timestamps (zmset_of \<Delta>)) t < zcount C t

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed