theory Prefix_Refinement

lemma env_closed_parallel_fragment:
  "is_matching_fragment sr osr rvr ctr1 cres1 s0 (E or Gg) s f
    \<Longrightarrow> is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g
    \<Longrightarrow> par_tr_fin_principle f
    \<Longrightarrow> par_tr_fin_principle g
    \<Longrightarrow> cres1 = cres2 \<Longrightarrow> length ctr1 = length ctr2
    \<Longrightarrow> \<forall>s xs. Q xs s \<longrightarrow> (sr s (snd (rev ctr1 ! length xs)))
        \<and> (sr s (snd (rev ctr2 ! length xs)))
        \<and> length xs < length ctr2
        \<and> fst (rev ctr1 ! length xs) = Env
        \<and> fst (rev ctr2 ! length xs) = Env
        \<and> E (last_st_tr xs s0) s
    \<Longrightarrow> env_closed Q s (parallel f g)" apply (subst env_closed_def, clarsimp) apply (frule is_matching_fragment_prefix_closed[where f=f]) apply (frule is_matching_fragment_prefix_closed[where f=g]) apply (subst(asm) parallel_def, clarsimp simp: length_Suc_conv) apply (strengthen in_fst_snd_image) apply (simp add: par_tr_fragment_parallel_def) apply (strengthen exI[where x="x # xs" for x xs]) apply (frule(1) is_matching_fragment_trD[where f=f]) apply (frule(1) is_matching_fragment_trD[where f=g]) apply (clarsimp simp: matching_tr_pfx_aCons rely_cond_Cons_eq
                        last_st_tr_map_zip pred_disj_def) apply (drule spec2, drule(1) mp[where P="Q xs s" for xs s]) apply clarsimp apply (drule_tac s'=s' in env_closedD[where f=f, OF is_matching_fragment_env_closed, rotated];
    simp?) apply (simp add: matching_tr_pfx_aCons rely_cond_Cons_eq last_st_tr_map_zip prod_eq_iff) apply (drule_tac s'=s' in env_closedD[where f=g, OF is_matching_fragment_env_closed, rotated];
    simp?) apply (simp add: matching_tr_pfx_aCons rely_cond_Cons_eq last_st_tr_map_zip prod_eq_iff) apply clarsimp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres1 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s\<rbrakk> \<Longrightarrow> env_closed Q s (parallel f g) proof (prove)
goal (1 subgoal):
 1. \<And>xs s'. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; (xs, Incomplete) \<in> parallel f g s; Q xs s'\<rbrakk> \<Longrightarrow> (Env, s') # xs \<in> fst ` parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>xs s'. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; (xs, Incomplete) \<in> parallel f g s; Q xs s'; prefix_closed f\<rbrakk> \<Longrightarrow> (Env, s') # xs \<in> fst ` parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>xs s'. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; (xs, Incomplete) \<in> parallel f g s; Q xs s'; prefix_closed f; prefix_closed g\<rbrakk> \<Longrightarrow> (Env, s') # xs \<in> fst ` parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s\<rbrakk> \<Longrightarrow> (Env, s') # xs \<in> fst ` parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s\<rbrakk> \<Longrightarrow> \<exists>y. ((Env, s') # xs, y) \<in> parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s\<rbrakk> \<Longrightarrow> \<exists>y f_steps. length f_steps = Suc (length xs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps ((Env, s') # xs), y) \<in> f s \<and> (\<exists>res'. (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps ((Env, s') # xs), res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s\<rbrakk> \<Longrightarrow> \<exists>x xsa xa. length (xa # xsa) = Suc (length xs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) (xa # xsa) ((Env, s') # xs), x) \<in> f s \<and> (\<exists>res'. (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) (xa # xsa) ((Env, s') # xs), res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s; rely_cond (E or Gg) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) \<and> matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1 \<and> (length (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) < length ctr1 \<longrightarrow> Incomplete = Incomplete) \<and> (length (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr Incomplete cres2)\<rbrakk> \<Longrightarrow> \<exists>x xsa xa. length (xa # xsa) = Suc (length xs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) (xa # xsa) ((Env, s') # xs), x) \<in> f s \<and> (\<exists>res'. (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) (xa # xsa) ((Env, s') # xs), res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (E or Gg) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s; rely_cond (E or Gg) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) \<and> matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1 \<and> (length (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) < length ctr1 \<longrightarrow> Incomplete = Incomplete) \<and> (length (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr Incomplete cres2); rely_cond (E or Gf) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) \<and> matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2 \<and> (length (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) < length ctr2 \<longrightarrow> Incomplete = Incomplete) \<and> (length (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) = length ctr2 \<longrightarrow> rel_tmres osr' rvr Incomplete cres2)\<rbrakk> \<Longrightarrow> \<exists>x xsa xa. length (xa # xsa) = Suc (length xs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) (xa # xsa) ((Env, s') # xs), x) \<in> f s \<and> (\<exists>res'. (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) (xa # xsa) ((Env, s') # xs), res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; \<forall>s xs. Q xs s \<longrightarrow> sr s (snd (rev ctr1 ! length xs)) \<and> sr s (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; length xs = length ctr2 \<longrightarrow> rel_tmres osr rvr Incomplete cres2; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; length xs = length ctr2 \<longrightarrow> rel_tmres osr' rvr Incomplete cres2\<rbrakk> \<Longrightarrow> \<exists>x xsa. length xsa = length xs \<and> ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, x) \<in> f s \<and> (\<exists>res'. ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; length xs = length ctr2 \<longrightarrow> rel_tmres osr rvr Incomplete cres2; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; length xs = length ctr2 \<longrightarrow> rel_tmres osr' rvr Incomplete cres2; sr s' (snd (rev ctr1 ! length xs)) \<and> sr s' (snd (rev ctr2 ! length xs)) \<and> length xs < length ctr2 \<and> fst (rev ctr1 ! length xs) = Env \<and> fst (rev ctr2 ! length xs) = Env \<and> E (last_st_tr xs s0) s'\<rbrakk> \<Longrightarrow> \<exists>x xsa. length xsa = length xs \<and> ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, x) \<in> f s \<and> (\<exists>res'. ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; sr s' (snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); length xs < length ctr2; fst (rev ctr1 ! length xs) = Env; fst (rev ctr2 ! length xs) = Env; E (last_st_tr xs s0) s'\<rbrakk> \<Longrightarrow> \<exists>x xsa. length xsa = length xs \<and> ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, x) \<in> f s \<and> (\<exists>res'. ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) proof (prove)
goal (2 subgoals):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; sr s' (snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); length xs < length ctr2; fst (rev ctr1 ! length xs) = Env; fst (rev ctr2 ! length xs) = Env; E (last_st_tr xs s0) s'\<rbrakk> \<Longrightarrow> matching_tr_pfx sr ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1 \<and> rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs)
 2. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; sr s' (snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); length xs < length ctr2; fst (rev ctr1 ! length xs) = Env; fst (rev ctr2 ! length xs) = Env; E (last_st_tr xs s0) s'; (Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>x xsa. length xsa = length xs \<and> ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, x) \<in> f s \<and> (\<exists>res'. ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; sr s' (snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); length xs < length ctr2; fst (rev ctr1 ! length xs) = Env; fst (rev ctr2 ! length xs) = Env; E (last_st_tr xs s0) s'; (Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>x xsa. length xsa = length xs \<and> ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, x) \<in> f s \<and> (\<exists>res'. ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) proof (prove)
goal (2 subgoals):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; sr s' (snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); length xs < length ctr2; fst (rev ctr1 ! length xs) = Env; fst (rev ctr2 ! length xs) = Env; E (last_st_tr xs s0) s'; (Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs \<in> fst ` f s\<rbrakk> \<Longrightarrow> matching_tr_pfx sr ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2 \<and> rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs)
 2. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; sr s' (snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); length xs < length ctr2; fst (rev ctr1 ! length xs) = Env; fst (rev ctr2 ! length xs) = Env; E (last_st_tr xs s0) s'; (Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs \<in> fst ` f s; (Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs \<in> fst ` g s\<rbrakk> \<Longrightarrow> \<exists>x xsa. length xsa = length xs \<and> ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, x) \<in> f s \<and> (\<exists>res'. ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; sr s' (snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); length xs < length ctr2; fst (rev ctr1 ! length xs) = Env; fst (rev ctr2 ! length xs) = Env; E (last_st_tr xs s0) s'; (Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs \<in> fst ` f s; (Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs \<in> fst ` g s\<rbrakk> \<Longrightarrow> \<exists>x xsa. length xsa = length xs \<and> ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, x) \<in> f s \<and> (\<exists>res'. ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' f_steps b ba. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres2 s0 (\<lambda>x xa. E x xa \<or> Gg x xa) s f; is_matching_fragment sr osr' rvr ctr2 cres2 s0 (\<lambda>x xa. E x xa \<or> Gf x xa) s g; par_tr_fin_principle f; par_tr_fin_principle g; cres1 = cres2; length ctr1 = length ctr2; Q xs s'; prefix_closed f; prefix_closed g; length f_steps = length xs; rely_cond (\<lambda>x xa. E x xa \<or> Gg x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); rely_cond (\<lambda>x xa. E x xa \<or> Gf x xa) s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; sr s' (snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); length xs < length ctr2; fst (rev ctr1 ! length xs) = Env; fst (rev ctr2 ! length xs) = Env; E (last_st_tr xs s0) s'; ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s; ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, ba) \<in> g s\<rbrakk> \<Longrightarrow> \<exists>x xsa. length xsa = length xs \<and> ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, x) \<in> f s \<and> (\<exists>res'. ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) proof (prove)
goal:
No subgoals!