theory Retype_R

lemma retype_region2_extra_ext_mapM_x_corres:
  shows "corres dc
           (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s))
           (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at' addr s)
           (retype_region2_extra_ext addrs Structures_A.apiobject_type.TCBObject)
           (mapM_x (\<lambda>addr. do cdom \<leftarrow> curDomain;
                              threadSet (tcbDomain_update (\<lambda>_. cdom)) addr
                           od)
             addrs)" apply (rule corres_guard_imp) apply (simp add: retype_region2_extra_ext_def curDomain_mapM_x_futz[symmetric] when_def) apply (rule corres_split_eqr[OF gcd_corres]) apply (rule_tac S="Id \<inter> {(x, y). x \<in> set addrs}"
                  and P="\<lambda>s. (\<forall>t \<in> set addrs. tcb_at t s) \<and> valid_etcbs s"
                  and P'="\<lambda>s. \<forall>t \<in> set addrs. tcb_at' t s"
                   in corres_mapM_x) apply simp apply (rule corres_guard_imp) apply (rule ethread_set_corres, simp_all add: etcb_relation_def non_exst_same_def)[1] apply (case_tac tcb') apply simp apply fastforce apply fastforce apply (wp hoare_vcg_ball_lift | simp)+ apply auto[1] apply (wp | simp add: curDomain_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at' addr s) (retype_region2_extra_ext addrs Structures_A.apiobject_type.TCBObject) (mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. cdom)) addr
od) addrs) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (retype_region2_extra_ext addrs Structures_A.apiobject_type.TCBObject) (mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. cdom)) addr
od) addrs)
 2. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ?Q s
 3. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) addrs
od) (do cdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. cdom))) addrs
od)
 2. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ?Q s
 3. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>cdom. corres dc (?R4 cdom) (?R'4 cdom) (mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) addrs) (mapM_x (threadSet (tcbDomain_update (\<lambda>_. cdom))) addrs)
 2. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>?R'4\<rbrace>
 4. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> corres dc (\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s) (\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s) (ethread_set (tcb_domain_update (\<lambda>_. cdom)) x) (threadSet (tcbDomain_update (\<lambda>_. cdom)) y)
 2. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. cdom)) x \<lbrace>\<lambda>rv s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 3. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. cdom)) y \<lbrace>\<lambda>rv s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 4. \<And>cdom. length addrs = length addrs
 5. \<And>cdom. set (zip addrs addrs) \<subseteq> Id \<inter> {(x, y). x \<in> set addrs}
 6. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 8. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>cdom x. x \<in> set addrs \<Longrightarrow> corres dc (\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s) (\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s) (ethread_set (tcb_domain_update (\<lambda>_. cdom)) x) (threadSet (tcbDomain_update (\<lambda>_. cdom)) x)
 2. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. cdom)) x \<lbrace>\<lambda>rv s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 3. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. cdom)) y \<lbrace>\<lambda>rv s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 4. \<And>cdom. length addrs = length addrs
 5. \<And>cdom. set (zip addrs addrs) \<subseteq> Id \<inter> {(x, y). x \<in> set addrs}
 6. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 8. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (11 subgoals):
 1. \<And>cdom x. x \<in> set addrs \<Longrightarrow> corres dc (?Q9 cdom x) (?Q'9 cdom x) (ethread_set (tcb_domain_update (\<lambda>_. cdom)) x) (threadSet (tcbDomain_update (\<lambda>_. cdom)) x)
 2. \<And>cdom x s. \<lbrakk>x \<in> set addrs; (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ?Q9 cdom x s
 3. \<And>cdom x s. \<lbrakk>x \<in> set addrs; \<forall>t\<in>set addrs. tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q'9 cdom x s
 4. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. cdom)) x \<lbrace>\<lambda>rv s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 5. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. cdom)) y \<lbrace>\<lambda>rv s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 6. \<And>cdom. length addrs = length addrs
 7. \<And>cdom. set (zip addrs addrs) \<subseteq> Id \<inter> {(x, y). x \<in> set addrs}
 8. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 10. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cdom x tcb'. x \<in> set addrs \<Longrightarrow> \<exists>d p ts. tcbDomain_update (\<lambda>_. cdom) tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) tcb'))
 2. \<And>cdom x s. \<lbrakk>x \<in> set addrs; (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at x and valid_etcbs) s
 3. \<And>cdom x s. \<lbrakk>x \<in> set addrs; \<forall>t\<in>set addrs. tcb_at' t s\<rbrakk> \<Longrightarrow> tcb_at' x s
 4. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. cdom)) x \<lbrace>\<lambda>rv s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 5. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. cdom)) y \<lbrace>\<lambda>rv s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 6. \<And>cdom. length addrs = length addrs
 7. \<And>cdom. set (zip addrs addrs) \<subseteq> Id \<inter> {(x, y). x \<in> set addrs}
 8. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 10. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cdom x tcb' x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>x \<in> set addrs; tcb' = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<exists>d p ts. tcbDomain_update (\<lambda>_. cdom) tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) tcb'))
 2. \<And>cdom x s. \<lbrakk>x \<in> set addrs; (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at x and valid_etcbs) s
 3. \<And>cdom x s. \<lbrakk>x \<in> set addrs; \<forall>t\<in>set addrs. tcb_at' t s\<rbrakk> \<Longrightarrow> tcb_at' x s
 4. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. cdom)) x \<lbrace>\<lambda>rv s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 5. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. cdom)) y \<lbrace>\<lambda>rv s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 6. \<And>cdom. length addrs = length addrs
 7. \<And>cdom. set (zip addrs addrs) \<subseteq> Id \<inter> {(x, y). x \<in> set addrs}
 8. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 10. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>cdom x s. \<lbrakk>x \<in> set addrs; (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at x and valid_etcbs) s
 2. \<And>cdom x s. \<lbrakk>x \<in> set addrs; \<forall>t\<in>set addrs. tcb_at' t s\<rbrakk> \<Longrightarrow> tcb_at' x s
 3. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. cdom)) x \<lbrace>\<lambda>rv s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 4. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. cdom)) y \<lbrace>\<lambda>rv s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 5. \<And>cdom. length addrs = length addrs
 6. \<And>cdom. set (zip addrs addrs) \<subseteq> Id \<inter> {(x, y). x \<in> set addrs}
 7. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 9. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>cdom x s. \<lbrakk>x \<in> set addrs; \<forall>t\<in>set addrs. tcb_at' t s\<rbrakk> \<Longrightarrow> tcb_at' x s
 2. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. cdom)) x \<lbrace>\<lambda>rv s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 3. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. cdom)) y \<lbrace>\<lambda>rv s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 4. \<And>cdom. length addrs = length addrs
 5. \<And>cdom. set (zip addrs addrs) \<subseteq> Id \<inter> {(x, y). x \<in> set addrs}
 6. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 8. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. cdom)) x \<lbrace>\<lambda>rv s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 2. \<And>cdom x y. (x, y) \<in> Id \<inter> {(x, y). x \<in> set addrs} \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. cdom)) y \<lbrace>\<lambda>rv s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 3. \<And>cdom. length addrs = length addrs
 4. \<And>cdom. set (zip addrs addrs) \<subseteq> Id \<inter> {(x, y). x \<in> set addrs}
 5. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 7. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. set (zip addrs addrs) \<subseteq> Id \<and> set (zip addrs addrs) \<subseteq> {(x, y). x \<in> set addrs}
 2. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 4. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>cdom s. (\<forall>t\<in>set addrs. tcb_at t s) \<and> valid_etcbs s\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> curDomain \<lbrace>\<lambda>cdom s. \<forall>t\<in>set addrs. tcb_at' t s\<rbrace>
 3. \<And>s. (valid_etcbs and (\<lambda>s. \<forall>addr\<in>set addrs. tcb_at addr s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. \<forall>addr\<in>set addrs. tcb_at' addr s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal:
No subgoals!