theory ExampleSystem

lemma s2_caps_of_state :
  "caps_of_state s2 p = Some cap \<Longrightarrow>
     cap = NullCap \<or>
     (p,cap) \<in>
       { ((6::obj_ref,(the_nat_to_bl_10 1)),  ThreadCap 3079),
         ((6::obj_ref,(the_nat_to_bl_10 2)),  CNodeCap 6 undefined undefined),
         ((6::obj_ref,(the_nat_to_bl_10 3)),  ArchObjectCap (PageDirectoryCap 3063 (Some asid2_3063))),
         ((6::obj_ref,(the_nat_to_bl_10 4)),  CNodeCap 5 undefined undefined),
         ((7::obj_ref,(the_nat_to_bl_10 1)),  ThreadCap 3080),
         ((7::obj_ref,(the_nat_to_bl_10 2)),  CNodeCap 7 undefined undefined),
         ((7::obj_ref,(the_nat_to_bl_10 3)),  ArchObjectCap (PageDirectoryCap 3065 (Some asid2_3065))),
         ((7::obj_ref,(the_nat_to_bl_10 4)),  CNodeCap 5 undefined undefined),
         ((3079::obj_ref, (tcb_cnode_index 0)), CNodeCap 6 undefined undefined ),
         ((3079::obj_ref, (tcb_cnode_index 1)), ArchObjectCap (PageDirectoryCap 3063 (Some asid2_3063))),
         ((3079::obj_ref, (tcb_cnode_index 2)), ReplyCap 3079 True {AllowGrant,AllowWrite}),
         ((3079::obj_ref, (tcb_cnode_index 3)), NullCap),
         ((3079::obj_ref, (tcb_cnode_index 4)), NullCap),
         ((3080::obj_ref, (tcb_cnode_index 0)), CNodeCap 7 undefined undefined ),
         ((3080::obj_ref, (tcb_cnode_index 1)), ArchObjectCap (PageDirectoryCap 3065 (Some asid2_3065))),
         ((3080::obj_ref, (tcb_cnode_index 2)), ReplyCap 3080 True {AllowGrant,AllowWrite}),
         ((3080::obj_ref, (tcb_cnode_index 3)), NullCap),
         ((3080::obj_ref, (tcb_cnode_index 4)), NullCap)} " apply (insert caps2_7_well_formed) apply (insert caps2_6_well_formed) apply (simp add: caps_of_state_cte_wp_at cte_wp_at_cases s2_def kh2_def kh2_obj_def) apply (case_tac p, clarsimp) apply (clarsimp simp: cte_wp_at_cases split: if_splits) apply (clarsimp simp: tcb_cap_cases_def split: if_splits)+ apply (clarsimp simp: caps2_7_def split: if_splits) apply (clarsimp simp: caps2_6_def cte_wp_at_cases  split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s2 p = Some cap \<Longrightarrow> cap = NullCap \<or> (p, cap) \<in> {((6, the_nat_to_bl_10 1), ThreadCap 0xC07), ((6, the_nat_to_bl_10 2), CNodeCap 6 undefined undefined), ((6, the_nat_to_bl_10 3), ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063))), ((6, the_nat_to_bl_10 4), CNodeCap 5 undefined undefined), ((7, the_nat_to_bl_10 1), ThreadCap 0xC08), ((7, the_nat_to_bl_10 2), CNodeCap 7 undefined undefined), ((7, the_nat_to_bl_10 3), ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065))), ((7, the_nat_to_bl_10 4), CNodeCap 5 undefined undefined), ((0xC07, tcb_cnode_index 0), CNodeCap 6 undefined undefined), ((0xC07, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063))), ((0xC07, tcb_cnode_index 2), ReplyCap 0xC07 True {AllowGrant, AllowWrite}), ((0xC07, tcb_cnode_index 3), NullCap), ((0xC07, tcb_cnode_index 4), NullCap), ((0xC08, tcb_cnode_index 0), CNodeCap 7 undefined undefined), ((0xC08, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065))), ((0xC08, tcb_cnode_index 2), ReplyCap 0xC08 True {AllowGrant, AllowWrite}), ((0xC08, tcb_cnode_index 3), NullCap), ((0xC08, tcb_cnode_index 4), NullCap)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s2 p = Some cap; well_formed_cnode_n 10 caps2_7\<rbrakk> \<Longrightarrow> cap = NullCap \<or> (p, cap) \<in> {((6, the_nat_to_bl_10 1), ThreadCap 0xC07), ((6, the_nat_to_bl_10 2), CNodeCap 6 undefined undefined), ((6, the_nat_to_bl_10 3), ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063))), ((6, the_nat_to_bl_10 4), CNodeCap 5 undefined undefined), ((7, the_nat_to_bl_10 1), ThreadCap 0xC08), ((7, the_nat_to_bl_10 2), CNodeCap 7 undefined undefined), ((7, the_nat_to_bl_10 3), ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065))), ((7, the_nat_to_bl_10 4), CNodeCap 5 undefined undefined), ((0xC07, tcb_cnode_index 0), CNodeCap 6 undefined undefined), ((0xC07, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063))), ((0xC07, tcb_cnode_index 2), ReplyCap 0xC07 True {AllowGrant, AllowWrite}), ((0xC07, tcb_cnode_index 3), NullCap), ((0xC07, tcb_cnode_index 4), NullCap), ((0xC08, tcb_cnode_index 0), CNodeCap 7 undefined undefined), ((0xC08, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065))), ((0xC08, tcb_cnode_index 2), ReplyCap 0xC08 True {AllowGrant, AllowWrite}), ((0xC08, tcb_cnode_index 3), NullCap), ((0xC08, tcb_cnode_index 4), NullCap)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s2 p = Some cap; well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6\<rbrakk> \<Longrightarrow> cap = NullCap \<or> (p, cap) \<in> {((6, the_nat_to_bl_10 1), ThreadCap 0xC07), ((6, the_nat_to_bl_10 2), CNodeCap 6 undefined undefined), ((6, the_nat_to_bl_10 3), ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063))), ((6, the_nat_to_bl_10 4), CNodeCap 5 undefined undefined), ((7, the_nat_to_bl_10 1), ThreadCap 0xC08), ((7, the_nat_to_bl_10 2), CNodeCap 7 undefined undefined), ((7, the_nat_to_bl_10 3), ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065))), ((7, the_nat_to_bl_10 4), CNodeCap 5 undefined undefined), ((0xC07, tcb_cnode_index 0), CNodeCap 6 undefined undefined), ((0xC07, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063))), ((0xC07, tcb_cnode_index 2), ReplyCap 0xC07 True {AllowGrant, AllowWrite}), ((0xC07, tcb_cnode_index 3), NullCap), ((0xC07, tcb_cnode_index 4), NullCap), ((0xC08, tcb_cnode_index 0), CNodeCap 7 undefined undefined), ((0xC08, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065))), ((0xC08, tcb_cnode_index 2), ReplyCap 0xC08 True {AllowGrant, AllowWrite}), ((0xC08, tcb_cnode_index 3), NullCap), ((0xC08, tcb_cnode_index 4), NullCap)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if \<exists>cap. (\<exists>sz fun. (if fst p = 0xC08 then Some (TCB \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if fst p = 0xC07 then Some (TCB \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if fst p = 0xC05 then Some (ArchObj (PageTable pt2_3077)) else if fst p = 0xC00 then Some (ArchObj (PageTable pt2_3072)) else if fst p = 0xBF9 then Some (ArchObj (PageDirectory pd2_3065)) else if fst p = 0xBF7 then Some (ArchObj (PageDirectory pd2_3063)) else if fst p = 9 then Some (Endpoint IdleEP) else if fst p = 7 then Some (CNode 10 caps2_7) else if fst p = 6 then Some (CNode 10 caps2_6) else None) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some cap) \<or> (\<exists>tcb. (if fst p = 0xC08 then Some (TCB \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if fst p = 0xC07 then Some (TCB \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if fst p = 0xC05 then Some (ArchObj (PageTable pt2_3077)) else if fst p = 0xC00 then Some (ArchObj (PageTable pt2_3072)) else if fst p = 0xBF9 then Some (ArchObj (PageDirectory pd2_3065)) else if fst p = 0xBF7 then Some (ArchObj (PageDirectory pd2_3063)) else if fst p = 9 then Some (Endpoint IdleEP) else if fst p = 7 then Some (CNode 10 caps2_7) else if fst p = 6 then Some (CNode 10 caps2_6) else None) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> cap = get tcb)) then Some (THE cap. (\<exists>sz fun. (if fst p = 0xC08 then Some (TCB \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if fst p = 0xC07 then Some (TCB \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if fst p = 0xC05 then Some (ArchObj (PageTable pt2_3077)) else if fst p = 0xC00 then Some (ArchObj (PageTable pt2_3072)) else if fst p = 0xBF9 then Some (ArchObj (PageDirectory pd2_3065)) else if fst p = 0xBF7 then Some (ArchObj (PageDirectory pd2_3063)) else if fst p = 9 then Some (Endpoint IdleEP) else if fst p = 7 then Some (CNode 10 caps2_7) else if fst p = 6 then Some (CNode 10 caps2_6) else None) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some cap) \<or> (\<exists>tcb. (if fst p = 0xC08 then Some (TCB \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if fst p = 0xC07 then Some (TCB \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if fst p = 0xC05 then Some (ArchObj (PageTable pt2_3077)) else if fst p = 0xC00 then Some (ArchObj (PageTable pt2_3072)) else if fst p = 0xBF9 then Some (ArchObj (PageDirectory pd2_3065)) else if fst p = 0xBF7 then Some (ArchObj (PageDirectory pd2_3063)) else if fst p = 9 then Some (Endpoint IdleEP) else if fst p = 7 then Some (CNode 10 caps2_7) else if fst p = 6 then Some (CNode 10 caps2_6) else None) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> cap = get tcb))) else None) = Some cap; well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6\<rbrakk> \<Longrightarrow> cap = NullCap \<or> p = (6, the_nat_to_bl_10 (Suc 0)) \<and> cap = ThreadCap 0xC07 \<or> p = (6, the_nat_to_bl_10 2) \<and> cap = CNodeCap 6 undefined undefined \<or> p = (6, the_nat_to_bl_10 3) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)) \<or> p = (6, the_nat_to_bl_10 4) \<and> cap = CNodeCap 5 undefined undefined \<or> p = (7, the_nat_to_bl_10 (Suc 0)) \<and> cap = ThreadCap 0xC08 \<or> p = (7, the_nat_to_bl_10 2) \<and> cap = CNodeCap 7 undefined undefined \<or> p = (7, the_nat_to_bl_10 3) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)) \<or> p = (7, the_nat_to_bl_10 4) \<and> cap = CNodeCap 5 undefined undefined \<or> p = (0xC07, tcb_cnode_index 0) \<and> cap = CNodeCap 6 undefined undefined \<or> p = (0xC07, tcb_cnode_index (Suc 0)) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)) \<or> p = (0xC07, tcb_cnode_index 2) \<and> cap = ReplyCap 0xC07 True {AllowGrant, AllowWrite} \<or> p = (0xC07, tcb_cnode_index 3) \<and> cap = NullCap \<or> p = (0xC07, tcb_cnode_index 4) \<and> cap = NullCap \<or> p = (0xC08, tcb_cnode_index 0) \<and> cap = CNodeCap 7 undefined undefined \<or> p = (0xC08, tcb_cnode_index (Suc 0)) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)) \<or> p = (0xC08, tcb_cnode_index 2) \<and> cap = ReplyCap 0xC08 True {AllowGrant, AllowWrite} \<or> p = (0xC08, tcb_cnode_index 3) \<and> cap = NullCap \<or> p = (0xC08, tcb_cnode_index 4) \<and> cap = NullCap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(if \<exists>cap. (\<exists>sz fun. (if a = 0xC08 then Some (TCB \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if a = 0xC07 then Some (TCB \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if a = 0xC05 then Some (ArchObj (PageTable pt2_3077)) else if a = 0xC00 then Some (ArchObj (PageTable pt2_3072)) else if a = 0xBF9 then Some (ArchObj (PageDirectory pd2_3065)) else if a = 0xBF7 then Some (ArchObj (PageDirectory pd2_3063)) else if a = 9 then Some (Endpoint IdleEP) else if a = 7 then Some (CNode 10 caps2_7) else if a = 6 then Some (CNode 10 caps2_6) else None) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some cap) \<or> (\<exists>tcb. (if a = 0xC08 then Some (TCB \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if a = 0xC07 then Some (TCB \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if a = 0xC05 then Some (ArchObj (PageTable pt2_3077)) else if a = 0xC00 then Some (ArchObj (PageTable pt2_3072)) else if a = 0xBF9 then Some (ArchObj (PageDirectory pd2_3065)) else if a = 0xBF7 then Some (ArchObj (PageDirectory pd2_3063)) else if a = 9 then Some (Endpoint IdleEP) else if a = 7 then Some (CNode 10 caps2_7) else if a = 6 then Some (CNode 10 caps2_6) else None) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb)) then Some (THE cap. (\<exists>sz fun. (if a = 0xC08 then Some (TCB \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if a = 0xC07 then Some (TCB \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if a = 0xC05 then Some (ArchObj (PageTable pt2_3077)) else if a = 0xC00 then Some (ArchObj (PageTable pt2_3072)) else if a = 0xBF9 then Some (ArchObj (PageDirectory pd2_3065)) else if a = 0xBF7 then Some (ArchObj (PageDirectory pd2_3063)) else if a = 9 then Some (Endpoint IdleEP) else if a = 7 then Some (CNode 10 caps2_7) else if a = 6 then Some (CNode 10 caps2_6) else None) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some cap) \<or> (\<exists>tcb. (if a = 0xC08 then Some (TCB \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if a = 0xC07 then Some (TCB \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>) else if a = 0xC05 then Some (ArchObj (PageTable pt2_3077)) else if a = 0xC00 then Some (ArchObj (PageTable pt2_3072)) else if a = 0xBF9 then Some (ArchObj (PageDirectory pd2_3065)) else if a = 0xBF7 then Some (ArchObj (PageDirectory pd2_3063)) else if a = 9 then Some (Endpoint IdleEP) else if a = 7 then Some (CNode 10 caps2_7) else if a = 6 then Some (CNode 10 caps2_6) else None) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))) else None) = Some cap; well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6; p = (a, b); cap \<noteq> NullCap; b = the_nat_to_bl_10 (Suc 0) \<longrightarrow> a = 6 \<longrightarrow> cap \<noteq> ThreadCap 0xC07; b = the_nat_to_bl_10 2 \<longrightarrow> a = 6 \<longrightarrow> cap \<noteq> CNodeCap 6 undefined undefined; b = the_nat_to_bl_10 3 \<longrightarrow> a = 6 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)); b = the_nat_to_bl_10 4 \<longrightarrow> a = 6 \<longrightarrow> cap \<noteq> CNodeCap 5 undefined undefined; b = the_nat_to_bl_10 (Suc 0) \<longrightarrow> a = 7 \<longrightarrow> cap \<noteq> ThreadCap 0xC08; b = the_nat_to_bl_10 2 \<longrightarrow> a = 7 \<longrightarrow> cap \<noteq> CNodeCap 7 undefined undefined; b = the_nat_to_bl_10 3 \<longrightarrow> a = 7 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)); b = the_nat_to_bl_10 4 \<longrightarrow> a = 7 \<longrightarrow> cap \<noteq> CNodeCap 5 undefined undefined; b = tcb_cnode_index 0 \<longrightarrow> a = 0xC07 \<longrightarrow> cap \<noteq> CNodeCap 6 undefined undefined; b = tcb_cnode_index (Suc 0) \<longrightarrow> a = 0xC07 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)); b = tcb_cnode_index 2 \<longrightarrow> a = 0xC07 \<longrightarrow> cap \<noteq> ReplyCap 0xC07 True {AllowGrant, AllowWrite}; b = tcb_cnode_index 0 \<longrightarrow> a = 0xC08 \<longrightarrow> cap \<noteq> CNodeCap 7 undefined undefined; b = tcb_cnode_index (Suc 0) \<longrightarrow> a = 0xC08 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)); b = tcb_cnode_index 2 \<longrightarrow> a = 0xC08 \<longrightarrow> cap \<noteq> ReplyCap 0xC08 True {AllowGrant, AllowWrite}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>b get set restr. \<lbrakk>well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6; p = (0xC08, b); get \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> \<noteq> NullCap; b \<noteq> tcb_cnode_index 0; b \<noteq> tcb_cnode_index (Suc 0); b \<noteq> tcb_cnode_index 2; cap = get \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> False
 2. \<And>b get set restr. \<lbrakk>well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6; p = (0xC07, b); get \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> \<noteq> NullCap; b \<noteq> tcb_cnode_index 0; b \<noteq> tcb_cnode_index (Suc 0); b \<noteq> tcb_cnode_index 2; cap = get \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> False
 3. \<And>b. \<lbrakk>well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6; p = (7, b); cap \<noteq> NullCap; b = the_nat_to_bl_10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap 0xC08; b = the_nat_to_bl_10 2 \<longrightarrow> cap \<noteq> CNodeCap 7 undefined undefined; b = the_nat_to_bl_10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)); b = the_nat_to_bl_10 4 \<longrightarrow> cap \<noteq> CNodeCap 5 undefined undefined; caps2_7 b = Some cap\<rbrakk> \<Longrightarrow> False
 4. \<And>b. \<lbrakk>well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6; p = (6, b); cap \<noteq> NullCap; b = the_nat_to_bl_10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap 0xC07; b = the_nat_to_bl_10 2 \<longrightarrow> cap \<noteq> CNodeCap 6 undefined undefined; b = the_nat_to_bl_10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)); b = the_nat_to_bl_10 4 \<longrightarrow> cap \<noteq> CNodeCap 5 undefined undefined; caps2_6 b = Some cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6; p = (7, b); cap \<noteq> NullCap; b = the_nat_to_bl_10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap 0xC08; b = the_nat_to_bl_10 2 \<longrightarrow> cap \<noteq> CNodeCap 7 undefined undefined; b = the_nat_to_bl_10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)); b = the_nat_to_bl_10 4 \<longrightarrow> cap \<noteq> CNodeCap 5 undefined undefined; caps2_7 b = Some cap\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6; p = (6, b); cap \<noteq> NullCap; b = the_nat_to_bl_10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap 0xC07; b = the_nat_to_bl_10 2 \<longrightarrow> cap \<noteq> CNodeCap 6 undefined undefined; b = the_nat_to_bl_10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)); b = the_nat_to_bl_10 4 \<longrightarrow> cap \<noteq> CNodeCap 5 undefined undefined; caps2_6 b = Some cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>well_formed_cnode_n 10 caps2_7; well_formed_cnode_n 10 caps2_6; p = (6, b); cap \<noteq> NullCap; b = the_nat_to_bl_10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap 0xC07; b = the_nat_to_bl_10 2 \<longrightarrow> cap \<noteq> CNodeCap 6 undefined undefined; b = the_nat_to_bl_10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)); b = the_nat_to_bl_10 4 \<longrightarrow> cap \<noteq> CNodeCap 5 undefined undefined; caps2_6 b = Some cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!