theory Finalise_DR

lemma finalise_preemption_corres:
  "dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) \<top> \<top>
      (monadic_trancl_preemptible finalise_slot_inner2 S) (preemption_point)" apply (simp add: finalise_slot_inner2_def preemption_point_def split_def) apply (subst OR_choiceE_det) apply (simp add: work_units_limit_reached_def) apply ((simp add: work_units_limit_reached_def | wp)+)[1] apply (rule corres_guard_imp) apply (rule dcorres_symb_exec_rE) apply (rule dcorres_symb_exec_rE) apply simp apply (rule conjI, clarsimp) apply (rule dcorres_symb_exec_rE) apply (rule dcorres_symb_exec_rE) apply (simp split: option.splits) apply (rule conjI, clarsimp) apply (rule monadic_rewrite_corres_l) apply (rule monadic_trancl_preemptible_return) apply (rule dcorres_returnOk, simp) apply clarsimp apply (rule corres_guard_imp) apply (rule monadic_rewrite_corres_l) apply (rule monadic_trancl_preemptible_f) apply (rule corres_alternate2[OF dcorres_throw], simp_all)[4] apply ((wp | simp)+)[1] apply (rule hoare_TrueI) apply ((simp add: reset_work_units_def | wp)+)[1] apply clarsimp apply (rule corres_guard_imp) apply (rule monadic_rewrite_corres_l) apply (rule monadic_trancl_preemptible_return) apply (rule dcorres_returnOk, simp_all)[3] apply (rule hoare_TrueI) apply ((simp add: work_units_limit_reached_def | wp)+)[1] apply (rule hoare_TrueI) apply (simp add: update_work_units_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (\<lambda>_. True) (\<lambda>_. True) (monadic_trancl_preemptible finalise_slot_inner2 S) Exceptions_A.preemption_point proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (\<lambda>_. True) (\<lambda>_. True) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (doE y <- liftE update_work_units;
OR_choiceE work_units_limit_reached (doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE) (returnOk ())
odE) proof (prove)
goal (3 subgoals):
 1. \<And>y. det work_units_limit_reached
 2. \<And>y P. \<lbrace>P\<rbrace> work_units_limit_reached \<lbrace>\<lambda>rv. P\<rbrace>
 3. dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (\<lambda>_. True) (\<lambda>_. True) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (doE y <- liftE update_work_units;
rv <- liftE work_units_limit_reached;
if rv then doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE else returnOk ()
odE) proof (prove)
goal (2 subgoals):
 1. \<And>y P. \<lbrace>P\<rbrace> work_units_limit_reached \<lbrace>\<lambda>rv. P\<rbrace>
 2. dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (\<lambda>_. True) (\<lambda>_. True) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (doE y <- liftE update_work_units;
rv <- liftE work_units_limit_reached;
if rv then doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE else returnOk ()
odE) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (\<lambda>_. True) (\<lambda>_. True) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (doE y <- liftE update_work_units;
rv <- liftE work_units_limit_reached;
if rv then doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE else returnOk ()
odE) proof (prove)
goal (3 subgoals):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 ?Q'7 (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (doE y <- liftE update_work_units;
rv <- liftE work_units_limit_reached;
if rv then doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE else returnOk ()
odE)
 2. \<And>s. True \<Longrightarrow> ?Q7 s
 3. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (5 subgoals):
 1. \<And>rv. dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'11 rv) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (doE rv <- liftE work_units_limit_reached;
if rv then doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE else returnOk ()
odE)
 2. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q7 s
 5. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (7 subgoals):
 1. \<And>rv rva. dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'15 rv rva) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (if rva then doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE else returnOk ())
 2. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s. True \<Longrightarrow> ?Q7 s
 7. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (7 subgoals):
 1. \<And>rva. (rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'15 () True) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (doE y <- liftE reset_work_units;
a <- liftE (do_machine_op (getActiveIRQ True));
case a of None \<Rightarrow> returnOk () | Some y \<Rightarrow> throwError ()
odE)) \<and> (\<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ()))
 2. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s. True \<Longrightarrow> ?Q7 s
 7. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (8 subgoals):
 1. \<And>rva. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'15 () True) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (doE y <- liftE reset_work_units;
a <- liftE (do_machine_op (getActiveIRQ True));
case a of None \<Rightarrow> returnOk () | Some y \<Rightarrow> throwError ()
odE)
 2. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 3. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 4. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>s. True \<Longrightarrow> ?Q7 s
 8. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (10 subgoals):
 1. \<And>rva rv. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'29 rva rv) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (doE a <- liftE (do_machine_op (getActiveIRQ True));
case a of None \<Rightarrow> returnOk () | Some y \<Rightarrow> throwError ()
odE)
 2. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 3. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 5. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 6. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>s. True \<Longrightarrow> ?Q7 s
 10. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (12 subgoals):
 1. \<And>rva rv rvb. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'35 rva rv rvb) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (case rvb of None \<Rightarrow> returnOk () | Some y \<Rightarrow> throwError ())
 2. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?Q'35 rva rv\<rbrace>
 3. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 5. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 7. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 8. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rva rvb. rva \<Longrightarrow> (rvb = None \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'35 True () None) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())) \<and> (\<forall>x2. rvb = Some x2 \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'35 True () (Some x2)) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (throwError ()))
 2. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?Q'35 rva rv\<rbrace>
 3. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 5. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 7. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 8. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rva. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'35 True () None) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 2. \<And>rva rvb. rva \<Longrightarrow> \<forall>x2. rvb = Some x2 \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'35 True () (Some x2)) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (throwError ())
 3. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?Q'35 rva rv\<rbrace>
 4. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 6. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?Q7 (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 8. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 9. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rva. rva \<Longrightarrow> monadic_rewrite False (?E50 rva) ?Q55 (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (?a'50 rva)
 2. \<And>rva. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?P57 (?Q'35 True () None) (?a'50 rva) (returnOk ())
 3. \<And>rva rvb. rva \<Longrightarrow> \<forall>x2. rvb = Some x2 \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?P57 and ?Q55) (?Q'35 True () (Some x2)) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (throwError ())
 4. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?Q'35 rva rv\<rbrace>
 5. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 7. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?P57 and ?Q55) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 9. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 10. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rva. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ?P57 (?Q'35 True () None) (returnOk S) (returnOk ())
 2. \<And>rva rvb. rva \<Longrightarrow> \<forall>x2. rvb = Some x2 \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?P57 and (\<lambda>a. True)) (?Q'35 True () (Some x2)) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (throwError ())
 3. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?Q'35 rva rv\<rbrace>
 4. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 6. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?P57 and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 8. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 9. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rva rvb. rva \<Longrightarrow> \<forall>x2. rvb = Some x2 \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (\<lambda>a. True) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (throwError ())
 2. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>a b. rva\<rbrace>
 3. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 5. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 7. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 8. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rva. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (\<lambda>a. True) (\<lambda>a. True) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (throwError ())
 2. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>a b. rva\<rbrace>
 3. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 5. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 7. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 8. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 12 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rva. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?Q68 rva) (?Q'68 rva) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (throwError ())
 2. \<And>rva s. \<lbrakk>rva; True\<rbrakk> \<Longrightarrow> ?Q68 rva s
 3. \<And>rva s. \<lbrakk>rva; True\<rbrakk> \<Longrightarrow> ?Q'68 rva s
 4. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>a b. rva\<rbrace>
 5. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 7. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 9. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 10. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 14 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rva. rva \<Longrightarrow> monadic_rewrite False (?E72 rva) (?Q72 rva) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (?a'72 rva)
 2. \<And>rva. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?P72 rva) (?Q'68 rva) (?a'72 rva) (throwError ())
 3. \<And>rva s. \<lbrakk>rva; True\<rbrakk> \<Longrightarrow> (?P72 rva and ?Q72 rva) s
 4. \<And>rva s. \<lbrakk>rva; True\<rbrakk> \<Longrightarrow> ?Q'68 rva s
 5. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>a b. rva\<rbrace>
 6. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 8. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 10. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rva. rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?P72 rva) (?Q'68 rva) (liftE (do p <- select (fst S);
pa <- finalise_slot_inner1 (fst p);
region' <- gets (get_zombie_range (fst pa));
return (fst S \<union> region' \<times> {True}, if snd pa then {(fst p, snd p)} else {})
od) \<sqinter> liftE (do p <- select {p. (fst p, True) \<in> fst S \<and> (snd p, True) \<in> fst S \<and> fst p \<noteq> snd p};
y <- swap_for_delete (fst p) (snd p);
return (fst S, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd S};
y <- PageTableUnmap_D.empty_slot victim';
return (fst S, {})
od) \<sqinter> throw) (throwError ())
 2. \<And>rva s. \<lbrakk>rva; True\<rbrakk> \<Longrightarrow> (?P72 rva and (\<lambda>_. True)) s
 3. \<And>rva s. \<lbrakk>rva; True\<rbrakk> \<Longrightarrow> ?Q'68 rva s
 4. \<And>rva rv. rva \<Longrightarrow> \<lbrace>?Q'29 rva rv\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>a b. rva\<rbrace>
 5. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 7. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 9. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 10. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 14 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rva rv cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 3. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 5. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 6. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 10. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (9 subgoals):
 1. \<And>rva. rva \<Longrightarrow> \<lbrace>?Q'15 () True\<rbrace> reset_work_units \<lbrace>?Q'29 rva\<rbrace>
 2. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 4. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 9. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (8 subgoals):
 1. \<And>rva cs. rva \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reset_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 3. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 4. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 8. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (7 subgoals):
 1. \<And>rva. \<not> rva \<longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) ((\<lambda>a. True) and (\<lambda>a. True)) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 2. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 7. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (7 subgoals):
 1. \<And>rva. \<not> rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (\<lambda>a. True) (?Q'15 () False) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 2. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 7. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (9 subgoals):
 1. \<And>rva. \<not> rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?Q93 rva) (?Q'93 rva) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (returnOk ())
 2. \<And>rva s. \<lbrakk>\<not> rva; True\<rbrakk> \<Longrightarrow> ?Q93 rva s
 3. \<And>rva s. \<lbrakk>\<not> rva; ?Q'15 () False s\<rbrakk> \<Longrightarrow> ?Q'93 rva s
 4. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 9. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (10 subgoals):
 1. \<And>rva. \<not> rva \<Longrightarrow> monadic_rewrite False (?E98 rva) (?Q98 rva) (monadic_trancl_preemptible (\<lambda>p. liftE (do pa <- select (fst p);
pb <- finalise_slot_inner1 (fst pa);
region' <- gets (get_zombie_range (fst pb));
return (fst p \<union> region' \<times> {True}, if snd pb then {(fst pa, snd pa)} else {})
od) \<sqinter> liftE (do pa <- select {pa. (fst pa, True) \<in> fst p \<and> (snd pa, True) \<in> fst p \<and> fst pa \<noteq> snd pa};
y <- swap_for_delete (fst pa) (snd pa);
return (fst p, {})
od) \<sqinter> liftE (do victim' <- select {x. (x, True) \<in> snd p};
y <- PageTableUnmap_D.empty_slot victim';
return (fst p, {})
od) \<sqinter> throw) S) (?a'98 rva)
 2. \<And>rva. \<not> rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?P98 rva) (?Q'93 rva) (?a'98 rva) (returnOk ())
 3. \<And>rva s. \<lbrakk>\<not> rva; True\<rbrakk> \<Longrightarrow> (?P98 rva and ?Q98 rva) s
 4. \<And>rva s. \<lbrakk>\<not> rva; ?Q'15 () False s\<rbrakk> \<Longrightarrow> ?Q'93 rva s
 5. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 6. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 10. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (9 subgoals):
 1. \<And>rva. \<not> rva \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) (?P98 rva) (?Q'93 rva) (returnOk S) (returnOk ())
 2. \<And>rva s. \<lbrakk>\<not> rva; True\<rbrakk> \<Longrightarrow> (?P98 rva and (\<lambda>_. True)) s
 3. \<And>rva s. \<lbrakk>\<not> rva; ?Q'15 () False s\<rbrakk> \<Longrightarrow> ?Q'93 rva s
 4. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 9. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (6 subgoals):
 1. \<And>rv. \<lbrace>?Q'11 rv\<rbrace> work_units_limit_reached \<lbrace>?Q'15 rv\<rbrace>
 2. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 6. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (5 subgoals):
 1. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> work_units_limit_reached \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 5. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q'7\<rbrace> update_work_units \<lbrace>?Q'11\<rbrace>
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 4. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal (3 subgoals):
 1. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> update_work_units \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 3. \<And>s. True \<Longrightarrow> ?Q'7 s proof (prove)
goal:
No subgoals!