theory Retype_DP

lemma dummy_detype_if_untyped:
  "\<lbrakk>finite obj_range ;<(\<And>* ptr\<in>obj_range. ptr \<mapsto>o Untyped) \<and>* P > s\<rbrakk>
  \<Longrightarrow> (detype obj_range s) = s" apply (case_tac s,clarsimp simp:detype_def sep_set_conj_def) apply (rule ext) apply (clarsimp simp:sep_state_projection_def sep_conj_def) apply (subst (asm) sep.prod.remove) apply simp+ apply (clarsimp simp:sep_map_o_conj image_def) apply (drule_tac f = sep_heap in arg_cong) apply (drule_tac x = "(x,Fields)" in fun_cong)+ apply (case_tac xa,case_tac y) apply (clarsimp simp:plus_sep_state_def sep_state_add_def asid_reset_def
    intent_reset_def update_slots_def object_wipe_slots_def sep_disj_sep_state_def
    object_to_sep_state_def object_project_def object_clean_def
    sep_state_disj_def) apply (drule map_disj_None_right'[rotated]) apply simp apply (clarsimp simp: map_add_def split:option.splits) apply (case_tac z) apply (clarsimp simp:plus_sep_state_def sep_state_add_def asid_reset_def
    intent_reset_def update_slots_def object_wipe_slots_def sep_disj_sep_state_def
    object_to_sep_state_def object_project_def object_clean_def
    sep_state_disj_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite obj_range; cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> detype obj_range s = s proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objectsa cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. \<lbrakk>cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>\<rbrakk> \<Longrightarrow> (\<lambda>x. if x \<in> obj_range then Some Untyped else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x) = cdl_objectsa proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objectsa cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x. \<lbrakk>cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>\<rbrakk> \<Longrightarrow> (if x \<in> obj_range then Some Untyped else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x) = cdl_objectsa x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; xa ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects obj_id)) (\<lambda>irq. Some (cdl_irq_node irq)) = xa + y; (SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) xa; P y; x \<in> obj_range\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (3 subgoals):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y. \<lbrakk>P y; x \<in> obj_range; s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; xa ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects obj_id)) (\<lambda>irq. Some (cdl_irq_node irq)) = xa + y\<rbrakk> \<Longrightarrow> finite obj_range
 2. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y. \<lbrakk>P y; x \<in> obj_range; s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; xa ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects obj_id)) (\<lambda>irq. Some (cdl_irq_node irq)) = xa + y\<rbrakk> \<Longrightarrow> ?x13 cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y \<in> obj_range
 3. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; xa ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects obj_id)) (\<lambda>irq. Some (cdl_irq_node irq)) = xa + y; (?x13 cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y \<mapsto>o Untyped \<and>* (SETSEPCONJ ptr:obj_range - {?x13 cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y}. ptr \<mapsto>o Untyped)) xa; P y; x \<in> obj_range\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; xa ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects obj_id)) (\<lambda>irq. Some (cdl_irq_node irq)) = xa + y; (x \<mapsto>o Untyped \<and>* (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped)) xa; P y; x \<in> obj_range\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; xa ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects obj_id)) (\<lambda>irq. Some (cdl_irq_node irq)) = xa + y; P y; x \<in> obj_range; sep_heap xa |` ({x} \<times> UNIV) = object_to_sep_state x Untyped UNIV; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (sep_heap xa |` (UNIV - {x} \<times> UNIV)) (sep_irq_node xa))\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; xa ## y; P y; x \<in> obj_range; sep_heap xa |` ({x} \<times> UNIV) = object_to_sep_state x Untyped UNIV; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (sep_heap xa |` (UNIV - {x} \<times> UNIV)) (sep_irq_node xa)); sep_heap (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects obj_id)) (\<lambda>irq. Some (cdl_irq_node irq))) = sep_heap (xa + y)\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; xa ## y; P y; x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (sep_heap xa |` (UNIV - {x} \<times> UNIV)) (sep_irq_node xa)); (sep_heap xa |` ({x} \<times> UNIV)) (x, Fields) = object_to_sep_state x Untyped UNIV (x, Fields); sep_heap (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects obj_id)) (\<lambda>irq. Some (cdl_irq_node irq))) (x, Fields) = sep_heap (xa + y) (x, Fields)\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x xa y x1 x2 x1a x2a. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; xa ## y; P y; x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (sep_heap xa |` (UNIV - {x} \<times> UNIV)) (sep_irq_node xa)); (sep_heap xa |` ({x} \<times> UNIV)) (x, Fields) = object_to_sep_state x Untyped UNIV (x, Fields); sep_heap (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects obj_id)) (\<lambda>irq. Some (cdl_irq_node irq))) (x, Fields) = sep_heap (xa + y) (x, Fields); xa = SepState x1 x2; y = SepState x1a x2a\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); map_option (object_project Fields) (cdl_objects x) = (x1 ++ x1a) (x, Fields); x1 \<bottom> x1a; x2 \<bottom> x2a\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (2 subgoals):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); map_option (object_project Fields) (cdl_objects x) = (x1 ++ x1a) (x, Fields); x2 \<bottom> x2a\<rbrakk> \<Longrightarrow> x1 (?x26 cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a) = Some (?y26 cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a)
 2. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); map_option (object_project Fields) (cdl_objects x) = (x1 ++ x1a) (x, Fields); x2 \<bottom> x2a; x1a (?x26 cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a) = None\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); map_option (object_project Fields) (cdl_objects x) = (x1 ++ x1a) (x, Fields); x2 \<bottom> x2a; x1a (x, Fields) = None\<rbrakk> \<Longrightarrow> Some Untyped = cdl_objects x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped\<rbrakk> \<Longrightarrow> Untyped = z proof (prove)
goal (10 subgoals):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = Endpoint\<rbrakk> \<Longrightarrow> Untyped = z
 2. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = Notification\<rbrakk> \<Longrightarrow> Untyped = z
 3. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z x3. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = Tcb x3\<rbrakk> \<Longrightarrow> Untyped = z
 4. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z x4. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = CNode x4\<rbrakk> \<Longrightarrow> Untyped = z
 5. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z x5. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = AsidPool x5\<rbrakk> \<Longrightarrow> Untyped = z
 6. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z x6. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = PageTable x6\<rbrakk> \<Longrightarrow> Untyped = z
 7. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z x7. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = PageDirectory x7\<rbrakk> \<Longrightarrow> Untyped = z
 8. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z x8. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = Frame x8\<rbrakk> \<Longrightarrow> Untyped = z
 9. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = Untyped\<rbrakk> \<Longrightarrow> Untyped = z
 10. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x x1 x2 x1a x2a z x10. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; P (SepState x1a x2a); x \<in> obj_range; (SETSEPCONJ ptr:obj_range - {x}. ptr \<mapsto>o Untyped) (SepState (x1 |` (UNIV - {x} \<times> UNIV)) x2); x1 (x, Fields) = Some (CDL_Object Untyped); x2 \<bottom> x2a; x1a (x, Fields) = None; cdl_objects x = Some z; object_project Fields z = CDL_Object Untyped; z = IRQNode x10\<rbrakk> \<Longrightarrow> Untyped = z proof (prove)
goal:
No subgoals!