theory Prefix_Refinement

theorem prefix_refinement_parallel:
  "prefix_refinement sr isr osr rvr P Q (AE or Gc) (E or Gd) a b
    \<Longrightarrow> prefix_refinement sr isr osr rvr P Q (AE or Ga) (E or Gb) c d
    \<Longrightarrow> par_tr_fin_principle a
    \<Longrightarrow> par_tr_fin_principle c
    \<Longrightarrow> \<lbrace>Q\<rbrace>,\<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>
    \<Longrightarrow> \<lbrace>Q\<rbrace>,\<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>
    \<Longrightarrow> (Ga = \<top>\<top> \<and> Gc = \<top>\<top>)
        \<or> (\<lbrace>P\<rbrace>,\<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>
            \<and> \<lbrace>P\<rbrace>,\<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>)
    \<Longrightarrow> prefix_refinement sr isr osr rvr P Q AE E (parallel a c) (parallel b d)" apply (subst prefix_refinement_def, clarsimp) apply (drule tr_in_parallel, clarify) apply (frule(6) tr_in_parallel_validI) apply (clarsimp simp: parallel_def3) apply (rename_tac b_tr d_tr bd_res) apply (drule(5) prefix_refinementD)+ apply clarsimp apply (rename_tac f_a f_c) apply (rule_tac x="rely (parallel f_a f_c) AE s0" in exI) apply (rule conjI[rotated]) apply (simp add: parallel_def3 triv_refinement_def rely_def) apply blast apply (subst is_matching_fragment_def, clarsimp) apply (frule(1) is_matching_fragment_validI_disj[where g=a and G=Ga], blast) apply (frule(1) is_matching_fragment_validI_disj[where g=c and G=Gc], blast) apply (intro conjI prefix_closed_parallel prefix_closed_rely rely_self_closed,
    simp_all add: is_matching_fragment_prefix_closed) apply (rule self_closed_parallel_fragment,
        (assumption | erule par_tr_fin_principle_triv_refinement[rotated])+) apply simp apply (frule list_all2_lengthD) apply (simp add: list_all2_lengthD eq_Me_neq_Env rev_nth split_def fun_eq_iff
                cong: conj_cong) apply (rule rely_env_closed[where P=P and P'=P for P, rotated]) apply (simp add: rely_cond_Cons_eq) apply (rule env_closed_parallel_fragment,
        (assumption | erule par_tr_fin_principle_triv_refinement[rotated])+) apply simp apply (simp add: list_all2_lengthD) apply (clarsimp simp: matching_tr_pfx_aCons rev_map split_def
                          zip_rev[symmetric] list_all2_lengthD[symmetric]
                          rely_cond_Cons_eq) apply (frule list_all2_lengthD) apply (drule(1) list_all2_rev_nthD, simp) apply (simp split: if_split_asm) apply (simp add: rely_def par_tr_fragment_parallel_def list_all2_lengthD
                    par_tr_fin_principle_triv_refinement set_eq_iff) apply (strengthen exI[where x=Nil] in_fst_snd_image)+ apply (simp add: is_matching_fragment_Nil[simplified image_def Bex_def, simplified]) apply (clarsimp simp: parallel_def3 rely_def) apply (drule(1) is_matching_fragment_trD)+ apply (clarsimp simp: list_all2_lengthD) apply (rule matching_tr_pfx_parallel_zip; assumption?) apply (simp add: list_all2_lengthD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr isr osr rvr P Q (AE or Gc) (E or Gd) a b; prefix_refinement sr isr osr rvr P Q (AE or Ga) (E or Gb) c d; par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr P Q AE E (parallel a c) (parallel b d) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t aa ba. \<lbrakk>prefix_refinement sr isr osr rvr P Q (AE or Gc) (E or Gd) a b; prefix_refinement sr isr osr rvr P Q (AE or Ga) (E or Gb) c d; par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; (aa, ba) \<in> parallel b d t; rely_cond E t0 aa\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr aa ba s0 AE s f \<and> triv_refinement (parallel a c) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t aa ba f_tr g_tr. \<lbrakk>prefix_refinement sr isr osr rvr P Q (AE or Gc) (E or Gd) a b; prefix_refinement sr isr osr rvr P Q (AE or Ga) (E or Gb) c d; par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 aa; (f_tr, ba) \<in> b t; (g_tr, ba) \<in> d t; (aa, ba) \<in> parallel (K {(f_tr, ba)}) (K {(g_tr, ba)}) t\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr aa ba s0 AE s f \<and> triv_refinement (parallel a c) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t aa ba f_tr g_tr. \<lbrakk>prefix_refinement sr isr osr rvr P Q (AE or Gc) (E or Gd) a b; prefix_refinement sr isr osr rvr P Q (AE or Ga) (E or Gb) c d; par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 aa; (f_tr, ba) \<in> b t; (g_tr, ba) \<in> d t; (aa, ba) \<in> parallel (K {(f_tr, ba)}) (K {(g_tr, ba)}) t; rely_cond (E or Gd) t0 f_tr \<and> rely_cond (E or Gb) t0 g_tr\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr aa ba s0 AE s f \<and> triv_refinement (parallel a c) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t f_tr g_tr ba. \<lbrakk>prefix_refinement sr isr osr rvr P Q (AE or Gc) (E or Gd) a b; prefix_refinement sr isr osr rvr P Q (AE or Ga) (E or Gb) c d; par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) f_tr g_tr); (f_tr, ba) \<in> b t; (g_tr, ba) \<in> d t; rely_cond (E or Gd) t0 f_tr; rely_cond (E or Gb) t0 g_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) f_tr g_tr\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) f_tr g_tr) ba s0 AE s f \<and> triv_refinement (\<lambda>s. (\<lambda>x. case x of (ys, zs, xa) \<Rightarrow> (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, xa)) ` {(ys, zs, rv). (ys, rv) \<in> a s \<and> (zs, rv) \<in> c s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs}) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res. \<lbrakk>prefix_refinement sr isr osr rvr P Q (AE or Gc) (E or Gd) a b; prefix_refinement sr isr osr rvr P Q (AE or Ga) (E or Gb) c d; par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) bd_res s0 AE s f \<and> triv_refinement (\<lambda>s. (\<lambda>x. case x of (ys, zs, xa) \<Rightarrow> (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, xa)) ` {(ys, zs, rv). (ys, rv) \<in> a s \<and> (zs, rv) \<in> c s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs}) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; case (b_tr, bd_res) of (ctr, cres) \<Rightarrow> rely_cond (E or Gd) t0 ctr \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr ctr cres s0 (AE or Gc) s f \<and> triv_refinement a f); case (d_tr, bd_res) of (ctr, cres) \<Rightarrow> rely_cond (E or Gb) t0 ctr \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr ctr cres s0 (AE or Ga) s f \<and> triv_refinement c f)\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) bd_res s0 AE s f \<and> triv_refinement (\<lambda>s. (\<lambda>x. case x of (ys, zs, xa) \<Rightarrow> (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, xa)) ` {(ys, zs, rv). (ys, rv) \<in> a s \<and> (zs, rv) \<in> c s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs}) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f fa. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f; triv_refinement a f; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s fa; triv_refinement c fa\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) bd_res s0 AE s f \<and> triv_refinement (\<lambda>s. (\<lambda>x. case x of (ys, zs, xa) \<Rightarrow> (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, xa)) ` {(ys, zs, rv). (ys, rv) \<in> a s \<and> (zs, rv) \<in> c s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs}) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) bd_res s0 AE s f \<and> triv_refinement (\<lambda>s. (\<lambda>x. case x of (ys, zs, xa) \<Rightarrow> (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, xa)) ` {(ys, zs, rv). (ys, rv) \<in> a s \<and> (zs, rv) \<in> c s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs}) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) bd_res s0 AE s (rely (parallel f_a f_c) AE s0) \<and> triv_refinement (\<lambda>s. (\<lambda>x. case x of (ys, zs, xa) \<Rightarrow> (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, xa)) ` {(ys, zs, rv). (ys, rv) \<in> a s \<and> (zs, rv) \<in> c s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs}) (rely (parallel f_a f_c) AE s0) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c\<rbrakk> \<Longrightarrow> triv_refinement (\<lambda>s. (\<lambda>x. case x of (ys, zs, xa) \<Rightarrow> (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, xa)) ` {(ys, zs, rv). (ys, rv) \<in> a s \<and> (zs, rv) \<in> c s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs}) (rely (parallel f_a f_c) AE s0)
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) bd_res s0 AE s (rely (parallel f_a f_c) AE s0) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; \<forall>s. f_a s \<subseteq> a s; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; \<forall>s. f_c s \<subseteq> c s\<rbrakk> \<Longrightarrow> \<forall>s. (\<lambda>x. case x of (ys, zs, xa) \<Rightarrow> (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, xa)) ` {(ys, zs, rv). (ys, rv) \<in> f_a s \<and> (zs, rv) \<in> f_c s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs} \<inter> Collect (rely_cond AE s0) \<times> UNIV \<subseteq> (\<lambda>x. case x of (ys, zs, xa) \<Rightarrow> (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, xa)) ` {(ys, zs, rv). (ys, rv) \<in> a s \<and> (zs, rv) \<in> c s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs}
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) bd_res s0 AE s (rely (parallel f_a f_c) AE s0) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) bd_res s0 AE s (rely (parallel f_a f_c) AE s0) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c\<rbrakk> \<Longrightarrow> prefix_closed (rely (parallel f_a f_c) AE s0) \<and> self_closed (\<lambda>xs. length xs < length b_tr \<and> length xs < length d_tr \<and> fst (rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) ! length xs) = Me) s (rely (parallel f_a f_c) AE s0) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (rely (parallel f_a f_c) AE s0) \<and> rely (parallel f_a f_c) AE s0 s \<noteq> {} \<and> (\<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res)) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> prefix_closed (rely (parallel f_a f_c) AE s0) \<and> self_closed (\<lambda>xs. length xs < length b_tr \<and> length xs < length d_tr \<and> fst (rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) ! length xs) = Me) s (rely (parallel f_a f_c) AE s0) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (rely (parallel f_a f_c) AE s0) \<and> rely (parallel f_a f_c) AE s0 s \<noteq> {} \<and> (\<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res)) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> prefix_closed (rely (parallel f_a f_c) AE s0) \<and> self_closed (\<lambda>xs. length xs < length b_tr \<and> length xs < length d_tr \<and> fst (rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) ! length xs) = Me) s (rely (parallel f_a f_c) AE s0) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (rely (parallel f_a f_c) AE s0) \<and> rely (parallel f_a f_c) AE s0 s \<noteq> {} \<and> (\<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res)) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> self_closed (\<lambda>xs. length xs < length b_tr \<and> length xs < length d_tr \<and> fst (rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) ! length xs) = Me) s (parallel f_a f_c)
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (rely (parallel f_a f_c) AE s0)
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 4. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (5 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> bd_res = bd_res
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> (\<lambda>xs. length xs < length b_tr \<and> length xs < length d_tr \<and> fst (rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) ! length xs) = Me) = (\<lambda>xs. length xs < length b_tr \<and> (fst (rev b_tr ! length xs) \<noteq> Env \<or> fst (rev d_tr ! length xs) \<noteq> Env))
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (rely (parallel f_a f_c) AE s0)
 4. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 5. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> (\<lambda>xs. length xs < length b_tr \<and> length xs < length d_tr \<and> fst (rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) ! length xs) = Me) = (\<lambda>xs. length xs < length b_tr \<and> (fst (rev b_tr ! length xs) \<noteq> Env \<or> fst (rev d_tr ! length xs) \<noteq> Env))
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (rely (parallel f_a f_c) AE s0)
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 4. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; length b_tr = length d_tr\<rbrakk> \<Longrightarrow> (\<lambda>xs. length xs < length b_tr \<and> length xs < length d_tr \<and> fst (rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) ! length xs) = Me) = (\<lambda>xs. length xs < length b_tr \<and> (fst (rev b_tr ! length xs) \<noteq> Env \<or> fst (rev d_tr ! length xs) \<noteq> Env))
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (rely (parallel f_a f_c) AE s0)
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 4. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (rely (parallel f_a f_c) AE s0)
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs) \<longrightarrow> rely_cond AE s0 xs \<longrightarrow> (matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) \<and> AE (last_st_tr xs s0) s
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (parallel f_a f_c)
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 4. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs)) s (parallel f_a f_c)
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (5 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> bd_res = bd_res
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> length b_tr = length d_tr
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s xs. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs) \<longrightarrow> sr s (snd (rev b_tr ! length xs)) \<and> sr s (snd (rev d_tr ! length xs)) \<and> length xs < length d_tr \<and> fst (rev b_tr ! length xs) = Env \<and> fst (rev d_tr ! length xs) = Env \<and> AE (last_st_tr xs s0) s
 4. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 5. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (4 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> length b_tr = length d_tr
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s xs. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs) \<longrightarrow> sr s (snd (rev b_tr ! length xs)) \<and> sr s (snd (rev d_tr ! length xs)) \<and> length xs < length d_tr \<and> fst (rev b_tr ! length xs) = Env \<and> fst (rev d_tr ! length xs) = Env \<and> AE (last_st_tr xs s0) s
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 4. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s xs. matching_tr_pfx sr ((Env, s) # xs) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> rely_cond AE s0 ((Env, s) # xs) \<longrightarrow> sr s (snd (rev b_tr ! length xs)) \<and> sr s (snd (rev d_tr ! length xs)) \<and> length xs < length d_tr \<and> fst (rev b_tr ! length xs) = Env \<and> fst (rev d_tr ! length xs) = Env \<and> AE (last_st_tr xs s0) s
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c sa xs. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip b_tr d_tr)); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; length xs < length b_tr; rely_cond AE s0 xs; AE (last_st_tr xs s0) sa; (if fst (rev b_tr ! length xs) = Env then fst (snd (zip (rev b_tr) (rev d_tr) ! length xs)) else fst (fst (zip (rev b_tr) (rev d_tr) ! length xs))) = Env; sr sa (snd (rev b_tr ! length xs)); matching_tr_pfx sr xs (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip b_tr d_tr))\<rbrakk> \<Longrightarrow> sr sa (snd (rev d_tr ! length xs)) \<and> fst (rev b_tr ! length xs) = Env \<and> fst (rev d_tr ! length xs) = Env
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c sa xs. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip b_tr d_tr)); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; length xs < length b_tr; rely_cond AE s0 xs; AE (last_st_tr xs s0) sa; (if fst (rev b_tr ! length xs) = Env then fst (snd (zip (rev b_tr) (rev d_tr) ! length xs)) else fst (fst (zip (rev b_tr) (rev d_tr) ! length xs))) = Env; sr sa (snd (rev b_tr ! length xs)); matching_tr_pfx sr xs (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip b_tr d_tr)); length b_tr = length d_tr\<rbrakk> \<Longrightarrow> sr sa (snd (rev d_tr ! length xs)) \<and> fst (rev b_tr ! length xs) = Env \<and> fst (rev d_tr ! length xs) = Env
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (3 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c sa xs. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip b_tr d_tr)); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; length xs < length d_tr; rely_cond AE s0 xs; AE (last_st_tr xs s0) sa; (if fst (rev b_tr ! length xs) = Env then fst (snd (zip (rev b_tr) (rev d_tr) ! length xs)) else fst (fst (zip (rev b_tr) (rev d_tr) ! length xs))) = Env; sr sa (snd (rev d_tr ! length xs)); matching_tr_pfx sr xs (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip b_tr d_tr)); length b_tr = length d_tr; (fst (rev b_tr ! length xs) = Env \<or> fst (rev d_tr ! length xs) = Env) \<and> snd (rev b_tr ! length xs) = snd (rev d_tr ! length xs)\<rbrakk> \<Longrightarrow> fst (rev b_tr ! length xs) = Env \<and> fst (rev d_tr ! length xs) = Env
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 3. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> rely (parallel f_a f_c) AE s0 s \<noteq> {}
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b f_steps. length f_steps = length a \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps a, b) \<in> f_a s \<and> (\<exists>res'. (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a, res') \<in> f_c s)) \<and> rely_cond AE s0 a
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> (\<exists>x. length [] = length [] \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) [] [], x) \<in> f_a s \<and> (\<exists>res'. (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) [] [], res') \<in> f_c s)) \<and> rely_cond AE s0 []
 2. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely (parallel f_a f_c) AE s0 s. case x of (tr, res) \<Rightarrow> rely_cond AE s0 tr \<and> matching_tr_pfx sr tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (length tr < length b_tr \<and> length tr < length d_tr \<longrightarrow> res = Incomplete) \<and> (length tr = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr res bd_res) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c aa ab ba. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; is_matching_fragment sr osr rvr b_tr bd_res s0 (AE or Gc) s f_a; triv_refinement a f_a; is_matching_fragment sr osr rvr d_tr bd_res s0 (AE or Ga) s f_c; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; rely_cond AE s0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) aa ab); (aa, ba) \<in> f_a s; (ab, ba) \<in> f_c s; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) aa ab\<rbrakk> \<Longrightarrow> matching_tr_pfx sr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) aa ab) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (min (length aa) (length ab) < length b_tr \<and> min (length aa) (length ab) < length d_tr \<longrightarrow> ba = Incomplete) \<and> (min (length aa) (length ab) = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr ba bd_res) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c aa ab ba. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; triv_refinement a f_a; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; rely_cond AE s0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) aa ab); (aa, ba) \<in> f_a s; (ab, ba) \<in> f_c s; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) aa ab; rely_cond (AE or Gc) s0 aa \<and> matching_tr_pfx sr aa b_tr \<and> (length aa < length b_tr \<longrightarrow> ba = Incomplete) \<and> (length aa = length b_tr \<longrightarrow> rel_tmres osr rvr ba bd_res); rely_cond (AE or Ga) s0 ab \<and> matching_tr_pfx sr ab d_tr \<and> (length ab < length d_tr \<longrightarrow> ba = Incomplete) \<and> (length ab = length d_tr \<longrightarrow> rel_tmres osr rvr ba bd_res)\<rbrakk> \<Longrightarrow> matching_tr_pfx sr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) aa ab) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) \<and> (min (length aa) (length ab) < length b_tr \<and> min (length aa) (length ab) < length d_tr \<longrightarrow> ba = Incomplete) \<and> (min (length aa) (length ab) = min (length b_tr) (length d_tr) \<longrightarrow> rel_tmres osr rvr ba bd_res) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c aa ab ba. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; triv_refinement a f_a; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; rely_cond AE s0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) aa ab); (aa, ba) \<in> f_a s; (ab, ba) \<in> f_c s; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) aa ab; rely_cond (AE or Gc) s0 aa; matching_tr_pfx sr aa b_tr; rely_cond (AE or Ga) s0 ab; matching_tr_pfx sr ab d_tr; length ab < length d_tr \<longrightarrow> ba = Incomplete; length ab = length d_tr \<longrightarrow> rel_tmres osr rvr ba bd_res\<rbrakk> \<Longrightarrow> matching_tr_pfx sr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) aa ab) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t b_tr d_tr bd_res f_a f_c aa ab ba. \<lbrakk>par_tr_fin_principle a; par_tr_fin_principle c; \<lbrace>Q\<rbrace>, \<lbrace>E or Gd\<rbrace> b \<lbrace>Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>Q\<rbrace>, \<lbrace>E or Gb\<rbrace> d \<lbrace>Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; Ga = (\<lambda>_ _. True) \<and> Gc = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<and> \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; isr s t; P s0 s; sr s0 t0; Q t0 t; rely_cond E t0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) b_tr d_tr); (b_tr, bd_res) \<in> b t; (d_tr, bd_res) \<in> d t; rely_cond (E or Gd) t0 b_tr; rely_cond (E or Gb) t0 d_tr; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) b_tr d_tr; triv_refinement a f_a; triv_refinement c f_c; \<lbrace>P\<rbrace>, \<lbrace>AE or Gc\<rbrace> f_a \<lbrace>Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>AE or Ga\<rbrace> f_c \<lbrace>Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; rely_cond AE s0 (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) aa ab); (aa, ba) \<in> f_a s; (ab, ba) \<in> f_c s; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) aa ab; rely_cond (AE or Gc) s0 aa; matching_tr_pfx sr aa b_tr; rely_cond (AE or Ga) s0 ab; matching_tr_pfx sr ab d_tr; length ab < length d_tr \<longrightarrow> ba = Incomplete; length ab = length d_tr \<longrightarrow> rel_tmres osr rvr ba bd_res\<rbrakk> \<Longrightarrow> length aa = length ab proof (prove)
goal:
No subgoals!