theory Delete_C

lemma ccorres_cutMon_locateSlotCap_Zombie:
  "\<lbrakk> (capZombiePtr cap + 2 ^ cte_level_bits * n, s) \<in> fst (locateSlotCap cap n s)
    \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf
      Q Q' hs
      (cutMon ((=) s) (a (capZombiePtr cap + 2 ^ cte_level_bits * n))) c \<rbrakk>
    \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf
      (Q and valid_cap' cap and (\<lambda>_. isZombie cap \<and> n = of_nat (capZombieNumber cap - 1)))
      {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - 1)
           (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'} hs
      (cutMon ((=) s) (locateSlotCap cap n >>= a)) c" apply (simp add: locateSlot_conv in_monad cutMon_walk_bind) apply (rule ccorres_gen_asm) apply (rule ccorres_guard_imp2) apply (rule ccorres_drop_cutMon_bind) apply (rule ccorres_symb_exec_l) apply (rule ccorres_cutMon) apply (clarsimp simp: in_monad stateAssert_def) apply (rule_tac P="\<lambda>s'. (capZombieType cap \<noteq> ZombieTCB \<longrightarrow>
           (case gsCNodes s' (capUntypedPtr cap) of None \<Rightarrow> False
                | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < 2 ^ n))"
              in ccorres_cross_over_guard) apply (clarsimp simp: isCap_simps) apply assumption apply (wp | simp)+ apply (clarsimp simp: isCap_simps stateAssert_def in_monad) apply (cases "capZombieType cap = ZombieTCB") apply (clarsimp simp: valid_cap_simps') apply (drule(1) rf_sr_tcb_ctes_array_assertion[
       where tcb="tcb_ptr_to_ctcb_ptr t" for t, simplified]) apply (simp add: tcb_cnode_index_defs array_assertion_shrink_right) apply (clarsimp simp: option.split[where P="\<lambda>x. x"]) apply (rule conjI) apply clarsimp apply blast apply (clarsimp dest!: of_nat_less_t2n) apply (drule(1) rf_sr_gsCNodes_array_assertion) apply (erule notE, erule array_assertion_shrink_right) apply (frule valid_Zombie_number_word_bits, simp+) by (simp add: unat_arith_simps unat_of_nat word_bits_def
                   valid_cap_simps')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((capZombiePtr cap + 2 ^ cte_level_bits * n, s) \<in> fst (locateSlotCap cap n s) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (capZombiePtr cap + 2 ^ cte_level_bits * n))) c) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf (Q and valid_cap' cap and (\<lambda>_. isZombie cap \<and> n = word_of_nat (capZombieNumber cap - 1))) {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - 1) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'} hs (cutMon ((=) s) (locateSlotCap cap n >>= a)) c proof (prove)
goal (1 subgoal):
 1. (((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf (Q and valid_cap' cap and (\<lambda>_. isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0))) {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'} hs (do rv <- cutMon ((=) s) (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) []);
cutMon (\<lambda>s'. ((), s') \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s)) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))
od) c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf (Q and valid_cap' cap) {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'} hs (do rv <- cutMon ((=) s) (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) []);
cutMon (\<lambda>s'. ((), s') \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s)) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))
od) c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf ?Q10 ?Q'10 hs (do rv <- cutMon ((=) s) (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) []);
cutMon (\<lambda>s'. ((), s') \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s)) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))
od) c
 2. \<And>sa s'. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); (sa, s') \<in> rf_sr; (Q and valid_cap' cap) sa; s' \<in> {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q10 sa \<and> s' \<in> ?Q'10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf ?Q10 ?Q'10 hs (do rv <- stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [];
cutMon (\<lambda>s'. ((), s') \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s)) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))
od) c
 2. \<And>sa s'. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); (sa, s') \<in> rf_sr; (Q and valid_cap' cap) sa; s' \<in> {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q10 sa \<and> s' \<in> ?Q'10 proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf (?Q15 rv) (?Q'15 rv) hs (cutMon (\<lambda>s'. ((), s') \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s)) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c
 2. \<And>sa. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>?Q15\<rbrace>
 4. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [])
 5. \<And>sa s'. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); (sa, s') \<in> rf_sr; (Q and valid_cap' cap) sa; s' \<in> {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q10 sa \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q15 rv s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (5 subgoals):
 1. \<And>rv sa. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); ((), sa) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s)\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf (?Q15 rv) (?Q'15 rv) hs (cutMon ((=) sa) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c
 2. \<And>sa. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>?Q15\<rbrace>
 4. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [])
 5. \<And>sa s'. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); (sa, s') \<in> rf_sr; (Q and valid_cap' cap) sa; s' \<in> {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q10 sa \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q15 rv s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (5 subgoals):
 1. \<lbrakk>capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * word_of_nat (capZombieNumber cap - Suc 0)))) c; (isCNodeCap cap \<or> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap cap \<and> n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> word_of_nat (capZombieNumber cap - Suc 0) < 2 ^ n) \<or> isThreadCap cap \<or> capZombieType cap = ZombieTCB; isZombie cap; n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf (?Q15 ()) (?Q'15 ()) hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * word_of_nat (capZombieNumber cap - Suc 0)))) c
 2. \<And>sa. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>?Q15\<rbrace>
 4. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [])
 5. \<And>sa s'. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); (sa, s') \<in> rf_sr; (Q and valid_cap' cap) sa; s' \<in> {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q10 sa \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q15 rv s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (5 subgoals):
 1. \<lbrakk>capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * word_of_nat (capZombieNumber cap - Suc 0)))) c; (isCNodeCap cap \<or> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap cap \<and> n = capCNodeBits cap \<or> isZombie cap \<and> n = zombieCTEBits (capZombieType cap)) \<and> word_of_nat (capZombieNumber cap - Suc 0) < 2 ^ n) \<or> isThreadCap cap \<or> capZombieType cap = ZombieTCB; isZombie cap; n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf (?P'42 ()) (?Q41 ()) hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * word_of_nat (capZombieNumber cap - Suc 0)))) c
 2. \<And>sa. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>\<lambda>a. (\<lambda>s'. capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s' (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) and ?P'42 a\<rbrace>
 4. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [])
 5. \<And>sa s'. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); (sa, s') \<in> rf_sr; (Q and valid_cap' cap) sa; s' \<in> {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q10 sa \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s'. capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s' (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) and ?P'42 rv) s \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> (capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) \<longrightarrow> s' \<in> ?Q41 rv}} proof (prove)
goal (5 subgoals):
 1. \<And>v0 v1 v2. \<lbrakk>ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; v1 \<noteq> ZombieTCB \<and> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<or> v1 = ZombieTCB; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf (?P'42 ()) (?Q41 ()) hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c
 2. \<And>sa. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>\<lambda>a. (\<lambda>s'. capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s' (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) and ?P'42 a\<rbrace>
 4. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [])
 5. \<And>sa s'. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); (sa, s') \<in> rf_sr; (Q and valid_cap' cap) sa; s' \<in> {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q10 sa \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s'. capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s' (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) and ?P'42 rv) s \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> (capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) \<longrightarrow> s' \<in> ?Q41 rv}} proof (prove)
goal (4 subgoals):
 1. \<And>sa. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] \<lbrace>\<lambda>a. (\<lambda>s'. capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s' (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) and Q\<rbrace>
 3. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0)\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [])
 4. \<And>sa s'. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> isZombie cap \<and> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> isZombie cap \<and> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * n))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); (sa, s') \<in> rf_sr; (Q and valid_cap' cap) sa; s' \<in> {s. array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q10 sa \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s'. capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s' (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) and Q) s \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> (capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) \<longrightarrow> s' \<in> Q'}} proof (prove)
goal (1 subgoal):
 1. \<And>sa s'. \<lbrakk>((), s) \<in> fst (stateAssert (\<lambda>s. (isCNodeCap cap \<or> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<or> isThreadCap cap \<or> capZombieType cap = ZombieTCB) [] s) \<and> capZombiePtr cap = global.capUntypedPtr cap \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (global.capUntypedPtr cap + 2 ^ cte_level_bits * word_of_nat (capZombieNumber cap - Suc 0)))) c; isZombie cap \<and> n = word_of_nat (capZombieNumber cap - Suc 0); (sa, s') \<in> rf_sr; Q sa \<and> valid_cap' cap sa; array_assertion (cte_Ptr (capZombiePtr cap)) (capZombieNumber cap - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'\<rbrakk> \<Longrightarrow> ((isCNodeCap cap \<or> capZombieType cap \<noteq> ZombieTCB) \<and> (case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> (isCNodeCap cap \<and> na = capCNodeBits cap \<or> isZombie cap \<and> na = zombieCTEBits (capZombieType cap)) \<and> n < 2 ^ na) \<longrightarrow> capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) \<and> (isThreadCap cap \<longrightarrow> capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes sa (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> (capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n)) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (capZombieType cap \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber cap - 1) < (2::?'g38) ^ n))) \<longrightarrow> s' \<in> Q') proof (prove)
goal (1 subgoal):
 1. \<And>sa s' v0 v1 v2. \<lbrakk>v1 \<noteq> ZombieTCB \<and> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<or> v1 = ZombieTCB \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa\<rbrakk> \<Longrightarrow> (v1 \<noteq> ZombieTCB \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n))) \<longrightarrow> s' \<in> Q') proof (prove)
goal (2 subgoals):
 1. \<And>sa s' v0 v1 v2. \<lbrakk>v1 \<noteq> ZombieTCB \<and> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<or> v1 = ZombieTCB \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; capZombieType cap = ZombieTCB\<rbrakk> \<Longrightarrow> (v1 \<noteq> ZombieTCB \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n))) \<longrightarrow> s' \<in> Q')
 2. \<And>sa s' v0 v1 v2. \<lbrakk>v1 \<noteq> ZombieTCB \<and> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<or> v1 = ZombieTCB \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; capZombieType cap \<noteq> ZombieTCB\<rbrakk> \<Longrightarrow> (v1 \<noteq> ZombieTCB \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n))) \<longrightarrow> s' \<in> Q') proof (prove)
goal (2 subgoals):
 1. \<And>sa s' v0 v2 saa sb. \<lbrakk>ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 ZombieTCB v2; Q sa; capAligned (capability.Zombie v0 ZombieTCB v2); v2 \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' v0 sa; (saa, s') \<in> rf_sr; Q saa; (sb, s') \<in> rf_sr; \<not> array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> s' \<in> Q'
 2. \<And>sa s' v0 v1 v2. \<lbrakk>v1 \<noteq> ZombieTCB \<and> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<or> v1 = ZombieTCB \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; capZombieType cap \<noteq> ZombieTCB\<rbrakk> \<Longrightarrow> (v1 \<noteq> ZombieTCB \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n))) \<longrightarrow> s' \<in> Q') proof (prove)
goal (2 subgoals):
 1. \<And>sa s' v0 v2 saa sb. \<lbrakk>ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 ZombieTCB v2; Q sa; capAligned (capability.Zombie v0 ZombieTCB v2); v2 \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' v0 sa; (saa, s') \<in> rf_sr; Q saa; (sb, s') \<in> rf_sr; \<not> array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))); array_assertion (cte_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr v0) && 0xFFFFFE00)) (unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> s' \<in> Q'
 2. \<And>sa s' v0 v1 v2. \<lbrakk>v1 \<noteq> ZombieTCB \<and> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<or> v1 = ZombieTCB \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; capZombieType cap \<noteq> ZombieTCB\<rbrakk> \<Longrightarrow> (v1 \<noteq> ZombieTCB \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n))) \<longrightarrow> s' \<in> Q') proof (prove)
goal (1 subgoal):
 1. \<And>sa s' v0 v1 v2. \<lbrakk>v1 \<noteq> ZombieTCB \<and> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<or> v1 = ZombieTCB \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; capZombieType cap \<noteq> ZombieTCB\<rbrakk> \<Longrightarrow> (v1 \<noteq> ZombieTCB \<and> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> n = capCNodeBits (capability.Zombie v0 v1 v2) \<or> isZombie (capability.Zombie v0 v1 v2) \<and> n = zombieCTEBits (capZombieType (capability.Zombie v0 v1 v2))) \<and> word_of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - Suc 0) < 2 ^ n) \<longrightarrow> (case gsCNodes sa v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n)) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (v1 \<noteq> ZombieTCB \<longrightarrow> (case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> of_nat (capZombieNumber (capability.Zombie v0 v1 v2) - 1) < (2::?'g38) ^ n))) \<longrightarrow> s' \<in> Q') proof (prove)
goal (1 subgoal):
 1. \<And>sa s' v0 v1 v2. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB\<rbrakk> \<Longrightarrow> ((\<exists>y. gsCNodes sa v0 = Some y) \<and> (\<forall>x2. gsCNodes sa v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<longrightarrow> (\<forall>x2. gsCNodes sa v0 = Some x2 \<longrightarrow> of_nat (v2 - Suc 0) < (2::?'g38) ^ x2)) \<and> ((\<exists>s. (s, s') \<in> rf_sr \<and> (\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> of_nat (v2 - Suc 0) < (2::?'g38) ^ x2) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> of_nat (v2 - Suc 0) < (2::?'g38) ^ x2)) \<longrightarrow> s' \<in> Q') proof (prove)
goal (2 subgoals):
 1. \<And>sa s' v0 v1 v2. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB\<rbrakk> \<Longrightarrow> (\<exists>y. gsCNodes sa v0 = Some y) \<and> (\<forall>x2. gsCNodes sa v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<longrightarrow> (\<forall>x2. gsCNodes sa v0 = Some x2 \<longrightarrow> of_nat (v2 - Suc 0) < (2::?'g38) ^ x2)
 2. \<And>sa s' v0 v1 v2. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB\<rbrakk> \<Longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> of_nat (v2 - Suc 0) < (2::?'g38) ^ x2) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> of_nat (v2 - Suc 0) < (2::?'g38) ^ x2)) \<longrightarrow> s' \<in> Q' proof (prove)
goal (2 subgoals):
 1. \<And>sa s' v0 v1 v2 y. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB; gsCNodes sa v0 = Some y; isCNodeCap (capability.Zombie v0 v1 v2) \<and> y = capCNodeBits (capability.Zombie v0 v1 v2) \<or> y = zombieCTEBits v1; word_of_nat (v2 - Suc 0) < 2 ^ y\<rbrakk> \<Longrightarrow> of_nat (v2 - Suc 0) < (2::?'g38) ^ y
 2. \<And>sa s' v0 v1 v2. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB\<rbrakk> \<Longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> of_nat (v2 - Suc 0) < (2::?'g38) ^ x2) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> of_nat (v2 - Suc 0) < (2::?'g38) ^ x2)) \<longrightarrow> s' \<in> Q' proof (prove)
goal (1 subgoal):
 1. \<And>sa s' v0 v1 v2. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<in> Q'; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB\<rbrakk> \<Longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<and> Q s) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr \<and> (\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> word_of_nat (v2 - Suc 0) < 2 ^ x2)) \<longrightarrow> s' \<in> Q' proof (prove)
goal (1 subgoal):
 1. \<And>sa s' v0 v1 v2 saa y sb ya. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB; (saa, s') \<in> rf_sr; gsCNodes saa v0 = Some y; Q saa; (sb, s') \<in> rf_sr; gsCNodes sb v0 = Some ya; \<not> array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))); y < 32; unat (word_of_nat (v2 - Suc 0)) < 2 ^ y; ya < 32; unat (word_of_nat (v2 - Suc 0)) < 2 ^ ya\<rbrakk> \<Longrightarrow> s' \<in> Q' proof (prove)
goal (1 subgoal):
 1. \<And>sa s' v0 v1 v2 saa y sb ya. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB; (saa, s') \<in> rf_sr; Q saa; (sb, s') \<in> rf_sr; gsCNodes sb v0 = Some ya; \<not> array_assertion (cte_Ptr v0) (v2 - Suc 0) (hrs_htd (t_hrs_' (globals s'))); y < 32; unat (word_of_nat (v2 - Suc 0)) < 2 ^ y; ya < 32; unat (word_of_nat (v2 - Suc 0)) < 2 ^ ya; array_assertion (cte_Ptr v0) (2 ^ y) (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> s' \<in> Q' proof (prove)
goal (1 subgoal):
 1. \<And>sa s' v0 v1 v2 saa y sb ya. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB; (saa, s') \<in> rf_sr; Q saa; (sb, s') \<in> rf_sr; gsCNodes sb v0 = Some ya; y < 32; unat (word_of_nat (v2 - Suc 0)) < 2 ^ y; ya < 32; unat (word_of_nat (v2 - Suc 0)) < 2 ^ ya\<rbrakk> \<Longrightarrow> v2 - Suc 0 \<le> 2 ^ y proof (prove)
goal (1 subgoal):
 1. \<And>sa s' v0 v1 v2 saa y sb ya. \<lbrakk>(\<exists>y. gsCNodes s v0 = Some y) \<and> (\<forall>x2. gsCNodes s v0 = Some x2 \<longrightarrow> (isCNodeCap (capability.Zombie v0 v1 v2) \<and> x2 = capCNodeBits (capability.Zombie v0 v1 v2) \<or> x2 = zombieCTEBits v1) \<and> word_of_nat (v2 - Suc 0) < 2 ^ x2) \<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf Q Q' hs (cutMon ((=) s) (a (v0 + 2 ^ cte_level_bits * word_of_nat (v2 - Suc 0)))) c; (sa, s') \<in> rf_sr; n = word_of_nat (v2 - Suc 0); cap = capability.Zombie v0 v1 v2; Q sa; valid_cap' (capability.Zombie v0 v1 v2) sa; v1 \<noteq> ZombieTCB; (saa, s') \<in> rf_sr; Q saa; (sb, s') \<in> rf_sr; gsCNodes sb v0 = Some ya; y < 32; unat (word_of_nat (v2 - Suc 0)) < 2 ^ y; ya < 32; unat (word_of_nat (v2 - Suc 0)) < 2 ^ ya; v2 < 2 ^ word_bits\<rbrakk> \<Longrightarrow> v2 - Suc 0 \<le> 2 ^ y