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

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

goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
show "InvRecordCount c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
unfolding InvRecordCount_def complex_change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>q. records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) = GlobalIncomingInfoAt c0 q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) + c_glob c1 q
[PROOF STEP]
by (auto intro: assms(1)[unfolded InvRecordCount_def, rule_format] simp: change)
[PROOF STATE]
proof (state)
this:
InvRecordCount c1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sendupd_preserves_InvRecordCount:
  assumes "InvRecordCount c0"
    and   "next_sendupd' c0 c1 p tt"
  shows   "InvRecordCount c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvRecordCount c1
[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' q. if p' = p then c_msg c0 p q @ [{#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}] else c_msg c0 p' 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. InvRecordCount c1
[PROOF STEP]
note complex_change = 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. InvRecordCount c1
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
InvRecordCount c0
[PROOF STEP]
show "InvRecordCount c1"
[PROOF STATE]
proof (prove)
using this:
InvRecordCount c0

goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
unfolding InvRecordCount_def complex_change change(5)
[PROOF STATE]
proof (prove)
using this:
\<forall>q. records c0 = GlobalIncomingInfoAt c0 q + c_glob c0 q

goal (1 subgoal):
 1. \<forall>q. records c0 = GlobalIncomingInfoAt c0 q + c_glob c0 q
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
InvRecordCount c1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma recvupd_preserves_InvRecordCount:
  assumes "InvRecordCount c0"
    and   "next_recvupd' c0 c1 p q"
  shows   "InvRecordCount c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvRecordCount c1
[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. InvRecordCount c1
[PROOF STEP]
note complex_change = next_recvupd_complexD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
records c1 = records c0
IncomingInfo c1 0 ?p' ?q' = (if ?p' = p \<and> ?q' = q then IncomingInfo c0 0 ?p' ?q' - hd (c_msg c0 p q) else IncomingInfo c0 0 ?p' ?q')
IncomingInfo c1 ?k ?p' ?q' = (if ?p' = p \<and> ?q' = q then IncomingInfo c0 (?k + 1) ?p' ?q' else IncomingInfo c0 ?k ?p' ?q')
GlobalIncomingInfoAt c1 ?q' = (if ?q' = q then GlobalIncomingInfoAt c0 ?q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 ?q')
InfoAt c1 ?k p q = InfoAt c0 (?k + 1) p q
InfoAt c1 ?k ?p' ?q' = (if ?p' = p \<and> ?q' = q then InfoAt c0 (?k + 1) p q else InfoAt c0 ?k ?p' ?q')

goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
show "InvRecordCount c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
unfolding InvRecordCount_def complex_change change(4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>qa. records c0 = (if qa = q then GlobalIncomingInfoAt c0 qa - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 qa) + ((c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))) qa
[PROOF STEP]
by (auto simp: assms(1)[unfolded InvRecordCount_def, rule_format])
[PROOF STATE]
proof (state)
this:
InvRecordCount c1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma recvcap_preserves_InvRecordCount:
  assumes "InvRecordCount c0"
    and   "next_recvcap' c0 c1 p t"
  shows   "InvRecordCount c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
note change = next_recvcapD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
(p, t) \<in># c_data_msg c0
c_temp c1 = c_temp c0
c_msg c1 = c_msg c0
c_glob c1 = c_glob c0
c_caps c1 = (c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z)
c_data_msg c1 = remove1_mset (p, t) (c_data_msg c0)

goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
note complex_change = next_recvcap_complexD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
records c1 = records c0
IncomingInfo c1 = IncomingInfo c0
GlobalIncomingInfo c1 = GlobalIncomingInfo c0
InfoAt c1 ?k ?p' ?q = InfoAt c0 ?k ?p' ?q

goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
show "InvRecordCount c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvRecordCount c1
[PROOF STEP]
unfolding InvRecordCount_def complex_change change(4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>q. records c0 = GlobalIncomingInfoAt c0 q + c_glob c0 q
[PROOF STEP]
by (auto simp: assms(1)[unfolded InvRecordCount_def, rule_format])
[PROOF STATE]
proof (state)
this:
InvRecordCount c1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_preserves_InvRecordCount: "InvRecordCount c0 \<Longrightarrow> next' c0 c1 \<Longrightarrow> InvRecordCount c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next' c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
unfolding next'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next_performop c0 c1 \<or> next_sendupd c0 c1 \<or> next_recvupd c0 c1 \<or> next_recvcap c0 c1 \<or> c1 = c0\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>InvRecordCount c0; next_performop c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 2. \<lbrakk>InvRecordCount c0; next_sendupd c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 3. \<lbrakk>InvRecordCount c0; next_recvupd c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 4. \<lbrakk>InvRecordCount c0; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 5. \<lbrakk>InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next_performop c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
using performop_preserves_InvRecordCount
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvRecordCount ?c0.0; next_performop' ?c0.0 ?c1.0 ?p ?\<Delta>neg ?\<Delta>mint_msg ?\<Delta>mint_self\<rbrakk> \<Longrightarrow> InvRecordCount ?c1.0

goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next_performop c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>InvRecordCount c0; next_sendupd c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 2. \<lbrakk>InvRecordCount c0; next_recvupd c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 3. \<lbrakk>InvRecordCount c0; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 4. \<lbrakk>InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next_sendupd c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
using sendupd_preserves_InvRecordCount
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvRecordCount ?c0.0; next_sendupd' ?c0.0 ?c1.0 ?p ?tt\<rbrakk> \<Longrightarrow> InvRecordCount ?c1.0

goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next_sendupd c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>InvRecordCount c0; next_recvupd c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 2. \<lbrakk>InvRecordCount c0; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 3. \<lbrakk>InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next_recvupd c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
using recvupd_preserves_InvRecordCount
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvRecordCount ?c0.0; next_recvupd' ?c0.0 ?c1.0 ?p ?q\<rbrakk> \<Longrightarrow> InvRecordCount ?c1.0

goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next_recvupd c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvRecordCount c0; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
 2. \<lbrakk>InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
using recvcap_preserves_InvRecordCount
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvRecordCount ?c0.0; next_recvcap' ?c0.0 ?c1.0 ?p ?t\<rbrakk> \<Longrightarrow> InvRecordCount ?c1.0

goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvRecordCount c0; c1 = c0\<rbrakk> \<Longrightarrow> InvRecordCount c1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma alw_InvRecordCount: "spec s \<Longrightarrow> alw (holds InvRecordCount) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvRecordCount) s
[PROOF STEP]
using lift_invariant_to_spec init_config_implies_InvRecordCount next_preserves_InvRecordCount
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>c. init_config c \<Longrightarrow> ?P c; \<And>s. \<lbrakk>holds ?P s; next s\<rbrakk> \<Longrightarrow> nxt (holds ?P) s; spec ?s\<rbrakk> \<Longrightarrow> alw (holds ?P) ?s
init_config ?c \<Longrightarrow> InvRecordCount ?c
\<lbrakk>InvRecordCount ?c0.0; next' ?c0.0 ?c1.0\<rbrakk> \<Longrightarrow> InvRecordCount ?c1.0

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvRecordCount) s
[PROOF STEP]
by (metis (mono_tags, lifting) holds.elims(2) holds.elims(3) nxt.simps)


[STATEMENT]
lemma init_config_implies_InvCapsNonneg: "init_config c \<Longrightarrow> InvCapsNonneg c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init_config c \<Longrightarrow> InvCapsNonneg c
[PROOF STEP]
unfolding init_config_def InvCapsNonneg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p. c_temp c p = {#}\<^sub>z) \<and> (\<forall>p1 p2. c_msg c p1 p2 = []) \<and> (\<forall>p t. 0 \<le> zcount (c_caps c p) t) \<and> (\<forall>p. c_glob c p = records c) \<and> c_data_msg c = {#} \<Longrightarrow> \<forall>p t. 0 \<le> zcount (c_caps c p) t
[PROOF STEP]
by simp


[STATEMENT]
lemma performop_preserves_InvCapsNonneg:
  assumes "InvCapsNonneg c0"
    and   "next_performop' c0 c1 p \<Delta>\<^sub>m \<Delta>\<^sub>p\<^sub>1 \<Delta>\<^sub>p\<^sub>2"
  shows   "InvCapsNonneg c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvCapsNonneg c1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvCapsNonneg c0
next_performop' c0 c1 p \<Delta>\<^sub>m \<Delta>\<^sub>p\<^sub>1 \<Delta>\<^sub>p\<^sub>2

goal (1 subgoal):
 1. InvCapsNonneg c1
[PROOF STEP]
unfolding InvCapsNonneg_def next_performop'_def Let_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p t. 0 \<le> zcount (c_caps c0 p) t
(\<Delta>\<^sub>p\<^sub>1 \<noteq> {#} \<or> zmset_of \<Delta>\<^sub>p\<^sub>2 - zmset_of \<Delta>\<^sub>m \<noteq> {#}\<^sub>z) \<and> (\<forall>t. int (count \<Delta>\<^sub>m t) \<le> zcount (c_caps c0 p) t) \<and> minting_self (c_caps c0 p) \<Delta>\<^sub>p\<^sub>2 \<and> minting_msg (c_caps c0 p) \<Delta>\<^sub>p\<^sub>1 \<and> c1 = c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>\<^sub>p\<^sub>2 - zmset_of \<Delta>\<^sub>m), c_data_msg := c_data_msg c0 + \<Delta>\<^sub>p\<^sub>1, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>\<^sub>p\<^sub>1) + zmset_of \<Delta>\<^sub>p\<^sub>2 - zmset_of \<Delta>\<^sub>m))\<rparr>

goal (1 subgoal):
 1. \<forall>p t. 0 \<le> zcount (c_caps c1 p) t
[PROOF STEP]
by clarsimp (metis add.right_neutral add_mono_thms_linordered_semiring(1) of_nat_0_le_iff)


[STATEMENT]
lemma sendupd_performs_InvCapsNonneg:
  assumes "InvCapsNonneg c0"
    and   "next_sendupd' c0 c1 p tt"
  shows   "InvCapsNonneg c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvCapsNonneg c1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvCapsNonneg c0
next_sendupd' c0 c1 p tt

goal (1 subgoal):
 1. InvCapsNonneg c1
[PROOF STEP]
by (simp add: InvCapsNonneg_def next_sendupd'_def Let_def)


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

goal (1 subgoal):
 1. InvCapsNonneg c1
[PROOF STEP]
unfolding InvCapsNonneg_def next_recvupd'_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p t. 0 \<le> zcount (c_caps c0 p) t
c_msg c0 p q \<noteq> [] \<and> c1 = c0\<lparr>c_msg := (c_msg c0)(p := (c_msg c0 p)(q := tl (c_msg c0 p q))), c_glob := (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))\<rparr>

goal (1 subgoal):
 1. \<forall>p t. 0 \<le> zcount (c_caps c1 p) t
[PROOF STEP]
by simp


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

goal (1 subgoal):
 1. InvCapsNonneg c1
[PROOF STEP]
unfolding InvCapsNonneg_def next_recvcap'_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p t. 0 \<le> zcount (c_caps c0 p) t
(p, t) \<in># c_data_msg c0 \<and> c1 = c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z), c_data_msg := remove1_mset (p, t) (c_data_msg c0)\<rparr>

goal (1 subgoal):
 1. \<forall>p t. 0 \<le> zcount (c_caps c1 p) t
[PROOF STEP]
by simp


[STATEMENT]
lemma next_preserves_InvCapsNonneg: "holds InvCapsNonneg s \<Longrightarrow> next s \<Longrightarrow> nxt (holds InvCapsNonneg) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next s\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
unfolding next'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>holds InvCapsNonneg s; next_performop (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 2. \<lbrakk>holds InvCapsNonneg s; next_sendupd (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 3. \<lbrakk>holds InvCapsNonneg s; next_recvupd (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 4. \<lbrakk>holds InvCapsNonneg s; next_recvcap (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 5. \<lbrakk>holds InvCapsNonneg s; shd (stl s) = shd s\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next_performop (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
using performop_preserves_InvCapsNonneg
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvCapsNonneg ?c0.0; next_performop' ?c0.0 ?c1.0 ?p ?\<Delta>\<^sub>m ?\<Delta>\<^sub>p\<^sub>1 ?\<Delta>\<^sub>p\<^sub>2\<rbrakk> \<Longrightarrow> InvCapsNonneg ?c1.0

goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next_performop (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>holds InvCapsNonneg s; next_sendupd (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 2. \<lbrakk>holds InvCapsNonneg s; next_recvupd (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 3. \<lbrakk>holds InvCapsNonneg s; next_recvcap (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 4. \<lbrakk>holds InvCapsNonneg s; shd (stl s) = shd s\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next_sendupd (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
using sendupd_performs_InvCapsNonneg
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvCapsNonneg ?c0.0; next_sendupd' ?c0.0 ?c1.0 ?p ?tt\<rbrakk> \<Longrightarrow> InvCapsNonneg ?c1.0

goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next_sendupd (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>holds InvCapsNonneg s; next_recvupd (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 2. \<lbrakk>holds InvCapsNonneg s; next_recvcap (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 3. \<lbrakk>holds InvCapsNonneg s; shd (stl s) = shd s\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next_recvupd (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
using recvupd_preserves_InvCapsNonneg
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvCapsNonneg ?c0.0; next_recvupd' ?c0.0 ?c1.0 ?p ?q\<rbrakk> \<Longrightarrow> InvCapsNonneg ?c1.0

goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next_recvupd (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>holds InvCapsNonneg s; next_recvcap (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
 2. \<lbrakk>holds InvCapsNonneg s; shd (stl s) = shd s\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next_recvcap (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
using recvcap_preserves_InvCapsNonneg
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvCapsNonneg ?c0.0; next_recvcap' ?c0.0 ?c1.0 ?p ?t\<rbrakk> \<Longrightarrow> InvCapsNonneg ?c1.0

goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; next_recvcap (shd s) (shd (stl s))\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; shd (stl s) = shd s\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds InvCapsNonneg s; shd (stl s) = shd s\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) s
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma alw_InvCapsNonneg: "spec s \<Longrightarrow> alw (holds InvCapsNonneg) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvCapsNonneg) s
[PROOF STEP]
using lift_invariant_to_spec next_preserves_InvCapsNonneg init_config_implies_InvCapsNonneg
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>c. init_config c \<Longrightarrow> ?P c; \<And>s. \<lbrakk>holds ?P s; next s\<rbrakk> \<Longrightarrow> nxt (holds ?P) s; spec ?s\<rbrakk> \<Longrightarrow> alw (holds ?P) ?s
\<lbrakk>holds InvCapsNonneg ?s; next ?s\<rbrakk> \<Longrightarrow> nxt (holds InvCapsNonneg) ?s
init_config ?c \<Longrightarrow> InvCapsNonneg ?c

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvCapsNonneg) s
[PROOF STEP]
by blast


[STATEMENT]
lemma alw_InvRecordsNonneg: "spec s \<Longrightarrow> alw (holds InvRecordsNonneg) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvRecordsNonneg) s
[PROOF STEP]
apply (rule alw_mp[where \<phi> = "holds InvCapsNonneg"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. spec s \<Longrightarrow> alw (holds InvCapsNonneg) s
 2. spec s \<Longrightarrow> alw (\<lambda>xs. holds InvCapsNonneg xs \<longrightarrow> holds InvRecordsNonneg xs) s
[PROOF STEP]
using alw_InvCapsNonneg
[PROOF STATE]
proof (prove)
using this:
spec ?s \<Longrightarrow> alw (holds InvCapsNonneg) ?s

goal (2 subgoals):
 1. spec s \<Longrightarrow> alw (holds InvCapsNonneg) s
 2. spec s \<Longrightarrow> alw (\<lambda>xs. holds InvCapsNonneg xs \<longrightarrow> holds InvRecordsNonneg xs) s
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (\<lambda>xs. holds InvCapsNonneg xs \<longrightarrow> holds InvRecordsNonneg xs) s
[PROOF STEP]
apply (rule all_imp_alw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. spec s \<Longrightarrow> holds InvCapsNonneg xs \<longrightarrow> holds InvRecordsNonneg xs
[PROOF STEP]
unfolding InvCapsNonneg_def InvRecordsNonneg_def records_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. spec s \<Longrightarrow> holds (\<lambda>c. \<forall>p t. 0 \<le> zcount (c_caps c p) t) xs \<longrightarrow> holds (\<lambda>c. \<forall>t. 0 \<le> zcount (sum (c_caps c) UNIV + timestamps (zmset_of (c_data_msg c))) t) xs
[PROOF STEP]
apply (auto intro!: add_nonneg_nonneg sum_nonneg simp: zcount_sum)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pos_caps_pos_records:
  assumes "InvCapsNonneg c"
  shows "0 < zcount (c_caps c p) x \<Longrightarrow> 0 < zcount (records c) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (c_caps c p) x \<Longrightarrow> 0 < zcount (records c) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < zcount (c_caps c p) x \<Longrightarrow> 0 < zcount (records c) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < zcount (c_caps c p) x \<Longrightarrow> 0 < zcount (records c) x
[PROOF STEP]
assume "0 < zcount (c_caps c p) x"
[PROOF STATE]
proof (state)
this:
0 < zcount (c_caps c p) x

goal (1 subgoal):
 1. 0 < zcount (c_caps c p) x \<Longrightarrow> 0 < zcount (records c) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (c_caps c p) x
[PROOF STEP]
have "0 < zcount (\<Sum>p\<in>UNIV. c_caps c p) x"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_caps c p) x

goal (1 subgoal):
 1. 0 < zcount (sum (c_caps c) UNIV) x
[PROOF STEP]
using assms(1)[unfolded InvCapsNonneg_def]
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_caps c p) x
\<forall>p t. 0 \<le> zcount (c_caps c p) t

goal (1 subgoal):
 1. 0 < zcount (sum (c_caps c) UNIV) x
[PROOF STEP]
by (auto intro!: sum_pos2 simp: zcount_sum)
[PROOF STATE]
proof (state)
this:
0 < zcount (sum (c_caps c) UNIV) x

goal (1 subgoal):
 1. 0 < zcount (c_caps c p) x \<Longrightarrow> 0 < zcount (records c) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (sum (c_caps c) UNIV) x
[PROOF STEP]
show "0 < zcount (records c) x"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (sum (c_caps c) UNIV) x

goal (1 subgoal):
 1. 0 < zcount (records c) x
[PROOF STEP]
unfolding records_def
[PROOF STATE]
proof (prove)
using this:
0 < zcount (sum (c_caps c) UNIV) x

goal (1 subgoal):
 1. 0 < zcount (sum (c_caps c) UNIV + timestamps (zmset_of (c_data_msg c))) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < zcount (records c) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma performop_preserves_RecordsVacantUpto:
  assumes "RecordsVacantUpto c0 t"
    and   "next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self"
    and   "InvRecordsNonneg c1"
    and   "InvCapsNonneg c0"
  shows   "RecordsVacantUpto c1 t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
note InvRecordsNonneg = assms(3)[rule_format]
[PROOF STATE]
proof (state)
this:
InvRecordsNonneg c1

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
InvRecordsNonneg c1

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
let ?\<Delta>pos = "timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
let ?\<Delta> = "?\<Delta>pos - zmset_of \<Delta>neg"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
note change = next_performopD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
\<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z
\<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t
minting_self (c_caps c0 p) \<Delta>mint_self
minting_msg (c_caps c0 p) \<Delta>mint_msg
c_temp c1 = (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
c_msg c1 = c_msg c0
c_glob c1 = c_glob c0
c_data_msg c1 = c_data_msg c0 + \<Delta>mint_msg
c_caps c1 = (c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))

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

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
assume s: "s \<le> t" "zcount (records c1) s \<noteq> 0"
[PROOF STATE]
proof (state)
this:
s \<le> t
zcount (records c1) s \<noteq> 0

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<le> t
zcount (records c1) s \<noteq> 0
[PROOF STEP]
have s_pos: "0 < zcount (records c1) s"
[PROOF STATE]
proof (prove)
using this:
s \<le> t
zcount (records c1) s \<noteq> 0

goal (1 subgoal):
 1. 0 < zcount (records c1) s
[PROOF STEP]
using InvRecordsNonneg
[PROOF STATE]
proof (prove)
using this:
s \<le> t
zcount (records c1) s \<noteq> 0
InvRecordsNonneg c1

goal (1 subgoal):
 1. 0 < zcount (records c1) s
[PROOF STEP]
by (simp add: order_class.order.not_eq_order_implies_strict InvRecordsNonneg_def)
[PROOF STATE]
proof (state)
this:
0 < zcount (records c1) s

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
have \<Delta>_in_nrec: "0 < zcount ?\<Delta> t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply (subst (asm) zcount_diff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) t - zcount (zmset_of \<Delta>neg) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply (subst (asm) zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t + zcount (zmset_of \<Delta>mint_self) t - zcount (zmset_of \<Delta>neg) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply (drule zero_lt_diff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> zcount (zmset_of \<Delta>neg) t
 2. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t + zcount (zmset_of \<Delta>mint_self) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t + zcount (zmset_of \<Delta>mint_self) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply (drule zero_lt_add_disj)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 \<le> zcount (timestamps (zmset_of \<Delta>mint_msg)) t
 2. 0 \<le> zcount (zmset_of \<Delta>mint_self) t
 3. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t \<or> 0 < zcount (zmset_of \<Delta>mint_self) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> zcount (zmset_of \<Delta>mint_self) t
 2. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t \<or> 0 < zcount (zmset_of \<Delta>mint_self) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t \<or> 0 < zcount (zmset_of \<Delta>mint_self) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
 2. 0 < zcount (zmset_of \<Delta>mint_self) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg)) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply (drule pos_image_zmset_obtain_pre[rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. 0 \<le> zcount (zmset_of \<Delta>mint_msg) t
 2. \<exists>m. 0 < zcount (zmset_of \<Delta>mint_msg) m \<and> (case m of (x, t) \<Rightarrow> t) = t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
apply (auto dest!: change(4)[unfolded minting_msg_def, rule_format] pos_caps_pos_records[OF assms(4)] less_imp_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (zmset_of \<Delta>mint_self) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (zmset_of \<Delta>mint_self) t \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (records c0) t'
[PROOF STEP]
by (auto dest!: change(3)[unfolded minting_self_def, rule_format] pos_caps_pos_records[OF assms(4)])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) ?t \<Longrightarrow> \<exists>t'\<le>?t. 0 < zcount (records c0) t'

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
have nrec0s: "zcount (records c0) s = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (records c0) s = 0
[PROOF STEP]
by (rule assms(1)[unfolded vacant_upto_def, rule_format, OF s(1)])
[PROOF STATE]
proof (state)
this:
zcount (records c0) s = 0

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
have "zcount (records c1) s \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (records c1) s \<le> 0
[PROOF STEP]
unfolding complex_change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) s \<le> 0
[PROOF STEP]
apply (subst zcount_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (records c0) s + zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) s \<le> 0
[PROOF STEP]
apply (subst nrec0s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) s \<le> 0
[PROOF STEP]
apply (subst add_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) s \<le> 0
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) s \<le> 0 \<Longrightarrow> False
[PROOF STEP]
unfolding not_le
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) s \<Longrightarrow> False
[PROOF STEP]
apply (drule \<Delta>_in_nrec[of s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'\<le>s. 0 < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
apply (meson assms(1) order_trans pos_zcount_in_zmset s(1) vacant_upto_def zcount_ne_zero_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
zcount (records c1) s \<le> 0

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
with s_pos
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (records c1) s
zcount (records c1) s \<le> 0
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
0 < zcount (records c1) s
zcount (records c1) s \<le> 0

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

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s2 \<le> t; zcount (records c1) ?s2 \<noteq> 0\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
note r = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s2 \<le> t; zcount (records c1) ?s2 \<noteq> 0\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
RecordsVacantUpto c0 t
next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self
InvRecordsNonneg c1
InvCapsNonneg c0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
RecordsVacantUpto c0 t
next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self
InvRecordsNonneg c1
InvCapsNonneg c0

goal (1 subgoal):
 1. RecordsVacantUpto c1 t
[PROOF STEP]
unfolding next_performop'_def Let_def vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<le>t. zcount (records c0) s = 0
(\<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z) \<and> (\<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t) \<and> minting_self (c_caps c0 p) \<Delta>mint_self \<and> minting_msg (c_caps c0 p) \<Delta>mint_msg \<and> c1 = c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>
InvRecordsNonneg c1
InvCapsNonneg c0

goal (1 subgoal):
 1. \<forall>s\<le>t. zcount (records c1) s = 0
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s\<le>t. zcount (records c0) s = 0; InvRecordsNonneg (c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>); InvCapsNonneg c0; \<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z; \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t; minting_self (c_caps c0 p) \<Delta>mint_self; minting_msg (c_caps c0 p) \<Delta>mint_msg; c1 = c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>; s \<le> t\<rbrakk> \<Longrightarrow> zcount (records (c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>)) s = 0
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s\<le>t. zcount (records c0) s = 0; InvRecordsNonneg (c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>); InvCapsNonneg c0; \<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z; \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t; minting_self (c_caps c0 p) \<Delta>mint_self; minting_msg (c_caps c0 p) \<Delta>mint_msg; c1 = c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>; s \<le> t; zcount (records (c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>)) s \<noteq> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rule r)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s\<le>t. zcount (records c0) s = 0; InvRecordsNonneg (c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>); InvCapsNonneg c0; \<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z; \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t; minting_self (c_caps c0 p) \<Delta>mint_self; minting_msg (c_caps c0 p) \<Delta>mint_msg; c1 = c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>; s \<le> t; zcount (records (c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>)) s \<noteq> 0\<rbrakk> \<Longrightarrow> ?s16 s \<le> t
 2. \<And>s. \<lbrakk>\<forall>s\<le>t. zcount (records c0) s = 0; InvRecordsNonneg (c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>); InvCapsNonneg c0; \<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z; \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t; minting_self (c_caps c0 p) \<Delta>mint_self; minting_msg (c_caps c0 p) \<Delta>mint_msg; c1 = c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>; s \<le> t; zcount (records (c0\<lparr>c_caps := (c_caps c0)(p := c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg), c_data_msg := c_data_msg c0 + \<Delta>mint_msg, c_temp := (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))\<rparr>)) s \<noteq> 0\<rbrakk> \<Longrightarrow> zcount (records c1) (?s16 s) \<noteq> 0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
RecordsVacantUpto c1 t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next'_preserves_RecordsVacantUpto:
  fixes c0 :: "('p::finite, 'a) configuration"
  shows "InvCapsNonneg c0 \<Longrightarrow> InvRecordsNonneg c1 \<Longrightarrow> RecordsVacantUpto c0 t \<Longrightarrow> next' c0 c1 \<Longrightarrow> RecordsVacantUpto c1 t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next' c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
unfolding next'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_performop c0 c1 \<or> next_sendupd c0 c1 \<or> next_recvupd c0 c1 \<or> next_recvcap c0 c1 \<or> c1 = c0\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_performop c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 2. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_sendupd c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 3. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_recvupd c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 4. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 5. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; c1 = c0\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_performop c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
by (auto intro: performop_preserves_RecordsVacantUpto)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_sendupd c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 2. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_recvupd c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 3. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 4. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; c1 = c0\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_sendupd c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
by (auto simp: next_sendupd'_def Let_def records_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_recvupd c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 2. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 3. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; c1 = c0\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_recvupd c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
by (auto simp: next_recvupd'_def records_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
 2. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; c1 = c0\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; next_recvcap c0 c1\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
by (auto dest: next_recvcap_complexD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; c1 = c0\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvRecordsNonneg c1; RecordsVacantUpto c0 t; c1 = c0\<rbrakk> \<Longrightarrow> RecordsVacantUpto c1 t
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma alw_next_implies_alw_SafeRecordsMono:
  "alw next s \<Longrightarrow> alw (holds InvCapsNonneg) s \<Longrightarrow> alw (holds InvRecordsNonneg) s \<Longrightarrow> alw SafeRecordsMono s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw next s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s\<rbrakk> \<Longrightarrow> alw SafeRecordsMono s
[PROOF STEP]
apply (coinduction arbitrary: s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw next s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> SafeRecordsMono xs \<and> ((\<exists>s. stl xs = s \<and> alw next s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvRecordsNonneg) s) \<or> alw SafeRecordsMono (stl xs))
[PROOF STEP]
subgoal for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw next s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> SafeRecordsMono xs \<and> ((\<exists>s. stl xs = s \<and> alw next s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvRecordsNonneg) s) \<or> alw SafeRecordsMono (stl xs))
[PROOF STEP]
unfolding spec_def next'_def SafeRecordsMono_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> (\<forall>t. RecordsVacantUpto (shd xs) t \<longrightarrow> alw (holds (\<lambda>c. RecordsVacantUpto c t)) xs) \<and> ((\<exists>s. stl xs = s \<and> alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvRecordsNonneg) s) \<or> alw (\<lambda>s. \<forall>t. RecordsVacantUpto (shd s) t \<longrightarrow> alw (holds (\<lambda>c. RecordsVacantUpto c t)) s) (stl xs))
[PROOF STEP]
apply (rule exI[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s\<rbrakk> \<Longrightarrow> s = s \<and> (\<forall>t. RecordsVacantUpto (shd s) t \<longrightarrow> alw (holds (\<lambda>c. RecordsVacantUpto c t)) s) \<and> ((\<exists>s. stl s = s \<and> alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvRecordsNonneg) s) \<or> alw (\<lambda>s. \<forall>t. RecordsVacantUpto (shd s) t \<longrightarrow> alw (holds (\<lambda>c. RecordsVacantUpto c t)) s) (stl s))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; RecordsVacantUpto (shd s) t\<rbrakk> \<Longrightarrow> alw (holds (\<lambda>c. RecordsVacantUpto c t)) s
 2. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; \<not> alw (\<lambda>s. \<forall>t. RecordsVacantUpto (shd s) t \<longrightarrow> alw (holds (\<lambda>c. RecordsVacantUpto c t)) s) (stl s)\<rbrakk> \<Longrightarrow> \<exists>s. stl s = s \<and> alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvRecordsNonneg) s
[PROOF STEP]
subgoal for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; RecordsVacantUpto (shd s) t\<rbrakk> \<Longrightarrow> alw (holds (\<lambda>c. RecordsVacantUpto c t)) s
[PROOF STEP]
apply (coinduction arbitrary: s rule: alw.coinduct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; RecordsVacantUpto (shd s) t\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> holds (\<lambda>c. RecordsVacantUpto c t) xs \<and> ((\<exists>s. stl xs = s \<and> alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvRecordsNonneg) s \<and> RecordsVacantUpto (shd s) t) \<or> alw (holds (\<lambda>c. RecordsVacantUpto c t)) (stl xs))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; RecordsVacantUpto (shd s) t; \<not> alw (holds (\<lambda>c. RecordsVacantUpto c t)) (stl s)\<rbrakk> \<Longrightarrow> alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) (stl s) \<and> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvRecordsNonneg) (stl s) \<and> RecordsVacantUpto (shd (stl s)) t
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; RecordsVacantUpto (shd s) t; \<not> alw (holds (\<lambda>c. RecordsVacantUpto c t)) (stl s)\<rbrakk> \<Longrightarrow> alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) (stl s)
 2. \<And>s. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; RecordsVacantUpto (shd s) t; \<not> alw (holds (\<lambda>c. RecordsVacantUpto c t)) (stl s)\<rbrakk> \<Longrightarrow> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvRecordsNonneg) (stl s) \<and> RecordsVacantUpto (shd (stl s)) t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; RecordsVacantUpto (shd s) t; \<not> alw (holds (\<lambda>c. RecordsVacantUpto c t)) (stl s)\<rbrakk> \<Longrightarrow> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvRecordsNonneg) (stl s) \<and> RecordsVacantUpto (shd (stl s)) t
[PROOF STEP]
apply (erule alw.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s xs. \<lbrakk>alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; RecordsVacantUpto (shd s) t; \<not> alw (holds (\<lambda>c. RecordsVacantUpto c t)) (stl s); s = xs; next_performop (shd xs) (shd (stl xs)) \<or> next_sendupd (shd xs) (shd (stl xs)) \<or> next_recvupd (shd xs) (shd (stl xs)) \<or> next_recvcap (shd xs) (shd (stl xs)) \<or> shd (stl xs) = shd xs; alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) (stl xs)\<rbrakk> \<Longrightarrow> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvRecordsNonneg) (stl s) \<and> RecordsVacantUpto (shd (stl s)) t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>alw (holds InvCapsNonneg) xs; alw (holds InvRecordsNonneg) xs; RecordsVacantUpto (shd xs) t; \<not> alw (holds (\<lambda>c. RecordsVacantUpto c t)) (stl xs); next_performop (shd xs) (shd (stl xs)) \<or> next_sendupd (shd xs) (shd (stl xs)) \<or> next_recvupd (shd xs) (shd (stl xs)) \<or> next_recvcap (shd xs) (shd (stl xs)) \<or> shd (stl xs) = shd xs; alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) (stl xs)\<rbrakk> \<Longrightarrow> alw (holds InvCapsNonneg) (stl xs) \<and> alw (holds InvRecordsNonneg) (stl xs) \<and> RecordsVacantUpto (shd (stl xs)) t
[PROOF STEP]
apply (metis (no_types, lifting) next'_def next'_preserves_RecordsVacantUpto alw_holds2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s; alw (holds InvCapsNonneg) s; alw (holds InvRecordsNonneg) s; \<not> alw (\<lambda>s. \<forall>t. RecordsVacantUpto (shd s) t \<longrightarrow> alw (holds (\<lambda>c. RecordsVacantUpto c t)) s) (stl s)\<rbrakk> \<Longrightarrow> \<exists>s. stl s = s \<and> alw (\<lambda>s. next_performop (shd s) (shd (stl s)) \<or> next_sendupd (shd s) (shd (stl s)) \<or> next_recvupd (shd s) (shd (stl s)) \<or> next_recvcap (shd s) (shd (stl s)) \<or> shd (stl s) = shd s) s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvRecordsNonneg) s
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma alw_SafeRecordsMono: "spec s \<Longrightarrow> alw SafeRecordsMono s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw SafeRecordsMono s
[PROOF STEP]
by (auto intro!: alw_next_implies_alw_SafeRecordsMono alw_InvRecordsNonneg alw_InvCapsNonneg simp: spec_def)