theory Prefix_Refinement

theorem matching_fragment_matching_tr:
  assumes match: "is_matching_fragment sr osr rvr ctr cres s0 R' s f"
  and rely: "rely_cond R t0 ctr"
  and sr0: "sr s0 t0"
  and sr: "(\<forall>s t t'. sr s t \<longrightarrow> R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> R' s s'))"
  shows "\<exists>(atr, ares) \<in> f s. matching_tr sr atr ctr
                    \<and> rel_tmres osr rvr ares cres
                    \<and> rely_cond R' s0 atr" proof - note pfx_closed = is_matching_fragment_prefix_closed[OF match] note f_prop = is_matching_fragment_trD[OF match] note env_closed = is_matching_fragment_env_closed[OF match] note self_closed = is_matching_fragment_self_closed[OF match] note pfx_closedD = pfx_closed[THEN prefix_closedD] have extend:
    "\<And>tmid s' tr res. ((tmid, s') # tr, res) \<in> f s \<Longrightarrow> rely_cond R' s0 tr
        \<Longrightarrow> \<exists>x res. (x # tr, res) \<in> f s \<and> rely_cond R' s0 (x # tr)" apply (case_tac tmid) apply (fastforce simp: rely_cond_Cons) apply (frule f_prop[OF pfx_closedD], clarsimp) apply (frule f_prop, clarsimp simp: matching_tr_pfx_aCons) apply (frule rely_cond_nth[rotated], rule rely, simp) apply (drule_tac s="last_st_tr tr s0" in sr[rule_format, rotated]) apply (clarsimp simp: sr0 neq_Nil_conv matching_tr_pfx_aCons) apply clarsimp apply (rename_tac t' s'_rely) apply (drule_tac s'="s'_rely" in env_closedD[where f=f, OF env_closed, OF prefix_closedD[OF pfx_closed]]) apply (clarsimp simp: matching_tr_pfx_aCons rely_cond_Cons_eq) apply clarsimp apply (fastforce intro!: rely_cond_Cons) done have extend2:
    "\<And>tr res. (tr, res) \<in> f s \<Longrightarrow> rely_cond R' s0 tr
        \<Longrightarrow> length tr < length ctr
        \<Longrightarrow> \<exists>x res. (x # tr, res) \<in> f s \<and> rely_cond R' s0 (x # tr)" apply (frule f_prop, clarsimp) apply (case_tac "fst (rev ctr ! length tr)") apply (frule self_closed[THEN self_closedD], simp) apply (fastforce intro: rely_cond_Cons) apply (frule rely_cond_nth[rotated], rule rely, simp) apply (drule_tac s="last_st_tr tr s0" in sr[rule_format, rotated]) apply (clarsimp simp: sr0 neq_Nil_conv matching_tr_pfx_aCons) apply clarsimp apply (drule_tac s'=s' in env_closedD[OF env_closed]) apply (simp add: matching_tr_pfx_aCons prod_eq_iff rely_cond_Cons) apply (fastforce intro: rely_cond_Cons) done { fix n have "\<exists>(tr, res) \<in> f s. (n \<le> length ctr \<longrightarrow> length tr = n)
        \<and> rely_cond R' s0 tr" apply (induct n) apply (cut_tac f=f in is_matching_fragment_Nil;
          (rule sr0 match)?) apply fastforce apply clarsimp apply (case_tac "\<not> (Suc n \<le> length ctr)") apply fastforce apply clarsimp apply (drule(1) extend2, simp) apply (fastforce elim: rev_bexI) done } note induct = this[rule_format] show ?thesis using induct[where n="length ctr"] apply clarsimp apply (rule rev_bexI, assumption) apply clarsimp apply (frule is_matching_fragment_trD[OF match]) apply (clarsimp simp: matching_tr_pfx_def matching_tr_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
this:
prefix_closed f

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
this:
(?tr, ?res) \<in> f s \<Longrightarrow> 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)

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
this:
env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R' s0 ((Env, s) # xs)) s f

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
this:
self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
this:
(?x # ?xs, ?y) \<in> f ?s \<Longrightarrow> (?xs, Incomplete) \<in> f ?s

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
goal (1 subgoal):
 1. \<And>tmid s' tr res. \<lbrakk>((tmid, s') # tr, res) \<in> f s; rely_cond R' s0 tr\<rbrakk> \<Longrightarrow> \<exists>x res. (x # tr, res) \<in> f s \<and> rely_cond R' s0 (x # tr) proof (prove)
goal (2 subgoals):
 1. \<And>tmid s' tr res. \<lbrakk>((tmid, s') # tr, res) \<in> f s; rely_cond R' s0 tr; tmid = Me\<rbrakk> \<Longrightarrow> \<exists>x res. (x # tr, res) \<in> f s \<and> rely_cond R' s0 (x # tr)
 2. \<And>tmid s' tr res. \<lbrakk>((tmid, s') # tr, res) \<in> f s; rely_cond R' s0 tr; tmid = Env\<rbrakk> \<Longrightarrow> \<exists>x res. (x # tr, res) \<in> f s \<and> rely_cond R' s0 (x # tr) proof (prove)
goal (1 subgoal):
 1. \<And>tmid s' tr res. \<lbrakk>((tmid, s') # tr, res) \<in> f s; rely_cond R' s0 tr; tmid = Env\<rbrakk> \<Longrightarrow> \<exists>x res. (x # tr, res) \<in> f s \<and> rely_cond R' s0 (x # tr) proof (prove)
goal (1 subgoal):
 1. \<And>s' tr res. \<lbrakk>((Env, s') # tr, res) \<in> f s; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; length tr = length ctr \<longrightarrow> rel_tmres osr rvr Incomplete cres\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>s' tr res s'a. \<lbrakk>((Env, s') # tr, res) \<in> f s; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, s'a); sr s' s'a\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>s' tr res s'a. \<lbrakk>((Env, s') # tr, res) \<in> f s; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, s'a); sr s' s'a; R (if tr = [] then t0 else snd (rev ctr ! (length tr - 1))) s'a\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (2 subgoals):
 1. \<And>s' tr res s'a. \<lbrakk>((Env, s') # tr, res) \<in> f s; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, s'a); sr s' s'a\<rbrakk> \<Longrightarrow> sr (last_st_tr tr s0) (if tr = [] then t0 else snd (rev ctr ! (length tr - 1)))
 2. \<And>s' tr res s'a. \<lbrakk>((Env, s') # tr, res) \<in> f s; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, s'a); sr s' s'a; \<exists>s'. sr s' s'a \<and> R' (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>s' tr res s'a. \<lbrakk>((Env, s') # tr, res) \<in> f s; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, s'a); sr s' s'a; \<exists>s'. sr s' s'a \<and> R' (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>s' tr res s'a s'b. \<lbrakk>((Env, s') # tr, res) \<in> f s; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, s'a); sr s' s'a; sr s'b s'a; R' (last_st_tr tr s0) s'b\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>s' tr res t' s'_rely. \<lbrakk>((Env, s') # tr, res) \<in> f s; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, t'); sr s' t'; sr s'_rely t'; R' (last_st_tr tr s0) s'_rely\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (2 subgoals):
 1. \<And>s' tr res t' s'_rely. \<lbrakk>rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, t'); sr s' t'; sr s'_rely t'; R' (last_st_tr tr s0) s'_rely\<rbrakk> \<Longrightarrow> matching_tr_pfx sr ((Env, s'_rely) # tr) ctr \<and> rely_cond R' s0 ((Env, s'_rely) # tr)
 2. \<And>s' tr res t' s'_rely. \<lbrakk>rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, t'); sr s' t'; sr s'_rely t'; R' (last_st_tr tr s0) s'_rely; (Env, s'_rely) # tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>s' tr res t' s'_rely. \<lbrakk>rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, t'); sr s' t'; sr s'_rely t'; R' (last_st_tr tr s0) s'_rely; (Env, s'_rely) # tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>s' tr res t' s'_rely b. \<lbrakk>rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; rely_cond R' s0 ((Env, s') # tr); length tr < length ctr; Suc (length tr) < length ctr \<longrightarrow> res = Incomplete; Suc (length tr) = length ctr \<longrightarrow> rel_tmres osr rvr res cres; rev ctr ! length tr = (Env, t'); sr s' t'; sr s'_rely t'; R' (last_st_tr tr s0) s'_rely; ((Env, s'_rely) # tr, b) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>((?tmid, ?s') # ?tr, ?res) \<in> f s; rely_cond R' s0 ?tr\<rbrakk> \<Longrightarrow> \<exists>x res. (x # ?tr, res) \<in> f s \<and> rely_cond R' s0 (x # ?tr)

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
goal (1 subgoal):
 1. \<And>tr res. \<lbrakk>(tr, res) \<in> f s; rely_cond R' s0 tr; length tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x res. (x # tr, res) \<in> f s \<and> rely_cond R' s0 (x # tr) proof (prove)
goal (1 subgoal):
 1. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (2 subgoals):
 1. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Me\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr)
 2. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (2 subgoals):
 1. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Me; \<exists>s'. (Me, s') # tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr)
 2. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env; R (if tr = [] then t0 else snd (rev ctr ! (length tr - 1))) (snd (rev ctr ! length tr))\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (2 subgoals):
 1. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env\<rbrakk> \<Longrightarrow> sr (last_st_tr tr s0) (if tr = [] then t0 else snd (rev ctr ! (length tr - 1)))
 2. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env; \<exists>s'. sr s' (snd (rev ctr ! length tr)) \<and> R' (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>tr. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env; \<exists>s'. sr s' (snd (rev ctr ! length tr)) \<and> R' (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>tr s'. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env; sr s' (snd (rev ctr ! length tr)); R' (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (2 subgoals):
 1. \<And>tr s'. \<lbrakk>length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env; sr s' (snd (rev ctr ! length tr)); R' (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> matching_tr_pfx sr ((Env, s') # tr) ctr \<and> rely_cond R' s0 ((Env, s') # tr)
 2. \<And>tr s'. \<lbrakk>length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env; sr s' (snd (rev ctr ! length tr)); R' (last_st_tr tr s0) s'; (Env, s') # tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal (1 subgoal):
 1. \<And>tr s'. \<lbrakk>length tr < length ctr; rely_cond R' s0 tr; matching_tr_pfx sr tr ctr; fst (rev ctr ! length tr) = Env; sr s' (snd (rev ctr ! length tr)); R' (last_st_tr tr s0) s'; (Env, s') # tr \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>res. ((a, b) # tr, res) \<in> f s) \<and> rely_cond R' s0 ((a, b) # tr) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>(?tr, ?res) \<in> f s; rely_cond R' s0 ?tr; length ?tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x res. (x # ?tr, res) \<in> f s \<and> rely_cond R' s0 (x # ?tr)

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
this:
\<lbrakk>(?tr, ?res) \<in> f s; rely_cond R' s0 ?tr; length ?tr < length ctr\<rbrakk> \<Longrightarrow> \<exists>x res. (x # ?tr, res) \<in> f s \<and> rely_cond R' s0 (x # ?tr)

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
goal (1 subgoal):
 1. \<exists>(tr, res)\<in>f s. (n \<le> length ctr \<longrightarrow> length tr = n) \<and> rely_cond R' s0 tr proof (prove)
goal (2 subgoals):
 1. \<exists>a\<in>f s. case a of (tr, res) \<Rightarrow> (0 \<le> length ctr \<longrightarrow> length tr = 0) \<and> rely_cond R' s0 tr
 2. \<And>n. \<exists>a\<in>f s. case a of (tr, res) \<Rightarrow> (n \<le> length ctr \<longrightarrow> length tr = n) \<and> rely_cond R' s0 tr \<Longrightarrow> \<exists>a\<in>f s. case a of (tr, res) \<Rightarrow> (Suc n \<le> length ctr \<longrightarrow> length tr = Suc n) \<and> rely_cond R' s0 tr proof (prove)
goal (2 subgoals):
 1. [] \<in> fst ` f s \<Longrightarrow> \<exists>a\<in>f s. case a of (tr, res) \<Rightarrow> (0 \<le> length ctr \<longrightarrow> length tr = 0) \<and> rely_cond R' s0 tr
 2. \<And>n. \<exists>a\<in>f s. case a of (tr, res) \<Rightarrow> (n \<le> length ctr \<longrightarrow> length tr = n) \<and> rely_cond R' s0 tr \<Longrightarrow> \<exists>a\<in>f s. case a of (tr, res) \<Rightarrow> (Suc n \<le> length ctr \<longrightarrow> length tr = Suc n) \<and> rely_cond R' s0 tr proof (prove)
goal (1 subgoal):
 1. \<And>n. \<exists>a\<in>f s. case a of (tr, res) \<Rightarrow> (n \<le> length ctr \<longrightarrow> length tr = n) \<and> rely_cond R' s0 tr \<Longrightarrow> \<exists>a\<in>f s. case a of (tr, res) \<Rightarrow> (Suc n \<le> length ctr \<longrightarrow> length tr = Suc n) \<and> rely_cond R' s0 tr proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>(a, b) \<in> f s; n \<le> length ctr \<longrightarrow> length a = n; rely_cond R' s0 a\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. case x of (tr, res) \<Rightarrow> (Suc n \<le> length ctr \<longrightarrow> length tr = Suc n) \<and> rely_cond R' s0 tr proof (prove)
goal (2 subgoals):
 1. \<And>n a b. \<lbrakk>(a, b) \<in> f s; n \<le> length ctr \<longrightarrow> length a = n; rely_cond R' s0 a; \<not> Suc n \<le> length ctr\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. case x of (tr, res) \<Rightarrow> (Suc n \<le> length ctr \<longrightarrow> length tr = Suc n) \<and> rely_cond R' s0 tr
 2. \<And>n a b. \<lbrakk>(a, b) \<in> f s; n \<le> length ctr \<longrightarrow> length a = n; rely_cond R' s0 a; \<not> \<not> Suc n \<le> length ctr\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. case x of (tr, res) \<Rightarrow> (Suc n \<le> length ctr \<longrightarrow> length tr = Suc n) \<and> rely_cond R' s0 tr proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>(a, b) \<in> f s; n \<le> length ctr \<longrightarrow> length a = n; rely_cond R' s0 a; \<not> \<not> Suc n \<le> length ctr\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. case x of (tr, res) \<Rightarrow> (Suc n \<le> length ctr \<longrightarrow> length tr = Suc n) \<and> rely_cond R' s0 tr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> f s; rely_cond R' s0 a; Suc (length a) \<le> length ctr\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. case x of (tr, res) \<Rightarrow> length tr = Suc (length a) \<and> rely_cond R' s0 tr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>rely_cond R' s0 a; Suc (length a) \<le> length ctr; \<exists>x res. (x # a, res) \<in> f s \<and> rely_cond R' s0 (x # a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. case x of (tr, res) \<Rightarrow> length tr = Suc (length a) \<and> rely_cond R' s0 tr proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>(tr, res)\<in>f s. (n \<le> length ctr \<longrightarrow> length tr = n) \<and> rely_cond R' s0 tr

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
this:
\<exists>(tr, res)\<in>f s. (?n2 \<le> length ctr \<longrightarrow> length tr = ?n2) \<and> rely_cond R' s0 tr

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
this:
\<exists>(tr, res)\<in>f s. (?n \<le> length ctr \<longrightarrow> length tr = ?n) \<and> rely_cond R' s0 tr

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
using this:
\<exists>(tr, res)\<in>f s. (length ctr \<le> length ctr \<longrightarrow> length tr = length ctr) \<and> rely_cond R' s0 tr

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> f s; length a = length ctr; rely_cond R' s0 a\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. case x of (atr, ares) \<Rightarrow> matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> f s; length a = length ctr; rely_cond R' s0 a\<rbrakk> \<Longrightarrow> case (a, b) of (atr, ares) \<Rightarrow> matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> f s; length a = length ctr; rely_cond R' s0 a\<rbrakk> \<Longrightarrow> matching_tr sr a ctr \<and> rel_tmres osr rvr b cres proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> f s; length a = length ctr; rely_cond R' s0 a; rely_cond R' s0 a \<and> matching_tr_pfx sr a ctr \<and> (length a < length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr \<longrightarrow> rel_tmres osr rvr b cres)\<rbrakk> \<Longrightarrow> matching_tr sr a ctr \<and> rel_tmres osr rvr b cres proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr

goal:
No subgoals!