[STATEMENT]
lemma recvupd_preserves_GlobVacantUpto:
  assumes "GlobVacantUpto c0 q t"
    and   "next_recvupd' c0 c1 p q"
    and   "InvInfoJustifiedWithGII c0"
    and   "InvGlobNonposEqVacant c1"
    and   "InvGlobVacantImpRecordsVacant c0"
    and   "InvRecordCount c0"
  shows   "GlobVacantUpto c1 q t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GlobVacantUpto c1 q t
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note npeq1 = assms(4)[unfolded InvGlobNonposEqVacant_def, rule_format]
[PROOF STATE]
proof (state)
this:
GlobVacantUpto c1 ?q ?t = GlobNonposUpto c1 ?q ?t

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note gvu0 = assms(1)[unfolded vacant_upto_def, rule_format]
[PROOF STATE]
proof (state)
this:
?s \<le> t \<Longrightarrow> zcount (c_glob c0 q) ?s = 0

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note nvu0 = assms(5)[unfolded InvGlobVacantImpRecordsVacant_def, rule_format, OF assms(1)]
[PROOF STATE]
proof (state)
this:
RecordsVacantUpto c0 t

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note recordcount = assms(6)[unfolded InvRecordCount_def zmultiset_eq_iff zcount_union, rule_format]
[PROOF STATE]
proof (state)
this:
zcount (records c0) ?a = zcount (GlobalIncomingInfoAt c0 ?q) ?a + zcount (c_glob c0 ?q) ?a

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note change = next_recvupdD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
c_msg c0 p q \<noteq> []
c_temp c1 = c_temp c0
c_msg c1 = (\<lambda>p' q'. if p' = p \<and> q' = q then tl (c_msg c0 p q) else c_msg c0 p' q')
c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))
c_caps c1 = c_caps c0
c_data_msg c1 = c_data_msg c0

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
let ?\<kappa> = "hd (c_msg c0 p q)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
from change(1)
[PROOF STATE]
proof (chain)
picking this:
c_msg c0 p q \<noteq> []
[PROOF STEP]
have ia\<kappa>: "?\<kappa> = InfoAt c0 0 p q"
[PROOF STATE]
proof (prove)
using this:
c_msg c0 p q \<noteq> []

goal (1 subgoal):
 1. hd (c_msg c0 p q) = InfoAt c0 0 p q
[PROOF STEP]
unfolding InfoAt_def
[PROOF STATE]
proof (prove)
using this:
c_msg c0 p q \<noteq> []

goal (1 subgoal):
 1. hd (c_msg c0 p q) = (if 0 \<le> 0 \<and> 0 < length (c_msg c0 p q) then c_msg c0 p q ! 0 else {#}\<^sub>z)
[PROOF STEP]
by (simp add: hd_conv_nth)
[PROOF STATE]
proof (state)
this:
hd (c_msg c0 p q) = InfoAt c0 0 p q

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
assume gvu1: "\<not> GlobVacantUpto c1 q t"
[PROOF STATE]
proof (state)
this:
\<not> GlobVacantUpto c1 q t

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
obtain t' where t':
    "t' \<le> t"
    "0 < zcount (c_glob c1 q) t'"
    "zcount (c_glob c0 q) t' = 0"
    "\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<le> t; 0 < zcount (c_glob c1 q) t'; zcount (c_glob c0 q) t' = 0; \<forall>s<t'. zcount (c_glob c1 q) s \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
using gvu1
[PROOF STATE]
proof (prove)
using this:
\<not> GlobVacantUpto c1 q t

goal (1 subgoal):
 1. \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
unfolding npeq1 nonpos_upto_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>s\<le>t. zcount (c_glob c1 q) s \<le> 0)

goal (1 subgoal):
 1. \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (simp add: not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<le>t. 0 < zcount (c_glob c1 q) s \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<le> t; 0 < zcount (c_glob c1 q) s\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (drule order_zmset_exists_foundation')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<le> t; \<exists>sa\<le>s. 0 < zcount (c_glob c1 q) sa \<and> (\<forall>u<sa. zcount (c_glob c1 q) u \<le> 0)\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>s \<le> t; sa \<le> s; 0 < zcount (c_glob c1 q) sa; \<forall>u<sa. zcount (c_glob c1 q) u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
subgoal for s s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> t; s' \<le> s; 0 < zcount (c_glob c1 q) s'; \<forall>u<s'. zcount (c_glob c1 q) u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (rule exI[of _ s'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> t; s' \<le> s; 0 < zcount (c_glob c1 q) s'; \<forall>u<s'. zcount (c_glob c1 q) u \<le> 0\<rbrakk> \<Longrightarrow> s' \<le> t \<and> 0 < zcount (c_glob c1 q) s' \<and> zcount (c_glob c0 q) s' = 0 \<and> (\<forall>s<s'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
using gvu0
[PROOF STATE]
proof (prove)
using this:
?s \<le> t \<Longrightarrow> zcount (c_glob c0 q) ?s = 0

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

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
from t'(2,3)
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (c_glob c1 q) t'
zcount (c_glob c0 q) t' = 0
[PROOF STEP]
have count\<kappa>: "0 < zcount ?\<kappa> t'"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_glob c1 q) t'
zcount (c_glob c0 q) t' = 0

goal (1 subgoal):
 1. 0 < zcount (hd (c_msg c0 p q)) t'
[PROOF STEP]
by (auto simp: change(4))
[PROOF STATE]
proof (state)
this:
0 < zcount (hd (c_msg c0 p q)) t'

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note assms(3)[unfolded InvInfoJustifiedWithGII_def justified_with_alt, rule_format, OF count\<kappa>[unfolded ia\<kappa>]]
[PROOF STATE]
proof (state)
this:
(\<exists>s<t'. (zcount (InfoAt c0 0 p q) s < 0 \<or> zcount (GlobalIncomingInfo c0 (0 + 1) p q) s < 0) \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)) \<or> (\<exists>s<t'. 0 < zcount (records c0) s) \<or> zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 (0 + 1) p q) t' < zcount (records c0) t'

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>s<t'. (zcount (InfoAt c0 0 p q) s < 0 \<or> zcount (GlobalIncomingInfo c0 (0 + 1) p q) s < 0) \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)) \<or> (\<exists>s<t'. 0 < zcount (records c0) s) \<or> zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 (0 + 1) p q) t' < zcount (records c0) t'
[PROOF STEP]
consider
    "\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)" |
    "\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)"
    "\<nexists>s. s < t' \<and> zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)" |
    "\<exists>s<t'. 0 < zcount (records c0) s" |
    "zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'"
[PROOF STATE]
proof (prove)
using this:
(\<exists>s<t'. (zcount (InfoAt c0 0 p q) s < 0 \<or> zcount (GlobalIncomingInfo c0 (0 + 1) p q) s < 0) \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)) \<or> (\<exists>s<t'. 0 < zcount (records c0) s) \<or> zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 (0 + 1) p q) t' < zcount (records c0) t'

goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> thesis; \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> thesis; \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> thesis; zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> ?thesis; \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> ?thesis; \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> ?thesis; zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> ?thesis; \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> ?thesis; \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> ?thesis; zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> ?thesis; \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> ?thesis; \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> ?thesis; zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)
[PROOF STEP]
obtain s where s: "s < t'" "zcount (InfoAt c0 0 p q) s < 0" "\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s < t'; zcount (InfoAt c0 0 p q) s < 0; \<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s < t'
zcount (InfoAt c0 0 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s < t'
zcount (InfoAt c0 0 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0
[PROOF STEP]
have globs: "zcount (c_glob c1 q) s < 0"
[PROOF STATE]
proof (prove)
using this:
s < t'
zcount (InfoAt c0 0 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0

goal (1 subgoal):
 1. zcount (c_glob c1 q) s < 0
[PROOF STEP]
using gvu0 ia\<kappa> t'(1)
[PROOF STATE]
proof (prove)
using this:
s < t'
zcount (InfoAt c0 0 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0
?s \<le> t \<Longrightarrow> zcount (c_glob c0 q) ?s = 0
hd (c_msg c0 p q) = InfoAt c0 0 p q
t' \<le> t

goal (1 subgoal):
 1. zcount (c_glob c1 q) s < 0
[PROOF STEP]
by (auto simp: change(4))
[PROOF STATE]
proof (state)
this:
zcount (c_glob c1 q) s < 0

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
have "zcount (c_glob c1 q) s \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (c_glob c1 q) s \<le> 0
[PROOF STEP]
using globs
[PROOF STATE]
proof (prove)
using this:
zcount (c_glob c1 q) s < 0

goal (1 subgoal):
 1. zcount (c_glob c1 q) s \<le> 0
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
zcount (c_glob c1 q) s \<le> 0

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (c_glob c1 q) s \<le> 0
[PROOF STEP]
have "\<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0"
[PROOF STATE]
proof (prove)
using this:
zcount (c_glob c1 q) s \<le> 0

goal (1 subgoal):
 1. \<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0
[PROOF STEP]
using s(1) t'(4)
[PROOF STATE]
proof (prove)
using this:
zcount (c_glob c1 q) s \<le> 0
s < t'
\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0

goal (1 subgoal):
 1. \<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
with globs
[PROOF STATE]
proof (chain)
picking this:
zcount (c_glob c1 q) s < 0
\<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
zcount (c_glob c1 q) s < 0
\<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: npeq1[unfolded nonpos_upto_def, symmetric] vacant_upto_def)
[PROOF STATE]
proof (state)
this:
False

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))
[PROOF STEP]
obtain s where s: "s < t'" "zcount (GlobalIncomingInfo c0 1 p q) s < 0" "\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s < t'; zcount (GlobalIncomingInfo c0 1 p q) s < 0; \<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s < t'
zcount (GlobalIncomingInfo c0 1 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
from 2(2) s(1,3)
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))
s < t'
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0
[PROOF STEP]
have "zcount (InfoAt c0 0 p q) s \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))
s < t'
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0

goal (1 subgoal):
 1. 0 \<le> zcount (InfoAt c0 0 p q) s
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 \<le> zcount (InfoAt c0 0 p q) s

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
have rc: "zcount (records c0) s = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (records c0) s = 0
[PROOF STEP]
using order.strict_implies_order order.strict_trans2 nvu0 s(1) t'(1) vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
?a < ?b \<Longrightarrow> ?a \<le> ?b
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c
RecordsVacantUpto c0 t
s < t'
t' \<le> t
vacant_upto ?a ?t \<equiv> \<forall>s\<le>?t. zcount ?a s = 0

goal (1 subgoal):
 1. zcount (records c0) s = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
zcount (records c0) s = 0

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(6) change(1,4) s(1,2) rc t'(4)
[PROOF STATE]
proof (prove)
using this:
InvRecordCount c0
c_msg c0 p q \<noteq> []
c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))
s < t'
zcount (GlobalIncomingInfo c0 1 p q) s < 0
zcount (records c0) s = 0
\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding GII_eq_GIA InvRecordCount_def fun_upd_same
[PROOF STATE]
proof (prove)
using this:
\<forall>q. records c0 = GlobalIncomingInfoAt c0 q + c_glob c0 q
c_msg c0 p q \<noteq> []
c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))
s < t'
zcount (if c_msg c0 p q = [] then GlobalIncomingInfoAt c0 q else GlobalIncomingInfoAt c0 q - hd (c_msg c0 p q)) s < 0
zcount (records c0) s = 0
\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by clarsimp (metis add.commute add_mono_thms_linordered_field(1) not_le recordcount)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 2. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 2. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
\<exists>s<t'. 0 < zcount (records c0) s

goal (2 subgoals):
 1. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 2. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
with nvu0 t'(1)
[PROOF STATE]
proof (chain)
picking this:
RecordsVacantUpto c0 t
t' \<le> t
\<exists>s<t'. 0 < zcount (records c0) s
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
RecordsVacantUpto c0 t
t' \<le> t
\<exists>s<t'. 0 < zcount (records c0) s

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<le>t. zcount (records c0) s = 0
t' \<le> t
\<exists>s<t'. 0 < zcount (records c0) s

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

goal (1 subgoal):
 1. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'

goal (1 subgoal):
 1. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'
[PROOF STEP]
have "0 < zcount (c_glob c0 q) t'"
[PROOF STATE]
proof (prove)
using this:
zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'

goal (1 subgoal):
 1. 0 < zcount (c_glob c0 q) t'
[PROOF STEP]
using change(1) ia\<kappa> t'(3)
[PROOF STATE]
proof (prove)
using this:
zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'
c_msg c0 p q \<noteq> []
hd (c_msg c0 p q) = InfoAt c0 0 p q
zcount (c_glob c0 q) t' = 0

goal (1 subgoal):
 1. 0 < zcount (c_glob c0 q) t'
[PROOF STEP]
unfolding GII_eq_GIA
[PROOF STATE]
proof (prove)
using this:
zcount (InfoAt c0 0 p q + (if c_msg c0 p q = [] then GlobalIncomingInfoAt c0 q else GlobalIncomingInfoAt c0 q - hd (c_msg c0 p q))) t' < zcount (records c0) t'
c_msg c0 p q \<noteq> []
hd (c_msg c0 p q) = InfoAt c0 0 p q
zcount (c_glob c0 q) t' = 0

goal (1 subgoal):
 1. 0 < zcount (c_glob c0 q) t'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>zcount (GlobalIncomingInfoAt c0 q) t' < zcount (records c0) t'; c_msg c0 p q \<noteq> []; hd (c_msg c0 p q) = InfoAt c0 0 p q; zcount (c_glob c0 q) t' = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis add.right_neutral preorder_class.less_irrefl recordcount)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
0 < zcount (c_glob c0 q) t'

goal (1 subgoal):
 1. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (c_glob c0 q) t'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_glob c0 q) t'

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: t'(3))
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed