theory PageTableDuplicates

lemma invokeCNode_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s)
  \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv
  \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (case_tac cinv) apply (clarsimp simp add:invokeCNode_def | wp | intro conjI)+ apply (rule valid_validE) apply (rule hoare_post_imp[OF _ cteRevoke_valid_duplicates']) apply simp apply (simp add:invs_valid_objs' invs_pspace_aligned') apply (clarsimp simp add:invokeCNode_def | wp | intro conjI)+ apply (rule hoare_pre) apply (wp unless_wp | wpc | simp)+ apply (simp add:invokeCNode_def) apply (wp getSlotCap_inv hoare_drop_imp
     |simp add:locateSlot_conv getThreadCallerSlot_def
     |wpc)+ apply (simp add:cteDelete_def invokeCNode_def) apply (wp getSlotCap_inv hoare_drop_imp
     |simp add:locateSlot_conv getThreadCallerSlot_def
    whenE_def split_def
     |wpc)+ apply (rule valid_validE) apply (rule hoare_post_imp[OF _ finaliseSlot_valid_duplicates']) apply simp apply (simp add:invs_valid_objs' invs_pspace_aligned') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13. cinv = Insert x11 x12 x13 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x21 x22 x23 x24 x25. cinv = Rotate x21 x22 x23 x24 x25 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x3. cinv = Revoke x3 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x41 x42 x43. cinv = Move x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. cinv = CancelBadgedSends x5 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x3. cinv = Revoke x3 \<Longrightarrow> \<lbrace>?Q40 x3\<rbrace> cteRevoke x3 \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x3 s. \<lbrakk>cinv = Revoke x3; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> cte_wp_at' (\<lambda>_. True) x3 s\<rbrakk> \<Longrightarrow> ?Q40 x3 s
 3. \<And>x41 x42 x43. cinv = Move x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x5. cinv = CancelBadgedSends x5 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x3. cinv = Revoke x3 \<Longrightarrow> \<lbrace>?Q40 x3\<rbrace> cteRevoke x3 \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x3 s. \<lbrakk>cinv = Revoke x3; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> cte_wp_at' (\<lambda>_. True) x3 s\<rbrakk> \<Longrightarrow> ?Q40 x3 s
 3. \<And>x41 x42 x43. cinv = Move x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x5. cinv = CancelBadgedSends x5 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x3 rv s. \<lbrakk>cinv = Revoke x3; invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 2. \<And>x3 s. \<lbrakk>cinv = Revoke x3; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> cte_wp_at' (\<lambda>_. True) x3 s\<rbrakk> \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s
 3. \<And>x41 x42 x43. cinv = Move x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x5. cinv = CancelBadgedSends x5 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x3 s. \<lbrakk>cinv = Revoke x3; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> cte_wp_at' (\<lambda>_. True) x3 s\<rbrakk> \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s
 2. \<And>x41 x42 x43. cinv = Move x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x5. cinv = CancelBadgedSends x5 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x41 x42 x43. cinv = Move x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. cinv = CancelBadgedSends x5 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x5. cinv = CancelBadgedSends x5 \<Longrightarrow> \<lbrace>?Q60 x5\<rbrace> case x5 of capability.EndpointCap ptr b x xa xb xc \<Rightarrow> withoutPreemption $ unless (b = 0) $ cancelBadgedSends ptr b | _ \<Rightarrow> haskell_fail [] \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5 s. \<lbrakk>cinv = CancelBadgedSends x5; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cap' x5 s \<and> hasCancelSendRights x5\<rbrakk> \<Longrightarrow> ?Q60 x5 s
 3. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x5. cinv = CancelBadgedSends x5 \<Longrightarrow> \<lbrace>?Q63 x5\<rbrace> case x5 of capability.EndpointCap ptr b x xa xb xc \<Rightarrow> withoutPreemption $ unless (b = 0) $ cancelBadgedSends ptr b | _ \<Rightarrow> haskell_fail [] \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5 s. \<lbrakk>cinv = CancelBadgedSends x5; ?Q60 x5 s\<rbrakk> \<Longrightarrow> ?Q63 x5 s
 3. \<And>x5 s. \<lbrakk>cinv = CancelBadgedSends x5; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cap' x5 s \<and> hasCancelSendRights x5\<rbrakk> \<Longrightarrow> ?Q60 x5 s
 4. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>?Q227 x6\<rbrace> invokeCNode (SaveCaller x6) \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x6 s. \<lbrakk>cinv = SaveCaller x6; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrakk> \<Longrightarrow> ?Q227 x6 s
 3. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x6. cinv = SaveCaller x6 \<Longrightarrow> \<lbrace>?Q227 x6\<rbrace> do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot x6 | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x6 s. \<lbrakk>cinv = SaveCaller x6; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrakk> \<Longrightarrow> ?Q227 x6 s
 3. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrace> invokeCNode cinv \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>?Q418 x7\<rbrace> invokeCNode (Delete x7) \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x7 s. \<lbrakk>cinv = Delete x7; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrakk> \<Longrightarrow> ?Q418 x7 s proof (prove)
goal (2 subgoals):
 1. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>?Q418 x7\<rbrace> doE (success, info) <- finaliseSlot x7 True;
whenE True (liftE (emptySlot x7 info))
odE \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x7 s. \<lbrakk>cinv = Delete x7; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrakk> \<Longrightarrow> ?Q418 x7 s proof (prove)
goal (2 subgoals):
 1. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>?Q418 x7\<rbrace> finaliseSlot x7 True \<lbrace>\<lambda>x s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x7 s. \<lbrakk>cinv = Delete x7; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrakk> \<Longrightarrow> ?Q418 x7 s proof (prove)
goal (2 subgoals):
 1. \<And>x7. cinv = Delete x7 \<Longrightarrow> \<lbrace>?Q418 x7\<rbrace> finaliseSlot x7 True \<lbrace>\<lambda>x s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x7 s. \<lbrakk>cinv = Delete x7; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrakk> \<Longrightarrow> ?Q418 x7 s proof (prove)
goal (2 subgoals):
 1. \<And>x7 rv s. \<lbrakk>cinv = Delete x7; invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 2. \<And>x7 s. \<lbrakk>cinv = Delete x7; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrakk> \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x7 s) proof (prove)
goal (1 subgoal):
 1. \<And>x7 s. \<lbrakk>cinv = Delete x7; invs' s \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> valid_cnode_inv' cinv s\<rbrakk> \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x7 s) proof (prove)
goal:
No subgoals!