theory SyscallArgs_C

lemma preemptionPoint_ccorres:
  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
      invs' UNIV []
      preemptionPoint (Call preemptionPoint_'proc)" apply (cinit simp: workUnitsLimit_def whenE_def) apply (rule ccorres_liftE_Seq) apply (rule ccorres_split_nothrow
               [where P=\<top> and P'=UNIV and r'=dc and xf'=xfdc]) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: modifyWorkUnits_def simpler_modify_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                             carch_state_relation_def
                             cmachine_state_relation_def) apply ceqv apply (rule ccorres_liftE_Seq) apply (rule ccorres_pre_getWorkUnits) apply (rule ccorres_cond_seq) apply (rule_tac R="\<lambda>s. rv = ksWorkUnitsCompleted s" in ccorres_cond2) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) prefer 2 apply simp apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (simp add: returnOk_def return_def) apply (rule ccorres_liftE_Seq) apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_split_nothrow
                 [where P=\<top> and P'=UNIV and r'=dc and xf'=xfdc]) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (thin_tac "P" for P)+ apply (clarsimp simp: setWorkUnits_def simpler_modify_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                               carch_state_relation_def
                               cmachine_state_relation_def) apply ceqv apply (rule ccorres_liftE_Seq) apply (ctac (no_vcg) add: isIRQPending_ccorres) apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def
                         return_def split: option.splits) apply (clarsimp simp: cintr_def exception_defs) apply wp+ apply vcg apply (unfold modifyWorkUnits_def)[1] apply wp apply vcg apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') invs' UNIV [] preemptionPoint (Call preemptionPoint_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') ?Q11 ?Q'11 [SKIP] (doE y <- liftE (modifyWorkUnits (\<lambda>u. u + 1));
workUnits <- liftE getWorkUnits;
if 0x64 \<le> workUnits then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()
odE) (\<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1;;
(IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q11 s \<and> s' \<in> ?Q'11 proof (prove)
goal (2 subgoals):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') ?Q11 ?Q'11 [SKIP] (do y <- modifyWorkUnits (\<lambda>u. u + 1);
doE workUnits <- liftE getWorkUnits;
if 0x64 \<le> workUnits then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()
odE
od) (\<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1;;
(IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q11 s \<and> s' \<in> ?Q'11 proof (prove)
goal (6 subgoals):
 1. ccorres dc xfdc (\<lambda>_. True) UNIV [SKIP] (modifyWorkUnits (\<lambda>u. u + 1)) (\<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1)
 2. \<And>rv' t t'. ceqv \<Gamma> xfdc rv' t t' (IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'19 rv')
 3. \<And>y rv'. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q19 y) (?Q'19 y rv') [SKIP] (doE workUnits <- liftE getWorkUnits;
if 0x64 \<le> workUnits then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()
odE) (?d'19 rv')
 4. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>?Q19\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> ?Q'19 y (xfdc s)}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (6 subgoals):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<exists>(rv, \<sigma>')\<in>fst (modifyWorkUnits (\<lambda>u. u + 1) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>rv' t t'. ceqv \<Gamma> xfdc rv' t t' (IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'19 rv')
 3. \<And>y rv'. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q19 y) (?Q'19 y rv') [SKIP] (doE workUnits <- liftE getWorkUnits;
if 0x64 \<le> workUnits then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()
odE) (?d'19 rv')
 4. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>?Q19\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> ?Q'19 y (xfdc s)}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma>. {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (modifyWorkUnits (\<lambda>u. u + 1) \<sigma>). (\<sigma>', globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. ksWorkUnitsCompleted_' (globals s) + 1)) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. ksWorkUnitsCompleted_' (globals s) + 1)) s))}
 2. \<And>rv' t t'. ceqv \<Gamma> xfdc rv' t t' (IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'19 rv')
 3. \<And>y rv'. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q19 y) (?Q'19 y rv') [SKIP] (doE workUnits <- liftE getWorkUnits;
if 0x64 \<le> workUnits then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()
odE) (?d'19 rv')
 4. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>?Q19\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> ?Q'19 y (xfdc s)}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> (\<sigma>\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted \<sigma> + 1\<rparr>, globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. ksWorkUnitsCompleted_' (globals x) + 1)) x) \<in> rf_sr
 2. \<And>rv' t t'. ceqv \<Gamma> xfdc rv' t t' (IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'19 rv')
 3. \<And>y rv'. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q19 y) (?Q'19 y rv') [SKIP] (doE workUnits <- liftE getWorkUnits;
if 0x64 \<le> workUnits then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()
odE) (?d'19 rv')
 4. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>?Q19\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> ?Q'19 y (xfdc s)}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. ceqv \<Gamma> xfdc rv' t t' (IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'19 rv')
 2. \<And>y rv'. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q19 y) (?Q'19 y rv') [SKIP] (doE workUnits <- liftE getWorkUnits;
if 0x64 \<le> workUnits then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()
odE) (?d'19 rv')
 3. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>?Q19\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> ?Q'19 y (xfdc s)}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (4 subgoals):
 1. \<And>y rv'. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q19 y) (?Q'19 y rv') [SKIP] (doE workUnits <- liftE getWorkUnits;
if 0x64 \<le> workUnits then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()
odE) (IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>?Q19\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> ?Q'19 y (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (4 subgoals):
 1. \<And>y rv'. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q19 y) (?Q'19 y rv') [SKIP] (do workUnits <- getWorkUnits;
if 0x64 \<le> workUnits then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()
od) (IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>?Q19\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> ?Q'19 y (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (4 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?P48 y rv) (?P'47 y rv' rv) [SKIP] (if 0x64 \<le> rv then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()) (IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ?P48 y rv s\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> ?P'47 y (xfdc s) rv}}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (4 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?P48 y rv) (?P'47 y rv' rv) [SKIP] (if 0x64 \<le> rv then doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE else returnOk ()) (IF 0x64 \<le> \<acute>ksWorkUnitsCompleted THEN
  \<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
ELSE
  SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
FI)
 2. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ?P48 y rv s\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> ?P'47 y (xfdc s) rv}}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (6 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> rv = ksWorkUnitsCompleted s \<longrightarrow> (0x64 \<le> rv) = (s' \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace>)
 2. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt55 y rv) (?Rt52 y rv' rv) [SKIP] (doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE) (\<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf57 y rv) (?Rf52 y rv' rv) [SKIP] (returnOk ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ?Pt55 y rv s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> ?Pf57 y rv s)) s\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rt52 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rf52 y (xfdc s) rv)}}}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (5 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt55 y rv) (?Rt52 y rv' rv) [SKIP] (doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE) (\<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf57 y rv) (?Rf52 y rv' rv) [SKIP] (returnOk ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ?Pt55 y rv s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> ?Pf57 y rv s)) s\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rt52 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rf52 y (xfdc s) rv)}}}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (5 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf57 y rv) (?Rf52 y rv' rv) [SKIP] (returnOk ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt55 y rv) (?Rt52 y rv' rv) [SKIP] (doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE) (\<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ?Pt55 y rv s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> ?Pf57 y rv s)) s\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rt52 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rf52 y (xfdc s) rv)}}}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (5 subgoals):
 1. \<And>rv' rv. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf57 () rv) (?Rf52 () rv' rv) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt55 y rv) (?Rt52 y rv' rv) [SKIP] (doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE) (\<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ?Pt55 y rv s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> ?Pf57 y rv s)) s\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rt52 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rf52 y (xfdc s) rv)}}}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (5 subgoals):
 1. \<And>rv' rv. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (returnOk () \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt55 y rv) (?Rt52 y rv' rv) [SKIP] (doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE) (\<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ?Pt55 y rv s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rt52 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (5 subgoals):
 1. \<And>rv' rv \<sigma>. {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (returnOk () \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt55 y rv) (?Rt52 y rv' rv) [SKIP] (doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE) (\<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ?Pt55 y rv s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rt52 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (4 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt55 y rv) (?Rt52 y rv' rv) [SKIP] (doE y <- liftE (setWorkUnits 0);
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE) (\<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ?Pt55 y rv s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rt52 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (4 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt55 y rv) (?Rt52 y rv' rv) [SKIP] (do y <- setWorkUnits 0;
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
od) (\<acute>ksWorkUnitsCompleted :== 0;;
\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ?Pt55 y rv s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rt52 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (4 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt55 y rv) (?Rt52 y rv' rv) [SKIP] (do y <- setWorkUnits 0;
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
od) (\<acute>ksWorkUnitsCompleted :== 0;;
(\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ?Pt55 y rv s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> ?Rt52 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (8 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) UNIV [SKIP] (setWorkUnits 0) (\<acute>ksWorkUnitsCompleted :== 0)
 2. \<And>y rv' rv rv'a t t'. dc y rv' \<Longrightarrow> ceqv \<Gamma> xfdc rv'a t t' (\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'91 y rv' rv rv'a)
 3. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q91 y rv' rv ya) (?Q'91 y rv' rv ya rv'a) [SKIP] (liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError) (?d'91 y rv' rv rv'a)
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>?Q91 y rv' rv\<rbrace>
 5. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> ?Q'91 y rv' rv ya (xfdc s)}
 6. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 7. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (8 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ksWorkUnitsCompleted :== 0 {s. \<exists>(rv, \<sigma>')\<in>fst (setWorkUnits 0 \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>y rv' rv rv'a t t'. dc y rv' \<Longrightarrow> ceqv \<Gamma> xfdc rv'a t t' (\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'91 y rv' rv rv'a)
 3. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q91 y rv' rv ya) (?Q'91 y rv' rv ya rv'a) [SKIP] (liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError) (?d'91 y rv' rv rv'a)
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>?Q91 y rv' rv\<rbrace>
 5. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> ?Q'91 y rv' rv ya (xfdc s)}
 6. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 7. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (8 subgoals):
 1. \<And>y rv' rv \<sigma>. dc y rv' \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setWorkUnits 0 \<sigma>). (\<sigma>', globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. 0)) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. 0)) s))}
 2. \<And>y rv' rv rv'a t t'. dc y rv' \<Longrightarrow> ceqv \<Gamma> xfdc rv'a t t' (\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'91 y rv' rv rv'a)
 3. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q91 y rv' rv ya) (?Q'91 y rv' rv ya rv'a) [SKIP] (liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError) (?d'91 y rv' rv rv'a)
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>?Q91 y rv' rv\<rbrace>
 5. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> ?Q'91 y rv' rv ya (xfdc s)}
 6. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 7. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (8 subgoals):
 1. \<And>y rv' rv \<sigma>. {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setWorkUnits 0 \<sigma>). (\<sigma>', globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. 0)) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. 0)) s))}
 2. \<And>y rv' rv rv'a t t'. dc y rv' \<Longrightarrow> ceqv \<Gamma> xfdc rv'a t t' (\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'91 y rv' rv rv'a)
 3. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q91 y rv' rv ya) (?Q'91 y rv' rv ya rv'a) [SKIP] (liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError) (?d'91 y rv' rv rv'a)
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>?Q91 y rv' rv\<rbrace>
 5. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> ?Q'91 y rv' rv ya (xfdc s)}
 6. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 7. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (8 subgoals):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> (\<sigma>\<lparr>ksWorkUnitsCompleted := 0\<rparr>, globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. 0)) x) \<in> rf_sr
 2. \<And>y rv' rv rv'a t t'. dc y rv' \<Longrightarrow> ceqv \<Gamma> xfdc rv'a t t' (\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'91 y rv' rv rv'a)
 3. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q91 y rv' rv ya) (?Q'91 y rv' rv ya rv'a) [SKIP] (liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError) (?d'91 y rv' rv rv'a)
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>?Q91 y rv' rv\<rbrace>
 5. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> ?Q'91 y rv' rv ya (xfdc s)}
 6. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 7. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (7 subgoals):
 1. \<And>y rv' rv rv'a t t'. dc y rv' \<Longrightarrow> ceqv \<Gamma> xfdc rv'a t t' (\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'91 y rv' rv rv'a)
 2. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q91 y rv' rv ya) (?Q'91 y rv' rv ya rv'a) [SKIP] (liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError) (?d'91 y rv' rv rv'a)
 3. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>?Q91 y rv' rv\<rbrace>
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> ?Q'91 y rv' rv ya (xfdc s)}
 5. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 6. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (6 subgoals):
 1. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q91 y rv' rv ya) (?Q'91 y rv' rv ya rv'a) [SKIP] (liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError) (\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>?Q91 y rv' rv\<rbrace>
 3. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> ?Q'91 y rv' rv ya (xfdc s)}
 4. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (6 subgoals):
 1. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q91 y rv' rv ya) (?Q'91 y rv' rv ya rv'a) [SKIP] (doMachineOp (getActiveIRQ True) >>= case_option (returnOk ()) throwError) (\<acute>ret__unsigned_long :== CALL isIRQPending_'proc();;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>?Q91 y rv' rv\<rbrace>
 3. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> ?Q'91 y rv' rv ya (xfdc s)}
 4. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (7 subgoals):
 1. \<And>y rv' rv ya rv'a rva ret__unsigned_long. \<lbrakk>dc y rv'; dc ya rv'a; ret__unsigned_long = from_bool (rva \<noteq> None)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q127 y rv' rv ya rv'a rva) (?Q'127 y rv' rv ya rv'a rva ret__unsigned_long) [SKIP] (case rva of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError x) (IF ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?R129 y rv' rv ya\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>?Q127 y rv' rv ya rv'a\<rbrace>
 3. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?R129 y rv' rv ya\<rbrace>
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rva. ret__unsigned_long_' t = from_bool (rva \<noteq> None) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'127 y rv' rv ya (xfdc s) rva (ret__unsigned_long_' t)}}
 5. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 6. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (7 subgoals):
 1. \<And>y rv' rv ya rv'a rva ret__unsigned_long. \<lbrakk>dc y rv'; dc ya rv'a; ret__unsigned_long = from_bool (rva \<noteq> None)\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} IF ret__unsigned_long \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst ((case rva of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError x) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?R129 y rv' rv ya\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?R129 y rv' rv ya\<rbrace>
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool (rv \<noteq> None) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}
 5. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 6. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (7 subgoals):
 1. \<And>y rv' rv ya rv'a rva ret__unsigned_long \<sigma>. \<lbrakk>dc y rv'; dc ya rv'a; ret__unsigned_long = from_bool (rva \<noteq> None)\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (ret__unsigned_long \<noteq> 0 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst ((case rva of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError x) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED, global_exn_var_' := Return\<rparr>)))) \<and> (\<not> ret__unsigned_long \<noteq> 0 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst ((case rva of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError x) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))))}
 2. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?R129 y rv' rv ya\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?R129 y rv' rv ya\<rbrace>
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool (rv \<noteq> None) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}
 5. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 6. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (7 subgoals):
 1. \<And>rva ret__unsigned_long \<sigma>. ret__unsigned_long = from_bool (\<exists>y. rva = Some y) \<Longrightarrow> \<forall>x2. rva = Some x2 \<longrightarrow> {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (\<sigma>, s) \<in> rf_sr \<and> EXCEPTION_PREEMPTED \<noteq> EXCEPTION_NONE \<and> cintr x2 (SCAST(32 signed \<rightarrow> 32) EXCEPTION_PREEMPTED) (errstate s)}
 2. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?R129 y rv' rv ya\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?R129 y rv' rv ya\<rbrace>
 4. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool (rv \<noteq> None) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}
 5. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 6. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (6 subgoals):
 1. \<And>y rv' rv ya rv'a. \<lbrakk>dc y rv'; dc ya rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?R129 y rv' rv ya\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<lbrace>?R92 y rv\<rbrace> setWorkUnits 0 \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?R129 y rv' rv ya\<rbrace>
 3. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool (rv \<noteq> None) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}
 4. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and ?R92 y rv) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (4 subgoals):
 1. \<And>y rv' rv. dc y rv' \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F91 y rv' rv\<^esub> (?R'91 y rv' rv) \<acute>ksWorkUnitsCompleted :== 0 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool (rv \<noteq> None) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> UNIV}}
 2. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rv. sa \<in> {sa. (sa \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV \<inter> ?R'91 y (xfdc s) rv) \<and> (sa \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R19\<rbrace> modifyWorkUnits (\<lambda>u. u + 1) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. \<forall>rv. s \<in> {s. (s \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> {s. \<forall>y. dc y (xfdc (globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. 0)) s)) \<longrightarrow> True \<and> (\<forall>t rv. ret__unsigned_long_' t = from_bool (rv \<noteq> None) \<longrightarrow> True)}) \<and> (s \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> s \<in> UNIV)}}}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R19\<rbrace> modify (\<lambda>ks. ks\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted ks + 1\<rparr>) \<lbrace>\<lambda>y s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) s\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. \<forall>rv. s \<in> {s. (s \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> {s. \<forall>y. dc y (xfdc (globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. 0)) s)) \<longrightarrow> True \<and> (\<forall>t rv. ret__unsigned_long_' t = from_bool (rv \<noteq> None) \<longrightarrow> True)}) \<and> (s \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> s \<in> UNIV)}}}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R19) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/?F19\<^esub> ?R'19 \<acute>ksWorkUnitsCompleted :== \<acute>ksWorkUnitsCompleted + 1 {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. \<forall>rv. s \<in> {s. (s \<in> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> {s. \<forall>y. dc y (xfdc (globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. 0)) s)) \<longrightarrow> True \<and> (\<forall>t rv. ret__unsigned_long_' t = from_bool (rv \<noteq> None) \<longrightarrow> True)}) \<and> (s \<notin> \<lbrace>0x64 \<le> \<acute>ksWorkUnitsCompleted\<rbrace> \<longrightarrow> s \<in> UNIV)}}}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<forall>rv. ksWorkUnitsCompleted (s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>) = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) (s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>))) s \<and> s' \<in> UNIV \<inter> ?R'19 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<forall>rv. ksWorkUnitsCompleted (s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>) = rv \<longrightarrow> ((\<lambda>s. rv = ksWorkUnitsCompleted s) and (\<lambda>s. 0x64 \<le> rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> True)) s) and (\<lambda>s. \<not> 0x64 \<le> rv \<longrightarrow> True)) (s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>))) s \<and> s' \<in> UNIV \<inter> {s. \<forall>y. dc y (xfdc (globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. ksWorkUnitsCompleted_' (globals s) + 1)) s)) \<longrightarrow> (\<forall>rv. (0x64 \<le> ksWorkUnitsCompleted_' (globals s) + 1 \<longrightarrow> True \<and> (\<forall>y. dc y (xfdc (globals_update (ksWorkUnitsCompleted_'_update (\<lambda>_. 0)) s)) \<longrightarrow> True \<and> (\<forall>t rv. ret__unsigned_long_' t = from_bool (rv \<noteq> None) \<longrightarrow> True))) \<and> (\<not> 0x64 \<le> ksWorkUnitsCompleted_' (globals s) + 1 \<longrightarrow> True))} proof (prove)
goal:
No subgoals!