theory ADT_C

lemma map_to_cnes_eq:
  assumes aligned: "pspace_aligned' s"   and aligned': "pspace_aligned' s'"
  assumes distinct: "pspace_distinct' s" and distinct': "pspace_distinct' s'"
  shows
  "ctes_of s' = ctes_of s \<Longrightarrow>
   map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s) \<Longrightarrow>
   (projectKO_opt::kernel_object\<rightharpoonup>cte) \<circ>\<^sub>m ksPSpace s' =
   (projectKO_opt::kernel_object\<rightharpoonup>cte) \<circ>\<^sub>m ksPSpace s" apply (rule ext) apply (simp add: fun_eq_iff) apply (drule_tac x=x in spec) apply (case_tac "ksPSpace s x", case_tac "ksPSpace s' x", simp) apply (clarsimp simp add: projectKO_opt_cte split: kernel_object.splits) apply (frule SR_lemmas_C.ctes_of_ksI[OF _ aligned' distinct'], simp) apply (drule_tac t="ctes_of s x" in sym) apply (frule ctes_of_cte_at, simp add: cte_at'_obj_at') apply (elim disjE) apply (simp add: obj_at'_def) apply (clarsimp simp add: obj_at'_real_def ko_wp_at'_def) apply (clarsimp simp add: projectKO_opt_tcb split: kernel_object.splits) apply (drule_tac x="x-n" in spec) apply (clarsimp simp add: map_comp_def projectKO_opt_tcb
                   split: option.splits kernel_object.splits) apply (frule_tac x="x-n" in pspace_distinctD'[OF _ distinct']) apply (simp add: objBitsKO_def) apply (erule_tac y=x and s=s' and getF=a and setF=b
          in tcb_space_clear[rotated], assumption+, simp+) apply (case_tac "ksPSpace s' x") apply (clarsimp simp add: projectKO_opt_cte split: kernel_object.splits) apply (frule SR_lemmas_C.ctes_of_ksI[OF _ aligned distinct], simp) apply (frule ctes_of_cte_at, simp add: cte_at'_obj_at') apply (elim disjE) apply (simp add: obj_at'_def) apply (clarsimp simp add: obj_at'_real_def ko_wp_at'_def) apply (clarsimp simp add: projectKO_opt_tcb split: kernel_object.splits) apply (drule_tac x="x-n" in spec) apply (clarsimp simp add: map_comp_def projectKO_opt_tcb
                   split: option.splits kernel_object.splits) apply (frule_tac x="x-n" in pspace_distinctD'[OF _ distinct]) apply (simp add: objBitsKO_def) apply (erule_tac y=x and s=s and getF=a and setF=b
          in tcb_space_clear[rotated], assumption+, simp+) apply (case_tac "EX cte. ksPSpace s x = Some (KOCTE cte)", clarsimp) apply (frule SR_lemmas_C.ctes_of_ksI[OF _ aligned distinct], simp) apply (drule ctes_of_cte_wp_atD)+ apply (simp add: cte_wp_at'_obj_at') apply (elim disjE) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def) apply (thin_tac "Bex A P" for A P) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKO_opt_cte) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def
                          projectKO_opt_cte projectKO_opt_tcb) apply (case_tac ko, simp_all, clarsimp simp: objBitsKO_def) apply (erule_tac y=x and s=s' and getF=a and setF=b
           in tcb_space_clear[rotated], assumption+) apply (drule_tac x=x in spec, simp add: projectKO_opt_tcb) apply simp apply (thin_tac "Bex A P" for A P) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def
                         projectKO_opt_cte projectKO_opt_tcb) apply (case_tac ko, simp_all, clarsimp simp: objBitsKO_def) apply (erule_tac y=x and s=s and getF=a and setF=b
          in tcb_space_clear[rotated], assumption+, simp+) apply (case_tac "EX cte. ksPSpace s' x = Some (KOCTE cte)", clarsimp) apply (frule SR_lemmas_C.ctes_of_ksI[OF _ aligned' distinct'], simp) apply (drule_tac t="ctes_of s x" in sym) apply (drule ctes_of_cte_wp_atD)+ apply (simp add: cte_wp_at'_obj_at') apply (elim disjE) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKO_opt_cte) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def
                         projectKO_opt_cte projectKO_opt_tcb) apply (case_tac ko, simp_all, clarsimp simp: objBitsKO_def) apply (erule_tac y=x and s=s and getF=aa and setF=b
          in tcb_space_clear[rotated], assumption+) apply (drule_tac x=x in spec, simp add: projectKO_opt_tcb) apply simp apply (clarsimp simp: projectKO_opt_cte split: kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s' = ctes_of s; map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s)\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') = map_to_cnes (ksPSpace s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ctes_of s' = ctes_of s; map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s)\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. ctes_of s' x = ctes_of s x; \<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = None; ksPSpace s' x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; Some x7 = ctes_of s x; ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = ctes_of s x\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = ctes_of s x; ctes_of s x = Some x7\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; real_cte_at' x s \<or> (\<exists>n\<in>dom tcb_cte_cases. tcb_at' (x - n) s)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (3 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; real_cte_at' x s\<rbrakk> \<Longrightarrow> False
 2. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (x - n) s\<rbrakk> \<Longrightarrow> False
 3. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (x - n) s\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n ko a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s (x - n) = Some ko; is_aligned (x - n) (objBitsKO ko); ps_clear (x - n) (objBitsKO ko) s; projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s (x - n) = Some (KOTCB obj); is_aligned (x - n) (objBitsKO (KOTCB obj)); ps_clear (x - n) (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b obj. \<lbrakk>ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s (x - n) = Some (KOTCB obj); is_aligned (x - n) (objBitsKO (KOTCB obj)); ps_clear (x - n) (objBitsKO (KOTCB obj)) s; map_to_tcbs (ksPSpace s') (x - n) = map_to_tcbs (ksPSpace s) (x - n)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b obj. \<lbrakk>ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s (x - n) = Some (KOTCB obj); is_aligned (x - n) (objBitsKO (KOTCB obj)); ps_clear (x - n) (objBitsKO (KOTCB obj)) s; ksPSpace s' (x - n) = Some (KOTCB obj)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b obj. \<lbrakk>ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s (x - n) = Some (KOTCB obj); is_aligned (x - n) (objBitsKO (KOTCB obj)); ps_clear (x - n) (objBitsKO (KOTCB obj)) s; ksPSpace s' (x - n) = Some (KOTCB obj); ps_clear (x - n) (objBitsKO (KOTCB obj)) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b obj. \<lbrakk>ksPSpace s x = None; ksPSpace s' x = Some (KOCTE x7); ctes_of s' x = Some x7; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s (x - n) = Some (KOTCB obj); is_aligned (x - n) tcbBlockSizeBits; ps_clear (x - n) tcbBlockSizeBits s; ksPSpace s' (x - n) = Some (KOTCB obj); ps_clear (x - n) tcbBlockSizeBits s'\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = None\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; real_cte_at' x s' \<or> (\<exists>n\<in>dom tcb_cte_cases. tcb_at' (x - n) s')\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (3 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; real_cte_at' x s'\<rbrakk> \<Longrightarrow> False
 2. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (x - n) s'\<rbrakk> \<Longrightarrow> False
 3. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; \<exists>n\<in>dom tcb_cte_cases. tcb_at' (x - n) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n ko a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s' (x - n) = Some ko; is_aligned (x - n) (objBitsKO ko); ps_clear (x - n) (objBitsKO ko) s'; projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s' (x - n) = Some (KOTCB obj); is_aligned (x - n) (objBitsKO (KOTCB obj)); ps_clear (x - n) (objBitsKO (KOTCB obj)) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b obj. \<lbrakk>ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s' (x - n) = Some (KOTCB obj); is_aligned (x - n) (objBitsKO (KOTCB obj)); ps_clear (x - n) (objBitsKO (KOTCB obj)) s'; map_to_tcbs (ksPSpace s') (x - n) = map_to_tcbs (ksPSpace s) (x - n)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b x6. \<lbrakk>ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s' (x - n) = Some (KOTCB x6); is_aligned (x - n) (objBitsKO (KOTCB x6)); ps_clear (x - n) (objBitsKO (KOTCB x6)) s'; ksPSpace s (x - n) = Some (KOTCB x6)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b x6. \<lbrakk>ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s' (x - n) = Some (KOTCB x6); is_aligned (x - n) (objBitsKO (KOTCB x6)); ps_clear (x - n) (objBitsKO (KOTCB x6)) s'; ksPSpace s (x - n) = Some (KOTCB x6); ps_clear (x - n) (objBitsKO (KOTCB x6)) s\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x x7 n a b x6. \<lbrakk>ctes_of s' x = Some x7; ksPSpace s x = Some (KOCTE x7); ksPSpace s' x = None; ctes_of s x = Some x7; tcb_cte_cases n = Some (a, b); ksPSpace s' (x - n) = Some (KOTCB x6); is_aligned (x - n) tcbBlockSizeBits; ps_clear (x - n) tcbBlockSizeBits s'; ksPSpace s (x - n) = Some (KOTCB x6); ps_clear (x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> map_to_cnes (ksPSpace s') x = projectKO_opt a proof (prove)
goal (1 subgoal):
 1. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<nexists>cte. ksPSpace s x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = Some cte; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; ctes_of s x = Some cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<nexists>cte. ksPSpace s x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; cte_wp_at' ((=) cte) x s'; cte_wp_at' ((=) cte) x s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<nexists>cte. ksPSpace s x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; obj_at' ((=) cte) x s' \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'); obj_at' ((=) cte) x s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<nexists>cte. ksPSpace s x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (5 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; obj_at' ((=) cte) x s'; obj_at' ((=) cte) x s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; obj_at' ((=) cte) x s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 3. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; obj_at' ((=) cte) x s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 4. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 5. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<nexists>cte. ksPSpace s x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (4 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; obj_at' ((=) cte) x s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; obj_at' ((=) cte) x s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 3. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 4. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<nexists>cte. ksPSpace s x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (4 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; obj_at' ((=) cte) x s'\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; obj_at' ((=) cte) x s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 3. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 4. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<nexists>cte. ksPSpace s x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (3 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; obj_at' ((=) cte) x s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 3. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<nexists>cte. ksPSpace s x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (3 subgoals):
 1. \<And>x aa n ko a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE (a obj)); ksPSpace s' x = Some aa; tcb_cte_cases n = Some (a, b); is_aligned x (objBitsKO (KOCTE (a obj))); ps_clear x (objBitsKO (KOCTE (a obj))) s; ksPSpace s' (x - n) = Some ko; is_aligned (x - n) (objBitsKO ko); ps_clear (x - n) (objBitsKO ko) s'; (case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some obj\<rbrakk> \<Longrightarrow> (case aa of KOCTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some (a obj)
 2. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 3. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<nexists>cte. ksPSpace s x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (3 subgoals):
 1. \<And>x aa n a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE (a obj)); ksPSpace s' x = Some aa; tcb_cte_cases n = Some (a, b); is_aligned x cteSizeBits; ps_clear x cteSizeBits s; ksPSpace s' (x - n) = Some (KOTCB obj); is_aligned (x - n) tcbBlockSizeBits; ps_clear (x - n) tcbBlockSizeBits s'\<rbrakk> \<Longrightarrow> (case aa of KOCTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some (a obj)
 2. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 3. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (4 subgoals):
 1. \<And>x aa n a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE (a obj)); ksPSpace s' x = Some aa; tcb_cte_cases n = Some (a, b); is_aligned x cteSizeBits; ps_clear x cteSizeBits s; ksPSpace s' (x - n) = Some (KOTCB obj); ps_clear (x - n) tcbBlockSizeBits s'; x - n = x; a = tcb.tcbCTable; b = tcbCTable_update\<rbrakk> \<Longrightarrow> (case aa of KOCTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some (a obj)
 2. \<And>x aa n a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE (a obj)); ksPSpace s' x = Some aa; tcb_cte_cases n = Some (a, b); is_aligned x cteSizeBits; ps_clear x cteSizeBits s; ksPSpace s' (x - n) = Some (KOTCB obj); ps_clear (x - n) tcbBlockSizeBits s'\<rbrakk> \<Longrightarrow> tcb_cte_cases (x - (x - n)) = Some (a, b)
 3. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 4. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (3 subgoals):
 1. \<And>x aa n a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE (a obj)); ksPSpace s' x = Some aa; tcb_cte_cases n = Some (a, b); is_aligned x cteSizeBits; ps_clear x cteSizeBits s; ksPSpace s' (x - n) = Some (KOTCB obj); ps_clear (x - n) tcbBlockSizeBits s'\<rbrakk> \<Longrightarrow> tcb_cte_cases (x - (x - n)) = Some (a, b)
 2. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 3. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s'; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x aa cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE cte); ksPSpace s' x = Some aa; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt (KOCTE cte)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x aa n ko a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE (a obj)); ksPSpace s' x = Some aa; tcb_cte_cases n = Some (a, b); ksPSpace s (x - n) = Some ko; is_aligned (x - n) (objBitsKO ko); ps_clear (x - n) (objBitsKO ko) s; (case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some obj\<rbrakk> \<Longrightarrow> (case aa of KOCTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some (a obj)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x aa n a b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some (KOCTE (a obj)); ksPSpace s' x = Some aa; tcb_cte_cases n = Some (a, b); ksPSpace s (x - n) = Some (KOTCB obj); is_aligned (x - n) tcbBlockSizeBits; ps_clear (x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (case aa of KOCTE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some (a obj)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (1 subgoal):
 1. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE cte); \<forall>cte. a \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt (KOCTE cte) = projectKO_opt a
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<nexists>cte. ksPSpace s' x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; Some cte = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE cte); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x\<rbrakk> \<Longrightarrow> projectKO_opt (KOCTE cte) = projectKO_opt a
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<nexists>cte. ksPSpace s' x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE cte); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; ctes_of s x = Some cte\<rbrakk> \<Longrightarrow> projectKO_opt (KOCTE cte) = projectKO_opt a
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<nexists>cte. ksPSpace s' x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE cte); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; cte_wp_at' ((=) cte) x s\<rbrakk> \<Longrightarrow> projectKO_opt (KOCTE cte) = projectKO_opt a
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<nexists>cte. ksPSpace s' x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE cte); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; obj_at' ((=) cte) x s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s)\<rbrakk> \<Longrightarrow> projectKO_opt (KOCTE cte) = projectKO_opt a
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<nexists>cte. ksPSpace s' x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (3 subgoals):
 1. \<And>x a cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE cte); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; obj_at' ((=) cte) x s\<rbrakk> \<Longrightarrow> projectKO_opt (KOCTE cte) = projectKO_opt a
 2. \<And>x a cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE cte); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt (KOCTE cte) = projectKO_opt a
 3. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<nexists>cte. ksPSpace s' x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a cte. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE cte); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (x - n) s\<rbrakk> \<Longrightarrow> projectKO_opt (KOCTE cte) = projectKO_opt a
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<nexists>cte. ksPSpace s' x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a n ko aa b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE (aa obj)); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; tcb_cte_cases n = Some (aa, b); ksPSpace s (x - n) = Some ko; is_aligned (x - n) (objBitsKO ko); ps_clear (x - n) (objBitsKO ko) s; (case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some obj\<rbrakk> \<Longrightarrow> Some (aa obj) = (case a of KOCTE x \<Rightarrow> Some x | _ \<Rightarrow> None)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<nexists>cte. ksPSpace s' x = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a n aa b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE (aa obj)); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; tcb_cte_cases n = Some (aa, b); ksPSpace s (x - n) = Some (KOTCB obj); is_aligned (x - n) tcbBlockSizeBits; ps_clear (x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> Some (aa obj) = (case a of KOCTE x \<Rightarrow> Some x | _ \<Rightarrow> None)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<forall>cte. aa \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (3 subgoals):
 1. \<And>x a n aa b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE (aa obj)); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; tcb_cte_cases n = Some (aa, b); ksPSpace s (x - n) = Some (KOTCB obj); ps_clear (x - n) tcbBlockSizeBits s; x - n = x; aa = tcb.tcbCTable; b = tcbCTable_update\<rbrakk> \<Longrightarrow> Some (aa obj) = (case a of KOCTE x \<Rightarrow> Some x | _ \<Rightarrow> None)
 2. \<And>x a n aa b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE (aa obj)); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; tcb_cte_cases n = Some (aa, b); ksPSpace s (x - n) = Some (KOTCB obj); ps_clear (x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (x - (x - n)) = Some (aa, b)
 3. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<forall>cte. aa \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (2 subgoals):
 1. \<And>x a n aa b obj. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ksPSpace s x = Some a; ksPSpace s' x = Some (KOCTE (aa obj)); \<forall>cte. a \<noteq> KOCTE cte; ctes_of s' x = ctes_of s x; tcb_cte_cases n = Some (aa, b); ksPSpace s (x - n) = Some (KOTCB obj); ps_clear (x - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (x - (x - n)) = Some (aa, b)
 2. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<forall>cte. aa \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal (1 subgoal):
 1. \<And>x a aa. \<lbrakk>\<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; ctes_of s' x = ctes_of s x; ksPSpace s x = Some a; ksPSpace s' x = Some aa; \<forall>cte. a \<noteq> KOCTE cte; \<forall>cte. aa \<noteq> KOCTE cte\<rbrakk> \<Longrightarrow> projectKO_opt aa = projectKO_opt a proof (prove)
goal:
No subgoals!