theory Example_Valid_StateH

lemma kh0_pspace_dom:
  "pspace_dom kh0 = {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr,
              irq_cnode_ptr, ntfn_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 \<union>
             pd_offs_range init_global_pd \<union>
             pd_offs_range High_pd_ptr \<union>
             pd_offs_range Low_pd_ptr \<union>
             pt_offs_range High_pt_ptr \<union>
             pt_offs_range Low_pt_ptr" supply nonzero_gt_zero[simp] gt_zero_nonzero[simp] apply (rule equalityI) apply (simp add: dom_def pspace_dom_def) apply clarsimp apply (clarsimp simp: kh0_def obj_relation_cuts_def pd_offs_in_range pt_offs_in_range
                         cnode_offs_in_range irq_node_offs_in_range s0_ptrs_aligned pageBits_def
                         kh0_obj_def cte_map_def' caps_dom_length_10
                  split: if_split_asm) apply (clarsimp simp: pspace_dom_def dom_def) apply (rule conjI) apply (rule_tac x=init_globals_frame in exI) apply (clarsimp simp: kh0_def kh0_obj_def s0_ptr_defs image_def) apply (rule_tac x=0 in exI) apply simp apply (rule conjI) apply (rule_tac x=idle_tcb_ptr in exI) apply (clarsimp simp: kh0_def kh0_obj_def s0_ptr_defs image_def) apply (rule conjI) apply (rule_tac x=High_tcb_ptr in exI) apply (clarsimp simp: kh0_def kh0_obj_def s0_ptr_defs image_def) apply (rule conjI) apply (rule_tac x=Low_tcb_ptr in exI) apply (clarsimp simp: kh0_def kh0_obj_def s0_ptr_defs image_def) apply (rule conjI) apply (rule_tac x=irq_cnode_ptr in exI) apply (clarsimp simp: kh0_def kh0_obj_def s0_ptr_defs image_def cte_map_def) apply (rule conjI) apply (rule_tac x=ntfn_ptr in exI) apply (clarsimp simp: kh0_def kh0_obj_def s0_ptr_defs image_def) apply (rule conjI) apply clarsimp apply (rule_tac x=x in exI) apply (drule offs_range_correct) apply clarsimp apply (force simp: kh0_def kh0_obj_def image_def cte_map_def') apply (rule conjI) apply clarsimp apply (rule_tac x=Silc_cnode_ptr in exI) apply (drule offs_range_correct) apply (force simp: kh0_def kh0_obj_def image_def s0_ptr_defs cte_map_def' dom_caps) apply (rule conjI) apply clarsimp apply (rule_tac x=High_cnode_ptr in exI) apply (drule offs_range_correct) apply (force simp: kh0_def kh0_obj_def image_def s0_ptr_defs cte_map_def' dom_caps) apply (rule conjI) apply clarsimp apply (rule_tac x=Low_cnode_ptr in exI) apply (drule offs_range_correct) apply (force simp: kh0_def kh0_obj_def image_def s0_ptr_defs cte_map_def' dom_caps) apply (rule conjI) apply clarsimp apply (rule_tac x=init_global_pd in exI) apply (drule offs_range_correct) apply (force simp: kh0_def kh0_obj_def image_def s0_ptr_defs) apply (rule conjI) apply clarsimp apply (rule_tac x=High_pd_ptr in exI) apply (drule offs_range_correct) apply (force simp: kh0_def kh0_obj_def image_def s0_ptr_defs) apply (rule conjI) apply clarsimp apply (rule_tac x=Low_pd_ptr in exI) apply (drule offs_range_correct) apply (force simp: kh0_def kh0_obj_def image_def s0_ptr_defs) apply (rule conjI) apply clarsimp apply (rule_tac x=High_pt_ptr in exI) apply (drule offs_range_correct) apply (force simp: kh0_def kh0_obj_def image_def s0_ptr_defs) apply clarsimp apply (rule_tac x=Low_pt_ptr in exI) apply (drule offs_range_correct) apply (force simp: kh0_def kh0_obj_def image_def s0_ptr_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_dom kh0 = {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_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 \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr proof (prove)
goal (1 subgoal):
 1. pspace_dom kh0 = {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_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 \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr proof (prove)
goal (2 subgoals):
 1. pspace_dom kh0 \<subseteq> {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_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 \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr
 2. {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_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 \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr \<subseteq> pspace_dom kh0 proof (prove)
goal (2 subgoals):
 1. (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<subseteq> insert init_globals_frame (insert idle_tcb_ptr (insert High_tcb_ptr (insert Low_tcb_ptr (insert irq_cnode_ptr (insert ntfn_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 \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr))))))
 2. {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_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 \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr \<subseteq> pspace_dom kh0 proof (prove)
goal (2 subgoals):
 1. \<And>xa a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y xa; a \<noteq> init_globals_frame; a \<noteq> idle_tcb_ptr; a \<noteq> High_tcb_ptr; a \<noteq> Low_tcb_ptr; a \<noteq> irq_cnode_ptr; a \<noteq> ntfn_ptr; a \<notin> pt_offs_range Low_pt_ptr; a \<notin> pt_offs_range High_pt_ptr; a \<notin> pd_offs_range Low_pd_ptr; a \<notin> pd_offs_range High_pd_ptr; a \<notin> pd_offs_range init_global_pd; a \<notin> cnode_offs_range Low_cnode_ptr; a \<notin> cnode_offs_range High_cnode_ptr; a \<notin> cnode_offs_range Silc_cnode_ptr; kh0 xa = Some y\<rbrakk> \<Longrightarrow> a \<in> irq_node_offs_range
 2. {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_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 \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr \<subseteq> pspace_dom kh0 proof (prove)
goal (1 subgoal):
 1. {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_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 \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr \<subseteq> pspace_dom kh0 proof (prove)
goal (1 subgoal):
 1. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> init_globals_frame \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> idle_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<exists>x. (\<exists>y. kh0 x = Some y) \<and> init_globals_frame \<in> fst ` obj_relation_cuts (the (kh0 x)) x
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> idle_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. (\<exists>y. kh0 init_globals_frame = Some y) \<and> init_globals_frame \<in> fst ` obj_relation_cuts (the (kh0 init_globals_frame)) init_globals_frame
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> idle_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<exists>n. n * 2 ^ pageBits = 0 \<and> n < 2 ^ (12 - pageBits)
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> idle_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. 0 * 2 ^ pageBits = 0 \<and> 0 < 2 ^ (12 - pageBits)
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> idle_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> idle_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<exists>x. (\<exists>y. kh0 x = Some y) \<and> idle_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. (\<exists>y. kh0 idle_tcb_ptr = Some y) \<and> idle_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 idle_tcb_ptr)) idle_tcb_ptr
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<exists>x. (\<exists>y. kh0 x = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. (\<exists>y. kh0 High_tcb_ptr = Some y) \<and> High_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 High_tcb_ptr)) High_tcb_ptr
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<exists>x. (\<exists>y. kh0 x = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. (\<exists>y. kh0 Low_tcb_ptr = Some y) \<and> Low_tcb_ptr \<in> fst ` obj_relation_cuts (the (kh0 Low_tcb_ptr)) Low_tcb_ptr
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<exists>x. (\<exists>y. kh0 x = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. (\<exists>y. kh0 irq_cnode_ptr = Some y) \<and> irq_cnode_ptr \<in> fst ` obj_relation_cuts (the (kh0 irq_cnode_ptr)) irq_cnode_ptr
 2. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. (\<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x) \<and> irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<exists>x. (\<exists>y. kh0 x = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 x)) x
 2. irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. (\<exists>y. kh0 ntfn_ptr = Some y) \<and> ntfn_ptr \<in> fst ` obj_relation_cuts (the (kh0 ntfn_ptr)) ntfn_ptr
 2. irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. irq_node_offs_range \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x)
 2. cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> irq_node_offs_range \<Longrightarrow> \<exists>xa. (\<exists>y. kh0 xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 xa)) xa
 2. cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> irq_node_offs_range \<Longrightarrow> (\<exists>y. kh0 x = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 x)) x
 2. cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>irq. x = init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<Longrightarrow> (\<exists>y. kh0 x = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 x)) x
 2. cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>irq. (\<exists>y. kh0 (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) = Some y) \<and> init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<in> fst ` obj_relation_cuts (the (kh0 (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)))) (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits))
 2. cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. cnode_offs_range Silc_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x)
 2. cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> cnode_offs_range Silc_cnode_ptr \<Longrightarrow> \<exists>xa. (\<exists>y. kh0 xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 xa)) xa
 2. cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> cnode_offs_range Silc_cnode_ptr \<Longrightarrow> (\<exists>y. kh0 Silc_cnode_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 Silc_cnode_ptr)) Silc_cnode_ptr
 2. cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>y. length y = 10 \<and> x = Silc_cnode_ptr + of_bl y * 0x10 \<Longrightarrow> (\<exists>y. kh0 Silc_cnode_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 Silc_cnode_ptr)) Silc_cnode_ptr
 2. cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. cnode_offs_range High_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x)
 2. cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> cnode_offs_range High_cnode_ptr \<Longrightarrow> \<exists>xa. (\<exists>y. kh0 xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 xa)) xa
 2. cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> cnode_offs_range High_cnode_ptr \<Longrightarrow> (\<exists>y. kh0 High_cnode_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 High_cnode_ptr)) High_cnode_ptr
 2. cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>y. length y = 10 \<and> x = High_cnode_ptr + of_bl y * 0x10 \<Longrightarrow> (\<exists>y. kh0 High_cnode_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 High_cnode_ptr)) High_cnode_ptr
 2. cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. cnode_offs_range Low_cnode_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x)
 2. pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> cnode_offs_range Low_cnode_ptr \<Longrightarrow> \<exists>xa. (\<exists>y. kh0 xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 xa)) xa
 2. pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> cnode_offs_range Low_cnode_ptr \<Longrightarrow> (\<exists>y. kh0 Low_cnode_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 Low_cnode_ptr)) Low_cnode_ptr
 2. pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>y. length y = 10 \<and> x = Low_cnode_ptr + of_bl y * 0x10 \<Longrightarrow> (\<exists>y. kh0 Low_cnode_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 Low_cnode_ptr)) Low_cnode_ptr
 2. pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. pd_offs_range init_global_pd \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x)
 2. pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> pd_offs_range init_global_pd \<Longrightarrow> \<exists>xa. (\<exists>y. kh0 xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 xa)) xa
 2. pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> pd_offs_range init_global_pd \<Longrightarrow> (\<exists>y. kh0 init_global_pd = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 init_global_pd)) init_global_pd
 2. pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>y. x = init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<Longrightarrow> (\<exists>y. kh0 init_global_pd = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 init_global_pd)) init_global_pd
 2. pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. pd_offs_range High_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x)
 2. pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> pd_offs_range High_pd_ptr \<Longrightarrow> \<exists>xa. (\<exists>y. kh0 xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 xa)) xa
 2. pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> pd_offs_range High_pd_ptr \<Longrightarrow> (\<exists>y. kh0 High_pd_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 High_pd_ptr)) High_pd_ptr
 2. pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>y. x = High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<Longrightarrow> (\<exists>y. kh0 High_pd_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 High_pd_ptr)) High_pd_ptr
 2. pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. pd_offs_range Low_pd_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x)
 2. pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> pd_offs_range Low_pd_ptr \<Longrightarrow> \<exists>xa. (\<exists>y. kh0 xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 xa)) xa
 2. pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> pd_offs_range Low_pd_ptr \<Longrightarrow> (\<exists>y. kh0 Low_pd_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 Low_pd_ptr)) Low_pd_ptr
 2. pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>y. x = Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<Longrightarrow> (\<exists>y. kh0 Low_pd_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 Low_pd_ptr)) Low_pd_ptr
 2. pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) \<and> pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. pt_offs_range High_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x)
 2. pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> pt_offs_range High_pt_ptr \<Longrightarrow> \<exists>xa. (\<exists>y. kh0 xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 xa)) xa
 2. pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> pt_offs_range High_pt_ptr \<Longrightarrow> (\<exists>y. kh0 High_pt_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 High_pt_ptr)) High_pt_ptr
 2. pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>y. x = High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<Longrightarrow> (\<exists>y. kh0 High_pt_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 High_pt_ptr)) High_pt_ptr
 2. pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. pt_offs_range Low_pt_ptr \<subseteq> (\<Union>x\<in>{a. \<exists>y. kh0 a = Some y}. fst ` obj_relation_cuts (the (kh0 x)) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> pt_offs_range Low_pt_ptr \<Longrightarrow> \<exists>xa. (\<exists>y. kh0 xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 xa)) xa proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> pt_offs_range Low_pt_ptr \<Longrightarrow> (\<exists>y. kh0 Low_pt_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 Low_pt_ptr)) Low_pt_ptr proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>y. x = Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<Longrightarrow> (\<exists>y. kh0 Low_pt_ptr = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kh0 Low_pt_ptr)) Low_pt_ptr proof (prove)
goal:
No subgoals!