theory KHeap_R

lemma map_to_ctes_upd_other:
  "\<lbrakk> s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True;
     case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True \<rbrakk> \<Longrightarrow>
     map_to_ctes (s (p \<mapsto> ko')) = (map_to_ctes s)" apply (rule ext) apply (simp    add: map_to_ctes_def Let_def dom_fun_upd2
           split del: if_split del: dom_fun_upd
                cong: if_cong) apply (rule if_cong) apply clarsimp apply fastforce apply clarsimp apply (rule if_cong) apply clarsimp apply fastforce apply clarsimp apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> map_to_ctes (s(p \<mapsto> ko')) = map_to_ctes s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> map_to_ctes (s(p \<mapsto> ko')) x = map_to_ctes s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> (if (\<exists>cte. (if x = p then Some ko' else s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case if x = p then Some ko' else s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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 s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. 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 s = {} then case 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. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> ((\<exists>cte. (if x = p then Some ko' else s x) = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}) = ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {})
 2. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}\<rbrakk> \<Longrightarrow> (case if x = p then Some ko' else s x of Some (KOCTE x) \<Rightarrow> Some x) = (case s x of Some (KOCTE x) \<Rightarrow> Some x)
 3. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {})\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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 s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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. 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 s = {} then case 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. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> ((\<exists>cte. ko' = KOCTE cte) \<and> is_aligned p (objBitsKO (KOCTE undefined)) \<and> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}) = ((\<exists>cte. ko = KOCTE cte) \<and> is_aligned p (objBitsKO (KOCTE undefined)) \<and> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {})
 2. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}\<rbrakk> \<Longrightarrow> (case if x = p then Some ko' else s x of Some (KOCTE x) \<Rightarrow> Some x) = (case s x of Some (KOCTE x) \<Rightarrow> Some x)
 3. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {})\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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 s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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. 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 s = {} then case 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>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}\<rbrakk> \<Longrightarrow> (case if x = p then Some ko' else s x of Some (KOCTE x) \<Rightarrow> Some x) = (case s x of Some (KOCTE x) \<Rightarrow> Some x)
 2. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {})\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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 s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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. 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 s = {} then case 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>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {})\<rbrakk> \<Longrightarrow> (if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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 s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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. 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 s = {} then case 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. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {})\<rbrakk> \<Longrightarrow> ((\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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 s = {}) = ((\<exists>tcb. 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 s = {})
 2. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}); (\<exists>tcb. 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 s = {}\<rbrakk> \<Longrightarrow> (case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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)))))) = (case 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))))))
 3. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}); \<not> ((\<exists>tcb. 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 s = {})\<rbrakk> \<Longrightarrow> None = None proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; is_aligned x (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. s x \<noteq> Some (KOCTE cte)) \<or> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s \<noteq> {}; p = x && ~~ mask (objBitsKO (KOTCB undefined))\<rbrakk> \<Longrightarrow> ((\<exists>tcb. ko' = KOTCB tcb) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {}) = ((\<exists>tcb. ko = KOTCB tcb) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {})
 2. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}); (\<exists>tcb. 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 s = {}\<rbrakk> \<Longrightarrow> (case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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)))))) = (case 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))))))
 3. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}); \<not> ((\<exists>tcb. 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 s = {})\<rbrakk> \<Longrightarrow> None = None proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}); (\<exists>tcb. 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 s = {}\<rbrakk> \<Longrightarrow> (case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some ko' else 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)))))) = (case 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))))))
 2. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}); \<not> ((\<exists>tcb. 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 s = {})\<rbrakk> \<Longrightarrow> None = None proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s p = Some ko; case ko of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; case ko' of KOTCB tcb \<Rightarrow> False | KOCTE cte \<Rightarrow> False | _ \<Rightarrow> True; \<not> ((\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {}); \<not> ((\<exists>tcb. 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 s = {})\<rbrakk> \<Longrightarrow> None = None proof (prove)
goal:
No subgoals!