theory Example_Valid_StateH

lemma map_to_ctes_kh0H_dom:
  "dom (map_to_ctes kh0H) =
             {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20,
              idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40,
              Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20,
              Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40,
              High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20,
              High_tcb_ptr + 0x30, High_tcb_ptr + 0x40,
              irq_cnode_ptr} \<union>
             irq_node_offs_range \<union>
             cnode_offs_range Silc_cnode_ptr \<union>
             cnode_offs_range High_cnode_ptr \<union>
             cnode_offs_range Low_cnode_ptr" supply option.case_cong[cong] if_cong[cong] apply (rule equalityI) apply (simp add: map_to_ctes_kh0H dom_def) apply clarsimp apply (clarsimp simp: offs_in_range option_update_range_def split: option.splits if_split_asm) apply (clarsimp simp: idle_tcb_cte_def) apply (clarsimp simp: High_tcb_cte_def) apply (clarsimp simp: Low_tcb_cte_def) apply (clarsimp simp: Silc_cte_cte_def cnode_offs_range_def split: if_split_asm) apply (clarsimp simp: High_cte_cte_def cnode_offs_range_def split: if_split_asm) apply (clarsimp simp: Low_cte_cte_def cnode_offs_range_def split: if_split_asm) apply (clarsimp simp: dom_def) apply (clarsimp simp: idle_tcb_cte_def Low_tcb_cte_def High_tcb_cte_def) apply (rule conjI) apply (fastforce dest: irq_node_offs_range_correct) apply (rule conjI) apply clarsimp apply (frule cnode_offs_range_correct) apply (clarsimp simp: Silc_cte_cte_def Silc_cte'_def Silc_capsH_def empty_cte_def cnode_offs_range_def) apply (rule conjI) apply clarsimp apply (frule cnode_offs_range_correct) apply (clarsimp simp: High_cte_cte_def High_cte'_def High_capsH_def empty_cte_def cnode_offs_range_def) apply clarsimp apply (frule cnode_offs_range_correct) apply (clarsimp simp: Low_cte_cte_def Low_cte'_def Low_capsH_def empty_cte_def cnode_offs_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (map_to_ctes kh0H) = {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr proof (prove)
goal (1 subgoal):
 1. dom (map_to_ctes kh0H) = {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr proof (prove)
goal (2 subgoals):
 1. dom (map_to_ctes kh0H) \<subseteq> {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr
 2. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (2 subgoals):
 1. {a. \<exists>y. option_update_range (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CTE capability.NullCap (MDB 0 0 False False)) else None) (option_update_range (Low_cte_cte Low_cnode_ptr) (option_update_range (High_cte_cte High_cnode_ptr) (option_update_range (Silc_cte_cte Silc_cnode_ptr) (option_update_range [irq_cnode_ptr \<mapsto> CTE capability.NullCap (MDB 0 0 False False)] (option_update_range Low_tcb_cte (option_update_range High_tcb_cte (option_update_range idle_tcb_cte (\<lambda>x. None)))))))) a = Some y} \<subseteq> insert idle_tcb_ptr (insert (idle_tcb_ptr + 0x10) (insert (idle_tcb_ptr + 0x20) (insert (idle_tcb_ptr + 0x30) (insert (idle_tcb_ptr + 0x40) (insert Low_tcb_ptr (insert (Low_tcb_ptr + 0x10) (insert (Low_tcb_ptr + 0x20) (insert (Low_tcb_ptr + 0x30) (insert (Low_tcb_ptr + 0x40) (insert High_tcb_ptr (insert (High_tcb_ptr + 0x10) (insert (High_tcb_ptr + 0x20) (insert (High_tcb_ptr + 0x30) (insert (High_tcb_ptr + 0x40) (insert irq_cnode_ptr (irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr))))))))))))))))
 2. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; option_update_range (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CTE capability.NullCap (MDB 0 0 False False)) else None) (option_update_range (Low_cte_cte Low_cnode_ptr) (option_update_range (High_cte_cte High_cnode_ptr) (option_update_range (Silc_cte_cte Silc_cnode_ptr) (option_update_range [irq_cnode_ptr \<mapsto> CTE capability.NullCap (MDB 0 0 False False)] (option_update_range Low_tcb_cte (option_update_range High_tcb_cte (option_update_range idle_tcb_cte (\<lambda>x. None)))))))) x = Some y\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 2. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = None; Low_tcb_cte x = None; High_tcb_cte x = None; idle_tcb_cte x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 2. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = None; Low_tcb_cte x = None; High_tcb_cte x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 3. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = None; Low_tcb_cte x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 4. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 5. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 6. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 7. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = None; Low_tcb_cte x = None; High_tcb_cte x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 2. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = None; Low_tcb_cte x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 3. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 4. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 5. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 6. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = None; Low_tcb_cte x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 2. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 3. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 4. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 5. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = None; Silc_cte_cte Silc_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 2. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 3. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 4. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = None; High_cte_cte High_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 2. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 3. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Low_cte_cte Low_cnode_ptr x = Some y; x \<noteq> idle_tcb_ptr; x \<noteq> idle_tcb_ptr + 0x10; x \<noteq> idle_tcb_ptr + 0x20; x \<noteq> idle_tcb_ptr + 0x30; x \<noteq> idle_tcb_ptr + 0x40; x \<noteq> Low_tcb_ptr; x \<noteq> Low_tcb_ptr + 0x10; x \<noteq> Low_tcb_ptr + 0x20; x \<noteq> Low_tcb_ptr + 0x30; x \<noteq> Low_tcb_ptr + 0x40; x \<noteq> High_tcb_ptr; x \<noteq> High_tcb_ptr + 0x10; x \<noteq> High_tcb_ptr + 0x20; x \<noteq> High_tcb_ptr + 0x30; x \<noteq> High_tcb_ptr + 0x40; x \<noteq> irq_cnode_ptr; x \<notin> cnode_offs_range Low_cnode_ptr; x \<notin> cnode_offs_range High_cnode_ptr; x \<notin> cnode_offs_range Silc_cnode_ptr; \<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x\<rbrakk> \<Longrightarrow> x \<in> irq_node_offs_range
 2. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (1 subgoal):
 1. {idle_tcb_ptr, idle_tcb_ptr + 0x10, idle_tcb_ptr + 0x20, idle_tcb_ptr + 0x30, idle_tcb_ptr + 0x40, Low_tcb_ptr, Low_tcb_ptr + 0x10, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x30, Low_tcb_ptr + 0x40, High_tcb_ptr, High_tcb_ptr + 0x10, High_tcb_ptr + 0x20, High_tcb_ptr + 0x30, High_tcb_ptr + 0x40, irq_cnode_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<subseteq> dom (map_to_ctes kh0H) proof (prove)
goal (1 subgoal):
 1. (\<exists>y. idle_tcb_cte idle_tcb_ptr = Some y) \<and> (\<exists>y. idle_tcb_cte (idle_tcb_ptr + 0x10) = Some y) \<and> (\<exists>y. idle_tcb_cte (idle_tcb_ptr + 0x20) = Some y) \<and> (\<exists>y. idle_tcb_cte (idle_tcb_ptr + 0x30) = Some y) \<and> (\<exists>y. idle_tcb_cte (idle_tcb_ptr + 0x40) = Some y) \<and> (\<exists>y. Low_tcb_cte Low_tcb_ptr = Some y) \<and> (\<exists>y. Low_tcb_cte (Low_tcb_ptr + 0x10) = Some y) \<and> (\<exists>y. Low_tcb_cte (Low_tcb_ptr + 0x20) = Some y) \<and> (\<exists>y. Low_tcb_cte (Low_tcb_ptr + 0x30) = Some y) \<and> (\<exists>y. Low_tcb_cte (Low_tcb_ptr + 0x40) = Some y) \<and> (\<exists>y. High_tcb_cte High_tcb_ptr = Some y) \<and> (\<exists>y. High_tcb_cte (High_tcb_ptr + 0x10) = Some y) \<and> (\<exists>y. High_tcb_cte (High_tcb_ptr + 0x20) = Some y) \<and> (\<exists>y. High_tcb_cte (High_tcb_ptr + 0x30) = Some y) \<and> (\<exists>y. High_tcb_cte (High_tcb_ptr + 0x40) = Some y) \<and> irq_node_offs_range \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (1 subgoal):
 1. irq_node_offs_range \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (2 subgoals):
 1. irq_node_offs_range \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y}
 2. cnode_offs_range Silc_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (1 subgoal):
 1. cnode_offs_range Silc_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (2 subgoals):
 1. cnode_offs_range Silc_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y}
 2. cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> cnode_offs_range Silc_cnode_ptr \<Longrightarrow> \<exists>y. map_to_ctes kh0H x = Some y
 2. cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> cnode_offs_range Silc_cnode_ptr; \<exists>y. length y = 10 \<and> x = Silc_cnode_ptr + of_bl y * 0x10\<rbrakk> \<Longrightarrow> \<exists>y. map_to_ctes kh0H x = Some y
 2. cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (1 subgoal):
 1. cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (2 subgoals):
 1. cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y}
 2. cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> cnode_offs_range High_cnode_ptr \<Longrightarrow> \<exists>y. map_to_ctes kh0H x = Some y
 2. cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> cnode_offs_range High_cnode_ptr; \<exists>y. length y = 10 \<and> x = High_cnode_ptr + of_bl y * 0x10\<rbrakk> \<Longrightarrow> \<exists>y. map_to_ctes kh0H x = Some y
 2. cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (1 subgoal):
 1. cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. map_to_ctes kh0H a = Some y} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> cnode_offs_range Low_cnode_ptr \<Longrightarrow> \<exists>y. map_to_ctes kh0H x = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> cnode_offs_range Low_cnode_ptr; \<exists>y. length y = 10 \<and> x = Low_cnode_ptr + of_bl y * 0x10\<rbrakk> \<Longrightarrow> \<exists>y. map_to_ctes kh0H x = Some y proof (prove)
goal:
No subgoals!