theory Bisim_UL

lemma bisim_split_req:
  assumes ac: "bisim (=) P P' a c"
  and     bd: "\<And>r. bisim R (Q r) (Q' r) (b r) (d r)"
  and     v1: "\<lbrace>S\<rbrace> a \<lbrace>\<lambda>r. Q r and Q' r\<rbrace>"
  shows "bisim R (P and S) P' (a >>= b) (c >>= d)" using ac apply - apply (rule bisim_underlyingI) apply (clarsimp simp: in_monad split_def) apply (erule bisim_underlyingE1) apply simp apply assumption+ apply (frule (1) use_valid [OF _ v1]) apply clarsimp apply (rule bisim_underlyingE1 [OF bd]) apply simp apply assumption+ apply (rename_tac r'' t'') apply (rule_tac x = "(r'', t'')" in bexI) apply clarsimp apply (fastforce simp: in_monad) apply (clarsimp simp: in_monad split_def) apply (erule bisim_underlyingE2) apply simp apply assumption+ apply (frule (1) use_valid [OF _ v1]) apply clarsimp apply (rule bisim_underlyingE2 [OF bd]) apply simp apply assumption+ apply (rename_tac r'' t'') apply (rule_tac x = "(r'', t'')" in bexI) apply clarsimp apply (fastforce simp: in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim R (P and S) P' (a >>= b) (c >>= d) proof (prove)
using this:
bisim (=) P P' a c

goal (1 subgoal):
 1. bisim R (P and S) P' (a >>= b) (c >>= d) proof (prove)
goal (1 subgoal):
 1. bisim (=) P P' a c \<Longrightarrow> bisim R (P and S) P' (a >>= b) (c >>= d) proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r, t) \<in> fst ((a >>= b) s)\<rbrakk> \<Longrightarrow> \<exists>(r', t')\<in>fst ((c >>= d) s'). R r r' \<and> t = t'
 2. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t s'' x. \<lbrakk>bisim (=) P P' a c; P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (6 subgoals):
 1. \<And>s' r t s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s'')\<rbrakk> \<Longrightarrow> ?s13 s' r t s'' x = ?s'13 s' r t s'' x
 2. \<And>s' r t s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s'')\<rbrakk> \<Longrightarrow> P (?s13 s' r t s'' x)
 3. \<And>s' r t s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s'')\<rbrakk> \<Longrightarrow> P' (?s'13 s' r t s'' x)
 4. \<And>s' r t s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s'')\<rbrakk> \<Longrightarrow> (?r13 s' r t s'' x, ?t13 s' r t s'' x) \<in> fst (a (?s13 s' r t s'' x))
 5. \<And>s' r t s'' x r' t'. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c (?s'13 s' r t s'' x)); ?r13 s' r t s'' x = r'; ?t13 s' r t s'' x = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 6. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (5 subgoals):
 1. \<And>s' r t s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s'')\<rbrakk> \<Longrightarrow> P (?s13 s' r t s'' x)
 2. \<And>s' r t s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s'')\<rbrakk> \<Longrightarrow> P' (?s13 s' r t s'' x)
 3. \<And>s' r t s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s'')\<rbrakk> \<Longrightarrow> (?r13 s' r t s'' x, ?t13 s' r t s'' x) \<in> fst (a (?s13 s' r t s'' x))
 4. \<And>s' r t s'' x r' t'. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c (?s13 s' r t s'' x)); ?r13 s' r t s'' x = r'; ?t13 s' r t s'' x = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 5. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t s'' x r' t'. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); x = r'; s'' = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t s'' x r' t'. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); x = r'; s'' = t'; (Q x and Q' x) s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t r' t'. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (6 subgoals):
 1. \<And>s' r t r' t'. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'\<rbrakk> \<Longrightarrow> ?s28 s' r t r' t' = ?s'28 s' r t r' t'
 2. \<And>s' r t r' t'. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'\<rbrakk> \<Longrightarrow> Q (?r29 s' r t r' t') (?s28 s' r t r' t')
 3. \<And>s' r t r' t'. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'\<rbrakk> \<Longrightarrow> Q' (?r29 s' r t r' t') (?s'28 s' r t r' t')
 4. \<And>s' r t r' t'. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'\<rbrakk> \<Longrightarrow> (?r28 s' r t r' t', ?t28 s' r t r' t') \<in> fst (b (?r29 s' r t r' t') (?s28 s' r t r' t'))
 5. \<And>s' r t r' t' r'a t'a. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'; (r'a, t'a) \<in> fst (d (?r29 s' r t r' t') (?s'28 s' r t r' t')); R (?r28 s' r t r' t') r'a; ?t28 s' r t r' t' = t'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 6. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (5 subgoals):
 1. \<And>s' r t r' t'. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'\<rbrakk> \<Longrightarrow> Q (?r29 s' r t r' t') (?s28 s' r t r' t')
 2. \<And>s' r t r' t'. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'\<rbrakk> \<Longrightarrow> Q' (?r29 s' r t r' t') (?s28 s' r t r' t')
 3. \<And>s' r t r' t'. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'\<rbrakk> \<Longrightarrow> (?r28 s' r t r' t', ?t28 s' r t r' t') \<in> fst (b (?r29 s' r t r' t') (?s28 s' r t r' t'))
 4. \<And>s' r t r' t' r'a t'a. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'; (r'a, t'a) \<in> fst (d (?r29 s' r t r' t') (?s28 s' r t r' t')); R (?r28 s' r t r' t') r'a; ?t28 s' r t r' t' = t'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 5. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t r' t' r'a t'a. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'; (r'a, t'a) \<in> fst (d r' t'); R r r'a; t = t'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t r' t' r'' t''. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'; (r'', t'') \<in> fst (d r' t'); R r r''; t = t''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (3 subgoals):
 1. \<And>s' r t r' t' r'' t''. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'; (r'', t'') \<in> fst (d r' t'); R r r''; t = t''\<rbrakk> \<Longrightarrow> R r (fst (r'', t'')) \<and> t = snd (r'', t'')
 2. \<And>s' r t r' t' r'' t''. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'; (r'', t'') \<in> fst (d r' t'); R r r''; t = t''\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((c >>= d) s')
 3. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t r' t' r'' t''. \<lbrakk>P' s'; P s'; S s'; (r', t') \<in> fst (a s'); (r, t) \<in> fst (b r' t'); (r', t') \<in> fst (c s'); Q r' t'; Q' r' t'; (r'', t'') \<in> fst (d r' t'); R r r''; t = t''\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((c >>= d) s')
 2. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>bisim (=) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x. \<lbrakk>bisim (=) P P' a c; P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (5 subgoals):
 1. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s'')\<rbrakk> \<Longrightarrow> ?s48 s' r' t' s'' x = ?s'48 s' r' t' s'' x
 2. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s'')\<rbrakk> \<Longrightarrow> P (?s48 s' r' t' s'' x)
 3. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s'')\<rbrakk> \<Longrightarrow> P' (?s'48 s' r' t' s'' x)
 4. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s'')\<rbrakk> \<Longrightarrow> (?r'48 s' r' t' s'' x, ?t'48 s' r' t' s'' x) \<in> fst (c (?s'48 s' r' t' s'' x))
 5. \<And>s' r' t' s'' x r t. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a (?s48 s' r' t' s'' x)); r = ?r'48 s' r' t' s'' x; t = ?t'48 s' r' t' s'' x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (4 subgoals):
 1. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s'')\<rbrakk> \<Longrightarrow> P (?s48 s' r' t' s'' x)
 2. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s'')\<rbrakk> \<Longrightarrow> P' (?s48 s' r' t' s'' x)
 3. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s'')\<rbrakk> \<Longrightarrow> (?r'48 s' r' t' s'' x, ?t'48 s' r' t' s'' x) \<in> fst (c (?s48 s' r' t' s'' x))
 4. \<And>s' r' t' s'' x r t. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a (?s48 s' r' t' s'' x)); r = ?r'48 s' r' t' s'' x; t = ?t'48 s' r' t' s'' x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x r t. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s'); r = x; t = s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x r t. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s'); r = x; t = s''; (Q r and Q' r) t\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (5 subgoals):
 1. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''\<rbrakk> \<Longrightarrow> ?s61 s' r' t' s'' x = ?s'61 s' r' t' s'' x
 2. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''\<rbrakk> \<Longrightarrow> Q (?r62 s' r' t' s'' x) (?s61 s' r' t' s'' x)
 3. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''\<rbrakk> \<Longrightarrow> Q' (?r62 s' r' t' s'' x) (?s'61 s' r' t' s'' x)
 4. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''\<rbrakk> \<Longrightarrow> (?r'61 s' r' t' s'' x, ?t'61 s' r' t' s'' x) \<in> fst (d (?r62 s' r' t' s'' x) (?s'61 s' r' t' s'' x))
 5. \<And>s' r' t' s'' x r t. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''; (r, t) \<in> fst (b (?r62 s' r' t' s'' x) (?s61 s' r' t' s'' x)); R r (?r'61 s' r' t' s'' x); t = ?t'61 s' r' t' s'' x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (4 subgoals):
 1. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''\<rbrakk> \<Longrightarrow> Q (?r62 s' r' t' s'' x) (?s61 s' r' t' s'' x)
 2. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''\<rbrakk> \<Longrightarrow> Q' (?r62 s' r' t' s'' x) (?s61 s' r' t' s'' x)
 3. \<And>s' r' t' s'' x. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''\<rbrakk> \<Longrightarrow> (?r'61 s' r' t' s'' x, ?t'61 s' r' t' s'' x) \<in> fst (d (?r62 s' r' t' s'' x) (?s61 s' r' t' s'' x))
 4. \<And>s' r' t' s'' x r t. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''; (r, t) \<in> fst (b (?r62 s' r' t' s'' x) (?s61 s' r' t' s'' x)); R r (?r'61 s' r' t' s'' x); t = ?t'61 s' r' t' s'' x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x r t. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''; (r, t) \<in> fst (b x s''); R r r'; t = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x r'' t''. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''; (r'', t'') \<in> fst (b x s''); R r'' r'; t'' = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s'). R (fst x) r' \<and> snd x = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r' t' s'' x r'' t''. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''; (r'', t'') \<in> fst (b x s''); R r'' r'; t'' = t'\<rbrakk> \<Longrightarrow> R (fst (r'', t'')) r' \<and> snd (r'', t'') = t'
 2. \<And>s' r' t' s'' x r'' t''. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''; (r'', t'') \<in> fst (b x s''); R r'' r'; t'' = t'\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((a >>= b) s') proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x r'' t''. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (x, s'') \<in> fst (a s'); Q x s''; Q' x s''; (r'', t'') \<in> fst (b x s''); R r'' r'; t'' = t'\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((a >>= b) s') proof (prove)
goal:
No subgoals!