theory Refine

lemma kernel_corres:
  "corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
              (\<lambda>s. scheduler_action s = resume_cur_thread) and
              (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s))
             (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
              (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
              (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
             (call_kernel event) (callKernel event)" unfolding callKernel_def K_bind_def apply (rule corres_cross_over_fastpathKernelAssertions, blast+) apply (rule corres_stateAssert_r) apply (rule corres_guard_imp) apply (rule corres_add_noop_lhs2) apply (simp only: bind_assoc[symmetric]) apply (rule corres_split[where r'=dc and
                                   R="\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s" and
                                   R'="\<lambda>_. \<top>"]) apply (simp only: bind_assoc) apply (rule kernel_corres') apply (rule corres_bind_return2, rule corres_stateAssert_assume_stronger) apply simp apply (simp add: kernelExitAssertions_def state_relation_def) apply (wp call_kernel_domain_time_inv_det_ext call_kernel_domain_list_inv_det_ext) apply wp apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (call_kernel event) (callKernel event) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (call_kernel event) (do y <- stateAssert fastpathKernelAssertions [];
y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and fastpathKernelAssertions) (call_kernel event) (do y <- stateAssert fastpathKernelAssertions [];
y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (call_kernel event) (do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q20 ?Q'20 (call_kernel event) (do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od)
 2. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> ?Q20 s
 3. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ?Q'20 s proof (prove)
goal (3 subgoals):
 1. corres dc ?Q20 ?Q'20 (do _ <- call_kernel event;
return ()
od) (do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od)
 2. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> ?Q20 s
 3. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ?Q'20 s proof (prove)
goal (3 subgoals):
 1. corres dc ?Q20 ?Q'20 (do _ <- call_kernel event;
return ()
od) (do y <- do y <- do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule
od;
activateThread
od;
stateAssert kernelExitAssertions []
od)
 2. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> ?Q20 s
 3. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ?Q'20 s proof (prove)
goal (6 subgoals):
 1. corres dc ?P26 ?P'26 (call_kernel event) (do y <- do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule
od;
activateThread
od)
 2. \<And>uu_ y. dc uu_ y \<Longrightarrow> corres dc (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) (\<lambda>_. True) (return ()) (stateAssert kernelExitAssertions [])
 3. \<lbrace>?Q26\<rbrace> call_kernel event \<lbrace>\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 4. \<lbrace>?Q'26\<rbrace> do y <- do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule
od;
activateThread
od \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> (?P26 and ?Q26) s
 6. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (?P'26 and ?Q'26) s proof (prove)
goal (6 subgoals):
 1. corres dc ?P26 ?P'26 (call_kernel event) (do x <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
y <- ThreadDecls_H.schedule;
activateThread
od)
 2. \<And>uu_ y. dc uu_ y \<Longrightarrow> corres dc (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) (\<lambda>_. True) (return ()) (stateAssert kernelExitAssertions [])
 3. \<lbrace>?Q26\<rbrace> call_kernel event \<lbrace>\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 4. \<lbrace>?Q'26\<rbrace> do y <- do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule
od;
activateThread
od \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> (?P26 and ?Q26) s
 6. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (?P'26 and ?Q'26) s proof (prove)
goal (5 subgoals):
 1. \<And>uu_ y. dc uu_ y \<Longrightarrow> corres dc (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) (\<lambda>_. True) (return ()) (stateAssert kernelExitAssertions [])
 2. \<lbrace>?Q26\<rbrace> call_kernel event \<lbrace>\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 3. \<lbrace>?Q'26\<rbrace> do y <- do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule
od;
activateThread
od \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q26) s
 5. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'26) s proof (prove)
goal (6 subgoals):
 1. \<And>uu_ y. dc uu_ y \<Longrightarrow> corres dc (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) (\<lambda>_. True) (return ()) (return ())
 2. \<And>uu_ y s s'. \<lbrakk>dc uu_ y; (s, s') \<in> state_relation; 0 < domain_time s \<and> valid_domain_list s; True\<rbrakk> \<Longrightarrow> kernelExitAssertions s'
 3. \<lbrace>?Q26\<rbrace> call_kernel event \<lbrace>\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 4. \<lbrace>?Q'26\<rbrace> do y <- do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule
od;
activateThread
od \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q26) s
 6. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'26) s proof (prove)
goal (5 subgoals):
 1. \<And>uu_ y s s'. \<lbrakk>dc uu_ y; (s, s') \<in> state_relation; 0 < domain_time s \<and> valid_domain_list s; True\<rbrakk> \<Longrightarrow> kernelExitAssertions s'
 2. \<lbrace>?Q26\<rbrace> call_kernel event \<lbrace>\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 3. \<lbrace>?Q'26\<rbrace> do y <- do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule
od;
activateThread
od \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q26) s
 5. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'26) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q26\<rbrace> call_kernel event \<lbrace>\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 2. \<lbrace>?Q'26\<rbrace> do y <- do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule
od;
activateThread
od \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q26) s
 4. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'26) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'26\<rbrace> do y <- do y <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule
od;
activateThread
od \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. ((\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)) s \<and> valid_domain_list s)) s
 3. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'26) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. ((\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)) s \<and> valid_domain_list s)) s
 2. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!