theory CSpace_R

lemma cteInsert_ifunsafe'[wp]:
  "\<lbrace>if_unsafe_then_cap' and cte_wp_at' (\<lambda>c. cteCap c = NullCap) dest
        and ex_cte_cap_to' dest\<rbrace>
     cteInsert cap src dest
   \<lbrace>\<lambda>rv s. if_unsafe_then_cap' s\<rbrace>" apply (simp add: ifunsafe'_def3 cteInsert_def setUntypedCapAsFull_def
             split del: if_split) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_to'_def
                        cteCaps_of_def
                 dest!: modify_map_K_D
                 split: if_split_asm) apply (intro conjI) apply clarsimp apply (erule_tac x = crefa in allE) apply (clarsimp simp:modify_map_def split:if_split_asm) apply (rule_tac x = cref in exI) apply fastforce apply (clarsimp simp:isCap_simps) apply (rule_tac x = cref' in exI) apply fastforce apply (intro conjI impI) apply clarsimp apply (rule_tac x = cref' in exI) apply fastforce apply (clarsimp simp:modify_map_def) apply (erule_tac x = crefa in allE) apply (intro conjI impI) apply clarsimp apply (rule_tac x = cref in exI) apply fastforce apply (clarsimp simp:isCap_simps) apply (rule_tac x = cref' in exI) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest and ex_cte_cap_wp_to' (\<lambda>_. True) dest\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest and ex_cte_cap_wp_to' (\<lambda>_. True) dest\<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 <- if isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap then updateCap src (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) else return ();
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>rv s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest and ex_cte_cap_wp_to' (\<lambda>_. True) dest) 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> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte)))) dest (K cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte)))) dest (K cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))) \<and> (\<not> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) dest (K cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) dest (K cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (isUntypedCap (cteCap cteb) \<and> isUntypedCap cap \<and> capPtr (cteCap cteb) = capPtr cap \<and> capBlockSize (cteCap cteb) = capBlockSize cap \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) src (\<lambda>y. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb))) dest (\<lambda>a. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) src (\<lambda>y. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb))) dest (\<lambda>a. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))) \<and> ((capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cteb) \<and> isUntypedCap cap \<and> capPtr (cteCap cteb) = capPtr cap \<and> capBlockSize (cteCap cteb) = capBlockSize cap \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) src (\<lambda>y. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb))) dest (\<lambda>a. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) src (\<lambda>y. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb))) dest (\<lambda>a. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea cteb crefa capa. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) src (\<lambda>y. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb))) dest (\<lambda>a. cap) crefa = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) src (\<lambda>y. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb))) dest (\<lambda>a. cap) cref' = Some cap' \<and> crefa \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea cteb crefa capa. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) src (\<lambda>y. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb))) dest (\<lambda>a. cap) crefa = Some capa; capa \<noteq> capability.NullCap; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) src (\<lambda>y. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb))) dest (\<lambda>a. cap) cref' = Some cap' \<and> crefa \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte cref ctea cteb. \<lbrakk>cap \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; dest \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = src \<longrightarrow> dest \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> dest \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> dest \<in> cte_refs' cap' (irq_node' s))))
 2. \<And>s cte cref ctea cteb. \<lbrakk>capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb) \<noteq> capability.NullCap; cteCap cteb \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; src \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = src \<longrightarrow> src \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> src \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s))))
 3. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> (dest = src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) \<and> (dest \<noteq> src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))))
 4. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte cref ctea cteb. \<lbrakk>cap \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; dest \<noteq> src\<rbrakk> \<Longrightarrow> (cref = src \<longrightarrow> dest \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref \<noteq> src \<longrightarrow> (cref = dest \<longrightarrow> dest \<in> cte_refs' cap (irq_node' s)) \<and> (cref \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap') \<and> dest \<in> cte_refs' cap' (irq_node' s))))
 2. \<And>s cte cref ctea cteb. \<lbrakk>capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb) \<noteq> capability.NullCap; cteCap cteb \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; src \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = src \<longrightarrow> src \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> src \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s))))
 3. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> (dest = src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) \<and> (dest \<noteq> src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))))
 4. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cref ctea cteb. \<lbrakk>capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cteb) \<noteq> capability.NullCap; cteCap cteb \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; src \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = src \<longrightarrow> src \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> src \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s))))
 2. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> (dest = src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) \<and> (dest \<noteq> src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))))
 3. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cref ctea cteb d da v0a v1a f fa cref' z. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; src \<noteq> dest; cteCap cteb = capability.UntypedCap d v0a v1a f; cap = capability.UntypedCap da v0a v1a fa; src \<in> cte_refs' (cteCap z) (irq_node' s); ctes_of s cref' = Some z\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> cref' \<noteq> dest \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s))))
 2. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> (dest = src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) \<and> (dest \<noteq> src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))))
 3. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cref ctea cteb d da v0a v1a f fa cref' z. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; src \<noteq> dest; cteCap cteb = capability.UntypedCap d v0a v1a f; cap = capability.UntypedCap da v0a v1a fa; src \<in> cte_refs' (cteCap z) (irq_node' s); ctes_of s cref' = Some z\<rbrakk> \<Longrightarrow> cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> cref' \<noteq> dest \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s))))
 2. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> (dest = src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) \<and> (dest \<noteq> src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))))
 3. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> (dest = src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) \<and> (dest \<noteq> src \<longrightarrow> (\<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))))
 2. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (3 subgoals):
 1. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za; dest = src\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za; dest \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))
 3. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za; dest \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = src \<longrightarrow> crefa \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))
 2. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea cteb crefa z cref' za. \<lbrakk>cteCap z \<noteq> capability.NullCap; ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap cteb); isUntypedCap cap; capPtr (cteCap cteb) = capPtr cap; capBlockSize (cteCap cteb) = capBlockSize cap; crefa \<noteq> dest; crefa \<noteq> src; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za; dest \<noteq> src\<rbrakk> \<Longrightarrow> (cref' = src \<longrightarrow> crefa \<in> cte_refs' (cteCap cteb) (irq_node' s)) \<and> (cref' \<noteq> src \<longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))
 2. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea cteb. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap) \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea cteb crefa. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap\<rbrakk> \<Longrightarrow> (crefa = dest \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref'. (cref' = dest \<longrightarrow> dest \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> dest \<in> cte_refs' cap' (irq_node' s))))) \<and> (crefa \<noteq> dest \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea cteb crefa. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> (crefa = dest \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref'. (cref' = dest \<longrightarrow> dest \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> dest \<in> cte_refs' cap' (irq_node' s))))) \<and> (crefa \<noteq> dest \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea cteb crefa. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s)); crefa = dest; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = dest \<longrightarrow> dest \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> dest \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte cref ctea cteb crefa. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s)); crefa \<noteq> dest; \<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea cteb. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = dest \<longrightarrow> dest \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> dest \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte cref ctea cteb crefa. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s)); crefa \<noteq> dest; \<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea cteb. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (cref = dest \<longrightarrow> dest \<in> cte_refs' cap (irq_node' s)) \<and> (cref \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap') \<and> dest \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte cref ctea cteb crefa. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s)); crefa \<noteq> dest; \<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea cteb crefa. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cteb) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s)); crefa \<noteq> dest; \<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea cteb crefa cref' z za. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> (\<exists>d v0 v1 f. cap = capability.UntypedCap d v0 v1 f) \<longrightarrow> (\<exists>d v0 v1 f. cteCap cteb = capability.UntypedCap d v0 v1 f) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; crefa \<noteq> dest; cteCap z \<noteq> capability.NullCap; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s crefa = Some z; ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea cteb crefa cref' z za. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; dest \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; capPtr (cteCap cteb) = capPtr cap \<longrightarrow> (\<exists>d v0 v1 f. cap = capability.UntypedCap d v0 v1 f) \<longrightarrow> (\<exists>d v0 v1 f. cteCap cteb = capability.UntypedCap d v0 v1 f) \<longrightarrow> capBlockSize (cteCap cteb) \<noteq> capBlockSize cap; crefa \<noteq> dest; cteCap z \<noteq> capability.NullCap; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s crefa = Some z; ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> (cref' = dest \<longrightarrow> crefa \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> dest \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal:
No subgoals!