theory CSpace_I

lemma distinct_zombies_seperateE:
  "\<lbrakk> distinct_zombies m;
      \<And>y cte. m y = Some cte \<Longrightarrow> x \<noteq> y
                \<Longrightarrow> \<not> isUntypedCap (cteCap cte)
                \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
                \<Longrightarrow> capClass (cteCap cte) = PhysicalClass
                \<Longrightarrow> capClass (cteCap cte') = PhysicalClass
                \<Longrightarrow> capUntypedPtr (cteCap cte) = capUntypedPtr (cteCap cte')
                \<Longrightarrow> capBits (cteCap cte) = capBits (cteCap cte') \<Longrightarrow> False \<rbrakk>
       \<Longrightarrow> distinct_zombies (m (x \<mapsto> cte'))" apply (simp add: distinct_zombies_def distinct_zombie_caps_def) apply (intro impI allI conjI) apply (clarsimp simp: isZombie_capClass) apply fastforce apply clarsimp apply (frule isZombie_capClass) apply (subgoal_tac "\<not> isUntypedCap (cteCap z) \<and> \<not> isArchPageCap (cteCap z)") apply fastforce apply (clarsimp simp: isCap_simps) apply clarsimp apply (erule notE[rotated], elim allE, erule mp) apply auto[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; 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 (1 subgoal):
 1. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> \<forall>ptr. (ptr = x \<longrightarrow> (\<forall>ptr'. ptr' \<noteq> x \<longrightarrow> (\<forall>cap'. (\<exists>z. m ptr' = Some z \<and> cteCap z = cap') \<and> isZombie (cteCap cte') \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits (cteCap cte') = capBits cap' \<longrightarrow> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap'))) \<and> (ptr \<noteq> x \<longrightarrow> (\<forall>ptr'. (ptr' = x \<longrightarrow> (\<forall>cap. (\<exists>z. m ptr = Some z \<and> cteCap z = cap) \<and> isZombie cap \<and> capClass (cteCap cte') = PhysicalClass \<and> \<not> isUntypedCap (cteCap cte') \<and> \<not> isArchPageCap (cteCap cte') \<and> capBits cap = capBits (cteCap cte') \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr (cteCap cte'))) \<and> (ptr' \<noteq> x \<longrightarrow> (\<forall>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')))) proof (prove)
goal (3 subgoals):
 1. \<And>ptr ptr' cap'. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr = x; ptr' \<noteq> x; (\<exists>z. m ptr' = Some z \<and> cteCap z = cap') \<and> isZombie (cteCap cte') \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits (cteCap cte') = capBits cap'\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap'
 2. \<And>ptr ptr' cap. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' = x; (\<exists>z. m ptr = Some z \<and> cteCap z = cap) \<and> isZombie cap \<and> capClass (cteCap cte') = PhysicalClass \<and> \<not> isUntypedCap (cteCap cte') \<and> \<not> isArchPageCap (cteCap cte') \<and> capBits cap = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr (cteCap cte')
 3. \<And>ptr ptr' cap cap'. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; (\<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'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (3 subgoals):
 1. \<And>ptr' z. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap z); capBits (cteCap cte) = capBits (cteCap z)\<rbrakk> \<Longrightarrow> False; ptr' \<noteq> x; isZombie (cteCap cte'); m ptr' = Some z; capClass (cteCap z) = PhysicalClass; \<not> isUntypedCap (cteCap z); \<not> isArchPageCap (cteCap z); capBits (cteCap cte') = capBits (cteCap z); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap z)\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' cap. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' = x; (\<exists>z. m ptr = Some z \<and> cteCap z = cap) \<and> isZombie cap \<and> capClass (cteCap cte') = PhysicalClass \<and> \<not> isUntypedCap (cteCap cte') \<and> \<not> isArchPageCap (cteCap cte') \<and> capBits cap = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr (cteCap cte')
 3. \<And>ptr ptr' cap cap'. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; (\<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'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (2 subgoals):
 1. \<And>ptr ptr' cap. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' = x; (\<exists>z. m ptr = Some z \<and> cteCap z = cap) \<and> isZombie cap \<and> capClass (cteCap cte') = PhysicalClass \<and> \<not> isUntypedCap (cteCap cte') \<and> \<not> isArchPageCap (cteCap cte') \<and> capBits cap = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr (cteCap cte')
 2. \<And>ptr ptr' cap cap'. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; (\<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'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (2 subgoals):
 1. \<And>ptr z. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<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; ptr \<noteq> x; isZombie (cteCap z); m ptr = Some z; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capBits (cteCap z) = capBits (cteCap cte'); global.capUntypedPtr (cteCap z) = global.capUntypedPtr (cteCap cte')\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' cap cap'. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; (\<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'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (2 subgoals):
 1. \<And>ptr z. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<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; ptr \<noteq> x; isZombie (cteCap z); m ptr = Some z; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capBits (cteCap z) = capBits (cteCap cte'); global.capUntypedPtr (cteCap z) = global.capUntypedPtr (cteCap cte'); capClass (cteCap z) = PhysicalClass\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' cap cap'. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; (\<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'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (3 subgoals):
 1. \<And>ptr z. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<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; ptr \<noteq> x; isZombie (cteCap z); m ptr = Some z; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capBits (cteCap z) = capBits (cteCap cte'); global.capUntypedPtr (cteCap z) = global.capUntypedPtr (cteCap cte'); capClass (cteCap z) = PhysicalClass; \<not> isUntypedCap (cteCap z) \<and> \<not> isArchPageCap (cteCap z)\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr z. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<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; ptr \<noteq> x; isZombie (cteCap z); m ptr = Some z; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capBits (cteCap z) = capBits (cteCap cte'); global.capUntypedPtr (cteCap z) = global.capUntypedPtr (cteCap cte'); capClass (cteCap z) = PhysicalClass\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap z) \<and> \<not> isArchPageCap (cteCap z)
 3. \<And>ptr ptr' cap cap'. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; (\<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'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (2 subgoals):
 1. \<And>ptr z. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<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; ptr \<noteq> x; isZombie (cteCap z); m ptr = Some z; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capBits (cteCap z) = capBits (cteCap cte'); global.capUntypedPtr (cteCap z) = global.capUntypedPtr (cteCap cte'); capClass (cteCap z) = PhysicalClass\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap z) \<and> \<not> isArchPageCap (cteCap z)
 2. \<And>ptr ptr' cap cap'. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; (\<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'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' cap cap'. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; (\<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'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' z za. \<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'; \<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; m ptr = Some z; ptr \<noteq> ptr'; m ptr' = Some za; isZombie (cteCap z); capClass (cteCap za) = PhysicalClass; \<not> isUntypedCap (cteCap za); \<not> isArchPageCap (cteCap za); capBits (cteCap z) = capBits (cteCap za); global.capUntypedPtr (cteCap z) = global.capUntypedPtr (cteCap za)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' z za. \<lbrakk>\<And>y cte. \<lbrakk>m y = Some cte; x \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap cte') = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); capBits (cteCap cte) = capBits (cteCap cte')\<rbrakk> \<Longrightarrow> False; ptr \<noteq> x; ptr' \<noteq> x; m ptr = Some z; ptr \<noteq> ptr'; m ptr' = Some za; isZombie (cteCap z); capClass (cteCap za) = PhysicalClass; \<not> isUntypedCap (cteCap za); \<not> isArchPageCap (cteCap za); capBits (cteCap z) = capBits (cteCap za)\<rbrakk> \<Longrightarrow> (\<exists>zb. m (?ptr150 ptr ptr' z za) = Some zb \<and> cteCap zb = cteCap z) \<and> (\<exists>zb. m (?ptr'151 ptr ptr' z za) = Some zb \<and> cteCap zb = cteCap za) \<and> ?ptr150 ptr ptr' z za \<noteq> ?ptr'151 ptr ptr' z za \<and> isZombie (cteCap z) \<and> capClass (cteCap za) = PhysicalClass \<and> \<not> isUntypedCap (cteCap za) \<and> \<not> isArchPageCap (cteCap za) \<and> capBits (cteCap z) = capBits (cteCap za) proof (prove)
goal:
No subgoals!