theory Frame_SD

lemma sep_map_o_conj:
  "(ptr \<mapsto>o obj \<and>* R) s = (( (sep_heap s) |` ({ptr} \<times> UNIV)
  = object_to_sep_state ptr obj UNIV)
  \<and> R (SepState (sep_heap s |` (UNIV - {ptr}\<times>UNIV))
                (sep_irq_node s)))" apply (clarsimp simp:sep_conj_def Let_def plus_sep_state_def sep_state_add_def
    sep_map_general_def sep_map_o_def) apply (rule iffI) apply (clarsimp simp:sep_map_c_def sep_disj_sep_state_def
     sep_map_general_def sep_state_disj_def map_disj_def) apply (subst dom_object_to_sep_state[where obj = obj,symmetric]) apply (subst map_add_restrict_dom_left) apply (simp add:map_disj_def) apply simp apply (erule arg_cong[where f = R,THEN iffD1,rotated]) apply (case_tac y,clarsimp) apply (rule ext) apply (clarsimp simp: map_add_restrict
     split:option.splits) apply (simp add:dom_object_to_sep_state[where obj = obj,symmetric]) apply (subst restrict_map_univ_disj_eq) apply (fastforce simp:map_disj_def) apply simp apply (rule_tac x = "SepState (object_to_sep_state ptr obj UNIV) Map.empty" in exI) apply (rule_tac x = "SepState (sep_heap s |` (UNIV - {ptr}\<times>UNIV))
                                (sep_irq_node s) " in exI) apply (clarsimp simp:sep_map_c_def sep_disj_sep_state_def
     sep_map_general_def sep_state_disj_def map_disj_def) apply (clarsimp simp:dom_object_to_sep_state) apply (case_tac s,simp) apply (rule ext) apply (case_tac "x \<in> {ptr}\<times>UNIV") apply (drule_tac x = x in fun_cong) apply (clarsimp simp:map_add_def restrict_map_def) apply (clarsimp simp:map_add_def split:option.splits) apply (clarsimp simp:object_to_sep_state_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr \<mapsto>o obj \<and>* R) s = (sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s))) proof (prove)
goal (1 subgoal):
 1. (\<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y) = (sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s))) proof (prove)
goal (2 subgoals):
 1. \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y \<Longrightarrow> sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s))
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> (object_to_sep_state ptr obj UNIV ++ sep_heap y) |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState ((object_to_sep_state ptr obj UNIV ++ sep_heap y) |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node y))
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> (object_to_sep_state ptr obj UNIV ++ sep_heap y) |` dom (object_to_sep_state ptr obj UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState ((object_to_sep_state ptr obj UNIV ++ sep_heap y) |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node y))
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> object_to_sep_state ptr obj UNIV \<bottom> sep_heap y
 2. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> object_to_sep_state ptr obj UNIV = object_to_sep_state ptr obj UNIV \<and> R (SepState ((object_to_sep_state ptr obj UNIV ++ sep_heap y) |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node y))
 3. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> object_to_sep_state ptr obj UNIV = object_to_sep_state ptr obj UNIV \<and> R (SepState ((object_to_sep_state ptr obj UNIV ++ sep_heap y) |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node y))
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> R (SepState ((object_to_sep_state ptr obj UNIV ++ sep_heap y) |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node y))
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> y = SepState ((object_to_sep_state ptr obj UNIV ++ sep_heap y) |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node y)
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom x1 = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ x1) x2; sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> x1 = (object_to_sep_state ptr obj UNIV ++ x1) |` (UNIV - {ptr} \<times> UNIV)
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2 xa. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom x1 = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ x1) x2; sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> x1 xa = ((object_to_sep_state ptr obj UNIV ++ x1) |` (UNIV - {ptr} \<times> UNIV)) xa
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2 a b. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom x1 = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ x1) x2; sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> x1 (a, b) = (object_to_sep_state ptr obj UNIV |` (UNIV - {ptr} \<times> UNIV) ++ x1 |` (UNIV - {ptr} \<times> UNIV)) (a, b)
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2 a b. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom x1 = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ x1) x2; sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> x1 (a, b) = (x1 |` (UNIV - dom (object_to_sep_state ptr obj UNIV))) (a, b)
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (3 subgoals):
 1. \<And>x x1 x2 a b. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom x1 = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ x1) x2; sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> x1 \<bottom> object_to_sep_state ptr obj UNIV
 2. \<And>x x1 x2 a b. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom x1 = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ x1) x2; sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> x1 (a, b) = x1 (a, b)
 3. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2 a b. \<lbrakk>dom (object_to_sep_state ptr obj UNIV) \<inter> dom x1 = {}; s = SepState (object_to_sep_state ptr obj UNIV ++ x1) x2; sep_heap x = object_to_sep_state ptr obj UNIV; sep_irq_node x = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> x1 (a, b) = x1 (a, b)
 2. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (1 subgoal):
 1. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> sep_heap x = object_to_sep_state ptr obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (1 subgoal):
 1. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> \<exists>y. SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None) ## y \<and> s = SepState (sep_heap (SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None)) ++ sep_heap y) (sep_irq_node (SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None)) ++ sep_irq_node y) \<and> sep_heap (SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None)) = object_to_sep_state ptr obj UNIV \<and> sep_irq_node (SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None)) = (\<lambda>x. None) \<and> R y proof (prove)
goal (1 subgoal):
 1. sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) \<Longrightarrow> SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None) ## SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s) \<and> s = SepState (sep_heap (SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None)) ++ sep_heap (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s))) (sep_irq_node (SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None)) ++ sep_irq_node (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s))) \<and> sep_heap (SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None)) = object_to_sep_state ptr obj UNIV \<and> sep_irq_node (SepState (object_to_sep_state ptr obj UNIV) (\<lambda>x. None)) = (\<lambda>x. None) \<and> R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV; R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> dom (object_to_sep_state ptr obj UNIV) \<inter> (dom (sep_heap s) - {ptr} \<times> UNIV) = {} \<and> s = SepState (object_to_sep_state ptr obj UNIV ++ sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV; R (SepState (sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> s = SepState (object_to_sep_state ptr obj UNIV ++ sep_heap s |` (UNIV - {ptr} \<times> UNIV)) (sep_irq_node s) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>x1 |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV; R (SepState (x1 |` (UNIV - {ptr} \<times> UNIV)) x2); s = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 = object_to_sep_state ptr obj UNIV ++ x1 |` (UNIV - {ptr} \<times> UNIV) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x. \<lbrakk>x1 |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV; R (SepState (x1 |` (UNIV - {ptr} \<times> UNIV)) x2); s = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 x = (object_to_sep_state ptr obj UNIV ++ x1 |` (UNIV - {ptr} \<times> UNIV)) x proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x. \<lbrakk>x1 |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV; R (SepState (x1 |` (UNIV - {ptr} \<times> UNIV)) x2); s = SepState x1 x2; x \<in> {ptr} \<times> UNIV\<rbrakk> \<Longrightarrow> x1 x = (object_to_sep_state ptr obj UNIV ++ x1 |` (UNIV - {ptr} \<times> UNIV)) x
 2. \<And>x1 x2 x. \<lbrakk>x1 |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV; R (SepState (x1 |` (UNIV - {ptr} \<times> UNIV)) x2); s = SepState x1 x2; x \<notin> {ptr} \<times> UNIV\<rbrakk> \<Longrightarrow> x1 x = (object_to_sep_state ptr obj UNIV ++ x1 |` (UNIV - {ptr} \<times> UNIV)) x proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x. \<lbrakk>R (SepState (x1 |` (UNIV - {ptr} \<times> UNIV)) x2); s = SepState x1 x2; x \<in> {ptr} \<times> UNIV; (x1 |` ({ptr} \<times> UNIV)) x = object_to_sep_state ptr obj UNIV x\<rbrakk> \<Longrightarrow> x1 x = (object_to_sep_state ptr obj UNIV ++ x1 |` (UNIV - {ptr} \<times> UNIV)) x
 2. \<And>x1 x2 x. \<lbrakk>x1 |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV; R (SepState (x1 |` (UNIV - {ptr} \<times> UNIV)) x2); s = SepState x1 x2; x \<notin> {ptr} \<times> UNIV\<rbrakk> \<Longrightarrow> x1 x = (object_to_sep_state ptr obj UNIV ++ x1 |` (UNIV - {ptr} \<times> UNIV)) x proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x. \<lbrakk>x1 |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV; R (SepState (x1 |` (UNIV - {ptr} \<times> UNIV)) x2); s = SepState x1 x2; x \<notin> {ptr} \<times> UNIV\<rbrakk> \<Longrightarrow> x1 x = (object_to_sep_state ptr obj UNIV ++ x1 |` (UNIV - {ptr} \<times> UNIV)) x proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b. \<lbrakk>x1 |` ({ptr} \<times> UNIV) = object_to_sep_state ptr obj UNIV; R (SepState (x1 |` (UNIV - {ptr} \<times> UNIV)) x2); s = SepState x1 x2; a \<noteq> ptr; x1 (a, b) = None\<rbrakk> \<Longrightarrow> None = object_to_sep_state ptr obj UNIV (a, b) proof (prove)
goal:
No subgoals!