[STATEMENT]
lemma InvJustifiedII_implies_InvJustifiedGII:
  assumes "InvJustifiedII c"
    and   "InvCapsNonneg c"
  shows   "InvJustifiedGII c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvJustifiedGII c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvJustifiedII c
InvCapsNonneg c

goal (1 subgoal):
 1. InvJustifiedGII c
[PROOF STEP]
unfolding
    InvJustifiedGII_def
    InvJustifiedII_def
    GlobalIncomingInfo_def
    records_def
    InvCapsNonneg_def
[PROOF STATE]
proof (prove)
using this:
\<forall>k p q. justified (c_caps c p) (IncomingInfo c k p q)
\<forall>p t. 0 \<le> zcount (c_caps c p) t

goal (1 subgoal):
 1. \<forall>k p q. justified (sum (c_caps c) UNIV + timestamps (zmset_of (c_data_msg c))) (\<Sum>p'\<in>UNIV. IncomingInfo c (if p' = p then k else 0) p' q)
[PROOF STEP]
by (auto intro!: justified_add_records justified_sum)


[STATEMENT]
lemma init_config_implies_InvJustifiedII: "init_config c \<Longrightarrow> InvJustifiedII c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init_config c \<Longrightarrow> InvJustifiedII c
[PROOF STEP]
by (simp add: init_config_def InvJustifiedII_def justified_alt IncomingInfo_def)


[STATEMENT]
lemma performop_preserves_InvJustifiedII:
  assumes "InvJustifiedII c0"
    and   "next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self"
    and   "InvCapsNonneg c0"
  shows   "InvJustifiedII c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvJustifiedII c1
[PROOF STEP]
unfolding InvJustifiedII_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k p q. justified (c_caps c1 p) (IncomingInfo c1 k p q)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k p q. justified (c_caps c1 p) (IncomingInfo c1 k p q)
[PROOF STEP]
subgoal for k p' q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified (c_caps c1 p') (IncomingInfo c1 k p' q)
[PROOF STEP]
apply (cases "p'=p")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p' = p \<Longrightarrow> justified (c_caps c1 p') (IncomingInfo c1 k p' q)
 2. p' \<noteq> p \<Longrightarrow> justified (c_caps c1 p') (IncomingInfo c1 k p' q)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified (c_caps c1 p') (IncomingInfo c1 k p' q)
[PROOF STEP]
unfolding next_performop_complexD[OF assms(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified (c_caps c1 p') (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)
[PROOF STEP]
apply (simp only: if_P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified (c_caps c1 p) (IncomingInfo c0 k p q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
apply (rule next_performop'_preserves_justified[
            OF assms(1)[unfolded InvJustifiedII_def, rule_format, of p k q],
            OF assms(2,3)])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified (c_caps c1 p') (IncomingInfo c1 k p' q)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified (c_caps c1 p') (IncomingInfo c1 k p' q)
[PROOF STEP]
unfolding
        next_performopD[OF assms(2)]
        next_performop_complexD[OF assms(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified (((c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p') (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)
[PROOF STEP]
using assms(1)[unfolded InvJustifiedII_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>k p q. justified (c_caps c0 p) (IncomingInfo c0 k p q)

goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified (((c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p') (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)
[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 sendupd_preserves_InvJustifiedII:
  assumes "InvJustifiedII c0"
    and   "next_sendupd' c0 c1 p tt"
  shows   "InvJustifiedII c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvJustifiedII c1
[PROOF STEP]
unfolding InvJustifiedII_def justified_alt supported_strong_def next_sendupdD(6)[OF assms(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k p q t. 0 < zcount (IncomingInfo c1 k p q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p) t') \<or> zcount (IncomingInfo c1 k p q) t < zcount (c_caps c0 p) t
[PROOF STEP]
apply (intro allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k p q t. 0 < zcount (IncomingInfo c1 k p q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p) t') \<or> zcount (IncomingInfo c1 k p q) t < zcount (c_caps c0 p) t
[PROOF STEP]
subgoal for k p' q t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (IncomingInfo c1 k p' q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p' q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p' q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c1 k p' q) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (cases "k \<le> length (c_msg c0 p q)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. k \<le> length (c_msg c0 p q) \<Longrightarrow> 0 < zcount (IncomingInfo c1 k p' q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p' q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p' q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c1 k p' q) t < zcount (c_caps c0 p') t
 2. \<not> k \<le> length (c_msg c0 p q) \<Longrightarrow> 0 < zcount (IncomingInfo c1 k p' q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p' q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p' q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c1 k p' q) t < zcount (c_caps c0 p') t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> length (c_msg c0 p q) \<Longrightarrow> 0 < zcount (IncomingInfo c1 k p' q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p' q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p' q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c1 k p' q) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (drule next_sendupd_complexD(4)[OF assms(2), of _ _ p'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IncomingInfo c1 k p' q = IncomingInfo c0 k p' q \<Longrightarrow> 0 < zcount (IncomingInfo c1 k p' q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p' q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p' q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c1 k p' q) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (auto dest: assms(1)[unfolded InvJustifiedII_def justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> k \<le> length (c_msg c0 p q) \<Longrightarrow> 0 < zcount (IncomingInfo c1 k p' q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p' q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p' q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c1 k p' q) t < zcount (c_caps c0 p') t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> k \<le> length (c_msg c0 p q) \<Longrightarrow> 0 < zcount (IncomingInfo c1 k p' q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p' q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p' q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c1 k p' q) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (subst (asm) not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (c_msg c0 p q) < k \<Longrightarrow> 0 < zcount (IncomingInfo c1 k p' q) t \<longrightarrow> (\<exists>s<t. zcount (IncomingInfo c1 k p' q) s < 0 \<and> nonpos_upto (IncomingInfo c1 k p' q) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c1 k p' q) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (subst (1 2 3 4) next_sendupd_complexD(5)[OF assms(2), of _ _ p'])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. length (c_msg c0 p q) < k \<Longrightarrow> length (c_msg c0 p q) < k
 2. \<And>s. length (c_msg c0 p q) < k \<Longrightarrow> length (c_msg c0 p q) < k
 3. length (c_msg c0 p q) < k \<Longrightarrow> 0 < zcount (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) t \<longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. length (c_msg c0 p q) < k \<Longrightarrow> length (c_msg c0 p q) < k
 2. length (c_msg c0 p q) < k \<Longrightarrow> 0 < zcount (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) t \<longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (c_msg c0 p q) < k \<Longrightarrow> 0 < zcount (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) t \<longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (cases "p'=p")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p\<rbrakk> \<Longrightarrow> 0 < zcount (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) t \<longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
 2. \<lbrakk>length (c_msg c0 p q) < k; p' \<noteq> p\<rbrakk> \<Longrightarrow> 0 < zcount (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) t \<longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p\<rbrakk> \<Longrightarrow> 0 < zcount (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) t \<longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (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) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (subst (asm) if_P)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p\<rbrakk> \<Longrightarrow> p' = p
 2. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (subst (1 2 3) if_P)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> p' = p
 2. \<And>s. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> p' = p
 3. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s < 0 \<and> nonpos_upto (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> p' = p
 2. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s < 0 \<and> nonpos_upto (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s < 0 \<and> nonpos_upto (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t < zcount (c_caps c0 p') t
[PROOF STEP]
unfolding IncomingInfo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s < 0 \<and> nonpos_upto (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (subst (asm) drop_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p\<rbrakk> \<Longrightarrow> length (c_msg c0 p' q) \<le> k
 2. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (sum_list [] + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s < 0 \<and> nonpos_upto (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (sum_list [] + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s < 0 \<and> nonpos_upto (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (subst drop_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (sum_list [] + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> length (c_msg c0 p' q) \<le> k
 2. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (sum_list [] + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (sum_list [] + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s < 0 \<and> nonpos_upto (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (sum_list [] + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (sum_list [] + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s < 0 \<and> nonpos_upto (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}) t < zcount (c_caps c0 p') t
[PROOF STEP]
apply (simp del: zcount_diff)
          \<comment> \<open>The justified condition ensures that anything remaining in temp satisfies this invariant\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p; 0 < zcount (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) s < 0 \<and> nonpos_upto (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p) t') \<or> zcount (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) t < zcount (c_caps c0 p) t
[PROOF STEP]
apply (drule next_sendupdD(2)[OF assms(2), unfolded justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' = p; (\<exists>s<t. zcount (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) s < 0 \<and> nonpos_upto (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p) t') \<or> zcount (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) t < zcount (c_caps c0 p) t\<rbrakk> \<Longrightarrow> (\<exists>s<t. zcount (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) s < 0 \<and> nonpos_upto (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p) t') \<or> zcount (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) t < zcount (c_caps c0 p) t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' \<noteq> p\<rbrakk> \<Longrightarrow> 0 < zcount (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) t \<longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (c_msg c0 p q) < k; p' \<noteq> p\<rbrakk> \<Longrightarrow> 0 < zcount (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) t \<longrightarrow> (\<exists>s<t. zcount (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) s < 0 \<and> nonpos_upto (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) s) \<or> (\<exists>t'<t. 0 < zcount (c_caps c0 p') t') \<or> zcount (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) t < zcount (c_caps c0 p') t
[PROOF STEP]
by (auto intro!: assms(1)[unfolded InvJustifiedII_def justified_alt supported_strong_def, rule_format])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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

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

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


[STATEMENT]
lemma recvcap_preserves_InvJustifiedII:
  assumes "InvJustifiedII c0"
    and   "next_recvcap' c0 c1 p t"
  shows   "InvJustifiedII c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvJustifiedII c1
[PROOF STEP]
unfolding InvJustifiedII_def justified_alt supported_strong_def next_recvcap_complexD[OF assms(2)] next_recvcapD(5)[OF assms(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k pa q ta. 0 < zcount (IncomingInfo c0 k pa q) ta \<longrightarrow> (\<exists>s<ta. zcount (IncomingInfo c0 k pa q) s < 0 \<and> nonpos_upto (IncomingInfo c0 k pa q) s) \<or> (\<exists>t'<ta. 0 < zcount (((c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z)) pa) t') \<or> zcount (IncomingInfo c0 k pa q) ta < zcount (((c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z)) pa) ta
[PROOF STEP]
by (auto dest!: assms(1)[unfolded InvJustifiedII_def justified_alt supported_strong_def, rule_format])


[STATEMENT]
lemma next'_preserves_InvJustifiedII:
  "InvCapsNonneg c0 \<Longrightarrow> InvJustifiedII c0 \<Longrightarrow> next' c0 c1 \<Longrightarrow> InvJustifiedII c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvJustifiedII c0; next' c0 c1\<rbrakk> \<Longrightarrow> InvJustifiedII c1
[PROOF STEP]
using
    next'_def
    performop_preserves_InvJustifiedII
    recvcap_preserves_InvJustifiedII
    recvupd_preserves_InvJustifiedII
    sendupd_preserves_InvJustifiedII
[PROOF STATE]
proof (prove)
using this:
next' ?c0.0 ?c1.0 = (next_performop ?c0.0 ?c1.0 \<or> next_sendupd ?c0.0 ?c1.0 \<or> next_recvupd ?c0.0 ?c1.0 \<or> next_recvcap ?c0.0 ?c1.0 \<or> ?c1.0 = ?c0.0)
\<lbrakk>InvJustifiedII ?c0.0; next_performop' ?c0.0 ?c1.0 ?p ?\<Delta>neg ?\<Delta>mint_msg ?\<Delta>mint_self; InvCapsNonneg ?c0.0\<rbrakk> \<Longrightarrow> InvJustifiedII ?c1.0
\<lbrakk>InvJustifiedII ?c0.0; next_recvcap' ?c0.0 ?c1.0 ?p ?t\<rbrakk> \<Longrightarrow> InvJustifiedII ?c1.0
\<lbrakk>InvJustifiedII ?c0.0; next_recvupd' ?c0.0 ?c1.0 ?p ?q\<rbrakk> \<Longrightarrow> InvJustifiedII ?c1.0
\<lbrakk>InvJustifiedII ?c0.0; next_sendupd' ?c0.0 ?c1.0 ?p ?tt\<rbrakk> \<Longrightarrow> InvJustifiedII ?c1.0

goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvJustifiedII c0; next' c0 c1\<rbrakk> \<Longrightarrow> InvJustifiedII c1
[PROOF STEP]
by blast


[STATEMENT]
lemma alw_InvJustifiedII: "spec s \<Longrightarrow> alw (holds InvJustifiedII) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvJustifiedII) 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 InvJustifiedII) 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\<rbrakk> \<Longrightarrow> alw (holds InvJustifiedII) s
[PROOF STEP]
apply (elim conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvCapsNonneg) s; holds init_config s; alw next s\<rbrakk> \<Longrightarrow> alw (holds InvJustifiedII) s
[PROOF STEP]
apply (subst (asm) holds.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvCapsNonneg) s; init_config (shd s); alw next s\<rbrakk> \<Longrightarrow> alw (holds InvJustifiedII) s
[PROOF STEP]
apply (drule init_config_implies_InvJustifiedII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvCapsNonneg) s; alw next s; InvJustifiedII (shd s)\<rbrakk> \<Longrightarrow> alw (holds InvJustifiedII) 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 next s; InvJustifiedII (shd s)\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> holds InvJustifiedII xs \<and> ((\<exists>s. stl xs = s \<and> alw (holds InvCapsNonneg) s \<and> alw next s \<and> InvJustifiedII (shd s)) \<or> alw (holds InvJustifiedII) (stl xs))
[PROOF STEP]
apply (subst (asm) (1 2) alw_nxt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>holds InvCapsNonneg s \<and> nxt (alw (holds InvCapsNonneg)) s; next s \<and> nxt (alw next) s; InvJustifiedII (shd s)\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> holds InvJustifiedII xs \<and> ((\<exists>s. stl xs = s \<and> alw (holds InvCapsNonneg) s \<and> alw next s \<and> InvJustifiedII (shd s)) \<or> alw (holds InvJustifiedII) (stl xs))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>InvJustifiedII (shd s); InvCapsNonneg (shd s); alw (holds InvCapsNonneg) (stl s); next s; alw next (stl s); \<not> alw (holds InvJustifiedII) (stl s)\<rbrakk> \<Longrightarrow> InvJustifiedII (shd (stl s))
[PROOF STEP]
using next'_preserves_InvJustifiedII
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvCapsNonneg ?c0.0; InvJustifiedII ?c0.0; next' ?c0.0 ?c1.0\<rbrakk> \<Longrightarrow> InvJustifiedII ?c1.0

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


[STATEMENT]
lemma alw_InvJustifiedGII: "spec s \<Longrightarrow> alw (holds InvJustifiedGII) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvJustifiedGII) s
[PROOF STEP]
apply (frule alw_InvJustifiedII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvJustifiedII) s\<rbrakk> \<Longrightarrow> alw (holds InvJustifiedGII) s
[PROOF STEP]
apply (drule alw_InvCapsNonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvJustifiedII) s; alw (holds InvCapsNonneg) s\<rbrakk> \<Longrightarrow> alw (holds InvJustifiedGII) s
[PROOF STEP]
apply (simp add: alw_iff_sdrop InvJustifiedII_implies_InvJustifiedGII)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma init_config_implies_InvTempJustified: "init_config c \<Longrightarrow> InvTempJustified c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init_config c \<Longrightarrow> InvTempJustified c
[PROOF STEP]
unfolding init_config_def InvTempJustified_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. justified (c_caps c p) (c_temp c p)
[PROOF STEP]
using justified_add_records[OF justified_empty]
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount ?C' t \<Longrightarrow> justified ({#}\<^sub>z + ?C') {#}\<^sub>z

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. justified (c_caps c p) (c_temp c p)
[PROOF STEP]
by auto


[STATEMENT]
lemma recvcap_preserves_InvTempJustified:
  assumes "InvTempJustified c0"
    and   "next_recvcap' c0 c1 p t"
  shows   "InvTempJustified c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvTempJustified c1
[PROOF STEP]
using assms(1)[unfolded InvTempJustified_def, rule_format, of p] assms(1)
[PROOF STATE]
proof (prove)
using this:
justified (c_caps c0 p) (c_temp c0 p)
InvTempJustified c0

goal (1 subgoal):
 1. InvTempJustified c1
[PROOF STEP]
unfolding next_recvcapD[OF assms(2)] InvTempJustified_def
[PROOF STATE]
proof (prove)
using this:
justified (c_caps c0 p) (c_temp c0 p)
\<forall>p. justified (c_caps c0 p) (c_temp c0 p)

goal (1 subgoal):
 1. \<forall>pa. justified (((c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z)) pa) (c_temp c0 pa)
[PROOF STEP]
by - (frule justified_add_records[of _ _ "{#t#}\<^sub>z"], auto)


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

goal (1 subgoal):
 1. InvTempJustified c1
[PROOF STEP]
unfolding next_recvupdD[OF assms(2)] InvTempJustified_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p. justified (c_caps c0 p) (c_temp c0 p)

goal (1 subgoal):
 1. \<forall>p. justified (c_caps c0 p) (c_temp c0 p)
[PROOF STEP]
by assumption


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

goal (1 subgoal):
 1. InvTempJustified c1
[PROOF STEP]
unfolding next_sendupdD[OF assms(2)] InvTempJustified_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p. justified (c_caps c0 p) (c_temp c0 p)

goal (1 subgoal):
 1. \<forall>pa. justified (c_caps c0 pa) (if pa = p then c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else c_temp c0 pa)
[PROOF STEP]
using next_sendupdD(2)[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<forall>p. justified (c_caps c0 p) (c_temp c0 p)
justified (c_caps c0 p) (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#})

goal (1 subgoal):
 1. \<forall>pa. justified (c_caps c0 pa) (if pa = p then c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else c_temp c0 pa)
[PROOF STEP]
by auto


[STATEMENT]
lemma performop_preserves_InvTempJustified:
  assumes "InvTempJustified c0"
    and   "next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self"
    and   "InvCapsNonneg c0"
  shows   "InvTempJustified c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvTempJustified c1
[PROOF STEP]
unfolding InvTempJustified_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. justified (c_caps c1 p) (c_temp c1 p)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. justified (c_caps c1 p) (c_temp c1 p)
[PROOF STEP]
subgoal for p'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified (c_caps c1 p') (c_temp c1 p')
[PROOF STEP]
apply (cases "p'=p")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p' = p \<Longrightarrow> justified (c_caps c1 p') (c_temp c1 p')
 2. p' \<noteq> p \<Longrightarrow> justified (c_caps c1 p') (c_temp c1 p')
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified (c_caps c1 p') (c_temp c1 p')
[PROOF STEP]
unfolding next_performopD(5)[OF assms(2)] fun_upd_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified (c_caps c1 p') (if p' = p then c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else c_temp c0 p')
[PROOF STEP]
apply (simp only: if_P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified (c_caps c1 p) (c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
apply (rule next_performop'_preserves_justified[
            OF assms(1)[unfolded InvTempJustified_def, rule_format, of p],
            OF assms(2,3)])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified (c_caps c1 p') (c_temp c1 p')
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified (c_caps c1 p') (c_temp c1 p')
[PROOF STEP]
unfolding
        next_performopD[OF assms(2)]
        next_performop_complexD[OF assms(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified (((c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p') (((c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p')
[PROOF STEP]
using assms(1)[unfolded InvTempJustified_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>p. justified (c_caps c0 p) (c_temp c0 p)

goal (1 subgoal):
 1. p' \<noteq> p \<Longrightarrow> justified (((c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p') (((c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p')
[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'_preserves_InvTempJustified:
  "InvCapsNonneg c0 \<Longrightarrow> InvTempJustified c0 \<Longrightarrow> next' c0 c1 \<Longrightarrow> InvTempJustified c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvTempJustified c0; next' c0 c1\<rbrakk> \<Longrightarrow> InvTempJustified c1
[PROOF STEP]
using
    next'_def
    performop_preserves_InvTempJustified
    recvcap_preserves_InvTempJustified
    recvupd_preserves_InvTempJustified
    sendupd_preserves_InvTempJustified
[PROOF STATE]
proof (prove)
using this:
next' ?c0.0 ?c1.0 = (next_performop ?c0.0 ?c1.0 \<or> next_sendupd ?c0.0 ?c1.0 \<or> next_recvupd ?c0.0 ?c1.0 \<or> next_recvcap ?c0.0 ?c1.0 \<or> ?c1.0 = ?c0.0)
\<lbrakk>InvTempJustified ?c0.0; next_performop' ?c0.0 ?c1.0 ?p ?\<Delta>neg ?\<Delta>mint_msg ?\<Delta>mint_self; InvCapsNonneg ?c0.0\<rbrakk> \<Longrightarrow> InvTempJustified ?c1.0
\<lbrakk>InvTempJustified ?c0.0; next_recvcap' ?c0.0 ?c1.0 ?p ?t\<rbrakk> \<Longrightarrow> InvTempJustified ?c1.0
\<lbrakk>InvTempJustified ?c0.0; next_recvupd' ?c0.0 ?c1.0 ?p ?t\<rbrakk> \<Longrightarrow> InvTempJustified ?c1.0
\<lbrakk>InvTempJustified ?c0.0; next_sendupd' ?c0.0 ?c1.0 ?p ?tt\<rbrakk> \<Longrightarrow> InvTempJustified ?c1.0

goal (1 subgoal):
 1. \<lbrakk>InvCapsNonneg c0; InvTempJustified c0; next' c0 c1\<rbrakk> \<Longrightarrow> InvTempJustified c1
[PROOF STEP]
by blast


[STATEMENT]
lemma alw_InvTempJustified: "spec s \<Longrightarrow> alw (holds InvTempJustified) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvTempJustified) 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 InvTempJustified) 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\<rbrakk> \<Longrightarrow> alw (holds InvTempJustified) s
[PROOF STEP]
apply (elim conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvCapsNonneg) s; holds init_config s; alw next s\<rbrakk> \<Longrightarrow> alw (holds InvTempJustified) s
[PROOF STEP]
apply (subst (asm) holds.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvCapsNonneg) s; init_config (shd s); alw next s\<rbrakk> \<Longrightarrow> alw (holds InvTempJustified) s
[PROOF STEP]
apply (drule init_config_implies_InvTempJustified)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvCapsNonneg) s; alw next s; InvTempJustified (shd s)\<rbrakk> \<Longrightarrow> alw (holds InvTempJustified) 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 next s; InvTempJustified (shd s)\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> holds InvTempJustified xs \<and> ((\<exists>s. stl xs = s \<and> alw (holds InvCapsNonneg) s \<and> alw next s \<and> InvTempJustified (shd s)) \<or> alw (holds InvTempJustified) (stl xs))
[PROOF STEP]
apply (subst (asm) (1 2) alw_nxt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>holds InvCapsNonneg s \<and> nxt (alw (holds InvCapsNonneg)) s; next s \<and> nxt (alw next) s; InvTempJustified (shd s)\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> holds InvTempJustified xs \<and> ((\<exists>s. stl xs = s \<and> alw (holds InvCapsNonneg) s \<and> alw next s \<and> InvTempJustified (shd s)) \<or> alw (holds InvTempJustified) (stl xs))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>InvTempJustified (shd s); InvCapsNonneg (shd s); alw (holds InvCapsNonneg) (stl s); next s; alw next (stl s); \<not> alw (holds InvTempJustified) (stl s)\<rbrakk> \<Longrightarrow> InvTempJustified (shd (stl s))
[PROOF STEP]
using next'_preserves_InvTempJustified
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvCapsNonneg ?c0.0; InvTempJustified ?c0.0; next' ?c0.0 ?c1.0\<rbrakk> \<Longrightarrow> InvTempJustified ?c1.0

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


[STATEMENT]
lemma invs_imp_InvGlobNonposImpRecordsNonpos:
  assumes "InvJustifiedGII c"
    and   "InvRecordCount c"
    and   "InvRecordsNonneg c"
  shows   "InvGlobNonposImpRecordsNonpos c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvGlobNonposImpRecordsNonpos c
[PROOF STEP]
unfolding InvGlobNonposImpRecordsNonpos_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t q. GlobNonposUpto c q t \<longrightarrow> nonpos_upto (records c) t
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>t q. GlobNonposUpto c q t \<longrightarrow> nonpos_upto (records c) t) \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp simp: nonpos_upto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t q s. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; s \<le> t; \<not> zcount (records c) s \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for t q u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?GII = "GlobalIncomingInfoAt c q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume gvu: "\<forall>sa\<le>t. zcount (c_glob c q) sa \<le> 0"
[PROOF STATE]
proof (state)
this:
\<forall>sa\<le>t. zcount (c_glob c q) sa \<le> 0

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume uleqt: "u \<le> t"
[PROOF STATE]
proof (state)
this:
u \<le> t

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<not> zcount (records c) u \<le> 0"
      \<comment> \<open>u is pointstamp that violates @{term InvGlobNonposImpRecordsNonpos}\<close>
[PROOF STATE]
proof (state)
this:
\<not> zcount (records c) u \<le> 0

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
InvRecordCount c
\<not> zcount (records c) u \<le> 0
[PROOF STEP]
have u: "0 < zcount (records c) u"
[PROOF STATE]
proof (prove)
using this:
InvRecordCount c
\<not> zcount (records c) u \<le> 0

goal (1 subgoal):
 1. 0 < zcount (records c) u
[PROOF STEP]
by linarith
        \<comment> \<open>u' is the least pointstamp with positive @{term records}\<close>
[PROOF STATE]
proof (state)
this:
0 < zcount (records c) u

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with uleqt
[PROOF STATE]
proof (chain)
picking this:
u \<le> t
0 < zcount (records c) u
[PROOF STEP]
obtain u' where u': "0 < zcount (records c) u'" "\<forall>u. 0 < zcount (records c) u \<longrightarrow> \<not> u < u'" "u' \<le> t"
[PROOF STATE]
proof (prove)
using this:
u \<le> t
0 < zcount (records c) u

goal (1 subgoal):
 1. (\<And>u'. \<lbrakk>0 < zcount (records c) u'; \<forall>u. 0 < zcount (records c) u \<longrightarrow> \<not> u < u'; u' \<le> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using order_zmset_exists_foundation[OF u]
[PROOF STATE]
proof (prove)
using this:
u \<le> t
0 < zcount (records c) u
\<exists>s\<le>u. 0 < zcount (records c) s \<and> (\<forall>u. 0 < zcount (records c) u \<longrightarrow> \<not> u < s)

goal (1 subgoal):
 1. (\<And>u'. \<lbrakk>0 < zcount (records c) u'; \<forall>u. 0 < zcount (records c) u \<longrightarrow> \<not> u < u'; u' \<le> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
        \<comment> \<open>from the @{term records} count we know that GII also has positive count\<close>
[PROOF STATE]
proof (state)
this:
0 < zcount (records c) u'
\<forall>u. 0 < zcount (records c) u \<longrightarrow> \<not> u < u'
u' \<le> t

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from u'(1,3) assms(2) gvu
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (records c) u'
u' \<le> t
InvRecordCount c
\<forall>sa\<le>t. zcount (c_glob c q) sa \<le> 0
[PROOF STEP]
have pos_gii: "0 < zcount ?GII u'"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (records c) u'
u' \<le> t
InvRecordCount c
\<forall>sa\<le>t. zcount (c_glob c q) sa \<le> 0

goal (1 subgoal):
 1. 0 < zcount (GlobalIncomingInfoAt c q) u'
[PROOF STEP]
by (simp add: InvRecordCount_def) (smt (verit) zcount_union)
        \<comment> \<open>Case distinction on which part of the partition GII's u is in\<close>
[PROOF STATE]
proof (state)
this:
0 < zcount (GlobalIncomingInfoAt c q) u'

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
{ \<comment> \<open>Original proof from Abadi paper, change is justified by uprightness\<close>
[PROOF STATE]
proof (state)
this:
0 < zcount (GlobalIncomingInfoAt c q) u'

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "supported_strong ?GII u'"
        \<comment> \<open>uprightness gives us a lesser pointstamp with negative count in GII..\<close>
[PROOF STATE]
proof (state)
this:
supported_strong (GlobalIncomingInfoAt c q) u'

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supported_strong (GlobalIncomingInfoAt c q) u'
[PROOF STEP]
obtain v where v: "v \<le> u'" "zcount ?GII v < 0"
[PROOF STATE]
proof (prove)
using this:
supported_strong (GlobalIncomingInfoAt c q) u'

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<le> u'; zcount (GlobalIncomingInfoAt c q) v < 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using order.strict_implies_order supported_strong_def
[PROOF STATE]
proof (prove)
using this:
supported_strong (GlobalIncomingInfoAt c q) u'
?a < ?b \<Longrightarrow> ?a \<le> ?b
supported_strong ?a ?t \<equiv> \<exists>s<?t. zcount ?a s < 0 \<and> nonpos_upto ?a s

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<le> u'; zcount (GlobalIncomingInfoAt c q) v < 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
          \<comment> \<open>..which is also negative in @{term records}..\<close>
[PROOF STATE]
proof (state)
this:
v \<le> u'
zcount (GlobalIncomingInfoAt c q) v < 0

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with u'(3) v(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
u' \<le> t
v \<le> u'
InvRecordCount c
v \<le> u'
zcount (GlobalIncomingInfoAt c q) v < 0
[PROOF STEP]
have "zcount (records c) v < 0"
[PROOF STATE]
proof (prove)
using this:
u' \<le> t
v \<le> u'
InvRecordCount c
v \<le> u'
zcount (GlobalIncomingInfoAt c q) v < 0

goal (1 subgoal):
 1. zcount (records c) v < 0
[PROOF STEP]
by (smt (verit, ccfv_threshold) InvRecordCount_def gvu local.order_trans zcount_union)
          \<comment> \<open>..contradicting InvNrecNonneg\<close>
[PROOF STATE]
proof (state)
this:
zcount (records c) v < 0

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
InvRecordsNonneg c
zcount (records c) v < 0
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
InvRecordsNonneg c
zcount (records c) v < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding InvRecordsNonneg_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount (records c) t
zcount (records c) v < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using order_class.leD
[PROOF STATE]
proof (prove)
using this:
\<forall>t. 0 \<le> zcount (records c) t
zcount (records c) v < 0
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
supported_strong (GlobalIncomingInfoAt c q) u' \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
supported_strong (GlobalIncomingInfoAt c q) u' \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
{ \<comment> \<open>Change is justified by strictly lesser pointstamp in @{term records}\<close>
[PROOF STATE]
proof (state)
this:
supported_strong (GlobalIncomingInfoAt c q) u' \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<exists>t'<u'. 0 < zcount (records c) t'"
        \<comment> \<open>v is a strictly lesser positive count in @{term records}..\<close>
[PROOF STATE]
proof (state)
this:
\<exists>t'<u'. 0 < zcount (records c) t'

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t'<u'. 0 < zcount (records c) t'
[PROOF STEP]
obtain v where v: "v < u'" "0 < zcount (records c) v"
[PROOF STATE]
proof (prove)
using this:
\<exists>t'<u'. 0 < zcount (records c) t'

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v < u'; 0 < zcount (records c) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
          \<comment> \<open>..which contradicts the fact that we obtained @{term u'} as the least, positive pointstamp in @{term records}\<close>
[PROOF STATE]
proof (state)
this:
v < u'
0 < zcount (records c) v

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with u'(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>u. 0 < zcount (records c) u \<longrightarrow> \<not> u < u'
v < u'
0 < zcount (records c) v
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
\<forall>u. 0 < zcount (records c) u \<longrightarrow> \<not> u < u'
v < u'
0 < zcount (records c) v

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>t'<u'. 0 < zcount (records c) t' \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>t'<u'. 0 < zcount (records c) t' \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
{ \<comment> \<open>Change is justified by records\<close>
[PROOF STATE]
proof (state)
this:
\<exists>t'<u'. 0 < zcount (records c) t' \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "zcount ?GII u' < zcount (records c) u'"
[PROOF STATE]
proof (state)
this:
zcount (GlobalIncomingInfoAt c q) u' < zcount (records c) u'

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (GlobalIncomingInfoAt c q) u' < zcount (records c) u'
[PROOF STEP]
have "0 < zcount (c_glob c q) u'"
[PROOF STATE]
proof (prove)
using this:
zcount (GlobalIncomingInfoAt c q) u' < zcount (records c) u'

goal (1 subgoal):
 1. 0 < zcount (c_glob c q) u'
[PROOF STEP]
by (simp add: assms(2)[unfolded InvRecordCount_def, rule_format, of q])
[PROOF STATE]
proof (state)
this:
0 < zcount (c_glob c q) u'

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (c_glob c q) u'
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_glob c q) u'

goal (1 subgoal):
 1. False
[PROOF STEP]
using gvu u'(3)
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_glob c q) u'
\<forall>sa\<le>t. zcount (c_glob c q) sa \<le> 0
u' \<le> t

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
zcount (GlobalIncomingInfoAt c q) u' < zcount (records c) u' \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<le>t. zcount (c_glob c q) s \<le> 0; u \<le> t; \<not> zcount (records c) u \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
supported_strong (GlobalIncomingInfoAt c q) u' \<Longrightarrow> False
\<exists>t'<u'. 0 < zcount (records c) t' \<Longrightarrow> False
zcount (GlobalIncomingInfoAt c q) u' < zcount (records c) u' \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
supported_strong (GlobalIncomingInfoAt c q) u' \<Longrightarrow> False
\<exists>t'<u'. 0 < zcount (records c) t' \<Longrightarrow> False
zcount (GlobalIncomingInfoAt c q) u' < zcount (records c) u' \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
using pos_gii assms(1)[unfolded InvJustifiedGII_def justified_alt, rule_format, OF pos_gii]
[PROOF STATE]
proof (prove)
using this:
supported_strong (GlobalIncomingInfoAt c q) u' \<Longrightarrow> False
\<exists>t'<u'. 0 < zcount (records c) t' \<Longrightarrow> False
zcount (GlobalIncomingInfoAt c q) u' < zcount (records c) u' \<Longrightarrow> False
0 < zcount (GlobalIncomingInfoAt c q) u'
supported_strong (GlobalIncomingInfoAt c q) u' \<or> (\<exists>t'<u'. 0 < zcount (records c) t') \<or> zcount (GlobalIncomingInfoAt c q) u' < zcount (records c) u'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma invs_imp_InvGlobVacantImpRecordsVacant:
  assumes "InvJustifiedGII c"
    and   "InvRecordCount c"
    and   "InvRecordsNonneg c"
  shows   "InvGlobVacantImpRecordsVacant c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
fix p x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
assume "GlobVacantUpto c p x"
[PROOF STATE]
proof (state)
this:
GlobVacantUpto c p x

goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
GlobVacantUpto c p x
[PROOF STEP]
have "GlobNonposUpto c p x"
[PROOF STATE]
proof (prove)
using this:
GlobVacantUpto c p x

goal (1 subgoal):
 1. GlobNonposUpto c p x
[PROOF STEP]
unfolding nonpos_upto_def vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<le>x. zcount (c_glob c p) s = 0

goal (1 subgoal):
 1. \<forall>s\<le>x. zcount (c_glob c p) s \<le> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
GlobNonposUpto c p x

goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
note invs_imp_InvGlobNonposImpRecordsNonpos[OF assms, unfolded InvGlobNonposImpRecordsNonpos_def, rule_format, OF this]
[PROOF STATE]
proof (state)
this:
nonpos_upto (records c) x

goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nonpos_upto (records c) x
[PROOF STEP]
have "RecordsVacantUpto c x"
[PROOF STATE]
proof (prove)
using this:
nonpos_upto (records c) x

goal (1 subgoal):
 1. RecordsVacantUpto c x
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
nonpos_upto (records c) x
InvRecordsNonneg c

goal (1 subgoal):
 1. RecordsVacantUpto c x
[PROOF STEP]
unfolding nonpos_upto_def vacant_upto_def InvRecordsNonneg_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<le>x. zcount (records c) s \<le> 0
\<forall>t. 0 \<le> zcount (records c) t

goal (1 subgoal):
 1. \<forall>s\<le>x. zcount (records c) s = 0
[PROOF STEP]
by (simp add: order_class.order.antisym)
[PROOF STATE]
proof (state)
this:
RecordsVacantUpto c x

goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
GlobVacantUpto c ?p2 ?x2 \<Longrightarrow> RecordsVacantUpto c ?x2

goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
GlobVacantUpto c ?p2 ?x2 \<Longrightarrow> RecordsVacantUpto c ?x2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
GlobVacantUpto c ?p2 ?x2 \<Longrightarrow> RecordsVacantUpto c ?x2

goal (1 subgoal):
 1. InvGlobVacantImpRecordsVacant c
[PROOF STEP]
unfolding InvGlobVacantImpRecordsVacant_def
[PROOF STATE]
proof (prove)
using this:
GlobVacantUpto c ?p2 ?x2 \<Longrightarrow> RecordsVacantUpto c ?x2

goal (1 subgoal):
 1. \<forall>t q. GlobVacantUpto c q t \<longrightarrow> RecordsVacantUpto c t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
InvGlobVacantImpRecordsVacant c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alw_InvGlobNonposImpRecordsNonpos: "spec s \<Longrightarrow> alw (holds InvGlobNonposImpRecordsNonpos) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvGlobNonposImpRecordsNonpos) s
[PROOF STEP]
apply (frule alw_InvJustifiedGII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvJustifiedGII) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobNonposImpRecordsNonpos) s
[PROOF STEP]
apply (frule alw_InvRecordCount)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvJustifiedGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobNonposImpRecordsNonpos) s
[PROOF STEP]
apply (drule alw_InvRecordsNonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvJustifiedGII) s; alw (holds InvRecordCount) s; alw (holds InvRecordsNonneg) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobNonposImpRecordsNonpos) s
[PROOF STEP]
apply (simp add: alw_iff_sdrop invs_imp_InvGlobNonposImpRecordsNonpos)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma alw_InvGlobVacantImpRecordsVacant: "spec s \<Longrightarrow> alw (holds InvGlobVacantImpRecordsVacant) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvGlobVacantImpRecordsVacant) s
[PROOF STEP]
apply (frule alw_InvGlobNonposImpRecordsNonpos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvGlobNonposImpRecordsNonpos) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobVacantImpRecordsVacant) s
[PROOF STEP]
apply (frule alw_InvJustifiedGII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvGlobNonposImpRecordsNonpos) s; alw (holds InvJustifiedGII) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobVacantImpRecordsVacant) s
[PROOF STEP]
apply (frule alw_InvRecordCount)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvGlobNonposImpRecordsNonpos) s; alw (holds InvJustifiedGII) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobVacantImpRecordsVacant) s
[PROOF STEP]
apply (drule alw_InvRecordsNonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvGlobNonposImpRecordsNonpos) s; alw (holds InvJustifiedGII) s; alw (holds InvRecordCount) s; alw (holds InvRecordsNonneg) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobVacantImpRecordsVacant) s
[PROOF STEP]
apply (simp add: alw_iff_sdrop invs_imp_InvGlobVacantImpRecordsVacant)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma invs_imp_SafeGlobVacantUptoImpliesStickyNrec:
  "SafeRecordsMono s \<Longrightarrow> holds InvGlobVacantImpRecordsVacant s \<Longrightarrow> SafeGlobVacantUptoImpliesStickyNrec s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SafeRecordsMono s; holds InvGlobVacantImpRecordsVacant s\<rbrakk> \<Longrightarrow> SafeGlobVacantUptoImpliesStickyNrec s
[PROOF STEP]
by (simp add: InvGlobVacantImpRecordsVacant_def SafeRecordsMono_def SafeGlobVacantUptoImpliesStickyNrec_def)


[STATEMENT]
lemma alw_SafeGlobVacantUptoImpliesStickyNrec:
  "spec s \<Longrightarrow> alw SafeGlobVacantUptoImpliesStickyNrec s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw SafeGlobVacantUptoImpliesStickyNrec s
[PROOF STEP]
by (meson alw_iff_sdrop invs_imp_SafeGlobVacantUptoImpliesStickyNrec alw_SafeRecordsMono alw_InvGlobVacantImpRecordsVacant)


[STATEMENT]
lemma invs_imp_InvGlobNonposEqVacant:
  assumes "InvRecordCount c"
    and   "InvJustifiedGII c"
    and   "InvRecordsNonneg c"
  shows   "InvGlobNonposEqVacant c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
note safe = invs_imp_InvGlobNonposImpRecordsNonpos[OF assms(2,1,3), unfolded InvGlobNonposImpRecordsNonpos_def nonpos_upto_def, THEN spec2, THEN mp]
[PROOF STATE]
proof (state)
this:
\<forall>s\<le>?x1. zcount (c_glob c ?y1) s \<le> 0 \<Longrightarrow> \<forall>s\<le>?x1. zcount (records c) s \<le> 0

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
note nonneg = assms(3)[unfolded InvRecordsNonneg_def, rule_format]
[PROOF STATE]
proof (state)
this:
0 \<le> zcount (records c) ?t

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
note count = assms(1)[unfolded InvRecordCount_def, rule_format]
[PROOF STATE]
proof (state)
this:
records c = GlobalIncomingInfoAt c ?q + c_glob c ?q

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
records c = GlobalIncomingInfoAt c ?q + c_glob c ?q

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
fix q t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
assume np: "GlobNonposUpto c q t"
[PROOF STATE]
proof (state)
this:
GlobNonposUpto c q t

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
assume nv: "\<not> GlobVacantUpto c q t"
      \<comment> \<open>Obtain the least, negative pointstamp in glob\<close>
[PROOF STATE]
proof (state)
this:
\<not> GlobVacantUpto c q t

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

goal (1 subgoal):
 1. \<exists>s\<le>t. zcount (c_glob c q) s < 0 \<and> (\<forall>s'<s. zcount (c_glob c q) s' = 0)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<le> t; s \<in>#\<^sub>z c_glob c q\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. zcount (c_glob c q) s < 0 \<and> (\<forall>s'<s. zcount (c_glob c q) s' = 0)
[PROOF STEP]
apply (drule elem_order_zmset_exists_foundation)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<le> t; \<exists>sa\<in>#\<^sub>zc_glob c q. sa \<le> s \<and> (\<forall>u\<in>#\<^sub>zc_glob c q. \<not> u < sa)\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. zcount (c_glob c q) s < 0 \<and> (\<forall>s'<s. zcount (c_glob c q) s' = 0)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>s \<le> t; sa \<in>#\<^sub>z c_glob c q; sa \<le> s; \<forall>u\<in>#\<^sub>zc_glob c q. \<not> u < sa\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. zcount (c_glob c q) s < 0 \<and> (\<forall>s'<s. zcount (c_glob c q) s' = 0)
[PROOF STEP]
subgoal for _ s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s_ \<le> t; s \<in>#\<^sub>z c_glob c q; s \<le> s_; \<forall>u\<in>#\<^sub>zc_glob c q. \<not> u < s\<rbrakk> \<Longrightarrow> \<exists>s\<le>t. zcount (c_glob c q) s < 0 \<and> (\<forall>s'<s. zcount (c_glob c q) s' = 0)
[PROOF STEP]
apply (rule exI[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s_ \<le> t; s \<in>#\<^sub>z c_glob c q; s \<le> s_; \<forall>u\<in>#\<^sub>zc_glob c q. \<not> u < s\<rbrakk> \<Longrightarrow> s \<le> t \<and> zcount (c_glob c q) s < 0 \<and> (\<forall>s'<s. zcount (c_glob c q) s' = 0)
[PROOF STEP]
apply (meson order.ordering_axioms nonpos_upto_def np order_class.le_less order_trans zcount_ne_zero_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
        \<comment> \<open>No records @{term "s' \<le> s"} can exist, since that would violate InvGlobNonposImpRecordsNonpos\<close>
[PROOF STATE]
proof (state)
this:
s \<le> t
zcount (c_glob c q) s < 0
\<forall>s'<s. zcount (c_glob c q) s' = 0

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
have norec: "s' \<le> s \<Longrightarrow> zcount (records c) s' = 0" for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' \<le> s \<Longrightarrow> zcount (records c) s' = 0
[PROOF STEP]
by (metis (full_types) nonneg nonpos_upto_def np order_class.antisym_conv order_trans s(1) safe)
        \<comment> \<open>Hence GII must be positive at @{term s}\<close>
[PROOF STATE]
proof (state)
this:
?s' \<le> s \<Longrightarrow> zcount (records c) ?s' = 0

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
have gii: "zcount (GlobalIncomingInfoAt c q) s > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (GlobalIncomingInfoAt c q) s
[PROOF STEP]
using count[of q] s(2) norec[of s, simplified]
[PROOF STATE]
proof (prove)
using this:
records c = GlobalIncomingInfoAt c q + c_glob c q
zcount (c_glob c q) s < 0
zcount (records c) s = 0

goal (1 subgoal):
 1. 0 < zcount (GlobalIncomingInfoAt c q) s
[PROOF STEP]
by (metis add.commute less_add_same_cancel1 zcount_union)
        \<comment> \<open>which means it must be justified by one of these three disjuncts\<close>
[PROOF STATE]
proof (state)
this:
0 < zcount (GlobalIncomingInfoAt c q) s

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (GlobalIncomingInfoAt c q) s
[PROOF STEP]
consider
      "supported_strong (GlobalIncomingInfoAt c q) s" |
      "\<exists>t'<s. 0 < zcount (records c) t'" |
      "zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (GlobalIncomingInfoAt c q) s

goal (1 subgoal):
 1. \<lbrakk>supported_strong (GlobalIncomingInfoAt c q) s \<Longrightarrow> thesis; \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> thesis; zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)[unfolded InvJustifiedGII_def justified_alt, rule_format, OF gii]
[PROOF STATE]
proof (prove)
using this:
0 < zcount (GlobalIncomingInfoAt c q) s
supported_strong (GlobalIncomingInfoAt c q) s \<or> (\<exists>t'<s. 0 < zcount (records c) t') \<or> zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s

goal (1 subgoal):
 1. \<lbrakk>supported_strong (GlobalIncomingInfoAt c q) s \<Longrightarrow> thesis; \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> thesis; zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>supported_strong (GlobalIncomingInfoAt c q) s \<Longrightarrow> ?thesis; \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> ?thesis; zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>supported_strong (GlobalIncomingInfoAt c q) s \<Longrightarrow> ?thesis; \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> ?thesis; zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>supported_strong (GlobalIncomingInfoAt c q) s \<Longrightarrow> ?thesis; \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> ?thesis; zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. supported_strong (GlobalIncomingInfoAt c q) s \<Longrightarrow> False
 2. \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> False
 3. zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> False
[PROOF STEP]
case 1 \<comment> \<open>@{term s} can't be @{term supported_strong}, since either glob or records would have to be positive at the support\<close>
[PROOF STATE]
proof (state)
this:
supported_strong (GlobalIncomingInfoAt c q) s

goal (3 subgoals):
 1. supported_strong (GlobalIncomingInfoAt c q) s \<Longrightarrow> False
 2. \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> False
 3. zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supported_strong (GlobalIncomingInfoAt c q) s
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
supported_strong (GlobalIncomingInfoAt c q) s

goal (1 subgoal):
 1. False
[PROOF STEP]
using norec count s(3)
[PROOF STATE]
proof (prove)
using this:
supported_strong (GlobalIncomingInfoAt c q) s
?s' \<le> s \<Longrightarrow> zcount (records c) ?s' = 0
records c = GlobalIncomingInfoAt c ?q + c_glob c ?q
\<forall>s'<s. zcount (c_glob c q) s' = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding supported_strong_def
[PROOF STATE]
proof (prove)
using this:
\<exists>sa<s. zcount (GlobalIncomingInfoAt c q) sa < 0 \<and> nonpos_upto (GlobalIncomingInfoAt c q) sa
?s' \<le> s \<Longrightarrow> zcount (records c) ?s' = 0
records c = GlobalIncomingInfoAt c ?q + c_glob c ?q
\<forall>s'<s. zcount (c_glob c q) s' = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (full_types) add.commute add.left_neutral less_le preorder_class.less_irrefl zcount_union)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> False
 2. zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> False
 2. zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> False
[PROOF STEP]
case 2 \<comment> \<open>no lesser capabilities exist\<close>
[PROOF STATE]
proof (state)
this:
\<exists>t'<s. 0 < zcount (records c) t'

goal (2 subgoals):
 1. \<exists>t'<s. 0 < zcount (records c) t' \<Longrightarrow> False
 2. zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t'<s. 0 < zcount (records c) t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>t'<s. 0 < zcount (records c) t'

goal (1 subgoal):
 1. False
[PROOF STEP]
using norec s(2,3) order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
\<exists>t'<s. 0 < zcount (records c) t'
?s' \<le> s \<Longrightarrow> zcount (records c) ?s' = 0
zcount (c_glob c q) s < 0
\<forall>s'<s. zcount (c_glob c q) s' = 0
(?a \<le> ?b) = (?a < ?b \<or> ?a = ?b)

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

goal (1 subgoal):
 1. zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> False
[PROOF STEP]
case 3 \<comment> \<open>no capabilities at @{term s} exist\<close>
[PROOF STATE]
proof (state)
this:
zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s

goal (1 subgoal):
 1. zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zcount (GlobalIncomingInfoAt c q) s < zcount (records c) s

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding norec[of s, simplified]
[PROOF STATE]
proof (prove)
using this:
zcount (GlobalIncomingInfoAt c q) s < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using gii
[PROOF STATE]
proof (prove)
using this:
zcount (GlobalIncomingInfoAt c q) s < 0
0 < zcount (GlobalIncomingInfoAt c q) s

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

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

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>GlobNonposUpto c ?q2 ?t2; \<not> GlobVacantUpto c ?q2 ?t2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>GlobNonposUpto c ?q2 ?t2; \<not> GlobVacantUpto c ?q2 ?t2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>GlobNonposUpto c ?q2 ?t2; \<not> GlobVacantUpto c ?q2 ?t2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. InvGlobNonposEqVacant c
[PROOF STEP]
unfolding InvGlobNonposEqVacant_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>GlobNonposUpto c ?q2 ?t2; \<not> GlobVacantUpto c ?q2 ?t2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>q t. GlobVacantUpto c q t = GlobNonposUpto c q t
[PROOF STEP]
apply (intro allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q t. (\<And>q t. \<lbrakk>GlobNonposUpto c q t; \<not> GlobVacantUpto c q t\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> GlobVacantUpto c q t = GlobNonposUpto c q t
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q t. \<lbrakk>\<And>q t. \<lbrakk>GlobNonposUpto c q t; \<not> GlobVacantUpto c q t\<rbrakk> \<Longrightarrow> False; GlobVacantUpto c q t\<rbrakk> \<Longrightarrow> GlobNonposUpto c q t
 2. \<And>q t. \<lbrakk>\<And>q t. \<lbrakk>GlobNonposUpto c q t; \<not> GlobVacantUpto c q t\<rbrakk> \<Longrightarrow> False; GlobNonposUpto c q t\<rbrakk> \<Longrightarrow> GlobVacantUpto c q t
[PROOF STEP]
apply (simp add: nonpos_upto_def vacant_upto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q t. \<lbrakk>\<And>q t. \<lbrakk>GlobNonposUpto c q t; \<not> GlobVacantUpto c q t\<rbrakk> \<Longrightarrow> False; GlobNonposUpto c q t\<rbrakk> \<Longrightarrow> GlobVacantUpto c q t
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
InvGlobNonposEqVacant c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alw_InvGlobNonposEqVacant: "spec s \<Longrightarrow> alw (holds InvGlobNonposEqVacant) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvGlobNonposEqVacant) s
[PROOF STEP]
using
    alw_InvJustifiedGII
    alw_InvRecordCount
    alw_InvRecordsNonneg
    invs_imp_InvGlobNonposEqVacant
[PROOF STATE]
proof (prove)
using this:
spec ?s \<Longrightarrow> alw (holds InvJustifiedGII) ?s
spec ?s \<Longrightarrow> alw (holds InvRecordCount) ?s
spec ?s \<Longrightarrow> alw (holds InvRecordsNonneg) ?s
\<lbrakk>InvRecordCount ?c; InvJustifiedGII ?c; InvRecordsNonneg ?c\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant ?c

goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds InvGlobNonposEqVacant) s
[PROOF STEP]
by (metis alw_iff_sdrop holds.elims(2) holds.elims(3))


[STATEMENT]
lemma init_config_implies_InvInfoJustifiedWithII: "init_config c \<Longrightarrow> InvInfoJustifiedWithII c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init_config c \<Longrightarrow> InvInfoJustifiedWithII c
[PROOF STEP]
unfolding init_config_def InvInfoJustifiedWithII_def justified_with_def InfoAt_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>k p q t. 0 < zcount (if 0 \<le> k \<and> k < length (c_msg c p q) then c_msg c p q ! k else {#}\<^sub>z) t \<longrightarrow> (\<exists>s<t. zcount (if 0 \<le> k \<and> k < length (c_msg c p q) then c_msg c p q ! k else {#}\<^sub>z) s < 0 \<or> zcount (IncomingInfo c (k + 1) p q) s < 0) \<or> (\<exists>s<t. 0 < zcount (c_caps c p) s) \<or> zcount ((if 0 \<le> k \<and> k < length (c_msg c p q) then c_msg c p q ! k else {#}\<^sub>z) + IncomingInfo c (k + 1) p q) t < zcount (c_caps c p) t
[PROOF STEP]
by auto


[STATEMENT]
lemma performop_preserves_InvInfoJustifiedWithII:
  assumes "InvInfoJustifiedWithII c0"
    and   "next_performop' c0 c1 p' \<Delta>neg \<Delta>mint_msg \<Delta>mint_self"
    and   "InvJustifiedII c0"
    and   "InvCapsNonneg 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]
apply (intro allI)
[PROOF STATE]
proof (prove)
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]
subgoal for k p q
[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 (cases "p'=p")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p' = p \<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]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified_with (c_caps c1 p) (InfoAt c1 k p q) (IncomingInfo c1 (k + 1) p q)
[PROOF STEP]
unfolding next_performop_complexD[OF assms(2)] next_performopD[OF assms(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified_with (((c_caps c0)(p' := c_caps c0 p' + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p) (InfoAt c0 k p q) (if p = p' then IncomingInfo c0 (k + 1) p q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 (k + 1) p q)
[PROOF STEP]
apply (simp only: add_diff_eq if_P fun_upd_same)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified_with (c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) (InfoAt c0 k p q) (IncomingInfo c0 (k + 1) p q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self) - zmset_of \<Delta>neg)
[PROOF STEP]
apply (subst (4) add.commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified_with (c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) (InfoAt c0 k p q) (IncomingInfo c0 (k + 1) p q + (zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg)) - zmset_of \<Delta>neg)
[PROOF STEP]
apply (subst add.assoc[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified_with (c_caps c0 p + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) (InfoAt c0 k p q) (IncomingInfo c0 (k + 1) p q + zmset_of \<Delta>mint_self + timestamps (zmset_of \<Delta>mint_msg) - zmset_of \<Delta>neg)
[PROOF STEP]
apply (rule next_performop'_preserves_justified_with)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. p' = p \<Longrightarrow> justified_with (c_caps c0 p) (InfoAt c0 k p q) (IncomingInfo c0 (k + 1) p q)
 2. p' = p \<Longrightarrow> next_performop' c0 ?c1.2 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self
 3. p' = p \<Longrightarrow> \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 4. p' = p \<Longrightarrow> justified (c_caps c0 p) (IncomingInfo c0 (k + 1) p q)
[PROOF STEP]
using assms(1)[unfolded InvInfoJustifiedWithII_def]
[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 (4 subgoals):
 1. p' = p \<Longrightarrow> justified_with (c_caps c0 p) (InfoAt c0 k p q) (IncomingInfo c0 (k + 1) p q)
 2. p' = p \<Longrightarrow> next_performop' c0 ?c1.2 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self
 3. p' = p \<Longrightarrow> \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 4. p' = p \<Longrightarrow> justified (c_caps c0 p) (IncomingInfo c0 (k + 1) p q)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. p' = p \<Longrightarrow> next_performop' c0 ?c1.2 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self
 2. p' = p \<Longrightarrow> \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 3. p' = p \<Longrightarrow> justified (c_caps c0 p) (IncomingInfo c0 (k + 1) p q)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
next_performop' c0 c1 p' \<Delta>neg \<Delta>mint_msg \<Delta>mint_self

goal (3 subgoals):
 1. p' = p \<Longrightarrow> next_performop' c0 ?c1.2 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self
 2. p' = p \<Longrightarrow> \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 3. p' = p \<Longrightarrow> justified (c_caps c0 p) (IncomingInfo c0 (k + 1) p q)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p' = p \<Longrightarrow> \<forall>t. 0 \<le> zcount (c_caps c0 p) t
 2. p' = p \<Longrightarrow> justified (c_caps c0 p) (IncomingInfo c0 (k + 1) p q)
[PROOF STEP]
using assms(4)[unfolded InvCapsNonneg_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>p t. 0 \<le> zcount (c_caps c0 p) t

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

goal (1 subgoal):
 1. p' = p \<Longrightarrow> justified (c_caps c0 p) (IncomingInfo c0 (k + 1) p q)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
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]
subgoal
[PROOF STATE]
proof (prove)
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]
using assms(1)[unfolded InvInfoJustifiedWithII_def justified_with_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>k p q t. 0 < zcount (InfoAt c0 k p q) t \<longrightarrow> (\<exists>s<t. zcount (InfoAt c0 k p q) s < 0 \<or> zcount (IncomingInfo c0 (k + 1) p q) s < 0) \<or> (\<exists>s<t. 0 < zcount (c_caps c0 p) s) \<or> zcount (InfoAt c0 k p q + IncomingInfo c0 (k + 1) p q) t < zcount (c_caps c0 p) t

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]
by (auto simp: not_less justified_with_def next_performop_complexD[OF assms(2)] next_performopD[OF assms(2)])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done