theory Abstract_Separation_D

lemma cdl_heap_add_assoc':
  "\<forall>obj_id. not_conflicting_objects x z obj_id \<and>
            not_conflicting_objects y z obj_id \<and>
            not_conflicting_objects x z obj_id \<Longrightarrow>
   cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z =
   cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))" apply (rule ext) apply (rename_tac obj_id) apply (erule_tac x=obj_id in allE) apply (clarsimp simp: cdl_heap_add_def cdl_ghost_state_add_def not_conflicting_objects_def) apply (simp add: Let_unfold split: option.splits) apply (rename_tac obj_y obj_x obj_z) apply (clarsimp simp: object_add_def clean_slots_def object_clean_def object_clean_slots_def Let_unfold) apply (case_tac "has_slots obj_z") apply (subgoal_tac "has_slots obj_y") apply (subgoal_tac "has_slots obj_x") apply ((clarsimp simp: has_slots_object_clean_fields has_slots_object_clean_slots has_slots_object_clean
                           map_add_restrict union_intersection |
            drule inter_empty_not_both |
            erule update_slots_object_clean_fields |
            erule object_type_has_slots, simp |
            simp | safe)+)[3] apply (subgoal_tac "\<not> has_slots obj_y") apply (subgoal_tac "\<not> has_slots obj_x") apply ((clarsimp simp: has_slots_object_clean_fields has_slots_object_clean_slots has_slots_object_clean
                           map_add_restrict union_intersection |
            drule inter_empty_not_both |
            erule object_clean_fields_no_slots |
            erule object_type_has_slots, simp |
            simp | safe)+) apply (fastforce simp: object_type_has_slots)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>obj_id. not_conflicting_objects x z obj_id \<and> not_conflicting_objects y z obj_id \<and> not_conflicting_objects x z obj_id \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<forall>obj_id. not_conflicting_objects x z obj_id \<and> not_conflicting_objects y z obj_id \<and> not_conflicting_objects x z obj_id \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z xa = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) xa proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<forall>obj_id. not_conflicting_objects x z obj_id \<and> not_conflicting_objects y z obj_id \<and> not_conflicting_objects x z obj_id \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z obj_id = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) obj_id proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. not_conflicting_objects x z obj_id \<and> not_conflicting_objects y z obj_id \<and> not_conflicting_objects x z obj_id \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z obj_id = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) obj_id proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}\<rbrakk> \<Longrightarrow> (let heap_b = sep_heap z in case heap_b obj_id of None \<Rightarrow> let heap_a = sep_heap x; heap_b = sep_heap y in case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (sep_ghost_state x obj_id) (sep_ghost_state y obj_id)) | Some obj_b \<Rightarrow> case let heap_a = sep_heap x; heap_b = sep_heap y in case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (sep_ghost_state x obj_id) (sep_ghost_state y obj_id)) of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (let heap_a = sep_heap x; heap_b = sep_heap y; gs_a = sep_ghost_state x; gs_b = sep_ghost_state y in if heap_a obj_id = None \<and> (\<exists>y. heap_b obj_id = Some y) then gs_b obj_id else if heap_b obj_id = None \<and> heap_a obj_id \<noteq> None then gs_a obj_id else gs_a obj_id \<union> gs_b obj_id) (sep_ghost_state z obj_id))) = (let heap_a = sep_heap x in case let heap_a = sep_heap y; heap_b = sep_heap z in case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (sep_ghost_state y obj_id) (sep_ghost_state z obj_id)) of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> let heap_a = sep_heap y; heap_b = sep_heap z in case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (sep_ghost_state y obj_id) (sep_ghost_state z obj_id)) | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (sep_ghost_state x obj_id) (let heap_a = sep_heap y; heap_b = sep_heap z; gs_a = sep_ghost_state y; gs_b = sep_ghost_state z in if heap_a obj_id = None \<and> (\<exists>y. heap_b obj_id = Some y) then gs_b obj_id else if heap_b obj_id = None \<and> heap_a obj_id \<noteq> None then gs_a obj_id else gs_a obj_id \<union> gs_b obj_id))) proof (prove)
goal (1 subgoal):
 1. \<And>obj_id x2 x2a x2b. \<lbrakk>sep_heap x obj_id = Some x2a; object_type x2a = object_type x2b \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; sep_heap y obj_id = Some x2; sep_heap z obj_id = Some x2b; object_type x2 = object_type x2b \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}\<rbrakk> \<Longrightarrow> object_add (object_add x2a x2 (sep_ghost_state x obj_id) (sep_ghost_state y obj_id)) x2b (sep_ghost_state x obj_id \<union> sep_ghost_state y obj_id) (sep_ghost_state z obj_id) = object_add x2a (object_add x2 x2b (sep_ghost_state y obj_id) (sep_ghost_state z obj_id)) (sep_ghost_state x obj_id) (sep_ghost_state y obj_id \<union> sep_ghost_state z obj_id) proof (prove)
goal (1 subgoal):
 1. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; object_type obj_x = object_type obj_z \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_y = object_type obj_z \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}\<rbrakk> \<Longrightarrow> object_add (object_add obj_x obj_y (sep_ghost_state x obj_id) (sep_ghost_state y obj_id)) obj_z (sep_ghost_state x obj_id \<union> sep_ghost_state y obj_id) (sep_ghost_state z obj_id) = object_add obj_x (object_add obj_y obj_z (sep_ghost_state y obj_id) (sep_ghost_state z obj_id)) (sep_ghost_state x obj_id) (sep_ghost_state y obj_id \<union> sep_ghost_state z obj_id) proof (prove)
goal (1 subgoal):
 1. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id))))))) proof (prove)
goal (2 subgoals):
 1. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; has_slots obj_z\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))))
 2. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id))))))) proof (prove)
goal (3 subgoals):
 1. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; has_slots obj_z; has_slots obj_y\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))))
 2. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; has_slots obj_z\<rbrakk> \<Longrightarrow> has_slots obj_y
 3. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id))))))) proof (prove)
goal (4 subgoals):
 1. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; has_slots obj_z; has_slots obj_y; has_slots obj_x\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))))
 2. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; has_slots obj_z; has_slots obj_y\<rbrakk> \<Longrightarrow> has_slots obj_x
 3. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; has_slots obj_z\<rbrakk> \<Longrightarrow> has_slots obj_y
 4. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id))))))) proof (prove)
goal (1 subgoal):
 1. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id))))))) proof (prove)
goal (2 subgoals):
 1. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z; \<not> has_slots obj_y\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))))
 2. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z\<rbrakk> \<Longrightarrow> \<not> has_slots obj_y proof (prove)
goal (3 subgoals):
 1. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z; \<not> has_slots obj_y; \<not> has_slots obj_x\<rbrakk> \<Longrightarrow> (None \<in> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_y) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_y (sep_ghost_state y obj_id))))))) \<and> (None \<notin> sep_ghost_state y obj_id \<longrightarrow> (sep_ghost_state y obj_id = {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set {}) (object_clean_fields obj_z {}) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set {}) obj_z) |` the_set {}) (object_clean_fields obj_z {})) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set {})) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z) |` (the_set {} \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))) \<and> (sep_ghost_state y obj_id \<noteq> {} \<longrightarrow> (None \<in> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_z (sep_ghost_state z obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_z) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_z)) (object_clean_fields obj_z (sep_ghost_state z obj_id))))) \<and> (None \<notin> sep_ghost_state z obj_id \<longrightarrow> (sep_ghost_state z obj_id = {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set {})) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))) \<and> (sep_ghost_state z obj_id \<noteq> {} \<longrightarrow> (sep_ghost_state x obj_id = {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) |` (the_set {} \<union> the_set (sep_ghost_state y obj_id))) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_y (sep_ghost_state y obj_id)) = update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) (object_clean_fields obj_y (sep_ghost_state y obj_id))) \<and> (sep_ghost_state x obj_id \<noteq> {} \<longrightarrow> update_slots (object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y)) obj_x) |` (the_set (sep_ghost_state x obj_id) \<union> the_set (sep_ghost_state y obj_id))) obj_x) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) (object_clean_fields obj_x (sep_ghost_state x obj_id)) = update_slots (object_slots (update_slots (object_slots obj_x |` the_set (sep_ghost_state x obj_id)) obj_x) ++ object_slots (update_slots (object_slots (update_slots (object_slots (update_slots (object_slots obj_y |` the_set (sep_ghost_state y obj_id)) obj_y) ++ object_slots (update_slots (object_slots obj_z |` the_set (sep_ghost_state z obj_id)) obj_z)) obj_y) |` (the_set (sep_ghost_state y obj_id) \<union> the_set (sep_ghost_state z obj_id))) obj_y)) (object_clean_fields obj_x (sep_ghost_state x obj_id)))))))
 2. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z; \<not> has_slots obj_y\<rbrakk> \<Longrightarrow> \<not> has_slots obj_x
 3. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z\<rbrakk> \<Longrightarrow> \<not> has_slots obj_y proof (prove)
goal (2 subgoals):
 1. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z; \<not> has_slots obj_y; has_slots obj_x\<rbrakk> \<Longrightarrow> False
 2. \<And>obj_id obj_y obj_x obj_z. \<lbrakk>sep_heap x obj_id = Some obj_x; sep_heap y obj_id = Some obj_y; sep_heap z obj_id = Some obj_z; object_type obj_x = object_type obj_z; sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}; object_type obj_y = object_type obj_z; sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<not> has_slots obj_z; has_slots obj_y\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!