theory CNodeInv_R

lemma ztc_replace_update_final:
  assumes chunk: "mdb_chunked m"
      and  slot: "m x = Some (CTE cap node)"
      and  ztc1: "isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap"
      and  ztc2: "isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'"
      and   unt: "capUntypedPtr cap = capUntypedPtr cap'"
      and  bits: "capBits cap = capBits cap'"
      and distz: "distinct_zombies m"
      and   Fin: "isFinal cap x (option_map cteCap \<circ> m)"
      and valid: "s \<turnstile>' cap" "s \<turnstile>' cap'"
      shows      "mdb_chunked (m (x \<mapsto> CTE cap' node))" proof (rule mdb_chunked_update_final [OF chunk, OF slot]) have cases: "capMasterCap cap = capMasterCap cap'
                  \<or> isZombie cap \<or> isZombie cap'" using bits unt ztc1 ztc2
          invalid_Thread_CNode [OF _ _ valid]
          invalid_Thread_CNode [OF _ _ valid(2) valid(1)] by (auto simp: isCap_simps) have Fin': "\<And>y cte. \<lbrakk> m y = Some cte; y \<noteq> x \<rbrakk> \<Longrightarrow> \<not> sameObjectAs cap (cteCap cte)" using Fin apply (clarsimp simp: isFinal_def) apply (drule_tac x=y in spec) apply (clarsimp simp: sameObjectAs_def3) done show Fin1: "\<And>y cte. \<lbrakk> m y = Some cte; y \<noteq> x \<rbrakk> \<Longrightarrow> \<not> sameRegionAs cap (cteCap cte)" by (clarsimp simp: ztc_sameRegion [OF ztc1] Fin') show capR: "capRange cap = capRange cap'" using unt bits ztc_phys[OF ztc1] ztc_phys[OF ztc2] by (simp add: capRange_def) have capR_neq: "capRange cap' \<noteq> {}" using capAligned_capUntypedPtr [OF valid_capAligned, OF valid(2)] by (clarsimp simp add: ztc_phys [OF ztc2]) have zombie_case_helper:
    "\<And>y cte. \<lbrakk> m y = Some cte; y \<noteq> x; isZombie cap \<rbrakk>
                 \<Longrightarrow> \<not> sameObjectAs cap' (cteCap cte)" apply (clarsimp simp: ztc_sameRegion ztc1 ztc2
                   elim!: sameObjectAsE) apply (rule distinct_zombiesD [OF slot distz], simp_all)[1] apply (drule master_eqE, rule capBits_Master) apply (simp add: bits) apply (drule arg_cong[where f=capUntypedPtr]) apply (simp add: capUntyped_Master unt) apply (drule arg_cong[where f=isUntypedCap]) apply (simp add: isCap_Master) apply (drule arg_cong[where f=isArchPageCap]) apply (clarsimp simp add: isCap_Master) apply (cut_tac ztc2, clarsimp simp: isCap_simps) apply (drule arg_cong[where f=capClass]) apply (simp add: capClass_Master ztc_phys[OF ztc2]) done show Fin2: "\<And>y cte. \<lbrakk> m y = Some cte; y \<noteq> x \<rbrakk> \<Longrightarrow> \<not> sameRegionAs cap' (cteCap cte)" using capR apply clarsimp apply (frule(1) Fin1) apply (rule disjE [OF cases]) apply (clarsimp simp: ztc_sameRegion ztc1 ztc2 sameObjectAs_def3) apply (drule_tac F="\<lambda>cap. (isNullCap cap, isZombie cap,
                                isUntypedCap cap, isArchPageCap cap,
                                capRange cap)" in  master_eqE,
             simp add: isCap_Master capRange_Master del: isNullCap)+ apply (auto simp: isCap_Master capRange_Master)[1] apply (erule disjE) apply (drule(2) zombie_case_helper) apply (simp add: ztc_sameRegion ztc1 ztc2) apply (clarsimp simp: ztc_sameRegion ztc1 ztc2
                   elim!: sameObjectAsE) done have untyped_helper:
    "\<And>cap cap'. \<lbrakk> isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap';
                  sameRegionAs cap cap' \<rbrakk>
                    \<Longrightarrow> isUntypedCap cap \<or> sameRegionAs cap' cap" apply (erule sameRegionAsE) apply (clarsimp simp: ztc_sameRegion sameObjectAs_def3) apply (drule_tac F="\<lambda>cap. (isNullCap cap, isZombie cap,
                                  isUntypedCap cap, isArchPageCap cap,
                                  capRange cap)" in  master_eqE,
               simp add: isCap_Master capRange_Master del: isNullCap)+ apply (auto simp: isCap_Master capRange_Master)[1] apply simp apply (clarsimp simp: isCap_simps)+ done show Fin3: "\<And>y cte. \<lbrakk> m y = Some cte; y \<noteq> x; sameRegionAs (cteCap cte) cap \<rbrakk>
                         \<Longrightarrow> isUntypedCap (cteCap cte)" apply (frule(1) Fin1) apply (drule untyped_helper[OF ztc1]) apply simp done show Fin4: "\<And>y cte. \<lbrakk> m y = Some cte; y \<noteq> x; sameRegionAs (cteCap cte) cap' \<rbrakk>
                         \<Longrightarrow> isUntypedCap (cteCap cte)" apply (frule(1) Fin2) apply (drule untyped_helper[OF ztc2]) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked (m(x \<mapsto> CTE cap' node)) proof (state)
goal (5 subgoals):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap (cteCap cte)
 2. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap cte)
 3. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 4. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 5. capRange cap = capRange cap' proof (prove)
goal (1 subgoal):
 1. capMasterCap cap = capMasterCap cap' \<or> isZombie cap \<or> isZombie cap' proof (prove)
using this:
capBits cap = capBits cap'
global.capUntypedPtr cap = global.capUntypedPtr cap'
isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap
isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'
\<lbrakk>isThreadCap cap; isCNodeCap cap'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'
\<lbrakk>isThreadCap cap'; isCNodeCap cap\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap' \<noteq> global.capUntypedPtr cap

goal (1 subgoal):
 1. capMasterCap cap = capMasterCap cap' \<or> isZombie cap \<or> isZombie cap' proof (state)
this:
capMasterCap cap = capMasterCap cap' \<or> isZombie cap \<or> isZombie cap'

goal (5 subgoals):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap (cteCap cte)
 2. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap cte)
 3. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 4. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 5. capRange cap = capRange cap' proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap cte) proof (prove)
using this:
isFinal cap x (map_option cteCap \<circ> m)

goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; \<not> isUntypedCap cap; \<forall>p' c. (\<exists>z. m p' = Some z \<and> cteCap z = c) \<longrightarrow> x \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c; global.sameObjectAs cap (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; \<not> isUntypedCap cap; global.sameObjectAs cap (cteCap cte); \<forall>c. (\<exists>z. m y = Some z \<and> cteCap z = c) \<longrightarrow> x \<noteq> y \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?y = Some ?cte; ?y \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap (cteCap ?cte)

goal (5 subgoals):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap (cteCap cte)
 2. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap cte)
 3. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 4. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 5. capRange cap = capRange cap' proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap (cteCap cte) proof (state)
this:
\<lbrakk>m ?y = Some ?cte; ?y \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap (cteCap ?cte)

goal (4 subgoals):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap cte)
 2. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 3. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 4. capRange cap = capRange cap' proof (prove)
goal (1 subgoal):
 1. capRange cap = capRange cap' proof (prove)
using this:
global.capUntypedPtr cap = global.capUntypedPtr cap'
capBits cap = capBits cap'
capClass cap = PhysicalClass
capClass cap' = PhysicalClass

goal (1 subgoal):
 1. capRange cap = capRange cap' proof (state)
this:
capRange cap = capRange cap'

goal (3 subgoals):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap cte)
 2. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 3. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. capRange cap' \<noteq> {} proof (prove)
using this:
capClass cap' = PhysicalClass \<Longrightarrow> global.capUntypedPtr cap' \<in> capRange cap'

goal (1 subgoal):
 1. capRange cap' \<noteq> {} proof (state)
this:
capRange cap' \<noteq> {}

goal (3 subgoals):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap cte)
 2. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 3. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap' (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capBits (cteCap cte) = capBits cap
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap
 3. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap cte)
 4. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
 5. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (5 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}; capBits cap' = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> capBits (cteCap cte) = capBits cap
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap
 3. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap cte)
 4. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
 5. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (4 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap cte)
 3. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
 4. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (4 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}; global.capUntypedPtr (capMasterCap cap') = global.capUntypedPtr (capMasterCap (cteCap cte))\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap cte)
 3. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
 4. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (3 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap cte)
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
 3. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (3 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}; isUntypedCap (capMasterCap cap') = isUntypedCap (capMasterCap (cteCap cte))\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap cte)
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
 3. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}; isArchPageCap (capMasterCap cap') = isArchPageCap (capMasterCap (cteCap cte))\<rbrakk> \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; capRange cap' \<noteq> {}; isArchPageCap cap'; isArchPageCap (cteCap cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; isZombie cap; cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}; capClass (capMasterCap cap') = capClass (capMasterCap (cteCap cte))\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?y = Some ?cte; ?y \<noteq> x; isZombie cap\<rbrakk> \<Longrightarrow> \<not> global.sameObjectAs cap' (cteCap ?cte)

goal (3 subgoals):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap cte)
 2. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 3. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap cte) proof (prove)
using this:
capRange cap = capRange cap'

goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); capMasterCap cap = capMasterCap cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); isZombie cap \<or> isZombie cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; cap = capability.NullCap \<or> isZombie cap \<or> isUntypedCap cap \<or> isArchPageCap cap \<and> capRange cap' = {}; capMasterCap cap = capMasterCap (cteCap cte); capMasterCap cap' = capMasterCap (cteCap cte); cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; cteCap cte \<noteq> capability.NullCap; \<not> isZombie (cteCap cte); \<not> isUntypedCap (cteCap cte); isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}; isArchPageCap (cteCap cte) \<longrightarrow> capRange (cteCap cte) \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); isZombie cap \<or> isZombie cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; cap = capability.NullCap \<or> isZombie cap \<or> isUntypedCap cap \<or> isArchPageCap cap \<and> capRange cap' = {}; cap' \<noteq> capability.NullCap; \<not> isZombie cap'; \<not> isUntypedCap cap'; cteCap cte \<noteq> capability.NullCap; \<not> isZombie (cteCap cte); \<not> isUntypedCap (cteCap cte); isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}; isArchPageCap (cteCap cte) \<longrightarrow> capRange (cteCap cte) \<noteq> {}; (isNullCap cap, isZombie cap, isUntypedCap cap, isArchPageCap cap, capRange cap) = (isNullCap (cteCap cte), isZombie (cteCap cte), isUntypedCap (cteCap cte), isArchPageCap (cteCap cte), capRange (cteCap cte)); (isNullCap cap', isZombie cap', isUntypedCap cap', isArchPageCap cap', capRange cap') = (isNullCap (cteCap cte), isZombie (cteCap cte), isUntypedCap (cteCap cte), isArchPageCap (cteCap cte), capRange (cteCap cte))\<rbrakk> \<Longrightarrow> False
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); isZombie cap \<or> isZombie cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); isZombie cap \<or> isZombie cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); isZombie cap\<rbrakk> \<Longrightarrow> False
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); isZombie cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); isZombie cap; \<not> global.sameObjectAs cap' (cteCap cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); isZombie cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; capRange cap = capRange cap'; global.sameRegionAs cap' (cteCap cte); \<not> global.sameRegionAs cap (cteCap cte); isZombie cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?y = Some ?cte; ?y \<noteq> x\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs cap' (cteCap ?cte)

goal (2 subgoals):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 2. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap proof (prove)
goal (4 subgoals):
 1. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 2. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 3. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 4. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap proof (prove)
goal (4 subgoals):
 1. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capMasterCap cap = capMasterCap cap'; cap \<noteq> capability.NullCap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {})
 2. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 3. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 4. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap proof (prove)
goal (4 subgoals):
 1. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; cap \<noteq> capability.NullCap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap; (isNullCap cap, isZombie cap, isUntypedCap cap, isArchPageCap cap, capRange cap) = (isNullCap cap', isZombie cap', isUntypedCap cap', isArchPageCap cap', capRange cap')\<rbrakk> \<Longrightarrow> cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {})
 2. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 3. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 4. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap proof (prove)
goal (3 subgoals):
 1. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 2. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 3. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap proof (prove)
goal (2 subgoals):
 1. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap
 2. \<And>cap cap'. \<lbrakk>isCNodeCap cap' \<or> isThreadCap cap' \<or> isZombie cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> isUntypedCap cap \<or> global.sameRegionAs cap' cap proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>isCNodeCap ?cap' \<or> isThreadCap ?cap' \<or> isZombie ?cap'; global.sameRegionAs ?cap ?cap'\<rbrakk> \<Longrightarrow> isUntypedCap ?cap \<or> global.sameRegionAs ?cap' ?cap

goal (2 subgoals):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 2. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; global.sameRegionAs (cteCap cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; global.sameRegionAs (cteCap cte) cap; \<not> global.sameRegionAs cap (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; \<not> global.sameRegionAs cap (cteCap cte); isUntypedCap (cteCap cte) \<or> global.sameRegionAs cap (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?y = Some ?cte; ?y \<noteq> x; global.sameRegionAs (cteCap ?cte) cap\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap ?cte)

goal (1 subgoal):
 1. \<And>xa cte. \<lbrakk>m xa = Some cte; xa \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; global.sameRegionAs (cteCap cte) cap'; \<not> global.sameRegionAs cap' (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; y \<noteq> x; \<not> global.sameRegionAs cap' (cteCap cte); isUntypedCap (cteCap cte) \<or> global.sameRegionAs cap' (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?y = Some ?cte; ?y \<noteq> x; global.sameRegionAs (cteCap ?cte) cap'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap ?cte)

goal:
No subgoals!