theory Prefix_Refinement

lemma prefix_refinement_mapM:
  "list_all2 xyr xs ys
    \<Longrightarrow> (\<forall>x y. x \<in> set xs \<longrightarrow> y \<in> set ys \<longrightarrow> xyr x y
        \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))
    \<Longrightarrow> (\<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>AR\<rbrace> f x \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>)
    \<Longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> g y \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>)
    \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys)" apply (induct xs ys rule: list_all2_induct) apply (simp add: mapM_def sequence_def prefix_refinement_return_imp) apply (clarsimp simp add: mapM_Cons all_conj_distrib imp_conjR) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind, assumption) apply (rule prefix_refinement_bind, assumption) apply (rule prefix_refinement_triv_pre, rule prefix_refinement_return_imp, simp) apply (wp validI_triv)+ apply (blast intro: validI_prefix_closed) apply (wp validI_triv | simp add: pred_conj_def
        | blast dest: validI_prefix_closed)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 xyr xs ys; \<forall>x y. x \<in> set xs \<longrightarrow> y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x y. x \<in> set [] \<longrightarrow> y \<in> set [] \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set [] \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>y. y \<in> set [] \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f []) (mapM g [])
 2. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; \<lbrakk>\<forall>x y. x \<in> set xs \<longrightarrow> y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); \<forall>xa ya. xa \<in> set (x # xs) \<longrightarrow> ya \<in> set (y # ys) \<longrightarrow> xyr xa ya \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f xa) (g ya); \<forall>xa. xa \<in> set (x # xs) \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f xa -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>ya. ya \<in> set (y # ys) \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g ya -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f (x # xs)) (mapM g (y # ys)) proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; \<lbrakk>\<forall>x y. x \<in> set xs \<longrightarrow> y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); \<forall>xa ya. xa \<in> set (x # xs) \<longrightarrow> ya \<in> set (y # ys) \<longrightarrow> xyr xa ya \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f xa) (g ya); \<forall>xa. xa \<in> set (x # xs) \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f xa -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>ya. ya \<in> set (y # ys) \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g ya -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f (x # xs)) (mapM g (y # ys)) proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (do y <- f x;
ys <- mapM f xs;
return (y # ys)
od) (do y <- g y;
ys <- mapM g ys;
return (y # ys)
od) proof (prove)
goal (3 subgoals):
 1. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) (?P'18 x xs y ys) (?Q'18 x xs y ys) AR R (do y <- f x;
ys <- mapM f xs;
return (y # ys)
od) (do y <- g y;
ys <- mapM g ys;
return (y # ys)
od)
 2. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ?P'18 x xs y ys s0 s
 3. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. intsr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ?Q'18 x xs y ys t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x xs y ys xa ya. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)); rvr xa ya\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) (?P''22 x xs y ys xa) (?Q''22 x xs y ys ya) AR R (do ys <- mapM f xs;
return (xa # ys)
od) (do ys <- mapM g ys;
return (ya # ys)
od)
 2. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 x xs y ys\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>?P''22 x xs y ys\<rbrace>
 3. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x xs y ys\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>?Q''22 x xs y ys\<rbrace>
 4. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> (P and ?P'22 x xs y ys) s0 s
 5. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. intsr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> (Q and ?Q'22 x xs y ys) t0 t proof (prove)
goal (7 subgoals):
 1. \<And>x xs y ys xa ya xb yb. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)); rvr xa ya; list_all2 rvr xb yb\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr intsr (list_all2 rvr) (?P''27 x xs y ys xa ya xb) (?Q''27 x xs y ys xa ya yb) AR R (return (xa # xb)) (return (ya # yb))
 2. \<And>x xs y ys xa ya. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)); rvr xa ya\<rbrakk> \<Longrightarrow> \<lbrace>?P'29 x xs y ys xa\<rbrace>, \<lbrace>AR\<rbrace> mapM f xs -, \<lbrace>?P''27 x xs y ys xa ya\<rbrace>
 3. \<And>x xs y ys xa ya. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)); rvr xa ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 x xs y ys ya\<rbrace>, \<lbrace>R\<rbrace> mapM g ys -, \<lbrace>?Q''27 x xs y ys xa ya\<rbrace>
 4. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 x xs y ys\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>xa. P and ?P'29 x xs y ys xa\<rbrace>
 5. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x xs y ys\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>ya. Q and ?Q'31 x xs y ys ya\<rbrace>
 6. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> (P and ?P'22 x xs y ys) s0 s
 7. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. intsr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> (Q and ?Q'22 x xs y ys) t0 t proof (prove)
goal (6 subgoals):
 1. \<And>x xs y ys xa ya. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)); rvr xa ya\<rbrakk> \<Longrightarrow> \<lbrace>?P'29 x xs y ys xa\<rbrace>, \<lbrace>AR\<rbrace> mapM f xs -, \<lbrace>\<lambda>xb _ _. True\<rbrace>
 2. \<And>x xs y ys xa ya. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)); rvr xa ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 x xs y ys ya\<rbrace>, \<lbrace>R\<rbrace> mapM g ys -, \<lbrace>\<lambda>yb _ _. True\<rbrace>
 3. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 x xs y ys\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>xa. P and ?P'29 x xs y ys xa\<rbrace>
 4. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x xs y ys\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>ya. Q and ?Q'31 x xs y ys ya\<rbrace>
 5. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> (P and ?P'22 x xs y ys) s0 s
 6. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. intsr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> (Q and ?Q'22 x xs y ys) t0 t proof (prove)
goal (6 subgoals):
 1. \<And>x xs y ys xa ya xb. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)); rvr xa ya; xb \<in> set xs\<rbrakk> \<Longrightarrow> prefix_closed (f xb)
 2. \<And>x xs y ys xa ya. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)); rvr xa ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 x xs y ys ya\<rbrace>, \<lbrace>R\<rbrace> mapM g ys -, \<lbrace>\<lambda>yb _ _. True\<rbrace>
 3. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 x xs y ys\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>xa. P and (\<lambda>_ _. True)\<rbrace>
 4. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x xs y ys\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>ya. Q and ?Q'31 x xs y ys ya\<rbrace>
 5. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> (P and ?P'22 x xs y ys) s0 s
 6. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. intsr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> (Q and ?Q'22 x xs y ys) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x xs y ys xa ya. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)); rvr xa ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 x xs y ys ya\<rbrace>, \<lbrace>R\<rbrace> mapM g ys -, \<lbrace>\<lambda>yb _ _. True\<rbrace>
 2. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 x xs y ys\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>xa. P and (\<lambda>_ _. True)\<rbrace>
 3. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x xs y ys\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>ya. Q and ?Q'31 x xs y ys ya\<rbrace>
 4. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> (P and ?P'22 x xs y ys) s0 s
 5. \<And>x xs y ys. \<lbrakk>xyr x y; list_all2 xyr xs ys; prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys); prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f x -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>y. y \<in> set ys \<longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g y -, \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x. x \<in> set xs \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y); \<forall>x. x \<in> set xs \<longrightarrow> (\<forall>y. y \<in> set ys \<longrightarrow> xyr x y \<longrightarrow> prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y))\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. intsr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> (Q and ?Q'22 x xs y ys) t0 t proof (prove)
goal:
No subgoals!