theory Schedule_R

lemma bitmapQ_lookupBitmapPriority_simp: (* neater unfold, actual unfold is really ugly *)
  "\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ;
     valid_bitmapQ s ; bitmapQ_no_L1_orphans s \<rbrakk> \<Longrightarrow>
   bitmapQ d (lookupBitmapPriority d s) s =
    (ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d) \<and>
     ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !!
       word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))" unfolding bitmapQ_def lookupBitmapPriority_def apply (drule word_log2_nth_same, clarsimp) apply (drule (1) bitmapQ_no_L1_orphansD, clarsimp) apply (drule word_log2_nth_same, clarsimp) apply (frule test_bit_size[where n="word_log2 (ksReadyQueuesL2Bitmap _ _)"]) apply (clarsimp simp: numPriorities_def wordBits_def word_size) apply (subst prioToL1Index_l1IndexToPrio_or_id) apply (subst unat_of_nat_eq) apply (fastforce intro: unat_less_helper word_log2_max[THEN order_less_le_trans]
                      simp: wordRadix_def word_size l2BitmapSize_def')+ apply (subst prioToL1Index_l1IndexToPrio_or_id) apply (fastforce intro: unat_less_helper word_log2_max of_nat_mono_maybe
                      simp: wordRadix_def word_size l2BitmapSize_def')+ apply (simp add: word_ao_dist) apply (subst less_mask_eq) apply (fastforce intro: word_of_nat_less simp: wordRadix_def' unat_of_nat word_size)+ apply (subst unat_of_nat_eq) apply (fastforce intro: word_log2_max[THEN order_less_le_trans] simp: word_size)+ done

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