theory KHeap_DR

lemma cdt_set_update_eq:
assumes dom_onto: "df =  transform_cslot_ptr ` dg"
assumes exc:  "\<forall>x\<in> dg. \<forall>y. transform_cslot_ptr x = transform_cslot_ptr y \<longrightarrow> ((y\<in> dg) \<or> (\<not> cte_at y s))"
assumes ran_map:"\<forall>x\<in>dg. f (transform_cslot_ptr x) = map_option transform_cslot_ptr (g x)"
assumes mdb1:"mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)"
assumes mdb2:"mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update s dg g)) (cdt (abs_cdt_set_update s dg g))"
shows
"cdl_cdt (cdl_cdt_set_update (transform s) df f)  = transform_cdt (abs_cdt_set_update s dg g)" apply (rule ext) apply (simp add:transform_cdt_def) apply (case_tac "x\<in> df") apply (clarsimp,rule sym) apply (clarsimp simp: map_lift_over_eq_cases cdl_cdt_set_update_def abs_cdt_set_update_def split:option.splits| rule conjI)+ using ran_map apply (drule_tac x = "(aa,ba)" in bspec) apply simp apply (clarsimp) apply (frule dom_onto[THEN dom_onto_ex]) apply clarsimp using exc apply (drule_tac x ="(ab,bb)" in bspec,simp) apply (drule_tac x ="(aa,ba)" in spec) apply clarsimp apply (rule classical) apply clarsimp apply (drule mdb_cte_atD[OF _ mdb1]) apply (clarsimp simp:cte_wp_at_cte_at) apply (drule dom_onto[THEN dom_onto_ex]) apply clarsimp apply (rule_tac x = aa in exI,rule_tac x = ba in exI) apply clarsimp using ran_map apply (drule_tac x = "(aa,ba)" in bspec) apply simp apply (clarsimp simp:option_map_def split:option.splits) using transform_cdt_slot_inj_on_mdb_cte_at[OF mdb2] apply (clarsimp simp:domI abs_cdt_set_update_def) apply (clarsimp simp:cdl_cdt_set_update_def transform_def transform_cdt_def) apply (clarsimp simp:map_lift_over_eq_cases split:option.splits) apply (simp add: transform_cdt_slot_inj_on_mdb_cte_at[OF mdb2] transform_cdt_slot_inj_on_mdb_cte_at[OF mdb1]) apply (clarsimp simp:abs_cdt_set_update_def| rule conjI)+ apply (drule_tac x= aa in spec,drule_tac x = ba in spec) apply (clarsimp split:if_splits) apply (drule dom_onto_is[OF dom_onto]) apply simp apply (clarsimp simp:abs_cdt_set_update_def | rule conjI)+ using dom_onto_is[OF dom_onto] apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_cdt (cdl_cdt_set_update (transform s) df f) = transform_cdt (abs_cdt_set_update s dg g) proof (prove)
goal (1 subgoal):
 1. \<And>x. cdl_cdt (cdl_cdt_set_update (transform s) df f) x = transform_cdt (abs_cdt_set_update s dg g) x proof (prove)
goal (1 subgoal):
 1. \<And>x. cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> df \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) (a, b) = cdl_cdt (cdl_cdt_set_update (transform s) df f) (a, b)
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); (aa, ba) \<in> dg; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> g (aa, ba) = None
 2. \<And>a b aa ba. \<lbrakk>(a, b) \<in> df; f (a, b) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x))\<rbrakk> \<Longrightarrow> (aa, ba) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s (aa, ba) = None
 3. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 4. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
using this:
\<forall>x\<in>dg. f (transform_cslot_ptr x) = map_option transform_cslot_ptr (g x)

goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); (aa, ba) \<in> dg; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> g (aa, ba) = None
 2. \<And>a b aa ba. \<lbrakk>(a, b) \<in> df; f (a, b) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x))\<rbrakk> \<Longrightarrow> (aa, ba) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s (aa, ba) = None
 3. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 4. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); (aa, ba) \<in> dg; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> dg
 2. \<And>a b aa ba. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); (aa, ba) \<in> dg; (a, b) = transform_cslot_ptr (aa, ba); f (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (g (aa, ba))\<rbrakk> \<Longrightarrow> g (aa, ba) = None
 3. \<And>a b aa ba. \<lbrakk>(a, b) \<in> df; f (a, b) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x))\<rbrakk> \<Longrightarrow> (aa, ba) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s (aa, ba) = None
 4. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 5. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); (aa, ba) \<in> dg; (a, b) = transform_cslot_ptr (aa, ba); f (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (g (aa, ba))\<rbrakk> \<Longrightarrow> g (aa, ba) = None
 2. \<And>a b aa ba. \<lbrakk>(a, b) \<in> df; f (a, b) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x))\<rbrakk> \<Longrightarrow> (aa, ba) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s (aa, ba) = None
 3. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 4. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> df; f (a, b) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x))\<rbrakk> \<Longrightarrow> (aa, ba) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> df; f (a, b) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); \<exists>t. transform_cslot_ptr t = (a, b) \<and> t \<in> dg\<rbrakk> \<Longrightarrow> (aa, ba) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba); (ab, bb) \<in> dg; (aa, ba) \<notin> dg; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
using this:
\<forall>x\<in>dg. \<forall>y. transform_cslot_ptr x = transform_cslot_ptr y \<longrightarrow> y \<in> dg \<or> \<not> cte_wp_at (\<lambda>_. True) y s

goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba); (ab, bb) \<in> dg; (aa, ba) \<notin> dg; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba); (ab, bb) \<in> dg; (aa, ba) \<notin> dg; (a, b) = transform_cslot_ptr (aa, ba); \<forall>y. transform_cslot_ptr (ab, bb) = transform_cslot_ptr y \<longrightarrow> y \<in> dg \<or> \<not> cte_wp_at (\<lambda>_. True) y s\<rbrakk> \<Longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba); (ab, bb) \<in> dg; (aa, ba) \<notin> dg; (a, b) = transform_cslot_ptr (aa, ba); transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba) \<longrightarrow> (aa, ba) \<in> dg \<or> \<not> cte_wp_at (\<lambda>_. True) (aa, ba) s\<rbrakk> \<Longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba); (ab, bb) \<in> dg; (aa, ba) \<notin> dg; (a, b) = transform_cslot_ptr (aa, ba); \<not> cte_wp_at (\<lambda>_. True) (aa, ba) s\<rbrakk> \<Longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba); (ab, bb) \<in> dg; (aa, ba) \<notin> dg; (a, b) = transform_cslot_ptr (aa, ba); \<not> cte_wp_at (\<lambda>_. True) (aa, ba) s; cdt s (aa, ba) \<noteq> None\<rbrakk> \<Longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba); (ab, bb) \<in> dg; (aa, ba) \<notin> dg; (a, b) = transform_cslot_ptr (aa, ba); \<not> cte_wp_at (\<lambda>_. True) (aa, ba) s; cdt s (aa, ba) = Some (ac, bc)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>transform_cslot_ptr (aa, ba) \<in> df; f (transform_cslot_ptr (aa, ba)) = None; inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)); transform_cslot_ptr (ab, bb) = transform_cslot_ptr (aa, ba); (ab, bb) \<in> dg; (aa, ba) \<notin> dg; (a, b) = transform_cslot_ptr (aa, ba); \<not> cte_wp_at (\<lambda>_. True) (aa, ba) s; swp (cte_wp_at ((\<noteq>) cap.NullCap)) s (ac, bc) \<and> swp (cte_wp_at ((\<noteq>) cap.NullCap)) s (aa, ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> df \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<exists>t. transform_cslot_ptr t = (a, b) \<and> t \<in> dg \<Longrightarrow> \<forall>aa ba. f (a, b) = Some (aa, ba) \<longrightarrow> (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (ab, bb) = Some (a, b))))
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) = (a, b); (aa, ba) \<in> dg; f (a, b) = Some (ab, bb)\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((aa, ba) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>a b. (ab, bb) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (aa, ba) = Some (a, b))) \<and> ((aa, ba) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>a b. (ab, bb) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (aa, ba) = Some (a, b)))
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) = (a, b); (aa, ba) \<in> dg; f (a, b) = Some (ab, bb)\<rbrakk> \<Longrightarrow> ((aa, ba) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>a b. (ab, bb) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (aa, ba) = Some (a, b))) \<and> ((aa, ba) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (aa, ba) \<and> (\<exists>a b. (ab, bb) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> cdt s (aa, ba) = Some (a, b)))
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) = (a, b); (aa, ba) \<in> dg; f (a, b) = Some (ab, bb)\<rbrakk> \<Longrightarrow> \<exists>a b. (ab, bb) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (aa, ba) = Some (a, b)
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
using this:
\<forall>x\<in>dg. f (transform_cslot_ptr x) = map_option transform_cslot_ptr (g x)

goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) = (a, b); (aa, ba) \<in> dg; f (a, b) = Some (ab, bb)\<rbrakk> \<Longrightarrow> \<exists>a b. (ab, bb) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (aa, ba) = Some (a, b)
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) = (a, b); (aa, ba) \<in> dg; f (a, b) = Some (ab, bb)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> dg
 2. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) = (a, b); (aa, ba) \<in> dg; f (a, b) = Some (ab, bb); f (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (g (aa, ba))\<rbrakk> \<Longrightarrow> \<exists>a b. (ab, bb) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (aa, ba) = Some (a, b)
 3. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) = (a, b); (aa, ba) \<in> dg; f (a, b) = Some (ab, bb); f (transform_cslot_ptr (aa, ba)) = map_option transform_cslot_ptr (g (aa, ba))\<rbrakk> \<Longrightarrow> \<exists>a b. (ab, bb) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x)) \<and> g (aa, ba) = Some (a, b)
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>(ab, bb) = transform_cslot_ptr (ac, bc); transform_cslot_ptr (aa, ba) = (a, b); (aa, ba) \<in> dg; g (aa, ba) = Some (ac, bc); f (a, b) = Some (transform_cslot_ptr (ac, bc))\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x))
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
using this:
inj_on transform_cslot_ptr (dom (cdt (abs_cdt_set_update s dg g)) \<union> ran (cdt (abs_cdt_set_update s dg g)))

goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>(ab, bb) = transform_cslot_ptr (ac, bc); transform_cslot_ptr (aa, ba) = (a, b); (aa, ba) \<in> dg; g (aa, ba) = Some (ac, bc); f (a, b) = Some (transform_cslot_ptr (ac, bc))\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr (dom (\<lambda>x. if x \<in> dg then g x else cdt s x) \<union> ran (\<lambda>x. if x \<in> dg then g x else cdt s x))
 2. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> df \<Longrightarrow> cdl_cdt (cdl_cdt_set_update (transform s) df f) x = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) x proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<notin> df \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) = map_lift_over transform_cslot_ptr (cdt (abs_cdt_set_update s dg g)) (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<notin> df \<Longrightarrow> ((inj_on transform_cslot_ptr (dom (cdt (abs_cdt_set_update s dg g)) \<union> ran (cdt (abs_cdt_set_update s dg g))) \<longrightarrow> (\<forall>aa ba. (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt (abs_cdt_set_update s dg g) (aa, ba) = None)) \<longrightarrow> inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)) \<longrightarrow> (\<forall>aa ba. (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s (aa, ba) = None)) \<and> (\<forall>aa ba. (\<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (cdt (abs_cdt_set_update s dg g)) \<union> ran (cdt (abs_cdt_set_update s dg g))) \<and> cdt (abs_cdt_set_update s dg g) (ab, bb) = Some (a, b))) \<longrightarrow> (\<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)) \<and> cdt s (ab, bb) = Some (a, b)))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<notin> df \<Longrightarrow> ((\<forall>aa ba. (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt (abs_cdt_set_update s dg g) (aa, ba) = None) \<longrightarrow> (\<forall>aa ba. (a, b) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s (aa, ba) = None)) \<and> (\<forall>aa ba. (\<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt (abs_cdt_set_update s dg g) (ab, bb) = Some (a, b))) \<longrightarrow> (\<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b)))) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>transform_cslot_ptr (aa, ba) \<notin> df; \<forall>a b. ((a, b) \<in> dg \<longrightarrow> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> g (a, b) = None) \<and> ((a, b) \<notin> dg \<longrightarrow> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<longrightarrow> cdt s (a, b) = None); (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<notin> df \<Longrightarrow> \<forall>aa ba. (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b)))) \<longrightarrow> (\<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b))) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>transform_cslot_ptr (aa, ba) \<notin> df; (a, b) = transform_cslot_ptr (aa, ba); ((aa, ba) \<in> dg \<longrightarrow> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (aa, ba) \<longrightarrow> g (aa, ba) = None) \<and> ((aa, ba) \<notin> dg \<longrightarrow> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (aa, ba) \<longrightarrow> cdt s (aa, ba) = None)\<rbrakk> \<Longrightarrow> cdt s (aa, ba) = None
 2. \<And>a b. (a, b) \<notin> df \<Longrightarrow> \<forall>aa ba. (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b)))) \<longrightarrow> (\<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b))) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) \<notin> df; (a, b) = transform_cslot_ptr (aa, ba); (aa, ba) \<in> dg; cdt s (aa, ba) = Some (ab, bb); g (aa, ba) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) \<notin> df \<Longrightarrow> \<forall>aa ba. (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b)))) \<longrightarrow> (\<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b))) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>transform_cslot_ptr (aa, ba) \<notin> df; (a, b) = transform_cslot_ptr (aa, ba); cdt s (aa, ba) = Some (ab, bb); g (aa, ba) = None; transform_cslot_ptr (aa, ba) \<in> df\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) \<notin> df \<Longrightarrow> \<forall>aa ba. (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b)))) \<longrightarrow> (\<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<notin> df \<Longrightarrow> \<forall>aa ba. (\<exists>ab bb. ((ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> g (ab, bb) = Some (a, b))) \<and> ((ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b)))) \<longrightarrow> (\<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<notin> df; (ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> g (ab, bb) = Some (a, b)); (ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b))\<rbrakk> \<Longrightarrow> \<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b)) proof (prove)
using this:
?x \<in> dg \<Longrightarrow> transform_cslot_ptr ?x \<in> df

goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<notin> df; (ab, bb) \<in> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> g (ab, bb) = Some (a, b)); (ab, bb) \<notin> dg \<longrightarrow> (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b))\<rbrakk> \<Longrightarrow> \<exists>ab bb. (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b)) proof (prove)
goal:
No subgoals!