[STATEMENT]
lemma next_performop'_preserves_justified:
  assumes "justified (c_caps c0 p) M"
    and   "next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self"
    and   "InvCapsNonneg c0"
  shows   "justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
let ?\<Delta>pos = "timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
let ?\<Delta> = "?\<Delta>pos - zmset_of \<Delta>neg"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
let ?M1 = "M + ?\<Delta>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
note change = next_performopD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
\<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z
\<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t
minting_self (c_caps c0 p) \<Delta>mint_self
minting_msg (c_caps c0 p) \<Delta>mint_msg
c_temp c1 = (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
c_msg c1 = c_msg c0
c_glob c1 = c_glob c0
c_data_msg c1 = c_data_msg c0 + \<Delta>mint_msg
c_caps c1 = (c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
note complex_change = next_performop_complexD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
records c1 = records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
GlobalIncomingInfoAt c1 ?q = GlobalIncomingInfoAt c0 ?q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
IncomingInfo c1 ?k ?p' ?q = (if ?p' = p then IncomingInfo c0 ?k ?p' ?q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 ?k ?p' ?q)
\<forall>t'<?t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) ?t = 0
InfoAt c1 ?k ?p' ?q = InfoAt c0 ?k ?p' ?q

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
note inv0 = assms(1)[unfolded InvJustifiedII_def justified_alt, rule_format]
[PROOF STATE]
proof (state)
this:
0 < zcount M ?t \<Longrightarrow> supported_strong M ?t \<or> (\<exists>t'<?t. 0 < zcount (c_caps c0 p) t') \<or> zcount M ?t < zcount (c_caps c0 p) ?t

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 < zcount M ?t \<Longrightarrow> supported_strong M ?t \<or> (\<exists>t'<?t. 0 < zcount (c_caps c0 p) t') \<or> zcount M ?t < zcount (c_caps c0 p) ?t

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
fix k q t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
assume t: "0 < zcount ?M1 t"
[PROOF STATE]
proof (state)
this:
0 < zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
assume least: "\<forall>t'<t. zcount ?M1 t' \<le> 0"
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' \<le> 0

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
from t
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t
[PROOF STEP]
consider "0 < zcount M t" | "zcount M t \<le> 0" "0 < zcount ?\<Delta> t"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t

goal (1 subgoal):
 1. \<lbrakk>0 < zcount M t \<Longrightarrow> thesis; \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim (auto simp: complex_change)
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < zcount M t \<Longrightarrow> ?thesis; \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < zcount M t \<Longrightarrow> ?thesis; \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have "supported_strong ?M1 t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount ?M1 t < zcount (c_caps c1 p) t"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < zcount M t \<Longrightarrow> ?thesis; \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < zcount M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
case 1 \<comment> \<open>@{term M} was already positive at @{term t} in @{term c0}\<close>
[PROOF STATE]
proof (state)
this:
0 < zcount M t

goal (2 subgoals):
 1. 0 < zcount M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
note Mcount = 1
[PROOF STATE]
proof (state)
this:
0 < zcount M t

goal (2 subgoals):
 1. 0 < zcount M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
note assms(1)[unfolded InvJustifiedII_def justified_alt, rule_format, OF Mcount]
[PROOF STATE]
proof (state)
this:
supported_strong M t \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p) t') \<or> zcount M t < zcount (c_caps c0 p) t

goal (2 subgoals):
 1. 0 < zcount M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supported_strong M t \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p) t') \<or> zcount M t < zcount (c_caps c0 p) t
[PROOF STEP]
consider
        "supported_strong M t" |
        "\<not> supported_strong M t" "\<exists>t'<t. 0 < zcount (c_caps c0 p) t'" |
        "\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0" "zcount M t < zcount (c_caps c0 p) t"
[PROOF STATE]
proof (prove)
using this:
supported_strong M t \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p) t') \<or> zcount M t < zcount (c_caps c0 p) t

goal (1 subgoal):
 1. \<lbrakk>supported_strong M t \<Longrightarrow> thesis; \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>supported_strong M t \<Longrightarrow> ?thesis; \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. 0 < zcount M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>supported_strong M t \<Longrightarrow> ?thesis; \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>supported_strong M t \<Longrightarrow> ?thesis; \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) 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 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
supported_strong M t

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
assume nosupp: "\<not> supported_strong ?M1 t"
[PROOF STATE]
proof (state)
this:
\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
assume "\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'"
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'
[PROOF STEP]
have nocaps: "\<forall>t'<t. zcount (c_caps c1 p) t' = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'

goal (1 subgoal):
 1. \<forall>t'<t. zcount (c_caps c1 p) t' = 0
[PROOF STEP]
using InvCapsNonneg_def assms(2) assms(3) order_class.le_less performop_preserves_InvCapsNonneg
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'
InvCapsNonneg ?c = (\<forall>p t. 0 \<le> zcount (c_caps ?c p) t)
next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self
InvCapsNonneg c0
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
\<lbrakk>InvCapsNonneg ?c0.0; next_performop' ?c0.0 ?c1.0 ?p ?\<Delta>\<^sub>m ?\<Delta>\<^sub>p\<^sub>1 ?\<Delta>\<^sub>p\<^sub>2\<rbrakk> \<Longrightarrow> InvCapsNonneg ?c1.0

goal (1 subgoal):
 1. \<forall>t'<t. zcount (c_caps c1 p) t' = 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. zcount (c_caps c1 p) t' = 0

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
supported_strong M t
[PROOF STEP]
obtain s where s: "s < t" "zcount M s < 0" "\<And>s'. s' < s \<Longrightarrow> zcount M s' = 0"
[PROOF STATE]
proof (prove)
using this:
supported_strong M t

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

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s < t; zcount M s < 0; \<And>s'. s' < s \<Longrightarrow> zcount M s' = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s<t. zcount M s < 0 \<and> (\<forall>sa\<le>s. zcount M sa \<le> 0) \<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>s < t; zcount M s < 0; \<forall>sa\<le>s. zcount M sa \<le> 0\<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>s < t; \<forall>sa\<le>s. zcount M sa \<le> 0; \<exists>sa\<le>s. zcount M sa < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < sa)\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>s < t; \<forall>sa\<le>s. zcount M sa \<le> 0; sa \<le> s \<and> zcount M sa < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < sa)\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
subgoal for _ s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s_ < t; \<forall>sa\<le>s_. zcount M sa \<le> 0; s \<le> s_ \<and> zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> \<exists>s<t. zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
apply (rule exI[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s_ < t; \<forall>sa\<le>s_. zcount M sa \<le> 0; s \<le> s_ \<and> zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> s < t \<and> zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s_ < t; \<forall>sa\<le>s_. zcount M sa \<le> 0; s \<le> s_ \<and> zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> s < t
 2. \<lbrakk>s_ < t; \<forall>sa\<le>s_. zcount M sa \<le> 0; s \<le> s_ \<and> zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
using le_less_trans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (2 subgoals):
 1. \<lbrakk>s_ < t; \<forall>sa\<le>s_. zcount M sa \<le> 0; s \<le> s_ \<and> zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> s < t
 2. \<lbrakk>s_ < t; \<forall>sa\<le>s_. zcount M sa \<le> 0; s \<le> s_ \<and> zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s_ < t; \<forall>sa\<le>s_. zcount M sa \<le> 0; s \<le> s_ \<and> zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> zcount M s < 0 \<and> (\<forall>s'<s. zcount M s' = 0)
[PROOF STEP]
using less_imp_le order_trans order_class.order.not_eq_order_implies_strict
[PROOF STATE]
proof (prove)
using this:
?x < ?y \<Longrightarrow> ?x \<le> ?y
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
\<lbrakk>?a \<noteq> ?b; ?a \<le> ?b\<rbrakk> \<Longrightarrow> ?a < ?b

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

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have count1s: "0 \<le> zcount ?M1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s \<Longrightarrow> False
[PROOF STEP]
apply (subst (asm) not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0 \<Longrightarrow> False
[PROOF STEP]
using nosupp[unfolded nonpos_upto_def supported_strong_def, simplified, rule_format]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>zcount M ?s + (int (count {#t. (p, t) \<in># \<Delta>mint_msg#} ?s) + int (count \<Delta>mint_self ?s) - int (count \<Delta>neg ?s)) < 0; ?s < t\<rbrakk> \<Longrightarrow> \<exists>s\<le>?s. \<not> zcount M s + (int (count {#t. (p, t) \<in># \<Delta>mint_msg#} s) + int (count \<Delta>mint_self s) - int (count \<Delta>neg s)) \<le> 0

goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0 \<Longrightarrow> False
[PROOF STEP]
using least order.strict_trans2 s(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>zcount M ?s + (int (count {#t. (p, t) \<in># \<Delta>mint_msg#} ?s) + int (count \<Delta>mint_self ?s) - int (count \<Delta>neg ?s)) < 0; ?s < t\<rbrakk> \<Longrightarrow> \<exists>s\<le>?s. \<not> zcount M s + (int (count {#t. (p, t) \<in># \<Delta>mint_msg#} s) + int (count \<Delta>mint_self s) - int (count \<Delta>neg s)) \<le> 0
\<forall>t'<t. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' \<le> 0
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c
s < t

goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0 \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have \<Delta>inc: "0 < zcount ?\<Delta> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) s
[PROOF STEP]
using complex_change(3) count1s s(2)
[PROOF STATE]
proof (prove)
using this:
IncomingInfo c1 ?k ?p' ?q = (if ?p' = p then IncomingInfo c0 ?k ?p' ?q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 ?k ?p' ?q)
0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s
zcount M s < 0

goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) s

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have "0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) s
[PROOF STEP]
using \<Delta>inc change(2)[rule_format, of s] nocaps[rule_format, OF s(1)]
[PROOF STATE]
proof (prove)
using this:
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) s
int (count \<Delta>neg s) \<le> zcount (c_caps c0 p) s
zcount (c_caps c1 p) s = 0

goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) s
[PROOF STEP]
unfolding change(9) fun_upd_same zcount_union zcount_diff
[PROOF STATE]
proof (prove)
using this:
0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) s + zcount (zmset_of \<Delta>mint_self) s - zcount (zmset_of \<Delta>neg) s
int (count \<Delta>neg s) \<le> zcount (c_caps c0 p) s
zcount (c_caps c0 p) s + (zcount (zmset_of \<Delta>mint_self) s - zcount (zmset_of \<Delta>neg) s) = 0

goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) s
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) s

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

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u < s; 0 < zcount (c_caps c0 p) u; \<forall>u'<u. zcount (c_caps c0 p) u' = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) s \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply (drule pos_image_zmset_obtain_pre[rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. 0 \<le> zcount (zmset_of \<Delta>mint_msg) t
 2. \<exists>m. 0 < zcount (zmset_of \<Delta>mint_msg) m \<and> (case m of (x, t) \<Rightarrow> t) = s \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. 0 < zcount (zmset_of \<Delta>mint_msg) m \<and> (case m of (x, t) \<Rightarrow> t) = s \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. 0 < zcount (zmset_of \<Delta>mint_msg) (a, s) \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
subgoal for p'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (zmset_of \<Delta>mint_msg) (p', s) \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p', s) \<in># \<Delta>mint_msg \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply (drule change(4)[unfolded minting_msg_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (p', s) of (pa, t) \<Rightarrow> \<exists>t'<t. 0 < zcount (c_caps c0 p) t' \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'<s. 0 < zcount (c_caps c0 p) t' \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>t' < s; 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply (drule order_zmset_exists_foundation)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>t' < s; \<exists>s\<le>t'. 0 < zcount (c_caps c0 p) s \<and> (\<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t' sa. \<lbrakk>t' < s; sa \<le> t'; 0 < zcount (c_caps c0 p) sa; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < sa\<rbrakk> \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
subgoal for s' u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> \<exists>u<s. 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply (rule exI[of _ u])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> u < s \<and> 0 < zcount (c_caps c0 p) u \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < s; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> u < s \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
using assms(3)[unfolded InvCapsNonneg_def, rule_format]
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount (c_caps c0 ?p) ?t

goal (1 subgoal):
 1. \<lbrakk>s' < s; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> u < s \<and> (\<forall>u'<u. zcount (c_caps c0 p) u' = 0)
[PROOF STEP]
apply (metis le_less_trans order_class.order.not_eq_order_implies_strict)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
u < s
0 < zcount (c_caps c0 p) u
\<forall>u'<u. zcount (c_caps c0 p) u' = 0

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have count1u: "zcount ?M1 u < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u < 0
[PROOF STEP]
using complex_change(4)[of u] nocaps[unfolded change(9) fun_upd_same] order.strict_trans[OF u(1) s(1)] s(3)[OF u(1)] u(2) u(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<u. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) u = 0
\<forall>t'<t. zcount (c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' = 0
u < t
zcount M u = 0
0 < zcount (c_caps c0 p) u
\<forall>u'<u. zcount (c_caps c0 p) u' = 0

goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u < 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u < 0

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u < 0
[PROOF STEP]
have "nonpos_upto ?M1 u"
[PROOF STATE]
proof (prove)
using this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u < 0

goal (1 subgoal):
 1. nonpos_upto (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u
[PROOF STEP]
unfolding nonpos_upto_def
[PROOF STATE]
proof (prove)
using this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u < 0

goal (1 subgoal):
 1. \<forall>s\<le>u. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s \<le> 0
[PROOF STEP]
using least order.strict_implies_order order.strict_trans1 s(1) u(1)
[PROOF STATE]
proof (prove)
using this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u < 0
\<forall>t'<t. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' \<le> 0
?a < ?b \<Longrightarrow> ?a \<le> ?b
\<lbrakk>?a \<le> ?b; ?b < ?c\<rbrakk> \<Longrightarrow> ?a < ?c
s < t
u < s

goal (1 subgoal):
 1. \<forall>s\<le>u. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s \<le> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
nonpos_upto (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nonpos_upto (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u
[PROOF STEP]
have "supported_strong ?M1 t"
[PROOF STATE]
proof (prove)
using this:
nonpos_upto (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u

goal (1 subgoal):
 1. supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t
[PROOF STEP]
using count1u order.strict_trans s(1) u(1) supported_strong_def
[PROOF STATE]
proof (prove)
using this:
nonpos_upto (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u < 0
\<lbrakk>?a < ?b; ?b < ?c\<rbrakk> \<Longrightarrow> ?a < ?c
s < t
u < s
supported_strong ?a ?t \<equiv> \<exists>s<?t. zcount ?a s < 0 \<and> nonpos_upto ?a s

goal (1 subgoal):
 1. supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
with nosupp
[PROOF STATE]
proof (chain)
picking this:
\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t
supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t
supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t; \<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'\<rbrakk> \<Longrightarrow> False

goal (3 subgoals):
 1. supported_strong M t \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 3. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t; \<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t; \<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<not> supported_strong M t
\<exists>t'<t. 0 < zcount (c_caps c0 p) t'

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> supported_strong M t
\<exists>t'<t. 0 < zcount (c_caps c0 p) t'

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
assume nosupp: "\<not> supported_strong ?M1 t"
[PROOF STATE]
proof (state)
this:
\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
assume "\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'"
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'
[PROOF STEP]
have nocaps: "\<forall>t'<t. zcount (c_caps c1 p) t' = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'

goal (1 subgoal):
 1. \<forall>t'<t. zcount (c_caps c1 p) t' = 0
[PROOF STEP]
using InvCapsNonneg_def assms(2) assms(3) order_class.le_less performop_preserves_InvCapsNonneg
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'
InvCapsNonneg ?c = (\<forall>p t. 0 \<le> zcount (c_caps ?c p) t)
next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self
InvCapsNonneg c0
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
\<lbrakk>InvCapsNonneg ?c0.0; next_performop' ?c0.0 ?c1.0 ?p ?\<Delta>\<^sub>m ?\<Delta>\<^sub>p\<^sub>1 ?\<Delta>\<^sub>p\<^sub>2\<rbrakk> \<Longrightarrow> InvCapsNonneg ?c1.0

goal (1 subgoal):
 1. \<forall>t'<t. zcount (c_caps c1 p) t' = 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. zcount (c_caps c1 p) t' = 0

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
from 2(2)
[PROOF STATE]
proof (chain)
picking this:
\<exists>t'<t. 0 < zcount (c_caps c0 p) t'
[PROOF STEP]
obtain s where s: "s < t" "0 < zcount (c_caps c0 p) s" "\<forall>s'<s. zcount (c_caps c0 p) s' = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>t'<t. 0 < zcount (c_caps c0 p) t'

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s < t; 0 < zcount (c_caps c0 p) s; \<forall>s'<s. zcount (c_caps c0 p) 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_caps c0 p) t' \<Longrightarrow> \<exists>s<t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>t' < t; 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) 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_caps c0 p) s \<and> (\<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) 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_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
subgoal for _ s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t'_ < t; s \<le> t'_; 0 < zcount (c_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) 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_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s\<rbrakk> \<Longrightarrow> s < t \<and> 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (rule conjI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t'_ < t; s \<le> t'_; 0 < zcount (c_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s\<rbrakk> \<Longrightarrow> 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (rule conjI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t'_ < t; s \<le> t'_; 0 < zcount (c_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s\<rbrakk> \<Longrightarrow> \<forall>s'<s. zcount (c_caps c0 p) 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_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s; s' < s\<rbrakk> \<Longrightarrow> zcount (c_caps c0 p) s' = 0
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>t'_ < t; s \<le> t'_; 0 < zcount (c_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s; s' < s; zcount (c_caps c0 p) s' \<noteq> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t'_ < t; s \<le> t'_; 0 < zcount (c_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s; s'_ < s; zcount (c_caps c0 p) s'_ \<noteq> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms(3)[unfolded InvCapsNonneg_def, rule_format]
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount (c_caps c0 ?p) ?t

goal (1 subgoal):
 1. \<lbrakk>t'_ < t; s \<le> t'_; 0 < zcount (c_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s; s'_ < s; zcount (c_caps c0 p) s'_ \<noteq> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t'_ < t; s \<le> t'_; 0 < zcount (c_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s; s'_ < s; s'_ \<in>#\<^sub>z c_caps c0 p; \<And>p t. 0 \<le> zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis order_class.le_less zcount_ne_zero_iff)
[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_caps c0 p) s
\<forall>s'<s. zcount (c_caps c0 p) s' = 0

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have \<Delta>counts:
            "\<And>s. s < t \<Longrightarrow> count \<Delta>neg s = zcount (c_caps c0 p) s"
            "\<And>s. s < t \<Longrightarrow> count \<Delta>mint_self s = 0"
            "\<And>p s'. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p,s') = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s < t \<Longrightarrow> int (count \<Delta>neg s) = zcount (c_caps c0 p) s) &&& (\<And>s. s < t \<Longrightarrow> count \<Delta>mint_self s = 0) &&& (\<And>p s'. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0)
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' < t \<Longrightarrow> int (count \<Delta>neg s') = zcount (c_caps c0 p) s'
[PROOF STEP]
using change(2) nocaps s(1) order_class.order.not_eq_order_implies_strict
[PROOF STATE]
proof (prove)
using this:
\<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t
\<forall>t'<t. zcount (c_caps c1 p) t' = 0
s < t
\<lbrakk>?a \<noteq> ?b; ?a \<le> ?b\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. s' < t \<Longrightarrow> int (count \<Delta>neg s') = zcount (c_caps c0 p) s'
[PROOF STEP]
by (fastforce simp: change(9))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. s < t \<Longrightarrow> count \<Delta>mint_self s = 0
 2. \<And>p s'. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' < t \<Longrightarrow> count \<Delta>mint_self s' = 0
[PROOF STEP]
using nocaps[rule_format, of s']
[PROOF STATE]
proof (prove)
using this:
s' < t \<Longrightarrow> zcount (c_caps c1 p) s' = 0

goal (1 subgoal):
 1. s' < t \<Longrightarrow> count \<Delta>mint_self s' = 0
[PROOF STEP]
by (simp add: change(9) \<open>\<And>s'. s' < t \<Longrightarrow> int (count \<Delta>neg s') = zcount (c_caps c0 p) s'\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p s'. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0
[PROOF STEP]
subgoal for p s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0
[PROOF STEP]
using change(4)[unfolded minting_msg_def, rule_format, of "(p,s')"] s(3)
[PROOF STATE]
proof (prove)
using this:
(p, s') \<in># \<Delta>mint_msg \<Longrightarrow> case (p, s') of (pa, t) \<Rightarrow> \<exists>t'<t. 0 < zcount (c_caps c0 p) t'
\<forall>s'<s. zcount (c_caps c0 p) s' = 0

goal (1 subgoal):
 1. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0
[PROOF STEP]
by (force intro: ccontr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
?s < t \<Longrightarrow> int (count \<Delta>neg ?s) = zcount (c_caps c0 p) ?s
?s < t \<Longrightarrow> count \<Delta>mint_self ?s = 0
?s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (?p, ?s') = 0

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have caps_le_ii0: "zcount (c_caps c0 p) s \<le> zcount M s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (c_caps c0 p) s \<le> zcount M s
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> zcount (c_caps c0 p) s \<le> zcount M s \<Longrightarrow> False
[PROOF STEP]
assume nle: "\<not> zcount (c_caps c0 p) s \<le> zcount M s"
[PROOF STATE]
proof (state)
this:
\<not> zcount (c_caps c0 p) s \<le> zcount M s

goal (1 subgoal):
 1. \<not> zcount (c_caps c0 p) s \<le> zcount M s \<Longrightarrow> False
[PROOF STEP]
have "zcount ?M1 s < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
[PROOF STEP]
unfolding complex_change(3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
[PROOF STEP]
using complex_change(4) nle s(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<?t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) ?t = 0
\<not> zcount (c_caps c0 p) s \<le> zcount M s
\<forall>s'<s. zcount (c_caps c0 p) s' = 0

goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
[PROOF STEP]
by (auto simp: \<Delta>counts(1,2)[OF s(1)])
[PROOF STATE]
proof (state)
this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0

goal (1 subgoal):
 1. \<not> zcount (c_caps c0 p) s \<le> zcount M s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using s(1) least
[PROOF STATE]
proof (prove)
using this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
s < t
\<forall>t'<t. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' \<le> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (force dest!: nosupp[unfolded supported_strong_def, simplified, rule_format] simp: nonpos_upto_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
zcount (c_caps c0 p) s \<le> zcount M s

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
with s(2)
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (c_caps c0 p) s
zcount (c_caps c0 p) s \<le> zcount M s
[PROOF STEP]
have count0s: "0 < zcount M s"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_caps c0 p) s
zcount (c_caps c0 p) s \<le> zcount M s

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

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using inv0[OF count0s]
[PROOF STATE]
proof (prove)
using this:
supported_strong M s \<or> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t') \<or> zcount M s < zcount (c_caps c0 p) s

goal (1 subgoal):
 1. False
[PROOF STEP]
apply (elim disj3_split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. supported_strong M s \<Longrightarrow> False
 2. \<not> supported_strong M s \<and> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t') \<Longrightarrow> False
 3. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using 2(1) order.strict_trans s(1) supported_strong_def
[PROOF STATE]
proof (prove)
using this:
\<not> supported_strong M t
\<lbrakk>?a < ?b; ?b < ?c\<rbrakk> \<Longrightarrow> ?a < ?c
s < t
supported_strong ?a ?t \<equiv> \<exists>s<?t. zcount ?a s < 0 \<and> nonpos_upto ?a s

goal (3 subgoals):
 1. supported_strong M s \<Longrightarrow> False
 2. \<not> supported_strong M s \<and> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t') \<Longrightarrow> False
 3. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> supported_strong M s \<and> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t') \<Longrightarrow> False
 2. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using s(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>s'<s. zcount (c_caps c0 p) s' = 0

goal (2 subgoals):
 1. \<not> supported_strong M s \<and> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t') \<Longrightarrow> False
 2. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using caps_le_ii0
[PROOF STATE]
proof (prove)
using this:
zcount (c_caps c0 p) s \<le> zcount M s

goal (1 subgoal):
 1. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply linarith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t; \<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. \<lbrakk>\<not> supported_strong M t; \<exists>t'<t. 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t; \<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t; \<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t

goal (1 subgoal):
 1. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0
zcount M t < zcount (c_caps c0 p) t

goal (1 subgoal):
 1. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0
zcount M t < zcount (c_caps c0 p) t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0
zcount M t < zcount (c_caps c0 p) t

goal (1 subgoal):
 1. supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
(* positive and negative changes to a least pointstamp are directly reflected in c_caps *)
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0
zcount M t < zcount (c_caps c0 p) t

goal (1 subgoal):
 1. supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
apply (intro disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
unfolding complex_change(3) change(9)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (((c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p) t
[PROOF STEP]
apply (simp only: if_P zcount_union zcount_diff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> zcount M t + (zcount (timestamps (zmset_of \<Delta>mint_msg)) t + zcount (zmset_of \<Delta>mint_self) t - zcount (zmset_of \<Delta>neg) t) < zcount (((c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p) t
[PROOF STEP]
apply (subst complex_change(4)[of t])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> \<forall>t'<t. zcount (c_caps c0 p) t' = 0
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> zcount M t + (0 + zcount (zmset_of \<Delta>mint_self) t - zcount (zmset_of \<Delta>neg) t) < zcount (((c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p) t
[PROOF STEP]
using assms(3)[unfolded InvCapsNonneg_def, rule_format]
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount (c_caps c0 ?p) ?t

goal (2 subgoals):
 1. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> \<forall>t'<t. zcount (c_caps c0 p) t' = 0
 2. \<lbrakk>\<forall>t'<t. zcount (c_caps c0 p) t' \<le> 0; zcount M t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> zcount M t + (0 + zcount (zmset_of \<Delta>mint_self) t - zcount (zmset_of \<Delta>neg) t) < zcount (((c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p) t
[PROOF STEP]
apply (simp_all add: antisym)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t

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

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
next \<comment> \<open>Adding @{term \<Delta>} made @{term M} positive at @{term t} in @{term c}1\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
zcount M t \<le> 0
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
zcount M t \<le> 0
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
assume nosupp: "\<not> supported_strong ?M1 t"
[PROOF STATE]
proof (state)
this:
\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
assume "\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'"
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'
[PROOF STEP]
have nocaps: "\<forall>t'<t. zcount (c_caps c1 p) t' = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'

goal (1 subgoal):
 1. \<forall>t'<t. zcount (c_caps c1 p) t' = 0
[PROOF STEP]
using InvCapsNonneg_def assms(2) assms(3) order_class.le_less performop_preserves_InvCapsNonneg
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'
InvCapsNonneg ?c = (\<forall>p t. 0 \<le> zcount (c_caps ?c p) t)
next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self
InvCapsNonneg c0
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
\<lbrakk>InvCapsNonneg ?c0.0; next_performop' ?c0.0 ?c1.0 ?p ?\<Delta>\<^sub>m ?\<Delta>\<^sub>p\<^sub>1 ?\<Delta>\<^sub>p\<^sub>2\<rbrakk> \<Longrightarrow> InvCapsNonneg ?c1.0

goal (1 subgoal):
 1. \<forall>t'<t. zcount (c_caps c1 p) t' = 0
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>t'<t. zcount (c_caps c1 p) t' = 0

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
assume "\<not> zcount ?M1 t < zcount (c_caps c1 p) t"
[PROOF STATE]
proof (state)
this:
\<not> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have caps_le: "zcount (c_caps c1 p) t \<le> zcount ?M1 t"
[PROOF STATE]
proof (prove)
using this:
\<not> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t

goal (1 subgoal):
 1. zcount (c_caps c1 p) t \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
zcount (c_caps c1 p) t \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
zcount M t \<le> 0
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t
[PROOF STEP]
have "count \<Delta>neg t < zcount ?\<Delta>pos t"
[PROOF STATE]
proof (prove)
using this:
zcount M t \<le> 0
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t

goal (1 subgoal):
 1. int (count \<Delta>neg t) < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (count \<Delta>neg t) < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) t

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int (count \<Delta>neg t) < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) t
[PROOF STEP]
have "0 < count \<Delta>mint_self t \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t"
[PROOF STATE]
proof (prove)
using this:
int (count \<Delta>neg t) < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) t

goal (1 subgoal):
 1. 0 < count \<Delta>mint_self t \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t
[PROOF STEP]
by (metis 2(2) add.commute add.left_neutral not_gr_zero of_nat_0 zero_lt_diff zcount_diff zcount_of_mset zcount_union zcount_zmset_of_nonneg)
[PROOF STATE]
proof (state)
this:
0 < count \<Delta>mint_self t \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < count \<Delta>mint_self t \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t
[PROOF STEP]
obtain s where s: "s \<le> t" "0 < zcount (c_caps c0 p) s" "\<forall>s'<s. zcount (c_caps c0 p) s' = 0"
[PROOF STATE]
proof (prove)
using this:
0 < count \<Delta>mint_self t \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<le> t; 0 < zcount (c_caps c0 p) s; \<forall>s'<s. zcount (c_caps c0 p) s' = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < count \<Delta>mint_self t \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < count \<Delta>mint_self t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
 2. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < count \<Delta>mint_self t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in># \<Delta>mint_self \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (drule change(3)[unfolded minting_self_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'\<le>t. 0 < zcount (c_caps c0 p) t' \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>t' \<le> t; 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (drule order_zmset_exists_foundation)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>t' \<le> t; \<exists>s\<le>t'. 0 < zcount (c_caps c0 p) s \<and> (\<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t' s. \<lbrakk>t' \<le> t; s \<le> t'; 0 < zcount (c_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
subgoal for s' u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<le> t; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (rule exI[of _ u])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<le> t; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> u \<le> t \<and> 0 < zcount (c_caps c0 p) u \<and> (\<forall>s'<u. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<le> t; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> u \<le> t \<and> (\<forall>s'<u. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
using assms(3)[unfolded InvCapsNonneg_def, rule_format]
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount (c_caps c0 ?p) ?t

goal (1 subgoal):
 1. \<lbrakk>s' \<le> t; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> u \<le> t \<and> (\<forall>s'<u. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (metis order.trans order_class.order.not_eq_order_implies_strict)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (drule pos_image_zmset_obtain_pre[rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. 0 \<le> zcount (zmset_of \<Delta>mint_msg) t
 2. \<exists>m. 0 < zcount (zmset_of \<Delta>mint_msg) m \<and> (case m of (x, t) \<Rightarrow> t) = t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. 0 < zcount (zmset_of \<Delta>mint_msg) m \<and> (case m of (x, t) \<Rightarrow> t) = t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. 0 < zcount (zmset_of \<Delta>mint_msg) (a, t) \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
subgoal for p'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (zmset_of \<Delta>mint_msg) (p', t) \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p', t) \<in># \<Delta>mint_msg \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (drule change(4)[unfolded minting_msg_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (p', t) of (pa, t) \<Rightarrow> \<exists>t'<t. 0 < zcount (c_caps c0 p) t' \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'<t. 0 < zcount (c_caps c0 p) t' \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>t' < t; 0 < zcount (c_caps c0 p) t'\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) 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_caps c0 p) s \<and> (\<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s)\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t' s. \<lbrakk>t' < t; s \<le> t'; 0 < zcount (c_caps c0 p) s; \<forall>u. 0 < zcount (c_caps c0 p) u \<longrightarrow> \<not> u < s\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
subgoal for s' u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < t; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. 0 < zcount (c_caps c0 p) s \<and> (\<forall>s'<s. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (rule exI[of _ u])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < t; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> u \<le> t \<and> 0 < zcount (c_caps c0 p) u \<and> (\<forall>s'<u. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' < t; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> u \<le> t \<and> (\<forall>s'<u. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
using assms(3)[unfolded InvCapsNonneg_def, rule_format]
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount (c_caps c0 ?p) ?t

goal (1 subgoal):
 1. \<lbrakk>s' < t; u \<le> s'; 0 < zcount (c_caps c0 p) u; \<forall>ua. 0 < zcount (c_caps c0 p) ua \<longrightarrow> \<not> ua < u\<rbrakk> \<Longrightarrow> u \<le> t \<and> (\<forall>s'<u. zcount (c_caps c0 p) s' = 0)
[PROOF STEP]
apply (metis order.strict_trans1 less_imp_le order_class.order.not_eq_order_implies_strict)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
s \<le> t
0 < zcount (c_caps c0 p) s
\<forall>s'<s. zcount (c_caps c0 p) s' = 0

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have \<Delta>counts:
          "\<And>s. s < t \<Longrightarrow> count \<Delta>neg s = zcount (c_caps c0 p) s"
          "\<And>s. s < t \<Longrightarrow> count \<Delta>mint_self s = 0"
          "\<And>p s'. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p,s') = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s < t \<Longrightarrow> int (count \<Delta>neg s) = zcount (c_caps c0 p) s) &&& (\<And>s. s < t \<Longrightarrow> count \<Delta>mint_self s = 0) &&& (\<And>p s'. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0)
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' < t \<Longrightarrow> int (count \<Delta>neg s') = zcount (c_caps c0 p) s'
[PROOF STEP]
using change(2) nocaps s(1) order_class.order.not_eq_order_implies_strict
[PROOF STATE]
proof (prove)
using this:
\<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t
\<forall>t'<t. zcount (c_caps c1 p) t' = 0
s \<le> t
\<lbrakk>?a \<noteq> ?b; ?a \<le> ?b\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. s' < t \<Longrightarrow> int (count \<Delta>neg s') = zcount (c_caps c0 p) s'
[PROOF STEP]
by (fastforce simp: change(9))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. s < t \<Longrightarrow> count \<Delta>mint_self s = 0
 2. \<And>p s'. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0
[PROOF STEP]
subgoal for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' < t \<Longrightarrow> count \<Delta>mint_self s' = 0
[PROOF STEP]
using nocaps[rule_format, of s']
[PROOF STATE]
proof (prove)
using this:
s' < t \<Longrightarrow> zcount (c_caps c1 p) s' = 0

goal (1 subgoal):
 1. s' < t \<Longrightarrow> count \<Delta>mint_self s' = 0
[PROOF STEP]
by (simp add: change(9) \<open>\<And>s'. s' < t \<Longrightarrow> int (count \<Delta>neg s') = zcount (c_caps c0 p) s'\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p s'. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0
[PROOF STEP]
subgoal for p s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0
[PROOF STEP]
using change(4)[unfolded minting_msg_def, rule_format, of "(p,s')"] s(3)
[PROOF STATE]
proof (prove)
using this:
(p, s') \<in># \<Delta>mint_msg \<Longrightarrow> case (p, s') of (pa, t) \<Rightarrow> \<exists>t'<t. 0 < zcount (c_caps c0 p) t'
\<forall>s'<s. zcount (c_caps c0 p) s' = 0

goal (1 subgoal):
 1. s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (p, s') = 0
[PROOF STEP]
by (force intro: ccontr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
?s < t \<Longrightarrow> int (count \<Delta>neg ?s) = zcount (c_caps c0 p) ?s
?s < t \<Longrightarrow> count \<Delta>mint_self ?s = 0
?s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (?p, ?s') = 0

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?s < t \<Longrightarrow> int (count \<Delta>neg ?s) = zcount (c_caps c0 p) ?s
?s < t \<Longrightarrow> count \<Delta>mint_self ?s = 0
?s' \<le> s \<Longrightarrow> count \<Delta>mint_msg (?p, ?s') = 0

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
assume less: "s < t"
[PROOF STATE]
proof (state)
this:
s < t

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have caps_le_ii0: "zcount (c_caps c0 p) s \<le> zcount M s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (c_caps c0 p) s \<le> zcount M s
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> zcount (c_caps c0 p) s \<le> zcount M s \<Longrightarrow> False
[PROOF STEP]
assume nle: "\<not> zcount (c_caps c0 p) s \<le> zcount M s"
[PROOF STATE]
proof (state)
this:
\<not> zcount (c_caps c0 p) s \<le> zcount M s

goal (1 subgoal):
 1. \<not> zcount (c_caps c0 p) s \<le> zcount M s \<Longrightarrow> False
[PROOF STEP]
have "zcount ?M1 s < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
[PROOF STEP]
unfolding complex_change(3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
[PROOF STEP]
using complex_change(4) nle s(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<?t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) ?t = 0
\<not> zcount (c_caps c0 p) s \<le> zcount M s
\<forall>s'<s. zcount (c_caps c0 p) s' = 0

goal (1 subgoal):
 1. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
[PROOF STEP]
by (auto simp: \<Delta>counts(1,2)[OF less])
[PROOF STATE]
proof (state)
this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0

goal (1 subgoal):
 1. \<not> zcount (c_caps c0 p) s \<le> zcount M s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using less least order.strict_trans2
[PROOF STATE]
proof (prove)
using this:
zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s < 0
s < t
\<forall>t'<t. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' \<le> 0
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c

goal (1 subgoal):
 1. False
[PROOF STEP]
by (force dest!: nosupp[unfolded supported_strong_def, simplified, rule_format] simp: nonpos_upto_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
zcount (c_caps c0 p) s \<le> zcount M s

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
with s(2)
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (c_caps c0 p) s
zcount (c_caps c0 p) s \<le> zcount M s
[PROOF STEP]
have count0s: "0 < zcount M s"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_caps c0 p) s
zcount (c_caps c0 p) s \<le> zcount M s

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

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using inv0[OF count0s]
[PROOF STATE]
proof (prove)
using this:
supported_strong M s \<or> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t') \<or> zcount M s < zcount (c_caps c0 p) s

goal (1 subgoal):
 1. False
[PROOF STEP]
apply (elim disj3_split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. supported_strong M s \<Longrightarrow> False
 2. \<not> supported_strong M s \<and> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t') \<Longrightarrow> False
 3. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supported_strong M s \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. supported_strong M s \<Longrightarrow> False
[PROOF STEP]
assume "supported_strong M s"
[PROOF STATE]
proof (state)
this:
supported_strong M s

goal (1 subgoal):
 1. supported_strong M s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supported_strong M s
[PROOF STEP]
obtain u where u: "u < s" "zcount M u < 0"
[PROOF STATE]
proof (prove)
using this:
supported_strong M s

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u < s; zcount M u < 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[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. (\<And>u. \<lbrakk>u < s; zcount M u < 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u < s
zcount M u < 0

goal (1 subgoal):
 1. supported_strong M s \<Longrightarrow> False
[PROOF STEP]
have "0 \<le> zcount ?M1 u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u
[PROOF STEP]
using least nosupp[unfolded supported_strong_def nonpos_upto_def, simplified, rule_format, of u] order.strict_trans[OF u(1) less]
[PROOF STATE]
proof (prove)
using this:
\<forall>t'<t. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' \<le> 0
\<lbrakk>zcount M u + (int (count {#t. (p, t) \<in># \<Delta>mint_msg#} u) + int (count \<Delta>mint_self u) - int (count \<Delta>neg u)) < 0; u < t\<rbrakk> \<Longrightarrow> \<exists>s\<le>u. \<not> zcount M s + (int (count {#t. (p, t) \<in># \<Delta>mint_msg#} s) + int (count \<Delta>mint_self s) - int (count \<Delta>neg s)) \<le> 0
u < t

goal (1 subgoal):
 1. 0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u

goal (1 subgoal):
 1. supported_strong M s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u
[PROOF STEP]
have "0 < zcount ?\<Delta>pos u"
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u

goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) u
[PROOF STEP]
using \<Delta>counts(1)[of u] s(3) u(1) u(2) less
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) u
u < t \<Longrightarrow> int (count \<Delta>neg u) = zcount (c_caps c0 p) u
\<forall>s'<s. zcount (c_caps c0 p) s' = 0
u < s
zcount M u < 0
s < t

goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) u
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) u

goal (1 subgoal):
 1. supported_strong M s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) u
[PROOF STEP]
have "0 < count \<Delta>mint_self u \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) u

goal (1 subgoal):
 1. 0 < count \<Delta>mint_self u \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u
[PROOF STEP]
using gr0I
[PROOF STATE]
proof (prove)
using this:
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) u
(?n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < ?n

goal (1 subgoal):
 1. 0 < count \<Delta>mint_self u \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
0 < count \<Delta>mint_self u \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u

goal (1 subgoal):
 1. supported_strong M s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < count \<Delta>mint_self u \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u
[PROOF STEP]
obtain u' where "u' \<le> u" "0 < zcount (c_caps c0 p) u'"
[PROOF STATE]
proof (prove)
using this:
0 < count \<Delta>mint_self u \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u

goal (1 subgoal):
 1. (\<And>u'. \<lbrakk>u' \<le> u; 0 < zcount (c_caps c0 p) u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < count \<Delta>mint_self u \<or> 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < count \<Delta>mint_self u \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
 2. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < count \<Delta>mint_self u \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in># \<Delta>mint_self \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
apply (drule change(3)[unfolded minting_self_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'\<le>u. 0 < zcount (c_caps c0 p) t' \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
using s(1) s(2)
[PROOF STATE]
proof (prove)
using this:
s \<le> t
0 < zcount (c_caps c0 p) s

goal (1 subgoal):
 1. \<exists>t'\<le>u. 0 < zcount (c_caps c0 p) t' \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) u \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
apply (drule pos_image_zmset_obtain_pre[rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. 0 \<le> zcount (zmset_of \<Delta>mint_msg) t
 2. \<exists>m. 0 < zcount (zmset_of \<Delta>mint_msg) m \<and> (case m of (x, t) \<Rightarrow> t) = u \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. 0 < zcount (zmset_of \<Delta>mint_msg) m \<and> (case m of (x, t) \<Rightarrow> t) = u \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. 0 < zcount (zmset_of \<Delta>mint_msg) (a, u) \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
subgoal for p'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (zmset_of \<Delta>mint_msg) (p', u) \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p', u) \<in># \<Delta>mint_msg \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
apply (drule change(4)[unfolded minting_msg_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (p', u) of (pa, t) \<Rightarrow> \<exists>t'<t. 0 < zcount (c_caps c0 p) t' \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[PROOF STEP]
using order.strict_iff_order
[PROOF STATE]
proof (prove)
using this:
(?a < ?b) = (?a \<le> ?b \<and> ?a \<noteq> ?b)

goal (1 subgoal):
 1. case (p', u) of (pa, t) \<Rightarrow> \<exists>t'<t. 0 < zcount (c_caps c0 p) t' \<Longrightarrow> \<exists>u'\<le>u. 0 < zcount (c_caps c0 p) u'
[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:
u' \<le> u
0 < zcount (c_caps c0 p) u'

goal (1 subgoal):
 1. supported_strong M s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u' \<le> u
0 < zcount (c_caps c0 p) u'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
u' \<le> u
0 < zcount (c_caps c0 p) u'

goal (1 subgoal):
 1. False
[PROOF STEP]
using s(3) u(1)
[PROOF STATE]
proof (prove)
using this:
u' \<le> u
0 < zcount (c_caps c0 p) u'
\<forall>s'<s. zcount (c_caps c0 p) s' = 0
u < s

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> supported_strong M s \<and> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t') \<Longrightarrow> False
 2. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using s(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>s'<s. zcount (c_caps c0 p) s' = 0

goal (2 subgoals):
 1. \<not> supported_strong M s \<and> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t') \<Longrightarrow> False
 2. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using caps_le_ii0
[PROOF STATE]
proof (prove)
using this:
zcount (c_caps c0 p) s \<le> zcount M s

goal (1 subgoal):
 1. \<lbrakk>\<not> supported_strong M s; \<not> (\<exists>t'<s. 0 < zcount (c_caps c0 p) t'); zcount M s < zcount (c_caps c0 p) s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply linarith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
s < t \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s < t \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
s < t \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
assume eq: "s = t"
[PROOF STATE]
proof (state)
this:
s = t

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have count0t: "0 < zcount M t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount M t
[PROOF STEP]
using eq caps_le change(9) complex_change(3,4) s(2,3)
[PROOF STATE]
proof (prove)
using this:
s = t
zcount (c_caps c1 p) t \<le> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t
c_caps c1 = (c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
IncomingInfo c1 ?k ?p' ?q = (if ?p' = p then IncomingInfo c0 ?k ?p' ?q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 ?k ?p' ?q)
\<forall>t'<?t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) ?t = 0
0 < zcount (c_caps c0 p) s
\<forall>s'<s. zcount (c_caps c0 p) s' = 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. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using 2(1) count0t
[PROOF STATE]
proof (prove)
using this:
zcount M t \<le> 0
0 < zcount M t

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
s = t \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s < t \<Longrightarrow> False
s = t \<Longrightarrow> False
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
s < t \<Longrightarrow> False
s = t \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
using order.not_eq_order_implies_strict s(1)
[PROOF STATE]
proof (prove)
using this:
s < t \<Longrightarrow> False
s = t \<Longrightarrow> False
\<lbrakk>?a \<noteq> ?b; ?a \<le> ?b\<rbrakk> \<Longrightarrow> ?a < ?b
s \<le> t

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t; \<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'; \<not> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>zcount M t \<le> 0; 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t; \<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'; \<not> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t; \<forall>t'<t. \<not> 0 < zcount (c_caps c1 p) t'; \<not> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t \<or> (\<exists>t'<t. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t < zcount (c_caps c1 p) t

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

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) ?t2; \<forall>t'<?t2. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) ?t2 \<or> (\<exists>t'<?t2. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) ?t2 < zcount (c_caps c1 p) ?t2

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) ?t2; \<forall>t'<?t2. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) ?t2 \<or> (\<exists>t'<?t2. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) ?t2 < zcount (c_caps c1 p) ?t2
[PROOF STEP]
show "justified (c_caps c1 p) ?M1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) ?t2; \<forall>t'<?t2. zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) t' \<le> 0\<rbrakk> \<Longrightarrow> supported_strong (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) ?t2 \<or> (\<exists>t'<?t2. 0 < zcount (c_caps c1 p) t') \<or> zcount (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) ?t2 < zcount (c_caps c1 p) ?t2

goal (1 subgoal):
 1. justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
by (intro justified_leastI) blast
[PROOF STATE]
proof (state)
this:
justified (c_caps c1 p) (M + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))

goal:
No subgoals!
[PROOF STEP]
qed