theory Ipc_R

lemma cteInsert_cte_wp_at:
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s
       \<and> valid_mdb' s \<and> valid_objs' s
       \<and> (if p = dest then P cap
            else cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s)\<rbrace>
    cteInsert cap src dest
   \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>" apply (simp add: cteInsert_def) apply (wp updateMDB_weak_cte_wp_at updateCap_cte_wp_at_cases getCTE_wp hoare_weak_lift_imp
         | clarsimp simp: comp_def
         | unfold setUntypedCapAsFull_def)+ apply (drule cte_at_cte_wp_atD) apply (elim exE) apply (rule_tac x=cte in exI) apply clarsimp apply (drule cte_at_cte_wp_atD) apply (elim exE) apply (rule_tac x=ctea in exI) apply clarsimp apply (cases "p=dest") apply (clarsimp simp: cte_wp_at'_def) apply (cases "p=src") apply clarsimp apply (intro conjI impI) apply ((clarsimp simp: cte_wp_at'_def maskedAsFull_def split: if_split_asm)+)[2] apply clarsimp apply (rule conjI) apply (clarsimp simp: maskedAsFull_def cte_wp_at_ctes_of split:if_split_asm) apply (erule disjE) prefer 2 apply simp apply (clarsimp simp: is_derived'_def isCap_simps) apply (drule valid_mdb_untyped_incD') apply (case_tac cte, case_tac cteb, clarsimp) apply (drule untyped_incD', (simp add: isCap_simps)+) apply (frule(1) ctes_of_valid'[where p = p]) apply (clarsimp simp:valid_cap'_def capAligned_def split:if_splits) apply (drule_tac y ="of_nat fb"  in word_plus_mono_right[OF _  is_aligned_no_overflow',rotated]) apply simp+ apply (rule word_of_nat_less) apply simp apply (simp add:p_assoc_help) apply (simp add: max_free_index_def) apply (clarsimp simp: maskedAsFull_def is_derived'_def badge_derived'_def
                        isCap_simps capMasterCap_def cte_wp_at_ctes_of
                  split: if_split_asm capability.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> (if p = dest then P cap else cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap) \<and> (p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p 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 <- updateCap dest cap;
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>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' (\<lambda>_. True) src s\<rbrakk> \<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> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; \<exists>cte. cte_wp_at' ((=) cte) src s\<rbrakk> \<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> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s\<rbrakk> \<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> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) cte) src s \<and> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' (\<lambda>_. True) dest s\<rbrakk> \<Longrightarrow> \<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; \<exists>cte. cte_wp_at' ((=) cte) dest s\<rbrakk> \<Longrightarrow> \<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s\<rbrakk> \<Longrightarrow> \<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) ctea) dest s \<and> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p = dest\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s))
 2. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s))
 2. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; src \<noteq> dest; p = src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) src s\<rbrakk> \<Longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) src s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) src s)
 2. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; src \<noteq> dest; p = src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) src s; isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap; mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) src s
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; src \<noteq> dest; p = src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) src s; capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap; mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) src s
 3. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>p = dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> P cap; p \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>a. True) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. True) p s)) \<and> (dest \<noteq> p \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (src = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>x. P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) p s) \<and> (src \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea cteb. \<lbrakk>ctes_of s src = Some cte; ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; is_derived' (ctes_of s) src cap (cteCap cte); valid_mdb' s; valid_objs' s; capBlockSize (cteCap cteb) = capBlockSize cap \<longrightarrow> capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> ctes_of s p = Some cteb \<and> P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb)); capPtr (cteCap cteb) = capPtr cap \<and> isUntypedCap (cteCap cteb) \<and> capBlockSize (cteCap cteb) = capBlockSize cap \<or> ctes_of s p = Some cteb \<and> P (cteCap cteb); isUntypedCap (cteCap cte); isUntypedCap cap; capPtr (cteCap cte) = capPtr cap; capBlockSize (cteCap cte) = capBlockSize cap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte)
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea cteb. \<lbrakk>ctes_of s src = Some cte; ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; is_derived' (ctes_of s) src cap (cteCap cte); valid_mdb' s; valid_objs' s; capBlockSize (cteCap cteb) = capBlockSize cap \<longrightarrow> capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> ctes_of s p = Some cteb \<and> P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb)); isUntypedCap (cteCap cte); isUntypedCap cap; capPtr (cteCap cte) = capPtr cap; capBlockSize (cteCap cte) = capBlockSize cap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; capPtr (cteCap cteb) = capPtr cap \<and> isUntypedCap (cteCap cteb) \<and> capBlockSize (cteCap cteb) = capBlockSize cap\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte)
 2. \<And>s cte ctea cteb. \<lbrakk>ctes_of s src = Some cte; ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; is_derived' (ctes_of s) src cap (cteCap cte); valid_mdb' s; valid_objs' s; capBlockSize (cteCap cteb) = capBlockSize cap \<longrightarrow> capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> ctes_of s p = Some cteb \<and> P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb)); isUntypedCap (cteCap cte); isUntypedCap cap; capPtr (cteCap cte) = capPtr cap; capBlockSize (cteCap cte) = capBlockSize cap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; ctes_of s p = Some cteb \<and> P (cteCap cteb)\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte)
 3. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea cteb. \<lbrakk>ctes_of s src = Some cte; ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; is_derived' (ctes_of s) src cap (cteCap cte); valid_mdb' s; valid_objs' s; capBlockSize (cteCap cteb) = capBlockSize cap \<longrightarrow> capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> ctes_of s p = Some cteb \<and> P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb)); isUntypedCap (cteCap cte); isUntypedCap cap; capPtr (cteCap cte) = capPtr cap; capBlockSize (cteCap cte) = capBlockSize cap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; ctes_of s p = Some cteb \<and> P (cteCap cteb)\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte)
 2. \<And>s cte ctea cteb. \<lbrakk>ctes_of s src = Some cte; ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; is_derived' (ctes_of s) src cap (cteCap cte); valid_mdb' s; valid_objs' s; capBlockSize (cteCap cteb) = capBlockSize cap \<longrightarrow> capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> ctes_of s p = Some cteb \<and> P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb)); isUntypedCap (cteCap cte); isUntypedCap cap; capPtr (cteCap cte) = capPtr cap; capBlockSize (cteCap cte) = capBlockSize cap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; capPtr (cteCap cteb) = capPtr cap \<and> isUntypedCap (cteCap cteb) \<and> capBlockSize (cteCap cteb) = capBlockSize cap\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte)
 3. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea cteb. \<lbrakk>ctes_of s src = Some cte; ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; is_derived' (ctes_of s) src cap (cteCap cte); valid_mdb' s; valid_objs' s; capBlockSize (cteCap cteb) = capBlockSize cap \<longrightarrow> capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> ctes_of s p = Some cteb \<and> P (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb)); isUntypedCap (cteCap cte); isUntypedCap cap; capPtr (cteCap cte) = capPtr cap; capBlockSize (cteCap cte) = capBlockSize cap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; capPtr (cteCap cteb) = capPtr cap \<and> isUntypedCap (cteCap cteb) \<and> capBlockSize (cteCap cteb) = capBlockSize cap\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte)
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea cteb d da v0a v1a f fa db fb. \<lbrakk>ctes_of s src = Some cte; ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_mdb' s; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cteCap cte = capability.UntypedCap d v0a v1a f; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some cteb; P (capability.UntypedCap db v0a v1a (max_free_index v1a)); cteCap cteb = capability.UntypedCap db v0a v1a fb; badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea cteb d da v0a v1a f fa db fb. \<lbrakk>ctes_of s src = Some cte; ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cteCap cte = capability.UntypedCap d v0a v1a f; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some cteb; P (capability.UntypedCap db v0a v1a (max_free_index v1a)); cteCap cteb = capability.UntypedCap db v0a v1a fb; badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s ctea d da v0a v1a f fa db fb x2 x2a. \<lbrakk>ctes_of s src = Some (CTE (capability.UntypedCap d v0a v1a f) x2); ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); src \<in> descendants_of' p (ctes_of s) \<and> (if fb < 2 ^ v1a then {v0a + word_of_nat fb..v0a + 2 ^ v1a - 1} else {}) = {}\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); src \<in> descendants_of' p (ctes_of s) \<and> (if fb < 2 ^ v1a then {v0a + word_of_nat fb..v0a + 2 ^ v1a - 1} else {}) = {}; valid_cap' (cteCap (CTE (capability.UntypedCap db v0a v1a fb) x2a)) s\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (3 subgoals):
 1. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); fb < 2 ^ v1a; is_aligned v0a v1a; v1a < word_bits; valid_untyped' db v0a v1a fb s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (word_of_nat fb) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s); \<not> v0a + word_of_nat fb \<le> v0a + 2 ^ v1a - 1\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 2. \<And>s ctea d da v0a v1a f fa db x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a (2 ^ v1a)) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); is_aligned v0a v1a; v1a < word_bits; valid_untyped' db v0a v1a (2 ^ v1a) s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (2 ^ v1a) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a (2 ^ v1a))
 3. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (4 subgoals):
 1. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); fb < 2 ^ v1a; v1a < word_bits; valid_untyped' db v0a v1a fb s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (word_of_nat fb) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s); \<not> v0a + word_of_nat fb \<le> v0a + 2 ^ v1a - 1\<rbrakk> \<Longrightarrow> word_of_nat fb \<le> 2 ^ v1a - 1
 2. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); fb < 2 ^ v1a; v1a < word_bits; valid_untyped' db v0a v1a fb s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (word_of_nat fb) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s); \<not> v0a + word_of_nat fb \<le> v0a + 2 ^ v1a - 1; v0a + word_of_nat fb \<le> v0a + (2 ^ v1a - 1)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 3. \<And>s ctea d da v0a v1a f fa db x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a (2 ^ v1a)) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); is_aligned v0a v1a; v1a < word_bits; valid_untyped' db v0a v1a (2 ^ v1a) s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (2 ^ v1a) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a (2 ^ v1a))
 4. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (4 subgoals):
 1. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); fb < 2 ^ v1a; v1a < word_bits; valid_untyped' db v0a v1a fb s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (word_of_nat fb) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s); \<not> v0a + word_of_nat fb \<le> v0a + 2 ^ v1a - 1\<rbrakk> \<Longrightarrow> word_of_nat fb < 2 ^ v1a
 2. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); fb < 2 ^ v1a; v1a < word_bits; valid_untyped' db v0a v1a fb s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (word_of_nat fb) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s); \<not> v0a + word_of_nat fb \<le> v0a + 2 ^ v1a - 1; v0a + word_of_nat fb \<le> v0a + (2 ^ v1a - 1)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 3. \<And>s ctea d da v0a v1a f fa db x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a (2 ^ v1a)) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); is_aligned v0a v1a; v1a < word_bits; valid_untyped' db v0a v1a (2 ^ v1a) s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (2 ^ v1a) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a (2 ^ v1a))
 4. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (4 subgoals):
 1. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); fb < 2 ^ v1a; v1a < word_bits; valid_untyped' db v0a v1a fb s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (word_of_nat fb) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s); \<not> v0a + word_of_nat fb \<le> v0a + 2 ^ v1a - 1\<rbrakk> \<Longrightarrow> fb < unat (2 ^ v1a)
 2. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); fb < 2 ^ v1a; v1a < word_bits; valid_untyped' db v0a v1a fb s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (word_of_nat fb) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s); \<not> v0a + word_of_nat fb \<le> v0a + 2 ^ v1a - 1; v0a + word_of_nat fb \<le> v0a + (2 ^ v1a - 1)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 3. \<And>s ctea d da v0a v1a f fa db x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a (2 ^ v1a)) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); is_aligned v0a v1a; v1a < word_bits; valid_untyped' db v0a v1a (2 ^ v1a) s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (2 ^ v1a) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a (2 ^ v1a))
 4. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (3 subgoals):
 1. \<And>s ctea d da v0a v1a f fa db fb x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a fb) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); fb < 2 ^ v1a; v1a < word_bits; valid_untyped' db v0a v1a fb s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (word_of_nat fb) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s); \<not> v0a + word_of_nat fb \<le> v0a + 2 ^ v1a - 1; v0a + word_of_nat fb \<le> v0a + (2 ^ v1a - 1)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a fb)
 2. \<And>s ctea d da v0a v1a f fa db x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a (2 ^ v1a)) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); is_aligned v0a v1a; v1a < word_bits; valid_untyped' db v0a v1a (2 ^ v1a) s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (2 ^ v1a) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a (2 ^ v1a))
 3. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (2 subgoals):
 1. \<And>s ctea d da v0a v1a f fa db x2a. \<lbrakk>ctes_of s dest = Some ctea; p \<noteq> dest; p \<noteq> src; valid_objs' s; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cteCap ctea = capability.NullCap; cap = capability.UntypedCap da v0a v1a fa; ctes_of s p = Some (CTE (capability.UntypedCap db v0a v1a (2 ^ v1a)) x2a); P (capability.UntypedCap db v0a v1a (max_free_index v1a)); badge_derived' (capability.UntypedCap da v0a v1a fa) (capability.UntypedCap d v0a v1a f); descendants_of' src (ctes_of s) = {}; vsCapRef (capability.UntypedCap d v0a v1a f) = vsCapRef (capability.UntypedCap da v0a v1a fa); untyped_inc' (ctes_of s); is_aligned v0a v1a; v1a < word_bits; valid_untyped' db v0a v1a (2 ^ v1a) s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; is_aligned (2 ^ v1a) minUntypedSizeBits; src \<in> descendants_of' p (ctes_of s)\<rbrakk> \<Longrightarrow> P (capability.UntypedCap db v0a v1a (2 ^ v1a))
 2. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) dest s; p \<noteq> dest; p \<noteq> src; cte_wp_at' (\<lambda>c. is_derived' (ctes_of s) src cap (cteCap c)) src s; valid_mdb' s; valid_objs' s; cte_wp_at' (\<lambda>c. P (maskedAsFull (cteCap c) cap)) p s\<rbrakk> \<Longrightarrow> (capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s proof (prove)
goal:
No subgoals!