theory VSpaceEntries_AI

lemma mapME_x_accumulate_checks:
  assumes P:  "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>"
  and Q : "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>"
  and P': "\<And>x y. y \<noteq> x  \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>"
  and distinct: "distinct xs"
  shows       "\<lbrace>Q \<rbrace> mapME_x f xs \<lbrace>\<lambda>rv s. \<forall>x \<in> set xs. P x s\<rbrace>, \<lbrace>E\<rbrace>" using assms proof (induct xs) case Nil show ?case by (simp add: mapME_x_Nil, wp) next case (Cons y ys) show ?case apply (simp add: mapME_x_Cons) apply wp apply (rule hoare_vcg_conj_liftE_weaker) apply (wp mapME_x_wp' P P'
          hoare_vcg_const_Ball_liftE
          | simp add:Q
          | rule hoare_post_impErr[OF P])+ using Cons.prems apply fastforce apply (wp Cons.hyps) apply (rule Cons.prems,simp) apply (wp Cons.prems(2);simp) apply (wp Cons.prems(3);simp) using Cons.prems apply fastforce apply (rule hoare_pre) apply (rule hoare_vcg_conj_liftE_weaker) apply (wp Cons.prems| simp)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?x\<rbrace>, \<lbrace>E\<rbrace>
?x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>
?y \<noteq> ?x \<Longrightarrow> \<lbrace>P ?y\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?y\<rbrace>, \<lbrace>E\<rbrace>
distinct xs

goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>, \<lbrace>E\<rbrace> proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. x \<in> set [] \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set [] \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct []\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f [] \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. P x s\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct xs\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv s. \<forall>x\<in>set (a # xs). P x s\<rbrace>, \<lbrace>E\<rbrace> proof (state)
this:
?x \<in> set [] \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?x\<rbrace>, \<lbrace>E\<rbrace>
?x \<in> set [] \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>
?y \<noteq> ?x \<Longrightarrow> \<lbrace>P ?y\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?y\<rbrace>, \<lbrace>E\<rbrace>
distinct []

goal (2 subgoals):
 1. \<lbrakk>\<And>x. x \<in> set [] \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set [] \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct []\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f [] \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. P x s\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct xs\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv s. \<forall>x\<in>set (a # xs). P x s\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> mapME_x f [] \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. P x s\<rbrace>, \<lbrace>E\<rbrace> proof (state)
this:
\<lbrace>Q\<rbrace> mapME_x f [] \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. P x s\<rbrace>, \<lbrace>E\<rbrace>

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct xs\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv s. \<forall>x\<in>set (a # xs). P x s\<rbrace>, \<lbrace>E\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct xs\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv s. \<forall>x\<in>set (a # xs). P x s\<rbrace>, \<lbrace>E\<rbrace> proof (state)
this:
\<lbrakk>\<And>x. x \<in> set ys \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set ys \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct ys\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. P x s\<rbrace>, \<lbrace>E\<rbrace>
?x \<in> set (y # ys) \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?x\<rbrace>, \<lbrace>E\<rbrace>
?x \<in> set (y # ys) \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>
?y \<noteq> ?x \<Longrightarrow> \<lbrace>P ?y\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?y\<rbrace>, \<lbrace>E\<rbrace>
distinct (y # ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct xs\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>Q\<rbrace> f x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>y x. y \<noteq> x \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv s. \<forall>x\<in>set (a # xs). P x s\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> mapME_x f (y # ys) \<lbrace>\<lambda>rv s. \<forall>x\<in>set (y # ys). P x s\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> doE y <- f y;
mapME_x f ys
odE \<lbrace>\<lambda>rv s. P y s \<and> (\<forall>x\<in>set ys. P x s)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B10 x\<rbrace> mapME_x f ys \<lbrace>\<lambda>rv s. P y s \<and> (\<forall>x\<in>set ys. P x s)\<rbrace>, \<lbrace>E\<rbrace>
 2. \<lbrace>?Q9\<rbrace> f y \<lbrace>?B10\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?P11 x\<rbrace> mapME_x f ys \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>x. \<lbrace>?P'11 x\<rbrace> mapME_x f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. P x s\<rbrace>, \<lbrace>E\<rbrace>
 3. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. ?P11 x s \<and> ?P'11 x s\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>xa. xa \<in> set ys \<Longrightarrow> y \<noteq> xa
 2. \<And>x. \<lbrace>?P'11 x\<rbrace> mapME_x f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. P x s\<rbrace>, \<lbrace>E\<rbrace>
 3. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> ?P'11 x s\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
using this:
?x \<in> set (y # ys) \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?x\<rbrace>, \<lbrace>E\<rbrace>
?x \<in> set (y # ys) \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>
?y \<noteq> ?x \<Longrightarrow> \<lbrace>P ?y\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?y\<rbrace>, \<lbrace>E\<rbrace>
distinct (y # ys)

goal (4 subgoals):
 1. \<And>xa. xa \<in> set ys \<Longrightarrow> y \<noteq> xa
 2. \<And>x. \<lbrace>?P'11 x\<rbrace> mapME_x f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. P x s\<rbrace>, \<lbrace>E\<rbrace>
 3. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> ?P'11 x s\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?P'11 x\<rbrace> mapME_x f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. P x s\<rbrace>, \<lbrace>E\<rbrace>
 2. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> ?P'11 x s\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (6 subgoals):
 1. \<And>x xa. xa \<in> set ys \<Longrightarrow> \<lbrace>Q\<rbrace> f xa \<lbrace>\<lambda>rv. P xa\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>x xa. xa \<in> set ys \<Longrightarrow> \<lbrace>Q\<rbrace> f xa \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>x y xa. y \<noteq> xa \<Longrightarrow> \<lbrace>P y\<rbrace> f xa \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>x. distinct ys
 5. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> Q s\<rbrace>, \<lbrace>E\<rbrace>
 6. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (5 subgoals):
 1. \<And>x xa. xa \<in> set ys \<Longrightarrow> \<lbrace>Q\<rbrace> f xa \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>x y xa. y \<noteq> xa \<Longrightarrow> \<lbrace>P y\<rbrace> f xa \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>x. distinct ys
 4. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> Q s\<rbrace>, \<lbrace>E\<rbrace>
 5. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>x y xa. y \<noteq> xa \<Longrightarrow> \<lbrace>P y\<rbrace> f xa \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>x. distinct ys
 3. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> Q s\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. \<And>x. distinct ys
 2. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> Q s\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
using this:
?x \<in> set (y # ys) \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?x\<rbrace>, \<lbrace>E\<rbrace>
?x \<in> set (y # ys) \<Longrightarrow> \<lbrace>Q\<rbrace> f ?x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>
?y \<noteq> ?x \<Longrightarrow> \<lbrace>P ?y\<rbrace> f ?x \<lbrace>\<lambda>rv. P ?y\<rbrace>, \<lbrace>E\<rbrace>
distinct (y # ys)

goal (3 subgoals):
 1. \<And>x. distinct ys
 2. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> Q s\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> Q s\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q54\<rbrace> f y \<lbrace>\<lambda>x s. P y s \<and> Q s\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s. ?Q9 s \<Longrightarrow> ?Q54 s
 3. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P57\<rbrace> f y \<lbrace>\<lambda>rv. P y\<rbrace>, \<lbrace>E\<rbrace>
 2. \<lbrace>?P'57\<rbrace> f y \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s. ?Q9 s \<Longrightarrow> ?P57 s \<and> ?P'57 s
 4. \<And>s. Q s \<Longrightarrow> ?Q9 s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>Q\<rbrace> mapME_x f (y # ys) \<lbrace>\<lambda>rv s. \<forall>x\<in>set (y # ys). P x s\<rbrace>, \<lbrace>E\<rbrace>

goal:
No subgoals!