theory Prefix_Refinement

lemma self_closed_parallel_fragment:
  notes if_split[split del]
  shows
  "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> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>
    \<Longrightarrow> P s0 s
    \<Longrightarrow> cres1 = cres2
    \<Longrightarrow> Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) \<noteq> Env
            \<or> fst (rev ctr2 ! length xs) \<noteq> Env))
    \<Longrightarrow> self_closed Q s (parallel f g)" apply (subst self_closed_def, clarsimp) apply (subst(asm) parallel_def, clarsimp) apply (frule list_all2_lengthD[symmetric]) 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 (clarsimp simp: length_Suc_conv) apply (frule(1) list_all2_rev_nthD, clarsimp) apply (case_tac "fst (rev ctr1 ! length xs) = Env"; simp) apply (frule is_matching_fragment_self_closed[where f=g],
     drule(1) self_closedD, simp add: eq_Me_neq_Env) apply (thin_tac "v \<in> g s" for v s) apply clarsimp apply (frule(1) is_matching_fragment_trD[where f=g]) apply clarsimp apply (frule(3) validI_GD[where f=g]) apply (clarsimp simp: guar_cond_Cons_eq matching_tr_pfx_aCons) apply (drule_tac s'=s' in matching_env_closedD[where f=f], simp+) apply (simp add: last_st_tr_map_zip) apply (clarsimp simp: ex_bool_eq del: disjCI) apply (blast intro: in_fst_snd_image) 
  (* pretty much identical proof for symmetric case. sad. *)
   apply (frule is_matching_fragment_self_closed[where f=f],
    drule(1) self_closedD, simp add: eq_Me_neq_Env) apply (thin_tac "v \<in> f s" for v s) apply clarsimp apply (frule(1) is_matching_fragment_trD[where f=f]) apply clarsimp apply (frule(3) validI_GD[where f=f]) apply (clarsimp simp: guar_cond_Cons_eq matching_tr_pfx_aCons) apply (drule_tac s'=s' in matching_env_closedD[where f=g], simp+) apply (simp add: last_st_tr_map_zip) apply (clarsimp simp: ex_bool_eq del: disjCI) apply (blast intro: in_fst_snd_image) 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) \<noteq> Env \<or> fst (rev ctr2 ! length xs) \<noteq> Env))\<rbrakk> \<Longrightarrow> self_closed Q s (parallel f g) proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); (xs, Incomplete) \<in> parallel f g s; length xs < length ctr1; fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>s'. (Me, s') # xs \<in> fst ` parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env; 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>s'. (Me, s') # xs \<in> fst ` parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1\<rbrakk> \<Longrightarrow> \<exists>s'. (Me, s') # xs \<in> fst ` parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1\<rbrakk> \<Longrightarrow> \<exists>x y. ((Me, x) # xs, y) \<in> parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1\<rbrakk> \<Longrightarrow> \<exists>x 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 ((Me, x) # xs), y) \<in> f s \<and> (\<exists>res'. (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps ((Me, x) # xs), res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1\<rbrakk> \<Longrightarrow> \<exists>x xa xsa xb. length (xb # xsa) = Suc (length xs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) (xb # xsa) ((Me, x) # xs), xa) \<in> f s \<and> (\<exists>res'. (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) (xb # xsa) ((Me, x) # xs), res') \<in> g s) proof (prove)
goal (1 subgoal):
 1. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1; fst (rev ctr1 ! length xs) = Env \<or> fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs)\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) = Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) = Env; \<exists>s'. (Me, 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 xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) = Env; \<exists>s'. (Me, 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 xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, b) \<in> g s\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, b) \<in> g s; rely_cond (E or Gf) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) \<and> matching_tr_pfx sr ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2 \<and> (length ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) < length ctr2 \<longrightarrow> b = Incomplete) \<and> (length ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) = length ctr2 \<longrightarrow> rel_tmres osr' rvr b cres2)\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, b) \<in> g s; rely_cond (E or Gf) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr' rvr b cres2\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; fst (rev ctr2 ! length xs) \<noteq> Env; 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; length ctr2 = length ctr1; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, b) \<in> g s; rely_cond (E or Gf) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); matching_tr_pfx sr ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr' rvr b cres2; guar_cond Gg s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs)\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr1 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, b) \<in> g s; rely_cond (E or Gf) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr' rvr b cres2; guar_cond Gg s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Gg (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) s0) s'; rev ctr2 ! length xs = (Me, snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr1 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s)) proof (prove)
goal (3 subgoals):
 1. \<And>xs f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; length f_steps = length xs; length ctr2 = length ctr1; fst (rev ctr1 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, b) \<in> g s; rely_cond (E or Gf) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr' rvr b cres2; guar_cond Gg s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Gg (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) s0) s'; rev ctr2 ! length xs = (Me, snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr1 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2\<rbrakk> \<Longrightarrow> E (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) s0) s' \<or> Gg (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) s0) s'
 2. \<And>xs f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; length f_steps = length xs; length ctr2 = length ctr1; fst (rev ctr1 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, b) \<in> g s; rely_cond (E or Gf) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr' rvr b cres2; guar_cond Gg s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Gg (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) s0) s'; rev ctr2 ! length xs = (Me, snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr1 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; (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 xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 3. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; length f_steps = length xs; length ctr2 = length ctr1; fst (rev ctr1 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, b) \<in> g s; rely_cond (E or Gf) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr' rvr b cres2; guar_cond Gg s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Gg (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) s0) s'; rev ctr2 ! length xs = (Me, snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr1 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; (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 xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b ba. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; length f_steps = length xs; length ctr2 = length ctr1; fst (rev ctr1 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, b) \<in> g s; rely_cond (E or Gf) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr' rvr b cres2; guar_cond Gg s0 (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs); Gg (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) s0) s'; rev ctr2 ! length xs = (Me, snd (rev ctr1 ! length xs)); sr s' (snd (rev ctr1 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) ctr2; ((Env, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, ba) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (((Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) \<or> ((Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s))
 2. \<And>xs 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env; \<exists>s'. (Me, 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 xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env; \<exists>s'. (Me, 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 xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s; rely_cond (E or Gg) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) \<and> matching_tr_pfx sr ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1 \<and> (length ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) < length ctr1 \<longrightarrow> b = Incomplete) \<and> (length ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr b cres2)\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s; rely_cond (E or Gg) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); matching_tr_pfx sr ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr b cres2\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; snd (rev ctr1 ! length xs) = snd (rev ctr2 ! length xs); fst (rev ctr1 ! length xs) \<noteq> Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s; rely_cond (E or Gg) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); matching_tr_pfx sr ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr b cres2; guar_cond Gf s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs)\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; 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; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s; rely_cond (E or Gg) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr b cres2; guar_cond Gf s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Gf (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) s0) s'; rev ctr1 ! length xs = (Me, snd (rev ctr2 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1\<rbrakk> \<Longrightarrow> \<exists>x xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; length f_steps = length xs; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s; rely_cond (E or Gg) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr b cres2; guar_cond Gf s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Gf (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) s0) s'; rev ctr1 ! length xs = (Me, snd (rev ctr2 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1\<rbrakk> \<Longrightarrow> E (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) s0) s' \<or> Gf (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs) s0) s'
 2. \<And>xs f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; length f_steps = length xs; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s; rely_cond (E or Gg) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr b cres2; guar_cond Gf s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Gf (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) s0) s'; rev ctr1 ! length xs = (Me, snd (rev ctr2 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; (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 xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; length f_steps = length xs; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s; rely_cond (E or Gg) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr b cres2; guar_cond Gf s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Gf (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) s0) s'; rev ctr1 ! length xs = (Me, snd (rev ctr2 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; (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 xa xsa. length xsa = length xs \<and> (\<exists>xb. ((if xb then Me else Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((if xb then Env else Me, x) # 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 f_steps s' b ba. \<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; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ctr1 ctr2; \<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P s0 s; cres1 = cres2; Q = (\<lambda>xs. length xs < length ctr1 \<and> (fst (rev ctr1 ! length xs) = Env \<longrightarrow> fst (rev ctr2 ! length xs) \<noteq> Env)); length xs < length ctr1; length f_steps = length xs; length ctr2 = length ctr1; fst (rev ctr2 ! length xs) = Env; ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, b) \<in> f s; rely_cond (E or Gg) s0 ((Me, s') # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Suc (length xs) < length ctr1 \<longrightarrow> b = Incomplete; Suc (length xs) = length ctr1 \<longrightarrow> rel_tmres osr rvr b cres2; guar_cond Gf s0 (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs); Gf (last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) s0) s'; rev ctr1 ! length xs = (Me, snd (rev ctr2 ! length xs)); sr s' (snd (rev ctr2 ! length xs)); matching_tr_pfx sr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs) ctr1; ((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 xa xsa. length xsa = length xs \<and> (((Me, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) xsa xs, res') \<in> g s) \<or> ((Env, x) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) xsa xs, xa) \<in> f s \<and> (\<exists>res'. ((Me, x) # 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!