theory MonadicRewrite

lemma monadic_rewrite_bind:
  "\<lbrakk> monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= (\<lambda>x. h x)) (g >>= (\<lambda>x. j x))" apply (cases E) apply (clarsimp simp: monadic_rewrite_def snd_bind imp_conjL) apply (drule spec, drule(1) mp, clarsimp) apply (rule bind_apply_cong) apply simp apply (frule(2) use_valid) apply fastforce apply (clarsimp simp: monadic_rewrite_def snd_bind imp_conjL) apply (simp add: bind_def split_def) apply (rule conjI) apply (rule UN_mono) apply simp apply clarsimp apply (frule(2) use_valid) apply fastforce apply (rule conjI) apply fastforce apply clarsimp apply (frule(2) use_valid) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j)
 2. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> f s = g s; \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> h x s = j x s; \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> (case x of (r, s') \<Rightarrow> snd (h r s')))\<rbrakk> \<Longrightarrow> (f >>= h) s = (g >>= j) s
 2. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> h x s = j x s; \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; E; P s; R s; F \<longrightarrow> \<not> snd (g s) \<and> (\<forall>x\<in>fst (g s). \<not> (case x of (r, s') \<Rightarrow> snd (h r s'))); f s = g s\<rbrakk> \<Longrightarrow> (f >>= h) s = (g >>= j) s
 2. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> h x s = j x s; \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; E; P s; R s; F \<longrightarrow> \<not> snd (g s) \<and> (\<forall>x\<in>fst (g s). \<not> (case x of (r, s') \<Rightarrow> snd (h r s'))); f s = g s\<rbrakk> \<Longrightarrow> f s = g s
 2. \<And>s rv st. \<lbrakk>\<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> h x s = j x s; \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; E; P s; R s; F \<longrightarrow> \<not> snd (g s) \<and> (\<forall>x\<in>fst (g s). \<not> (case x of (r, s') \<Rightarrow> snd (h r s'))); f s = g s; (rv, st) \<in> fst (g s)\<rbrakk> \<Longrightarrow> h rv st = j rv st
 3. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j) proof (prove)
goal (2 subgoals):
 1. \<And>s rv st. \<lbrakk>\<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> h x s = j x s; \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; E; P s; R s; F \<longrightarrow> \<not> snd (g s) \<and> (\<forall>x\<in>fst (g s). \<not> (case x of (r, s') \<Rightarrow> snd (h r s'))); f s = g s; (rv, st) \<in> fst (g s)\<rbrakk> \<Longrightarrow> h rv st = j rv st
 2. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j) proof (prove)
goal (2 subgoals):
 1. \<And>s rv st. \<lbrakk>\<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> h x s = j x s; \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; E; P s; R s; F \<longrightarrow> \<not> snd (g s) \<and> (\<forall>x\<in>fst (g s). \<not> (case x of (r, s') \<Rightarrow> snd (h r s'))); f s = g s; (rv, st) \<in> fst (g s); Q rv st\<rbrakk> \<Longrightarrow> h rv st = j rv st
 2. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> (case x of (r, s') \<Rightarrow> snd (h r s')))\<rbrakk> \<Longrightarrow> fst ((g >>= j) s) \<subseteq> fst ((f >>= h) s) \<and> (snd (g s) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). case x of (r, s') \<Rightarrow> snd (h r s'))) \<and> ((\<exists>x\<in>fst (g s). case x of (r, s') \<Rightarrow> snd (j r s')) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). case x of (r, s') \<Rightarrow> snd (h r s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (g s). fst (j (fst x) (snd x))) \<subseteq> (\<Union>x\<in>fst (f s). fst (h (fst x) (snd x))) \<and> (snd (g s) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) \<and> ((\<exists>x\<in>fst (g s). snd (j (fst x) (snd x))) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (g s). fst (j (fst x) (snd x))) \<subseteq> (\<Union>x\<in>fst (f s). fst (h (fst x) (snd x)))
 2. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (snd (g s) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) \<and> ((\<exists>x\<in>fst (g s). snd (j (fst x) (snd x))) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> fst (g s) \<subseteq> fst (f s)
 2. \<And>s x. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x))); x \<in> fst (g s)\<rbrakk> \<Longrightarrow> fst (j (fst x) (snd x)) \<subseteq> fst (h (fst x) (snd x))
 3. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (snd (g s) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) \<and> ((\<exists>x\<in>fst (g s). snd (j (fst x) (snd x))) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x))); x \<in> fst (g s)\<rbrakk> \<Longrightarrow> fst (j (fst x) (snd x)) \<subseteq> fst (h (fst x) (snd x))
 2. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (snd (g s) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) \<and> ((\<exists>x\<in>fst (g s). snd (j (fst x) (snd x))) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x))); (a, b) \<in> fst (g s); (aa, ba) \<in> fst (j a b)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> fst (h a b)
 2. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (snd (g s) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) \<and> ((\<exists>x\<in>fst (g s). snd (j (fst x) (snd x))) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x))); (a, b) \<in> fst (g s); (aa, ba) \<in> fst (j a b); Q a b\<rbrakk> \<Longrightarrow> (aa, ba) \<in> fst (h a b)
 2. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (snd (g s) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) \<and> ((\<exists>x\<in>fst (g s). snd (j (fst x) (snd x))) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (snd (g s) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) \<and> ((\<exists>x\<in>fst (g s). snd (j (fst x) (snd x))) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> snd (g s) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x)))
 2. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (g s). snd (j (fst x) (snd x))) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s) \<and> (\<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (g s). snd (j (fst x) (snd x))) \<longrightarrow> snd (f s) \<or> (\<exists>x\<in>fst (f s). snd (h (fst x) (snd x))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s); (a, b) \<in> fst (g s); snd (j a b); \<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x))\<rbrakk> \<Longrightarrow> snd (f s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)); \<And>x. \<forall>s. Q x s \<longrightarrow> (F \<longrightarrow> \<not> snd (h x s)) \<longrightarrow> fst (j x s) \<subseteq> fst (h x s) \<and> (snd (j x s) \<longrightarrow> snd (h x s)); \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>; \<not> E; P s; R s; F \<longrightarrow> \<not> snd (f s); (a, b) \<in> fst (g s); snd (j a b); \<forall>x\<in>fst (f s). \<not> snd (h (fst x) (snd x)); Q a b\<rbrakk> \<Longrightarrow> snd (f s) proof (prove)
goal:
No subgoals!