theory MonadicRewrite

lemma monadic_rewrite_symb_exec_l':
  "\<lbrakk> \<And>rv. monadic_rewrite F E (Q rv) (x rv) y;
     \<And>P. m \<lbrace>P\<rbrace>; empty_fail m;
     \<not> F \<longrightarrow> no_fail P' m;
     \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= (\<lambda>rv. x rv)) y" apply (cases E) subgoal  (* E *)
      apply (clarsimp simp: monadic_rewrite_def bind_def prod_eq_iff) apply (subgoal_tac "\<not> snd (m s)") apply (simp add: empty_fail_def, drule_tac x=s in spec) apply (prop_tac "\<forall>(rv, s') \<in> fst (m s). x rv s' = y s") apply clarsimp apply (drule (1) in_inv_by_hoareD) apply (frule (2) use_valid) apply (clarsimp simp: Ball_def prod_eq_iff) apply (rule conjI) apply (rule equalityI) apply (clarsimp simp: Ball_def) apply (fastforce simp: Ball_def elim!: nonemptyE elim: rev_bexI) apply (simp add: Bex_def Ball_def cong: conj_cong) apply auto[1] apply (clarsimp simp: no_fail_def) done subgoal  (* \<not> E *)
     apply (clarsimp simp: monadic_rewrite_def bind_def) apply (prop_tac "\<not> snd (m s)") apply (fastforce simp: no_failD) apply (prop_tac "\<forall>v \<in> fst (m s). Q (fst v) (snd v) \<and> snd v = s") apply clarsimp apply (frule(2) use_valid) apply (frule use_valid, assumption, rule refl) apply simp apply clarsimp apply (frule (1) empty_failD2) apply (clarsimp simp: split_def) apply fastforce done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= x) y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= x) y
 2. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= x) y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= x) y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= x) y proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) = fst (y s) \<and> ((\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s)) = snd (y s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) = fst (y s) \<and> ((\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s)) = snd (y s)
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s)\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) = fst (y s) \<and> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s)\<rbrakk> \<Longrightarrow> \<forall>(rv, s')\<in>fst (m s). x rv s' = y s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) = fst (y s) \<and> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) \<noteq> {}; (a, b) \<in> fst (m s)\<rbrakk> \<Longrightarrow> x a b = y s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) = fst (y s) \<and> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) \<noteq> {}; (a, b) \<in> fst (m s); b = s\<rbrakk> \<Longrightarrow> x a b = y s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) = fst (y s) \<and> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) \<noteq> {}; (a, b) \<in> fst (m s); b = s; Q a b\<rbrakk> \<Longrightarrow> x a b = y s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) = fst (y s) \<and> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) = fst (y s) \<and> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) = fst (y s)
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<subseteq> fst (y s)
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb))
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 4. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb))
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 3. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). x rv s' = y s\<rbrakk> \<Longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) = snd (y s)
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<exists>a b. (a, b) \<in> fst (m s)) \<longrightarrow> \<not> snd (y s); \<not> snd (m s); fst (m s) \<noteq> {}; \<forall>a b. (a, b) \<in> fst (m s) \<longrightarrow> x a b = y s\<rbrakk> \<Longrightarrow> ((\<exists>a b. (a, b) \<in> fst (m s)) \<and> snd (y s)) = snd (y s)
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (x rv s) = fst (y s) \<and> snd (x rv s) = snd (y s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= x) y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= x) y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= x) y proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s)
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); \<not> snd (m s); \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); (a, b) \<in> fst (m s)\<rbrakk> \<Longrightarrow> Q a b \<and> b = s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); \<not> snd (m s); \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); (a, b) \<in> fst (m s); Q a b\<rbrakk> \<Longrightarrow> Q a b \<and> b = s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); \<not> snd (m s); \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); (a, b) \<in> fst (m s); Q a b; ?t48 s b a b = ?t47 s b a b\<rbrakk> \<Longrightarrow> Q a b \<and> b = s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); \<not> snd (m s); \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s))
flex-flex pairs:
\<lambda>s. ?t47 s s \<equiv>\<^sup>? \<lambda>s. ?t48 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); \<not> snd (m s); \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<or> snd (m s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)); \<not> snd (m s); \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s; \<exists>v. v \<in> fst (m s)\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>a\<in>fst (m s). fst (case a of (xa, xb) \<Rightarrow> x xa xb)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (case xa of (xa, xb) \<Rightarrow> x xa xb))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> fst (y s) \<subseteq> fst (x rv s) \<and> (snd (y s) \<longrightarrow> snd (x rv s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<not> F \<longrightarrow> no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (x (fst xa) s)); \<not> snd (m s); \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s; (a, b) \<in> fst (m s)\<rbrakk> \<Longrightarrow> fst (y s) \<subseteq> (\<Union>xa\<in>fst (m s). fst (x (fst xa) s)) \<and> (snd (y s) \<longrightarrow> (\<exists>xa\<in>fst (m s). snd (x (fst xa) s))) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!