theory Prefix_Refinement

lemma prefix_refinement_in_place_trans:
  "prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0 s. sr s0 t0 \<and> sr s t \<and> R s0 s) f g
    \<Longrightarrow> prefix_refinement sr isr osr (=) (\<lambda>_ _. True) Q AR R g h
    \<Longrightarrow> equivp sr \<Longrightarrow> equivp osr \<Longrightarrow> equivp isr
    \<Longrightarrow> (\<forall>s t t'. sr s t \<longrightarrow> R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s'))
    \<Longrightarrow> prefix_refinement sr isr osr (=) P Q AR R f h" apply (subst prefix_refinement_def, clarsimp) apply (drule_tac s=t and t=t and ?t0.0=t0 and cprog=h in pfx_refnD;
      assumption?) apply (metis equivp_reflp_symp_transp reflpD) apply metis apply clarsimp apply (rename_tac h_tr h_res frag_g) apply (rule_tac x="\<lambda>s. \<Union>(tr, res) \<in> frag_g t \<inter> ({tr. length tr = length h_tr} \<times> UNIV).
    \<Union>frag_f \<in> {frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f
                \<and> triv_refinement f frag_f}. frag_f s" in exI) apply (rule conjI) apply (rule is_matching_fragment_UNION) apply clarsimp apply (rename_tac g_tr g_res) apply (rule is_matching_fragment_UNION) apply clarsimp apply (erule(1) is_matching_fragment_trans; simp) apply (clarsimp simp: is_matching_fragment_def) apply clarsimp apply (drule(1) triv_refinement_elemD) apply (frule(1) is_matching_fragment_trD) apply (clarsimp simp: matching_tr_pfx_def) apply (drule matching_tr_symp[THEN sympD, rotated], metis equivp_reflp_symp_transp) apply (drule(1) matching_tr_rely_cond) apply (erule equivp_reflp) apply (fastforce elim: pfx_refnD2) apply clarsimp apply (rule prefix_closed_UNION) apply (clarsimp simp: is_matching_fragment_def) apply (drule(2) matching_fragment_matching_tr, simp) apply (clarsimp simp: matching_tr_def dest!: list_all2_lengthD) apply blast apply (clarsimp simp: triv_refinement_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0 s. sr s0 t0 \<and> sr s t \<and> R s0 s) f g; prefix_refinement sr isr osr (=) (\<lambda>_ _. True) Q AR R g h; equivp sr; equivp osr; equivp isr; \<forall>s t t'. sr s t \<longrightarrow> R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr (=) P Q AR R f h proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; prefix_refinement sr isr osr (=) (\<lambda>_ _. True) Q AR R g h; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> h t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr (=) a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> h t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> isr t t
 2. \<And>s s0 t0 t a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> h t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> True
 3. \<And>s s0 t0 t a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> h t; rely_cond R t0 a; case (a, b) of (ctr, cres) \<Rightarrow> rely_cond R t0 ctr \<longrightarrow> (\<exists>f. is_matching_fragment sr osr (=) ctr cres s0 AR t f \<and> triv_refinement g f)\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr (=) a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> h t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> True
 2. \<And>s s0 t0 t a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> h t; rely_cond R t0 a; case (a, b) of (ctr, cres) \<Rightarrow> rely_cond R t0 ctr \<longrightarrow> (\<exists>f. is_matching_fragment sr osr (=) ctr cres s0 AR t f \<and> triv_refinement g f)\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr (=) a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> h t; rely_cond R t0 a; case (a, b) of (ctr, cres) \<Rightarrow> rely_cond R t0 ctr \<longrightarrow> (\<exists>f. is_matching_fragment sr osr (=) ctr cres s0 AR t f \<and> triv_refinement g f)\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr (=) a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b fa. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> h t; rely_cond R t0 a; is_matching_fragment sr osr (=) a b s0 AR t fa; triv_refinement g fa\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr (=) a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr (=) h_tr h_res s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (=) h_tr h_res s0 AR s (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) \<and> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (=) h_tr h_res s0 AR s (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> is_matching_fragment sr osr (=) h_tr h_res s0 AR s (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (a, b) \<in> frag_g t; length a = length h_tr\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (=) h_tr h_res s0 AR s (\<lambda>s. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) a b s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (=) h_tr h_res s0 AR s (\<lambda>s. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) g_tr g_res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (6 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> \<forall>frag_f. frag_f \<in> {frag_f. is_matching_fragment sr osr (=) g_tr g_res s0 AR s frag_f \<and> triv_refinement f frag_f} \<longrightarrow> is_matching_fragment sr osr (=) h_tr h_res s0 AR s frag_f
 2. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> \<forall>s' frag_f. frag_f \<in> {frag_f. is_matching_fragment sr osr (=) g_tr g_res s0 AR s' frag_f \<and> triv_refinement f frag_f} \<longrightarrow> prefix_closed frag_f
 3. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> {frag_f. is_matching_fragment sr osr (=) g_tr g_res s0 AR s frag_f \<and> triv_refinement f frag_f} \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 5. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 6. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (6 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res frag_f. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; is_matching_fragment sr osr (=) g_tr g_res s0 AR s frag_f; triv_refinement f frag_f\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (=) h_tr h_res s0 AR s frag_f
 2. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> \<forall>s' frag_f. frag_f \<in> {frag_f. is_matching_fragment sr osr (=) g_tr g_res s0 AR s' frag_f \<and> triv_refinement f frag_f} \<longrightarrow> prefix_closed frag_f
 3. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> {frag_f. is_matching_fragment sr osr (=) g_tr g_res s0 AR s frag_f \<and> triv_refinement f frag_f} \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 5. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 6. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (5 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> \<forall>s' frag_f. frag_f \<in> {frag_f. is_matching_fragment sr osr (=) g_tr g_res s0 AR s' frag_f \<and> triv_refinement f frag_f} \<longrightarrow> prefix_closed frag_f
 2. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> {frag_f. is_matching_fragment sr osr (=) g_tr g_res s0 AR s frag_f \<and> triv_refinement f frag_f} \<noteq> {}
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 5. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> {frag_f. is_matching_fragment sr osr (=) g_tr g_res s0 AR s frag_f \<and> triv_refinement f frag_f} \<noteq> {}
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr\<rbrakk> \<Longrightarrow> \<exists>x. is_matching_fragment sr osr (=) g_tr g_res s0 AR s x \<and> triv_refinement f x
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; (g_tr, g_res) \<in> g t\<rbrakk> \<Longrightarrow> \<exists>x. is_matching_fragment sr osr (=) g_tr g_res s0 AR s x \<and> triv_refinement f x
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; (g_tr, g_res) \<in> g t; rely_cond AR s0 g_tr \<and> matching_tr_pfx sr g_tr h_tr \<and> (length g_tr < length h_tr \<longrightarrow> g_res = Incomplete) \<and> (length g_tr = length h_tr \<longrightarrow> rel_tmres osr (=) g_res h_res)\<rbrakk> \<Longrightarrow> \<exists>x. is_matching_fragment sr osr (=) g_tr g_res s0 AR s x \<and> triv_refinement f x
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; (g_tr, g_res) \<in> g t; rely_cond AR s0 g_tr; matching_tr sr (rev g_tr) (rev h_tr); rel_tmres osr (=) g_res h_res\<rbrakk> \<Longrightarrow> \<exists>x. is_matching_fragment sr osr (=) g_tr g_res s0 AR s x \<and> triv_refinement f x
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; (g_tr, g_res) \<in> g t; rely_cond AR s0 g_tr; rel_tmres osr (=) g_res h_res; matching_tr sr (rev h_tr) (rev g_tr)\<rbrakk> \<Longrightarrow> \<exists>x. is_matching_fragment sr osr (=) g_tr g_res s0 AR s x \<and> triv_refinement f x
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (5 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; (g_tr, g_res) \<in> g t; rely_cond AR s0 g_tr; rel_tmres osr (=) g_res h_res\<rbrakk> \<Longrightarrow> sr t0 (?t0.103 s s0 t0 t h_tr h_res frag_g g_tr g_res)
 2. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; (g_tr, g_res) \<in> g t; rely_cond AR s0 g_tr; rel_tmres osr (=) g_res h_res; rely_cond (\<lambda>t0 t. \<exists>s0 s. sr s0 t0 \<and> sr s t \<and> R s0 s) (?t0.103 s s0 t0 t h_tr h_res frag_g g_tr g_res) g_tr\<rbrakk> \<Longrightarrow> \<exists>x. is_matching_fragment sr osr (=) g_tr g_res s0 AR s x \<and> triv_refinement f x
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 5. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g g_tr g_res. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; (g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; (g_tr, g_res) \<in> g t; rely_cond AR s0 g_tr; rel_tmres osr (=) g_res h_res; rely_cond (\<lambda>t0 t. \<exists>s0 s. sr s0 t0 \<and> sr s t \<and> R s0 s) t0 g_tr\<rbrakk> \<Longrightarrow> \<exists>x. is_matching_fragment sr osr (=) g_tr g_res s0 AR s x \<and> triv_refinement f x
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 4. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> \<forall>s' x. x \<in> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<longrightarrow> prefix_closed (\<lambda>s. case x of (tr, res) \<Rightarrow> \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (a, b) \<in> frag_g t; length a = length h_tr\<rbrakk> \<Longrightarrow> prefix_closed (\<lambda>s. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) a b s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s)
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g; (a, b) \<in> frag_g t; length a = length h_tr\<rbrakk> \<Longrightarrow> \<forall>s' frag_f. frag_f \<in> {frag_f. is_matching_fragment sr osr (=) a b s0 AR s' frag_f \<and> triv_refinement f frag_f} \<longrightarrow> prefix_closed frag_f
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 3. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; triv_refinement g frag_g; \<exists>(atr, ares)\<in>frag_g t. matching_tr sr atr h_tr \<and> rel_tmres osr (=) ares h_res \<and> rely_cond AR s0 atr\<rbrakk> \<Longrightarrow> frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV \<noteq> {}
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t h_tr h_res frag_g a b. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; triv_refinement g frag_g; (a, b) \<in> frag_g t; length a = length h_tr; rel_tmres osr (=) b h_res; rely_cond AR s0 a; frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t h_tr h_res frag_g. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; triv_refinement g frag_g\<rbrakk> \<Longrightarrow> triv_refinement f (\<lambda>s. \<Union>(tr, res)\<in>frag_g t \<inter> {tr. length tr = length h_tr} \<times> UNIV. \<Union>frag_f\<in>{frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f \<and> triv_refinement f frag_f}. frag_f s) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t h_tr h_res frag_g sa a b aa ba x. \<lbrakk>prefix_refinement sr isr osr (=) P (\<lambda>_ _. True) AR (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) f g; equivp sr; equivp osr; equivp isr; \<forall>s t. sr s t \<longrightarrow> (\<forall>t'. R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> AR s s')); isr s t; P s0 s; sr s0 t0; Q t0 t; (h_tr, h_res) \<in> h t; rely_cond R t0 h_tr; is_matching_fragment sr osr (=) h_tr h_res s0 AR t frag_g; \<forall>s. frag_g s \<subseteq> g s; (a, b) \<in> x sa; (aa, ba) \<in> frag_g t; length aa = length h_tr; is_matching_fragment sr osr (=) aa ba s0 AR sa x; \<forall>s. x s \<subseteq> f s\<rbrakk> \<Longrightarrow> (a, b) \<in> f sa proof (prove)
goal:
No subgoals!