theory Schedule_R

lemma bitmapL1_highest_lookup:
  "\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ;
     bitmapQ d p' s \<rbrakk>
   \<Longrightarrow> p' \<le> lookupBitmapPriority d s" apply (subgoal_tac "ksReadyQueuesL1Bitmap s d \<noteq> 0") prefer 2 apply (clarsimp simp add: bitmapQ_def) apply (case_tac "prioToL1Index (lookupBitmapPriority d s) = prioToL1Index p'") apply (rule prioToL1Index_le_mask, simp) apply (frule (2) bitmapQ_from_bitmap_lookup) apply (clarsimp simp: bitmapQ_lookupBitmapPriority_simp) apply (clarsimp simp: bitmapQ_def lookupBitmapPriority_def) apply (subst mask_or_not_mask[where n=wordRadix and x=p', symmetric]) apply (subst word_bw_comms(2))  (* || commute *)
    apply (simp add: word_ao_dist mask_AND_NOT_mask mask_twice) apply (subst less_mask_eq[where x="of_nat _"]) apply (subst word_less_nat_alt) apply (subst unat_of_nat_eq) apply (rule order_less_le_trans[OF word_log2_max]) apply (simp add: word_size) apply (rule order_less_le_trans[OF word_log2_max]) apply (simp add: word_size wordRadix_def') apply (subst word_le_nat_alt) apply (subst unat_of_nat_eq) apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size) apply (rule word_log2_highest) apply (subst (asm) prioToL1Index_l1IndexToPrio_or_id) apply (subst unat_of_nat_eq) apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size) apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size wordRadix_def') apply (simp add: word_size) apply (drule (1) bitmapQ_no_L1_orphansD[where d=d and i="word_log2 _"]) apply (simp add: numPriorities_def wordBits_def word_size l2BitmapSize_def') apply simp apply (rule prioToL1Index_le_index[rotated], simp) apply (frule (2) bitmapQ_from_bitmap_lookup) apply (clarsimp simp: bitmapQ_lookupBitmapPriority_simp) apply (clarsimp simp: bitmapQ_def lookupBitmapPriority_def) apply (subst prioToL1Index_l1IndexToPrio_or_id) apply (subst unat_of_nat_eq) apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size) apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size wordRadix_def') apply (fastforce dest: bitmapQ_no_L1_orphansD
                    simp: wordBits_def numPriorities_def word_size l2BitmapSize_def') apply (erule word_log2_highest) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap s d \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap s d \<noteq> 0
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) = prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) = prioToL1Index p'\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> lookupBitmapPriority d s && mask wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) = prioToL1Index p'; bitmapQ d (lookupBitmapPriority d s) s\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> lookupBitmapPriority d s && mask wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> lookupBitmapPriority d s && mask wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) && mask wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> (p' && mask wordRadix || p' && ~~ mask wordRadix) && mask wordRadix \<le> (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) && mask wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> (p' && ~~ mask wordRadix || p' && mask wordRadix) && mask wordRadix \<le> (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) && mask wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> (p' && ~~ mask wordRadix || p' && mask wordRadix) && mask wordRadix \<le> (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) && mask wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))) && mask wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))) < 2 ^ wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> unat (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) < unat (2 ^ wordRadix)
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < 2 ^ LENGTH(8)
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < unat (2 ^ wordRadix)
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))
 4. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> size (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) \<le> 2 ^ LENGTH(8)
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < unat (2 ^ wordRadix)
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))
 4. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < unat (2 ^ wordRadix)
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> size (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) \<le> unat (2 ^ wordRadix)
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> p' && mask wordRadix \<le> word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> unat (p' && mask wordRadix) \<le> unat (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < 2 ^ LENGTH(8)
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> unat (p' && mask wordRadix) \<le> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> unat (p' && mask wordRadix) \<le> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! unat (p' && mask wordRadix)
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> unat (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) < 2 ^ wordRadix
 2. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < size (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; word_log2 (ksReadyQueuesL1Bitmap s d) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! unat (p' && mask wordRadix)
 4. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < 2 ^ LENGTH(8)
 2. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < 2 ^ wordRadix
 3. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < size (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))
 4. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; word_log2 (ksReadyQueuesL1Bitmap s d) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! unat (p' && mask wordRadix)
 5. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < 2 ^ wordRadix
 2. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < size (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; word_log2 (ksReadyQueuesL1Bitmap s d) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! unat (p' && mask wordRadix)
 4. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < size (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; word_log2 (ksReadyQueuesL1Bitmap s d) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! unat (p' && mask wordRadix)
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < 8
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; word_log2 (ksReadyQueuesL1Bitmap s d) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! unat (p' && mask wordRadix)
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix); valid_bitmapQ s; ksReadyQueuesL1Bitmap s d \<noteq> 0; ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0 \<and> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < 8
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; word_log2 (ksReadyQueuesL1Bitmap s d) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! unat (p' && mask wordRadix)
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; word_log2 (ksReadyQueuesL1Bitmap s d) = prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! unat (p' && mask wordRadix)
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> p' \<le> lookupBitmapPriority d s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'\<rbrakk> \<Longrightarrow> prioToL1Index p' \<le> prioToL1Index (lookupBitmapPriority d s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'; bitmapQ d (lookupBitmapPriority d s) s\<rbrakk> \<Longrightarrow> prioToL1Index p' \<le> prioToL1Index (lookupBitmapPriority d s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; bitmapQ d p' s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (lookupBitmapPriority d s) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))\<rbrakk> \<Longrightarrow> prioToL1Index p' \<le> prioToL1Index (lookupBitmapPriority d s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> prioToL1Index p' \<le> prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> unat (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) < 2 ^ wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < size (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> prioToL1Index p' \<le> word_log2 (ksReadyQueuesL1Bitmap s d) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < 2 ^ LENGTH(8)
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < 2 ^ wordRadix
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < size (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))
 4. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> prioToL1Index p' \<le> word_log2 (ksReadyQueuesL1Bitmap s d) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))) < 2 ^ wordRadix
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < size (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))
 3. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> prioToL1Index p' \<le> word_log2 (ksReadyQueuesL1Bitmap s d) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < size (word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))
 2. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> prioToL1Index p' \<le> word_log2 (ksReadyQueuesL1Bitmap s d) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L1_orphans s; ksReadyQueuesL1Bitmap s d \<noteq> 0; prioToL1Index (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<noteq> prioToL1Index p'; ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d); ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))); ksReadyQueuesL1Bitmap s d !! prioToL1Index p'; ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p')) !! unat (p' && mask wordRadix)\<rbrakk> \<Longrightarrow> prioToL1Index p' \<le> word_log2 (ksReadyQueuesL1Bitmap s d) proof (prove)
goal:
No subgoals!