[STATEMENT]
lemma sendupd_preserves_InvInfoJustifiedWithII:
  assumes "InvInfoJustifiedWithII c0"
    and   "next_sendupd' c0 c1 p' tt"
    and   "InvTempJustified c0"
  shows   "InvInfoJustifiedWithII c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvInfoJustifiedWithII c1
[PROOF STEP]
unfolding InvInfoJustifiedWithII_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k p q. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k p q. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
fix k :: nat and p q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k p q. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
note complex = next_sendupd_complexD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
records c1 = records c0
IncomingInfo c1 0 = IncomingInfo c0 0
IncomingInfo c1 ?k ?p' ?q = (if ?p' = p' \<and> length (c_msg c0 p' ?q) < ?k then IncomingInfo c0 ?k ?p' ?q - {#t \<in>#\<^sub>z c_temp c0 ?p'. t \<in> tt#} else IncomingInfo c0 ?k ?p' ?q)
?k \<le> length (c_msg c0 p' ?q) \<Longrightarrow> IncomingInfo c1 ?k ?p' ?q = IncomingInfo c0 ?k ?p' ?q
length (c_msg c0 p' ?q) < ?k \<Longrightarrow> IncomingInfo c1 ?k ?p' ?q = (if ?p' = p' then IncomingInfo c0 ?k ?p' ?q - {#t \<in>#\<^sub>z c_temp c0 ?p'. t \<in> tt#} else IncomingInfo c0 ?k ?p' ?q)
GlobalIncomingInfoAt c1 ?q = GlobalIncomingInfoAt c0 ?q
InfoAt c1 ?k ?p' ?q = (if ?p' = p' \<and> ?k = length (c_msg c0 p' ?q) then {#t \<in>#\<^sub>z c_temp c0 ?p'. t \<in> tt#} else InfoAt c0 ?k ?p' ?q)

goal (1 subgoal):
 1. \<And>k p q. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
note change = next_sendupdD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
{#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} \<noteq> {#}\<^sub>z
justified (c_caps c0 p') (c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#})
c_temp c1 ?p' = (if ?p' = p' then c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else c_temp c0 ?p')
c_msg c1 = (\<lambda>p'a q. if p'a = p' then c_msg c0 p' q @ [{#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}] else c_msg c0 p'a q)
c_glob c1 = c_glob c0
c_caps c1 = c_caps c0
c_data_msg c1 = c_data_msg c0

goal (1 subgoal):
 1. \<And>k p q. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
consider
    "p' = p" "k < length (c_msg c0 p q)" |
    "p' = p" "k = length (c_msg c0 p q)" |
    "p' = p" "k > length (c_msg c0 p q)" |
    "p' \<noteq> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>p' = p; k < length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> thesis; p' \<noteq> p \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>p' = p; k < length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> ?thesis; p' \<noteq> p \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>k p q. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk>p' = p; k < length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> ?thesis; p' \<noteq> p \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k+1) p q)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>p' = p; k < length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> ?thesis; p' \<noteq> p \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>p' = p; k < length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 3. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 4. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
p' = p
k < length (c_msg c0 p q)

goal (4 subgoals):
 1. \<lbrakk>p' = p; k < length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 3. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 4. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' = p
k < length (c_msg c0 p q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p' = p
k < length (c_msg c0 p q)

goal (1 subgoal):
 1. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
by (metis InvInfoJustifiedWithII_def Suc_eq_plus1 Suc_le_eq assms(1) change(6) complex(4,7) order_class.less_le)
[PROOF STATE]
proof (state)
this:
justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)

goal (3 subgoals):
 1. \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 3. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 3. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
p' = p
k = length (c_msg c0 p q)

goal (3 subgoals):
 1. \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 3. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
have temp0: "c_temp c0 p = InfoAt c1 k p q + c_temp c1 p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_temp c0 p = InfoAt c1 k p q + c_temp c1 p
[PROOF STEP]
unfolding complex change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_temp c0 p = (if p = p' \<and> k = length (c_msg c0 p' q) then {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else InfoAt c0 k p q) + (if p = p' then c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else c_temp c0 p)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
p' = p
k = length (c_msg c0 p q)

goal (1 subgoal):
 1. c_temp c0 p = (if p = p' \<and> k = length (c_msg c0 p' q) then {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else InfoAt c0 k p q) + (if p = p' then c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else c_temp c0 p)
[PROOF STEP]
by (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
c_temp c0 p = InfoAt c1 k p q + c_temp c1 p

goal (3 subgoals):
 1. \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 3. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
have pi: "PositiveImplies (InfoAt c1 k p q) (c_temp c0 p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PositiveImplies (InfoAt c1 k p q) (c_temp c0 p)
[PROOF STEP]
unfolding PositiveImplies_def complex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 < zcount (if p = p' \<and> k = length (c_msg c0 p' q) then {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else InfoAt c0 k p q) t \<longrightarrow> 0 < zcount (c_temp c0 p) t
[PROOF STEP]
using 2(2)
[PROOF STATE]
proof (prove)
using this:
k = length (c_msg c0 p q)

goal (1 subgoal):
 1. \<forall>t. 0 < zcount (if p = p' \<and> k = length (c_msg c0 p' q) then {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else InfoAt c0 k p q) t \<longrightarrow> 0 < zcount (c_temp c0 p) t
[PROOF STEP]
by (auto simp: InfoAt_def)
[PROOF STATE]
proof (state)
this:
PositiveImplies (InfoAt c1 k p q) (c_temp c0 p)

goal (3 subgoals):
 1. \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 3. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
have iitemp: "IncomingInfo c1 (k+1) p q = c_temp c1 p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IncomingInfo c1 (k + 1) p q = c_temp c1 p
[PROOF STEP]
unfolding IncomingInfo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (drop (k + 1) (c_msg c1 p q)) + c_temp c1 p = c_temp c1 p
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
p' = p
k = length (c_msg c0 p q)

goal (1 subgoal):
 1. sum_list (drop (k + 1) (c_msg c1 p q)) + c_temp c1 p = c_temp c1 p
[PROOF STEP]
by (simp add: change)
[PROOF STATE]
proof (state)
this:
IncomingInfo c1 (k + 1) p q = c_temp c1 p

goal (3 subgoals):
 1. \<lbrakk>p' = p; k = length (c_msg c0 p q)\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 3. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
apply (rule PositiveImplies_justified_with)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. justified (c_caps c1 p) (InfoAt c1 k p q + IncomingInfo c1 (k + 1) p q)
 2. PositiveImplies (InfoAt c1 k p q) (InfoAt c1 k p q + IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
unfolding iitemp temp0[symmetric]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. justified (c_caps c1 p) (c_temp c0 p)
 2. PositiveImplies (InfoAt c1 k p q) (c_temp c0 p)
[PROOF STEP]
unfolding change
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. justified (c_caps c0 p) (c_temp c0 p)
 2. PositiveImplies (InfoAt c1 k p q) (c_temp c0 p)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
InvTempJustified c0

goal (2 subgoals):
 1. justified (c_caps c0 p) (c_temp c0 p)
 2. PositiveImplies (InfoAt c1 k p q) (c_temp c0 p)
[PROOF STEP]
apply (simp add: InvTempJustified_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PositiveImplies (InfoAt c1 k p q) (c_temp c0 p)
[PROOF STEP]
using pi
[PROOF STATE]
proof (prove)
using this:
PositiveImplies (InfoAt c1 k p q) (c_temp c0 p)

goal (1 subgoal):
 1. PositiveImplies (InfoAt c1 k p q) (c_temp c0 p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)

goal (2 subgoals):
 1. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
p' = p
length (c_msg c0 p q) < k

goal (2 subgoals):
 1. \<lbrakk>p' = p; length (c_msg c0 p q) < k\<rbrakk> \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
 2. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' = p
length (c_msg c0 p q) < k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p' = p
length (c_msg c0 p q) < k

goal (1 subgoal):
 1. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
by (metis add_cancel_right_left complex(7) justified_with_leastI preorder_class.less_asym InfoAt_def zcount_union)
[PROOF STATE]
proof (state)
this:
justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)

goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
p' \<noteq> p

goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' \<noteq> p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p' \<noteq> p

goal (1 subgoal):
 1. justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
unfolding complex change
[PROOF STATE]
proof (prove)
using this:
p' \<noteq> p

goal (1 subgoal):
 1. justified_with (c_caps c0 p) (if p = p' \<and> k = length (c_msg c0 p' q) then {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else InfoAt c0 k p q) (if p = p' \<and> length (c_msg c0 p' q) < k + 1 then IncomingInfo c0 (k + 1) p q - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else IncomingInfo c0 (k + 1) p q)
[PROOF STEP]
using assms(1)[unfolded InvInfoJustifiedWithII_def, rule_format]
[PROOF STATE]
proof (prove)
using this:
p' \<noteq> p
justified_with (c_caps c0 ?p) (InfoAt c0 ?k ?p ?q) (IncomingInfo c0 (?k + 1) ?p ?q)

goal (1 subgoal):
 1. justified_with (c_caps c0 p) (if p = p' \<and> k = length (c_msg c0 p' q) then {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else InfoAt c0 k p q) (if p = p' \<and> length (c_msg c0 p' q) < k + 1 then IncomingInfo c0 (k + 1) p q - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else IncomingInfo c0 (k + 1) p q)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma recvupd_preserves_InvInfoJustifiedWithII:
  assumes "InvInfoJustifiedWithII c0"
    and   "next_recvupd' c0 c1 p q"
  shows   "InvInfoJustifiedWithII c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvInfoJustifiedWithII c1
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
InvInfoJustifiedWithII c0

goal (1 subgoal):
 1. InvInfoJustifiedWithII c1
[PROOF STEP]
unfolding
    InvInfoJustifiedWithII_def
    next_recvupd_complexD[OF assms(2)]
    next_recvupdD[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<forall>k p q. justified_with (c_caps c0 p) (InfoAt c0 k p q) (IncomingInfo c0 (k + 1) p q)

goal (1 subgoal):
 1. \<forall>k pa qa. justified_with (c_caps c0 pa) (if pa = p \<and> qa = q then InfoAt c0 (k + 1) p q else InfoAt c0 k pa qa) (if pa = p \<and> qa = q then IncomingInfo c0 (k + 1 + 1) pa qa else IncomingInfo c0 (k + 1) pa qa)
[PROOF STEP]
by auto


[STATEMENT]
lemma recvcap_preserves_InvInfoJustifiedWithII:
  assumes "InvInfoJustifiedWithII c0"
    and   "next_recvcap' c0 c1 p t"
  shows   "InvInfoJustifiedWithII c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvInfoJustifiedWithII c1
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
InvInfoJustifiedWithII c0

goal (1 subgoal):
 1. InvInfoJustifiedWithII c1
[PROOF STEP]
unfolding
    InvInfoJustifiedWithII_def
    next_recvcap_complexD[OF assms(2)]
    next_recvcapD[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<forall>k p q. justified_with (c_caps c0 p) (InfoAt c0 k p q) (IncomingInfo c0 (k + 1) p q)

goal (1 subgoal):
 1. \<forall>k pa q. justified_with (((c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z)) pa) (InfoAt c0 k pa q) (IncomingInfo c0 (k + 1) pa q)
[PROOF STEP]
by simp


[STATEMENT]
lemma invs_imp_InvInfoJustifiedWithGII:
  assumes "InvInfoJustifiedWithII c"
    and   "InvJustifiedII c"
    and   "InvCapsNonneg c"
  shows   "InvInfoJustifiedWithGII c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvInfoJustifiedWithGII c
[PROOF STEP]
unfolding InvInfoJustifiedWithGII_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k p q. justified_with (records c) (InfoAt c k p q) (GlobalIncomingInfo c (k + 1) p q)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k p q. justified_with (records c) (InfoAt c k p q) (GlobalIncomingInfo c (k + 1) p q)
[PROOF STEP]
subgoal for k p q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (records c) (InfoAt c k p q) (GlobalIncomingInfo c (k + 1) p q)
[PROOF STEP]
unfolding GlobalIncomingInfo_def records_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (sum (c_caps c) UNIV + timestamps (zmset_of (c_data_msg c))) (InfoAt c k p q) (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then k + 1 else 0) p' q)
[PROOF STEP]
apply (rule justified_with_add_records)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. justified_with (sum (c_caps c) UNIV) (InfoAt c k p q) (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then k + 1 else 0) p' q)
 2. \<forall>t. 0 \<le> zcount (timestamps (zmset_of (c_data_msg c))) t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with (sum (c_caps c) UNIV) (InfoAt c k p q) (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then k + 1 else 0) p' q)
[PROOF STEP]
apply (rule justified_with_sum[where x = p])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. finite UNIV
 2. UNIV \<noteq> {}
 3. p \<in> UNIV
 4. justified_with (c_caps c p) (InfoAt c k p q) (IncomingInfo c (if p = p then k + 1 else 0) p q)
 5. \<forall>p'\<in>UNIV. justified (c_caps c p') (IncomingInfo c (if p' = p then k + 1 else 0) p' q)
 6. \<forall>p'\<in>UNIV. \<forall>t. 0 \<le> zcount (c_caps c p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. UNIV \<noteq> {}
 2. p \<in> UNIV
 3. justified_with (c_caps c p) (InfoAt c k p q) (IncomingInfo c (if p = p then k + 1 else 0) p q)
 4. \<forall>p'\<in>UNIV. justified (c_caps c p') (IncomingInfo c (if p' = p then k + 1 else 0) p' q)
 5. \<forall>p'\<in>UNIV. \<forall>t. 0 \<le> zcount (c_caps c p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. p \<in> UNIV
 2. justified_with (c_caps c p) (InfoAt c k p q) (IncomingInfo c (if p = p then k + 1 else 0) p q)
 3. \<forall>p'\<in>UNIV. justified (c_caps c p') (IncomingInfo c (if p' = p then k + 1 else 0) p' q)
 4. \<forall>p'\<in>UNIV. \<forall>t. 0 \<le> zcount (c_caps c p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. justified_with (c_caps c p) (InfoAt c k p q) (IncomingInfo c (if p = p then k + 1 else 0) p q)
 2. \<forall>p'\<in>UNIV. justified (c_caps c p') (IncomingInfo c (if p' = p then k + 1 else 0) p' q)
 3. \<forall>p'\<in>UNIV. \<forall>t. 0 \<le> zcount (c_caps c p') t
[PROOF STEP]
using assms(1)[unfolded InvInfoJustifiedWithII_def, rule_format, of p k q]
[PROOF STATE]
proof (prove)
using this:
justified_with (c_caps c p) (InfoAt c k p q) (IncomingInfo c (k + 1) p q)

goal (3 subgoals):
 1. justified_with (c_caps c p) (InfoAt c k p q) (IncomingInfo c (if p = p then k + 1 else 0) p q)
 2. \<forall>p'\<in>UNIV. justified (c_caps c p') (IncomingInfo c (if p' = p then k + 1 else 0) p' q)
 3. \<forall>p'\<in>UNIV. \<forall>t. 0 \<le> zcount (c_caps c p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>p'\<in>UNIV. justified (c_caps c p') (IncomingInfo c (if p' = p then k + 1 else 0) p' q)
 2. \<forall>p'\<in>UNIV. \<forall>t. 0 \<le> zcount (c_caps c p') t
[PROOF STEP]
using assms(2)[unfolded InvJustifiedII_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>k p q. justified (c_caps c p) (IncomingInfo c k p q)

goal (2 subgoals):
 1. \<forall>p'\<in>UNIV. justified (c_caps c p') (IncomingInfo c (if p' = p then k + 1 else 0) p' q)
 2. \<forall>p'\<in>UNIV. \<forall>t. 0 \<le> zcount (c_caps c p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p'\<in>UNIV. \<forall>t. 0 \<le> zcount (c_caps c p') t
[PROOF STEP]
using assms(3)[unfolded InvCapsNonneg_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>p t. 0 \<le> zcount (c_caps c p) t

goal (1 subgoal):
 1. \<forall>p'\<in>UNIV. \<forall>t. 0 \<le> zcount (c_caps c p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 \<le> zcount (timestamps (zmset_of (c_data_msg c))) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma next'_preserves_InvInfoJustifiedWithII:
  assumes "InvInfoJustifiedWithII c0"
    and   "next' c0 c1"
    and   "InvCapsNonneg c0"
    and   "InvJustifiedII c0"
    and   "InvTempJustified c0"
  shows   "InvInfoJustifiedWithII c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvInfoJustifiedWithII c1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvInfoJustifiedWithII c0
next' c0 c1
InvCapsNonneg c0
InvJustifiedII c0
InvTempJustified c0

goal (1 subgoal):
 1. InvInfoJustifiedWithII c1
[PROOF STEP]
unfolding next'_def
[PROOF STATE]
proof (prove)
using this:
InvInfoJustifiedWithII c0
next_performop c0 c1 \<or> next_sendupd c0 c1 \<or> next_recvupd c0 c1 \<or> next_recvcap c0 c1 \<or> c1 = c0
InvCapsNonneg c0
InvJustifiedII c0
InvTempJustified c0

goal (1 subgoal):
 1. InvInfoJustifiedWithII c1
[PROOF STEP]
apply (elim disjE exE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>p \<Delta>neg \<Delta>mint_msg x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 2. \<And>p x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_sendupd' c0 c1 p x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 3. \<And>p x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_recvupd' c0 c1 p x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 4. \<And>p x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_recvcap' c0 c1 p x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 5. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; c1 = c0\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
[PROOF STEP]
apply (drule (4) performop_preserves_InvInfoJustifiedWithII)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>p x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_sendupd' c0 c1 p x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 2. \<And>p x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_recvupd' c0 c1 p x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 3. \<And>p x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_recvcap' c0 c1 p x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 4. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; c1 = c0\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
[PROOF STEP]
apply (drule (3) sendupd_preserves_InvInfoJustifiedWithII)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_recvupd' c0 c1 p x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 2. \<And>p x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_recvcap' c0 c1 p x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 3. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; c1 = c0\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
[PROOF STEP]
apply (drule (2) recvupd_preserves_InvInfoJustifiedWithII)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p x. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; next_recvcap' c0 c1 p x\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
 2. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; c1 = c0\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
[PROOF STEP]
apply (drule (2) recvcap_preserves_InvInfoJustifiedWithII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithII c0; InvCapsNonneg c0; InvJustifiedII c0; InvTempJustified c0; c1 = c0\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII c1
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma alw_InvInfoJustifiedWithII: "spec s \<Longrightarrow> alw (holds InvInfoJustifiedWithII) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvInfoJustifiedWithII) s
[PROOF STEP]
apply (frule alw_InvCapsNonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvCapsNonneg) s\<rbrakk> \<Longrightarrow> alw (holds InvInfoJustifiedWithII) s
[PROOF STEP]
apply (frule alw_InvJustifiedII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvCapsNonneg) s; alw (holds InvJustifiedII) s\<rbrakk> \<Longrightarrow> alw (holds InvInfoJustifiedWithII) s
[PROOF STEP]
apply (frule alw_InvTempJustified)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvCapsNonneg) s; alw (holds InvJustifiedII) s; alw (holds InvTempJustified) s\<rbrakk> \<Longrightarrow> alw (holds InvInfoJustifiedWithII) s
[PROOF STEP]
unfolding spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds init_config s \<and> alw next s; alw (holds InvCapsNonneg) s; alw (holds InvJustifiedII) s; alw (holds InvTempJustified) s\<rbrakk> \<Longrightarrow> alw (holds InvInfoJustifiedWithII) s
[PROOF STEP]
apply (elim conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvCapsNonneg) s; alw (holds InvJustifiedII) s; alw (holds InvTempJustified) s; holds init_config s; alw next s\<rbrakk> \<Longrightarrow> alw (holds InvInfoJustifiedWithII) s
[PROOF STEP]
apply (subst (asm) holds.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvCapsNonneg) s; alw (holds InvJustifiedII) s; alw (holds InvTempJustified) s; init_config (shd s); alw next s\<rbrakk> \<Longrightarrow> alw (holds InvInfoJustifiedWithII) s
[PROOF STEP]
apply (drule init_config_implies_InvInfoJustifiedWithII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvCapsNonneg) s; alw (holds InvJustifiedII) s; alw (holds InvTempJustified) s; alw next s; InvInfoJustifiedWithII (shd s)\<rbrakk> \<Longrightarrow> alw (holds InvInfoJustifiedWithII) s
[PROOF STEP]
apply (coinduction arbitrary: s rule: alw.coinduct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw (holds InvCapsNonneg) s; alw (holds InvJustifiedII) s; alw (holds InvTempJustified) s; alw next s; InvInfoJustifiedWithII (shd s)\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> holds InvInfoJustifiedWithII xs \<and> ((\<exists>s. stl xs = s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvJustifiedII) s \<and> alw (holds InvTempJustified) s \<and> alw next s \<and> InvInfoJustifiedWithII (shd s)) \<or> alw (holds InvInfoJustifiedWithII) (stl xs))
[PROOF STEP]
apply (subst (asm) (1 2 3) alw_nxt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>holds InvCapsNonneg s \<and> nxt (alw (holds InvCapsNonneg)) s; holds InvJustifiedII s \<and> nxt (alw (holds InvJustifiedII)) s; holds InvTempJustified s \<and> nxt (alw (holds InvTempJustified)) s; alw next s; InvInfoJustifiedWithII (shd s)\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> holds InvInfoJustifiedWithII xs \<and> ((\<exists>s. stl xs = s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvJustifiedII) s \<and> alw (holds InvTempJustified) s \<and> alw next s \<and> InvInfoJustifiedWithII (shd s)) \<or> alw (holds InvInfoJustifiedWithII) (stl xs))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw next s; InvInfoJustifiedWithII (shd s); InvCapsNonneg (shd s); alw (holds InvCapsNonneg) (stl s); InvJustifiedII (shd s); alw (holds InvJustifiedII) (stl s); InvTempJustified (shd s); alw (holds InvTempJustified) (stl s); \<not> alw (holds InvInfoJustifiedWithII) (stl s)\<rbrakk> \<Longrightarrow> alw next (stl s) \<and> InvInfoJustifiedWithII (shd (stl s))
[PROOF STEP]
using next'_preserves_InvInfoJustifiedWithII
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvInfoJustifiedWithII ?c0.0; next' ?c0.0 ?c1.0; InvCapsNonneg ?c0.0; InvJustifiedII ?c0.0; InvTempJustified ?c0.0\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII ?c1.0

goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw next s; InvInfoJustifiedWithII (shd s); InvCapsNonneg (shd s); alw (holds InvCapsNonneg) (stl s); InvJustifiedII (shd s); alw (holds InvJustifiedII) (stl s); InvTempJustified (shd s); alw (holds InvTempJustified) (stl s); \<not> alw (holds InvInfoJustifiedWithII) (stl s)\<rbrakk> \<Longrightarrow> alw next (stl s) \<and> InvInfoJustifiedWithII (shd (stl s))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma alw_InvInfoJustifiedWithGII: "spec s \<Longrightarrow> alw (holds InvInfoJustifiedWithGII) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvInfoJustifiedWithGII) s
[PROOF STEP]
by (metis alw_InvCapsNonneg alw_InvInfoJustifiedWithII alw_InvJustifiedII alw_iff_sdrop holds.elims(2,3) invs_imp_InvInfoJustifiedWithGII)


[STATEMENT]
lemma not_InvMsgInGlob_imp_not_SafeGlobMono:
  assumes "\<not> InvMsgInGlob c0"
    and   "InvGlobNonposEqVacant c0"
  shows   "\<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1
[PROOF STEP]
note npeq0 = assms(2)[unfolded InvGlobNonposEqVacant_def, rule_format]
[PROOF STATE]
proof (state)
this:
GlobVacantUpto c0 ?q ?t = GlobNonposUpto c0 ?q ?t

goal (1 subgoal):
 1. \<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<not> InvMsgInGlob c0
[PROOF STEP]
obtain p q t c1 where t:
    "next_recvupd' c0 c1 p q"
    "t \<in>#\<^sub>z hd (c_msg c0 p q)"
    "GlobVacantUpto c0 q t"
[PROOF STATE]
proof (prove)
using this:
\<not> InvMsgInGlob c0

goal (1 subgoal):
 1. (\<And>c1 p q t. \<lbrakk>next_recvupd' c0 c1 p q; t \<in>#\<^sub>z hd (c_msg c0 p q); GlobVacantUpto c0 q t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: InvMsgInGlob_def npeq0 nonpos_upto_def not_less dest!: ex_next_recvupd)
[PROOF STATE]
proof (state)
this:
next_recvupd' c0 c1 p q
t \<in>#\<^sub>z hd (c_msg c0 p q)
GlobVacantUpto c0 q t

goal (1 subgoal):
 1. \<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1
[PROOF STEP]
have nvu: "\<not> GlobVacantUpto c1 q t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t
[PROOF STEP]
unfolding vacant_upto_def next_recvupdD(4)[OF t(1)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>s\<le>t. zcount (((c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))) q) s = 0)
[PROOF STEP]
using t(2) t(3) vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
t \<in>#\<^sub>z hd (c_msg c0 p q)
GlobVacantUpto c0 q t
vacant_upto ?a ?t \<equiv> \<forall>s\<le>?t. zcount ?a s = 0

goal (1 subgoal):
 1. \<not> (\<forall>s\<le>t. zcount (((c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))) q) s = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> GlobVacantUpto c1 q t

goal (1 subgoal):
 1. \<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1
[PROOF STEP]
from t(3) nvu
[PROOF STATE]
proof (chain)
picking this:
GlobVacantUpto c0 q t
\<not> GlobVacantUpto c1 q t
[PROOF STEP]
have "\<not> SafeGlobMono c0 c1"
[PROOF STATE]
proof (prove)
using this:
GlobVacantUpto c0 q t
\<not> GlobVacantUpto c1 q t

goal (1 subgoal):
 1. \<not> SafeGlobMono c0 c1
[PROOF STEP]
by (auto simp: SafeGlobMono_def)
[PROOF STATE]
proof (state)
this:
\<not> SafeGlobMono c0 c1

goal (1 subgoal):
 1. \<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1
[PROOF STEP]
with t(1)
[PROOF STATE]
proof (chain)
picking this:
next_recvupd' c0 c1 p q
\<not> SafeGlobMono c0 c1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
next_recvupd' c0 c1 p q
\<not> SafeGlobMono c0 c1

goal (1 subgoal):
 1. \<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma GII_eq_GIA: "GlobalIncomingInfo c 1 p q = (if c_msg c p q = [] then GlobalIncomingInfoAt c q else GlobalIncomingInfoAt c q - hd (c_msg c p q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GlobalIncomingInfo c 1 p q = (if c_msg c p q = [] then GlobalIncomingInfoAt c q else GlobalIncomingInfoAt c q - hd (c_msg c p q))
[PROOF STEP]
unfolding GlobalIncomingInfo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then 1 else 0) p' q) = (if c_msg c p q = [] then \<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q else (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q) - hd (c_msg c p q))
[PROOF STEP]
apply (cases "c_msg c p q = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. c_msg c p q = [] \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then 1 else 0) p' q) = (if c_msg c p q = [] then \<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q else (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q) - hd (c_msg c p q))
 2. c_msg c p q \<noteq> [] \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then 1 else 0) p' q) = (if c_msg c p q = [] then \<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q else (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q) - hd (c_msg c p q))
[PROOF STEP]
apply (simp add: IncomingInfo_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. c_msg c p q = [] \<Longrightarrow> (\<Sum>p'\<in>UNIV. sum_list (drop (if p' = p then 1 else 0) (c_msg c p' q)) + c_temp c p') = (\<Sum>p'\<in>UNIV. sum_list (c_msg c p' q) + c_temp c p')
 2. c_msg c p q \<noteq> [] \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then 1 else 0) p' q) = (if c_msg c p q = [] then \<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q else (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q) - hd (c_msg c p q))
[PROOF STEP]
apply (rule sum.cong[OF refl], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_msg c p q \<noteq> [] \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then 1 else 0) p' q) = (if c_msg c p q = [] then \<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q else (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = q then 0 else 0) p' q) - hd (c_msg c p q))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_msg c p q \<noteq> [] \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then 1 else 0) p' q) = (\<Sum>p'\<in>UNIV. IncomingInfo c 0 p' q) - hd (c_msg c p q)
[PROOF STEP]
apply (subst diff_conv_add_uminus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_msg c p q \<noteq> [] \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then 1 else 0) p' q) = (\<Sum>p'\<in>UNIV. IncomingInfo c 0 p' q) + - hd (c_msg c p q)
[PROOF STEP]
apply (rule Sum_eq_pick_changed_elem)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. c_msg c p q \<noteq> [] \<Longrightarrow> finite UNIV
 2. c_msg c p q \<noteq> [] \<Longrightarrow> ?m13 \<in> UNIV
 3. c_msg c p q \<noteq> [] \<Longrightarrow> IncomingInfo c (if ?m13 = p then 1 else 0) ?m13 q = IncomingInfo c 0 ?m13 q + - hd (c_msg c p q)
 4. \<And>n. \<lbrakk>c_msg c p q \<noteq> []; n \<noteq> ?m13 \<and> n \<in> UNIV\<rbrakk> \<Longrightarrow> IncomingInfo c (if n = p then 1 else 0) n q = IncomingInfo c 0 n q
[PROOF STEP]
apply (auto simp: IncomingInfo_def drop_Suc sum_list_hd_tl algebra_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma recvupd_imp_SafeGlobMono:
  assumes "next_recvupd' c0 c1 p q"
    and   "InvInfoJustifiedWithGII c0"
    and   "InvGlobNonposEqVacant c1"
    and   "InvGlobVacantImpRecordsVacant c0"
    and   "InvRecordCount c0"
  shows   "SafeGlobMono c0 c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SafeGlobMono c0 c1
[PROOF STEP]
unfolding SafeGlobMono_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p t. GlobVacantUpto c0 p t \<longrightarrow> GlobVacantUpto c1 p t
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p t. GlobVacantUpto c0 p t \<Longrightarrow> GlobVacantUpto c1 p t
[PROOF STEP]
subgoal for q' t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GlobVacantUpto c0 q' t \<Longrightarrow> GlobVacantUpto c1 q' t
[PROOF STEP]
apply (cases "q'=q")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> GlobVacantUpto c1 q' t
 2. \<lbrakk>GlobVacantUpto c0 q' t; q' \<noteq> q\<rbrakk> \<Longrightarrow> GlobVacantUpto c1 q' t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> GlobVacantUpto c1 q' t
[PROOF STEP]
apply (rule recvupd_preserves_GlobVacantUpto)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> GlobVacantUpto ?c0.0 q' t
 2. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> next_recvupd' ?c0.0 c1 ?p q'
 3. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithGII ?c0.0
 4. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant c1
 5. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant ?c0.0
 6. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> InvRecordCount ?c0.0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next_recvupd' c0 c1 p q
InvInfoJustifiedWithGII c0
InvGlobNonposEqVacant c1
InvGlobVacantImpRecordsVacant c0
InvRecordCount c0

goal (6 subgoals):
 1. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> GlobVacantUpto ?c0.0 q' t
 2. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> next_recvupd' ?c0.0 c1 ?p q'
 3. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithGII ?c0.0
 4. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant c1
 5. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant ?c0.0
 6. \<lbrakk>GlobVacantUpto c0 q' t; q' = q\<rbrakk> \<Longrightarrow> InvRecordCount ?c0.0
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GlobVacantUpto c0 q' t; q' \<noteq> q\<rbrakk> \<Longrightarrow> GlobVacantUpto c1 q' t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GlobVacantUpto c0 q' t; q' \<noteq> q\<rbrakk> \<Longrightarrow> GlobVacantUpto c1 q' t
[PROOF STEP]
unfolding next_recvupdD[OF assms(1)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GlobVacantUpto c0 q' t; q' \<noteq> q\<rbrakk> \<Longrightarrow> vacant_upto (((c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))) q') t
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma next'_imp_SafeGlobMono:
  assumes "next' c0 c1"
    and   "InvInfoJustifiedWithGII c0"
    and   "InvGlobNonposEqVacant c1"
    and   "InvGlobVacantImpRecordsVacant c0"
    and   "InvRecordCount c0"
  shows   "SafeGlobMono c0 c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SafeGlobMono c0 c1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next' c0 c1
InvInfoJustifiedWithGII c0
InvGlobNonposEqVacant c1
InvGlobVacantImpRecordsVacant c0
InvRecordCount c0

goal (1 subgoal):
 1. SafeGlobMono c0 c1
[PROOF STEP]
unfolding next'_def
[PROOF STATE]
proof (prove)
using this:
next_performop c0 c1 \<or> next_sendupd c0 c1 \<or> next_recvupd c0 c1 \<or> next_recvcap c0 c1 \<or> c1 = c0
InvInfoJustifiedWithGII c0
InvGlobNonposEqVacant c1
InvGlobVacantImpRecordsVacant c0
InvRecordCount c0

goal (1 subgoal):
 1. SafeGlobMono c0 c1
[PROOF STEP]
apply (elim disjE exE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>p \<Delta>neg \<Delta>mint_msg x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 2. \<And>p x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_sendupd' c0 c1 p x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 3. \<And>p x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_recvupd' c0 c1 p x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 4. \<And>p x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_recvcap' c0 c1 p x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 5. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_performop' c0 c1 p_ \<Delta>neg_ \<Delta>mint_msg_ x_\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
by (auto simp: SafeGlobMono_def dest: next_performopD(7))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>p x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_sendupd' c0 c1 p x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 2. \<And>p x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_recvupd' c0 c1 p x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 3. \<And>p x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_recvcap' c0 c1 p x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 4. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_sendupd' c0 c1 p_ x_\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
by (auto simp: SafeGlobMono_def dest: next_sendupdD(5))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_recvupd' c0 c1 p x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 2. \<And>p x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_recvcap' c0 c1 p x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 3. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_recvupd' c0 c1 p_ x_\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
by (auto intro: recvupd_imp_SafeGlobMono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p x. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_recvcap' c0 c1 p x\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
 2. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; next_recvcap' c0 c1 p_ x_\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
by (auto simp: SafeGlobMono_def dest: next_recvcapD(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c1; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> SafeGlobMono c0 c1
[PROOF STEP]
by (simp add: SafeGlobMono_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma invs_imp_InvMsgInGlob:
  fixes c0 :: "('p::finite, 'a) configuration"
  assumes "InvInfoJustifiedWithGII c0"
    and   "InvGlobNonposEqVacant c0"
    and   "InvGlobVacantImpRecordsVacant c0"
    and   "InvRecordCount c0"
    and   "InvJustifiedII c0"
    and   "InvCapsNonneg c0"
    and   "InvRecordsNonneg c0"
  shows   "InvMsgInGlob c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvMsgInGlob c0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvInfoJustifiedWithGII c0
InvGlobNonposEqVacant c0
InvGlobVacantImpRecordsVacant c0
InvRecordCount c0
InvJustifiedII c0
InvCapsNonneg c0
InvRecordsNonneg c0

goal (1 subgoal):
 1. InvMsgInGlob c0
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0\<rbrakk> \<Longrightarrow> InvMsgInGlob c0
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> InvMsgInGlob c0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule not_InvMsgInGlob_imp_not_SafeGlobMono[rotated, OF assms(2)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<exists>c1. next_recvupd c0 c1 \<and> \<not> SafeGlobMono c0 c1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule recvupd_imp_SafeGlobMono)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithGII c0
 2. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant c1
 3. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant c0
 4. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvRecordCount c0
 5. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q; SafeGlobMono c0 c1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant c1
 2. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant c0
 3. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvRecordCount c0
 4. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q; SafeGlobMono c0 c1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant c1_
[PROOF STEP]
apply (rule invs_imp_InvGlobNonposEqVacant)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvRecordCount c1_
 2. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvJustifiedGII c1_
 3. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvRecordsNonneg c1_
[PROOF STEP]
apply (drule (2) recvupd_preserves_InvRecordCount)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvJustifiedGII c1_
 2. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvRecordsNonneg c1_
[PROOF STEP]
apply (drule (1) recvupd_preserves_InvJustifiedII)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_; InvJustifiedII c1_\<rbrakk> \<Longrightarrow> InvJustifiedGII c1_
 2. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvRecordsNonneg c1_
[PROOF STEP]
apply (rule InvJustifiedII_implies_InvJustifiedGII)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_; InvJustifiedII c1_\<rbrakk> \<Longrightarrow> InvJustifiedII c1_
 2. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_; InvJustifiedII c1_\<rbrakk> \<Longrightarrow> InvCapsNonneg c1_
 3. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvRecordsNonneg c1_
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_; InvJustifiedII c1_\<rbrakk> \<Longrightarrow> InvCapsNonneg c1_
 2. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvRecordsNonneg c1_
[PROOF STEP]
apply (drule (2) recvupd_preserves_InvCapsNonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1_; next_recvupd' c0 c1_ p_ q_\<rbrakk> \<Longrightarrow> InvRecordsNonneg c1_
[PROOF STEP]
apply (simp add: InvRecordsNonneg_def next_recvupd_complexD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant c0
 2. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvRecordCount c0
 3. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q; SafeGlobMono c0 c1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q\<rbrakk> \<Longrightarrow> InvRecordCount c0
 2. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q; SafeGlobMono c0 c1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c1 p q. \<lbrakk>InvInfoJustifiedWithGII c0; InvGlobNonposEqVacant c0; InvGlobVacantImpRecordsVacant c0; InvRecordCount c0; InvJustifiedII c0; InvCapsNonneg c0; InvRecordsNonneg c0; \<not> SafeGlobMono c0 c1; next_recvupd' c0 c1 p q; SafeGlobMono c0 c1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma alw_SafeGlobMono: "spec s \<Longrightarrow> alw (relates SafeGlobMono) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
assume spec: "spec s"
[PROOF STATE]
proof (state)
this:
spec s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
spec s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
assume "alw next s"
[PROOF STATE]
proof (state)
this:
alw next s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
alw next s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
assume "alw (holds InvGlobNonposEqVacant) s"
[PROOF STATE]
proof (state)
this:
alw (holds InvGlobNonposEqVacant) s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
alw (holds InvGlobNonposEqVacant) s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
assume "alw (holds InvGlobVacantImpRecordsVacant) s"
[PROOF STATE]
proof (state)
this:
alw (holds InvGlobVacantImpRecordsVacant) s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
alw (holds InvGlobVacantImpRecordsVacant) s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
assume "alw (holds InvInfoJustifiedWithGII) s"
[PROOF STATE]
proof (state)
this:
alw (holds InvInfoJustifiedWithGII) s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
alw (holds InvInfoJustifiedWithGII) s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
assume "alw (holds InvRecordCount) s"
[PROOF STATE]
proof (state)
this:
alw (holds InvRecordCount) s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
alw next s
alw (holds InvGlobNonposEqVacant) s
alw (holds InvGlobVacantImpRecordsVacant) s
alw (holds InvInfoJustifiedWithGII) s
alw (holds InvRecordCount) s
[PROOF STEP]
have "alw (relates SafeGlobMono) s"
[PROOF STATE]
proof (prove)
using this:
alw next s
alw (holds InvGlobNonposEqVacant) s
alw (holds InvGlobVacantImpRecordsVacant) s
alw (holds InvInfoJustifiedWithGII) s
alw (holds InvRecordCount) s

goal (1 subgoal):
 1. alw (relates SafeGlobMono) s
[PROOF STEP]
apply (coinduction arbitrary: s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> relates SafeGlobMono xs \<and> ((\<exists>s. stl xs = s \<and> alw next s \<and> alw (holds InvGlobNonposEqVacant) s \<and> alw (holds InvGlobVacantImpRecordsVacant) s \<and> alw (holds InvInfoJustifiedWithGII) s \<and> alw (holds InvRecordCount) s) \<or> alw (relates SafeGlobMono) (stl xs))
[PROOF STEP]
apply (clarsimp simp: relates_def intro!: next'_imp_SafeGlobMono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> SafeGlobMono (shd s) (shd (stl s)) \<and> (alw next (stl s) \<and> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvInfoJustifiedWithGII) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<or> alw (relates SafeGlobMono) (stl s))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> SafeGlobMono (shd s) (shd (stl s))
 2. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw next (stl s) \<and> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvInfoJustifiedWithGII) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<or> alw (relates SafeGlobMono) (stl s)
[PROOF STEP]
apply (rule next'_imp_SafeGlobMono)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> next s
 2. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithGII (shd s)
 3. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant (shd (stl s))
 4. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant (shd s)
 5. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvRecordCount (shd s)
 6. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw next (stl s) \<and> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvInfoJustifiedWithGII) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<or> alw (relates SafeGlobMono) (stl s)
[PROOF STEP]
apply auto [2]
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant (shd (stl s))
 2. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant (shd s)
 3. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvRecordCount (shd s)
 4. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw next (stl s) \<and> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvInfoJustifiedWithGII) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<or> alw (relates SafeGlobMono) (stl s)
[PROOF STEP]
apply (subst (asm) alw_holds2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>alw next s; InvGlobNonposEqVacant (shd s) \<and> alw (holds InvGlobNonposEqVacant) (stl s); alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant (shd (stl s))
 2. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant (shd s)
 3. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvRecordCount (shd s)
 4. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw next (stl s) \<and> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvInfoJustifiedWithGII) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<or> alw (relates SafeGlobMono) (stl s)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s; InvGlobNonposEqVacant (shd s); alw (holds InvGlobNonposEqVacant) (stl s)\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant (shd (stl s))
 2. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant (shd s)
 3. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvRecordCount (shd s)
 4. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw next (stl s) \<and> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvInfoJustifiedWithGII) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<or> alw (relates SafeGlobMono) (stl s)
[PROOF STEP]
apply (drule alwD)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>InvGlobNonposEqVacant (shd s); next s; holds InvGlobVacantImpRecordsVacant s; holds InvInfoJustifiedWithGII s; holds InvRecordCount s; holds InvGlobNonposEqVacant (stl s)\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant (shd (stl s))
 2. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant (shd s)
 3. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvRecordCount (shd s)
 4. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw next (stl s) \<and> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvInfoJustifiedWithGII) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<or> alw (relates SafeGlobMono) (stl s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant (shd s)
 2. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> InvRecordCount (shd s)
 3. \<And>s. \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw next (stl s) \<and> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvInfoJustifiedWithGII) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<or> alw (relates SafeGlobMono) (stl s)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
alw (relates SafeGlobMono) s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
with spec
[PROOF STATE]
proof (chain)
picking this:
spec s
\<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
spec s
\<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s

goal (1 subgoal):
 1. alw (relates SafeGlobMono) s
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
apply (frule alw_InvGlobNonposEqVacant)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s; alw (holds InvGlobNonposEqVacant) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
apply (frule alw_InvGlobVacantImpRecordsVacant)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
apply (frule alw_InvInfoJustifiedWithGII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
apply (frule alw_InvRecordCount)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
unfolding spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds init_config s \<and> alw next s; \<lbrakk>alw next s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (relates SafeGlobMono) s
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
alw (relates SafeGlobMono) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alw_InvMsgInGlob: "spec s \<Longrightarrow> alw (holds InvMsgInGlob) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvMsgInGlob) s
[PROOF STEP]
apply (frule alw_InvInfoJustifiedWithGII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvInfoJustifiedWithGII) s\<rbrakk> \<Longrightarrow> alw (holds InvMsgInGlob) s
[PROOF STEP]
apply (frule alw_InvGlobNonposEqVacant)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvGlobNonposEqVacant) s\<rbrakk> \<Longrightarrow> alw (holds InvMsgInGlob) s
[PROOF STEP]
apply (frule alw_InvGlobVacantImpRecordsVacant)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s\<rbrakk> \<Longrightarrow> alw (holds InvMsgInGlob) s
[PROOF STEP]
apply (frule alw_InvRecordCount)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (holds InvMsgInGlob) s
[PROOF STEP]
apply (frule alw_InvJustifiedII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvJustifiedII) s\<rbrakk> \<Longrightarrow> alw (holds InvMsgInGlob) s
[PROOF STEP]
apply (frule alw_InvCapsNonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvInfoJustifiedWithGII) s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvJustifiedII) s; alw (holds InvCapsNonneg) s\<rbrakk> \<Longrightarrow> alw (holds InvMsgInGlob) s
[PROOF STEP]
apply (drule alw_InvRecordsNonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvInfoJustifiedWithGII) s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvJustifiedII) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s\<rbrakk> \<Longrightarrow> alw (holds InvMsgInGlob) s
[PROOF STEP]
apply (simp add: alw_iff_sdrop invs_imp_InvMsgInGlob)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SafeGlobMono_preserves_vacant:
  assumes "\<forall>t'\<le>t. zcount (c_glob c0 q) t' = 0"
    and   "(\<lambda>c0 c1. SafeGlobMono c0 c1)\<^sup>*\<^sup>* c0 c1"
  shows   "\<forall>t'\<le>t. zcount (c_glob c1 q) t' = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t'\<le>t. zcount (c_glob c1 q) t' = 0
[PROOF STEP]
using assms(2,1)
[PROOF STATE]
proof (prove)
using this:
SafeGlobMono\<^sup>*\<^sup>* c0 c1
\<forall>t'\<le>t. zcount (c_glob c0 q) t' = 0

goal (1 subgoal):
 1. \<forall>t'\<le>t. zcount (c_glob c1 q) t' = 0
[PROOF STEP]
by (induct rule: rtranclp_induct)(auto simp: SafeGlobMono_def vacant_upto_def)


[STATEMENT]
lemma rtranclp_all_imp_rel: "r\<^sup>*\<^sup>* x y \<Longrightarrow> \<forall>a b. r a b \<longrightarrow> r' a b \<Longrightarrow> r'\<^sup>*\<^sup>* x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r\<^sup>*\<^sup>* x y; \<forall>a b. r a b \<longrightarrow> r' a b\<rbrakk> \<Longrightarrow> r'\<^sup>*\<^sup>* x y
[PROOF STEP]
by (metis mono_rtranclp)


[STATEMENT]
lemma rtranclp_rel_and_invar: "r\<^sup>*\<^sup>* x y \<Longrightarrow> Q x \<Longrightarrow> \<forall>a b. Q a \<and> r a b \<longrightarrow> P a b \<and> Q b \<Longrightarrow> (\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r\<^sup>*\<^sup>* x y; Q x; \<forall>a b. Q a \<and> r a b \<longrightarrow> P a b \<and> Q b\<rbrakk> \<Longrightarrow> (\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply (induct rule: rtranclp_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Q x; \<forall>a b. Q a \<and> r a b \<longrightarrow> P a b \<and> Q b\<rbrakk> \<Longrightarrow> (\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x x
 2. \<And>y z. \<lbrakk>r\<^sup>*\<^sup>* x y; r y z; \<lbrakk>Q x; \<forall>a b. Q a \<and> r a b \<longrightarrow> P a b \<and> Q b\<rbrakk> \<Longrightarrow> (\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x y; Q x; \<forall>a b. Q a \<and> r a b \<longrightarrow> P a b \<and> Q b\<rbrakk> \<Longrightarrow> (\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x z
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>r\<^sup>*\<^sup>* x y; r y z; \<lbrakk>Q x; \<forall>a b. Q a \<and> r a b \<longrightarrow> P a b \<and> Q b\<rbrakk> \<Longrightarrow> (\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x y; Q x; \<forall>a b. Q a \<and> r a b \<longrightarrow> P a b \<and> Q b\<rbrakk> \<Longrightarrow> (\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x z
[PROOF STEP]
apply (metis (no_types, lifting) rtranclp.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rtranclp_invar_conclude_last: "(\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x y \<Longrightarrow> Q x \<Longrightarrow> Q y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x y; Q x\<rbrakk> \<Longrightarrow> Q y
[PROOF STEP]
using rtranclp.cases
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r\<^sup>*\<^sup>* ?a1.0 ?a2.0; \<And>a. \<lbrakk>?a1.0 = a; ?a2.0 = a\<rbrakk> \<Longrightarrow> ?P; \<And>a b c. \<lbrakk>?a1.0 = a; ?a2.0 = c; ?r\<^sup>*\<^sup>* a b; ?r b c\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x y. P x y \<and> Q y)\<^sup>*\<^sup>* x y; Q x\<rbrakk> \<Longrightarrow> Q y
[PROOF STEP]
by fastforce


[STATEMENT]
lemma InvCapsNonneg_imp_InvRecordsNonneg: "InvCapsNonneg c \<Longrightarrow> InvRecordsNonneg c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvCapsNonneg c \<Longrightarrow> InvRecordsNonneg c
[PROOF STEP]
unfolding InvCapsNonneg_def InvRecordsNonneg_def records_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p t. 0 \<le> zcount (c_caps c p) t \<Longrightarrow> \<forall>t. 0 \<le> zcount (sum (c_caps c) UNIV + timestamps (zmset_of (c_data_msg c))) t
[PROOF STEP]
by (auto simp: zcount_sum intro!: sum_nonneg add_nonneg_nonneg)