theory Corres_D

lemma corres_alternative_throw_splitE:
  assumes a: "corres_underlying R False z (dc \<oplus> r') P P' (f \<sqinter> Monads_D.throw) f'"
  assumes b:  "\<And>x x'. r' x x' \<Longrightarrow> corres_underlying R False z (dc \<oplus> r) (Q x) (Q' x') (g x \<sqinter> Monads_D.throw) (g' x')"
  assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_. \<top>\<rbrace>"
  assumes f': "\<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>_. \<top>\<rbrace>"
  assumes f'_eq: "\<And>s. \<lbrace>(=) s\<rbrace> f' \<lbrace>\<lambda>_. (=) s\<rbrace>"
  assumes g'_eq: "\<And>s x. \<lbrace>\<lambda>s'. s' = s \<and> Q' x s'\<rbrace> g' x \<lbrace>\<lambda>_. \<top>\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>"
  shows "corres_underlying R False z (dc \<oplus> r) P P' ((f >>=E g) \<sqinter> Monads_D.throw) (f' >>=E g')" apply (clarsimp simp: bindE_def corres_underlying_def) apply (rule conjI) prefer 2 apply (frule (2) corres_underlyingD [OF a]) apply simp apply (clarsimp simp: bind_def split_def lift_def) apply (clarsimp simp: throwError_def return_def split: sum.splits) apply (drule (1) bspec, clarsimp simp: alternative_def) apply (drule b) apply (thin_tac "(a,b) \<in> R") apply (drule (1) corres_underlyingD) apply (drule use_valid, rule f[unfolded validE_def]) apply assumption apply simp apply (drule use_valid, rule f'[unfolded validE_def]) apply assumption apply simp apply simp apply simp apply (clarsimp simp: in_bind) apply (frule (3) corres_underlyingD2 [OF a]) apply simp apply (clarsimp simp: in_alternative in_throwError) apply (erule disjE) prefer 2 apply (clarsimp simp: lift_def in_throwError) apply (clarsimp simp: alternative_def throwError_def return_def) apply (simp add: lift_def split: sum.splits) apply (clarsimp simp: in_throwError) apply (rule_tac x="(Inl x',bb)" in bexI) apply simp apply (clarsimp simp: alternative_def bind_def) apply (rule bexI) prefer 2 apply assumption apply (simp add: lift_def throwError_def return_def) apply clarsimp apply (drule b) apply (drule_tac s'=s'' in corres_underlyingD2, assumption) apply (drule use_valid, rule f[unfolded validE_def]) apply assumption apply simp apply (drule use_valid, rule f'[unfolded validE_def]) apply assumption apply simp apply assumption apply simp apply (clarsimp simp: in_alternative in_throwError) apply (erule disjE) apply (rule bexI, fastforce) apply (clarsimp simp: alternative_def) apply (simp add: bind_def) apply (rule bexI) prefer 2 apply assumption apply (clarsimp simp: lift_def) apply clarsimp apply (frule use_valid, rule f'_eq, rule refl) apply clarsimp apply (drule use_valid, rule g'_eq[unfolded validE_def]) apply (rule conjI, rule refl) apply (drule use_valid, rule f'[unfolded validE_def], assumption) apply simp apply (simp add: alternative_def throwError_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying R False z (dc \<oplus> r) P P' (f >>=E g \<sqinter> throw) (f' >>=E g') proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd ((f' >>= lift g') b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift g') b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift g') b)
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((f \<sqinter> throw) a)
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; (\<forall>(r'a, t')\<in>fst (f' b). \<exists>(r, t)\<in>fst ((f \<sqinter> throw) a). (t, t') \<in> R \<and> (dc \<oplus> r') r r'a) \<and> (z \<longrightarrow> \<not> snd (f' b))\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift g') b)
 3. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; (\<forall>(r'a, t')\<in>fst (f' b). \<exists>(r, t)\<in>fst ((f \<sqinter> throw) a). (t, t') \<in> R \<and> (dc \<oplus> r') r r'a) \<and> (z \<longrightarrow> \<not> snd (f' b))\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift g') b)
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> R; P a; P' b; \<forall>x\<in>fst (f' b). \<exists>xa\<in>fst ((f \<sqinter> throw) a). (snd xa, snd x) \<in> R \<and> (dc \<oplus> r') (fst xa) (fst x); z; (aa, ba) \<in> fst (f' b); snd ((case aa of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g' x) ba); \<not> snd (f' b)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b ba x2. \<lbrakk>\<not> snd (f' b); (a, b) \<in> R; P a; P' b; \<forall>x\<in>fst (f' b). \<exists>xa\<in>fst ((f \<sqinter> (\<lambda>s. ({(Inl undefined, s)}, False))) a). (snd xa, snd x) \<in> R \<and> (dc \<oplus> r') (fst xa) (fst x); z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); (a, b) \<in> R; P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; r' x' x2\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); (a, b) \<in> R; P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; corres_underlying R False z (dc \<oplus> r) (Q x') (Q' x2) (g x' \<sqinter> throw) (g' x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; corres_underlying R False z (dc \<oplus> r) (Q x') (Q' x2) (g x' \<sqinter> throw) (g' x2)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (5 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> Q x' bb
 2. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> Q' x2 ba
 3. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 4. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; (\<forall>(r', t')\<in>fst (g' x2 ba). \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' x2 ba))\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (6 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> P a
 2. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (bb, ba) \<in> R; case Inr x' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r bb\<rbrakk> \<Longrightarrow> Q x' bb
 3. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> Q' x2 ba
 4. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 5. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; (\<forall>(r', t')\<in>fst (g' x2 ba). \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' x2 ba))\<rbrakk> \<Longrightarrow> False
 6. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (5 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (bb, ba) \<in> R; case Inr x' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r bb\<rbrakk> \<Longrightarrow> Q x' bb
 2. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> Q' x2 ba
 3. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 4. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; (\<forall>(r', t')\<in>fst (g' x2 ba). \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' x2 ba))\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (4 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> Q' x2 ba
 2. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 3. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; (\<forall>(r', t')\<in>fst (g' x2 ba). \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' x2 ba))\<rbrakk> \<Longrightarrow> False
 4. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (5 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> P' b
 2. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; case Inr x2 of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q' r ba\<rbrakk> \<Longrightarrow> Q' x2 ba
 3. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 4. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; (\<forall>(r', t')\<in>fst (g' x2 ba). \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' x2 ba))\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (4 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; case Inr x2 of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q' r ba\<rbrakk> \<Longrightarrow> Q' x2 ba
 2. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 3. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; (\<forall>(r', t')\<in>fst (g' x2 ba). \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' x2 ba))\<rbrakk> \<Longrightarrow> False
 4. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (3 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 2. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; (\<forall>(r', t')\<in>fst (g' x2 ba). \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' x2 ba))\<rbrakk> \<Longrightarrow> False
 3. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b ba x2 bb x'. \<lbrakk>\<not> snd (f' b); P a; P' b; z; (Inr x2, ba) \<in> fst (f' b); snd (g' x2 ba); (Inr x', bb) \<in> fst (f a); (bb, ba) \<in> R; (\<forall>(r', t')\<in>fst (g' x2 ba). \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' x2 ba))\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift g') b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' x. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' x. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s'')\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((f \<sqinter> throw) a)
 2. \<And>a b aa ba s'' x. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s''); \<exists>(r, t)\<in>fst ((f \<sqinter> throw) a). (t, s'') \<in> R \<and> (dc \<oplus> r') r x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' x. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s''); \<exists>(r, t)\<in>fst ((f \<sqinter> throw) a). (t, s'') \<in> R \<and> (dc \<oplus> r') r x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' x ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s''); (ab, bb) \<in> fst (f a) \<or> ab = Inl undefined \<and> bb = a; (bb, s'') \<in> R; (dc \<oplus> r') ab x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' x ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s''); (bb, s'') \<in> R; (dc \<oplus> r') ab x; (ab, bb) \<in> fst (f a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 2. \<And>a b aa ba s'' x ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s''); (bb, s'') \<in> R; (dc \<oplus> r') ab x; ab = Inl undefined \<and> bb = a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' x ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s''); (bb, s'') \<in> R; (dc \<oplus> r') ab x; ab = Inl undefined \<and> bb = a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 2. \<And>a b aa ba s'' x ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s''); (bb, s'') \<in> R; (dc \<oplus> r') ab x; (ab, bb) \<in> fst (f a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b ba y'. \<lbrakk>(a, b) \<in> R; P a; P' b; (Inl y', ba) \<in> fst (f' b); (a, ba) \<in> R\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x')
 2. \<And>a b aa ba s'' x ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s''); (bb, s'') \<in> R; (dc \<oplus> r') ab x; (ab, bb) \<in> fst (f a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' x ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift g' x s''); (bb, s'') \<in> R; (dc \<oplus> r') ab x; (ab, bb) \<in> fst (f a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' x ab bb x1. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inl x'; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, s'') \<in> fst (f' b); x = Inl x1; (aa, ba) \<in> fst (throwError x1 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 2. \<And>a b aa ba s'' x ab bb x2. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inr x' \<and> r' x' x2; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); x = Inr x2; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x')
 2. \<And>a b aa ba s'' x ab bb x2. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inr x' \<and> r' x' x2; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); x = Inr x2; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b)\<rbrakk> \<Longrightarrow> case (Inl x', bb) of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x')
 2. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b)\<rbrakk> \<Longrightarrow> (Inl x', bb) \<in> fst ((f >>= lift g \<sqinter> throw) a)
 3. \<And>a b aa ba s'' x ab bb x2. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inr x' \<and> r' x' x2; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); x = Inr x2; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b)\<rbrakk> \<Longrightarrow> (Inl x', bb) \<in> fst ((f >>= lift g \<sqinter> throw) a)
 2. \<And>a b aa ba s'' x ab bb x2. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inr x' \<and> r' x' x2; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); x = Inr x2; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b); (Inl x', bb) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). (Inl x', bb) \<in> fst (case x of (x, xa) \<Rightarrow> lift g x xa)
 2. \<And>a b aa ba s'' x ab bb x2. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inr x' \<and> r' x' x2; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); x = Inr x2; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b); (Inl x', bb) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> (Inl x', bb) \<in> fst (case ?x131 a b ba bb x1 x' of (x, xa) \<Rightarrow> lift g x xa)
 2. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b); (Inl x', bb) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> ?x131 a b ba bb x1 x' \<in> fst (f a)
 3. \<And>a b aa ba s'' x ab bb x2. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inr x' \<and> r' x' x2; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); x = Inr x2; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b); (Inl x', bb) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> ?x131 a b ba bb x1 x' \<in> fst (f a)
 2. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b); (Inl x', bb) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> (Inl x', bb) \<in> fst (case ?x131 a b ba bb x1 x' of (x, xa) \<Rightarrow> lift g x xa)
 3. \<And>a b aa ba s'' x ab bb x2. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inr x' \<and> r' x' x2; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); x = Inr x2; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb x1 x'. \<lbrakk>(bb, ba) \<in> R; (Inl x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inl x1, ba) \<in> fst (f' b); (Inl x', bb) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> (Inl x', bb) \<in> fst (case (Inl x', bb) of (x, xa) \<Rightarrow> lift g x xa)
 2. \<And>a b aa ba s'' x ab bb x2. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inr x' \<and> r' x' x2; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); x = Inr x2; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' x ab bb x2. \<lbrakk>(bb, s'') \<in> R; \<exists>x'. ab = Inr x' \<and> r' x' x2; (ab, bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); x = Inr x2; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); r' x' x2\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); corres_underlying R False z (dc \<oplus> r) (Q x') (Q' x2) (g x' \<sqinter> throw) (g' x2)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> Q x' bb
 2. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> Q' x2 s''
 3. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> (?r'140 a b aa ba s'' bb x2 x', ?t'140 a b aa ba s'' bb x2 x') \<in> fst (g' x2 s'')
 4. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 5. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, ?t'140 a b aa ba s'' bb x2 x') \<in> R \<and> (dc \<oplus> r) ra (?r'140 a b aa ba s'' bb x2 x')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> P a
 2. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); case Inr x' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r bb\<rbrakk> \<Longrightarrow> Q x' bb
 3. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> Q' x2 s''
 4. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> (?r'140 a b aa ba s'' bb x2 x', ?t'140 a b aa ba s'' bb x2 x') \<in> fst (g' x2 s'')
 5. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 6. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, ?t'140 a b aa ba s'' bb x2 x') \<in> R \<and> (dc \<oplus> r) ra (?r'140 a b aa ba s'' bb x2 x')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); case Inr x' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r bb\<rbrakk> \<Longrightarrow> Q x' bb
 2. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> Q' x2 s''
 3. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> (?r'140 a b aa ba s'' bb x2 x', ?t'140 a b aa ba s'' bb x2 x') \<in> fst (g' x2 s'')
 4. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 5. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, ?t'140 a b aa ba s'' bb x2 x') \<in> R \<and> (dc \<oplus> r) ra (?r'140 a b aa ba s'' bb x2 x')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> Q' x2 s''
 2. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> (?r'140 a b aa ba s'' bb x2 x', ?t'140 a b aa ba s'' bb x2 x') \<in> fst (g' x2 s'')
 3. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 4. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, ?t'140 a b aa ba s'' bb x2 x') \<in> R \<and> (dc \<oplus> r) ra (?r'140 a b aa ba s'' bb x2 x')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> P' b
 2. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (aa, ba) \<in> fst (g' x2 s''); case Inr x2 of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q' r s''\<rbrakk> \<Longrightarrow> Q' x2 s''
 3. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> (?r'140 a b aa ba s'' bb x2 x', ?t'140 a b aa ba s'' bb x2 x') \<in> fst (g' x2 s'')
 4. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 5. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, ?t'140 a b aa ba s'' bb x2 x') \<in> R \<and> (dc \<oplus> r) ra (?r'140 a b aa ba s'' bb x2 x')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (aa, ba) \<in> fst (g' x2 s''); case Inr x2 of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q' r s''\<rbrakk> \<Longrightarrow> Q' x2 s''
 2. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> (?r'140 a b aa ba s'' bb x2 x', ?t'140 a b aa ba s'' bb x2 x') \<in> fst (g' x2 s'')
 3. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 4. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, ?t'140 a b aa ba s'' bb x2 x') \<in> R \<and> (dc \<oplus> r) ra (?r'140 a b aa ba s'' bb x2 x')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> (?r'140 a b aa ba s'' bb x2 x', ?t'140 a b aa ba s'' bb x2 x') \<in> fst (g' x2 s'')
 2. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 3. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, ?t'140 a b aa ba s'' bb x2 x') \<in> R \<and> (dc \<oplus> r) ra (?r'140 a b aa ba s'' bb x2 x')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s'')\<rbrakk> \<Longrightarrow> False \<longrightarrow> \<not> snd ((g x' \<sqinter> throw) bb)
 2. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' bb x2 x'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); \<exists>(ra, t)\<in>fst ((g x' \<sqinter> throw) bb). (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (ab, bc) \<in> fst (g x' bb) \<or> ab = Inl undefined \<and> bc = bb; (bc, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; (ab, bc) \<in> fst (g x' bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 2. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; ab = Inl undefined \<and> bc = bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; (ab, bc) \<in> fst (g x' bb)\<rbrakk> \<Longrightarrow> (ab, bc) \<in> fst ((f >>= lift g \<sqinter> throw) a)
 2. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; ab = Inl undefined \<and> bc = bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; (ab, bc) \<in> fst (g x' bb); (ab, bc) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> (ab, bc) \<in> fst ((f >>= lift g) a)
 2. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; ab = Inl undefined \<and> bc = bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; (ab, bc) \<in> fst (g x' bb); (ab, bc) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). (ab, bc) \<in> fst (case x of (x, xa) \<Rightarrow> lift g x xa)
 2. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; ab = Inl undefined \<and> bc = bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; (ab, bc) \<in> fst (g x' bb); (ab, bc) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> (ab, bc) \<in> fst (case ?x255 a b aa ba s'' bb x2 x' ab bc of (x, xa) \<Rightarrow> lift g x xa)
 2. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; (ab, bc) \<in> fst (g x' bb); (ab, bc) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> ?x255 a b aa ba s'' bb x2 x' ab bc \<in> fst (f a)
 3. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; ab = Inl undefined \<and> bc = bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; (ab, bc) \<in> fst (g x' bb); (ab, bc) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> ?x255 a b aa ba s'' bb x2 x' ab bc \<in> fst (f a)
 2. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; (ab, bc) \<in> fst (g x' bb); (ab, bc) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> (ab, bc) \<in> fst (case ?x255 a b aa ba s'' bb x2 x' ab bc of (x, xa) \<Rightarrow> lift g x xa)
 3. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; ab = Inl undefined \<and> bc = bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; (ab, bc) \<in> fst (g x' bb); (ab, bc) \<notin> fst (throw a)\<rbrakk> \<Longrightarrow> (ab, bc) \<in> fst (case (Inr x', bb) of (x, xa) \<Rightarrow> lift g x xa)
 2. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; ab = Inl undefined \<and> bc = bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s'' bb x2 x' ab bc. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (aa, ba) \<in> fst (g' x2 s''); (bc, ba) \<in> R; (dc \<oplus> r) ab aa; ab = Inl undefined \<and> bc = bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (Inl y', ba) \<in> fst (g' x2 s''); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x') proof (prove)
goal (1 subgoal):
 1. \<And>a b ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, b) \<in> R; P a; P' b; (Inr x2, s'') \<in> fst (f' b); (Inl y', ba) \<in> fst (g' x2 s''); (bb, ba) \<in> R; b = s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x') proof (prove)
goal (1 subgoal):
 1. \<And>a ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, s'') \<in> R; P a; P' s''; (Inr x2, s'') \<in> fst (f' s''); (Inl y', ba) \<in> fst (g' x2 s''); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x') proof (prove)
goal (2 subgoals):
 1. \<And>a ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, s'') \<in> R; P a; P' s''; (Inr x2, s'') \<in> fst (f' s''); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> s'' = ?s272 a ba s'' bb x2 x' y' \<and> Q' x2 s''
 2. \<And>a ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, s'') \<in> R; P a; P' s''; (Inr x2, s'') \<in> fst (f' s''); (bb, ba) \<in> R; case Inl y' of Inl e \<Rightarrow> ?s272 a ba s'' bb x2 x' y' = ba | Inr r \<Rightarrow> True\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x') proof (prove)
goal (2 subgoals):
 1. \<And>a ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, s'') \<in> R; P a; P' s''; (Inr x2, s'') \<in> fst (f' s''); (bb, ba) \<in> R\<rbrakk> \<Longrightarrow> Q' x2 s''
 2. \<And>a ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, s'') \<in> R; P a; P' s''; (Inr x2, s'') \<in> fst (f' s''); (bb, ba) \<in> R; case Inl y' of Inl e \<Rightarrow> s'' = ba | Inr r \<Rightarrow> True\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x') proof (prove)
goal (2 subgoals):
 1. \<And>a ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, s'') \<in> R; P a; P' s''; (bb, ba) \<in> R; case Inr x2 of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q' r s''\<rbrakk> \<Longrightarrow> Q' x2 s''
 2. \<And>a ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, s'') \<in> R; P a; P' s''; (Inr x2, s'') \<in> fst (f' s''); (bb, ba) \<in> R; case Inl y' of Inl e \<Rightarrow> s'' = ba | Inr r \<Rightarrow> True\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x') proof (prove)
goal (1 subgoal):
 1. \<And>a ba s'' bb x2 x' y'. \<lbrakk>(bb, s'') \<in> R; (Inr x', bb) \<in> fst (f a); (a, s'') \<in> R; P a; P' s''; (Inr x2, s'') \<in> fst (f' s''); (bb, ba) \<in> R; case Inl y' of Inl e \<Rightarrow> s'' = ba | Inr r \<Rightarrow> True\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= lift g \<sqinter> throw) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x') proof (prove)
goal:
No subgoals!