theory CSpace_I

lemma distinct_zombies_copyE:
  "\<lbrakk> distinct_zombies m; m x = Some cte;
       capClass (cteCap cte') = PhysicalClass
               \<Longrightarrow> isZombie (cteCap cte) = isZombie (cteCap cte');
       \<lbrakk> capClass (cteCap cte') = PhysicalClass; isUntypedCap (cteCap cte) \<rbrakk>
               \<Longrightarrow> isUntypedCap (cteCap cte');
       \<lbrakk> capClass (cteCap cte') = PhysicalClass; isArchPageCap (cteCap cte) \<rbrakk>
               \<Longrightarrow> isArchPageCap (cteCap cte');
       isZombie (cteCap cte') \<Longrightarrow> x = y;
       capClass (cteCap cte') = PhysicalClass \<Longrightarrow>
               capBits (cteCap cte') = capBits (cteCap cte);
       capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass;
       capClass (cteCap cte') = PhysicalClass \<Longrightarrow>
            capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \<rbrakk>
        \<Longrightarrow> distinct_zombies (m (y \<mapsto> cte'))" apply (simp add: distinct_zombies_def distinct_zombie_caps_def) apply clarsimp apply (intro allI conjI impI) apply clarsimp apply (drule_tac x=y in spec) apply (drule_tac x=ptr' in spec) apply (clarsimp simp: isCap_simps) apply clarsimp apply (drule_tac x=ptr in spec) apply (drule_tac x=x in spec) apply clarsimp apply auto[1] apply clarsimp apply (drule_tac x=ptr in spec) apply (drule_tac x=ptr' in spec) apply auto[1] done

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