theory Untyped_R

lemma corres_list_all2_mapM_':
  assumes w: "suffix xs oxs" "suffix ys oys"
  assumes y: "\<And>x xs y ys. \<lbrakk> F x y; suffix (x # xs) oxs; suffix (y # ys) oys \<rbrakk>
               \<Longrightarrow> corres dc (P (x # xs)) (P' (y # ys)) (f x) (g y)"
  assumes z: "\<And>x y xs. \<lbrakk> F x y; suffix (x # xs) oxs \<rbrakk> \<Longrightarrow> \<lbrace>P (x # xs)\<rbrace> f x \<lbrace>\<lambda>rv. P xs\<rbrace>"
             "\<And>x y ys. \<lbrakk> F x y; suffix (y # ys) oys \<rbrakk> \<Longrightarrow> \<lbrace>P' (y # ys)\<rbrace> g y \<lbrace>\<lambda>rv. P' ys\<rbrace>"
  assumes x: "list_all2 F xs ys"
  shows "corres dc (P xs) (P' ys) (mapM_x f xs) (mapM_x g ys)" apply (insert x w) apply (induct xs arbitrary: ys) apply (simp add: mapM_x_def sequence_x_def) apply (case_tac ys) apply simp apply (clarsimp simp add: mapM_x_def sequence_x_def) apply (rule corres_guard_imp) apply (rule corres_split[OF y]) apply assumption apply assumption apply assumption apply (clarsimp dest!: suffix_ConsD) apply (erule meta_allE, (drule(1) meta_mp)+) apply assumption apply (erule(1) z)+ apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (P xs) (P' ys) (mapM_x f xs) (mapM_x g ys) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (mapM_x f xs) (mapM_x g ys) proof (prove)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>list_all2 F [] ys; suffix [] oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P []) (P' ys) (mapM_x f []) (mapM_x g ys)
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (mapM_x f xs) (mapM_x g ys); list_all2 F (a # xs) ys; suffix (a # xs) oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P (a # xs)) (P' ys) (mapM_x f (a # xs)) (mapM_x g ys) proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (mapM_x f xs) (mapM_x g ys); list_all2 F (a # xs) ys; suffix (a # xs) oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P (a # xs)) (P' ys) (mapM_x f (a # xs)) (mapM_x g ys) proof (prove)
goal (2 subgoals):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (mapM_x f xs) (mapM_x g ys); list_all2 F (a # xs) ys; suffix (a # xs) oxs; suffix ys oys; ys = []\<rbrakk> \<Longrightarrow> corres dc (P (a # xs)) (P' ys) (mapM_x f (a # xs)) (mapM_x g ys)
 2. \<And>a xs ys aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (mapM_x f xs) (mapM_x g ys); list_all2 F (a # xs) ys; suffix (a # xs) oxs; suffix ys oys; ys = aa # list\<rbrakk> \<Longrightarrow> corres dc (P (a # xs)) (P' ys) (mapM_x f (a # xs)) (mapM_x g ys) proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (mapM_x f xs) (mapM_x g ys); list_all2 F (a # xs) ys; suffix (a # xs) oxs; suffix ys oys; ys = aa # list\<rbrakk> \<Longrightarrow> corres dc (P (a # xs)) (P' ys) (mapM_x f (a # xs)) (mapM_x g ys) proof (prove)
goal (1 subgoal):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> corres dc (P (a # xs)) (P' (aa # list)) (do _ <- f a;
foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())
od) (do _ <- g aa;
foldr (\<lambda>x y. do _ <- x;
y
od) (map g list) (return ())
od) proof (prove)
goal (3 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> corres dc (?Q6 a xs aa list) (?Q'6 a xs aa list) (do _ <- f a;
foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())
od) (do _ <- g aa;
foldr (\<lambda>x y. do _ <- x;
y
od) (map g list) (return ())
od)
 2. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P (a # xs) s\<rbrakk> \<Longrightarrow> ?Q6 a xs aa list s
 3. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P' (aa # list) s\<rbrakk> \<Longrightarrow> ?Q'6 a xs aa list s proof (prove)
goal (8 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> F a aa
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> suffix (a # ?xs11 a xs aa list) oxs
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> suffix (aa # ?ys11 a xs aa list) oys
 4. \<And>a xs aa list uu_ uua_. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; dc uu_ uua_\<rbrakk> \<Longrightarrow> corres dc (?R10 a xs aa list uu_) (?R'10 a xs aa list uua_) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g list) (return ()))
 5. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a xs aa list\<rbrace> f a \<lbrace>?R10 a xs aa list\<rbrace>
 6. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a xs aa list\<rbrace> g aa \<lbrace>?R'10 a xs aa list\<rbrace>
 7. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P (a # xs) s\<rbrakk> \<Longrightarrow> (P (a # ?xs11 a xs aa list) and ?Q10 a xs aa list) s
 8. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P' (aa # list) s\<rbrakk> \<Longrightarrow> (P' (aa # ?ys11 a xs aa list) and ?Q'10 a xs aa list) s proof (prove)
goal (7 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> suffix (a # ?xs11 a xs aa list) oxs
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> suffix (aa # ?ys11 a xs aa list) oys
 3. \<And>a xs aa list uu_ uua_. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; dc uu_ uua_\<rbrakk> \<Longrightarrow> corres dc (?R10 a xs aa list uu_) (?R'10 a xs aa list uua_) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g list) (return ()))
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a xs aa list\<rbrace> f a \<lbrace>?R10 a xs aa list\<rbrace>
 5. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a xs aa list\<rbrace> g aa \<lbrace>?R'10 a xs aa list\<rbrace>
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P (a # xs) s\<rbrakk> \<Longrightarrow> (P (a # ?xs11 a xs aa list) and ?Q10 a xs aa list) s
 7. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P' (aa # list) s\<rbrakk> \<Longrightarrow> (P' (aa # ?ys11 a xs aa list) and ?Q'10 a xs aa list) s proof (prove)
goal (6 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> suffix (aa # ?ys11 a xs aa list) oys
 2. \<And>a xs aa list uu_ uua_. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; dc uu_ uua_\<rbrakk> \<Longrightarrow> corres dc (?R10 a xs aa list uu_) (?R'10 a xs aa list uua_) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g list) (return ()))
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a xs aa list\<rbrace> f a \<lbrace>?R10 a xs aa list\<rbrace>
 4. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a xs aa list\<rbrace> g aa \<lbrace>?R'10 a xs aa list\<rbrace>
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P (a # xs) s\<rbrakk> \<Longrightarrow> (P (a # xs) and ?Q10 a xs aa list) s
 6. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P' (aa # list) s\<rbrakk> \<Longrightarrow> (P' (aa # ?ys11 a xs aa list) and ?Q'10 a xs aa list) s proof (prove)
goal (5 subgoals):
 1. \<And>a xs aa list uu_ uua_. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; dc uu_ uua_\<rbrakk> \<Longrightarrow> corres dc (?R10 a xs aa list uu_) (?R'10 a xs aa list uua_) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g list) (return ()))
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a xs aa list\<rbrace> f a \<lbrace>?R10 a xs aa list\<rbrace>
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a xs aa list\<rbrace> g aa \<lbrace>?R'10 a xs aa list\<rbrace>
 4. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P (a # xs) s\<rbrakk> \<Longrightarrow> (P (a # xs) and ?Q10 a xs aa list) s
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P' (aa # list) s\<rbrakk> \<Longrightarrow> (P' (aa # list) and ?Q'10 a xs aa list) s proof (prove)
goal (5 subgoals):
 1. \<And>a xs aa list uu_ uua_. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); F a aa; list_all2 F xs list; suffix xs oxs; suffix list oys\<rbrakk> \<Longrightarrow> corres dc (?R10 a xs aa list uu_) (?R'10 a xs aa list uua_) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g list) (return ()))
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a xs aa list\<rbrace> f a \<lbrace>?R10 a xs aa list\<rbrace>
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a xs aa list\<rbrace> g aa \<lbrace>?R'10 a xs aa list\<rbrace>
 4. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P (a # xs) s\<rbrakk> \<Longrightarrow> (P (a # xs) and ?Q10 a xs aa list) s
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P' (aa # list) s\<rbrakk> \<Longrightarrow> (P' (aa # list) and ?Q'10 a xs aa list) s proof (prove)
goal (5 subgoals):
 1. \<And>a xs aa list uu_ uua_. \<lbrakk>F a aa; list_all2 F xs list; suffix xs oxs; suffix list oys; corres dc (P xs) (P' list) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g list) (return ()))\<rbrakk> \<Longrightarrow> corres dc (?R10 a xs aa list uu_) (?R'10 a xs aa list uua_) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g list) (return ()))
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a xs aa list\<rbrace> f a \<lbrace>?R10 a xs aa list\<rbrace>
 3. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a xs aa list\<rbrace> g aa \<lbrace>?R'10 a xs aa list\<rbrace>
 4. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P (a # xs) s\<rbrakk> \<Longrightarrow> (P (a # xs) and ?Q10 a xs aa list) s
 5. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P' (aa # list) s\<rbrakk> \<Longrightarrow> (P' (aa # list) and ?Q'10 a xs aa list) s proof (prove)
goal (4 subgoals):
 1. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a xs aa list\<rbrace> f a \<lbrace>\<lambda>_. P xs\<rbrace>
 2. \<And>a xs aa list. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a xs aa list\<rbrace> g aa \<lbrace>\<lambda>_. P' list\<rbrace>
 3. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P (a # xs) s\<rbrakk> \<Longrightarrow> (P (a # xs) and ?Q10 a xs aa list) s
 4. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P' (aa # list) s\<rbrakk> \<Longrightarrow> (P' (aa # list) and ?Q'10 a xs aa list) s proof (prove)
goal (2 subgoals):
 1. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P (a # xs) s\<rbrakk> \<Longrightarrow> (P (a # xs) and P (a # xs)) s
 2. \<And>a xs aa list s. \<lbrakk>\<And>ys. \<lbrakk>list_all2 F xs ys; suffix xs oxs; suffix ys oys\<rbrakk> \<Longrightarrow> corres dc (P xs) (P' ys) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ())) (foldr (\<lambda>x y. do _ <- x;
y
od) (map g ys) (return ())); suffix (a # xs) oxs; suffix (aa # list) oys; F a aa; list_all2 F xs list; P' (aa # list) s\<rbrakk> \<Longrightarrow> (P' (aa # list) and P' (aa # list)) s proof (prove)
goal:
No subgoals!