theory IsolatedThreadAction

lemma map_to_ctes_partial_overwrite:
  "\<forall>x. tcb_at' (idx x) s \<Longrightarrow>
   map_to_ctes (partial_overwrite idx tsrs (ksPSpace s))
     = ctes_of s" supply if_split[split del] apply (rule ext) apply (frule dom_partial_overwrite[where tsrs=tsrs]) apply (simp add: map_to_ctes_def partial_overwrite_def
                   Let_def) apply (case_tac "x \<in> range idx") apply (clarsimp simp: put_tcb_state_regs_def) apply (drule_tac x=xa in spec) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
                   cong: if_cong) apply (simp add: put_tcb_state_regs_def put_tcb_state_regs_tcb_def
                    objBits_simps
              cong: if_cong option.case_cong) apply (case_tac obj, simp split: tcb_state_regs.split if_split) apply simp apply (rule if_cong[OF refl]) apply simp apply (case_tac "x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx") apply (clarsimp simp: put_tcb_state_regs_def) apply (drule_tac x=xa in spec) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
                   cong: if_cong) apply (simp add: put_tcb_state_regs_def put_tcb_state_regs_tcb_def
                    objBits_simps'
              cong: if_cong option.case_cong) apply (case_tac obj, simp split: tcb_state_regs.split if_split) apply (intro impI allI) apply (subgoal_tac "x - idx xa = x && mask 9") apply (clarsimp simp: tcb_cte_cases_def split: if_split) apply (drule_tac t = "idx xa" in sym) apply simp apply (simp cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> map_to_ctes (partial_overwrite idx tsrs (ksPSpace s)) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> map_to_ctes (partial_overwrite idx tsrs (ksPSpace s)) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> map_to_ctes (partial_overwrite idx tsrs (ksPSpace s)) x = ctes_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (partial_overwrite idx tsrs (ksPSpace s)) = dom (ksPSpace s)\<rbrakk> \<Longrightarrow> map_to_ctes (partial_overwrite idx tsrs (ksPSpace s)) x = ctes_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s)\<rbrakk> \<Longrightarrow> (if (\<exists>cte. (if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<in> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>cte. (if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>cte. (if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx x)) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s x) = dom (ksPSpace s)\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if idx xa && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx (idx xa && ~~ mask (objBitsKO (KOTCB undefined))))) (case ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(idx xa && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(idx xa && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if idx xa && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx (idx xa && ~~ mask (objBitsKO (KOTCB undefined))))) (case ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (idx xa - (idx xa && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (idx xa) = Some (KOCTE cte)) \<and> is_aligned (idx xa) (objBitsKO (KOCTE undefined)) \<and> {idx xa + 1..idx xa + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (idx xa) of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(idx xa && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(idx xa && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (idx xa - (idx xa && ~~ mask (objBitsKO (KOTCB undefined))))) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>cte. (if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx x)) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s x) = dom (ksPSpace s); tcb_at' (idx xa) s\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if idx xa && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx (idx xa && ~~ mask (objBitsKO (KOTCB undefined))))) (case ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(idx xa && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(idx xa && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if idx xa && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx (idx xa && ~~ mask (objBitsKO (KOTCB undefined))))) (case ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (idx xa - (idx xa && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (idx xa) = Some (KOCTE cte)) \<and> is_aligned (idx xa) (objBitsKO (KOCTE undefined)) \<and> {idx xa + 1..idx xa + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (idx xa) of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(idx xa && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(idx xa && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (idx xa && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (idx xa - (idx xa && ~~ mask (objBitsKO (KOTCB undefined))))) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>cte. (if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>xa obj. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx x)) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s x) = dom (ksPSpace s); ksPSpace s (idx xa) = Some (KOTCB obj); is_aligned (idx xa) tcbBlockSizeBits; ps_clear (idx xa) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (if {idx xa + 1..idx xa + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then Some (tcbCTable (put_tcb_state_regs_tcb (tsrs (inv idx (idx xa))) obj)) else None) = (if {idx xa + 1..idx xa + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then Some (tcbCTable obj) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>cte. (if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>xa obj. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (case tsrs (inv idx x) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcbState_update (\<lambda>_. st) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject)))) else ksPSpace s x) = dom (ksPSpace s); ksPSpace s (idx xa) = Some (KOTCB obj); is_aligned (idx xa) tcbBlockSizeBits; ps_clear (idx xa) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (if {idx xa + 1..idx xa + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then Some (tcbCTable (case tsrs (inv idx (idx xa)) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch obj)) (tcbState_update (\<lambda>_. st) obj))) else None) = (if {idx xa + 1..idx xa + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then Some (tcbCTable obj) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>cte. (if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>cte. (if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> (case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x) = (case ksPSpace s x of Some (KOCTE x) \<Rightarrow> Some x)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {})\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {})\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx x)) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; x && ~~ mask (objBitsKO (KOTCB undefined)) = idx xa\<rbrakk> \<Longrightarrow> (if {idx xa + 1..idx xa + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then map_option (\<lambda>(getF, setF). getF (put_tcb_state_regs_tcb (tsrs (inv idx (idx xa))) (case ksPSpace s (idx xa) of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcb_cte_cases (x && mask (objBitsKO (KOTCB undefined)))) else None) = (if (\<exists>tcb. ksPSpace s (idx xa) = Some (KOTCB tcb)) \<and> {idx xa + 1..idx xa + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (idx xa) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx x)) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; x && ~~ mask (objBitsKO (KOTCB undefined)) = idx xa; tcb_at' (idx xa) s\<rbrakk> \<Longrightarrow> (if {idx xa + 1..idx xa + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then map_option (\<lambda>(getF, setF). getF (put_tcb_state_regs_tcb (tsrs (inv idx (idx xa))) (case ksPSpace s (idx xa) of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcb_cte_cases (x && mask (objBitsKO (KOTCB undefined)))) else None) = (if (\<exists>tcb. ksPSpace s (idx xa) = Some (KOTCB tcb)) \<and> {idx xa + 1..idx xa + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (idx xa) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x xa obj. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (put_tcb_state_regs_tcb (tsrs (inv idx x)) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x cteSizeBits \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..x + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; x && ~~ mask tcbBlockSizeBits = idx xa; ksPSpace s (idx xa) = Some (KOTCB obj); is_aligned (idx xa) tcbBlockSizeBits; ps_clear (idx xa) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (if {idx xa + 1..idx xa + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then map_option (\<lambda>(getF, setF). getF (put_tcb_state_regs_tcb (tsrs (inv idx (idx xa))) obj)) (tcb_cte_cases (x && mask tcbBlockSizeBits)) else None) = (if {idx xa + 1..idx xa + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then map_option (\<lambda>(getF, setF). getF obj) (tcb_cte_cases (x - idx xa)) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x xa obj. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (case tsrs (inv idx x) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcbState_update (\<lambda>_. st) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject)))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x 4 \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..0xF + x} \<inter> dom (ksPSpace s) \<noteq> {}; x && ~~ mask 9 = idx xa; ksPSpace s (idx xa) = Some (KOTCB obj); is_aligned (idx xa) 9; ps_clear (idx xa) 9 s\<rbrakk> \<Longrightarrow> (if {idx xa + 1..0x1FF + idx xa} \<inter> dom (ksPSpace s) = {} then map_option (\<lambda>(getF, setF). getF (case tsrs (inv idx (idx xa)) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch obj)) (tcbState_update (\<lambda>_. st) obj))) (tcb_cte_cases (x && mask 9)) else None) = (if {idx xa + 1..0x1FF + idx xa} \<inter> dom (ksPSpace s) = {} then map_option (\<lambda>(getF, setF). getF obj) (tcb_cte_cases (x - idx xa)) else None)
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x xa obj x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (case tsrs (inv idx x) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcbState_update (\<lambda>_. st) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject)))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x 4 \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..0xF + x} \<inter> dom (ksPSpace s) \<noteq> {}; x && ~~ mask 9 = idx xa; ksPSpace s (idx xa) = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); is_aligned (idx xa) 9; ps_clear (idx xa) 9 s; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> {idx xa + 1..0x1FF + idx xa} \<inter> dom (ksPSpace s) = {} \<longrightarrow> (\<forall>x1a x2a. tsrs (inv idx (idx xa)) = TCBStateRegs x1a x2a \<longrightarrow> map_option (\<lambda>(getF, setF). getF (Thread x1 x2 x3 x4 x5 x6 x1a x8 x9 x10 x11 x12 x13 x14 x15 (atcbContextSet x2a x16))) (tcb_cte_cases (x && mask 9)) = map_option (\<lambda>(getF, setF). getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)) (tcb_cte_cases (x - idx xa)))
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x xa obj x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x1a x2a. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (case tsrs (inv idx x) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcbState_update (\<lambda>_. st) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject)))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x 4 \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..0xF + x} \<inter> dom (ksPSpace s) \<noteq> {}; x && ~~ mask 9 = idx xa; ksPSpace s (idx xa) = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); is_aligned (idx xa) 9; ps_clear (idx xa) 9 s; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16; {idx xa + 1..0x1FF + idx xa} \<inter> dom (ksPSpace s) = {}; tsrs (inv idx (idx xa)) = TCBStateRegs x1a x2a\<rbrakk> \<Longrightarrow> map_option (\<lambda>(getF, setF). getF (Thread x1 x2 x3 x4 x5 x6 x1a x8 x9 x10 x11 x12 x13 x14 x15 (atcbContextSet x2a x16))) (tcb_cte_cases (x && mask 9)) = map_option (\<lambda>(getF, setF). getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)) (tcb_cte_cases (x - idx xa))
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (3 subgoals):
 1. \<And>x xa obj x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x1a x2a. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (case tsrs (inv idx x) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcbState_update (\<lambda>_. st) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject)))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x 4 \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..0xF + x} \<inter> dom (ksPSpace s) \<noteq> {}; x && ~~ mask 9 = idx xa; ksPSpace s (idx xa) = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); is_aligned (idx xa) 9; ps_clear (idx xa) 9 s; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16; {idx xa + 1..0x1FF + idx xa} \<inter> dom (ksPSpace s) = {}; tsrs (inv idx (idx xa)) = TCBStateRegs x1a x2a; x - idx xa = x && mask 9\<rbrakk> \<Longrightarrow> map_option (\<lambda>(getF, setF). getF (Thread x1 x2 x3 x4 x5 x6 x1a x8 x9 x10 x11 x12 x13 x14 x15 (atcbContextSet x2a x16))) (tcb_cte_cases (x && mask 9)) = map_option (\<lambda>(getF, setF). getF (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)) (tcb_cte_cases (x - idx xa))
 2. \<And>x xa obj x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x1a x2a. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (case tsrs (inv idx x) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcbState_update (\<lambda>_. st) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject)))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x 4 \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..0xF + x} \<inter> dom (ksPSpace s) \<noteq> {}; x && ~~ mask 9 = idx xa; ksPSpace s (idx xa) = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); is_aligned (idx xa) 9; ps_clear (idx xa) 9 s; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16; {idx xa + 1..0x1FF + idx xa} \<inter> dom (ksPSpace s) = {}; tsrs (inv idx (idx xa)) = TCBStateRegs x1a x2a\<rbrakk> \<Longrightarrow> x - idx xa = x && mask 9
 3. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x xa obj x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x1a x2a. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (case tsrs (inv idx x) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcbState_update (\<lambda>_. st) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject)))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x 4 \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..0xF + x} \<inter> dom (ksPSpace s) \<noteq> {}; x && ~~ mask 9 = idx xa; ksPSpace s (idx xa) = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); is_aligned (idx xa) 9; ps_clear (idx xa) 9 s; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16; {idx xa + 1..0x1FF + idx xa} \<inter> dom (ksPSpace s) = {}; tsrs (inv idx (idx xa)) = TCBStateRegs x1a x2a\<rbrakk> \<Longrightarrow> x - idx xa = x && mask 9
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x xa obj x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x1a x2a. \<lbrakk>dom (\<lambda>x. if x \<in> range idx then Some (KOTCB (case tsrs (inv idx x) of TCBStateRegs st regs \<Rightarrow> tcbArch_update (\<lambda>_. atcbContextSet regs (tcbArch (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject))) (tcbState_update (\<lambda>_. st) (case ksPSpace s x of None \<Rightarrow> makeObject | Some (KOTCB tcb) \<Rightarrow> tcb | Some _ \<Rightarrow> makeObject)))) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; is_aligned x 4 \<longrightarrow> (\<forall>cte. ksPSpace s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..0xF + x} \<inter> dom (ksPSpace s) \<noteq> {}; ksPSpace s (idx xa) = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); is_aligned (idx xa) 9; ps_clear (idx xa) 9 s; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16; {idx xa + 1..0x1FF + idx xa} \<inter> dom (ksPSpace s) = {}; tsrs (inv idx (idx xa)) = TCBStateRegs x1a x2a; idx xa = x && ~~ mask 9\<rbrakk> \<Longrightarrow> x - idx xa = x && mask 9
 2. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); x \<notin> range idx; \<not> ((\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}); x && ~~ mask (objBitsKO (KOTCB undefined)) \<notin> range idx\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx then put_tcb_state_regs (tsrs (inv idx (x && ~~ mask (objBitsKO (KOTCB undefined))))) (ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined)))) else ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal:
No subgoals!