theory Tcb_DR

lemma arch_same_obj_as_lift:
  "\<lbrakk>cap_aligned a;is_arch_cap a;ca = transform_cap a;cb=transform_cap b\<rbrakk>
  \<Longrightarrow> cdl_same_arch_obj_as (ca) (cb) = same_object_as a b" apply (clarsimp simp:is_arch_cap_def split:cap.split_asm) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (simp add:same_object_as_def) apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (clarsimp simp:cdl_same_arch_obj_as_def)+ apply (simp add:same_object_as_def) apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply ((clarsimp simp:cdl_same_arch_obj_as_def)+)[5] apply (simp add:same_object_as_def) apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (fastforce simp:cdl_same_arch_obj_as_def cap_aligned_def)+ apply (simp add:same_object_as_def) apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (fastforce simp:cdl_same_arch_obj_as_def cap_aligned_def)+ apply (simp add:same_object_as_def) apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (fastforce simp:cdl_same_arch_obj_as_def cap_aligned_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_aligned a; is_arch_cap a; ca = transform_cap a; cb = transform_cap b\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as ca cb = same_object_as a b proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>ca = transform_cap (ArchObjectCap x12); cb = transform_cap b; cap_aligned (ArchObjectCap x12); a = ArchObjectCap x12\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap x12)) (transform_cap b) = same_object_as (ArchObjectCap x12) b proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (5 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 2. \<And>arch_cap. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 4. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 5. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (5 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>ca = AsidPoolCap x11 (fst (transform_asid x12)); cb = transform_cap b; cap_aligned (ArchObjectCap (ASIDPoolCap x11 x12)); a = ArchObjectCap (ASIDPoolCap x11 x12); arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (AsidPoolCap x11 (fst (transform_asid x12))) (transform_cap b) = (case b of ArchObjectCap x \<Rightarrow> same_aobject_as (ASIDPoolCap x11 x12) x | _ \<Rightarrow> same_region_as (ArchObjectCap (ASIDPoolCap x11 x12)) b)
 2. \<And>arch_cap. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 4. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 5. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 x12a. \<lbrakk>ca = AsidPoolCap x11 (fst (transform_asid x12)); cb = transform_cap (ArchObjectCap x12a); cap_aligned (ArchObjectCap (ASIDPoolCap x11 x12)); a = ArchObjectCap (ASIDPoolCap x11 x12); b = ArchObjectCap x12a\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap x12a) of AsidPoolCap y xa \<Rightarrow> y = x11 | _ \<Rightarrow> False) = arch_same_region_as (ASIDPoolCap x11 x12) x12a
 2. \<And>arch_cap. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 4. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 5. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 arch_cap. \<lbrakk>ca = AsidPoolCap x11 (fst (transform_asid x12)); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (ASIDPoolCap x11 x12)); a = ArchObjectCap (ASIDPoolCap x11 x12); b = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidPoolCap y xa \<Rightarrow> y = x11 | _ \<Rightarrow> False) = arch_same_region_as (ASIDPoolCap x11 x12) arch_cap
 2. \<And>arch_cap. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 4. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 5. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (9 subgoals):
 1. \<And>x11 x12 arch_cap x11a x12a. \<lbrakk>ca = AsidPoolCap x11 (fst (transform_asid x12)); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (ASIDPoolCap x11 x12)); a = ArchObjectCap (ASIDPoolCap x11 x12); b = ArchObjectCap arch_cap; arch_cap = ASIDPoolCap x11a x12a\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidPoolCap y xa \<Rightarrow> y = x11 | _ \<Rightarrow> False) = arch_same_region_as (ASIDPoolCap x11 x12) arch_cap
 2. \<And>x11 x12 arch_cap. \<lbrakk>ca = AsidPoolCap x11 (fst (transform_asid x12)); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (ASIDPoolCap x11 x12)); a = ArchObjectCap (ASIDPoolCap x11 x12); b = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidPoolCap y xa \<Rightarrow> y = x11 | _ \<Rightarrow> False) = arch_same_region_as (ASIDPoolCap x11 x12) arch_cap
 3. \<And>x11 x12 arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = AsidPoolCap x11 (fst (transform_asid x12)); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (ASIDPoolCap x11 x12)); a = ArchObjectCap (ASIDPoolCap x11 x12); b = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidPoolCap y xa \<Rightarrow> y = x11 | _ \<Rightarrow> False) = arch_same_region_as (ASIDPoolCap x11 x12) arch_cap
 4. \<And>x11 x12 arch_cap x41 x42. \<lbrakk>ca = AsidPoolCap x11 (fst (transform_asid x12)); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (ASIDPoolCap x11 x12)); a = ArchObjectCap (ASIDPoolCap x11 x12); b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidPoolCap y xa \<Rightarrow> y = x11 | _ \<Rightarrow> False) = arch_same_region_as (ASIDPoolCap x11 x12) arch_cap
 5. \<And>x11 x12 arch_cap x51 x52. \<lbrakk>ca = AsidPoolCap x11 (fst (transform_asid x12)); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (ASIDPoolCap x11 x12)); a = ArchObjectCap (ASIDPoolCap x11 x12); b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidPoolCap y xa \<Rightarrow> y = x11 | _ \<Rightarrow> False) = arch_same_region_as (ASIDPoolCap x11 x12) arch_cap
 6. \<And>arch_cap. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 7. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 8. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 9. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ca = AsidControlCap; cb = transform_cap b; cap_aligned (ArchObjectCap ASIDControlCap); a = ArchObjectCap ASIDControlCap\<rbrakk> \<Longrightarrow> (case transform_cap b of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False) = same_object_as (ArchObjectCap ASIDControlCap) b
 2. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 4. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ca = AsidControlCap; cb = transform_cap b; cap_aligned (ArchObjectCap ASIDControlCap); a = ArchObjectCap ASIDControlCap\<rbrakk> \<Longrightarrow> (case transform_cap b of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False) = (case b of ArchObjectCap x \<Rightarrow> same_aobject_as ASIDControlCap x | _ \<Rightarrow> same_region_as (ArchObjectCap ASIDControlCap) b)
 2. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 4. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (4 subgoals):
 1. \<And>x12. \<lbrakk>ca = AsidControlCap; cb = transform_cap (ArchObjectCap x12); cap_aligned (ArchObjectCap ASIDControlCap); a = ArchObjectCap ASIDControlCap; b = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap x12) of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False) = arch_same_region_as ASIDControlCap x12
 2. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 4. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (4 subgoals):
 1. \<And>arch_cap. \<lbrakk>ca = AsidControlCap; cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap ASIDControlCap); a = ArchObjectCap ASIDControlCap; b = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False) = arch_same_region_as ASIDControlCap arch_cap
 2. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 4. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (8 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>ca = AsidControlCap; cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap ASIDControlCap); a = ArchObjectCap ASIDControlCap; b = ArchObjectCap arch_cap; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False) = arch_same_region_as ASIDControlCap arch_cap
 2. \<And>arch_cap. \<lbrakk>ca = AsidControlCap; cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap ASIDControlCap); a = ArchObjectCap ASIDControlCap; b = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False) = arch_same_region_as ASIDControlCap arch_cap
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = AsidControlCap; cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap ASIDControlCap); a = ArchObjectCap ASIDControlCap; b = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False) = arch_same_region_as ASIDControlCap arch_cap
 4. \<And>arch_cap x41 x42. \<lbrakk>ca = AsidControlCap; cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap ASIDControlCap); a = ArchObjectCap ASIDControlCap; b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False) = arch_same_region_as ASIDControlCap arch_cap
 5. \<And>arch_cap x51 x52. \<lbrakk>ca = AsidControlCap; cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap ASIDControlCap); a = ArchObjectCap ASIDControlCap; b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False) = arch_same_region_as ASIDControlCap arch_cap
 6. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 7. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 8. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (3 subgoals):
 1. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 2. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (3 subgoals):
 1. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cb = transform_cap b; cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); a = ArchObjectCap (PageCap x31 x32 x33 x34 x35); arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35)) (transform_cap b) = (case b of ArchObjectCap x \<Rightarrow> same_aobject_as (PageCap x31 x32 x33 x34 x35) x | _ \<Rightarrow> same_region_as (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) b)
 2. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x12. \<lbrakk>ca = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cb = transform_cap (ArchObjectCap x12); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); a = ArchObjectCap (PageCap x31 x32 x33 x34 x35); b = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap x12) of FrameCap dev' rb x sb xa xb \<Rightarrow> rb = x32 \<and> sb = pageBitsForSize x34 \<and> x31 = dev' | _ \<Rightarrow> False) = (case x12 of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (x31, x32, x34) = (dev', ref', pgsz') \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 | _ \<Rightarrow> arch_same_region_as (PageCap x31 x32 x33 x34 x35) x12)
 2. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 arch_cap. \<lbrakk>ca = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); a = ArchObjectCap (PageCap x31 x32 x33 x34 x35); b = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of FrameCap dev' rb x sb xa xb \<Rightarrow> rb = x32 \<and> sb = pageBitsForSize x34 \<and> x31 = dev' | _ \<Rightarrow> False) = (case arch_cap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (x31, x32, x34) = (dev', ref', pgsz') \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 | _ \<Rightarrow> arch_same_region_as (PageCap x31 x32 x33 x34 x35) arch_cap)
 2. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 3. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (7 subgoals):
 1. \<And>x31 x32 x33 x34 x35 arch_cap x11 x12. \<lbrakk>ca = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); a = ArchObjectCap (PageCap x31 x32 x33 x34 x35); b = ArchObjectCap arch_cap; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of FrameCap dev' rb x sb xa xb \<Rightarrow> rb = x32 \<and> sb = pageBitsForSize x34 \<and> x31 = dev' | _ \<Rightarrow> False) = (case arch_cap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (x31, x32, x34) = (dev', ref', pgsz') \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 | _ \<Rightarrow> arch_same_region_as (PageCap x31 x32 x33 x34 x35) arch_cap)
 2. \<And>x31 x32 x33 x34 x35 arch_cap. \<lbrakk>ca = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); a = ArchObjectCap (PageCap x31 x32 x33 x34 x35); b = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of FrameCap dev' rb x sb xa xb \<Rightarrow> rb = x32 \<and> sb = pageBitsForSize x34 \<and> x31 = dev' | _ \<Rightarrow> False) = (case arch_cap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (x31, x32, x34) = (dev', ref', pgsz') \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 | _ \<Rightarrow> arch_same_region_as (PageCap x31 x32 x33 x34 x35) arch_cap)
 3. \<And>x31 x32 x33 x34 x35 arch_cap x31a x32a x33a x34a x35a. \<lbrakk>ca = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); a = ArchObjectCap (PageCap x31 x32 x33 x34 x35); b = ArchObjectCap arch_cap; arch_cap = PageCap x31a x32a x33a x34a x35a\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of FrameCap dev' rb x sb xa xb \<Rightarrow> rb = x32 \<and> sb = pageBitsForSize x34 \<and> x31 = dev' | _ \<Rightarrow> False) = (case arch_cap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (x31, x32, x34) = (dev', ref', pgsz') \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 | _ \<Rightarrow> arch_same_region_as (PageCap x31 x32 x33 x34 x35) arch_cap)
 4. \<And>x31 x32 x33 x34 x35 arch_cap x41 x42. \<lbrakk>ca = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); a = ArchObjectCap (PageCap x31 x32 x33 x34 x35); b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of FrameCap dev' rb x sb xa xb \<Rightarrow> rb = x32 \<and> sb = pageBitsForSize x34 \<and> x31 = dev' | _ \<Rightarrow> False) = (case arch_cap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (x31, x32, x34) = (dev', ref', pgsz') \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 | _ \<Rightarrow> arch_same_region_as (PageCap x31 x32 x33 x34 x35) arch_cap)
 5. \<And>x31 x32 x33 x34 x35 arch_cap x51 x52. \<lbrakk>ca = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); a = ArchObjectCap (PageCap x31 x32 x33 x34 x35); b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of FrameCap dev' rb x sb xa xb \<Rightarrow> rb = x32 \<and> sb = pageBitsForSize x34 \<and> x31 = dev' | _ \<Rightarrow> False) = (case arch_cap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (x31, x32, x34) = (dev', ref', pgsz') \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 | _ \<Rightarrow> arch_same_region_as (PageCap x31 x32 x33 x34 x35) arch_cap)
 6. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 7. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap x41 x42. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b
 2. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap x41 x42. \<lbrakk>ca = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cb = transform_cap b; cap_aligned (ArchObjectCap (arch_cap.PageTableCap x41 x42)); a = ArchObjectCap (arch_cap.PageTableCap x41 x42); arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (cdl_cap.PageTableCap x41 Real (transform_mapping x42)) (transform_cap b) = (case b of ArchObjectCap x \<Rightarrow> same_aobject_as (arch_cap.PageTableCap x41 x42) x | _ \<Rightarrow> same_region_as (ArchObjectCap (arch_cap.PageTableCap x41 x42)) b)
 2. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x12. \<lbrakk>ca = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cb = transform_cap (ArchObjectCap x12); cap_aligned (ArchObjectCap (arch_cap.PageTableCap x41 x42)); a = ArchObjectCap (arch_cap.PageTableCap x41 x42); b = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap x12) of cdl_cap.PageTableCap b x xa \<Rightarrow> b = x41 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageTableCap x41 x42) x12
 2. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 arch_cap. \<lbrakk>ca = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageTableCap x41 x42)); a = ArchObjectCap (arch_cap.PageTableCap x41 x42); b = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageTableCap b x xa \<Rightarrow> b = x41 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageTableCap x41 x42) arch_cap
 2. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (6 subgoals):
 1. \<And>x41 x42 arch_cap x11 x12. \<lbrakk>ca = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageTableCap x41 x42)); a = ArchObjectCap (arch_cap.PageTableCap x41 x42); b = ArchObjectCap arch_cap; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageTableCap b x xa \<Rightarrow> b = x41 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageTableCap x41 x42) arch_cap
 2. \<And>x41 x42 arch_cap. \<lbrakk>ca = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageTableCap x41 x42)); a = ArchObjectCap (arch_cap.PageTableCap x41 x42); b = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageTableCap b x xa \<Rightarrow> b = x41 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageTableCap x41 x42) arch_cap
 3. \<And>x41 x42 arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageTableCap x41 x42)); a = ArchObjectCap (arch_cap.PageTableCap x41 x42); b = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageTableCap b x xa \<Rightarrow> b = x41 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageTableCap x41 x42) arch_cap
 4. \<And>x41 x42 arch_cap x41a x42a. \<lbrakk>ca = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageTableCap x41 x42)); a = ArchObjectCap (arch_cap.PageTableCap x41 x42); b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41a x42a\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageTableCap b x xa \<Rightarrow> b = x41 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageTableCap x41 x42) arch_cap
 5. \<And>x41 x42 arch_cap x51 x52. \<lbrakk>ca = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageTableCap x41 x42)); a = ArchObjectCap (arch_cap.PageTableCap x41 x42); b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageTableCap b x xa \<Rightarrow> b = x41 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageTableCap x41 x42) arch_cap
 6. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap x51 x52. \<lbrakk>ca = transform_cap (ArchObjectCap arch_cap); cb = transform_cap b; cap_aligned (ArchObjectCap arch_cap); a = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (transform_cap (ArchObjectCap arch_cap)) (transform_cap b) = same_object_as (ArchObjectCap arch_cap) b proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap x51 x52. \<lbrakk>ca = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cb = transform_cap b; cap_aligned (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); a = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cdl_same_arch_obj_as (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52)) (transform_cap b) = (case b of ArchObjectCap x \<Rightarrow> same_aobject_as (arch_cap.PageDirectoryCap x51 x52) x | _ \<Rightarrow> same_region_as (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)) b) proof (prove)
goal (1 subgoal):
 1. \<And>x51 x52 x12. \<lbrakk>ca = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cb = transform_cap (ArchObjectCap x12); cap_aligned (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); a = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); b = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap x12) of cdl_cap.PageDirectoryCap b x xa \<Rightarrow> b = x51 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageDirectoryCap x51 x52) x12 proof (prove)
goal (1 subgoal):
 1. \<And>x51 x52 arch_cap. \<lbrakk>ca = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); a = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); b = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageDirectoryCap b x xa \<Rightarrow> b = x51 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageDirectoryCap x51 x52) arch_cap proof (prove)
goal (5 subgoals):
 1. \<And>x51 x52 arch_cap x11 x12. \<lbrakk>ca = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); a = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); b = ArchObjectCap arch_cap; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageDirectoryCap b x xa \<Rightarrow> b = x51 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageDirectoryCap x51 x52) arch_cap
 2. \<And>x51 x52 arch_cap. \<lbrakk>ca = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); a = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); b = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageDirectoryCap b x xa \<Rightarrow> b = x51 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageDirectoryCap x51 x52) arch_cap
 3. \<And>x51 x52 arch_cap x31 x32 x33 x34 x35. \<lbrakk>ca = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); a = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); b = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageDirectoryCap b x xa \<Rightarrow> b = x51 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageDirectoryCap x51 x52) arch_cap
 4. \<And>x51 x52 arch_cap x41 x42. \<lbrakk>ca = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); a = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageDirectoryCap b x xa \<Rightarrow> b = x51 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageDirectoryCap x51 x52) arch_cap
 5. \<And>x51 x52 arch_cap x51a x52a. \<lbrakk>ca = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cb = transform_cap (ArchObjectCap arch_cap); cap_aligned (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); a = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51a x52a\<rbrakk> \<Longrightarrow> (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.PageDirectoryCap b x xa \<Rightarrow> b = x51 | _ \<Rightarrow> False) = arch_same_region_as (arch_cap.PageDirectoryCap x51 x52) arch_cap proof (prove)
goal:
No subgoals!