[STATEMENT]
lemma invs_imp_msg_in_glob:
  fixes c :: "('p::finite, 'a) configuration"
  assumes "M \<in> set (c_msg c p q)"
    and   "t \<in>#\<^sub>z M"
    and   "InvGlobNonposEqVacant c"
    and   "InvJustifiedII c"
    and   "InvInfoJustifiedWithII c"
    and   "InvGlobVacantImpRecordsVacant c"
    and   "InvRecordCount c"
    and   "InvCapsNonneg c"
    and   "InvMsgInGlob c"
  shows   "\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'\<le>t. 0 < zcount (c_glob c q) t'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t')"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t')

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t')
[PROOF STEP]
have vacant: "\<forall>t'\<le>t. zcount (c_glob c q) t' = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t')

goal (1 subgoal):
 1. \<forall>t'\<le>t. zcount (c_glob c q) t' = 0
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t')
InvGlobNonposEqVacant c

goal (1 subgoal):
 1. \<forall>t'\<le>t. zcount (c_glob c q) t' = 0
[PROOF STEP]
by (auto simp: InvGlobNonposEqVacant_def vacant_upto_def nonpos_upto_def)
[PROOF STATE]
proof (state)
this:
\<forall>t'\<le>t. zcount (c_glob c q) t' = 0

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
let ?c1 = "the (while_option (\<lambda>c. hd (c_msg c p q) \<noteq> M) (\<lambda>c. SOME c'. next_recvupd' c c' p q) c)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
have r[simp]: "M \<in> set (c_msg c p q) \<Longrightarrow> c_msg (SOME c'. next_recvupd' c c' p q) p q = tl (c_msg c p q)" for c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<in> set (c_msg c p q) \<Longrightarrow> c_msg (SOME c'. next_recvupd' c c' p q) p q = tl (c_msg c p q)
[PROOF STEP]
by (rule someI2_ex[OF ex_next_recvupd]) (auto simp: next_recvupd'_def)
[PROOF STATE]
proof (state)
this:
M \<in> set (c_msg ?c p q) \<Longrightarrow> c_msg (SOME c'. next_recvupd' ?c c' p q) p q = tl (c_msg ?c p q)

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
obtain c1 where while_some:
    "while_option (\<lambda>c. hd (c_msg c p q) \<noteq> M) (\<lambda>c. SOME c'. next_recvupd' c c' p q) c = Some c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c1. while_option (\<lambda>c. hd (c_msg c p q) \<noteq> M) (\<lambda>c. SOME c'. next_recvupd' c c' p q) c = Some c1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c1. while_option (\<lambda>c. hd (c_msg c p q) \<noteq> M) (\<lambda>c. SOME c'. next_recvupd' c c' p q) c = Some c1
[PROOF STEP]
apply (rule measure_while_option_Some[where P="\<lambda>c. M \<in> set (c_msg c p q)"
          and f="\<lambda>c. Min {i. i < length (c_msg c p q) \<and> M = c_msg c p q ! i}"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> M \<in> set (c_msg (SOME c'. next_recvupd' s c' p q) p q) \<and> Min {i. i < length (c_msg (SOME c'. next_recvupd' s c' p q) p q) \<and> M = c_msg (SOME c'. next_recvupd' s c' p q) p q ! i} < Min {i. i < length (c_msg s p q) \<and> M = c_msg s p q ! i}
 2. M \<in> set (c_msg c p q)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> M \<in> set (tl (c_msg s p q)) \<and> Min {i. i < length (c_msg s p q) - Suc 0 \<and> M = tl (c_msg s p q) ! i} < Min {i. i < length (c_msg s p q) \<and> M = c_msg s p q ! i}
 2. M \<in> set (c_msg c p q)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> M \<in> set (tl (c_msg s p q))
 2. \<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> Min {i. i < length (c_msg s p q) - Suc 0 \<and> M = tl (c_msg s p q) ! i} < Min {i. i < length (c_msg s p q) \<and> M = c_msg s p q ! i}
 3. M \<in> set (c_msg c p q)
[PROOF STEP]
apply (metis list.exhaust_sel list.sel(2) set_ConsD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> Min {i. i < length (c_msg s p q) - Suc 0 \<and> M = tl (c_msg s p q) ! i} < Min {i. i < length (c_msg s p q) \<and> M = c_msg s p q ! i}
 2. M \<in> set (c_msg c p q)
[PROOF STEP]
apply (subst Min_gr_iff)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> finite {i. i < length (c_msg s p q) \<and> M = c_msg s p q ! i}
 2. \<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> {i. i < length (c_msg s p q) \<and> M = c_msg s p q ! i} \<noteq> {}
 3. \<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> Ball {i. i < length (c_msg s p q) \<and> M = c_msg s p q ! i} ((<) (Min {i. i < length (c_msg s p q) - Suc 0 \<and> M = tl (c_msg s p q) ! i}))
 4. M \<in> set (c_msg c p q)
[PROOF STEP]
apply (auto simp: in_set_conv_nth nth_tl) [2]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> Ball {i. i < length (c_msg s p q) \<and> M = c_msg s p q ! i} ((<) (Min {i. i < length (c_msg s p q) - Suc 0 \<and> M = tl (c_msg s p q) ! i}))
 2. M \<in> set (c_msg c p q)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> Min {i. i < length (c_msg s p q) - Suc 0 \<and> c_msg s p q ! x = tl (c_msg s p q) ! i} < x
 2. M \<in> set (c_msg c p q)
[PROOF STEP]
apply (subst Min_less_iff)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> finite {i. i < length (c_msg s p q) - Suc 0 \<and> c_msg s p q ! x = tl (c_msg s p q) ! i}
 2. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> {i. i < length (c_msg s p q) - Suc 0 \<and> c_msg s p q ! x = tl (c_msg s p q) ! i} \<noteq> {}
 3. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> \<exists>a\<in>{i. i < length (c_msg s p q) - Suc 0 \<and> c_msg s p q ! x = tl (c_msg s p q) ! i}. a < x
 4. M \<in> set (c_msg c p q)
[PROOF STEP]
apply (auto simp: in_set_conv_nth nth_tl) []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> {i. i < length (c_msg s p q) - Suc 0 \<and> c_msg s p q ! x = tl (c_msg s p q) ! i} \<noteq> {}
 2. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> \<exists>a\<in>{i. i < length (c_msg s p q) - Suc 0 \<and> c_msg s p q ! x = tl (c_msg s p q) ! i}. a < x
 3. M \<in> set (c_msg c p q)
[PROOF STEP]
apply (clarsimp simp: in_set_conv_nth nth_tl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> \<exists>xa<length (c_msg s p q) - Suc 0. c_msg s p q ! x = c_msg s p q ! Suc xa
 2. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> \<exists>a\<in>{i. i < length (c_msg s p q) - Suc 0 \<and> c_msg s p q ! x = tl (c_msg s p q) ! i}. a < x
 3. M \<in> set (c_msg c p q)
[PROOF STEP]
apply (metis (no_types, opaque_lifting) Suc_less_eq Suc_pred hd_conv_nth list.size(3) not_gr_zero not_less_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> \<exists>a\<in>{i. i < length (c_msg s p q) - Suc 0 \<and> c_msg s p q ! x = tl (c_msg s p q) ! i}. a < x
 2. M \<in> set (c_msg c p q)
[PROOF STEP]
apply (clarsimp simp: in_set_conv_nth nth_tl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> \<exists>a<length (c_msg s p q) - Suc 0. c_msg s p q ! x = tl (c_msg s p q) ! a \<and> a < x
 2. M \<in> set (c_msg c p q)
[PROOF STEP]
subgoal for s x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hd (c_msg s p q) \<noteq> c_msg s p q ! x; x < length (c_msg s p q); M = c_msg s p q ! x\<rbrakk> \<Longrightarrow> \<exists>a<length (c_msg s p q) - Suc 0. c_msg s p q ! x = tl (c_msg s p q) ! a \<and> a < x
[PROOF STEP]
by (rule exI[of _ "x-1"])
        (metis One_nat_def Suc_le_eq Suc_pred' diff_less diff_less_mono hd_conv_nth length_tl list.size(3) not_gr_zero nth_tl zero_less_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<in> set (c_msg c p q)
[PROOF STEP]
apply (meson assms(1) in_set_conv_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
while_option (\<lambda>c. hd (c_msg c p q) \<noteq> M) (\<lambda>c. SOME c'. next_recvupd' c c' p q) c = Some c1

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
have c1: "(\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c c1" "c_msg c1 p q \<noteq> []" "hd (c_msg c1 p q) = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c c1 &&& c_msg c1 p q \<noteq> [] &&& hd (c_msg c1 p q) = M
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c c1
[PROOF STEP]
apply (rule conjunct2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?P \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c c1
[PROOF STEP]
apply (rule while_option_rule[OF _ while_some, where P="\<lambda>d. M \<in> set (c_msg d p q) \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c d"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>M \<in> set (c_msg s p q) \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c s; hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> M \<in> set (c_msg (SOME c'. next_recvupd' s c' p q) p q) \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c (SOME c'. next_recvupd' s c' p q)
 2. M \<in> set (c_msg c p q) \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c c
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>M \<in> set (c_msg s p q) \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c s; hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> M \<in> set (c_msg (SOME c'. next_recvupd' s c' p q) p q)
 2. \<And>s. \<lbrakk>M \<in> set (c_msg s p q) \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c s; hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c (SOME c'. next_recvupd' s c' p q)
 3. M \<in> set (c_msg c p q) \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c c
[PROOF STEP]
apply (metis list.sel(1) list.sel(3) list.set_cases r)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>M \<in> set (c_msg s p q) \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c s; hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c (SOME c'. next_recvupd' s c' p q)
 2. M \<in> set (c_msg c p q) \<and> (\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c c
[PROOF STEP]
apply (auto simp: assms(1) elim!: rtrancl_into_rtrancl[to_pred] intro: someI2_ex[OF ex_next_recvupd])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. c_msg c1 p q \<noteq> []
 2. hd (c_msg c1 p q) = M
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_msg c1 p q \<noteq> []
[PROOF STEP]
using while_option_rule[OF _ while_some, where P="\<lambda>c. M \<in> set (c_msg c p q)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>s. \<lbrakk>M \<in> set (c_msg s p q); hd (c_msg s p q) \<noteq> M\<rbrakk> \<Longrightarrow> M \<in> set (c_msg (SOME c'. next_recvupd' s c' p q) p q); M \<in> set (c_msg c p q)\<rbrakk> \<Longrightarrow> M \<in> set (c_msg c1 p q)

goal (1 subgoal):
 1. c_msg c1 p q \<noteq> []
[PROOF STEP]
by (metis assms(1) empty_iff hd_Cons_tl list.set(1) r set_ConsD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (c_msg c1 p q) = M
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (c_msg c1 p q) = M
[PROOF STEP]
using while_option_stop[OF while_some]
[PROOF STATE]
proof (prove)
using this:
\<not> hd (c_msg c1 p q) \<noteq> M

goal (1 subgoal):
 1. hd (c_msg c1 p q) = M
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c c1
c_msg c1 p q \<noteq> []
hd (c_msg c1 p q) = M

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
have invs_trancl:
    "(\<lambda>c0 c1. SafeGlobMono c0 c1 \<and> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1)\<^sup>*\<^sup>* c c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>c0 c1. SafeGlobMono c0 c1 \<and> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1)\<^sup>*\<^sup>* c c1
[PROOF STEP]
apply (rule rtranclp_rel_and_invar)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ?r\<^sup>*\<^sup>* c c1
 2. InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c
 3. \<forall>a b. (InvJustifiedII a \<and> InvGlobNonposEqVacant a \<and> InvInfoJustifiedWithII a \<and> InvGlobVacantImpRecordsVacant a \<and> InvRecordCount a \<and> InvCapsNonneg a) \<and> ?r a b \<longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
using c1(1)
[PROOF STATE]
proof (prove)
using this:
(\<lambda>c0 c1. next_recvupd' c0 c1 p q)\<^sup>*\<^sup>* c c1

goal (3 subgoals):
 1. ?r\<^sup>*\<^sup>* c c1
 2. InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c
 3. \<forall>a b. (InvJustifiedII a \<and> InvGlobNonposEqVacant a \<and> InvInfoJustifiedWithII a \<and> InvGlobVacantImpRecordsVacant a \<and> InvRecordCount a \<and> InvCapsNonneg a) \<and> ?r a b \<longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c
 2. \<forall>a b. (InvJustifiedII a \<and> InvGlobNonposEqVacant a \<and> InvInfoJustifiedWithII a \<and> InvGlobVacantImpRecordsVacant a \<and> InvRecordCount a \<and> InvCapsNonneg a) \<and> next_recvupd' a b p q \<longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
using assms(3-8)
[PROOF STATE]
proof (prove)
using this:
InvGlobNonposEqVacant c
InvJustifiedII c
InvInfoJustifiedWithII c
InvGlobVacantImpRecordsVacant c
InvRecordCount c
InvCapsNonneg c

goal (2 subgoals):
 1. InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c
 2. \<forall>a b. (InvJustifiedII a \<and> InvGlobNonposEqVacant a \<and> InvInfoJustifiedWithII a \<and> InvGlobVacantImpRecordsVacant a \<and> InvRecordCount a \<and> InvCapsNonneg a) \<and> next_recvupd' a b p q \<longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. (InvJustifiedII a \<and> InvGlobNonposEqVacant a \<and> InvInfoJustifiedWithII a \<and> InvGlobVacantImpRecordsVacant a \<and> InvRecordCount a \<and> InvCapsNonneg a) \<and> next_recvupd' a b p q \<longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
subgoal for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule InvJustifiedII_implies_InvJustifiedGII)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q\<rbrakk> \<Longrightarrow> InvCapsNonneg a
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule recvupd_preserves_InvJustifiedII)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a\<rbrakk> \<Longrightarrow> next_recvupd' a ?c1.3 ?p3 ?q3
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII ?c1.3\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule InvCapsNonneg_imp_InvRecordsNonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule next_preserves_InvRecordCount[of _ b])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a\<rbrakk> \<Longrightarrow> next' a b
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (auto simp: next'_def) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule recvupd_preserves_InvCapsNonneg[of _ b])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b\<rbrakk> \<Longrightarrow> next_recvupd' a b ?p20 ?q20
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule InvJustifiedII_implies_InvJustifiedGII[of b])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b\<rbrakk> \<Longrightarrow> InvCapsNonneg b
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule InvCapsNonneg_imp_InvRecordsNonneg[of b])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule invs_imp_InvGlobNonposEqVacant[of b])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b\<rbrakk> \<Longrightarrow> InvJustifiedGII b
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b\<rbrakk> \<Longrightarrow> InvRecordsNonneg b
 3. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp_all [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule recvupd_preserves_InvInfoJustifiedWithII[of _ b])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b\<rbrakk> \<Longrightarrow> next_recvupd' a b ?p34 ?q34
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule invs_imp_InvInfoJustifiedWithGII)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b\<rbrakk> \<Longrightarrow> InvJustifiedII a
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b\<rbrakk> \<Longrightarrow> InvCapsNonneg a
 3. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp_all [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (frule invs_imp_InvInfoJustifiedWithGII[of b])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a\<rbrakk> \<Longrightarrow> InvJustifiedII b
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a\<rbrakk> \<Longrightarrow> InvCapsNonneg b
 3. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply simp_all [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> SafeGlobMono a b \<and> InvJustifiedII b \<and> InvGlobNonposEqVacant b \<and> InvInfoJustifiedWithII b \<and> InvGlobVacantImpRecordsVacant b \<and> InvRecordCount b \<and> InvCapsNonneg b
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> SafeGlobMono a b
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvJustifiedII b
 3. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant b
 4. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII b
 5. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant b
 6. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvRecordCount b
 7. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvCapsNonneg b
[PROOF STEP]
apply (rule next'_imp_SafeGlobMono)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> next' a b
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithGII a
 3. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant b
 4. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant a
 5. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvRecordCount a
 6. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvJustifiedII b
 7. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant b
 8. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII b
 9. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant b
 10. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvRecordCount b
A total of 11 subgoals...
[PROOF STEP]
apply (clarsimp simp: next'_def)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithGII a
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant b
 3. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant a
 4. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvRecordCount a
 5. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvJustifiedII b
 6. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant b
 7. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII b
 8. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant b
 9. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvRecordCount b
 10. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvCapsNonneg b
[PROOF STEP]
apply simp_all [7]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant b
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvRecordCount b
 3. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvCapsNonneg b
[PROOF STEP]
apply (rule invs_imp_InvGlobVacantImpRecordsVacant)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvJustifiedGII b
 2. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvRecordCount b
 3. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvRecordsNonneg b
 4. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvRecordCount b
 5. \<lbrakk>InvJustifiedII a; InvGlobNonposEqVacant a; InvInfoJustifiedWithII a; InvGlobVacantImpRecordsVacant a; InvRecordCount a; InvCapsNonneg a; next_recvupd' a b p q; InvJustifiedGII a; InvJustifiedII b; InvRecordsNonneg a; InvRecordCount b; InvCapsNonneg b; InvJustifiedGII b; InvRecordsNonneg b; InvGlobNonposEqVacant b; InvInfoJustifiedWithII b; InvInfoJustifiedWithGII a; InvInfoJustifiedWithGII b\<rbrakk> \<Longrightarrow> InvCapsNonneg b
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>c0 c1. SafeGlobMono c0 c1 \<and> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1)\<^sup>*\<^sup>* c c1

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>c0 c1. SafeGlobMono c0 c1 \<and> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1)\<^sup>*\<^sup>* c c1
[PROOF STEP]
have trancl_mono: "(\<lambda>c0 c1. SafeGlobMono c0 c1)\<^sup>*\<^sup>* c c1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>c0 c1. SafeGlobMono c0 c1 \<and> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1)\<^sup>*\<^sup>* c c1

goal (1 subgoal):
 1. SafeGlobMono\<^sup>*\<^sup>* c c1
[PROOF STEP]
by (metis (no_types, lifting) rtranclp_all_imp_rel)
[PROOF STATE]
proof (state)
this:
SafeGlobMono\<^sup>*\<^sup>* c c1

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
SafeGlobMono\<^sup>*\<^sup>* c c1
[PROOF STEP]
have vacant_c1: "\<forall>t'\<le>t. zcount (c_glob c1 q) t' = 0"
[PROOF STATE]
proof (prove)
using this:
SafeGlobMono\<^sup>*\<^sup>* c c1

goal (1 subgoal):
 1. \<forall>t'\<le>t. zcount (c_glob c1 q) t' = 0
[PROOF STEP]
by (rule SafeGlobMono_preserves_vacant[OF vacant])
[PROOF STATE]
proof (state)
this:
\<forall>t'\<le>t. zcount (c_glob c1 q) t' = 0

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
have InvMsgInGlob: "InvMsgInGlob c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvMsgInGlob c1
[PROOF STEP]
using rtranclp_invar_conclude_last[OF invs_trancl] assms
[PROOF STATE]
proof (prove)
using this:
InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1
M \<in> set (c_msg c p q)
t \<in>#\<^sub>z M
InvGlobNonposEqVacant c
InvJustifiedII c
InvInfoJustifiedWithII c
InvGlobVacantImpRecordsVacant c
InvRecordCount c
InvCapsNonneg c
InvMsgInGlob c

goal (1 subgoal):
 1. InvMsgInGlob c1
[PROOF STEP]
apply (intro invs_imp_InvMsgInGlob)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithGII c1
 2. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant c1
 3. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant c1
 4. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvRecordCount c1
 5. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvJustifiedII c1
 6. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvCapsNonneg c1
 7. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvRecordsNonneg c1
[PROOF STEP]
using invs_imp_InvInfoJustifiedWithGII InvCapsNonneg_imp_InvRecordsNonneg
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>InvInfoJustifiedWithII ?c; InvJustifiedII ?c; InvCapsNonneg ?c\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithGII ?c
InvCapsNonneg ?c \<Longrightarrow> InvRecordsNonneg ?c

goal (7 subgoals):
 1. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithGII c1
 2. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant c1
 3. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant c1
 4. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvRecordCount c1
 5. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvJustifiedII c1
 6. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvCapsNonneg c1
 7. \<lbrakk>InvJustifiedII c \<and> InvGlobNonposEqVacant c \<and> InvInfoJustifiedWithII c \<and> InvGlobVacantImpRecordsVacant c \<and> InvRecordCount c \<and> InvCapsNonneg c \<Longrightarrow> InvJustifiedII c1 \<and> InvGlobNonposEqVacant c1 \<and> InvInfoJustifiedWithII c1 \<and> InvGlobVacantImpRecordsVacant c1 \<and> InvRecordCount c1 \<and> InvCapsNonneg c1; M \<in> set (c_msg c p q); t \<in>#\<^sub>z M; InvGlobNonposEqVacant c; InvJustifiedII c; InvInfoJustifiedWithII c; InvGlobVacantImpRecordsVacant c; InvRecordCount c; InvCapsNonneg c; InvMsgInGlob c\<rbrakk> \<Longrightarrow> InvRecordsNonneg c1
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
InvMsgInGlob c1

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
have "\<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t'
[PROOF STEP]
using InvMsgInGlob[unfolded InvMsgInGlob_def] c1(2,3) assms(1,2)
[PROOF STATE]
proof (prove)
using this:
\<forall>p q t. c_msg c1 p q \<noteq> [] \<longrightarrow> t \<in>#\<^sub>z hd (c_msg c1 p q) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t')
c_msg c1 p q \<noteq> []
hd (c_msg c1 p q) = M
M \<in> set (c_msg c p q)
t \<in>#\<^sub>z M

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

goal (1 subgoal):
 1. \<not> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t') \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alw_msg_glob: "spec s \<Longrightarrow>
  alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M \<in> set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) s
[PROOF STEP]
apply (frule alw_InvGlobNonposEqVacant)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvGlobNonposEqVacant) s\<rbrakk> \<Longrightarrow> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) s
[PROOF STEP]
apply (frule alw_InvJustifiedII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s\<rbrakk> \<Longrightarrow> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) s
[PROOF STEP]
apply (frule alw_InvInfoJustifiedWithII)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s\<rbrakk> \<Longrightarrow> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) s
[PROOF STEP]
apply (frule alw_InvGlobVacantImpRecordsVacant)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s\<rbrakk> \<Longrightarrow> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) s
[PROOF STEP]
apply (frule alw_InvRecordCount)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s\<rbrakk> \<Longrightarrow> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) s
[PROOF STEP]
apply (frule alw_InvCapsNonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec s; alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s\<rbrakk> \<Longrightarrow> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) s
[PROOF STEP]
apply (drule alw_InvMsgInGlob)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s\<rbrakk> \<Longrightarrow> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) s
[PROOF STEP]
apply (coinduction arbitrary: s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t')) xs \<and> ((\<exists>s. stl xs = s \<and> alw (holds InvGlobNonposEqVacant) s \<and> alw (holds InvJustifiedII) s \<and> alw (holds InvInfoJustifiedWithII) s \<and> alw (holds InvGlobVacantImpRecordsVacant) s \<and> alw (holds InvRecordCount) s \<and> alw (holds InvCapsNonneg) s \<and> alw (holds InvMsgInGlob) s) \<or> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) (stl xs))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s\<rbrakk> \<Longrightarrow> (\<forall>p q t. (\<exists>M\<in>set (c_msg (shd s) p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob (shd s) q) t')) \<and> (alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvJustifiedII) (stl s) \<and> alw (holds InvInfoJustifiedWithII) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<and> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvMsgInGlob) (stl s) \<or> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) (stl s))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s\<rbrakk> \<Longrightarrow> \<forall>p q t. (\<exists>M\<in>set (c_msg (shd s) p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob (shd s) q) t')
 2. \<And>s. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvJustifiedII) (stl s) \<and> alw (holds InvInfoJustifiedWithII) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<and> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvMsgInGlob) (stl s) \<or> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) (stl s)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob (shd s) q) t'
 2. \<And>s. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvJustifiedII) (stl s) \<and> alw (holds InvInfoJustifiedWithII) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<and> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvMsgInGlob) (stl s) \<or> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) (stl s)
[PROOF STEP]
apply (rule invs_imp_msg_in_glob)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> ?M32 s p q t M \<in> set (c_msg (shd s) (?p32 s p q t M) q)
 2. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> t \<in>#\<^sub>z ?M32 s p q t M
 3. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant (shd s)
 4. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvJustifiedII (shd s)
 5. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII (shd s)
 6. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant (shd s)
 7. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvRecordCount (shd s)
 8. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvCapsNonneg (shd s)
 9. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvMsgInGlob (shd s)
 10. \<And>s. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvJustifiedII) (stl s) \<and> alw (holds InvInfoJustifiedWithII) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<and> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvMsgInGlob) (stl s) \<or> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) (stl s)
[PROOF STEP]
apply auto [2]
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant (shd s)
 2. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvJustifiedII (shd s)
 3. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII (shd s)
 4. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant (shd s)
 5. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvRecordCount (shd s)
 6. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvCapsNonneg (shd s)
 7. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvMsgInGlob (shd s)
 8. \<And>s. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvJustifiedII) (stl s) \<and> alw (holds InvInfoJustifiedWithII) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<and> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvMsgInGlob) (stl s) \<or> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) (stl s)
[PROOF STEP]
using holds.elims(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>holds ?x ?xa; \<And>P xs. \<lbrakk>?x = P; ?xa = xs; P (shd xs)\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (8 subgoals):
 1. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvGlobNonposEqVacant (shd s)
 2. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvJustifiedII (shd s)
 3. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvInfoJustifiedWithII (shd s)
 4. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvGlobVacantImpRecordsVacant (shd s)
 5. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvRecordCount (shd s)
 6. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvCapsNonneg (shd s)
 7. \<And>s p q t M. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s; M \<in> set (c_msg (shd s) p q); t \<in>#\<^sub>z M\<rbrakk> \<Longrightarrow> InvMsgInGlob (shd s)
 8. \<And>s. \<lbrakk>alw (holds InvGlobNonposEqVacant) s; alw (holds InvJustifiedII) s; alw (holds InvInfoJustifiedWithII) s; alw (holds InvGlobVacantImpRecordsVacant) s; alw (holds InvRecordCount) s; alw (holds InvCapsNonneg) s; alw (holds InvMsgInGlob) s\<rbrakk> \<Longrightarrow> alw (holds InvGlobNonposEqVacant) (stl s) \<and> alw (holds InvJustifiedII) (stl s) \<and> alw (holds InvInfoJustifiedWithII) (stl s) \<and> alw (holds InvGlobVacantImpRecordsVacant) (stl s) \<and> alw (holds InvRecordCount) (stl s) \<and> alw (holds InvCapsNonneg) (stl s) \<and> alw (holds InvMsgInGlob) (stl s) \<or> alw (holds (\<lambda>c. \<forall>p q t. (\<exists>M\<in>set (c_msg c p q). t \<in>#\<^sub>z M) \<longrightarrow> (\<exists>t'\<le>t. 0 < zcount (c_glob c q) t'))) (stl s)
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma conj_assoc: "(x \<^bold>\<sqinter> y) \<^bold>\<sqinter> z = x \<^bold>\<sqinter> (y \<^bold>\<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<^bold>\<sqinter> y) \<^bold>\<sqinter> z = x \<^bold>\<sqinter> y \<^bold>\<sqinter> z
[PROOF STEP]
by (fact conj.assoc)


[STATEMENT]
lemma conj_commute: "x \<^bold>\<sqinter> y = y \<^bold>\<sqinter> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<sqinter> y = y \<^bold>\<sqinter> x
[PROOF STEP]
by (fact conj.commute)


[STATEMENT]
lemma conj_one_left: "\<^bold>1 \<^bold>\<sqinter> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>1 \<^bold>\<sqinter> x = x
[PROOF STEP]
by (fact conj.left_neutral)


[STATEMENT]
lemma conj_left_absorb: "x \<^bold>\<sqinter> (x \<^bold>\<sqinter> y) = x \<^bold>\<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<sqinter> x \<^bold>\<sqinter> y = x \<^bold>\<sqinter> y
[PROOF STEP]
by (fact conj.left_idem)


[STATEMENT]
lemma conj_absorb: "x \<^bold>\<sqinter> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<sqinter> x = x
[PROOF STEP]
by (fact conj.idem)


[STATEMENT]
lemma disj_assoc: "(x \<^bold>\<squnion> y) \<^bold>\<squnion> z = x \<^bold>\<squnion> (y \<^bold>\<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<^bold>\<squnion> y) \<^bold>\<squnion> z = x \<^bold>\<squnion> y \<^bold>\<squnion> z
[PROOF STEP]
by (fact disj.assoc)


[STATEMENT]
lemma disj_commute: "x \<^bold>\<squnion> y = y \<^bold>\<squnion> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<squnion> y = y \<^bold>\<squnion> x
[PROOF STEP]
by (fact disj.commute)


[STATEMENT]
lemma disj_zero_left: "\<^bold>0 \<^bold>\<squnion> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>0 \<^bold>\<squnion> x = x
[PROOF STEP]
by (fact disj.left_neutral)


[STATEMENT]
lemma disj_left_absorb: "x \<^bold>\<squnion> (x \<^bold>\<squnion> y) = x \<^bold>\<squnion> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<squnion> x \<^bold>\<squnion> y = x \<^bold>\<squnion> y
[PROOF STEP]
by (fact disj.left_idem)


[STATEMENT]
lemma disj_absorb: "x \<^bold>\<squnion> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<squnion> x = x
[PROOF STEP]
by (fact disj.idem)


[STATEMENT]
lemma xor_zero_right: "x \<^bold>\<ominus> \<^bold>0 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<ominus> \<^bold>0 = x
[PROOF STEP]
by (fact xor.comm_neutral)


[STATEMENT]
lemma xor_zero_left: "\<^bold>0 \<^bold>\<ominus> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>0 \<^bold>\<ominus> x = x
[PROOF STEP]
by (fact xor.left_neutral)


[STATEMENT]
lemma complement_mask:
  "complement (2 ^ n - 1) = not (mask n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (2 ^ n - 1) = not (mask n)
[PROOF STEP]
unfolding mask_eq_decr_exp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (2 ^ n - 1) = not (2 ^ n - 1)
[PROOF STEP]
by simp


[STATEMENT]
lemma bit_bshiftr1_iff:
  \<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close>
    for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (or (w div 2) (push_bit (LENGTH('a) - Suc 0) (of_bool b))) n = (b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n))
[PROOF STEP]
by (auto simp add: bit_simps simp flip: bit_Suc)


[STATEMENT]
lemma bit_setBit_iff:
  \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (set_bit m w) n = (m = n \<and> n < LENGTH('a) \<or> bit w n)
[PROOF STEP]
by (auto simp add: bit_simps)


[STATEMENT]
lemma bit_clearBit_iff:
  \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (unset_bit m w) n = (m \<noteq> n \<and> bit w n)
[PROOF STEP]
by (auto simp add: bit_simps)


[STATEMENT]
lemma hidden_unmod: "\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs e) i" and
 "\<And>Vs. hidden Vs i \<Longrightarrow> unmods (compEs\<^sub>1 Vs es) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs e) i) &&& (\<And>Vs. hidden Vs i \<Longrightarrow> unmods (compEs\<^sub>1 Vs es) i)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs e) i) &&& (\<And>Vs. hidden Vs i \<Longrightarrow> unmods (compEs\<^sub>1 Vs es) i)
[PROOF STEP]
proof(induct e and es rule: compE\<^sub>1.induct compEs\<^sub>1.induct)
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>x Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs (new x)) i
 2. \<And>x1 x2 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x2) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (Cast x1 x2)) i
 3. \<And>x Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs (Val x)) i
 4. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; \<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x3) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) i
 5. \<And>x Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs (Var x)) i
 6. \<And>x1 x2 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x2) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1:=x2)) i
 7. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) i
 8. \<And>x1 x2 x3 x4 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; \<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x4) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) i
 9. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; \<And>Vs. hidden Vs i \<Longrightarrow> unmods (compEs\<^sub>1 Vs x3) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) i
 10. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x3) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs {x1:x2; x3}) i
A total of 17 subgoals...
[PROOF STEP]
case TryCatch
[PROOF STATE]
proof (state)
this:
hidden ?Vs i \<Longrightarrow> unmod (compE\<^sub>1 ?Vs x1_) i
hidden ?Vs i \<Longrightarrow> unmod (compE\<^sub>1 ?Vs x4_) i
hidden Vs i

goal (17 subgoals):
 1. \<And>x Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs (new x)) i
 2. \<And>x1 x2 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x2) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (Cast x1 x2)) i
 3. \<And>x Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs (Val x)) i
 4. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; \<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x3) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) i
 5. \<And>x Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs (Var x)) i
 6. \<And>x1 x2 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x2) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1:=x2)) i
 7. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) i
 8. \<And>x1 x2 x3 x4 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; \<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x4) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) i
 9. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; \<And>Vs. hidden Vs i \<Longrightarrow> unmods (compEs\<^sub>1 Vs x3) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) i
 10. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x3) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs {x1:x2; x3}) i
A total of 17 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hidden ?Vs i \<Longrightarrow> unmod (compE\<^sub>1 ?Vs x1_) i
hidden ?Vs i \<Longrightarrow> unmod (compE\<^sub>1 ?Vs x4_) i
hidden Vs i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hidden ?Vs i \<Longrightarrow> unmod (compE\<^sub>1 ?Vs x1_) i
hidden ?Vs i \<Longrightarrow> unmod (compE\<^sub>1 ?Vs x4_) i
hidden Vs i

goal (1 subgoal):
 1. unmod (compE\<^sub>1 Vs (try x1_ catch(x2_ x3_) x4_)) i
[PROOF STEP]
by(simp add:hidden_inacc)(auto simp add:hidden_def)
[PROOF STATE]
proof (state)
this:
unmod (compE\<^sub>1 Vs (try x1_ catch(x2_ x3_) x4_)) i

goal (16 subgoals):
 1. \<And>x Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs (new x)) i
 2. \<And>x1 x2 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x2) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (Cast x1 x2)) i
 3. \<And>x Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs (Val x)) i
 4. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; \<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x3) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) i
 5. \<And>x Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs (Var x)) i
 6. \<And>x1 x2 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x2) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1:=x2)) i
 7. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) i
 8. \<And>x1 x2 x3 x4 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; \<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x4) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) i
 9. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x1) i; \<And>Vs. hidden Vs i \<Longrightarrow> unmods (compEs\<^sub>1 Vs x3) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) i
 10. \<And>x1 x2 x3 Vs. \<lbrakk>\<And>Vs. hidden Vs i \<Longrightarrow> unmod (compE\<^sub>1 Vs x3) i; hidden Vs i\<rbrakk> \<Longrightarrow> unmod (compE\<^sub>1 Vs {x1:x2; x3}) i
A total of 16 subgoals...
[PROOF STEP]
qed (simp_all add:hidden_inacc)