theory Untyped_R

lemma updateFreeIndex_mdb_simple':
  "\<lbrace>\<lambda>s. descendants_of' src (ctes_of s) = {} \<and>
        pspace_no_overlap' (capPtr cap) (capBlockSize cap) s \<and>
        valid_pspace' s \<and> cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>_. idx') cap) src s \<and>
        isUntypedCap cap\<rbrace>
   updateCap src (capFreeIndex_update (\<lambda>_. idx) cap)
   \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>" apply (clarsimp simp:valid_mdb'_def updateCap_def valid_pspace'_def) apply (wp getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of isCap_simps simp del:fun_upd_apply) apply (frule mdb_inv_preserve_updateCap[where index=idx and m="ctes_of s" and slot=src for s]) apply (simp add: isCap_simps) apply (simp add: modify_map_def) apply (clarsimp simp add: mdb_inv_preserve.preserve_stuff mdb_inv_preserve.by_products valid_mdb_ctes_def) proof - fix s cte ptr sz idx' d assume descendants: "descendants_of' src (ctes_of s) = {}"
  and    cte_wp_at' :"ctes_of s src = Some cte" "cteCap cte = capability.UntypedCap d ptr sz idx'"
  and      unt_inc' :"untyped_inc' (ctes_of s)"
  and   valid_objs' :"valid_objs' s"
  and invp: "mdb_inv_preserve (ctes_of s) ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. UntypedCap d ptr sz idx) cte))"
    (is "mdb_inv_preserve (ctes_of s) ?ctes") show "untyped_inc' ?ctes" using cte_wp_at' apply (clarsimp simp:untyped_inc'_def mdb_inv_preserve.descendants_of[OF invp, symmetric]
                       descendants
             split del: if_split) apply (case_tac "ctes_of s p") apply (simp split: if_split_asm) apply (case_tac "ctes_of s p'") apply (simp split: if_split_asm) apply (case_tac "the (ctes_of s p)", case_tac "the (ctes_of s p')") apply clarsimp apply (cut_tac p=p and p'=p' in untyped_incD'[OF _ _ _ _ unt_inc']) apply assumption apply (clarsimp simp: isCap_simps split: if_split_asm) apply assumption apply (clarsimp simp: isCap_simps split: if_split_asm) apply (clarsimp simp: descendants split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_of' src (ctes_of s) = {} \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s \<and> valid_pspace' s \<and> cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>_. idx') cap) src s \<and> isUntypedCap cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_of' src (ctes_of s) = {} \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>_. idx') cap) src s \<and> isUntypedCap cap\<rbrace> do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) cap) cte)
od \<lbrace>\<lambda>rv s. valid_mdb_ctes (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. descendants_of' src (ctes_of s) = {} \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>_. idx') cap) src s \<and> isUntypedCap cap \<Longrightarrow> cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> valid_mdb_ctes ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) cap) cte))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f idx'. \<lbrakk>descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cap = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 idx'; ctes_of s src = Some cte\<rbrakk> \<Longrightarrow> valid_mdb_ctes ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte d v0 v1 f idx'. \<lbrakk>descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cap = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 idx'; ctes_of s src = Some cte\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 2. \<And>s cte d v0 v1 f idx'. \<lbrakk>descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cap = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 idx'; ctes_of s src = Some cte; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte))))\<rbrakk> \<Longrightarrow> valid_mdb_ctes ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f idx'. \<lbrakk>descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cap = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 idx'; ctes_of s src = Some cte; mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte))))\<rbrakk> \<Longrightarrow> valid_mdb_ctes ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f idx'. \<lbrakk>descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); cap = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 idx'; ctes_of s src = Some cte; mdb_inv_preserve (ctes_of s) ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte))\<rbrakk> \<Longrightarrow> valid_mdb_ctes ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f idx'. \<lbrakk>descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; cap = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 idx'; ctes_of s src = Some cte; mdb_inv_preserve (ctes_of s) ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); valid_dlist ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); no_0 ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); mdb_chain_0 ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); valid_badges ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); caps_contained' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); mdb_chunked ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); untyped_mdb' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); untyped_inc' (ctes_of s); valid_nullcaps ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); ut_revocable' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); class_links ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); distinct_zombies ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); irq_control ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); reply_masters_rvk_fb ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte))\<rbrakk> \<Longrightarrow> untyped_inc' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)) proof (state)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f idx'. \<lbrakk>descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; cap = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 idx'; ctes_of s src = Some cte; mdb_inv_preserve (ctes_of s) ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); valid_dlist ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); no_0 ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); mdb_chain_0 ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); valid_badges ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); caps_contained' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); mdb_chunked ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); untyped_mdb' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); untyped_inc' (ctes_of s); valid_nullcaps ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); ut_revocable' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); class_links ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); distinct_zombies ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); irq_control ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); reply_masters_rvk_fb ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte))\<rbrakk> \<Longrightarrow> untyped_inc' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)) proof (state)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f idx'. \<lbrakk>descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; cap = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 idx'; ctes_of s src = Some cte; mdb_inv_preserve (ctes_of s) ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); valid_dlist ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); no_0 ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); mdb_chain_0 ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); valid_badges ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); caps_contained' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); mdb_chunked ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); untyped_mdb' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); untyped_inc' (ctes_of s); valid_nullcaps ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); ut_revocable' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); class_links ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); distinct_zombies ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); irq_control ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); reply_masters_rvk_fb ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte))\<rbrakk> \<Longrightarrow> untyped_inc' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)) proof (state)
this:
descendants_of' src (ctes_of s) = {}
ctes_of s src = Some cte
cteCap cte = capability.UntypedCap d ptr sz idx'
untyped_inc' (ctes_of s)
valid_objs' s
mdb_inv_preserve (ctes_of s) ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte))

goal (1 subgoal):
 1. \<And>s cte d v0 v1 f idx'. \<lbrakk>descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; cap = capability.UntypedCap d v0 v1 f; cteCap cte = capability.UntypedCap d v0 v1 idx'; ctes_of s src = Some cte; mdb_inv_preserve (ctes_of s) ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); valid_dlist ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); no_0 ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); mdb_chain_0 ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); valid_badges ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); caps_contained' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); mdb_chunked ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); untyped_mdb' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); untyped_inc' (ctes_of s); valid_nullcaps ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); ut_revocable' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); class_links ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); distinct_zombies ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); irq_control ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)); reply_masters_rvk_fb ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte))\<rbrakk> \<Longrightarrow> untyped_inc' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)) proof (prove)
goal (1 subgoal):
 1. untyped_inc' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte)) proof (prove)
using this:
ctes_of s src = Some cte
cteCap cte = capability.UntypedCap d ptr sz idx'

goal (1 subgoal):
 1. untyped_inc' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte)) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = None\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p')
 2. \<And>p p' c n c' n' a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some a\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some a\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some a; ctes_of s p' = None\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p')
 2. \<And>p p' c n c' n' a aa. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some a; ctes_of s p' = Some aa\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' a aa. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some a; ctes_of s p' = Some aa\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' a aa x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some a; ctes_of s p' = Some aa; the (ctes_of s p) = CTE x1 x2; the (ctes_of s p') = CTE x1a x2a\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (5 subgoals):
 1. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> ctes_of s p = Some (CTE (?c77 p p' c n c' n' x1 x2 x1a x2a) (?n77 p p' c n c' n' x1 x2 x1a x2a))
 2. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> isUntypedCap (?c77 p p' c n c' n' x1 x2 x1a x2a)
 3. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> ctes_of s p' = Some (CTE (?c'77 p p' c n c' n' x1 x2 x1a x2a) (?n'77 p p' c n c' n' x1 x2 x1a x2a))
 4. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> isUntypedCap (?c'77 p p' c n c' n' x1 x2 x1a x2a)
 5. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a); (untypedRange (?c77 p p' c n c' n' x1 x2 x1a x2a) \<subseteq> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<or> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<subseteq> untypedRange (?c77 p p' c n c' n' x1 x2 x1a x2a) \<or> untypedRange (?c77 p p' c n c' n' x1 x2 x1a x2a) \<inter> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) = {}) \<and> (untypedRange (?c77 p p' c n c' n' x1 x2 x1a x2a) \<subset> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange (?c77 p p' c n c' n' x1 x2 x1a x2a) \<inter> usableUntypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) = {}) \<and> (untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<subset> untypedRange (?c77 p p' c n c' n' x1 x2 x1a x2a) \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<inter> usableUntypedRange (?c77 p p' c n c' n' x1 x2 x1a x2a) = {}) \<and> (untypedRange (?c77 p p' c n c' n' x1 x2 x1a x2a) = untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange (?c77 p p' c n c' n' x1 x2 x1a x2a) = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (4 subgoals):
 1. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> isUntypedCap x1
 2. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> ctes_of s p' = Some (CTE (?c'77 p p' c n c' n' x1 x2 x1a x2a) (?n'77 p p' c n c' n' x1 x2 x1a x2a))
 3. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> isUntypedCap (?c'77 p p' c n c' n' x1 x2 x1a x2a)
 4. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a); (untypedRange x1 \<subseteq> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<or> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<subseteq> untypedRange x1 \<or> untypedRange x1 \<inter> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) = {}) \<and> (untypedRange x1 \<subset> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) = {}) \<and> (untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<subset> untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 = untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (3 subgoals):
 1. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> ctes_of s p' = Some (CTE (?c'77 p p' c n c' n' x1 x2 x1a x2a) (?n'77 p p' c n c' n' x1 x2 x1a x2a))
 2. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> isUntypedCap (?c'77 p p' c n c' n' x1 x2 x1a x2a)
 3. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a); (untypedRange x1 \<subseteq> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<or> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<subseteq> untypedRange x1 \<or> untypedRange x1 \<inter> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) = {}) \<and> (untypedRange x1 \<subset> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) = {}) \<and> (untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<subset> untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 = untypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange (?c'77 p p' c n c' n' x1 x2 x1a x2a) = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> isUntypedCap x1a
 2. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a); (untypedRange x1 \<subseteq> untypedRange x1a \<or> untypedRange x1a \<subseteq> untypedRange x1 \<or> untypedRange x1 \<inter> untypedRange x1a = {}) \<and> (untypedRange x1 \<subset> untypedRange x1a \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange x1a = {}) \<and> (untypedRange x1a \<subset> untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange x1a \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 = untypedRange x1a \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x1 x2 x1a x2a. \<lbrakk>ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx'; (if p = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p) = Some (CTE c n); isUntypedCap c; (if p' = src then Some (cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte) else ctes_of s p') = Some (CTE c' n'); isUntypedCap c'; ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a); (untypedRange x1 \<subseteq> untypedRange x1a \<or> untypedRange x1a \<subseteq> untypedRange x1 \<or> untypedRange x1 \<inter> untypedRange x1a = {}) \<and> (untypedRange x1 \<subset> untypedRange x1a \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange x1 \<inter> usableUntypedRange x1a = {}) \<and> (untypedRange x1a \<subset> untypedRange x1 \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange x1a \<inter> usableUntypedRange x1 = {}) \<and> (untypedRange x1 = untypedRange x1a \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange x1 = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange x1a = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' (ctes_of s) \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p (ctes_of s) \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' (ctes_of s) \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal:
No subgoals! proof (state)
this:
untyped_inc' ((ctes_of s)(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d ptr sz idx) cte))

goal:
No subgoals!