theory CSpace_R

lemma cteInsert_untyped_inc':
  "\<lbrace>valid_mdb' and pspace_distinct' and pspace_aligned' and valid_objs' and (\<lambda>s. src \<noteq> dest) and
    (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace>
  cteInsert cap src dest
  \<lbrace>\<lambda>_ s. untyped_inc' (ctes_of s)\<rbrace>" apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: if_split) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of
    setUntypedCapAsFull_ctes_of_no_0 mdb_inv_preserve_modify_map
    setUntypedCapAsFull_untyped_mdb' mdb_inv_preserve_fun_upd) apply (wp getCTE_wp setUntypedCapAsFull_ctes)+ apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) apply (subgoal_tac "src \<noteq> 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (subgoal_tac "dest \<noteq> 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (rule conjI) apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (case_tac cte) apply (rename_tac s_cap s_node) apply (case_tac cteb) apply (rename_tac d_cap d_node) apply (simp add: nullPointer_def) apply (subgoal_tac "mdb_insert_der
    (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))
    src (maskedAsFull s_cap cap) s_node dest NullCap d_node cap") prefer 2 apply unfold_locales[1] apply (clarsimp simp:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (erule(2) valid_mdb_ctesE[OF valid_mdb_ctes_maskedAsFull]) apply (clarsimp simp:modify_map_def) apply (erule(2) valid_mdb_ctesE[OF valid_mdb_ctes_maskedAsFull]) apply simp apply (clarsimp simp:modify_map_def maskedAsFull_derived') apply (case_tac "isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap
                   (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap)
                   (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap)
                   (mdbPrev_update (\<lambda>a. src) s_node))))") apply (subgoal_tac "mdb_insert_child
     (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))
     src (maskedAsFull s_cap cap) s_node dest NullCap d_node cap") prefer 2 apply (simp add: mdb_insert_child_def mdb_insert_child_axioms_def) apply (drule mdb_insert_child.untyped_inc_n) apply (rule capAligned_maskedAsFull[OF valid_capAligned]) apply (erule(1) ctes_of_valid_cap') apply (intro impI maskedAsFull_usable_empty) apply (clarsimp simp:is_derived'_def badge_derived'_def) apply simp apply (clarsimp simp: modify_map_apply untyped_inc_prev_update maskedAsFull_revokable
                         descendants_of_prev_update) apply (subgoal_tac "mdb_insert_sib
    (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))
    src (maskedAsFull s_cap cap) s_node dest NullCap d_node cap") prefer 2 apply (simp add: mdb_insert_sib_def mdb_insert_sib_axioms_def) apply (drule mdb_insert_sib.untyped_inc_n) apply (rule capAligned_master[OF valid_capAligned]) apply (erule(1) ctes_of_valid_cap') apply (clarsimp simp:is_derived'_def badge_derived'_def) apply (clarsimp simp: modify_map_apply untyped_inc_prev_update maskedAsFull_revokable
                        descendants_of_prev_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and pspace_distinct' and pspace_aligned' and valid_objs' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_ s. untyped_inc' (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and pspace_distinct' and pspace_aligned' and valid_objs' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> do srcCTE <- getCTE src;
srcMDB <- return (cteMDBNode srcCTE);
srcCap <- return (cteCap srcCTE);
newCapIsRevocable <- return (revokable' srcCap cap);
newMDB <- return (mdbFirstBadged_update (\<lambda>_. newCapIsRevocable) (mdbRevocable_update (\<lambda>_. newCapIsRevocable) (mdbPrev_update (\<lambda>_. src) srcMDB)));
oldCTE <- getCTE dest;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
setUntypedCapAsFull srcCap cap src;
do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
updateMDB dest (const newMDB);
updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext newMDB) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>_ s. untyped_inc' (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_distinct' and pspace_aligned' and valid_objs' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>_ s. untyped_inc' (ctes_of s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x y ya. \<lbrace>?B4 srcCTE x y ya\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. \<forall>cte. cte_wp_at' ((=) cte) dest s \<longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) \<and> no_0 (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) \<and> no_0 (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) \<and> untyped_inc' (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))\<rbrace>
 2. \<And>srcCTE x y. \<lbrace>?B3 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B4 srcCTE x y\<rbrace>
 3. \<And>srcCTE x. \<lbrace>?B2 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B3 srcCTE x\<rbrace>
 4. \<And>srcCTE. \<lbrace>?B1 srcCTE\<rbrace> getCTE dest \<lbrace>?B2 srcCTE\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE src \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_distinct' and pspace_aligned' and valid_objs' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x. \<lbrace>?B4 srcCTE x () ()\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. \<forall>cte. ctes_of s dest = Some cte \<longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) \<and> untyped_inc' (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))\<rbrace>
 2. \<And>srcCTE x y. \<lbrace>?B3 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B4 srcCTE x y\<rbrace>
 3. \<And>srcCTE x. \<lbrace>?B2 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B3 srcCTE x\<rbrace>
 4. \<And>srcCTE. \<lbrace>?B1 srcCTE\<rbrace> getCTE dest \<lbrace>?B2 srcCTE\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE src \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_distinct' and pspace_aligned' and valid_objs' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x cte. \<lbrace>?P'38 srcCTE x () () cte\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>rv s. untyped_inc' (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))\<rbrace>
 2. \<And>srcCTE x y. \<lbrace>?B3 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>\<lambda>a b. \<forall>xa. (src \<noteq> dest \<and> ctes_of b dest \<noteq> Some xa \<or> src = dest \<and> Some (CTE (maskedAsFull (cteCap srcCTE) cap) (cteMDBNode srcCTE)) \<noteq> Some xa \<and> cte_wp_at' ((=) srcCTE) src b) \<or> (no_0 ((ctes_of b)(dest \<mapsto> cteCap_update (\<lambda>_. cap) xa)) \<and> cte_wp_at' ((=) srcCTE) src b) \<and> ?P'38 srcCTE x y a xa b\<rbrace>
 3. \<And>srcCTE x. \<lbrace>?B2 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B3 srcCTE x\<rbrace>
 4. \<And>srcCTE. \<lbrace>?B1 srcCTE\<rbrace> getCTE dest \<lbrace>?B2 srcCTE\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE src \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_distinct' and pspace_aligned' and valid_objs' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_distinct' and pspace_aligned' and valid_objs' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (cteCap ctea = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> (\<forall>x. (src \<noteq> dest \<and> ctes_of s dest \<noteq> Some x \<or> src = dest \<and> Some (CTE (maskedAsFull (cteCap cte) cap) (cteMDBNode cte)) \<noteq> Some x \<and> cte_wp_at' ((=) cte) src s) \<or> (no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> cte_wp_at' ((=) cte) src s) \<and> cte_wp_at' (\<lambda>c. c = cte) src s \<and> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) \<and> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) \<and> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> src \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> src \<noteq> 0
 2. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) \<and> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) \<and> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) \<and> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> dest \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 2. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) \<and> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) \<and> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb))
 2. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb s_cap s_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE d_cap d_node\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap)))(dest \<mapsto> cteCap_update (\<lambda>_. cap) cteb)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (11 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)) src = Some (CTE (maskedAsFull s_cap cap) s_node)
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)) dest = Some (CTE capability.NullCap d_node)
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> capability.NullCap = capability.NullCap
 5. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> mdbPrev d_node = 0
 6. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> mdbNext d_node = 0
 7. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> valid_badges (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))
 8. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> ut_revocable' (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))
 9. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> src \<noteq> dest
 10. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src cap (maskedAsFull s_cap cap)
A total of 11 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>s s_cap s_node d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> valid_badges ((ctes_of s)(src \<mapsto> CTE (maskedAsFull s_cap cap) s_node))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> ut_revocable' (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> src \<noteq> dest
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src cap (maskedAsFull s_cap cap)
 5. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> ut_revocable' (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> src \<noteq> dest
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src cap (maskedAsFull s_cap cap)
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (4 subgoals):
 1. \<And>s s_cap s_node d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> ut_revocable' ((ctes_of s)(src \<mapsto> CTE (maskedAsFull s_cap cap) s_node))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> src \<noteq> dest
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src cap (maskedAsFull s_cap cap)
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> src \<noteq> dest
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src cap (maskedAsFull s_cap cap)
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src cap (maskedAsFull s_cap cap)
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); mdb_insert_child (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> mdb_insert_child (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> mdb_insert_child (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); mdb_insert_child (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); mdb_insert_child (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> capAligned (maskedAsFull s_cap cap)
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> isUntypedCap (maskedAsFull s_cap cap) \<longrightarrow> usableUntypedRange (maskedAsFull s_cap cap) = {}
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> valid_cap' s_cap (?s130 s cte cteb s_cap s_node d_cap d_node)
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> isUntypedCap (maskedAsFull s_cap cap) \<longrightarrow> usableUntypedRange (maskedAsFull s_cap cap) = {}
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> isUntypedCap (maskedAsFull s_cap cap) \<longrightarrow> usableUntypedRange (maskedAsFull s_cap cap) = {}
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); isUntypedCap (maskedAsFull s_cap cap)\<rbrakk> \<Longrightarrow> capMasterCap cap = capMasterCap s_cap
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); isUntypedCap (maskedAsFull s_cap cap)\<rbrakk> \<Longrightarrow> isUntypedCap (maskedAsFull s_cap cap)
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); isUntypedCap (maskedAsFull s_cap cap)\<rbrakk> \<Longrightarrow> isUntypedCap (maskedAsFull s_cap cap)
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); mdb_insert_sib (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> mdb_insert_sib (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> mdb_insert_sib (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); mdb_insert_sib (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); mdb_insert_sib (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> capAligned cap
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> valid_cap' (?cap140 s cte cteb s_cap s_node d_cap d_node) (?s141 s cte cteb s_cap s_node d_cap d_node)
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> capMasterCap (?cap140 s cte cteb s_cap s_node d_cap d_node) = capMasterCap cap
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))\<rbrakk> \<Longrightarrow> capMasterCap s_cap = capMasterCap cap
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; valid_objs' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest capability.NullCap d_node cap; \<not> isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node)))); untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\<lambda>a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> untyped_inc' (modify_map (modify_map (modify_map ((modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull s_cap cap)))(dest \<mapsto> CTE cap d_node)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal:
No subgoals!