theory Hoare_Sep_Tactics

lemma sep_hoare_fold_mapM_x:
  "(\<And>R x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>)
    \<Longrightarrow> \<lbrace>\<lambda>s. (sep_fold P Q R xs) (sep_lift s)\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>" apply (clarsimp simp: sep_fold_def) apply (induct xs arbitrary: R) apply (clarsimp simp: mapM_x_def sequence_x_def)+ apply wp apply assumption+ apply atomize apply (erule allE) apply (erule allE) apply (erule_tac x=a in allE) apply clarsimp apply (rule hoare_chain) apply assumption+ apply (sep_erule (direct) sep_mp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>R x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs (sep_lift s)\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>R x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>R. (\<And>R x. x \<in> set [] \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) [] R (sep_lift s)\<rbrace> mapM_x f [] \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>
 2. \<And>a xs R. \<lbrakk>\<And>R. (\<And>R x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) (a # xs) R (sep_lift s)\<rbrace> mapM_x f (a # xs) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs R. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrace> do _ <- f a;
foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())
od \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a xs R uu_. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?B3 a xs R uu_\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>
 2. \<And>a xs R. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 a xs R\<rbrace> f a \<lbrace>?B3 a xs R\<rbrace>
 3. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?Q2 a xs R s proof (prove)
goal (2 subgoals):
 1. \<And>a xs R. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 a xs R\<rbrace> f a \<lbrace>\<lambda>_ s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace>
 2. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?Q2 a xs R s proof (prove)
goal (2 subgoals):
 1. \<And>a xs R. \<lbrakk>\<forall>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<forall>R x. x = a \<or> x \<in> set xs \<longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 a xs R\<rbrace> f a \<lbrace>\<lambda>_ s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace>
 2. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?Q2 a xs R s proof (prove)
goal (2 subgoals):
 1. \<And>a xs R. \<lbrakk>\<forall>R x. x = a \<or> x \<in> set xs \<longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (?x15 a xs R) (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. ?x15 a xs R (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 a xs R\<rbrace> f a \<lbrace>\<lambda>_ s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace>
 2. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?Q2 a xs R s proof (prove)
goal (2 subgoals):
 1. \<And>a xs R. \<lbrakk>\<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (?x15 a xs R) (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. ?x15 a xs R (sep_lift s)\<rbrace>; \<forall>x. x = a \<or> x \<in> set xs \<longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* ?x17 a xs R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* ?x17 a xs R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 a xs R\<rbrace> f a \<lbrace>\<lambda>_ s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace>
 2. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?Q2 a xs R s proof (prove)
goal (2 subgoals):
 1. \<And>a xs R. \<lbrakk>\<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (?x15 a xs R) (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. ?x15 a xs R (sep_lift s)\<rbrace>; a = a \<or> a \<in> set xs \<longrightarrow> \<lbrace>\<lambda>s. (P a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace> f a \<lbrace>\<lambda>_ s. (Q a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 a xs R\<rbrace> f a \<lbrace>\<lambda>_ s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace>
 2. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?Q2 a xs R s proof (prove)
goal (2 subgoals):
 1. \<And>a xs R. \<lbrakk>\<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (?x15 a xs R) (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. ?x15 a xs R (sep_lift s)\<rbrace>; \<lbrace>\<lambda>s. (P a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace> f a \<lbrace>\<lambda>_ s. (Q a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 a xs R\<rbrace> f a \<lbrace>\<lambda>_ s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace>
 2. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?Q2 a xs R s proof (prove)
goal (4 subgoals):
 1. \<And>a xs R. \<lbrakk>\<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (?x15 a xs R) (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. ?x15 a xs R (sep_lift s)\<rbrace>; \<lbrace>\<lambda>s. (P a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace> f a \<lbrace>\<lambda>_ s. (Q a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P23 a xs R\<rbrace> f a \<lbrace>?Q23 a xs R\<rbrace>
 2. \<And>a xs R s. \<lbrakk>\<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (?x15 a xs R) (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. ?x15 a xs R (sep_lift s)\<rbrace>; \<lbrace>\<lambda>s. (P a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace> f a \<lbrace>\<lambda>_ s. (Q a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace>; ?Q2 a xs R s\<rbrakk> \<Longrightarrow> ?P23 a xs R s
 3. \<And>a xs R rv s. \<lbrakk>\<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (?x15 a xs R) (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. ?x15 a xs R (sep_lift s)\<rbrace>; \<lbrace>\<lambda>s. (P a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace> f a \<lbrace>\<lambda>_ s. (Q a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace>; ?Q23 a xs R rv s\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)
 4. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?Q2 a xs R s proof (prove)
goal (2 subgoals):
 1. \<And>a xs R rv s. \<lbrakk>\<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (?x15 a xs R) (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. ?x15 a xs R (sep_lift s)\<rbrace>; \<lbrace>\<lambda>s. (P a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace> f a \<lbrace>\<lambda>_ s. (Q a \<and>* ?x17 a xs R) (sep_lift s)\<rbrace>; (Q a \<and>* ?x17 a xs R) (sep_lift s)\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)
 2. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> (P a \<and>* ?x17 a xs R) (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>a xs R s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R (sep_lift s)\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ()) \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>; \<And>R x. x = a \<or> x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P x \<and>* R) (sep_lift s)\<rbrace> f x \<lbrace>\<lambda>_ s. (Q x \<and>* R) (sep_lift s)\<rbrace>; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s)\<rbrakk> \<Longrightarrow> (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) (sep_lift s) proof (prove)
goal:
No subgoals!