theory CSpaceInv_AI

lemma zombies_final_def2:
  "zombies_final = (\<lambda>s. \<forall>p p' cap cap'. (cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s
                                          \<and> (obj_refs cap \<inter> obj_refs cap' \<noteq> {}) \<and> p \<noteq> p')
                                      \<longrightarrow> (\<not> is_zombie cap \<and> \<not> is_zombie cap'))" unfolding zombies_final_def apply (rule ext) apply (rule iffI) apply (intro allI impI conjI notI) apply (elim conjE) apply (simp only: simp_thms conj_commute final_cap_at_eq cte_wp_at_def) apply (elim allE, drule mp, rule exI, erule(1) conjI) apply (elim exE conjE) apply (drule spec, drule mp, rule conjI, erule not_sym) apply simp apply (clarsimp simp: gen_obj_refs_Int) apply (elim conjE) apply (simp only: simp_thms conj_commute final_cap_at_eq cte_wp_at_def) apply (elim allE, drule mp, rule exI, erule(1) conjI) apply (elim exE conjE) apply (drule spec, drule mp, erule conjI) apply simp apply (clarsimp simp: Int_commute gen_obj_refs_Int) apply (clarsimp simp: final_cap_at_eq cte_wp_at_def
                        zombie_has_refs gen_obj_refs_Int
                        zombie_cap_irqs
                  simp del: split_paired_Ex) apply (rule ccontr) apply (elim allE, erule impE, (erule conjI)+) apply (clarsimp simp: is_cap_simps) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombies_final = (\<lambda>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap') proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s) = (\<lambda>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap') proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s) = (\<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap') proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s \<Longrightarrow> \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'
 2. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (3 subgoals):
 1. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p'; is_zombie cap\<rbrakk> \<Longrightarrow> False
 2. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p'; is_zombie cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (3 subgoals):
 1. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; is_zombie cap; cte_wp_at ((=) cap) p s; cte_wp_at ((=) cap') p' s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'\<rbrakk> \<Longrightarrow> False
 2. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p'; is_zombie cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (3 subgoals):
 1. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. (\<exists>cap. is_zombie cap \<and> fst (get_cap p s) = {(cap, s)}) \<longrightarrow> (\<exists>cp. fst (get_cap p s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. p' \<noteq> p \<and> (\<exists>cap. fst (get_cap p' s) = {(cap, s)}) \<longrightarrow> (\<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p' s) = {(cap, s)}))); is_zombie cap; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'\<rbrakk> \<Longrightarrow> False
 2. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p'; is_zombie cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (3 subgoals):
 1. \<And>s p p' cap cap'. \<lbrakk>is_zombie cap; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; \<exists>cp. fst (get_cap p s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. p' \<noteq> p \<and> (\<exists>cap. fst (get_cap p' s) = {(cap, s)}) \<longrightarrow> (\<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p' s) = {(cap, s)}))\<rbrakk> \<Longrightarrow> False
 2. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p'; is_zombie cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (3 subgoals):
 1. \<And>s p p' cap cap' cp. \<lbrakk>is_zombie cap; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; fst (get_cap p s) = {(cp, s)}; gen_obj_refs cp \<noteq> {}; \<forall>p'. p' \<noteq> p \<and> (\<exists>cap. fst (get_cap p' s) = {(cap, s)}) \<longrightarrow> (\<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p' s) = {(cap, s)})\<rbrakk> \<Longrightarrow> False
 2. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p'; is_zombie cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (4 subgoals):
 1. \<And>s p p' cap cap' cp. \<lbrakk>is_zombie cap; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; fst (get_cap p s) = {(cp, s)}; gen_obj_refs cp \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap. fst (get_cap p' s) = {(cap, s)}
 2. \<And>s p p' cap cap' cp. \<lbrakk>is_zombie cap; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; fst (get_cap p s) = {(cp, s)}; gen_obj_refs cp \<noteq> {}; \<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p' s) = {(cap, s)}\<rbrakk> \<Longrightarrow> False
 3. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p'; is_zombie cap'\<rbrakk> \<Longrightarrow> False
 4. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (3 subgoals):
 1. \<And>s p p' cap cap' cp. \<lbrakk>is_zombie cap; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; fst (get_cap p s) = {(cp, s)}; gen_obj_refs cp \<noteq> {}; \<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p' s) = {(cap, s)}\<rbrakk> \<Longrightarrow> False
 2. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p'; is_zombie cap'\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (2 subgoals):
 1. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p'; is_zombie cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (2 subgoals):
 1. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; is_zombie cap'; cte_wp_at ((=) cap) p s; cte_wp_at ((=) cap') p' s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (2 subgoals):
 1. \<And>s p p' cap cap'. \<lbrakk>\<forall>p. (\<exists>cap. is_zombie cap \<and> fst (get_cap p s) = {(cap, s)}) \<longrightarrow> (\<exists>cp. fst (get_cap p s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. p' \<noteq> p \<and> (\<exists>cap. fst (get_cap p' s) = {(cap, s)}) \<longrightarrow> (\<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p' s) = {(cap, s)}))); is_zombie cap'; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (2 subgoals):
 1. \<And>s p p' cap cap'. \<lbrakk>is_zombie cap'; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; \<exists>cp. fst (get_cap p' s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'a. p'a \<noteq> p' \<and> (\<exists>cap. fst (get_cap p'a s) = {(cap, s)}) \<longrightarrow> (\<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p'a s) = {(cap, s)}))\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (2 subgoals):
 1. \<And>s p p' cap cap' cp. \<lbrakk>is_zombie cap'; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; fst (get_cap p' s) = {(cp, s)}; gen_obj_refs cp \<noteq> {}; \<forall>p'a. p'a \<noteq> p' \<and> (\<exists>cap. fst (get_cap p'a s) = {(cap, s)}) \<longrightarrow> (\<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p'a s) = {(cap, s)})\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (3 subgoals):
 1. \<And>s p p' cap cap' cp. \<lbrakk>is_zombie cap'; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; fst (get_cap p' s) = {(cp, s)}; gen_obj_refs cp \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap. fst (get_cap p s) = {(cap, s)}
 2. \<And>s p p' cap cap' cp. \<lbrakk>is_zombie cap'; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; fst (get_cap p' s) = {(cp, s)}; gen_obj_refs cp \<noteq> {}; \<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p s) = {(cap, s)}\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (2 subgoals):
 1. \<And>s p p' cap cap' cp. \<lbrakk>is_zombie cap'; fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; obj_refs cap \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; fst (get_cap p' s) = {(cp, s)}; gen_obj_refs cp \<noteq> {}; \<exists>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {} \<and> fst (get_cap p s) = {(cap, s)}\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>p p' cap cap'. cte_wp_at ((=) cap) p s \<and> cte_wp_at ((=) cap') p' s \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap' \<Longrightarrow> \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap aa ba capa. \<lbrakk>\<forall>a b aa ba cap cap'. fst (get_cap (a, b) s) = {(cap, s)} \<and> fst (get_cap (aa, ba) s) = {(cap', s)} \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; fst (get_cap (a, b) s) = {(cap, s)}; is_zombie cap; aa = a \<longrightarrow> ba \<noteq> b; fst (get_cap (aa, ba) s) = {(capa, s)}\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<and> arch_gen_refs cap \<inter> arch_gen_refs capa = {} proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap aa ba capa. \<lbrakk>\<forall>a b aa ba cap cap'. fst (get_cap (a, b) s) = {(cap, s)} \<and> fst (get_cap (aa, ba) s) = {(cap', s)} \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; fst (get_cap (a, b) s) = {(cap, s)}; is_zombie cap; aa = a \<longrightarrow> ba \<noteq> b; fst (get_cap (aa, ba) s) = {(capa, s)}; \<not> (obj_refs cap \<inter> obj_refs capa = {} \<and> arch_gen_refs cap \<inter> arch_gen_refs capa = {})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap aa ba capa. \<lbrakk>is_zombie cap; aa = a \<longrightarrow> ba \<noteq> b; \<not> (obj_refs cap \<inter> obj_refs capa = {} \<and> arch_gen_refs cap \<inter> arch_gen_refs capa = {})\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs capa \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba)
 2. \<And>s a b cap aa ba capa. \<lbrakk>fst (get_cap (a, b) s) = {(cap, s)}; is_zombie cap; aa = a \<longrightarrow> ba \<noteq> b; fst (get_cap (aa, ba) s) = {(capa, s)}; \<not> (obj_refs cap \<inter> obj_refs capa = {} \<and> arch_gen_refs cap \<inter> arch_gen_refs capa = {}); \<not> is_zombie cap \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap aa ba capa. \<lbrakk>fst (get_cap (a, b) s) = {(cap, s)}; is_zombie cap; aa = a \<longrightarrow> ba \<noteq> b; fst (get_cap (aa, ba) s) = {(capa, s)}; \<not> (obj_refs cap \<inter> obj_refs capa = {} \<and> arch_gen_refs cap \<inter> arch_gen_refs capa = {}); \<not> is_zombie cap \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!