theory CSpaceInv_AI

lemma set_cap_zombies:
  "\<lbrace>\<lambda>s. zombies_final s
         \<and> cte_wp_at (\<lambda>cap'. \<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>p'.
                              (p \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' s)
                                \<longrightarrow> (cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap)) p s\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (wp set_cap_zombies') apply (clarsimp simp: cte_wp_at_def elim!: nonemptyE) apply (subgoal_tac "x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa") prefer 2 apply (rule impI) apply (drule(3) zombies_finalD2) apply clarsimp apply blast apply simp apply (simp only: ex_zombie_refs_def2 split: if_split_asm) apply simp apply (drule bspec, simp) apply (elim allE, erule disjE, erule(1) notE) apply simp apply simp apply (drule(1) bspec, elim allE, erule disjE, erule(1) notE) apply simp apply simp apply (erule impCE) apply (drule bspec, simp) apply (elim allE, erule impE, erule conjI) apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. zombies_final s \<and> cte_wp_at (\<lambda>cap'. \<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) p s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<and> cte_wp_at (\<lambda>cap'. \<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) p s \<Longrightarrow> zombies_final s \<and> cte_wp_at (\<lambda>cap'. \<forall>p' cap''. cte_wp_at ((=) cap'') p' s \<and> p \<noteq> p' \<and> obj_refs cap \<inter> obj_refs cap'' \<noteq> {} \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'') p s proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'' proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap''
 2. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''\<rbrakk> \<Longrightarrow> x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''\<rbrakk> \<Longrightarrow> x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa
 2. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'' proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa
 2. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'' proof (prove)
goal (3 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> obj_refs cap'' \<noteq> {}
 2. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa; \<not> is_zombie capa \<and> \<not> is_zombie cap''\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa
 3. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'' proof (prove)
goal (3 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa; obj_refs capa \<inter> obj_refs cap'' = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa; \<not> is_zombie capa \<and> \<not> is_zombie cap''\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa
 3. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'' proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa; \<not> is_zombie capa \<and> \<not> is_zombie cap''\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa
 2. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'' proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b cap'' x. \<lbrakk>zombies_final s; fst (get_cap p s) = {(capa, s)}; \<forall>r\<in>ex_zombie_refs (cap, capa). \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> is_zombie cap; fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'' proof (prove)
goal (3 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> True; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; is_zombie capa; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> True\<rbrakk> \<Longrightarrow> \<not> True \<and> \<not> is_zombie cap''
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> False; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; \<not> is_zombie capa; \<forall>r\<in>obj_refs cap. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> True\<rbrakk> \<Longrightarrow> \<not> True \<and> \<not> is_zombie cap''
 3. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> False\<rbrakk> \<Longrightarrow> \<not> False \<and> \<not> is_zombie cap'' proof (prove)
goal (3 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<notin> obj_refs capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; is_zombie capa; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p = (a, b) \<or> (\<forall>cap. fst (get_cap (a, b) s) = {(cap, s)} \<longrightarrow> r \<notin> obj_refs cap)\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> False; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; \<not> is_zombie capa; \<forall>r\<in>obj_refs cap. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> True\<rbrakk> \<Longrightarrow> \<not> True \<and> \<not> is_zombie cap''
 3. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> False\<rbrakk> \<Longrightarrow> \<not> False \<and> \<not> is_zombie cap'' proof (prove)
goal (3 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<notin> obj_refs capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; is_zombie capa; \<forall>a b. p = (a, b) \<or> (\<forall>cap. fst (get_cap (a, b) s) = {(cap, s)} \<longrightarrow> x \<notin> obj_refs cap)\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> False; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; \<not> is_zombie capa; \<forall>r\<in>obj_refs cap. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> True\<rbrakk> \<Longrightarrow> \<not> True \<and> \<not> is_zombie cap''
 3. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> False\<rbrakk> \<Longrightarrow> \<not> False \<and> \<not> is_zombie cap'' proof (prove)
goal (3 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<notin> obj_refs capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; is_zombie capa; \<forall>cap. fst (get_cap (a, b) s) = {(cap, s)} \<longrightarrow> x \<notin> obj_refs cap\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> False; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; \<not> is_zombie capa; \<forall>r\<in>obj_refs cap. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> True\<rbrakk> \<Longrightarrow> \<not> True \<and> \<not> is_zombie cap''
 3. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> False\<rbrakk> \<Longrightarrow> \<not> False \<and> \<not> is_zombie cap'' proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> False; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; \<not> is_zombie capa; \<forall>r\<in>obj_refs cap. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> True\<rbrakk> \<Longrightarrow> \<not> True \<and> \<not> is_zombie cap''
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> False\<rbrakk> \<Longrightarrow> \<not> False \<and> \<not> is_zombie cap'' proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; \<not> is_zombie capa; \<forall>r\<in>obj_refs cap. \<forall>a b. p = (a, b) \<or> (\<forall>cap. fst (get_cap (a, b) s) = {(cap, s)} \<longrightarrow> r \<notin> obj_refs cap)\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> False\<rbrakk> \<Longrightarrow> \<not> False \<and> \<not> is_zombie cap'' proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; is_zombie cap; \<not> is_zombie capa; \<forall>cap. fst (get_cap (a, b) s) = {(cap, s)} \<longrightarrow> x \<notin> obj_refs cap\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> False\<rbrakk> \<Longrightarrow> \<not> False \<and> \<not> is_zombie cap'' proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap) \<and> \<not> False\<rbrakk> \<Longrightarrow> \<not> False \<and> \<not> is_zombie cap'' proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; x \<in> obj_refs capa \<longrightarrow> \<not> is_zombie cap'' \<and> \<not> is_zombie capa; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap)\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap); x \<notin> obj_refs capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap''
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap); \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; x \<notin> obj_refs capa; \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> x \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap)\<rbrakk> \<Longrightarrow> \<not> is_zombie cap''
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap); \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' proof (prove)
goal (3 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; x \<notin> obj_refs capa\<rbrakk> \<Longrightarrow> \<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> x \<in> obj_refs cap
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; x \<notin> obj_refs capa; \<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap\<rbrakk> \<Longrightarrow> \<not> is_zombie cap''
 3. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap); \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; x \<notin> obj_refs capa; \<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap\<rbrakk> \<Longrightarrow> \<not> is_zombie cap''
 2. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap); \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b cap'' x. \<lbrakk>fst (get_cap (a, b) s) = {(cap'', s)}; p \<noteq> (a, b); x \<in> obj_refs cap; x \<in> obj_refs cap''; zombies_final s; fst (get_cap p s) = {(capa, s)}; \<not> is_zombie cap; \<forall>r\<in>obj_refs cap - obj_refs capa. \<forall>a b. p \<noteq> (a, b) \<and> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> r \<in> obj_refs cap) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> \<not> is_zombie cap); \<not> is_zombie cap'' \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap'' proof (prove)
goal:
No subgoals!