theory CSpaceInv_AI

lemma set_cap_valid_ioc[wp]:
  notes hoare_pre [wp_pre del]
  shows "\<lbrace>valid_ioc and (\<lambda>s. p = cap.NullCap \<longrightarrow> \<not> is_original_cap s pt)\<rbrace>
   set_cap p pt
   \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: set_cap_def split_def) apply (wp set_object_valid_ioc_caps get_object_sp) prefer 2 apply (rule get_object_sp) apply (rule hoare_conjI) apply (clarsimp simp: valid_def return_def fail_def split_def
                         a_type_simps obj_at_def valid_ioc_def
                  split: Structures_A.kernel_object.splits) apply (rule hoare_conjI) apply (clarsimp simp: valid_def return_def fail_def split_def
                         a_type_simps obj_at_def valid_ioc_def
                  split: Structures_A.kernel_object.splits) apply (auto simp: wf_unique wf_cs_upd)[1] apply (clarsimp simp: valid_def return_def fail_def split_def
                        null_filter_def cap_of_def tcb_cnode_map_tcb_cap_cases
                        obj_at_def valid_ioc_def cte_wp_at_cases
                 split: Structures_A.kernel_object.splits) apply (intro conjI allI impI) apply fastforce apply fastforce apply (rule ccontr, clarsimp) apply (drule spec, frule spec, erule impE, assumption) apply (drule_tac x="snd pt" in spec) apply (case_tac pt) apply (clarsimp simp: tcb_cap_cases_def  split: if_split_asm) apply fastforce apply (rule ccontr, clarsimp) apply (drule spec, frule spec, erule impE, assumption) apply (drule_tac x="snd pt" in spec) apply (case_tac pt) apply (clarsimp simp: tcb_cap_cases_def  split: if_split_asm) apply fastforce apply (rule ccontr, clarsimp) apply (drule spec, frule spec, erule impE, assumption) apply (drule_tac x="snd pt" in spec) apply (case_tac pt) apply (clarsimp simp: tcb_cap_cases_def  split: if_split_asm) apply fastforce apply (rule ccontr, clarsimp) apply (drule spec, frule spec, erule impE, assumption) apply (drule_tac x="snd pt" in spec) apply (case_tac pt) apply (clarsimp simp: tcb_cap_cases_def  split: if_split_asm) apply fastforce apply (rule ccontr, clarsimp) apply (drule spec, frule spec, erule impE, assumption) apply (drule_tac x="snd pt" in spec) apply (case_tac pt) apply (clarsimp simp: tcb_cap_cases_def  split: if_split_asm) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt)\<rbrace> set_cap p pt \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt)\<rbrace> do obj <- get_object (fst pt);
(case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst pt)
od \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>obj. \<lbrace>?B obj\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. valid_ioc s \<and> typ_at (a_type x) (fst pt) s \<and> (\<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> null_filter (cap_of x) b \<noteq> None)\<rbrace>
 2. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt)\<rbrace> get_object (fst pt) \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt)\<rbrace> get_object (fst pt) \<lbrace>?B\<rbrace>
 2. \<And>obj. \<lbrace>?B obj\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. valid_ioc s \<and> typ_at (a_type x) (fst pt) s \<and> (\<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> null_filter (cap_of x) b \<noteq> None)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt) and ko_at obj (fst pt)\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. valid_ioc s \<and> typ_at (a_type x) (fst pt) s \<and> (\<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> null_filter (cap_of x) b \<noteq> None)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>obj. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt) and ko_at obj (fst pt)\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>r. valid_ioc\<rbrace>
 2. \<And>obj. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt) and ko_at obj (fst pt)\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>r s. typ_at (a_type r) (fst pt) s \<and> (\<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> null_filter (cap_of r) b \<noteq> None)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt) and ko_at obj (fst pt)\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>r s. typ_at (a_type r) (fst pt) s \<and> (\<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> null_filter (cap_of r) b \<noteq> None)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>obj. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt) and ko_at obj (fst pt)\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>r. typ_at (a_type r) (fst pt)\<rbrace>
 2. \<And>obj. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt) and ko_at obj (fst pt)\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>r s. \<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> null_filter (cap_of r) b \<noteq> None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 y s. \<lbrakk>\<not> well_formed_cnode_n x11 (x12(snd pt \<mapsto> p)); well_formed_cnode_n x11 x12; x12 (snd pt) = Some y; \<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s; p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (CNode x11 x12)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt) and ko_at obj (fst pt)\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>r s. \<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> null_filter (cap_of r) b \<noteq> None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrace>valid_ioc and (\<lambda>s. p = NullCap \<longrightarrow> \<not> is_original_cap s pt) and ko_at obj (fst pt)\<rbrace> case obj of CNode sz cn \<Rightarrow> if snd pt \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd pt \<mapsto> p) else fail | TCB tcb \<Rightarrow> if snd pt = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := p\<rparr> else if snd pt = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := p\<rparr> else if snd pt = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := p\<rparr> else if snd pt = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := p\<rparr> else if snd pt = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := p\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>r s. \<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> null_filter (cap_of r) b \<noteq> None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. (\<forall>x11 x12. snd pt \<in> dom x12 \<and> well_formed_cnode_n x11 x12 \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> (\<forall>s. (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (CNode x11 x12) \<longrightarrow> (\<forall>b. b \<noteq> snd pt \<longrightarrow> (x12 b = Some NullCap \<longrightarrow> \<not> is_original_cap s (fst pt, b)) \<and> (x12 b \<noteq> Some NullCap \<longrightarrow> is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>y. x12 b = Some y))))) \<and> (\<forall>x2. (snd pt = tcb_cnode_index 4 \<longrightarrow> obj = TCB x2 \<longrightarrow> (\<forall>s. (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2) \<longrightarrow> (\<forall>b. ((\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ipcframe := p\<rparr>) = NullCap) \<longrightarrow> \<not> is_original_cap s (fst pt, b)) \<and> ((\<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ipcframe := p\<rparr>) \<noteq> NullCap) \<longrightarrow> is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)))))) \<and> (snd pt \<noteq> tcb_cnode_index 4 \<longrightarrow> (snd pt = tcb_cnode_index 3 \<longrightarrow> obj = TCB x2 \<longrightarrow> (\<forall>s. (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2) \<longrightarrow> (\<forall>b. ((\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap) \<longrightarrow> \<not> is_original_cap s (fst pt, b)) \<and> ((\<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap) \<longrightarrow> is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)))))) \<and> (snd pt \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd pt = tcb_cnode_index 2 \<longrightarrow> obj = TCB x2 \<longrightarrow> (\<forall>s. (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2) \<longrightarrow> (\<forall>b. ((\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap) \<longrightarrow> \<not> is_original_cap s (fst pt, b)) \<and> ((\<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap) \<longrightarrow> is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)))))) \<and> (snd pt \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd pt = tcb_cnode_index (Suc 0) \<longrightarrow> obj = TCB x2 \<longrightarrow> (\<forall>s. (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2) \<longrightarrow> (\<forall>b. ((\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap) \<longrightarrow> \<not> is_original_cap s (fst pt, b)) \<and> ((\<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap) \<longrightarrow> is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)))))) \<and> (snd pt \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> snd pt = tcb_cnode_index 0 \<longrightarrow> obj = TCB x2 \<longrightarrow> (\<forall>s. (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2) \<longrightarrow> (\<forall>b. ((\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap) \<longrightarrow> \<not> is_original_cap s (fst pt, b)) \<and> ((\<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap) \<longrightarrow> is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)))))))))) proof (prove)
goal (12 subgoals):
 1. \<And>obj x11 x12 s b. \<lbrakk>snd pt \<in> dom x12 \<and> well_formed_cnode_n x11 x12; obj = CNode x11 x12; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (CNode x11 x12); b \<noteq> snd pt; x12 b = Some NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 2. \<And>obj x11 x12 s b. \<lbrakk>snd pt \<in> dom x12 \<and> well_formed_cnode_n x11 x12; obj = CNode x11 x12; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (CNode x11 x12); b \<noteq> snd pt; x12 b \<noteq> Some NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>y. x12 b = Some y
 3. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ipcframe := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ipcframe := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 9. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 10. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>obj x11 x12 s b. \<lbrakk>snd pt \<in> dom x12 \<and> well_formed_cnode_n x11 x12; obj = CNode x11 x12; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (CNode x11 x12); b \<noteq> snd pt; x12 b \<noteq> Some NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>y. x12 b = Some y
 2. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ipcframe := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 3. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ipcframe := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 9. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 10. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ipcframe := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 2. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ipcframe := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 9. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 10. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (10 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 4; is_original_cap s (fst pt, b); \<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); a (x2\<lparr>tcb_ipcframe := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ipcframe := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 9. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 10. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (10 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 4; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_ipcframe := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); \<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ipcframe := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 9. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 10. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (10 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 4; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_ipcframe := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ipcframe := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 9. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 10. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (10 subgoals):
 1. \<And>x2 s b a aa ba ab bb. \<lbrakk>snd pt = tcb_cnode_index 4; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_ipcframe := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); pt = (ab, bb)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ipcframe := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 9. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 10. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (9 subgoals):
 1. \<And>obj x2 s b. \<lbrakk>snd pt = tcb_cnode_index 4; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ipcframe := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 9. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (8 subgoals):
 1. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (8 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 3; is_original_cap s (fst pt, b); \<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (8 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 3; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); \<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (8 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 3; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (8 subgoals):
 1. \<And>x2 s b a aa ba ab bb. \<lbrakk>snd pt = tcb_cnode_index 3; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_caller := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); pt = (ab, bb)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 8. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (7 subgoals):
 1. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt = tcb_cnode_index 3; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_caller := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 7. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (6 subgoals):
 1. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (6 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 2; is_original_cap s (fst pt, b); \<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (6 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 2; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); \<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (6 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 2; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (6 subgoals):
 1. \<And>x2 s b a aa ba ab bb. \<lbrakk>snd pt = tcb_cnode_index 2; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_reply := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); pt = (ab, bb)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 6. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (5 subgoals):
 1. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt = tcb_cnode_index 2; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_reply := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 5. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (4 subgoals):
 1. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (4 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index (Suc 0); is_original_cap s (fst pt, b); \<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (4 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index (Suc 0); is_original_cap s (fst pt, b); a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); \<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (4 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index (Suc 0); is_original_cap s (fst pt, b); a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (4 subgoals):
 1. \<And>x2 s b a aa ba ab bb. \<lbrakk>snd pt = tcb_cnode_index (Suc 0); is_original_cap s (fst pt, b); a (x2\<lparr>tcb_vtable := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); pt = (ab, bb)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 4. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (3 subgoals):
 1. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt = tcb_cnode_index (Suc 0); obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_vtable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 3. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (2 subgoals):
 1. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> \<not> is_original_cap s (fst pt, b)
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 0; is_original_cap s (fst pt, b); \<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 0; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); \<forall>b. is_original_cap s (fst pt, b) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s b a aa ba. \<lbrakk>snd pt = tcb_cnode_index 0; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s b a aa ba ab bb. \<lbrakk>snd pt = tcb_cnode_index 0; is_original_cap s (fst pt, b); a (x2\<lparr>tcb_ctable := p\<rparr>) = NullCap; tcb_cap_cases b = Some (a, aa, ba); p = NullCap \<longrightarrow> \<not> is_original_cap s pt; kheap s (fst pt) = Some (TCB x2); (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); is_original_cap s (fst pt, snd pt) \<longrightarrow> (\<exists>sz fun. kheap s (fst pt) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd pt) = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s (fst pt) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd pt) = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); pt = (ab, bb)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal (1 subgoal):
 1. \<And>obj x2 s b. \<lbrakk>snd pt \<noteq> tcb_cnode_index 4; snd pt \<noteq> tcb_cnode_index 3; snd pt \<noteq> tcb_cnode_index 2; snd pt \<noteq> tcb_cnode_index (Suc 0); snd pt = tcb_cnode_index 0; obj = TCB x2; (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))) \<and> (p = NullCap \<longrightarrow> \<not> is_original_cap s pt) \<and> kheap s (fst pt) = Some (TCB x2); \<forall>a. (\<forall>aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<or> a (x2\<lparr>tcb_ctable := p\<rparr>) \<noteq> NullCap; is_original_cap s (fst pt, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba) proof (prove)
goal:
No subgoals!