theory KHeap_DR

lemma remove_parent_corres:
  "dcorres dc \<top> (cte_at slot and weak_valid_mdb)
   (remove_parent (transform_cslot_ptr slot))
   (do a \<leftarrow> gets cdt;
           set_cdt
           ((\<lambda>p. if a p = Some slot then a slot else a p)
           (slot := None))
   od)" apply (subst cdl_remove_parent_def'[where slot = "(transform_cslot_ptr slot)"]) apply (subst abs_remove_parent_def') apply (clarsimp simp:bind_def corres_underlying_def simpler_modify_def) apply (cut_tac df=" {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)}"
             and dg = "{x. cdt b x = Some slot}"
    and f = "\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)" and g = "\<lambda>x. cdt b slot"
    and s = b
    in cdt_set_update_eq) defer apply (clarsimp simp: weak_valid_mdb_def) apply (frule(1) mdb_cte_atD) apply (drule sym, subst(asm) transform_cslot_ptr_inj, assumption) apply (clarsimp simp: cte_wp_at_caps_of_state) apply clarsimp defer apply (simp add:weak_valid_mdb_def)+ apply (case_tac slot) apply (fastforce simp:mdb_cte_at_def abs_cdt_set_update_def dom_def) apply (drule transform_cdt_set_update_helper[rotated]) apply simp apply clarsimp apply (rule sym, rule transform_cdt_single_remove_helper) apply simp apply (rule cdt_single_remove_eq) apply (case_tac slot) apply (simp add:weak_valid_mdb_def) apply (fastforce simp:mdb_cte_at_def abs_cdt_set_update_def dom_def) apply ((clarsimp simp:abs_cdt_set_update_def valid_irq_node_def)+)[3] apply (rule set_eqI) apply (clarsimp simp:dom_def image_def | rule conjI)+ apply (rule iffI) apply (clarsimp simp:transform_cdt_def transform_def map_lift_over_eq_Some) apply (clarsimp simp:weak_valid_mdb_def) apply (subst(asm) transform_cslot_ptr_inj, assumption) apply (drule(1) mdb_cte_atD, clarsimp simp: cte_wp_at_caps_of_state) apply fastforce apply (clarsimp simp:weak_valid_mdb_def) apply (subgoal_tac "cte_at (aa,bb) b") apply (drule_tac slot = "(aa,bb)" in transform_cdt_some,simp+) apply (clarsimp simp:transform_def option_map_def split:if_splits option.splits |rule conjI)+ apply (erule mdb_cte_at_cte_wp_at[THEN cte_wp_at_cte_at]) apply simp apply (clarsimp simp:option_map_def split:option.splits|rule conjI)+ apply (drule transform_cdt_none) apply (simp add:weak_valid_mdb_def transform_def)+ apply clarsimp apply (rule transform_cdt_some) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb) (remove_parent (transform_cslot_ptr slot)) (do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb) (modify (\<lambda>s. cdl_cdt_single_remove (cdl_cdt_set_update s {x. if cdl_cdt s x = Some (transform_cslot_ptr slot) then True else False} (\<lambda>x. cdl_cdt s (transform_cslot_ptr slot))) (transform_cslot_ptr slot))) (do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb) (modify (\<lambda>s. cdl_cdt_single_remove (cdl_cdt_set_update s {x. if cdl_cdt s x = Some (transform_cslot_ptr slot) then True else False} (\<lambda>x. cdl_cdt s (transform_cslot_ptr slot))) (transform_cslot_ptr slot))) (modify (\<lambda>s. abs_cdt_single_remove (abs_cdt_set_update s {x. if cdt s x = Some slot then True else False} (\<lambda>x. cdt s slot)) slot)) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot) proof (prove)
goal (6 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. \<forall>y. transform_cslot_ptr x = transform_cslot_ptr y \<longrightarrow> y \<in> {x. cdt b x = Some slot} \<or> \<not> cte_wp_at (\<lambda>_. True) y b
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot)
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 5. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 6. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot) proof (prove)
goal (6 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. \<forall>y. transform_cslot_ptr x = transform_cslot_ptr y \<longrightarrow> y \<in> {x. cdt b x = Some slot} \<or> \<not> cte_wp_at (\<lambda>_. True) y b
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 5. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 6. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot} proof (prove)
goal (6 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (a, ba) = Some slot; transform_cslot_ptr (a, ba) = transform_cslot_ptr (aa, bb); cdt b (aa, bb) \<noteq> Some slot; cte_wp_at (\<lambda>_. True) (aa, bb) b\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 5. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 6. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot} proof (prove)
goal (6 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (a, ba) = Some slot; transform_cslot_ptr (a, ba) = transform_cslot_ptr (aa, bb); cdt b (aa, bb) \<noteq> Some slot; cte_wp_at (\<lambda>_. True) (aa, bb) b; swp (cte_wp_at ((\<noteq>) cap.NullCap)) b slot \<and> swp (cte_wp_at ((\<noteq>) cap.NullCap)) b (a, ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 5. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 6. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot} proof (prove)
goal (7 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (a, ba) = Some slot; cdt b (aa, bb) \<noteq> Some slot; cte_wp_at (\<lambda>_. True) (aa, bb) b; swp (cte_wp_at ((\<noteq>) cap.NullCap)) b slot \<and> swp (cte_wp_at ((\<noteq>) cap.NullCap)) b (a, ba)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, ba) b
 2. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (a, ba) = Some slot; cdt b (aa, bb) \<noteq> Some slot; cte_wp_at (\<lambda>_. True) (aa, bb) b; swp (cte_wp_at ((\<noteq>) cap.NullCap)) b slot \<and> swp (cte_wp_at ((\<noteq>) cap.NullCap)) b (a, ba); (aa, bb) = (a, ba)\<rbrakk> \<Longrightarrow> False
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot)
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 5. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 6. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 7. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot} proof (prove)
goal (6 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (a, ba) = Some slot; cdt b (aa, bb) \<noteq> Some slot; cte_wp_at (\<lambda>_. True) (aa, bb) b; swp (cte_wp_at ((\<noteq>) cap.NullCap)) b slot \<and> swp (cte_wp_at ((\<noteq>) cap.NullCap)) b (a, ba); (aa, bb) = (a, ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 5. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 6. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot} proof (prove)
goal (5 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot)
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 5. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot} proof (prove)
goal (5 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 5. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (4 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> no_mloop (cdt b)\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (4 subgoals):
 1. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> no_mloop (cdt b); slot = (a, ba)\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) = transform_cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (4 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> transform b = transform b
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot))) (transform_cslot_ptr slot)
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> transform (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot) = cdl_cdt_single_remove (transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (transform_cslot_ptr slot)
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (4 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> ?s'95 b = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_remove (?s'95 b) (transform_cslot_ptr slot)) = transform_cdt (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_remove (transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (transform_cslot_ptr slot)) = transform_cdt (abs_cdt_single_remove (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)) slot)
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (4 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (4 subgoals):
 1. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)); slot = (a, ba)\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))) (cdt (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot)))
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (4 subgoals):
 1. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) (a, ba) b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> no_mloop (cdt b); cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr (a, ba))} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr (a, ba))) = transform (abs_cdt_set_update b {x. cdt b x = Some (a, ba)} (\<lambda>x. cdt b (a, ba))); slot = (a, ba)\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) (abs_cdt_set_update b {x. cdt b x = Some (a, ba)} (\<lambda>x. cdt b (a, ba)))) (cdt (abs_cdt_set_update b {x. cdt b x = Some (a, ba)} (\<lambda>x. cdt b (a, ba))))
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt_set_update (transform b) {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} (\<lambda>x. cdl_cdt (transform b) (transform_cslot_ptr slot)) = transform (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot (abs_cdt_set_update b {x. cdt b x = Some slot} (\<lambda>x. cdt b slot))
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)} = transform_cslot_ptr ` {x. cdt b x = Some slot}
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (2 subgoals):
 1. \<And>b x. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> (x \<in> {x. cdl_cdt (transform b) x = Some (transform_cslot_ptr slot)}) = (x \<in> transform_cslot_ptr ` {x. cdt b x = Some slot})
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> (cdl_cdt (transform b) (a, ba) = Some (transform_cslot_ptr slot)) = (\<exists>aa bb. cdt b (aa, bb) = Some slot \<and> (a, ba) = transform_cslot_ptr (aa, bb))
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdl_cdt (transform b) (a, ba) = Some (transform_cslot_ptr slot)\<rbrakk> \<Longrightarrow> \<exists>aa bb. cdt b (aa, bb) = Some slot \<and> (a, ba) = transform_cslot_ptr (aa, bb)
 2. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; \<exists>aa bb. cdt b (aa, bb) = Some slot \<and> (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (a, ba) = Some (transform_cslot_ptr slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba aa bb ab bc. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; (a, ba) = transform_cslot_ptr (aa, bb); transform_cslot_ptr slot = transform_cslot_ptr (ab, bc); inj_on transform_cslot_ptr (dom (cdt b) \<union> ran (cdt b)); cdt b (aa, bb) = Some (ab, bc)\<rbrakk> \<Longrightarrow> \<exists>a ba. cdt b (a, ba) = Some slot \<and> transform_cslot_ptr (aa, bb) = transform_cslot_ptr (a, ba)
 2. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; \<exists>aa bb. cdt b (aa, bb) = Some slot \<and> (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (a, ba) = Some (transform_cslot_ptr slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba aa bb ab bc. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; (a, ba) = transform_cslot_ptr (aa, bb); transform_cslot_ptr slot = transform_cslot_ptr (ab, bc); inj_on transform_cslot_ptr (dom (cdt b) \<union> ran (cdt b)); cdt b (aa, bb) = Some (ab, bc); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b)\<rbrakk> \<Longrightarrow> \<exists>a ba. cdt b (a, ba) = Some slot \<and> transform_cslot_ptr (aa, bb) = transform_cslot_ptr (a, ba)
 2. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; \<exists>aa bb. cdt b (aa, bb) = Some slot \<and> (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (a, ba) = Some (transform_cslot_ptr slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (4 subgoals):
 1. \<And>b a ba aa bb ab bc. \<lbrakk>inj_on transform_cslot_ptr (dom (cdt b) \<union> ran (cdt b)); cdt b (aa, bb) = Some (ab, bc); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cte_wp_at (\<lambda>_. True) slot b; (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ab, bc) b
 2. \<And>b a ba aa bb ab bc. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; (a, ba) = transform_cslot_ptr (aa, bb); slot = (ab, bc); inj_on transform_cslot_ptr (dom (cdt b) \<union> ran (cdt b)); cdt b (aa, bb) = Some (ab, bc); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b)\<rbrakk> \<Longrightarrow> \<exists>a ba. cdt b (a, ba) = Some slot \<and> transform_cslot_ptr (aa, bb) = transform_cslot_ptr (a, ba)
 3. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; \<exists>aa bb. cdt b (aa, bb) = Some slot \<and> (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (a, ba) = Some (transform_cslot_ptr slot)
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba aa bb ab bc. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; (a, ba) = transform_cslot_ptr (aa, bb); slot = (ab, bc); inj_on transform_cslot_ptr (dom (cdt b) \<union> ran (cdt b)); cdt b (aa, bb) = Some (ab, bc); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b)\<rbrakk> \<Longrightarrow> \<exists>a ba. cdt b (a, ba) = Some slot \<and> transform_cslot_ptr (aa, bb) = transform_cslot_ptr (a, ba)
 2. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; \<exists>aa bb. cdt b (aa, bb) = Some slot \<and> (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (a, ba) = Some (transform_cslot_ptr slot)
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; \<exists>aa bb. cdt b (aa, bb) = Some slot \<and> (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (a, ba) = Some (transform_cslot_ptr slot)
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (aa, bb) = Some slot; (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (transform_cslot_ptr (aa, bb)) = Some (transform_cslot_ptr slot)
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (aa, bb) = Some slot; (a, ba) = transform_cslot_ptr (aa, bb); cte_wp_at (\<lambda>_. True) (aa, bb) b\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (transform_cslot_ptr (aa, bb)) = Some (transform_cslot_ptr slot)
 2. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (aa, bb) = Some slot; (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, bb) b
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; no_mloop (cdt b); cdt b (aa, bb) = Some slot; (a, ba) = transform_cslot_ptr (aa, bb); cte_wp_at (\<lambda>_. True) (aa, bb) b; transform_cdt b (transform_cslot_ptr (aa, bb)) = Some (transform_cslot_ptr slot)\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (transform_cslot_ptr (aa, bb)) = Some (transform_cslot_ptr slot)
 2. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (aa, bb) = Some slot; (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, bb) b
 3. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b (aa, bb) = Some slot; (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, bb) b
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; no_mloop (cdt b); cdt b (aa, bb) = Some slot; (a, ba) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> cdt b (aa, bb) = Some (?slot'178 b a ba aa bb)
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>x\<in>{x. cdt b x = Some slot}. cdl_cdt (transform b) (transform_cslot_ptr slot) = map_option transform_cslot_ptr (cdt b slot) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b; cdt b slot = None; cdt b (a, ba) = Some slot\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (transform_cslot_ptr slot) = None
 2. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>a ba. cdt b slot = Some (a, ba) \<longrightarrow> (\<exists>a ba. cdt b (a, ba) = Some slot) \<longrightarrow> cdl_cdt (transform b) (transform_cslot_ptr slot) = Some (transform_cslot_ptr (a, ba)) proof (prove)
goal (4 subgoals):
 1. \<And>b a ba. \<lbrakk>weak_valid_mdb b; cdt b slot = None; cdt b (a, ba) = Some slot\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; cdt b slot = None; cdt b (a, ba) = Some slot\<rbrakk> \<Longrightarrow> cdt b slot = None
 3. \<And>b a ba. \<lbrakk>weak_valid_mdb b; cdt b slot = None; cdt b (a, ba) = Some slot; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> cdl_cdt (transform b) (transform_cslot_ptr slot) = None
 4. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; weak_valid_mdb b\<rbrakk> \<Longrightarrow> \<forall>a ba. cdt b slot = Some (a, ba) \<longrightarrow> (\<exists>a ba. cdt b (a, ba) = Some slot) \<longrightarrow> cdl_cdt (transform b) (transform_cslot_ptr slot) = Some (transform_cslot_ptr (a, ba)) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> no_mloop (cdt b)\<rbrakk> \<Longrightarrow> \<forall>a ba. cdt b slot = Some (a, ba) \<longrightarrow> (\<exists>a ba. cdt b (a, ba) = Some slot) \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = Some (transform_cslot_ptr (a, ba)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b slot = Some (a, ba); cdt b (aa, bb) = Some slot\<rbrakk> \<Longrightarrow> transform_cdt b (transform_cslot_ptr slot) = Some (transform_cslot_ptr (a, ba)) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b slot = Some (a, ba); cdt b (aa, bb) = Some slot\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 2. \<And>b a ba aa bb. \<lbrakk>cte_wp_at (\<lambda>_. True) slot b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); no_mloop (cdt b); cdt b slot = Some (a, ba); cdt b (aa, bb) = Some slot\<rbrakk> \<Longrightarrow> cdt b slot = Some (a, ba) proof (prove)
goal:
No subgoals!