theory Syscall_DR

lemma decode_invocation_corres:
  "\<lbrakk> (Some intent) = transform_intent (invocation_type label) args;
     invoked_cap_ref = transform_cslot_ptr slot;
     invoked_cap = transform_cap cap;
     excaps = transform_cap_list excaps' \<rbrakk> \<Longrightarrow>
     dcorres (dc \<oplus> cdl_invocation_relation) \<top>
      (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s)
            and (cte_wp_at (Not \<circ> is_master_reply_cap) slot
            and cte_wp_at ((=) cap) slot)
            and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s)
            and valid_etcbs)
      (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
      (Decode_A.decode_invocation label args cap_index slot cap excaps')" apply(case_tac cap) apply (rule corres_guard_imp,rule decode_invocation_nullcap_corres, fastforce+)[1] apply (rule corres_guard_imp,rule decode_invocation_untypedcap_corres,
                     (fastforce elim: cte_wp_at_weakenE)+)[1] apply (rule corres_guard_imp,rule decode_invocation_endpointcap_corres, fastforce+)[1] apply (rule corres_guard_imp,rule decode_invocation_notificationcap_corres, fastforce+)[1] apply (rule corres_guard_imp,rule decode_invocation_replycap_corres, fastforce+)[1] apply (rule corres_guard_imp,rule decode_invocation_cnodecap_corres, fastforce+)[1] apply (rule corres_guard_imp, rule decode_invocation_tcbcap_corres, fastforce+)[1] apply (rule corres_guard_imp, rule decode_invocation_domaincap_corres, fastforce+)[1] apply (rule corres_guard_imp, rule decode_invocation_irqcontrolcap_corres, fastforce+)[1] apply (rule corres_guard_imp,rule decode_invocation_irqhandlercap_corres, fastforce+)[1] apply (rule corres_guard_imp,rule decode_invocation_zombiecap_corres, fastforce+)[1] apply (rule corres_guard_imp) apply (rule corres_rel_imp) apply (rule decode_invocation_archcap_corres, fastforce+)[1] apply clarsimp apply (case_tac x, simp) apply (clarsimp simp: cdl_invocation_relation_def) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (12 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x21 x22 x23 x24. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<And>x31 x32 x33. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 4. \<And>x41 x42 x43. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 5. \<And>x51 x52 x53. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 6. \<And>x61 x62 x63. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 7. \<And>x7. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 8. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 9. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 10. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x31 x32 x33. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<And>x41 x42 x43. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 4. \<And>x51 x52 x53. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 5. \<And>x61 x62 x63. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 6. \<And>x7. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 7. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 8. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 9. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 10. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x41 x42 x43. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<And>x51 x52 x53. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 4. \<And>x61 x62 x63. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 5. \<And>x7. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 6. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 7. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 8. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 9. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 10. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (9 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x51 x52 x53. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<And>x61 x62 x63. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 4. \<And>x7. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 5. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 6. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 7. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 8. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 9. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (8 subgoals):
 1. \<And>x51 x52 x53. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x61 x62 x63. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<And>x7. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 4. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 5. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 6. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 7. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 8. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (7 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x7. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 4. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 5. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 6. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 7. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (6 subgoals):
 1. \<And>x7. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 4. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 5. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 6. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (5 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 4. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 5. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 4. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (3 subgoals):
 1. \<And>x10. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 3. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps') proof (prove)
goal (3 subgoals):
 1. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (?Q380 x12) (?Q'380 x12) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; True\<rbrakk> \<Longrightarrow> ?Q380 x12 s
 3. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'380 x12 s proof (prove)
goal (4 subgoals):
 1. \<And>x12. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (?r'384 x12) (?Q380 x12) (?Q'380 x12) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label args cap_index slot cap excaps')
 2. \<And>x12 x y. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; ?r'384 x12 x y\<rbrakk> \<Longrightarrow> (dc \<oplus> cdl_invocation_relation) x y
 3. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; True\<rbrakk> \<Longrightarrow> ?Q380 x12 s
 4. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'380 x12 s proof (prove)
goal (3 subgoals):
 1. \<And>x12 x y. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (dc \<oplus> (\<lambda>rv rv'. \<exists>ai. rv' = InvokeArchObject ai \<and> arch_invocation_relation rv ai)) x y\<rbrakk> \<Longrightarrow> (dc \<oplus> cdl_invocation_relation) x y
 2. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; True\<rbrakk> \<Longrightarrow> True
 3. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and valid_etcbs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set (map fst excaps'). s \<turnstile> x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s)) s proof (prove)
goal (3 subgoals):
 1. \<And>x12 x y. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap (ArchObjectCap x12); excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (dc \<oplus> (\<lambda>rv rv'. \<exists>ai. rv' = InvokeArchObject ai \<and> arch_invocation_relation rv ai)) x y\<rbrakk> \<Longrightarrow> (dc \<oplus> cdl_invocation_relation) x y
 2. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; True\<rbrakk> \<Longrightarrow> True
 3. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and valid_etcbs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set (map fst excaps'). s \<turnstile> x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s)) s proof (prove)
goal (3 subgoals):
 1. \<And>x12 x y b. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap (ArchObjectCap x12); excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (dc \<oplus> (\<lambda>rv rv'. \<exists>ai. rv' = InvokeArchObject ai \<and> arch_invocation_relation rv ai)) x y; x = Inr b\<rbrakk> \<Longrightarrow> (dc \<oplus> cdl_invocation_relation) x y
 2. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; True\<rbrakk> \<Longrightarrow> True
 3. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and valid_etcbs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set (map fst excaps'). s \<turnstile> x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; True\<rbrakk> \<Longrightarrow> True
 2. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and valid_etcbs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set (map fst excaps'). s \<turnstile> x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>x12 s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = ArchObjectCap x12; (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) slot and cte_wp_at ((=) cap) slot) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and valid_etcbs and valid_cap cap and (\<lambda>s. \<forall>x\<in>set (map fst excaps'). s \<turnstile> x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s)) s proof (prove)
goal:
No subgoals!