theory TcbAcc_R

lemma removeFromBitmap_valid_bitmapQ_except:
  "\<lbrace> valid_bitmapQ_except d p \<rbrace>
   removeFromBitmap d p
   \<lbrace>\<lambda>_. valid_bitmapQ_except d p \<rbrace>" proof - have unat_ucast_mask[simp]:
   "\<And>x. unat ((ucast (p::priority) :: machine_word) && mask x) = unat (p && mask x)" by (simp add: ucast_and_mask[symmetric] unat_ucast_upcast is_up) show ?thesis unfolding removeFromBitmap_def supply bit_not_iff[simp del] bit_not_exp_iff[simp del] apply (simp add: let_into_return[symmetric]) unfolding bitmap_fun_defs when_def apply wp apply clarsimp apply (rule conjI) 
   (* after clearing bit in L2, all bits in L2 field are clear *)
    apply clarsimp apply (subst valid_bitmapQ_except_def, clarsimp)+ apply (clarsimp simp: bitmapQ_def) apply (rule conjI; clarsimp) apply (rename_tac p') apply (rule conjI; clarsimp simp: invertL1Index_eq_cancel) apply (drule_tac p=p' in valid_bitmapQ_exceptE[where d=d], clarsimp) apply (clarsimp simp: bitmapQ_def) apply (drule_tac n'="unat (p' && mask wordRadix)" in no_other_bits_set) apply (erule (1) prioToL1Index_bits_low_high_eq) apply (rule order_less_le_trans[OF word_unat_mask_lt]) apply (simp add: wordRadix_def' word_size)+ apply (rule order_less_le_trans[OF word_unat_mask_lt]) apply ((simp add: wordRadix_def' word_size)+)[3] apply (drule_tac p=p' and d=d in valid_bitmapQ_exceptE, simp) apply (clarsimp simp: bitmapQ_def prioToL1Index_complement_nth_w2p) apply (drule_tac p=pa and d=da in valid_bitmapQ_exceptE, simp) apply (clarsimp simp: bitmapQ_def prioToL1Index_complement_nth_w2p) 
  (* after clearing bit in L2, some bits in L2 field are still set *)
   apply clarsimp apply (subst valid_bitmapQ_except_def, clarsimp)+ apply (clarsimp simp: bitmapQ_def invertL1Index_eq_cancel) apply (rule conjI; clarsimp) apply (frule (1) prioToL1Index_bits_low_high_eq) apply (drule_tac d=d and p=pa in valid_bitmapQ_exceptE, simp) apply (clarsimp simp: bitmapQ_def) apply (subst complement_nth_w2p) apply (rule order_less_le_trans[OF word_unat_mask_lt]) apply ((simp add: wordRadix_def' word_size)+)[3] apply (clarsimp simp: valid_bitmapQ_except_def bitmapQ_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. unat (UCAST(8 \<rightarrow> 32) p && mask x) = unat (p && mask x) proof (state)
this:
unat (UCAST(8 \<rightarrow> 32) p && mask ?x) = unat (p && mask ?x)

goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
modifyReadyQueuesL2Bitmap d l1indexInverted $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- getReadyQueuesL2Bitmap d l1indexInverted;
when (l2 = 0) $ modifyReadyQueuesL1Bitmap d $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
modifyReadyQueuesL2Bitmap d l1indexInverted $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- getReadyQueuesL2Bitmap d l1indexInverted;
when (l2 = 0) $ modifyReadyQueuesL1Bitmap d $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p\<rbrace> do y <- modifyReadyQueuesL2Bitmap d (invertL1Index (prioToL1Index p)) (\<lambda>w. w && ~~ 2 ^ unat (p && mask wordRadix));
l2 <- getReadyQueuesL2Bitmap d (invertL1Index (prioToL1Index p));
when (l2 = 0) (modifyReadyQueuesL1Bitmap d (\<lambda>w. w && ~~ 2 ^ prioToL1Index p))
od \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ_except d p\<rbrace> do y <- do l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, invertL1Index (prioToL1Index p)));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, invertL1Index (prioToL1Index p)), l2 && ~~ 2 ^ unat (p && mask wordRadix))]\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, invertL1Index (prioToL1Index p)));
if l2 = 0 then do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, l1 && ~~ 2 ^ prioToL1Index p)]\<rparr>)
od else return ()
od \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> (ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap s aLU [((d, invertL1Index (prioToL1Index p)), ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))]\<rparr>) (d, invertL1Index (prioToL1Index p)) = 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap s aLU [((d, invertL1Index (prioToL1Index p)), ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))], ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap (s\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap s aLU [((d, invertL1Index (prioToL1Index p)), ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))]\<rparr>) aLU [(d, ksReadyQueuesL1Bitmap (s\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap s aLU [((d, invertL1Index (prioToL1Index p)), ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))]\<rparr>) d && ~~ 2 ^ prioToL1Index p)]\<rparr>)) \<and> (ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap s aLU [((d, invertL1Index (prioToL1Index p)), ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))]\<rparr>) (d, invertL1Index (prioToL1Index p)) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap s aLU [((d, invertL1Index (prioToL1Index p)), ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))]\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then 0 else ksReadyQueuesL2Bitmap s a, ksReadyQueuesL1Bitmap := \<lambda>a. if a = d then ksReadyQueuesL1Bitmap s d && ~~ 2 ^ prioToL1Index p else ksReadyQueuesL1Bitmap s a\<rparr>)) \<and> (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then 0 else ksReadyQueuesL2Bitmap s a, ksReadyQueuesL1Bitmap := \<lambda>a. if a = d then ksReadyQueuesL1Bitmap s d && ~~ 2 ^ prioToL1Index p else ksReadyQueuesL1Bitmap s a\<rparr>)
 2. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then 0 else ksReadyQueuesL2Bitmap s a, ksReadyQueuesL1Bitmap := \<lambda>a. if a = d then ksReadyQueuesL1Bitmap s d && ~~ 2 ^ prioToL1Index p else ksReadyQueuesL1Bitmap s a\<rparr>)
 2. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0\<rbrakk> \<Longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then 0 else ksReadyQueuesL2Bitmap s a, ksReadyQueuesL1Bitmap := \<lambda>a. if a = d then ksReadyQueuesL1Bitmap s d && ~~ 2 ^ prioToL1Index p else ksReadyQueuesL1Bitmap s a\<rparr>)
 2. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da = d \<longrightarrow> pa \<noteq> p\<rbrakk> \<Longrightarrow> bitmapQ da pa (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then 0 else ksReadyQueuesL2Bitmap s a, ksReadyQueuesL1Bitmap := \<lambda>a. if a = d then ksReadyQueuesL1Bitmap s d && ~~ 2 ^ prioToL1Index p else ksReadyQueuesL1Bitmap s a\<rparr>) = (ksReadyQueues s (da, pa) \<noteq> [])
 2. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da = d \<longrightarrow> pa \<noteq> p\<rbrakk> \<Longrightarrow> (da = d \<longrightarrow> (invertL1Index (prioToL1Index pa) = invertL1Index (prioToL1Index p) \<longrightarrow> ksReadyQueues s (d, pa) = []) \<and> (invertL1Index (prioToL1Index pa) \<noteq> invertL1Index (prioToL1Index p) \<longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index pa \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> []))) \<and> (da \<noteq> d \<longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> []))
 2. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; pa \<noteq> p\<rbrakk> \<Longrightarrow> (invertL1Index (prioToL1Index pa) = invertL1Index (prioToL1Index p) \<longrightarrow> ksReadyQueues s (d, pa) = []) \<and> (invertL1Index (prioToL1Index pa) \<noteq> invertL1Index (prioToL1Index p) \<longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index pa \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> []))
 2. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 3. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p\<rbrakk> \<Longrightarrow> (invertL1Index (prioToL1Index p') = invertL1Index (prioToL1Index p) \<longrightarrow> ksReadyQueues s (d, p') = []) \<and> (invertL1Index (prioToL1Index p') \<noteq> invertL1Index (prioToL1Index p) \<longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> []))
 2. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 3. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' = prioToL1Index p\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p') = []
 2. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 3. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 4. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s p'. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' = prioToL1Index p; bitmapQ d p' s = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p') = []
 2. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 3. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 4. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s p'. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p') = []
 2. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 3. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 4. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (7 subgoals):
 1. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> unat (p' && mask wordRadix) \<noteq> unat (p && mask wordRadix)
 2. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> unat (p && mask wordRadix) < size (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)))
 3. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> unat (p' && mask wordRadix) < size (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)))
 4. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> []); \<not> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p') = []
 5. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 6. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 7. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> unat (p && mask wordRadix) < size (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)))
 2. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> unat (p' && mask wordRadix) < size (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)))
 3. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> []); \<not> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p') = []
 4. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 5. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 6. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (7 subgoals):
 1. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> wordRadix \<le> size p
 2. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> 2 ^ wordRadix \<le> size (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)))
 3. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> unat (p' && mask wordRadix) < size (ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)))
 4. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> []); \<not> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p') = []
 5. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 6. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 7. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask 5)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> unat (p' && mask 5) < 32
 2. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> []); \<not> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p') = []
 3. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 4. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 5. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask 5)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> 5 \<le> size p'
 2. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask 5)) = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> 2 ^ 5 \<le> 32
 3. \<And>s p'. \<lbrakk>p' \<noteq> p; prioToL1Index p' = prioToL1Index p; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> []); \<not> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p') = []
 4. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 5. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 6. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s p'. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 2. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 3. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s p'. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; p' \<noteq> p; prioToL1Index p' \<noteq> prioToL1Index p; bitmapQ d p' s = (ksReadyQueues s (d, p') \<noteq> [])\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p' \<and> (~~ 2 ^ prioToL1Index p) !! prioToL1Index p' \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)) = (ksReadyQueues s (d, p') \<noteq> [])
 2. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 3. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 2. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s da pa. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) = 0; da \<noteq> d; bitmapQ da pa s = (ksReadyQueues s (da, pa) \<noteq> [])\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])
 2. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_bitmapQ_except d p s \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0 \<longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0\<rbrakk> \<Longrightarrow> valid_bitmapQ_except d p (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; da = d \<longrightarrow> pa \<noteq> p\<rbrakk> \<Longrightarrow> bitmapQ da pa (s\<lparr>ksReadyQueuesL2Bitmap := \<lambda>a. if a = (d, invertL1Index (prioToL1Index p)) then ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) else ksReadyQueuesL2Bitmap s a\<rparr>) = (ksReadyQueues s (da, pa) \<noteq> []) proof (prove)
goal (1 subgoal):
 1. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; da = d \<longrightarrow> pa \<noteq> p\<rbrakk> \<Longrightarrow> (da = d \<and> prioToL1Index pa = prioToL1Index p \<longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix) \<and> (~~ 2 ^ unat (p && mask wordRadix)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])) \<and> ((da = d \<longrightarrow> prioToL1Index pa \<noteq> prioToL1Index p) \<longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> [])) proof (prove)
goal (2 subgoals):
 1. \<And>s pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; pa \<noteq> p; prioToL1Index pa = prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix) \<and> (~~ 2 ^ unat (p && mask wordRadix)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])
 2. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; da = d \<longrightarrow> pa \<noteq> p; da = d \<longrightarrow> prioToL1Index pa \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> []) proof (prove)
goal (2 subgoals):
 1. \<And>s pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; pa \<noteq> p; prioToL1Index pa = prioToL1Index p; unat (pa && mask wordRadix) \<noteq> unat (p && mask wordRadix)\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix) \<and> (~~ 2 ^ unat (p && mask wordRadix)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])
 2. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; da = d \<longrightarrow> pa \<noteq> p; da = d \<longrightarrow> prioToL1Index pa \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> []) proof (prove)
goal (2 subgoals):
 1. \<And>s pa. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; pa \<noteq> p; prioToL1Index pa = prioToL1Index p; unat (pa && mask wordRadix) \<noteq> unat (p && mask wordRadix); bitmapQ d pa s = (ksReadyQueues s (d, pa) \<noteq> [])\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix) \<and> (~~ 2 ^ unat (p && mask wordRadix)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])
 2. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; da = d \<longrightarrow> pa \<noteq> p; da = d \<longrightarrow> prioToL1Index pa \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> []) proof (prove)
goal (2 subgoals):
 1. \<And>s pa. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; pa \<noteq> p; prioToL1Index pa = prioToL1Index p; pa && mask wordRadix \<noteq> p && mask wordRadix; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix) \<and> (~~ 2 ^ unat (p && mask wordRadix)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])
 2. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; da = d \<longrightarrow> pa \<noteq> p; da = d \<longrightarrow> prioToL1Index pa \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> []) proof (prove)
goal (3 subgoals):
 1. \<And>s pa. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; pa \<noteq> p; prioToL1Index pa = prioToL1Index p; pa && mask wordRadix \<noteq> p && mask wordRadix; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])\<rbrakk> \<Longrightarrow> unat (pa && mask wordRadix) < LENGTH(32)
 2. \<And>s pa. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; pa \<noteq> p; prioToL1Index pa = prioToL1Index p; pa && mask wordRadix \<noteq> p && mask wordRadix; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix) \<and> unat (pa && mask wordRadix) \<noteq> unat (p && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])
 3. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; da = d \<longrightarrow> pa \<noteq> p; da = d \<longrightarrow> prioToL1Index pa \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> []) proof (prove)
goal (4 subgoals):
 1. \<And>s pa. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; pa \<noteq> p; prioToL1Index pa = prioToL1Index p; pa && mask wordRadix \<noteq> p && mask wordRadix; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])\<rbrakk> \<Longrightarrow> wordRadix \<le> size pa
 2. \<And>s pa. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; pa \<noteq> p; prioToL1Index pa = prioToL1Index p; pa && mask wordRadix \<noteq> p && mask wordRadix; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])\<rbrakk> \<Longrightarrow> 2 ^ wordRadix \<le> LENGTH(32)
 3. \<And>s pa. \<lbrakk>ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; pa \<noteq> p; prioToL1Index pa = prioToL1Index p; pa && mask wordRadix \<noteq> p && mask wordRadix; (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (pa && mask wordRadix) \<and> unat (pa && mask wordRadix) \<noteq> unat (p && mask wordRadix)) = (ksReadyQueues s (d, pa) \<noteq> [])
 4. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; da = d \<longrightarrow> pa \<noteq> p; da = d \<longrightarrow> prioToL1Index pa \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> []) proof (prove)
goal (1 subgoal):
 1. \<And>s da pa. \<lbrakk>valid_bitmapQ_except d p s; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix) \<noteq> 0; da = d \<longrightarrow> pa \<noteq> p; da = d \<longrightarrow> prioToL1Index pa \<noteq> prioToL1Index p\<rbrakk> \<Longrightarrow> (ksReadyQueuesL1Bitmap s da !! prioToL1Index pa \<and> ksReadyQueuesL2Bitmap s (da, invertL1Index (prioToL1Index pa)) !! unat (pa && mask wordRadix)) = (ksReadyQueues s (da, pa) \<noteq> []) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>valid_bitmapQ_except d p\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. valid_bitmapQ_except d p\<rbrace>

goal:
No subgoals!