theory ArchIRQMasks_IF

lemma invoke_tcb_irq_masks[IRQMasks_IF_assms]:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace>
   invoke_tcb tinv
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" apply (case_tac tinv) apply((wp restart_irq_masks hoare_vcg_if_lift  mapM_x_wp[OF _ subset_refl]
                | wpc
                | simp split del: if_split add: check_cap_at_def
                | clarsimp)+)[3] defer apply ((wp | simp )+)[2] 
    (* NotificationControl *)
     apply (rename_tac option) apply (case_tac option) apply ((wp | simp)+)[2] 
   (* just ThreadControl left *)
    apply (simp add: split_def cong: option.case_cong) apply wpsimp+ apply (rule hoare_post_impErr[OF cap_delete_irq_masks[where P=P]]) apply blast apply blast apply (wpsimp wp: hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R hoare_vcg_all_lift hoare_drop_imps
                        checked_cap_insert_domain_sep_inv)+ apply (rule_tac Q="\<lambda> r s. domain_sep_inv False st s \<and> P (irq_masks_of_state s)"
                  and E="\<lambda>_ s. P (irq_masks_of_state s)" in hoare_post_impErr) apply (wp hoare_vcg_conj_liftE1 cap_delete_irq_masks) apply fastforce apply blast apply (wpsimp wp: hoare_weak_lift_imp hoare_vcg_all_lift checked_cap_insert_domain_sep_inv)+ apply (rule_tac Q="\<lambda> r s. domain_sep_inv False st s \<and> P (irq_masks_of_state s)"
                 and E="\<lambda>_ s. P (irq_masks_of_state s)" in hoare_post_impErr) apply (wp hoare_vcg_conj_liftE1 cap_delete_irq_masks) apply fastforce apply blast apply (simp add: option_update_thread_def | wp hoare_weak_lift_imp hoare_vcg_all_lift | wpc)+ by fastforce+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. tinv = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x21 x22 x23 x24. tinv = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37. tinv = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x5. tinv = Suspend x5 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 6. \<And>x6. tinv = Resume x6 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 7. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 8. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x5. tinv = Suspend x5 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x6. tinv = Resume x6 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x5. tinv = Suspend x5 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x6. tinv = Resume x6 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 option. tinv = NotificationControl x71 option \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x71 option. \<lbrakk>tinv = NotificationControl x71 option; option = None\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x71 option a. \<lbrakk>tinv = NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and (tcb_at x81 and ex_nonz_cap_to x81)\<rbrace> liftE (do y <- as_user x81 (setRegister tlsBaseRegister x82);
cur <- gets cur_thread;
y <- when (x81 = cur) reschedule_required;
return []
od) \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x1 x2a. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 (Some (x1, x2a)) \<Longrightarrow> \<lbrace>?R279 x41 a b x43 x44 x45 x46 x47 (Some (x1, x2a)) () () () () (x1, x2a) x1 x2a\<rbrace> cap_delete (x41, tcb_cnode_index 4) \<lbrace>\<lambda>a b. (x2a = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state b)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state b))) \<and> ((\<exists>a aa b. x2a = Some (a, aa, b)) \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state b)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state b)))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x xa. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B226 x41 a b x43 x44 x45 x46 x47 x48 y x xa\<rbrace> case x47 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index (Suc 0));
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index (Suc 0)))))
odE \<lbrace>\<lambda>xb s. (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>xc. x48 = Some xc \<longrightarrow> (\<forall>xd xe. xc = (xd, xe) \<longrightarrow> ?R279 x41 a b x43 x44 x45 x46 x47 x48 y x xa xb xc xd xe s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace> case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index 0))))
odE \<lbrace>?B226 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 6. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (7 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x1 x2a rv s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 (Some (x1, x2a)); P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> (x2a = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state s))) \<and> ((\<exists>a aa b. x2a = Some (a, aa, b)) \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state s)))
 2. \<And>x41 a b x43 x44 x45 x46 x47 x1 x2a e s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 (Some (x1, x2a)); P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s)
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x xa. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B226 x41 a b x43 x44 x45 x46 x47 x48 y x xa\<rbrace> case x47 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index (Suc 0));
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index (Suc 0)))))
odE \<lbrace>\<lambda>xb s. (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>xc. x48 = Some xc \<longrightarrow> (\<forall>xd xe. xc = (xd, xe) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st382 x41 a b x43 x44 x45 x46 x47 x48 y x xa xb xc xd xe)) s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace> case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index 0))))
odE \<lbrace>?B226 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 6. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 7. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (6 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x1 x2a e s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 (Some (x1, x2a)); P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s)
 2. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x xa. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B226 x41 a b x43 x44 x45 x46 x47 x48 y x xa\<rbrace> case x47 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index (Suc 0));
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index (Suc 0)))))
odE \<lbrace>\<lambda>xb s. (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>xc. x48 = Some xc \<longrightarrow> (\<forall>xd xe. xc = (xd, xe) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st382 x41 a b x43 x44 x45 x46 x47 x48 y x xa xb xc xd xe)) s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace> case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index 0))))
odE \<lbrace>?B226 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 6. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (5 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x xa. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B226 x41 a b x43 x44 x45 x46 x47 x48 y x xa\<rbrace> case x47 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index (Suc 0));
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index (Suc 0)))))
odE \<lbrace>\<lambda>xb s. (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>xc. x48 = Some xc \<longrightarrow> (\<forall>xd xe. xc = (xd, xe) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st382 x41 a b x43 x44 x45 x46 x47 x48 y x xa xb xc xd xe)) s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace> case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index 0))))
odE \<lbrace>?B226 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (5 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x48 x1 ac bb. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 (Some (x1, ac, bb)) x48 \<Longrightarrow> \<lbrace>?R468 ac bb x41 a b x43 x44 x45 x46 (Some (x1, ac, bb)) x48 () () () (x1, ac, bb) x1 (ac, bb)\<rbrace> cap_delete (x41, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>xb s. P (irq_masks_of_state s) \<and> (\<forall>aa ba x xa. domain_sep_inv False (?st466 aa ba x1 ac bb (ac, bb) (x1, ac, bb) x41 a b x43 x44 x45 x46 (Some (x1, ac, bb)) x48 () () () (aa, ba) x xa) s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace> case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index 0))))
odE \<lbrace>\<lambda>xa s. (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>xb. x48 = Some xb \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st466 (fst xb) (snd xb) (fst (the x47)) (fst (snd (the x47))) (snd (snd (the x47))) (snd (the x47)) (the x47) x41 a b x43 x44 x45 x46 x47 x48 y x xa xb xc xd)) s))) \<and> (\<forall>xb. x47 = Some xb \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> ?R468 (fst xd) (snd xd) x41 a b x43 x44 x45 x46 x47 x48 y x xa xb xc xd s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (7 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x48 x1 ac bb. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 (Some (x1, ac, bb)) x48 \<Longrightarrow> \<lbrace>?R852 x41 a b x43 x44 x45 x46 ac bb (Some (x1, ac, bb)) x48 () () () (x1, ac, bb) x1 (ac, bb)\<rbrace> cap_delete (x41, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>r s. domain_sep_inv False st s \<and> P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 a b x43 x44 x45 x46 x48 x1 ac bb rv s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 (Some (x1, ac, bb)) x48; domain_sep_inv False st s \<and> P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s) \<and> (\<forall>aa ba x xa. domain_sep_inv False (?st466 aa ba x1 ac bb (ac, bb) (x1, ac, bb) x41 a b x43 x44 x45 x46 (Some (x1, ac, bb)) x48 () () () (aa, ba) x xa) s)
 3. \<And>x41 a b x43 x44 x45 x46 x48 x1 ac bb e s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 (Some (x1, ac, bb)) x48; P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s)
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace> case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index 0))))
odE \<lbrace>\<lambda>xa s. (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>xb. x48 = Some xb \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st466 (fst xb) (snd xb) (fst (the x47)) (fst (snd (the x47))) (snd (snd (the x47))) (snd (the x47)) (the x47) x41 a b x43 x44 x45 x46 x47 x48 y x xa xb xc xd)) s))) \<and> (\<forall>xb. x47 = Some xb \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> ?R852 x41 a b x43 x44 x45 x46 (fst xd) (snd xd) x47 x48 y x xa xb xc xd s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 6. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 7. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (6 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x48 x1 ac bb rv s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 (Some (x1, ac, bb)) x48; domain_sep_inv False st s \<and> P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s) \<and> (\<forall>aa ba x xa. domain_sep_inv False (?st466 aa ba x1 ac bb (ac, bb) (x1, ac, bb) x41 a b x43 x44 x45 x46 (Some (x1, ac, bb)) x48 () () () (aa, ba) x xa) s)
 2. \<And>x41 a b x43 x44 x45 x46 x48 x1 ac bb e s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 (Some (x1, ac, bb)) x48; P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s)
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace> case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index 0))))
odE \<lbrace>\<lambda>xa s. (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>xb. x48 = Some xb \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st466 (fst xb) (snd xb) (fst (the x47)) (fst (snd (the x47))) (snd (snd (the x47))) (snd (the x47)) (the x47) x41 a b x43 x44 x45 x46 x47 x48 y x xa xb xc xd)) s))) \<and> (\<forall>xb. x47 = Some xb \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st864 x41 a b x43 x44 x45 x46 (fst xd) (snd xd) x47 x48 y x xa xb xc xd))) s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 6. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (5 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x48 x1 ac bb e s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 (Some (x1, ac, bb)) x48; P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s)
 2. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace> case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index 0))))
odE \<lbrace>\<lambda>xa s. (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s))) \<and> (\<forall>xb. x47 = Some xb \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st864 x41 a b x43 x44 x45 x46 (fst xd) (snd xd) x47 x48 y x xa xb xc xd))) s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (4 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x48 y x. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y x\<rbrace> case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> case x2 of (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap x41) (a, b) (cap_insert new_cap src_slot (x41, tcb_cnode_index 0))))
odE \<lbrace>\<lambda>xa s. (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s))) \<and> (\<forall>xb. x47 = Some xb \<longrightarrow> (\<forall>xc xd. xb = (xc, xd) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st864 x41 a b x43 x44 x45 x46 (fst xd) (snd xd) x47 x48 y x xa xb xc xd))) s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>?B225 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (4 subgoals):
 1. \<And>x41 a b x43 x44 x45 x47 x48 x1 ac bb. tinv = ThreadControl x41 (a, b) x43 x44 x45 (Some (x1, ac, bb)) x47 x48 \<Longrightarrow> \<lbrace>?R981 ac bb x41 a b x43 x44 x45 (Some (x1, ac, bb)) x47 x48 () () (x1, ac, bb) x1 (ac, bb)\<rbrace> cap_delete (x41, tcb_cnode_index 0) \<lbrace>\<lambda>xa s. (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state s))) \<and> ((\<exists>a b. x48 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state s) \<and> domain_sep_inv False st s)) \<and> (\<forall>aa ab ba. x47 = Some (aa, ab, ba) \<longrightarrow> domain_sep_inv False st s \<and> P (irq_masks_of_state s) \<and> domain_sep_inv False (?st979 x1 ac bb (ac, bb) (x1, ac, bb) x41 a b x43 x44 x45 (Some (x1, ac, bb)) ab ba (Some (aa, ab, ba)) x48 () () (aa, ab, ba) aa (ab, ba)) s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>\<lambda>x s. (x46 = None \<longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s))) \<and> (\<forall>xa. x47 = Some xa \<longrightarrow> (\<forall>xb xc. xa = (xb, xc) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st979 (fst (the x46)) (fst (snd (the x46))) (snd (snd (the x46))) (snd (the x46)) (the x46) x41 a b x43 x44 x45 x46 (fst xc) (snd xc) x47 x48 y x xa xb xc))) s))) \<and> (\<forall>xa. x46 = Some xa \<longrightarrow> (\<forall>xb xc. xa = (xb, xc) \<longrightarrow> ?R981 (fst xc) (snd xc) x41 a b x43 x44 x45 x46 x47 x48 y x xa xb xc s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (6 subgoals):
 1. \<And>x41 a b x43 x44 x45 x47 x48 x1 ac bb. tinv = ThreadControl x41 (a, b) x43 x44 x45 (Some (x1, ac, bb)) x47 x48 \<Longrightarrow> \<lbrace>?R1846 x41 a b x43 x44 x45 ac bb (Some (x1, ac, bb)) x47 x48 () () (x1, ac, bb) x1 (ac, bb)\<rbrace> cap_delete (x41, tcb_cnode_index 0) \<lbrace>\<lambda>r s. domain_sep_inv False st s \<and> P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 a b x43 x44 x45 x47 x48 x1 ac bb rv s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 (Some (x1, ac, bb)) x47 x48; domain_sep_inv False st s \<and> P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state s))) \<and> ((\<exists>a b. x48 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state s) \<and> domain_sep_inv False st s)) \<and> (\<forall>aa ab ba. x47 = Some (aa, ab, ba) \<longrightarrow> domain_sep_inv False st s \<and> P (irq_masks_of_state s) \<and> domain_sep_inv False (?st979 x1 ac bb (ac, bb) (x1, ac, bb) x41 a b x43 x44 x45 (Some (x1, ac, bb)) ab ba (Some (aa, ab, ba)) x48 () () (aa, ab, ba) aa (ab, ba)) s)
 3. \<And>x41 a b x43 x44 x45 x47 x48 x1 ac bb e s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 (Some (x1, ac, bb)) x47 x48; P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s)
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>\<lambda>x s. (x46 = None \<longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s))) \<and> (\<forall>xa. x47 = Some xa \<longrightarrow> (\<forall>xb xc. xa = (xb, xc) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st979 (fst (the x46)) (fst (snd (the x46))) (snd (snd (the x46))) (snd (the x46)) (the x46) x41 a b x43 x44 x45 x46 (fst xc) (snd xc) x47 x48 y x xa xb xc))) s))) \<and> (\<forall>xa. x46 = Some xa \<longrightarrow> (\<forall>xb xc. xa = (xb, xc) \<longrightarrow> ?R1846 x41 a b x43 x44 x45 (fst xc) (snd xc) x46 x47 x48 y x xa xb xc s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 6. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (5 subgoals):
 1. \<And>x41 a b x43 x44 x45 x47 x48 x1 ac bb rv s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 (Some (x1, ac, bb)) x47 x48; domain_sep_inv False st s \<and> P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state s))) \<and> ((\<exists>a b. x48 = Some (a, b)) \<longrightarrow> P (irq_masks_of_state s) \<and> domain_sep_inv False st s)) \<and> (\<forall>aa ab ba. x47 = Some (aa, ab, ba) \<longrightarrow> domain_sep_inv False st s \<and> P (irq_masks_of_state s) \<and> domain_sep_inv False (?st979 x1 ac bb (ac, bb) (x1, ac, bb) x41 a b x43 x44 x45 (Some (x1, ac, bb)) ab ba (Some (aa, ab, ba)) x48 () () (aa, ab, ba) aa (ab, ba)) s)
 2. \<And>x41 a b x43 x44 x45 x47 x48 x1 ac bb e s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 (Some (x1, ac, bb)) x47 x48; P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s)
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>\<lambda>x s. (x46 = None \<longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s))) \<and> (\<forall>xa. x47 = Some xa \<longrightarrow> (\<forall>xb xc. xa = (xb, xc) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st979 (fst (the x46)) (fst (snd (the x46))) (snd (snd (the x46))) (snd (the x46)) (the x46) x41 a b x43 x44 x45 x46 (fst xc) (snd xc) x47 x48 y x xa xb xc))) s))) \<and> (\<forall>xa. x46 = Some xa \<longrightarrow> (\<forall>xb xc. xa = (xb, xc) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st1858 x41 a b x43 x44 x45 (fst xc) (snd xc) x46 x47 x48 y x xa xb xc))) s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (4 subgoals):
 1. \<And>x41 a b x43 x44 x45 x47 x48 x1 ac bb e s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 (Some (x1, ac, bb)) x47 x48; P (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> P (irq_masks_of_state s)
 2. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>\<lambda>x s. (x46 = None \<longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s))) \<and> (\<forall>x. x47 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st)) s))) \<and> (\<forall>xa. x46 = Some xa \<longrightarrow> (\<forall>xb xc. xa = (xb, xc) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st1858 x41 a b x43 x44 x45 (fst xc) (snd xc) x46 x47 x48 y x xa xb xc))) s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (3 subgoals):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x48 y. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48 y\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> case x2 of (newmcp, x) \<Rightarrow> set_mcpriority x41 newmcp) \<lbrace>\<lambda>x s. (x46 = None \<longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> P (irq_masks_of_state s)) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> P (irq_masks_of_state s)))) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s))) \<and> (\<forall>x. x47 = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st)) s))) \<and> (\<forall>xa. x46 = Some xa \<longrightarrow> (\<forall>xb xc. xa = (xb, xc) \<longrightarrow> (domain_sep_inv False st and ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (?st1858 x41 a b x43 x44 x45 (fst xc) (snd xc) x46 x47 x48 y x xa xb xc))) s))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x41 a b x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>?Q224 x41 a b (a, b) x43 x44 x45 x46 x47 x48\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>?B222 x41 a b x43 x44 x45 x46 x47 x48\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and tcb_inv_wf tinv) s\<rbrakk> \<Longrightarrow> ?Q224 x41 (fst x42) (snd x42) x42 x43 x44 x45 x46 x47 x48 s proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> tcb_at x41 s \<and> (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case x46 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) \<and> (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s \<and> (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case x47 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) \<and> (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s \<and> (case x48 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case x48 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case x48 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case x48 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) \<and> (case x48 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s \<and> ((\<exists>a aa b. x46 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s) \<and> ((\<exists>a aa b. x47 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s) \<and> ((\<exists>a b. x48 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s) \<and> (case x43 of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) \<and> (case x45 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) pr) auth s) \<and> (case x44 of None \<Rightarrow> True | Some (mcp, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) mcp) auth s) \<and> ex_nonz_cap_to x41 s\<rbrakk> \<Longrightarrow> \<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> (x44 = None \<longrightarrow> (x43 = None \<longrightarrow> domain_sep_inv False (?st2479 x41 (fst x42) (snd x42) x42 None x45 x47 x48 x xa xb) s) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> domain_sep_inv False (?st2503 x41 (fst x42) (snd x42) x42 (Some xc) x45 x47 x48 x xa xb xc) s)) \<and> (\<forall>xc xd. x44 = Some (xc, xd) \<longrightarrow> (x43 = None \<longrightarrow> domain_sep_inv False (?st2536 x41 (fst x42) (snd x42) x42 None x45 x47 x48 x xa xb xc xd) s) \<and> (\<forall>xe. x43 = Some xe \<longrightarrow> domain_sep_inv False (?st2560 x41 (fst x42) (snd x42) x42 (Some xe) x45 x47 x48 x xa xb xc xd xe) s))
flex-flex pairs:
\<lambda>x41 a b x45 x47 x48 x xa xb aa ba x2. ?st2560 x41 a b (a, b) (Some x2) x45 x47 x48 x xa xb aa ba x2 \<equiv>\<^sup>? \<lambda>x41 a b x45 x47 x48 x xa xb aa ba x2. ?st2559 x41 a b x2 (Some x2) (Some (aa, ba)) x45 x47 x48 () x xa xb (aa, ba) aa ba
\<lambda>x41 a b x45 x47 x48 x xa xb aa ba. ?st2559 x41 a b (the (ds_id None)) (ds_id None) (Some (aa, ba)) x45 x47 x48 () x xa xb (aa, ba) aa ba \<equiv>\<^sup>? \<lambda>x41 a b. ?st2536 x41 a b (a, b) (ds_id None)
\<lambda>x41 a b x45 x47 x48 x xa xb x2. ?st2503 x41 a b (a, b) (Some x2) x45 x47 x48 x xa xb x2 \<equiv>\<^sup>? \<lambda>x41 a b x45 x47 x48 x xa xb x2. ?st2502 x41 a b x2 (Some x2) (ds_id None) x45 x47 x48 () x xa xb
\<lambda>x41 a b x45 x47 x48. ?st2502 x41 a b (the (ds_id None)) (ds_id None) (ds_id None) x45 x47 x48 () \<equiv>\<^sup>? \<lambda>x41 a b. ?st2479 x41 a b (a, b) (ds_id None)
\<lambda>x41 a b x43 x45 x47 x48 aa ab ba x1 x2a. ?st2559 x41 a b (the x43) x43 (Some (x1, x2a)) x45 x47 x48 () aa ab ba (x1, x2a) x1 x2a \<equiv>\<^sup>? \<lambda>x41 a b x43 x45 x47 x48 aa ab ba x1 x2a. ?st2119 x1 x2a (x1, x2a) x41 a b x43 (Some (x1, x2a)) x45 ab ba (Some (aa, ab, ba)) x47 x48 () () (aa, ab, ba) aa (ab, ba)
\<lambda>x41 a b x43 x45 x47 x48. ?st2502 x41 a b (the x43) x43 (ds_id None) x45 x47 x48 () \<equiv>\<^sup>? \<lambda>x41 a b x43 x45 x47 x48 aa ab ba. ?st2119 (fst (the (ds_id None))) (snd (the (ds_id None))) (the (ds_id None)) x41 a b x43 (ds_id None) x45 ab ba (Some (aa, ab, ba)) x47 x48 () () (aa, ab, ba) aa (ab, ba)