theory Detype_C

lemma cpspace_tcb_relation_address_subset:
  assumes     vuc: "s \<turnstile>' capability.UntypedCap d ptr bits idx"
  and        invs: "invs' s"
  and     ctcbrel: "cpspace_tcb_relation (ksPSpace s) (t_hrs_' (globals s'))"
  shows "cmap_relation (map_to_tcbs (ksPSpace s |` (- {ptr..+2 ^ bits - unat ctcb_offset})))
      (cslift s' |` (- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})) tcb_ptr_to_ctcb_ptr
      ctcb_relation
   = cmap_relation (map_to_tcbs (ksPSpace s |` (- {ptr..+2 ^ bits})))
        (cslift s' |` (- Ptr ` {ptr..+2 ^ bits})) tcb_ptr_to_ctcb_ptr
        ctcb_relation" (is "cmap_relation ?am ?cm tcb_ptr_to_ctcb_ptr ctcb_relation
  = cmap_relation ?am' ?cm' tcb_ptr_to_ctcb_ptr ctcb_relation") proof (rule cmap_relation_cong) from vuc have al: "is_aligned ptr bits" and wb: "bits < word_bits" by (auto elim: valid_untyped_capE) have r1: "\<And>x tcb. \<lbrakk> (map_to_tcbs (ksPSpace s) x) = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk>
    \<Longrightarrow> x \<in> {ptr..+2 ^ bits - unat ctcb_offset}" proof (subst intvl_aligned_top [where 'a=32, folded word_bits_def, OF _ al _ _ wb]) fix x tcb assume mtcb: "map_to_tcbs (ksPSpace s) x = Some tcb" and xin: "x \<in> {ptr..+2 ^ bits}" from mtcb invs have koat: "ko_at' tcb x s" by (fastforce simp: map_comp_Some_iff projectKOs intro: aligned_distinct_obj_atI') thus "is_aligned x (objBits tcb)" by (clarsimp elim!: obj_atE' simp: projectKOs objBits_def) 

    (* FIXME: generalise *)
     with xin koat show "objBits tcb \<le> bits" using wb apply - apply (frule is_aligned_no_overflow) apply (drule valid_untyped_cap_ko_at_disjoint [OF vuc]) apply (erule contrapos_pn) apply (subst upto_intvl_eq [OF al]) apply (erule orthD1) apply simp apply (drule (1) range_subsetD) apply clarsimp apply (drule (1) word_sub_mono2 [where b = "(2 :: word32) ^ objBits tcb - 1"
        and d = "2 ^ bits - 1", simplified field_simps]) apply (subst field_simps [symmetric], subst olen_add_eqv [symmetric]) apply (simp add: field_simps) apply (subst field_simps [symmetric], subst olen_add_eqv [symmetric]) apply (rule is_aligned_no_overflow' [OF al]) apply (subgoal_tac "(2 :: word32) ^ objBits tcb \<noteq> 0") apply (simp add: word_le_nat_alt unat_minus_one le_diff_iff word_bits_def) apply (simp add: objBits_simps) done show "unat ctcb_offset < 2 ^ objBits tcb" by (fastforce simp add: ctcb_offset_defs objBits_simps' project_inject) show "x \<in> {ptr..+2 ^ bits}" by fact qed show "dom ?am = dom ?am'" apply (rule dom_eqI) apply (clarsimp dest!: r1 simp: map_comp_restrict_map_Some_iff) apply (clarsimp dest!: intvl_mem_weaken simp: map_comp_restrict_map_Some_iff) done let ?ran = "{ptr..+2 ^ bits}" let ?small_ran = "{ptr..+2 ^ bits - unat ctcb_offset}" show "dom ?cm = dom ?cm'" proof (rule dom_eqI) fix x y assume "?cm' x = Some y" hence cl: "cslift s' x = Some y" and xni: "x \<notin> Ptr ` ?ran" by (auto simp: restrict_map_Some_iff) with ctcbrel obtain x' tcb where mt: "map_to_tcbs (ksPSpace s) x' = Some tcb"
      and xv: "x = tcb_ptr_to_ctcb_ptr x'" by (fastforce elim!: cmap_relation_h_t_valid simp add: h_t_valid_clift_Some_iff) have "(cslift s' |` (- tcb_ptr_to_ctcb_ptr ` ?small_ran)) x = Some y" proof (subst restrict_in) show "x \<in> - tcb_ptr_to_ctcb_ptr ` ?small_ran" using xni proof (rule contrapos_np) assume "x \<notin> - tcb_ptr_to_ctcb_ptr ` ?small_ran" hence "x \<in> tcb_ptr_to_ctcb_ptr ` ?small_ran" by simp hence "x \<in> Ptr ` {ptr + ctcb_offset ..+ 2 ^ bits - unat ctcb_offset}" by (simp add: tcb_ptr_to_ctcb_ptr_to_Ptr) thus "x \<in> Ptr ` ?ran" by (clarsimp intro!: imageI elim!: intvl_plus_sub_offset) qed qed fact thus "\<exists>y. (cslift s' |` (- tcb_ptr_to_ctcb_ptr ` ?small_ran)) x = Some y" .. next fix x y assume "?cm x = Some y" hence cl: "cslift s' x = Some y" and xni: "x \<notin> tcb_ptr_to_ctcb_ptr ` ?small_ran" by (auto simp: restrict_map_Some_iff) with ctcbrel obtain x' tcb where mt: "map_to_tcbs (ksPSpace s) x' = Some tcb" and xv: "x = tcb_ptr_to_ctcb_ptr x'" by (fastforce elim!: cmap_relation_h_t_valid simp add: h_t_valid_clift_Some_iff) from mt invs have koat: "ko_at' tcb x' s" by (rule map_to_ko_atI') have "(cslift s' |` (- Ptr ` ?ran)) x = Some y" proof (subst restrict_in) show "x \<in> - Ptr ` ?ran" using xni apply (rule contrapos_np) apply (simp add: xv) apply (rule imageI) apply (rule r1 [OF mt]) apply (rule valid_untyped_cap_ctcb_member' [OF vuc koat]) apply (erule imageE) apply simp done qed fact thus "\<exists>y. (cslift s' |` (- Ptr ` ?ran)) x = Some y" .. qed qed (clarsimp simp: map_comp_Some_iff restrict_map_Some_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>)) (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) tcb_ptr_to_ctcb_ptr ctcb_relation = cmap_relation (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>)) (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) tcb_ptr_to_ctcb_ptr ctcb_relation proof (state)
goal (3 subgoals):
 1. dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>)) = dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>))
 2. dom (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) = dom (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>)
 3. \<And>p a a' b b'. \<lbrakk>map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) p = Some a; map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p = Some a'; (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b; (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (chain)
picking this:
valid_cap' (capability.UntypedCap d ptr bits idx) s proof (prove)
using this:
valid_cap' (capability.UntypedCap d ptr bits idx) s

goal (1 subgoal):
 1. is_aligned ptr bits &&& bits < word_bits proof (state)
this:
is_aligned ptr bits
bits < word_bits

goal (3 subgoals):
 1. dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>)) = dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>))
 2. dom (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) = dom (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>)
 3. \<And>p a a' b b'. \<lbrakk>map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) p = Some a; map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p = Some a'; (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b; (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (prove)
goal (1 subgoal):
 1. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits - unat ctcb_offset} proof (state)
goal (4 subgoals):
 1. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> is_aligned x (?n x tcb)
 2. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> ?n x tcb \<le> bits
 3. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> unat ctcb_offset < 2 ^ ?n x tcb
 4. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (state)
goal (4 subgoals):
 1. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> is_aligned x (?n x tcb)
 2. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> ?n x tcb \<le> bits
 3. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> unat ctcb_offset < 2 ^ ?n x tcb
 4. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (state)
this:
map_to_tcbs (ksPSpace s) x = Some tcb
x \<in> {ptr..+2 ^ bits}

goal (4 subgoals):
 1. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> is_aligned x (?n x tcb)
 2. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> ?n x tcb \<le> bits
 3. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> unat ctcb_offset < 2 ^ ?n x tcb
 4. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (chain)
picking this:
map_to_tcbs (ksPSpace s) x = Some tcb
invs' s proof (prove)
using this:
map_to_tcbs (ksPSpace s) x = Some tcb
invs' s

goal (1 subgoal):
 1. ko_at' tcb x s proof (state)
this:
ko_at' tcb x s

goal (4 subgoals):
 1. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> is_aligned x (?n x tcb)
 2. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> ?n x tcb \<le> bits
 3. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> unat ctcb_offset < 2 ^ ?n x tcb
 4. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (prove)
using this:
ko_at' tcb x s

goal (1 subgoal):
 1. is_aligned x (objBits tcb) proof (state)
this:
is_aligned x (objBits tcb)

goal (3 subgoals):
 1. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits
 2. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> unat ctcb_offset < 2 ^ objBits tcb
 3. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (state)
this:
is_aligned x (objBits tcb)

goal (3 subgoals):
 1. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits
 2. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> unat ctcb_offset < 2 ^ objBits tcb
 3. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (chain)
picking this:
x \<in> {ptr..+2 ^ bits}
ko_at' tcb x s
is_aligned x (objBits tcb) proof (prove)
using this:
x \<in> {ptr..+2 ^ bits}
ko_at' tcb x s
is_aligned x (objBits tcb)

goal (1 subgoal):
 1. objBits tcb \<le> bits proof (prove)
using this:
x \<in> {ptr..+2 ^ bits}
ko_at' tcb x s
is_aligned x (objBits tcb)
bits < word_bits

goal (1 subgoal):
 1. objBits tcb \<le> bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; ko_at' tcb x s; is_aligned x (objBits tcb); bits < word_bits\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; ko_at' tcb x s; is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}
 2. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1; {x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1; {x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> x \<notin> {ptr..+2 ^ bits}
 2. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1; {x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1; {x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> x \<notin> {ptr..ptr + 2 ^ bits - 1}
 2. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1; {x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1\<rbrakk> \<Longrightarrow> x \<in> {x..x + 2 ^ objBits tcb - 1}
 2. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1; {x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1; {x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; x \<le> x + 2 ^ objBits tcb - 1; ptr \<le> x \<and> x + 2 ^ objBits tcb - 1 \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x; x + 2 ^ objBits tcb - 1 \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x\<rbrakk> \<Longrightarrow> 2 ^ objBits tcb - 1 \<le> x + 2 ^ objBits tcb - 1
 2. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x\<rbrakk> \<Longrightarrow> 2 ^ bits - 1 \<le> ptr + 2 ^ bits - 1
 3. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x; 2 ^ objBits tcb - 1 \<le> 2 ^ bits - 1\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ objBits tcb - 1)
 2. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x\<rbrakk> \<Longrightarrow> 2 ^ bits - 1 \<le> ptr + 2 ^ bits - 1
 3. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x; 2 ^ objBits tcb - 1 \<le> 2 ^ bits - 1\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x\<rbrakk> \<Longrightarrow> 2 ^ bits - 1 \<le> ptr + 2 ^ bits - 1
 2. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x; 2 ^ objBits tcb - 1 \<le> 2 ^ bits - 1\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ bits - 1)
 2. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x; 2 ^ objBits tcb - 1 \<le> 2 ^ bits - 1\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x; 2 ^ objBits tcb - 1 \<le> 2 ^ bits - 1\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x; 2 ^ objBits tcb - 1 \<le> 2 ^ bits - 1; 2 ^ objBits tcb \<noteq> 0\<rbrakk> \<Longrightarrow> objBits tcb \<le> bits
 2. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x; 2 ^ objBits tcb - 1 \<le> 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 2 ^ objBits tcb \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> {ptr..+2 ^ bits}; is_aligned x (objBits tcb); bits < word_bits; ptr \<le> x; 2 ^ objBits tcb - 1 \<le> 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 2 ^ objBits tcb \<noteq> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
objBits tcb \<le> bits

goal (2 subgoals):
 1. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> unat ctcb_offset < 2 ^ objBits tcb
 2. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. unat ctcb_offset < 2 ^ objBits tcb proof (state)
this:
unat ctcb_offset < 2 ^ objBits tcb

goal (1 subgoal):
 1. \<And>x tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. x \<in> {ptr..+2 ^ bits} proof (state)
this:
x \<in> {ptr..+2 ^ bits}

goal:
No subgoals! proof (state)
this:
\<lbrakk>map_to_tcbs (ksPSpace s) ?x1 = Some ?tcb1; ?x1 \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> ?x1 \<in> {ptr..+2 ^ bits - unat ctcb_offset}

goal (3 subgoals):
 1. dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>)) = dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>))
 2. dom (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) = dom (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>)
 3. \<And>p a a' b b'. \<lbrakk>map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) p = Some a; map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p = Some a'; (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b; (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (prove)
goal (1 subgoal):
 1. dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>)) = dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>)) proof (prove)
goal (2 subgoals):
 1. \<And>x y. map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) x = Some y
 2. \<And>x y. map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x y. map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (prove)
goal:
No subgoals! proof (state)
this:
dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>)) = dom (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>))

goal (2 subgoals):
 1. dom (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) = dom (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>)
 2. \<And>p a a' b b'. \<lbrakk>map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) p = Some a; map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p = Some a'; (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b; (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (state)
goal (2 subgoals):
 1. dom (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) = dom (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>)
 2. \<And>p a a' b b'. \<lbrakk>map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) p = Some a; map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p = Some a'; (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b; (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (state)
goal (2 subgoals):
 1. dom (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) = dom (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>)
 2. \<And>p a a' b b'. \<lbrakk>map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) p = Some a; map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p = Some a'; (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b; (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (prove)
goal (1 subgoal):
 1. dom (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) = dom (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) proof (state)
goal (2 subgoals):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y
 2. \<And>x y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (state)
goal (2 subgoals):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y
 2. \<And>x y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (state)
this:
(cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y

goal (2 subgoals):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y
 2. \<And>x y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (prove)
using this:
(cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y

goal (1 subgoal):
 1. cslift s' x = Some y &&& x \<notin> tcb_Ptr ` {ptr..+2 ^ bits} proof (state)
this:
cslift s' x = Some y
x \<notin> tcb_Ptr ` {ptr..+2 ^ bits}

goal (2 subgoals):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y
 2. \<And>x y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (chain)
picking this:
cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation
cslift s' x = Some y
x \<notin> tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
using this:
cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation
cslift s' x = Some y
x \<notin> tcb_Ptr ` {ptr..+2 ^ bits}

goal (1 subgoal):
 1. (\<And>x' tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x' = Some tcb; x = tcb_ptr_to_ctcb_ptr x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
map_to_tcbs (ksPSpace s) x' = Some tcb
x = tcb_ptr_to_ctcb_ptr x'

goal (2 subgoals):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y
 2. \<And>x y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (prove)
goal (1 subgoal):
 1. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (state)
goal (2 subgoals):
 1. x \<in> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset}
 2. cslift s' x = Some y proof (prove)
goal (1 subgoal):
 1. x \<in> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} proof (prove)
using this:
x \<notin> tcb_Ptr ` {ptr..+2 ^ bits}

goal (1 subgoal):
 1. x \<in> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} proof (state)
goal (1 subgoal):
 1. x \<notin> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} \<Longrightarrow> x \<in> tcb_Ptr ` {ptr..+2 ^ bits} proof (state)
this:
x \<notin> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. x \<notin> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} \<Longrightarrow> x \<in> tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
using this:
x \<notin> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. x \<in> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} proof (state)
this:
x \<in> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. x \<notin> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} \<Longrightarrow> x \<in> tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
using this:
x \<in> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. x \<in> tcb_Ptr ` {ptr + ctcb_offset..+2 ^ bits - unat ctcb_offset} proof (state)
this:
x \<in> tcb_Ptr ` {ptr + ctcb_offset..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. x \<notin> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} \<Longrightarrow> x \<in> tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
using this:
x \<in> tcb_Ptr ` {ptr + ctcb_offset..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. x \<in> tcb_Ptr ` {ptr..+2 ^ bits} proof (state)
this:
x \<in> tcb_Ptr ` {ptr..+2 ^ bits}

goal:
No subgoals! proof (state)
this:
x \<in> - tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. cslift s' x = Some y proof (state)
this:
(cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y

goal (2 subgoals):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y
 2. \<And>x y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (prove)
using this:
(cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y

goal (1 subgoal):
 1. \<exists>y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y proof (state)
this:
\<exists>y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y

goal (1 subgoal):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (state)
goal (1 subgoal):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (state)
goal (1 subgoal):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (state)
this:
(cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y

goal (1 subgoal):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (prove)
using this:
(cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y

goal (1 subgoal):
 1. cslift s' x = Some y &&& x \<notin> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} proof (state)
this:
cslift s' x = Some y
x \<notin> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (chain)
picking this:
cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation
cslift s' x = Some y
x \<notin> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} proof (prove)
using this:
cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation
cslift s' x = Some y
x \<notin> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. (\<And>x' tcb. \<lbrakk>map_to_tcbs (ksPSpace s) x' = Some tcb; x = tcb_ptr_to_ctcb_ptr x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
map_to_tcbs (ksPSpace s) x' = Some tcb
x = tcb_ptr_to_ctcb_ptr x'

goal (1 subgoal):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (chain)
picking this:
map_to_tcbs (ksPSpace s) x' = Some tcb
invs' s proof (prove)
using this:
map_to_tcbs (ksPSpace s) x' = Some tcb
invs' s

goal (1 subgoal):
 1. ko_at' tcb x' s proof (state)
this:
ko_at' tcb x' s

goal (1 subgoal):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (prove)
goal (1 subgoal):
 1. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (state)
goal (2 subgoals):
 1. x \<in> - tcb_Ptr ` {ptr..+2 ^ bits}
 2. cslift s' x = Some y proof (prove)
goal (1 subgoal):
 1. x \<in> - tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
using this:
x \<notin> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset}

goal (1 subgoal):
 1. x \<in> - tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. x \<notin> - tcb_Ptr ` {ptr..+2 ^ bits} \<Longrightarrow> x \<in> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr x' \<in> tcb_Ptr ` {ptr..+2 ^ bits} \<Longrightarrow> tcb_ptr_to_ctcb_ptr x' \<in> tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset} proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr x' \<in> tcb_Ptr ` {ptr..+2 ^ bits} \<Longrightarrow> x' \<in> {ptr..+2 ^ bits - unat ctcb_offset} proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr x' \<in> tcb_Ptr ` {ptr..+2 ^ bits} \<Longrightarrow> x' \<in> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr x' \<in> tcb_Ptr ` {ptr..+2 ^ bits} \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr x') \<in> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>tcb_ptr_to_ctcb_ptr x' = tcb_Ptr x; x \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr x') \<in> {ptr..+2 ^ bits} proof (prove)
goal:
No subgoals! proof (state)
this:
x \<in> - tcb_Ptr ` {ptr..+2 ^ bits}

goal (1 subgoal):
 1. cslift s' x = Some y proof (state)
this:
(cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y

goal (1 subgoal):
 1. \<And>x y. (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) x = Some y \<Longrightarrow> \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (prove)
using this:
(cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y

goal (1 subgoal):
 1. \<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y proof (state)
this:
\<exists>y. (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) x = Some y

goal:
No subgoals! proof (state)
this:
dom (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) = dom (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>)

goal (1 subgoal):
 1. \<And>p a a' b b'. \<lbrakk>map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) p = Some a; map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p = Some a'; (cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b; (cslift s'|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b'