theory Retype_DP

lemma reset_untyped_cap_wp:
  "obj_range \<subseteq> tot_free_range
  \<Longrightarrow> \<lbrace>< (\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped)
    \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range
    \<and>* P >\<rbrace> reset_untyped_cap uref
  \<lbrace>\<lambda>y s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and>
    cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (\<And>*ptr\<in>tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrace>,-" apply (simp add:reset_untyped_cap_def bind_assoc bindE_assoc) apply (rule hoare_pre) apply (wp whenE_wp) apply (rule_tac P = "\<exists>fr. cap = UntypedCap dev obj_range fr
          \<and> (\<forall>fr\<in> set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range)" in hoare_gen_asmE) apply clarsimp apply (wp whenE_wp mapME_x_wp) apply (rule ballI) apply (rule hoare_pre) apply wp apply simp apply (rule hoare_post_imp[OF _ set_cap_wp]) apply clarsimp apply (rule_tac x = xa in exI) apply ((rule conjI, fastforce)+, sep_solve) apply clarsimp apply sep_solve apply (wp | clarsimp)+ apply (subst dummy_detype_if_untyped) apply simp apply (sep_select_asm 2) apply (frule opt_cap_sep_imp) apply (clarsimp dest!: reset_cap_asid_untyped_cap_eqD) apply (subgoal_tac "tot_free_range = obj_range \<union> (tot_free_range - obj_range)") apply simp apply (subst (asm) sep.prod.subset_diff) apply simp+ apply (sep_select_asm 2) apply (simp add:sep_conj_assoc) apply sep_solve apply blast apply (sep_select_asm 2, frule opt_cap_sep_imp) apply (clarsimp dest!: reset_cap_asid_simps2) apply (intro conjI impI exI allI) apply fastforce apply (elim conjE) apply (drule hd_in_set) apply (drule(1) bspec) apply force apply sep_solve apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)\<rbrace> reset_untyped_cap uref \<lbrace>\<lambda>y s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)\<rbrace> doE cap <- liftE (get_cap uref);
whenE (available_range cap \<noteq> cap_objects cap) (doE y <- liftE (modify (detype (cap_objects cap)));
liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) >>=E mapME_x (\<lambda>r. doE y <- liftE (set_cap uref (set_available_range cap r));
returnOk () \<sqinter> throw
odE)
odE)
odE \<lbrace>\<lambda>y s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> doE cap <- liftE (get_cap uref);
whenE (available_range cap \<noteq> cap_objects cap) (doE y <- liftE (modify (detype (cap_objects cap)));
liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) >>=E mapME_x (\<lambda>r. doE y <- liftE (set_cap uref (set_available_range cap r));
returnOk () \<sqinter> throw
odE)
odE)
odE \<lbrace>\<lambda>y s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrace>, -
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cap y x. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B10 cap y x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap uref (set_available_range cap r));
returnOk () \<sqinter> throw
odE) x \<lbrace>\<lambda>y s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrace>, -
 2. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>?B10 cap y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cap y x. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap; \<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range)\<rbrakk> \<Longrightarrow> \<lbrace>?P'12 cap y x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap uref (set_available_range cap r));
returnOk () \<sqinter> throw
odE) x \<lbrace>\<lambda>y s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrace>, -
 2. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. ?P'12 cap y x and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>x fr. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range\<rbrakk> \<Longrightarrow> \<lbrace>?P'12 (UntypedCap dev obj_range fr) () x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap uref (UntypedCap dev obj_range r));
returnOk () \<sqinter> throw
odE) x \<lbrace>\<lambda>y s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrace>, -
 2. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. ?P'12 cap y x and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>x fr. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. \<lbrace>\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a\<rbrace> doE y <- liftE (set_cap uref (UntypedCap dev obj_range x));
returnOk () \<sqinter> throw
odE \<lbrace>\<lambda>y a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>x fr xa. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a\<rbrace> doE y <- liftE (set_cap uref (UntypedCap dev obj_range xa));
returnOk () \<sqinter> throw
odE \<lbrace>\<lambda>y a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>x fr xa. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 x fr xa\<rbrace> doE y <- liftE (set_cap uref (UntypedCap dev obj_range xa));
returnOk () \<sqinter> throw
odE \<lbrace>\<lambda>y a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x fr xa s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> ?Q28 x fr xa s
 3. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>x fr xa. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x\<rbrakk> \<Longrightarrow> \<lbrace>?P'51 x fr xa\<rbrace> set_cap uref (UntypedCap dev obj_range xa) \<lbrace>\<lambda>rv s. (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> True \<and> True\<rbrace>
 2. \<And>x fr xa s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> True \<and> True \<and> True \<and> ?P'51 x fr xa s
 3. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>x fr xa. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x\<rbrakk> \<Longrightarrow> \<lbrace>?P'51 x fr xa\<rbrace> set_cap uref (UntypedCap dev obj_range xa) \<lbrace>\<lambda>rv s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrace>
 2. \<And>x fr xa s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> True \<and> True \<and> True \<and> ?P'51 x fr xa s
 3. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>x fr xa rv s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range xa \<and>* ?R57 x fr xa) s\<rbrakk> \<Longrightarrow> \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 2. \<And>x fr xa s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> True \<and> True \<and> True \<and> cdl.lift (uref \<mapsto>c - \<and>* ?R57 x fr xa) s
 3. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>x fr xa s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range xa \<and>* ?R57 x fr xa) s\<rbrakk> \<Longrightarrow> \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 2. \<And>x fr xa s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> True \<and> True \<and> True \<and> cdl.lift (uref \<mapsto>c - \<and>* ?R57 x fr xa) s
 3. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>x fr xa s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range xa \<and>* ?R57 x fr xa) s\<rbrakk> \<Longrightarrow> free_range \<subseteq> xa \<and> xa \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range xa \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 2. \<And>x fr xa s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> True \<and> True \<and> True \<and> cdl.lift (uref \<mapsto>c - \<and>* ?R57 x fr xa) s
 3. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>x fr xa s. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> True \<and> True \<and> True \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 2. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>x fr xa s fra. \<lbrakk>obj_range \<subseteq> tot_free_range; fr \<noteq> obj_range; \<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range; xa \<in> set x; free_range \<subseteq> fra; fra \<subseteq> obj_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fra \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 2. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>cap y. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B9 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. (\<lambda>a. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) a) and K (\<exists>fr. cap = UntypedCap dev obj_range fr \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>cap. \<lbrakk>obj_range \<subseteq> tot_free_range; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'7 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B9 cap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. obj_range \<subseteq> tot_free_range \<Longrightarrow> \<lbrace>?P'\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then \<lambda>s. True \<and> ?P'7 cap s else (\<lambda>s. \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) (detype (cap_objects (the (opt_cap uref s))) s)) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (3 subgoals):
 1. \<And>s fr x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> finite (cap_objects (the (opt_cap uref s)))
 2. \<And>s fr x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:cap_objects (the (opt_cap uref s)). ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 3. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s fr x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:cap_objects (the (opt_cap uref s)). ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s fr x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:cap_objects (the (opt_cap uref s)). ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s fr x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; \<exists>cap'. opt_cap uref s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:cap_objects (the (opt_cap uref s)). ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); tot_free_range = obj_range \<union> (tot_free_range - obj_range)\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> tot_free_range = obj_range \<union> (tot_free_range - obj_range)
 3. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); tot_free_range = obj_range \<union> tot_free_range\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> tot_free_range = obj_range \<union> (tot_free_range - obj_range)
 3. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>opt_cap uref s = Some (UntypedCap dev obj_range free_range); tot_free_range = obj_range \<union> tot_free_range; obj_range \<subseteq> tot_free_range\<rbrakk> \<Longrightarrow> ?B182 s \<subseteq> tot_free_range
 2. \<And>s. \<lbrakk>opt_cap uref s = Some (UntypedCap dev obj_range free_range); tot_free_range = obj_range \<union> tot_free_range; obj_range \<subseteq> tot_free_range\<rbrakk> \<Longrightarrow> finite tot_free_range
 3. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* ((SETSEPCONJ ptr:tot_free_range - ?B182 s. ptr \<mapsto>o Untyped) \<and>* (SETSEPCONJ ptr:?B182 s. ptr \<mapsto>o Untyped)) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); tot_free_range = obj_range \<union> tot_free_range\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 4. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> tot_free_range = obj_range \<union> (tot_free_range - obj_range)
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* ((SETSEPCONJ ptr:tot_free_range - obj_range. ptr \<mapsto>o Untyped) \<and>* (SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped)) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); tot_free_range = obj_range \<union> tot_free_range\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> tot_free_range = obj_range \<union> (tot_free_range - obj_range)
 3. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; opt_cap uref s = Some (UntypedCap dev obj_range free_range); tot_free_range = obj_range \<union> tot_free_range; cdl.lift (((SETSEPCONJ ptr:tot_free_range - obj_range. ptr \<mapsto>o Untyped) \<and>* (SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped)) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> tot_free_range = obj_range \<union> (tot_free_range - obj_range)
 3. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; opt_cap uref s = Some (UntypedCap dev obj_range free_range); tot_free_range = obj_range \<union> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range - obj_range. ptr \<mapsto>o Untyped) \<and>* (SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* ?P168 s) s
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> tot_free_range = obj_range \<union> (tot_free_range - obj_range)
 3. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> tot_free_range = obj_range \<union> (tot_free_range - obj_range)
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; \<exists>cap'. opt_cap uref s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> (available_range (the (opt_cap uref s)) \<noteq> cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap uref s)) \<and> available_range (the (opt_cap uref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<exists>fr. the (opt_cap uref s) = UntypedCap dev obj_range fr) \<and> (\<forall>fr\<in>set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range))) \<and> (available_range (the (opt_cap uref s)) = cap_objects (the (opt_cap uref s)) \<longrightarrow> (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> (free_range \<noteq> obj_range \<longrightarrow> (\<forall>x. (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range \<longrightarrow> (\<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s) \<and> (\<forall>x\<in>set x. free_range \<subseteq> x))) \<and> (free_range = obj_range \<longrightarrow> (\<exists>fr. obj_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s)) proof (prove)
goal (7 subgoals):
 1. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> free_range \<subseteq> ?fr230 s x
 2. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> ?fr230 s x \<subseteq> obj_range
 3. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range (?fr230 s x) \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 4. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. free_range \<subseteq> x
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> obj_range \<subseteq> ?fr223 s
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> ?fr223 s \<subseteq> obj_range
 7. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range (?fr223 s) \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> free_range \<subseteq> obj_range
 2. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 3. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. free_range \<subseteq> x
 4. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> obj_range \<subseteq> ?fr223 s
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> ?fr223 s \<subseteq> obj_range
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range (?fr223 s) \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; \<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S; x \<noteq> []; last x = obj_range\<rbrakk> \<Longrightarrow> free_range \<subseteq> obj_range
 2. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 3. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. free_range \<subseteq> x
 4. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> obj_range \<subseteq> ?fr223 s
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> ?fr223 s \<subseteq> obj_range
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range (?fr223 s) \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; \<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S; last x = obj_range; hd x \<in> set x\<rbrakk> \<Longrightarrow> free_range \<subseteq> obj_range
 2. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 3. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. free_range \<subseteq> x
 4. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> obj_range \<subseteq> ?fr223 s
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> ?fr223 s \<subseteq> obj_range
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range (?fr223 s) \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; last x = obj_range; hd x \<in> set x; hd x \<subseteq> obj_range \<and> free_range \<subset> hd x\<rbrakk> \<Longrightarrow> free_range \<subseteq> obj_range
 2. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 3. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. free_range \<subseteq> x
 4. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> obj_range \<subseteq> ?fr223 s
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> ?fr223 s \<subseteq> obj_range
 6. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range (?fr223 s) \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s proof (prove)
goal (5 subgoals):
 1. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s
 2. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. free_range \<subseteq> x
 3. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> obj_range \<subseteq> ?fr223 s
 4. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> ?fr223 s \<subseteq> obj_range
 5. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range (?fr223 s) \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range \<noteq> obj_range; (\<forall>S\<in>set x. S \<subseteq> obj_range \<and> free_range \<subset> S) \<and> x \<noteq> [] \<and> last x = obj_range\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. free_range \<subseteq> x
 2. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> obj_range \<subseteq> ?fr223 s
 3. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> ?fr223 s \<subseteq> obj_range
 4. \<And>s. \<lbrakk>obj_range \<subseteq> tot_free_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s; opt_cap uref s = Some (UntypedCap dev obj_range free_range); free_range = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c UntypedCap dev obj_range (?fr223 s) \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) s proof (prove)
goal:
No subgoals!