theory ArchCNodeInv_AI

lemma same_object_as_def2:
  "same_object_as cp cp' = (cap_master_cap cp = cap_master_cap cp'
                                \<and> \<not> cp = cap.NullCap \<and> \<not> is_untyped_cap cp
                                \<and> \<not> is_zombie cp
                                \<and> (is_arch_cap cp \<longrightarrow>
                                     (case the_arch_cap cp of arch_cap.PageCap d x rs sz v
                                              \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1
                                          | _ \<Rightarrow> True)))" apply (simp add: same_object_as_def is_cap_simps split: cap.split) apply (auto simp: cap_master_cap_def bits_of_def
             split: arch_cap.split_asm) apply (auto split: arch_cap.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_object_as cp cp' = (cap_master_cap cp = cap_master_cap cp' \<and> cp \<noteq> NullCap \<and> \<not> is_untyped_cap cp \<and> \<not> is_zombie cp \<and> (is_arch_cap cp \<longrightarrow> (case the_arch_cap cp of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) proof (prove)
goal (1 subgoal):
 1. (cp' = NullCap \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap NullCap) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap NullCap) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap NullCap) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap NullCap) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap NullCap) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap NullCap) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap NullCap) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap NullCap) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap NullCap \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (\<forall>x21 x22 x23 x24. cp' = UntypedCap x21 x22 x23 x24 \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap (UntypedCap x21 x22 x23 x24)) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap (UntypedCap x21 x22 x23 x24)) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap (UntypedCap x21 x22 x23 x24)) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap (UntypedCap x21 x22 x23 x24)) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap (UntypedCap x21 x22 x23 x24)) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap (UntypedCap x21 x22 x23 x24)) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap (UntypedCap x21 x22 x23 x24)) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap (UntypedCap x21 x22 x23 x24)) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap (UntypedCap x21 x22 x23 x24) \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (\<forall>x31 x32 x33. cp' = EndpointCap x31 x32 x33 \<longrightarrow> (\<forall>x31a x32a x33a. cp = EndpointCap x31a x32a x33a \<longrightarrow> (x31 = x31a) = (cap_master_cap (EndpointCap x31a x32a x33a) = cap_master_cap (EndpointCap x31 x32 x33))) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap (EndpointCap x31 x32 x33)) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap (EndpointCap x31 x32 x33)) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap (EndpointCap x31 x32 x33)) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap (EndpointCap x31 x32 x33)) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap (EndpointCap x31 x32 x33)) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap (EndpointCap x31 x32 x33)) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap (EndpointCap x31 x32 x33)) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap (EndpointCap x31 x32 x33) \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (\<forall>x41 x42 x43. cp' = NotificationCap x41 x42 x43 \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap (NotificationCap x41 x42 x43)) \<and> (\<forall>x41a x42a x43a. cp = NotificationCap x41a x42a x43a \<longrightarrow> (x41 = x41a) = (cap_master_cap (NotificationCap x41a x42a x43a) = cap_master_cap (NotificationCap x41 x42 x43))) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap (NotificationCap x41 x42 x43)) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap (NotificationCap x41 x42 x43)) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap (NotificationCap x41 x42 x43)) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap (NotificationCap x41 x42 x43)) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap (NotificationCap x41 x42 x43)) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap (NotificationCap x41 x42 x43)) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap (NotificationCap x41 x42 x43) \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (\<forall>x51 x52 x53. cp' = ReplyCap x51 x52 x53 \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap (ReplyCap x51 x52 x53)) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap (ReplyCap x51 x52 x53)) \<and> (\<forall>x51a x52a x53a. cp = ReplyCap x51a x52a x53a \<longrightarrow> (x51 = x51a) = (cap_master_cap (ReplyCap x51a x52a x53a) = cap_master_cap (ReplyCap x51 x52 x53))) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap (ReplyCap x51 x52 x53)) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap (ReplyCap x51 x52 x53)) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap (ReplyCap x51 x52 x53)) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap (ReplyCap x51 x52 x53)) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap (ReplyCap x51 x52 x53)) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap (ReplyCap x51 x52 x53) \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (\<forall>x61 x62 x63. cp' = CNodeCap x61 x62 x63 \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap (CNodeCap x61 x62 x63)) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap (CNodeCap x61 x62 x63)) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap (CNodeCap x61 x62 x63)) \<and> (\<forall>x61a x62a x63a. cp = CNodeCap x61a x62a x63a \<longrightarrow> (x61 = x61a \<and> bits_of (CNodeCap x61 x62 x63) = x62a) = (cap_master_cap (CNodeCap x61a x62a x63a) = cap_master_cap (CNodeCap x61 x62 x63))) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap (CNodeCap x61 x62 x63)) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap (CNodeCap x61 x62 x63)) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap (CNodeCap x61 x62 x63)) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap (CNodeCap x61 x62 x63)) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap (CNodeCap x61 x62 x63) \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (\<forall>x7. cp' = ThreadCap x7 \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap (ThreadCap x7)) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap (ThreadCap x7)) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap (ThreadCap x7)) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap (ThreadCap x7)) \<and> (\<forall>x7a. cp = ThreadCap x7a \<longrightarrow> (x7 = x7a) = (cap_master_cap (ThreadCap x7a) = cap_master_cap (ThreadCap x7))) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap (ThreadCap x7)) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap (ThreadCap x7)) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap (ThreadCap x7)) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap (ThreadCap x7) \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (cp' = DomainCap \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap DomainCap) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap DomainCap) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap DomainCap) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap DomainCap) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap DomainCap) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap DomainCap) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap DomainCap) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap DomainCap \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (cp' = IRQControlCap \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap IRQControlCap) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap IRQControlCap) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap IRQControlCap) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap IRQControlCap) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap IRQControlCap) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap IRQControlCap) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap IRQControlCap) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap IRQControlCap \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (\<forall>x10. cp' = IRQHandlerCap x10 \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap (IRQHandlerCap x10)) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap (IRQHandlerCap x10)) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap (IRQHandlerCap x10)) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap (IRQHandlerCap x10)) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap (IRQHandlerCap x10)) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap (IRQHandlerCap x10)) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap (IRQHandlerCap x10)) \<and> (\<forall>x10a. cp = IRQHandlerCap x10a \<longrightarrow> (x10 = x10a) = (cap_master_cap (IRQHandlerCap x10a) = cap_master_cap (IRQHandlerCap x10))) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap (IRQHandlerCap x10) \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (\<forall>x111 x112 x113. cp' = Zombie x111 x112 x113 \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap (Zombie x111 x112 x113)) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap (Zombie x111 x112 x113)) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap (Zombie x111 x112 x113)) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap (Zombie x111 x112 x113)) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap (Zombie x111 x112 x113)) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap (Zombie x111 x112 x113)) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap (Zombie x111 x112 x113)) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap (Zombie x111 x112 x113)) \<and> (\<forall>x12. cp = ArchObjectCap x12 \<longrightarrow> cap_master_cap (ArchObjectCap x12) = cap_master_cap (Zombie x111 x112 x113) \<longrightarrow> \<not> (case x12 of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True))) \<and> (\<forall>x12. cp' = ArchObjectCap x12 \<longrightarrow> (\<forall>x31 x32 x33. cp = EndpointCap x31 x32 x33 \<longrightarrow> cap_master_cap (EndpointCap x31 x32 x33) \<noteq> cap_master_cap (ArchObjectCap x12)) \<and> (\<forall>x41 x42 x43. cp = NotificationCap x41 x42 x43 \<longrightarrow> cap_master_cap (NotificationCap x41 x42 x43) \<noteq> cap_master_cap (ArchObjectCap x12)) \<and> (\<forall>x51 x52 x53. cp = ReplyCap x51 x52 x53 \<longrightarrow> cap_master_cap (ReplyCap x51 x52 x53) \<noteq> cap_master_cap (ArchObjectCap x12)) \<and> (\<forall>x61 x62 x63. cp = CNodeCap x61 x62 x63 \<longrightarrow> cap_master_cap (CNodeCap x61 x62 x63) \<noteq> cap_master_cap (ArchObjectCap x12)) \<and> (\<forall>x7. cp = ThreadCap x7 \<longrightarrow> cap_master_cap (ThreadCap x7) \<noteq> cap_master_cap (ArchObjectCap x12)) \<and> (cp = DomainCap \<longrightarrow> cap_master_cap DomainCap \<noteq> cap_master_cap (ArchObjectCap x12)) \<and> (cp = IRQControlCap \<longrightarrow> cap_master_cap IRQControlCap \<noteq> cap_master_cap (ArchObjectCap x12)) \<and> (\<forall>x10. cp = IRQHandlerCap x10 \<longrightarrow> cap_master_cap (IRQHandlerCap x10) \<noteq> cap_master_cap (ArchObjectCap x12)) \<and> (\<forall>x12a. cp = ArchObjectCap x12a \<longrightarrow> (case x12a of PageCap dev ref x pgsz xa \<Rightarrow> case x12 of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as x12a x12 | _ \<Rightarrow> arch_same_region_as x12a x12) = (cap_master_cap (ArchObjectCap x12a) = cap_master_cap (ArchObjectCap x12) \<and> (case x12a of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True)))) proof (prove)
goal (4 subgoals):
 1. \<And>x12 x11 x12b. \<lbrakk>cp' = ArchObjectCap x12; cp = ArchObjectCap (ASIDPoolCap x11 x12b); arch_same_region_as (ASIDPoolCap x11 x12b) x12\<rbrakk> \<Longrightarrow> ASIDPoolCap x11 0 = (case x12 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> x12 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None)
 2. \<And>x12. \<lbrakk>cp' = ArchObjectCap x12; cp = ArchObjectCap ASIDControlCap; arch_same_region_as ASIDControlCap x12\<rbrakk> \<Longrightarrow> ASIDControlCap = (case x12 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> x12 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None)
 3. \<And>x12 x41 x42. \<lbrakk>cp' = ArchObjectCap x12; cp = ArchObjectCap (PageTableCap x41 x42); arch_same_region_as (PageTableCap x41 x42) x12\<rbrakk> \<Longrightarrow> PageTableCap x41 None = (case x12 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> x12 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None)
 4. \<And>x12 x51 x52. \<lbrakk>cp' = ArchObjectCap x12; cp = ArchObjectCap (PageDirectoryCap x51 x52); arch_same_region_as (PageDirectoryCap x51 x52) x12\<rbrakk> \<Longrightarrow> PageDirectoryCap x51 None = (case x12 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> x12 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) proof (prove)
goal:
No subgoals!