theory Schedule_R

lemma isHighestPrio_corres:
  assumes "d' = d"
  assumes "p' = p"
  shows
    "corres ((=)) \<top> valid_queues
      (gets (is_highest_prio d p))
      (isHighestPrio d' p')" using assms apply (clarsimp simp: gets_is_highest_prio_expand isHighestPrio_def) apply (subst getHighestPrio_def') apply (rule corres_guard_imp) apply (rule corres_split[OF corres_gets_queues_getReadyQueuesL1Bitmap]) apply (rule corres_if_r'[where P'="\<lambda>_. True",rotated]) apply (rule_tac corres_symb_exec_r) apply (rule_tac
                       P="\<lambda>s. q = ready_queues s d
                              " and
                       P'="\<lambda>s. valid_queues s \<and>
                               l1 = ksReadyQueuesL1Bitmap s d \<and>
                               l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s" and
                       F="hprio = Max {prio. q prio \<noteq> []}" in corres_req) apply (elim conjE) apply (clarsimp simp: valid_queues_def) apply (subst lookupBitmapPriority_Max_eqI; blast?) apply (fastforce simp: ready_queues_relation_def dest!: state_relationD) apply fastforce apply (wpsimp simp: if_apply_def2 wp: hoare_drop_imps ksReadyQueuesL1Bitmap_return_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) Invariants_H.valid_queues (gets (is_highest_prio d p)) (isHighestPrio d' p') proof (prove)
using this:
d' = d
p' = p

goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) Invariants_H.valid_queues (gets (is_highest_prio d p)) (isHighestPrio d' p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>_. True) Invariants_H.valid_queues (do q <- gets (\<lambda>s. ready_queues s d);
return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)
od) (do l1 <- getReadyQueuesL1Bitmap d;
if l1 = 0 then return True else do hprio <- getHighestPrio d;
return (hprio \<le> p)
od
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>_. True) Invariants_H.valid_queues (do q <- gets (\<lambda>s. ready_queues s d);
return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)
od) (do l1 <- getReadyQueuesL1Bitmap d;
if l1 = 0 then return True else do hprio <- gets (lookupBitmapPriority d);
return (hprio \<le> p)
od
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> corres (=) ?Q2 ?Q'2 (do q <- gets (\<lambda>s. ready_queues s d);
return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)
od) (do l1 <- getReadyQueuesL1Bitmap d;
if l1 = 0 then return True else do hprio <- gets (lookupBitmapPriority d);
return (hprio \<le> p)
od
od)
 2. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (5 subgoals):
 1. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = [])\<rbrakk> \<Longrightarrow> corres (=) (?R6 q) (?R'6 l1) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (if l1 = 0 then return True else do hprio <- gets (lookupBitmapPriority d);
return (hprio \<le> p)
od)
 2. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>?R6\<rbrace>
 3. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>?R'6\<rbrace>
 4. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0\<rbrakk> \<Longrightarrow> corres (=) (?R6 q) (?Q'13 l1) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (do hprio <- gets (lookupBitmapPriority d);
return (hprio \<le> p)
od)
 2. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 = 0\<rbrakk> \<Longrightarrow> corres (=) (?R6 q) (\<lambda>_. True) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return True)
 3. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>?R6\<rbrace>
 4. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then \<lambda>_. True else ?Q'13 l1\<rbrace>
 5. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>q l1 hprio. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0\<rbrakk> \<Longrightarrow> corres (=) (?R6 q) (?Q'16 q l1 hprio) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return (hprio \<le> p))
 2. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 l1\<rbrace> gets (lookupBitmapPriority d) \<lbrace>?Q'16 q l1\<rbrace>
 3. \<And>q l1 s. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; ?Q'13 l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'13 l1) (gets (lookupBitmapPriority d))
 5. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 = 0\<rbrakk> \<Longrightarrow> corres (=) (?R6 q) (\<lambda>_. True) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return True)
 6. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>?R6\<rbrace>
 7. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then \<lambda>_. True else ?Q'13 l1\<rbrace>
 8. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>q l1 hprio s s'. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; (s, s') \<in> state_relation; q = ready_queues s d; Invariants_H.valid_queues s' \<and> l1 = ksReadyQueuesL1Bitmap s' d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s'\<rbrakk> \<Longrightarrow> hprio = Max {prio. q prio \<noteq> []}
 2. \<And>q l1 hprio. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; hprio = Max {prio. q prio \<noteq> []}\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return (hprio \<le> p))
 3. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 l1\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>hprio s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s\<rbrace>
 4. \<And>q l1 s. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; ?Q'13 l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'13 l1) (gets (lookupBitmapPriority d))
 6. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 = 0\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>_. True) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return True)
 7. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>q s. q = ready_queues s d\<rbrace>
 8. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then \<lambda>_. True else ?Q'13 l1\<rbrace>
 9. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>q l1 hprio s s'. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; (s, s') \<in> state_relation; q = ready_queues s d; Invariants_H.valid_queues s'; l1 = ksReadyQueuesL1Bitmap s' d; l1 \<noteq> 0; hprio = lookupBitmapPriority d s'\<rbrakk> \<Longrightarrow> hprio = Max {prio. q prio \<noteq> []}
 2. \<And>q l1 hprio. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; hprio = Max {prio. q prio \<noteq> []}\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return (hprio \<le> p))
 3. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 l1\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>hprio s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s\<rbrace>
 4. \<And>q l1 s. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; ?Q'13 l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'13 l1) (gets (lookupBitmapPriority d))
 6. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 = 0\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>_. True) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return True)
 7. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>q s. q = ready_queues s d\<rbrace>
 8. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then \<lambda>_. True else ?Q'13 l1\<rbrace>
 9. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>s s' pa. \<lbrakk>d' = d; p' = p; (ksReadyQueuesL1Bitmap s' d = 0) = (\<forall>p. ready_queues s d p = []); (s, s') \<in> state_relation; ready_queues s d pa \<noteq> []; valid_queues_no_bitmap s'; valid_bitmapQ s'; bitmapQ_no_L2_orphans s'; bitmapQ_no_L1_orphans s'\<rbrakk> \<Longrightarrow> lookupBitmapPriority d s' = Max {prio. ready_queues s d prio \<noteq> []}
 2. \<And>q l1 hprio. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; hprio = Max {prio. q prio \<noteq> []}\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return (hprio \<le> p))
 3. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 l1\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>hprio s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s\<rbrace>
 4. \<And>q l1 s. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; ?Q'13 l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'13 l1) (gets (lookupBitmapPriority d))
 6. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 = 0\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>_. True) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return True)
 7. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>q s. q = ready_queues s d\<rbrace>
 8. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then \<lambda>_. True else ?Q'13 l1\<rbrace>
 9. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>s s' pa. \<lbrakk>d' = d; p' = p; (ksReadyQueuesL1Bitmap s' d = 0) = (\<forall>p. ready_queues s d p = []); (s, s') \<in> state_relation; ready_queues s d pa \<noteq> []; valid_queues_no_bitmap s'; valid_bitmapQ s'; bitmapQ_no_L2_orphans s'; bitmapQ_no_L1_orphans s'\<rbrakk> \<Longrightarrow> Max {prio. ksReadyQueues s' (d, prio) \<noteq> []} = Max {prio. ready_queues s d prio \<noteq> []}
 2. \<And>q l1 hprio. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; hprio = Max {prio. q prio \<noteq> []}\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return (hprio \<le> p))
 3. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 l1\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>hprio s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s\<rbrace>
 4. \<And>q l1 s. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; ?Q'13 l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'13 l1) (gets (lookupBitmapPriority d))
 6. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 = 0\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>_. True) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return True)
 7. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>q s. q = ready_queues s d\<rbrace>
 8. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then \<lambda>_. True else ?Q'13 l1\<rbrace>
 9. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>q l1 hprio. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; hprio = Max {prio. q prio \<noteq> []}\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return (hprio \<le> p))
 2. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 l1\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>hprio s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s\<rbrace>
 3. \<And>q l1 s. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; ?Q'13 l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'13 l1) (gets (lookupBitmapPriority d))
 5. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 = 0\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>_. True) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return True)
 6. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>q s. q = ready_queues s d\<rbrace>
 7. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then \<lambda>_. True else ?Q'13 l1\<rbrace>
 8. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 l1\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>hprio s. Invariants_H.valid_queues s \<and> l1 = ksReadyQueuesL1Bitmap s d \<and> l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s\<rbrace>
 2. \<And>q l1 s. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; ?Q'13 l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets (lookupBitmapPriority d) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'13 l1) (gets (lookupBitmapPriority d))
 4. \<And>q l1. \<lbrakk>d' = d; p' = p; (l1 = 0) = (\<forall>p. q p = []); l1 = 0\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. q = ready_queues s d) (\<lambda>_. True) (return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p)) (return True)
 5. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>q s. q = ready_queues s d\<rbrace>
 6. \<lbrakk>d' = d; p' = p\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then \<lambda>_. True else ?Q'13 l1\<rbrace>
 7. \<And>s. \<lbrakk>d' = d; p' = p; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. \<lbrakk>d' = d; p' = p; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and ?Q'6) s proof (prove)
goal:
No subgoals!