theory Bisim_UL

lemma bisim_splitE_req:
  assumes ac: "bisim (f \<oplus> (=)) P P' a c"
  and     bd: "\<And>r. bisim (f \<oplus> 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 (f \<oplus> R) (P and S) P' (a >>=E b) (c >>=E d)" using ac apply - apply (simp add: bindE_def lift_def[abs_def]) 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 [unfolded validE_R_def validE_def]]) apply (clarsimp split: sum.splits) apply (fastforce simp: in_monad bind_def throwError_def return_def split: sum.splits prod.splits) 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 [unfolded validE_R_def validE_def]]) apply clarsimp apply (clarsimp split: sum.splits) apply (fastforce simp: in_monad bind_def throwError_def return_def split: sum.splits prod.splits) 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 (f \<oplus> R) (P and S) P' (a >>=E b) (c >>=E d) proof (prove)
using this:
bisim (f \<oplus> (=)) P P' a c

goal (1 subgoal):
 1. bisim (f \<oplus> R) (P and S) P' (a >>=E b) (c >>=E d) proof (prove)
goal (1 subgoal):
 1. bisim (f \<oplus> (=)) P P' a c \<Longrightarrow> bisim (f \<oplus> R) (P and S) P' (a >>=E b) (c >>=E d) proof (prove)
goal (1 subgoal):
 1. bisim (f \<oplus> (=)) P P' a c \<Longrightarrow> bisim (f \<oplus> R) (P and S) P' (do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) (do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r, t) \<in> fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s)\<rbrakk> \<Longrightarrow> \<exists>(r', t')\<in>fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s'). (f \<oplus> R) r r' \<and> t = t'
 2. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t s'' x. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; P' s'; P s'; S s'; (x, s'') \<in> fst (a s'); (r, t) \<in> fst ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> b x) s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> b x) s''); (r', t') \<in> fst (c (?s'13 s' r t s'' x)); (f \<oplus> (=)) (?r13 s' r t s'' x) r'; ?t13 s' r t s'' x = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 6. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> b x) s''); (r', t') \<in> fst (c (?s13 s' r t s'' x)); (f \<oplus> (=)) (?r13 s' r t s'' x) r'; ?t13 s' r t s'' x = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 5. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> b x) s''); (r', t') \<in> fst (c s'); (f \<oplus> (=)) x r'; s'' = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> b x) s''); (r', t') \<in> fst (c s'); (f \<oplus> (=)) x r'; s'' = t'; case x of Inl e \<Rightarrow> True | Inr r \<Rightarrow> (Q r and Q' r) s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (3 subgoals):
 1. \<And>s' r t t' x1 y'. \<lbrakk>(Inl y', t') \<in> fst (c s'); P' s'; P s'; S s'; (Inl x1, t') \<in> fst (a s'); (r, t) \<in> fst (throwError x1 t'); f x1 y'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 2. \<And>s' r t t' x2. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 3. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t t' x2. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (6 subgoals):
 1. \<And>s' r t t' x2. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'\<rbrakk> \<Longrightarrow> ?s163 s' r t t' x2 = ?s'163 s' r t t' x2
 2. \<And>s' r t t' x2. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'\<rbrakk> \<Longrightarrow> Q (?r164 s' r t t' x2) (?s163 s' r t t' x2)
 3. \<And>s' r t t' x2. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'\<rbrakk> \<Longrightarrow> Q' (?r164 s' r t t' x2) (?s'163 s' r t t' x2)
 4. \<And>s' r t t' x2. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'\<rbrakk> \<Longrightarrow> (?r163 s' r t t' x2, ?t163 s' r t t' x2) \<in> fst (b (?r164 s' r t t' x2) (?s163 s' r t t' x2))
 5. \<And>s' r t t' x2 r' t'a. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'; (r', t'a) \<in> fst (d (?r164 s' r t t' x2) (?s'163 s' r t t' x2)); (f \<oplus> R) (?r163 s' r t t' x2) r'; ?t163 s' r t t' x2 = t'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 6. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (5 subgoals):
 1. \<And>s' r t t' x2. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'\<rbrakk> \<Longrightarrow> Q (?r164 s' r t t' x2) (?s163 s' r t t' x2)
 2. \<And>s' r t t' x2. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'\<rbrakk> \<Longrightarrow> Q' (?r164 s' r t t' x2) (?s163 s' r t t' x2)
 3. \<And>s' r t t' x2. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'\<rbrakk> \<Longrightarrow> (?r163 s' r t t' x2, ?t163 s' r t t' x2) \<in> fst (b (?r164 s' r t t' x2) (?s163 s' r t t' x2))
 4. \<And>s' r t t' x2 r' t'a. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'; (r', t'a) \<in> fst (d (?r164 s' r t t' x2) (?s163 s' r t t' x2)); (f \<oplus> R) (?r163 s' r t t' x2) r'; ?t163 s' r t t' x2 = t'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 5. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t t' x2 r' t'a. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'; (r', t'a) \<in> fst (d x2 t'); (f \<oplus> R) r r'; t = t'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t t' x2 r'' t''. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'; (r'', t'') \<in> fst (d x2 t'); (f \<oplus> R) r r''; t = t''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= case_sum throwError d) s'). (f \<oplus> R) r (fst x) \<and> t = snd x
 2. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (3 subgoals):
 1. \<And>s' r t t' x2 r'' t''. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'; (r'', t'') \<in> fst (d x2 t'); (f \<oplus> R) r r''; t = t''\<rbrakk> \<Longrightarrow> (f \<oplus> R) r (fst (r'', t'')) \<and> t = snd (r'', t'')
 2. \<And>s' r t t' x2 r'' t''. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'; (r'', t'') \<in> fst (d x2 t'); (f \<oplus> R) r r''; t = t''\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((c >>= case_sum throwError d) s')
 3. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r t t' x2 r'' t''. \<lbrakk>(Inr x2, t') \<in> fst (c s'); P' s'; P s'; S s'; (Inr x2, t') \<in> fst (a s'); (r, t) \<in> fst (b x2 t'); Q x2 t'; Q' x2 t'; (r'', t'') \<in> fst (d x2 t'); (f \<oplus> R) r r''; t = t''\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((c >>= case_sum throwError d) s')
 2. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; s = s'; (P and S) s; P' s'; (r', t') \<in> fst ((do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) s). (f \<oplus> R) r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x. \<lbrakk>bisim (f \<oplus> (=)) P P' a c; P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s'')\<rbrakk> \<Longrightarrow> ?s183 s' r' t' s'' x = ?s'183 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s'')\<rbrakk> \<Longrightarrow> P (?s183 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s'')\<rbrakk> \<Longrightarrow> P' (?s'183 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s'')\<rbrakk> \<Longrightarrow> (?r'183 s' r' t' s'' x, ?t'183 s' r' t' s'' x) \<in> fst (c (?s'183 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s''); (r, t) \<in> fst (a (?s183 s' r' t' s'' x)); (f \<oplus> (=)) r (?r'183 s' r' t' s'' x); t = ?t'183 s' r' t' s'' x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s'')\<rbrakk> \<Longrightarrow> P (?s183 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s'')\<rbrakk> \<Longrightarrow> P' (?s183 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s'')\<rbrakk> \<Longrightarrow> (?r'183 s' r' t' s'' x, ?t'183 s' r' t' s'' x) \<in> fst (c (?s183 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s''); (r, t) \<in> fst (a (?s183 s' r' t' s'' x)); (f \<oplus> (=)) r (?r'183 s' r' t' s'' x); t = ?t'183 s' r' t' s'' x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s''); (r, t) \<in> fst (a s'); (f \<oplus> (=)) r x; t = s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> 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 ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s''); (r, t) \<in> fst (a s'); (f \<oplus> (=)) r x; t = s''; case r of Inl e \<Rightarrow> True | Inr r \<Rightarrow> (Q r and Q' r) t\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> R) (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x r. \<lbrakk>P' s'; P s'; S s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst ((case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> d x) s''); (r, s'') \<in> fst (a s'); (f \<oplus> (=)) r x; case r of Inl e \<Rightarrow> True | Inr r \<Rightarrow> (Q r and Q' r) s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> R) (fst x) r' \<and> snd x = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r' t' s'' x1 x1a. \<lbrakk>P' s'; P s'; S s'; (Inl x1, s'') \<in> fst (c s'); (r', t') \<in> fst (throwError x1 s''); (Inl x1a, s'') \<in> fst (a s'); f x1a x1\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> R) (fst x) r' \<and> snd x = t'
 2. \<And>s' r' t' s'' x2. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> R) (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x2. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> R) (fst x) r' \<and> snd x = t' proof (prove)
goal (5 subgoals):
 1. \<And>s' r' t' s'' x2. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''\<rbrakk> \<Longrightarrow> ?s348 s' r' t' s'' x2 = ?s'348 s' r' t' s'' x2
 2. \<And>s' r' t' s'' x2. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''\<rbrakk> \<Longrightarrow> Q (?r349 s' r' t' s'' x2) (?s348 s' r' t' s'' x2)
 3. \<And>s' r' t' s'' x2. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''\<rbrakk> \<Longrightarrow> Q' (?r349 s' r' t' s'' x2) (?s'348 s' r' t' s'' x2)
 4. \<And>s' r' t' s'' x2. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''\<rbrakk> \<Longrightarrow> (?r'348 s' r' t' s'' x2, ?t'348 s' r' t' s'' x2) \<in> fst (d (?r349 s' r' t' s'' x2) (?s'348 s' r' t' s'' x2))
 5. \<And>s' r' t' s'' x2 r t. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''; (r, t) \<in> fst (b (?r349 s' r' t' s'' x2) (?s348 s' r' t' s'' x2)); (f \<oplus> R) r (?r'348 s' r' t' s'' x2); t = ?t'348 s' r' t' s'' x2\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> R) (fst x) r' \<and> snd x = t' proof (prove)
goal (4 subgoals):
 1. \<And>s' r' t' s'' x2. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''\<rbrakk> \<Longrightarrow> Q (?r349 s' r' t' s'' x2) (?s348 s' r' t' s'' x2)
 2. \<And>s' r' t' s'' x2. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''\<rbrakk> \<Longrightarrow> Q' (?r349 s' r' t' s'' x2) (?s348 s' r' t' s'' x2)
 3. \<And>s' r' t' s'' x2. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''\<rbrakk> \<Longrightarrow> (?r'348 s' r' t' s'' x2, ?t'348 s' r' t' s'' x2) \<in> fst (d (?r349 s' r' t' s'' x2) (?s348 s' r' t' s'' x2))
 4. \<And>s' r' t' s'' x2 r t. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''; (r, t) \<in> fst (b (?r349 s' r' t' s'' x2) (?s348 s' r' t' s'' x2)); (f \<oplus> R) r (?r'348 s' r' t' s'' x2); t = ?t'348 s' r' t' s'' x2\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> R) (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x2 r t. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''; (r, t) \<in> fst (b x2 s''); (f \<oplus> R) r r'; t = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> R) (fst x) r' \<and> snd x = t' proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x2 r'' t''. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''; (r'', t'') \<in> fst (b x2 s''); (f \<oplus> R) r'' r'; t'' = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= case_sum throwError b) s'). (f \<oplus> R) (fst x) r' \<and> snd x = t' proof (prove)
goal (2 subgoals):
 1. \<And>s' r' t' s'' x2 r'' t''. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''; (r'', t'') \<in> fst (b x2 s''); (f \<oplus> R) r'' r'; t'' = t'\<rbrakk> \<Longrightarrow> (f \<oplus> R) (fst (r'', t'')) r' \<and> snd (r'', t'') = t'
 2. \<And>s' r' t' s'' x2 r'' t''. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''; (r'', t'') \<in> fst (b x2 s''); (f \<oplus> R) r'' r'; t'' = t'\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((a >>= case_sum throwError b) s') proof (prove)
goal (1 subgoal):
 1. \<And>s' r' t' s'' x2 r'' t''. \<lbrakk>(Inr x2, s'') \<in> fst (a s'); P' s'; P s'; S s'; (Inr x2, s'') \<in> fst (c s'); (r', t') \<in> fst (d x2 s''); Q x2 s''; Q' x2 s''; (r'', t'') \<in> fst (b x2 s''); (f \<oplus> R) r'' r'; t'' = t'\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((a >>= case_sum throwError b) s') proof (prove)
goal:
No subgoals!