theory Example_Valid_StateH

lemma map_to_ctes_kh0H_SomeD:
  "(map_to_ctes kh0H) x = Some y \<Longrightarrow>
        x = idle_tcb_ptr \<and> y = (CTE NullCap Null_mdb) \<or>
        x = idle_tcb_ptr + 0x10 \<and> y = (CTE NullCap Null_mdb) \<or>
        x = idle_tcb_ptr + 0x20 \<and> y = (CTE NullCap Null_mdb) \<or>
        x = idle_tcb_ptr + 0x30 \<and> y = (CTE NullCap Null_mdb) \<or>
        x = idle_tcb_ptr + 0x40 \<and> y = (CTE NullCap Null_mdb) \<or>
        x = Low_tcb_ptr \<and> y = (CTE (CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False)) \<or>
        x = Low_tcb_ptr + 0x10 \<and> y = (CTE (ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False)) \<or>
        x = Low_tcb_ptr + 0x20 \<and> y = (CTE (ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True)) \<or>
        x = Low_tcb_ptr + 0x30 \<and> y = (CTE NullCap Null_mdb) \<or>
        x = Low_tcb_ptr + 0x40 \<and> y = (CTE NullCap Null_mdb) \<or>
        x = High_tcb_ptr \<and> y = (CTE (CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False)) \<or>
        x = High_tcb_ptr + 0x10 \<and> y = (CTE (ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False)) \<or>
        x = High_tcb_ptr + 0x20 \<and> y = (CTE (ReplyCap High_tcb_ptr True True) (MDB 0 0 True True)) \<or>
        x = High_tcb_ptr + 0x30 \<and> y = (CTE NullCap Null_mdb) \<or>
        x = High_tcb_ptr + 0x40 \<and> y = (CTE NullCap Null_mdb) \<or>
        x = irq_cnode_ptr \<and> y = (CTE NullCap Null_mdb) \<or>
        x \<in> irq_node_offs_range \<and> y = (CTE NullCap Null_mdb) \<or>
        x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or>
        x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or>
        x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)" apply (frule map_to_ctes_kh0H_SomeD') apply (elim disjE) apply (clarsimp simp: idle_tcb_cte_def idle_tcbH_def Low_tcb_cte_def Low_tcbH_def Low_capsH_def High_tcb_cte_def High_tcbH_def High_capsH_def the_nat_to_bl_def nat_to_bl_def)+ by (drule offs_range_correct, clarsimp simp: offs_in_range)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_ctes kh0H x = Some y \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_to_ctes kh0H x = Some y; x = idle_tcb_ptr \<or> x = idle_tcb_ptr + 0x10 \<or> x = idle_tcb_ptr + 0x20 \<or> x = idle_tcb_ptr + 0x30 \<or> x = idle_tcb_ptr + 0x40 \<or> x = Low_tcb_ptr \<or> x = Low_tcb_ptr + 0x10 \<or> x = Low_tcb_ptr + 0x20 \<or> x = Low_tcb_ptr + 0x30 \<or> x = Low_tcb_ptr + 0x40 \<or> x = High_tcb_ptr \<or> x = High_tcb_ptr + 0x10 \<or> x = High_tcb_ptr + 0x20 \<or> x = High_tcb_ptr + 0x30 \<or> x = High_tcb_ptr + 0x40 \<or> x = irq_cnode_ptr \<or> x \<in> irq_node_offs_range \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<or> x \<in> cnode_offs_range High_cnode_ptr \<or> x \<in> cnode_offs_range Low_cnode_ptr\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x) proof (prove)
goal (20 subgoals):
 1. \<lbrakk>map_to_ctes kh0H x = Some y; x = idle_tcb_ptr\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 2. \<lbrakk>map_to_ctes kh0H x = Some y; x = idle_tcb_ptr + 0x10\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 3. \<lbrakk>map_to_ctes kh0H x = Some y; x = idle_tcb_ptr + 0x20\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 4. \<lbrakk>map_to_ctes kh0H x = Some y; x = idle_tcb_ptr + 0x30\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 5. \<lbrakk>map_to_ctes kh0H x = Some y; x = idle_tcb_ptr + 0x40\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 6. \<lbrakk>map_to_ctes kh0H x = Some y; x = Low_tcb_ptr\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 7. \<lbrakk>map_to_ctes kh0H x = Some y; x = Low_tcb_ptr + 0x10\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 8. \<lbrakk>map_to_ctes kh0H x = Some y; x = Low_tcb_ptr + 0x20\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 9. \<lbrakk>map_to_ctes kh0H x = Some y; x = Low_tcb_ptr + 0x30\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 10. \<lbrakk>map_to_ctes kh0H x = Some y; x = Low_tcb_ptr + 0x40\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
A total of 20 subgoals... proof (prove)
goal (4 subgoals):
 1. \<lbrakk>map_to_ctes kh0H x = Some y; x \<in> irq_node_offs_range; x = Low_tcb_ptr \<longrightarrow> y \<noteq> CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False); x = Low_tcb_ptr + 0x10 \<longrightarrow> y \<noteq> CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False); x = Low_tcb_ptr + 0x20 \<longrightarrow> y \<noteq> CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True); x = High_tcb_ptr \<longrightarrow> y \<noteq> CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False); x = High_tcb_ptr + 0x10 \<longrightarrow> y \<noteq> CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False); x = High_tcb_ptr + 0x20 \<longrightarrow> y \<noteq> CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True); y \<noteq> CTE capability.NullCap (MDB 0 0 False False); x \<in> cnode_offs_range Silc_cnode_ptr \<longrightarrow> Silc_cte_cte Silc_cnode_ptr x = None \<or> y \<noteq> the (Silc_cte_cte Silc_cnode_ptr x); x \<in> cnode_offs_range Low_cnode_ptr \<longrightarrow> Low_cte_cte Low_cnode_ptr x = None \<or> y \<noteq> the (Low_cte_cte Low_cnode_ptr x)\<rbrakk> \<Longrightarrow> x \<in> cnode_offs_range High_cnode_ptr \<and> (\<exists>y. High_cte_cte High_cnode_ptr x = Some y) \<and> y = the (High_cte_cte High_cnode_ptr x)
 2. \<lbrakk>map_to_ctes kh0H x = Some y; x \<in> cnode_offs_range Silc_cnode_ptr\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 3. \<lbrakk>map_to_ctes kh0H x = Some y; x \<in> cnode_offs_range High_cnode_ptr\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)
 4. \<lbrakk>map_to_ctes kh0H x = Some y; x \<in> cnode_offs_range Low_cnode_ptr\<rbrakk> \<Longrightarrow> x = idle_tcb_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x10 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x20 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = idle_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr \<and> y = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> x = Low_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> x = Low_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> x = Low_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = Low_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr \<and> y = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> x = High_tcb_ptr + 0x10 \<and> y = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> x = High_tcb_ptr + 0x20 \<and> y = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> x = High_tcb_ptr + 0x30 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = High_tcb_ptr + 0x40 \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x = irq_cnode_ptr \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> irq_node_offs_range \<and> y = CTE capability.NullCap (MDB 0 0 False False) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte_cte Silc_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte_cte Low_cnode_ptr x)