theory CNodeInv_R

lemma distinct_zombies_seperate_if_zombiedE:
  "\<lbrakk> distinct_zombies m; m x = Some cte;
        isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte');
        isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte');
        capClass (cteCap cte') = capClass (cteCap cte);
        capBits (cteCap cte') = capBits (cteCap cte);
        capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte);
        \<And>y cte''. \<lbrakk> m y = Some cte''; x \<noteq> y;
                    isZombie (cteCap cte'); \<not> isZombie (cteCap cte);
                    \<not> isZombie (cteCap cte'');
                    \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte'');
                    capClass (cteCap cte'') = PhysicalClass;
                    capUntypedPtr (cteCap cte'') = capUntypedPtr (cteCap cte);
                    capBits (cteCap cte'') = capBits (cteCap cte)
                        \<rbrakk> \<Longrightarrow> False    \<rbrakk>
          \<Longrightarrow> distinct_zombies (m (x \<mapsto> cte'))" apply (cases "isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte)") apply (subgoal_tac "\<forall>y cte''. m y = Some cte'' \<longrightarrow> y \<noteq> x
                            \<longrightarrow> capUntypedPtr (cteCap cte'') = capUntypedPtr (cteCap cte)
                            \<longrightarrow> capBits (cteCap cte'') = capBits (cteCap cte)
                            \<longrightarrow> \<not> isZombie (cteCap cte'')") apply (erule distinct_zombies_seperateE) apply (drule_tac x=y in spec, clarsimp) apply auto[1] apply (clarsimp simp add: distinct_zombies_def distinct_zombie_caps_def) apply (drule_tac x=y in spec, drule_tac x=x in spec) apply (frule isZombie_capClass[where cap="cteCap cte'"]) apply clarsimp apply (auto simp: isCap_simps)[1] apply clarsimp apply (erule(7) distinct_zombies_unzombieE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte)\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte'))
 2. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte); \<forall>y cte''. m y = Some cte'' \<longrightarrow> y \<noteq> x \<longrightarrow> global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte) \<longrightarrow> capBits (cteCap cte'') = capBits (cteCap cte) \<longrightarrow> \<not> isZombie (cteCap cte'')\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte'))
 2. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte)\<rbrakk> \<Longrightarrow> \<forall>y cte''. m y = Some cte'' \<longrightarrow> y \<noteq> x \<longrightarrow> global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte) \<longrightarrow> capBits (cteCap cte'') = capBits (cteCap cte) \<longrightarrow> \<not> isZombie (cteCap cte'')
 3. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (3 subgoals):
 1. \<And>y ctea. \<lbrakk>m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte); \<forall>y cte''. m y = Some cte'' \<longrightarrow> y \<noteq> x \<longrightarrow> global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte) \<longrightarrow> capBits (cteCap cte'') = capBits (cteCap cte) \<longrightarrow> \<not> isZombie (cteCap cte''); m y = Some ctea; x \<noteq> y; \<not> isUntypedCap (cteCap ctea); \<not> isArchPageCap (cteCap ctea); capClass (cteCap ctea) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap ctea) = global.capUntypedPtr (cteCap cte'); capBits (cteCap ctea) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte)\<rbrakk> \<Longrightarrow> \<forall>y cte''. m y = Some cte'' \<longrightarrow> y \<noteq> x \<longrightarrow> global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte) \<longrightarrow> capBits (cteCap cte'') = capBits (cteCap cte) \<longrightarrow> \<not> isZombie (cteCap cte'')
 3. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (3 subgoals):
 1. \<And>y ctea. \<lbrakk>m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); PhysicalClass = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; m y = Some ctea; x \<noteq> y; \<not> isUntypedCap (cteCap ctea); \<not> isArchPageCap (cteCap ctea); capClass (cteCap ctea) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap ctea) = global.capUntypedPtr (cteCap cte); capBits (cteCap ctea) = capBits (cteCap cte); \<not> isZombie (cteCap ctea); isZombie (cteCap cte'); \<not> isZombie (cteCap cte)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte)\<rbrakk> \<Longrightarrow> \<forall>y cte''. m y = Some cte'' \<longrightarrow> y \<noteq> x \<longrightarrow> global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte) \<longrightarrow> capBits (cteCap cte'') = capBits (cteCap cte) \<longrightarrow> \<not> isZombie (cteCap cte'')
 3. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte)\<rbrakk> \<Longrightarrow> \<forall>y cte''. m y = Some cte'' \<longrightarrow> y \<noteq> x \<longrightarrow> global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte) \<longrightarrow> capBits (cteCap cte'') = capBits (cteCap cte) \<longrightarrow> \<not> isZombie (cteCap cte'')
 2. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (2 subgoals):
 1. \<And>y cte''. \<lbrakk>\<forall>ptr ptr' cap cap'. (\<exists>z. m ptr = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m ptr' = Some z \<and> cteCap z = cap') \<and> ptr \<noteq> ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); m y = Some cte''; y \<noteq> x; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte); isZombie (cteCap cte'')\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (2 subgoals):
 1. \<And>y cte''. \<lbrakk>m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); m y = Some cte''; y \<noteq> x; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte); isZombie (cteCap cte''); \<forall>cap cap'. (\<exists>z. m y = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m x = Some z \<and> cteCap z = cap') \<and> y \<noteq> x \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (2 subgoals):
 1. \<And>y cte''. \<lbrakk>m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); m y = Some cte''; y \<noteq> x; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte); isZombie (cteCap cte''); \<forall>cap cap'. (\<exists>z. m y = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m x = Some z \<and> cteCap z = cap') \<and> y \<noteq> x \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (2 subgoals):
 1. \<And>y cte''. \<lbrakk>m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); PhysicalClass = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); m y = Some cte''; y \<noteq> x; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte); isZombie (cteCap cte''); isUntypedCap (cteCap cte) \<or> isArchPageCap (cteCap cte); capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<And>y cte''. \<lbrakk>m y = Some cte''; x \<noteq> y; isZombie (cteCap cte'); \<not> isZombie (cteCap cte); \<not> isZombie (cteCap cte''); \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); capClass (cteCap cte'') = PhysicalClass; global.capUntypedPtr (cteCap cte'') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte'') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False; \<not> (isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; m x = Some cte; isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); isZombie (cteCap cte') \<longrightarrow> isZombie (cteCap cte)\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) proof (prove)
goal:
No subgoals!