theory Retype_DP

lemma invoke_untyped_one_wp:
  "uinv = (Retype uref nt ts [dest_slot] has_kids (Suc 0))
  \<Longrightarrow> \<lbrace>K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType
     \<and> free_range \<subseteq> tot_free_range
     \<and> (\<not> retype_with_kids (InvokeUntyped uinv) \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range)
     and (\<lambda>s. cdl_current_domain s = minBound)
     and < dest_slot \<mapsto>c NullCap
    \<and>* (\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped)
    \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range
    \<and>* P > \<rbrace>
  invoke_untyped uinv
  \<lbrace>\<lambda>_ s. (\<exists>oid free_range'.
  oid \<in> free_range
  \<and> free_range' \<subseteq> free_range - {oid} \<and>
  < dest_slot \<mapsto>c (default_cap nt {oid} ts dev)
  \<and>* oid \<mapsto>o obj
  \<and>* (\<And>* ptr\<in>tot_free_range - {oid}. ptr \<mapsto>o Untyped)
  \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range'
  \<and>* P > s) \<rbrace>, -" apply simp apply (rule hoare_pre) apply (rule hoare_post_imp_R) apply (rule invoke_untyped_wp
      [where free_range = free_range and obj_range = obj_range
      and tot_free_range = tot_free_range and obj = obj and P = P]) apply clarsimp apply (case_tac nlist) apply simp+ apply (rule_tac x = "a" in exI) apply simp apply (rule_tac x = free_range' in exI) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> (case InvokeUntyped uinv of InvokeUntyped (Retype uref nt ts dest has_kids n) \<Rightarrow> has_kids) \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)\<rbrace> invoke_untyped uinv \<lbrace>\<lambda>_ s. \<exists>oid free_range'. oid \<in> free_range \<and> free_range' \<subseteq> free_range - {oid} \<and> cdl.lift (dest_slot \<mapsto>c default_cap nt {oid} ts dev \<and>* oid \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {oid}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>(\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)\<rbrace> invoke_untyped (Retype uref nt ts [dest_slot] has_kids (Suc 0)) \<lbrace>\<lambda>_ s. \<exists>oid. oid \<in> free_range \<and> (\<exists>free_range'\<subseteq>free_range - {oid}. cdl.lift (dest_slot \<mapsto>c default_cap nt {oid} ts dev \<and>* oid \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {oid}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'5\<rbrace> invoke_untyped (Retype uref nt ts [dest_slot] has_kids (Suc 0)) \<lbrace>\<lambda>_ s. \<exists>oid. oid \<in> free_range \<and> (\<exists>free_range'\<subseteq>free_range - {oid}. cdl.lift (dest_slot \<mapsto>c default_cap nt {oid} ts dev \<and>* oid \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {oid}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>, -
 2. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (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'5 s proof (prove)
goal (3 subgoals):
 1. uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'5\<rbrace> invoke_untyped (Retype uref nt ts [dest_slot] has_kids (Suc 0)) \<lbrace>?Q'8\<rbrace>, -
 2. \<And>rv s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ?Q'8 rv s\<rbrakk> \<Longrightarrow> \<exists>oid. oid \<in> free_range \<and> (\<exists>free_range'\<subseteq>free_range - {oid}. cdl.lift (dest_slot \<mapsto>c default_cap nt {oid} ts dev \<and>* oid \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {oid}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)
 3. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (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'5 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); \<exists>nlist free_range'. length nlist = Suc 0 \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> free_range' \<subseteq> free_range - set nlist \<and> cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts ?dev11) [dest_slot] (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range' \<and>* P) s\<rbrakk> \<Longrightarrow> \<exists>oid. oid \<in> free_range \<and> (\<exists>free_range'\<subseteq>free_range - {oid}. cdl.lift (dest_slot \<mapsto>c default_cap nt {oid} ts dev \<and>* oid \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {oid}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)
 2. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s\<rbrakk> \<Longrightarrow> (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length [dest_slot] = Suc 0 \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) [dest_slot] \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range \<and>* P)) s proof (prove)
goal (2 subgoals):
 1. \<And>s nlist free_range'. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); length nlist = Suc 0; distinct nlist; set nlist \<subseteq> free_range; free_range' \<subseteq> free_range - set nlist; cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts ?dev11) [dest_slot] (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range' \<and>* P) s\<rbrakk> \<Longrightarrow> \<exists>oid. oid \<in> free_range \<and> (\<exists>free_range'\<subseteq>free_range - {oid}. cdl.lift (dest_slot \<mapsto>c default_cap nt {oid} ts dev \<and>* oid \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {oid}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)
 2. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s\<rbrakk> \<Longrightarrow> (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length [dest_slot] = Suc 0 \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) [dest_slot] \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range \<and>* P)) s proof (prove)
goal (3 subgoals):
 1. \<And>s nlist free_range'. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); length nlist = Suc 0; distinct nlist; set nlist \<subseteq> free_range; free_range' \<subseteq> free_range - set nlist; cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts ?dev11) [dest_slot] (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range' \<and>* P) s; nlist = []\<rbrakk> \<Longrightarrow> \<exists>oid. oid \<in> free_range \<and> (\<exists>free_range'\<subseteq>free_range - {oid}. cdl.lift (dest_slot \<mapsto>c default_cap nt {oid} ts dev \<and>* oid \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {oid}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)
 2. \<And>s nlist free_range' a list. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); length nlist = Suc 0; distinct nlist; set nlist \<subseteq> free_range; free_range' \<subseteq> free_range - set nlist; cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts ?dev11) [dest_slot] (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range' \<and>* P) s; nlist = a # list\<rbrakk> \<Longrightarrow> \<exists>oid. oid \<in> free_range \<and> (\<exists>free_range'\<subseteq>free_range - {oid}. cdl.lift (dest_slot \<mapsto>c default_cap nt {oid} ts dev \<and>* oid \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {oid}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)
 3. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s\<rbrakk> \<Longrightarrow> (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length [dest_slot] = Suc 0 \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) [dest_slot] \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range \<and>* P)) s proof (prove)
goal (2 subgoals):
 1. \<And>s nlist free_range' a list. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); list = []; a \<in> free_range; free_range' \<subseteq> free_range - {a}; cdl.lift (dest_slot \<mapsto>c default_cap nt {a} ts ?dev11 \<and>* a \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {a}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range' \<and>* P) s; nlist = [a]\<rbrakk> \<Longrightarrow> \<exists>oid. oid \<in> free_range \<and> (\<exists>free_range'\<subseteq>free_range - {oid}. cdl.lift (dest_slot \<mapsto>c default_cap nt {oid} ts dev \<and>* oid \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {oid}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)
 2. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s\<rbrakk> \<Longrightarrow> (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length [dest_slot] = Suc 0 \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) [dest_slot] \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range \<and>* P)) s proof (prove)
goal (2 subgoals):
 1. \<And>s nlist free_range' a list. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); list = []; a \<in> free_range; free_range' \<subseteq> free_range - {a}; cdl.lift (dest_slot \<mapsto>c default_cap nt {a} ts ?dev11 \<and>* a \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {a}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range' \<and>* P) s; nlist = [a]\<rbrakk> \<Longrightarrow> a \<in> free_range \<and> (\<exists>free_range'\<subseteq>free_range - {a}. cdl.lift (dest_slot \<mapsto>c default_cap nt {a} ts dev \<and>* a \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {a}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)
 2. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s\<rbrakk> \<Longrightarrow> (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length [dest_slot] = Suc 0 \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) [dest_slot] \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range \<and>* P)) s proof (prove)
goal (2 subgoals):
 1. \<And>s nlist free_range' a list. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); list = []; a \<in> free_range; free_range' \<subseteq> free_range - {a}; cdl.lift (dest_slot \<mapsto>c default_cap nt {a} ts ?dev11 \<and>* a \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {a}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range' \<and>* P) s; nlist = [a]\<rbrakk> \<Longrightarrow> \<exists>free_range'\<subseteq>free_range - {a}. cdl.lift (dest_slot \<mapsto>c default_cap nt {a} ts dev \<and>* a \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {a}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s
 2. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s\<rbrakk> \<Longrightarrow> (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length [dest_slot] = Suc 0 \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) [dest_slot] \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range \<and>* P)) s proof (prove)
goal (2 subgoals):
 1. \<And>s nlist free_range' a list. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); list = []; a \<in> free_range; free_range' \<subseteq> free_range - {a}; cdl.lift (dest_slot \<mapsto>c default_cap nt {a} ts ?dev11 \<and>* a \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {a}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range' \<and>* P) s; nlist = [a]\<rbrakk> \<Longrightarrow> free_range' \<subseteq> free_range - {a} \<and> cdl.lift (dest_slot \<mapsto>c default_cap nt {a} ts dev \<and>* a \<mapsto>o obj \<and>* (SETSEPCONJ ptr:tot_free_range - {a}. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s
 2. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s\<rbrakk> \<Longrightarrow> (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length [dest_slot] = Suc 0 \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) [dest_slot] \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap ?dev11 obj_range free_range \<and>* P)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s\<rbrakk> \<Longrightarrow> (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length [dest_slot] = Suc 0 \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) [dest_slot] \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s proof (prove)
goal:
No subgoals!