theory Detype_R

lemma setCTE_modify_tcbDomain_commute:
 " monad_commute
    (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte)
    (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr)" proof - note blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
          atLeastAtMost_iff have hint:
      "\<And>P ptr a cte b src ra. monad_commute (tcb_at' ptr and ko_wp_at' P a )
      (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr)
             (modify (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a))))" apply (clarsimp simp add: monad_commute_def
        bind_def simpler_modify_def return_def) apply (clarsimp simp:threadSet_det simpler_modify_def) apply (subgoal_tac "tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)") prefer 2 apply (clarsimp simp:obj_at'_def) apply (intro conjI impI) apply simp apply (clarsimp simp:projectKO_eq
            projectKO_opt_tcb split:Structures_H.kernel_object.split_asm) apply (simp add:cte_update_def) apply (clarsimp simp:projectKO_eq
           projectKO_opt_tcb split:Structures_H.kernel_object.split_asm) apply (simp add:ps_clear_def) apply (clarsimp simp:projectKO_eq
          projectKO_opt_tcb split:Structures_H.kernel_object.split_asm) apply (simp add:ps_clear_def) apply (rule ccontr,simp) apply (erule in_emptyE) apply (clarsimp simp:ko_wp_at'_def) apply blast apply (simp add:threadSet_det simpler_modify_def) apply (subst (asm) obj_at'_def) apply (thin_tac "tcb_at' ptr P" for P) apply (clarsimp simp: obj_at'_def projectKO_eq projectKO_opt_tcb,
             simp split: Structures_H.kernel_object.split_asm) apply (case_tac s,clarsimp) apply (intro conjI) apply clarsimp apply (rule ext,clarsimp) apply (case_tac obj) apply (simp add:cte_update_def) apply clarsimp apply (rule ext) apply simp done show ?thesis apply (rule commute_name_pre_state) apply (clarsimp simp add: setCTE_def2) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF  monad_commute_split]) apply (rule hint) apply (rule commute_commute) apply (rule locateCTE_commute) apply (wp locateCTE_cte_no_fail)+ apply (wp threadSet_ko_wp_at2') apply (clarsimp simp:objBits_simps) apply (wp|simp)+ apply (wp locateCTE_inv locateCTE_ko_wp_at') apply clarsimp apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) proof (state)
goal (1 subgoal):
 1. monad_commute (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) proof (state)
this:
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)

goal (1 subgoal):
 1. monad_commute (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte b src ra. monad_commute (tcb_at' ptr and ko_wp_at' P a) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) (modify (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)))) proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s\<rbrakk> \<Longrightarrow> (\<Union>aa\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr s). fst (case aa of (x, s) \<Rightarrow> ({(((), ()), ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}, False))) = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> ((\<exists>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr s). snd (case x of (x, s) \<Rightarrow> ({(((), ()), ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}, False))) \<or> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr s)) = ((\<exists>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<or> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s))) proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s))
 2. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s\<rbrakk> \<Longrightarrow> tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s) proof (prove)
goal (2 subgoals):
 1. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s\<rbrakk> \<Longrightarrow> tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 2. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}\<rbrakk> \<Longrightarrow> (ptr = a \<longrightarrow> is_aligned a (objBitsKO (the (ksPSpace s a))) \<and> (\<exists>obj. fst (projectKO (cte_update cte (the (ksPSpace s a)) src a) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}) \<and> ps_clear a (objBitsKO (the (ksPSpace s a))) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) \<and> (ptr \<noteq> a \<longrightarrow> (\<exists>obj. fst (projectKO ko (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}) \<and> ps_clear ptr (objBitsKO ko) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s))
 2. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (6 subgoals):
 1. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr = a\<rbrakk> \<Longrightarrow> is_aligned a (objBitsKO (the (ksPSpace s a)))
 2. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr = a\<rbrakk> \<Longrightarrow> \<exists>obj. fst (projectKO (cte_update cte (the (ksPSpace s a)) src a) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}
 3. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr = a\<rbrakk> \<Longrightarrow> ps_clear a (objBitsKO (the (ksPSpace s a))) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 4. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>obj. fst (projectKO ko (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}
 5. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 6. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (5 subgoals):
 1. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr = a\<rbrakk> \<Longrightarrow> \<exists>obj. fst (projectKO (cte_update cte (the (ksPSpace s a)) src a) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}
 2. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr = a\<rbrakk> \<Longrightarrow> ps_clear a (objBitsKO (the (ksPSpace s a))) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 3. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>obj. fst (projectKO ko (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}
 4. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 5. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (5 subgoals):
 1. \<And>P a cte src s obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s a = Some (KOTCB obj); is_aligned a (objBitsKO (KOTCB obj)); ps_clear a (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> \<exists>obja. (case cte_update cte (KOTCB obj) src a of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some obja
 2. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr = a\<rbrakk> \<Longrightarrow> ps_clear a (objBitsKO (the (ksPSpace s a))) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 3. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>obj. fst (projectKO ko (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}
 4. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 5. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (4 subgoals):
 1. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr = a\<rbrakk> \<Longrightarrow> ps_clear a (objBitsKO (the (ksPSpace s a))) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 2. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>obj. fst (projectKO ko (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}
 3. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 4. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (4 subgoals):
 1. \<And>P a cte src s obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s a = Some (KOTCB obj); is_aligned a (objBitsKO (KOTCB obj)); ps_clear a (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> ps_clear a (objBitsKO (KOTCB obj)) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 2. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>obj. fst (projectKO ko (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}
 3. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 4. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (3 subgoals):
 1. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>obj. fst (projectKO ko (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) = {(obj, ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)}
 2. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 3. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>P ptr a cte src s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)
 2. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>P ptr a s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ({ptr..ptr + 2 ^ objBitsKO ko - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a\<rbrakk> \<Longrightarrow> a \<notin> {ptr..ptr + 2 ^ objBitsKO ko - 1}
 2. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>P ptr a s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ({ptr..ptr + 2 ^ objBitsKO ko - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a; a \<in> {ptr..ptr + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>P ptr a s ko obj. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a; a \<in> {ptr..ptr + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> ?x143 P ptr a s ko obj \<in> ({ptr..ptr + 2 ^ objBitsKO ko - 1} - {ptr}) \<inter> dom (ksPSpace s)
 2. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (2 subgoals):
 1. \<And>P ptr a s ko obj koa. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; ptr \<noteq> a; a \<in> {ptr..ptr + 2 ^ objBitsKO ko - 1}; ksPSpace s a = Some koa; is_aligned a (objBitsKO koa); P koa; ps_clear a (objBitsKO koa) s\<rbrakk> \<Longrightarrow> ?x143 P ptr a s ko obj \<in> {ptr..ptr + 2 ^ objBitsKO ko - 1} \<and> ?x143 P ptr a s ko obj \<noteq> ptr \<and> ?x143 P ptr a s ko obj \<in> dom (ksPSpace s)
 2. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> {(((), ()), ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s)} = (\<Union>a\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). fst (case a of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> (\<forall>x\<in>fst (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)). \<not> snd (case x of (x, s) \<Rightarrow> ({(((), ()), s)}, False))) \<and> \<not> snd (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)) proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra s. \<lbrakk>tcb_at' ptr s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s = ksPSpace_update ((\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb))) \<circ> (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a))) s proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra s. \<lbrakk>\<exists>ko obj. ksPSpace s ptr = Some ko \<and> is_aligned ptr (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> True \<and> ps_clear ptr (objBitsKO ko) s; ko_wp_at' P a s; tcb_at' ptr (ksPSpace_update (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) s)\<rbrakk> \<Longrightarrow> ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s = ksPSpace_update ((\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb))) \<circ> (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a))) s proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra s. \<lbrakk>\<exists>ko obj. ksPSpace s ptr = Some ko \<and> is_aligned ptr (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> True \<and> ps_clear ptr (objBitsKO ko) s; ko_wp_at' P a s\<rbrakk> \<Longrightarrow> ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s = ksPSpace_update ((\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb))) \<circ> (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a))) s proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra s ko obj x6. \<lbrakk>ko_wp_at' P a s; ksPSpace s ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) s; ko = KOTCB obj; x6 = obj\<rbrakk> \<Longrightarrow> ksPSpace_update ((\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a)) \<circ> (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb)))) s = ksPSpace_update ((\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb))) \<circ> (\<lambda>ps. ps(a \<mapsto> cte_update cte (the (ps a)) src a))) s proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> (ptr = a \<longrightarrow> ksPSpace(a \<mapsto> cte_update cte (KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) src a) = ksPSpace(a \<mapsto> case cte_update cte (the (ksPSpace a)) src a of KOTCB tcb \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb))) \<and> (ptr \<noteq> a \<longrightarrow> ksPSpace(ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj), a \<mapsto> cte_update cte (the (ksPSpace a)) src a) = ksPSpace(a \<mapsto> cte_update cte (the (ksPSpace a)) src a, ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj))) proof (prove)
goal (2 subgoals):
 1. \<And>P ptr a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> ptr = a \<longrightarrow> ksPSpace(a \<mapsto> cte_update cte (KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) src a) = ksPSpace(a \<mapsto> case cte_update cte (the (ksPSpace a)) src a of KOTCB tcb \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb))
 2. \<And>P ptr a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> ptr \<noteq> a \<longrightarrow> ksPSpace(ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj), a \<mapsto> cte_update cte (the (ksPSpace a)) src a) = ksPSpace(a \<mapsto> cte_update cte (the (ksPSpace a)) src a, ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) proof (prove)
goal (2 subgoals):
 1. \<And>P a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace a = Some (KOTCB obj); is_aligned a (objBitsKO (KOTCB obj)); ps_clear a (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> ksPSpace(a \<mapsto> cte_update cte (KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) src a) = ksPSpace(a \<mapsto> case cte_update cte (KOTCB obj) src a of KOTCB tcb \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb))
 2. \<And>P ptr a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> ptr \<noteq> a \<longrightarrow> ksPSpace(ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj), a \<mapsto> cte_update cte (the (ksPSpace a)) src a) = ksPSpace(a \<mapsto> cte_update cte (the (ksPSpace a)) src a, ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) proof (prove)
goal (2 subgoals):
 1. \<And>P a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace a = Some (KOTCB obj); is_aligned a (objBitsKO (KOTCB obj)); ps_clear a (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> cte_update cte (KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) src a = (case cte_update cte (KOTCB obj) src a of KOTCB tcb \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb))
 2. \<And>P ptr a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> ptr \<noteq> a \<longrightarrow> ksPSpace(ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj), a \<mapsto> cte_update cte (the (ksPSpace a)) src a) = ksPSpace(a \<mapsto> cte_update cte (the (ksPSpace a)) src a, ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) proof (prove)
goal (2 subgoals):
 1. \<And>P a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace a = Some (KOTCB obj); is_aligned a (objBitsKO (KOTCB obj)); ps_clear a (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> cte_update cte (KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) src a = (case cte_update cte (KOTCB obj) src a of KOTCB tcb \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. ra) tcb))
 2. \<And>P ptr a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> ptr \<noteq> a \<longrightarrow> ksPSpace(ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj), a \<mapsto> cte_update cte (the (ksPSpace a)) src a) = ksPSpace(a \<mapsto> cte_update cte (the (ksPSpace a)) src a, ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> ptr \<noteq> a \<longrightarrow> ksPSpace(ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj), a \<mapsto> cte_update cte (the (ksPSpace a)) src a) = ksPSpace(a \<mapsto> cte_update cte (the (ksPSpace a)) src a, ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ptr \<noteq> a\<rbrakk> \<Longrightarrow> ksPSpace(ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj), a \<mapsto> cte_update cte (the (ksPSpace a)) src a) = ksPSpace(a \<mapsto> cte_update cte (the (ksPSpace a)) src a, ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj)) proof (prove)
goal (1 subgoal):
 1. \<And>P ptr a cte src ra obj ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState x. \<lbrakk>ko_wp_at' P a \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace ptr = Some (KOTCB obj); is_aligned ptr (objBitsKO (KOTCB obj)); ps_clear ptr (objBitsKO (KOTCB obj)) \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ptr \<noteq> a\<rbrakk> \<Longrightarrow> (ksPSpace(ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj), a \<mapsto> cte_update cte (the (ksPSpace a)) src a)) x = (ksPSpace(a \<mapsto> cte_update cte (the (ksPSpace a)) src a, ptr \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. ra) obj))) x proof (prove)
goal:
No subgoals! proof (state)
this:
monad_commute (tcb_at' ?ptr and ko_wp_at' ?P ?a) (threadSet (tcbDomain_update (\<lambda>_. ?ra)) ?ptr) (modify (ksPSpace_update (\<lambda>ps. ps(?a \<mapsto> cte_update ?cte (the (ps ?a)) ?src ?a))))

goal (1 subgoal):
 1. monad_commute (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) proof (prove)
goal (1 subgoal):
 1. monad_commute (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> monad_commute (?P5 s) (do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr)
 2. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> ?P5 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s r. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> monad_commute (?Q9 s r) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) (modify (ksPSpace_update (\<lambda>ps. ps(r \<mapsto> cte_update cte (the (ps r)) src r))))
 2. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> monad_commute (?P9 s) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) (locateCTE src)
 3. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 s\<rbrace> locateCTE src \<lbrace>?Q9 s\<rbrace>
 4. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> (?P9 s and ?P'9 s) sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> monad_commute (?P9 s) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr) (locateCTE src)
 2. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 s\<rbrace> locateCTE src \<lbrace>\<lambda>r. tcb_at' ptr and ko_wp_at' (?P13 s r) r\<rbrace>
 3. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> (?P9 s and ?P'9 s) sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> monad_commute (?P9 s) (locateCTE src) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr)
 2. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 s\<rbrace> locateCTE src \<lbrace>\<lambda>r. tcb_at' ptr and ko_wp_at' (?P13 s r) r\<rbrace>
 3. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> (?P9 s and ?P'9 s) sa proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> no_fail (?P0.16 s) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr)
 2. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> no_fail (?P1.16 s) (locateCTE src)
 3. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P2.16 s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>a. pspace_distinct'\<rbrace>
 4. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P3.16 s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>a. pspace_aligned'\<rbrace>
 5. \<And>s Q dest. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. (?P0.16 s and ?P1.16 s and ?P2.16 s and ?P3.16 s) sa \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest sa\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>a. ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest\<rbrace>
 6. \<And>s dest. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. (?P0.16 s and ?P1.16 s and ?P2.16 s and ?P3.16 s) sa \<and> cte_wp_at' (\<lambda>_. True) dest sa\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 7. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 s\<rbrace> locateCTE src \<lbrace>\<lambda>r. tcb_at' ptr and ko_wp_at' (?P13 s r) r\<rbrace>
 8. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> (?P0.16 s and ?P1.16 s and ?P2.16 s and ?P3.16 s and ?P4.16 s and ?P5.16 s and pspace_aligned' and pspace_distinct' and ?P'9 s) sa proof (prove)
goal (4 subgoals):
 1. \<And>s Q dest. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>a. ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest\<rbrace>
 2. \<And>s dest. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 3. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 s\<rbrace> locateCTE src \<lbrace>\<lambda>r. tcb_at' ptr and ko_wp_at' (?P13 s r) r\<rbrace>
 4. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and ?P4.16 s and ?P5.16 s and pspace_aligned' and pspace_distinct' and ?P'9 s) sa proof (prove)
goal (4 subgoals):
 1. \<And>s Q dest sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') sa \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest sa\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>a. Q (objBitsKO a)) dest sa \<and> (\<forall>tcb_x. Q (objBitsKO (injectKOS (tcbDomain_update (\<lambda>_. ra) tcb_x))) = Q (objBitsKO (injectKOS tcb_x)))
 2. \<And>s dest. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 3. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 s\<rbrace> locateCTE src \<lbrace>\<lambda>r. tcb_at' ptr and ko_wp_at' (?P13 s r) r\<rbrace>
 4. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and ?P4.16 s and ?P5.16 s and pspace_aligned' and pspace_distinct' and ?P'9 s) sa proof (prove)
goal (3 subgoals):
 1. \<And>s dest. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 2. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 s\<rbrace> locateCTE src \<lbrace>\<lambda>r. tcb_at' ptr and ko_wp_at' (?P13 s r) r\<rbrace>
 3. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and ?P4.16 s and ?P5.16 s and pspace_aligned' and pspace_distinct' and ?P'9 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 s\<rbrace> locateCTE src \<lbrace>\<lambda>r sa. tcb_at' ptr sa \<and> ko_wp_at' (?P13 s r) r sa\<rbrace>
 2. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and ?P4.16 s and ?P5.16 s and pspace_aligned' and pspace_distinct' and ?P'9 s) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>tcb_at' ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s; s = sa\<rbrakk> \<Longrightarrow> (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and ?P4.16 s and ?P5.16 s and pspace_aligned' and pspace_distinct' and (\<lambda>s. tcb_at' ptr s \<and> (cte_wp_at' (\<lambda>_. True) src and pspace_distinct') s)) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>tcb_at' ptr sa; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa\<rbrakk> \<Longrightarrow> ?P4.16 sa sa \<and> ?P5.16 sa sa proof (prove)
goal:
No subgoals! proof (state)
this:
monad_commute (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr)

goal:
No subgoals!