theory Prefix_Refinement

lemma self_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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s'
            (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s')
    \<Longrightarrow> Q = matching_self_cond (ctr' @ ctr)
    \<Longrightarrow> cres = Incomplete \<longrightarrow> ctr' = []
    \<Longrightarrow> self_closed Q s (mbind f g s0)" apply (frule is_matching_fragment_self_closed) apply (subst self_closed_def, clarsimp simp: mbind_def) apply (rename_tac tr res) apply (strengthen in_fst_snd_image, simp) apply (frule(1) is_matching_fragment_trD) apply (case_tac "length tr < length ctr") apply clarsimp apply (drule(1) self_closedD) apply (simp add: trans[OF nth_append if_P]) apply clarsimp apply (thin_tac "(x, Incomplete) \<in> S" for x S) apply (strengthen rev_bexI[mk_strg I E]) apply (clarsimp split: tmres.split) apply (fastforce elim: image_eqI[rotated] intro: in_mres) apply (clarsimp simp: matching_tr_pfx_def) apply (erule tmres.rel_cases; clarsimp) apply (drule spec2, drule spec, drule(1) mp) apply clarsimp apply (drule(1) self_closedD) apply (simp add: trans[OF nth_append if_not_P]) apply (strengthen rev_bexI[mk_strg I E]) apply simp 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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length (ctr' @ ctr) \<and> fst (rev (ctr' @ ctr) ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []\<rbrakk> \<Longrightarrow> self_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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length (ctr' @ ctr) \<and> fst (rev (ctr' @ ctr) ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f\<rbrakk> \<Longrightarrow> self_closed Q s (mbind f g s0) proof (prove)
goal (1 subgoal):
 1. \<And>xs a b. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (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); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me\<rbrakk> \<Longrightarrow> \<exists>s'. (Me, 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me\<rbrakk> \<Longrightarrow> \<exists>s'. (Me, 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres)\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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>tr. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, Incomplete) \<in> f s; fst ((rev ctr @ rev ctr') ! length tr) = Me; length tr < length ctr; rely_cond R s0 tr; matching_tr_pfx sr tr ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # tr, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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>tr. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; (tr, Incomplete) \<in> f s; fst ((rev ctr @ rev ctr') ! length tr) = Me; length tr < length ctr; rely_cond R s0 tr; matching_tr_pfx sr tr ctr\<rbrakk> \<Longrightarrow> length tr < length ctr \<and> fst (rev ctr ! length tr) = Me
 2. \<And>tr. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; (tr, Incomplete) \<in> f s; fst ((rev ctr @ rev ctr') ! length tr) = Me; length tr < length ctr; rely_cond R s0 tr; matching_tr_pfx sr tr ctr; \<exists>s'. (Me, s') # tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # tr, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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>tr. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; (tr, Incomplete) \<in> f s; fst ((rev ctr @ rev ctr') ! length tr) = Me; length tr < length ctr; rely_cond R s0 tr; matching_tr_pfx sr tr ctr; \<exists>s'. (Me, s') # tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # tr, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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>tr s' b. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; (tr, Incomplete) \<in> f s; fst ((rev ctr @ rev ctr') ! length tr) = Me; length tr < length ctr; rely_cond R s0 tr; matching_tr_pfx sr tr ctr; ((Me, s') # tr, b) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # tr, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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>tr s' b. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; fst ((rev ctr @ rev ctr') ! length tr) = Me; length tr < length ctr; rely_cond R s0 tr; matching_tr_pfx sr tr ctr; ((Me, s') # tr, b) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # tr, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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>tr s' b. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; fst ((rev ctr @ rev ctr') ! length tr) = Me; length tr < length ctr; rely_cond R s0 tr; matching_tr_pfx sr tr ctr; ((Me, s') # tr, b) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x xa. ((Me, x) # tr, xa) \<in> (case ((Me, s') # 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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>tr s' a ba. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; fst ((rev ctr @ rev ctr') ! length tr) = Me; length tr < length ctr; rely_cond R s0 tr; matching_tr_pfx sr tr ctr; ((Me, s') # tr, Result (a, ba)) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x xa. ((Me, x) # tr, xa) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ (Me, s') # tr, x)) ` g s' a ba
 2. \<And>xs tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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 tr res. \<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> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); cres = Incomplete \<longrightarrow> ctr' = []; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, res) \<in> f s; (xs, Incomplete) \<in> (case res of Failed \<Rightarrow> {(tr, Failed)} | Incomplete \<Rightarrow> {(tr, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ tr, y)) ` g (last_st_tr tr s0) rv s); length xs < length ctr' + length ctr; fst ((rev ctr @ rev ctr') ! length xs) = Me; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); rel_tmres osr rvr res cres\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # xs, y) \<in> (case xa 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>tr a b aa ba ab. \<lbrakk>is_matching_fragment sr osr rvr ctr (Result (aa, ba)) s0 R s f; \<forall>tr x s'. (tr, Result (x, s')) \<in> f s \<longrightarrow> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (g (last_st_tr tr s0) x) \<and> [] \<in> fst ` g (last_st_tr tr s0) x s'; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, Result (a, b)) \<in> f s; length ab < length ctr'; fst ((rev ctr @ rev ctr') ! (length ab + length ctr)) = Me; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); cres = Result (aa, ba); (ab, Incomplete) \<in> g (last_st_tr tr s0) a b; rvr a aa; osr b ba\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # ab @ tr, y) \<in> (case xa 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>tr a b aa ba ab. \<lbrakk>is_matching_fragment sr osr rvr ctr (Result (aa, ba)) s0 R s f; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, Result (a, b)) \<in> f s; length ab < length ctr'; fst ((rev ctr @ rev ctr') ! (length ab + length ctr)) = Me; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); cres = Result (aa, ba); (ab, Incomplete) \<in> g (last_st_tr tr s0) a b; rvr a aa; osr b ba; self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) b (g (last_st_tr tr s0) a) \<and> [] \<in> fst ` g (last_st_tr tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # ab @ tr, y) \<in> (case xa 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>tr a b aa ba ab bb. \<lbrakk>is_matching_fragment sr osr rvr ctr (Result (aa, ba)) s0 R s f; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, Result (a, b)) \<in> f s; length ab < length ctr'; fst ((rev ctr @ rev ctr') ! (length ab + length ctr)) = Me; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); cres = Result (aa, ba); (ab, Incomplete) \<in> g (last_st_tr tr s0) a b; rvr a aa; osr b ba; self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) b (g (last_st_tr tr s0) a); ([], bb) \<in> g (last_st_tr tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # ab @ tr, y) \<in> (case xa 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>tr a b aa ba ab bb. \<lbrakk>is_matching_fragment sr osr rvr ctr (Result (aa, ba)) s0 R s f; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, Result (a, b)) \<in> f s; length ab < length ctr'; fst ((rev ctr @ rev ctr') ! (length ab + length ctr)) = Me; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); cres = Result (aa, ba); (ab, Incomplete) \<in> g (last_st_tr tr s0) a b; rvr a aa; osr b ba; ([], bb) \<in> g (last_st_tr tr s0) a b\<rbrakk> \<Longrightarrow> length ab < length ctr' \<and> fst (rev ctr' ! length ab) = Me
 2. \<And>tr a b aa ba ab bb. \<lbrakk>is_matching_fragment sr osr rvr ctr (Result (aa, ba)) s0 R s f; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, Result (a, b)) \<in> f s; length ab < length ctr'; fst ((rev ctr @ rev ctr') ! (length ab + length ctr)) = Me; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); cres = Result (aa, ba); (ab, Incomplete) \<in> g (last_st_tr tr s0) a b; rvr a aa; osr b ba; ([], bb) \<in> g (last_st_tr tr s0) a b; \<exists>s'. (Me, s') # ab \<in> fst ` g (last_st_tr tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # ab @ tr, y) \<in> (case xa 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>tr a b aa ba ab bb. \<lbrakk>is_matching_fragment sr osr rvr ctr (Result (aa, ba)) s0 R s f; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, Result (a, b)) \<in> f s; length ab < length ctr'; fst ((rev ctr @ rev ctr') ! (length ab + length ctr)) = Me; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); cres = Result (aa, ba); (ab, Incomplete) \<in> g (last_st_tr tr s0) a b; rvr a aa; osr b ba; ([], bb) \<in> g (last_st_tr tr s0) a b; \<exists>s'. (Me, s') # ab \<in> fst ` g (last_st_tr tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x y. \<exists>xa\<in>f s. ((Me, x) # ab @ tr, y) \<in> (case xa 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>tr a b aa ba ab bb. \<lbrakk>is_matching_fragment sr osr rvr ctr (Result (aa, ba)) s0 R s f; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, Result (a, b)) \<in> f s; length ab < length ctr'; fst ((rev ctr @ rev ctr') ! (length ab + length ctr)) = Me; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); cres = Result (aa, ba); (ab, Incomplete) \<in> g (last_st_tr tr s0) a b; rvr a aa; osr b ba; ([], bb) \<in> g (last_st_tr tr s0) a b; \<exists>s'. (Me, s') # ab \<in> fst ` g (last_st_tr tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x xa. ((Me, x) # ab @ tr, xa) \<in> (case (tr, Result (a, 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) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b aa ba ab bb. \<lbrakk>is_matching_fragment sr osr rvr ctr (Result (aa, ba)) s0 R s f; Q = (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me); self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; (tr, Result (a, b)) \<in> f s; length ab < length ctr'; fst ((rev ctr @ rev ctr') ! (length ab + length ctr)) = Me; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); cres = Result (aa, ba); (ab, Incomplete) \<in> g (last_st_tr tr s0) a b; rvr a aa; osr b ba; ([], bb) \<in> g (last_st_tr tr s0) a b; \<exists>s'. (Me, s') # ab \<in> fst ` g (last_st_tr tr s0) a b\<rbrakk> \<Longrightarrow> \<exists>x xa. ((Me, x) # ab @ tr, xa) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ tr, x)) ` g (last_st_tr tr s0) a b proof (prove)
goal:
No subgoals!