theory Prefix_Refinement

lemma env_closed_mbind:
  "is_matching_fragment sr osr rvr ctr' cres s0 R s f
    \<Longrightarrow> \<forall>tr x s'. (tr, Result (x, s')) \<in> f s
        \<longrightarrow> env_closed (matching_env_cond sr ctr'' (last_st_tr tr s0) R) s' (g (last_st_tr tr s0) x)
            \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'
    \<Longrightarrow> (if cres \<in> {Incomplete, Failed} then ctr = ctr' else ctr = ctr'' @ ctr')
    \<Longrightarrow> Q = matching_env_cond sr ctr s0 R
    \<Longrightarrow> env_closed Q s (mbind f g s0)" apply (simp add: if_bool_eq_conj) apply (subst env_closed_def, clarsimp simp: mbind_def) apply (strengthen in_fst_snd_image, simp) apply (rename_tac f_tr f_res s') apply (case_tac "f_res = Incomplete") apply (frule(1) is_matching_fragment_trD) apply clarsimp apply (drule is_matching_fragment_env_closed) apply (drule_tac s'=s' in env_closedD, assumption) apply (clarsimp simp: matching_tr_pfx_aCons matching_tr_pfx_def) apply (cases cres; clarsimp) apply clarsimp apply (strengthen bexI[where x="(x # xs, r)" for x xs r, mk_strg I _ E]) apply (simp split: tmres.split) apply clarsimp apply (drule spec2, drule spec, drule(1) mp) apply clarsimp apply (strengthen image_eqI[mk_strg I _ E]) apply simp apply (frule(1) is_matching_fragment_trD) apply (case_tac f_res; clarsimp) apply (cases cres; clarsimp simp: matching_tr_pfx_def) apply (strengthen bexI[mk_strg I _ E], simp) apply (drule spec2, drule spec, drule(1) mp)+ apply clarsimp apply (drule_tac s'=s' in env_closedD, assumption) apply (simp add: rely_cond_append rely_cond_Cons_eq matching_tr_pfx_aCons) apply (clarsimp simp: nth_append) apply (clarsimp simp: matching_tr_def list_all2_append) apply clarsimp apply (fastforce elim: image_eqI[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; if cres \<in> {Incomplete, Failed} then ctr = ctr' else ctr = ctr'' @ ctr'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs))\<rbrakk> \<Longrightarrow> env_closed Q s (mbind f g s0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; (cres = Incomplete \<longrightarrow> ctr = ctr') \<and> (cres = Failed \<longrightarrow> ctr = ctr') \<and> (cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'); Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs))\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (mbind f g s0) proof (prove)
goal (1 subgoal):
 1. \<And>xs a b s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (a, b) \<in> f s; (xs, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(aa, y). (aa @ a, y)) ` g (last_st_tr a s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs)\<rbrakk> \<Longrightarrow> (Env, s') # xs \<in> fst ` (\<Union>x\<in>f s. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>xs a b s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (a, b) \<in> f s; (xs, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(aa, y). (aa @ a, y)) ` g (last_st_tr a s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs)\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs)\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res = Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res = Incomplete; rely_cond R s0 f_tr \<and> matching_tr_pfx sr f_tr ctr' \<and> (length f_tr < length ctr' \<longrightarrow> f_res = Incomplete) \<and> (length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr f_res cres)\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # f_tr, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s'. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr' \<and> rely_cond R s0 ((Env, s) # xs)) s f\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # f_tr, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (3 subgoals):
 1. \<And>f_tr s'. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres\<rbrakk> \<Longrightarrow> matching_tr_pfx sr ((Env, s') # f_tr) ctr' \<and> rely_cond R s0 ((Env, s') # f_tr)
 2. \<And>f_tr s'. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; (Env, s') # f_tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # f_tr, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 3. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (3 subgoals):
 1. \<And>f_tr s'. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. Suc (length xs) \<le> length ctr'' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr'')) \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr)) \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; Suc (length f_tr) \<le> length ctr; matching_tr sr (rev f_tr @ [(Env, s')]) (take (Suc (length f_tr)) (rev ctr)); length f_tr \<le> length ctr'; matching_tr sr (rev f_tr) (take (length f_tr) (rev ctr'))\<rbrakk> \<Longrightarrow> Suc (length f_tr) \<le> length ctr' \<and> matching_tr sr (rev f_tr @ [(Env, s')]) (take (Suc (length f_tr)) (rev ctr'))
 2. \<And>f_tr s'. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; (Env, s') # f_tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # f_tr, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 3. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s'. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; (Env, s') # f_tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # f_tr, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' b. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; ((Env, s') # f_tr, b) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # f_tr, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' b. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; ((Env, s') # f_tr, b) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # f_tr, x) \<in> (case ((Env, s') # f_tr, b) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' b. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; ((Env, s') # f_tr, b) \<in> f s\<rbrakk> \<Longrightarrow> \<forall>a ba. b = Result (a, ba) \<longrightarrow> (\<exists>x. ((Env, s') # f_tr, x) \<in> (\<lambda>(a, y). (a @ (Env, s') # f_tr, y)) ` g s' a ba)
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' a ba. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; ((Env, s') # f_tr, Result (a, ba)) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ (Env, s') # f_tr, x)) ` g s' a ba
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' a ba. \<lbrakk>Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; ((Env, s') # f_tr, Result (a, ba)) \<in> f s; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr ((Env, s') # f_tr) s0) ((Env, s) # xs)) ba (g (last_st_tr ((Env, s') # f_tr) s0) a) \<and> [] \<in> fst ` g (last_st_tr ((Env, s') # f_tr) s0) a ba\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ (Env, s') # f_tr, x)) ` g s' a ba
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' a ba b. \<lbrakk>Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; ((Env, s') # f_tr, Result (a, ba)) \<in> f s; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R s' ((Env, s) # xs)) ba (g s' a); ([], b) \<in> g s' a ba\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ (Env, s') # f_tr, x)) ` g s' a ba
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' a ba b. \<lbrakk>Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Incomplete) \<in> f s; matching_tr_pfx sr ((Env, s') # f_tr) ctr; rely_cond R s0 ((Env, s') # f_tr); rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr Incomplete cres; ((Env, s') # f_tr, Result (a, ba)) \<in> f s; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R s' ((Env, s) # xs)) ba (g s' a); ([], b) \<in> g s' a ba\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # f_tr, x) = (case ([], b) of (a, x) \<Rightarrow> (a @ (Env, s') # f_tr, x))
 2. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>xs f_tr f_res s'. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, f_res) \<in> f s; (xs, Incomplete) \<in> (case f_res of Failed \<Rightarrow> {(f_tr, Failed)} | Incomplete \<Rightarrow> {(f_tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ f_tr, y)) ` g (last_st_tr f_tr s0) rv s); matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs); f_res \<noteq> Incomplete; rely_cond R s0 f_tr \<and> matching_tr_pfx sr f_tr ctr' \<and> (length f_tr < length ctr' \<longrightarrow> f_res = Incomplete) \<and> (length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr f_res cres)\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # xs, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>f_tr s' a b aa. \<lbrakk>is_matching_fragment sr osr rvr ctr' cres s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr'' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)); cres = Incomplete \<longrightarrow> ctr = ctr'; cres = Failed \<longrightarrow> ctr = ctr'; cres \<noteq> Incomplete \<and> cres \<noteq> Failed \<longrightarrow> ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; matching_tr_pfx sr ((Env, s') # aa @ f_tr) ctr; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; matching_tr_pfx sr f_tr ctr'; \<not> length f_tr < length ctr'; length f_tr = length ctr' \<longrightarrow> rel_tmres osr rvr (Result (a, b)) cres\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # aa @ f_tr, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>f_tr s' a b aa ab ba. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. Suc (length xs) \<le> length ctr'' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr'')) \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>f s. ((Env, s') # aa @ f_tr, y) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>f_tr s' a b aa ab ba. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> env_closed (\<lambda>xs s. Suc (length xs) \<le> length ctr'' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr'')) \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # aa @ f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ f_tr, x)) ` g (last_st_tr f_tr s0) a b proof (prove)
goal (1 subgoal):
 1. \<And>f_tr s' a b aa ab ba. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; env_closed (\<lambda>xs s. Suc (length xs) \<le> length ctr'' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr'')) \<and> rely_cond R (last_st_tr f_tr s0) ((Env, s) # xs)) b (g (last_st_tr f_tr s0) a) \<and> [] \<in> fst ` g (last_st_tr f_tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # aa @ f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ f_tr, x)) ` g (last_st_tr f_tr s0) a b proof (prove)
goal (1 subgoal):
 1. \<And>f_tr s' a b aa ab ba bb. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; env_closed (\<lambda>xs s. Suc (length xs) \<le> length ctr'' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr'')) \<and> rely_cond R (last_st_tr f_tr s0) ((Env, s) # xs)) b (g (last_st_tr f_tr s0) a); ([], bb) \<in> g (last_st_tr f_tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # aa @ f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ f_tr, x)) ` g (last_st_tr f_tr s0) a b proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' a b aa ab ba bb. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; ([], bb) \<in> g (last_st_tr f_tr s0) a b\<rbrakk> \<Longrightarrow> Suc (length aa) \<le> length ctr'' \<and> matching_tr sr (rev aa @ [(Env, s')]) (take (Suc (length aa)) (rev ctr'')) \<and> rely_cond R (last_st_tr f_tr s0) ((Env, s') # aa)
 2. \<And>f_tr s' a b aa ab ba bb. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; ([], bb) \<in> g (last_st_tr f_tr s0) a b; (Env, s') # aa \<in> fst ` g (last_st_tr f_tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # aa @ f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ f_tr, x)) ` g (last_st_tr f_tr s0) a b proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' a b aa ab ba bb. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 xs \<and> R (last_st_tr xs s0) s); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R (last_st_tr f_tr s0) aa \<and> R (last_st_tr aa (last_st_tr f_tr s0)) s'; (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; ([], bb) \<in> g (last_st_tr f_tr s0) a b\<rbrakk> \<Longrightarrow> matching_tr sr (rev aa @ [(Env, s')]) (take (Suc (length aa)) (rev ctr''))
 2. \<And>f_tr s' a b aa ab ba bb. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; ([], bb) \<in> g (last_st_tr f_tr s0) a b; (Env, s') # aa \<in> fst ` g (last_st_tr f_tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # aa @ f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ f_tr, x)) ` g (last_st_tr f_tr s0) a b proof (prove)
goal (2 subgoals):
 1. \<And>f_tr s' a b aa ab ba bb. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 xs \<and> R (last_st_tr xs s0) s); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; ([], bb) \<in> g (last_st_tr f_tr s0) a b; rely_cond R (last_st_tr f_tr s0) aa; R (last_st_tr aa (last_st_tr f_tr s0)) s'\<rbrakk> \<Longrightarrow> matching_tr sr (rev aa @ [(Env, s')]) (take (Suc (length aa)) (rev ctr''))
 2. \<And>f_tr s' a b aa ab ba bb. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; ([], bb) \<in> g (last_st_tr f_tr s0) a b; (Env, s') # aa \<in> fst ` g (last_st_tr f_tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # aa @ f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ f_tr, x)) ` g (last_st_tr f_tr s0) a b proof (prove)
goal (1 subgoal):
 1. \<And>f_tr s' a b aa ab ba bb. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; ([], bb) \<in> g (last_st_tr f_tr s0) a b; (Env, s') # aa \<in> fst ` g (last_st_tr f_tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # aa @ f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ f_tr, x)) ` g (last_st_tr f_tr s0) a b proof (prove)
goal (1 subgoal):
 1. \<And>f_tr s' a b aa ab ba bb bc. \<lbrakk>is_matching_fragment sr osr rvr ctr' (Result (ab, ba)) s0 R s f; Q = (\<lambda>xs s. Suc (length xs) \<le> length ctr'' + length ctr' \<and> matching_tr sr (rev xs @ [(Env, s)]) (take (Suc (length xs)) (rev ctr') @ take (Suc (length xs) - length ctr') (rev ctr'')) \<and> rely_cond R s0 ((Env, s) # xs)); ctr = ctr'' @ ctr'; (f_tr, Result (a, b)) \<in> f s; rely_cond R s0 ((Env, s') # aa @ f_tr); (aa, Incomplete) \<in> g (last_st_tr f_tr s0) a b; rely_cond R s0 f_tr; cres = Result (ab, ba); Suc (length aa) \<le> length ctr''; matching_tr sr (rev f_tr @ rev aa @ [(Env, s')]) (rev ctr' @ take (Suc (length aa)) (rev ctr'')); length f_tr = length ctr'; matching_tr sr (rev f_tr) (rev ctr'); rvr a ab; osr b ba; ([], bb) \<in> g (last_st_tr f_tr s0) a b; ((Env, s') # aa, bc) \<in> g (last_st_tr f_tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x. ((Env, s') # aa @ f_tr, x) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ f_tr, x)) ` g (last_st_tr f_tr s0) a b proof (prove)
goal:
No subgoals!