[STATEMENT]
lemma valid_trans:
  assumes   " \<Theta> ; \<B> ; \<Gamma> \<Turnstile> c0[z::=v]\<^sub>v"  and " \<Theta> ; \<B> ; (z,b,c0)#\<^sub>\<Gamma>\<Gamma> \<Turnstile> c1" and "atom z \<sharp> \<Gamma>" and "wfV \<Theta> \<B> \<Gamma> v b"
  shows " \<Theta> ; \<B> ; \<Gamma> \<Turnstile> c1[z::=v]\<^sub>v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
have *:"wfC \<Theta> \<B> ((z,b,c0)#\<^sub>\<Gamma>\<Gamma>) c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1
[PROOF STEP]
using valid.simps assms
[PROOF STATE]
proof (prove)
using this:
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c0[z::=v]\<^sub>v
\<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1
atom z \<sharp> \<Gamma>
 \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1

goal (1 subgoal):
 1. \<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
hence "wfC \<Theta> \<B> \<Gamma> (c1[z::=v]\<^sub>v)"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1[z::=v]\<^sub>v
[PROOF STEP]
using wf_subst1(2)[OF * , of GNil ]  assms subst_gv.simps subst_v_c_def
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1
\<lbrakk>(z, b, c0) #\<^sub>\<Gamma> \<Gamma> = GNil @ (?x, ?b', ?c') #\<^sub>\<Gamma> ?\<Gamma>\<^sub>2;  \<Theta> ; \<B> ; ?\<Gamma>\<^sub>2 \<turnstile>\<^sub>w\<^sub>f ?v' : ?b' \<rbrakk> \<Longrightarrow>  \<Theta> ; \<B> ; ((z, b, c0) #\<^sub>\<Gamma> \<Gamma>)[?x::=?v']\<^sub>\<Gamma>\<^sub>v   \<turnstile>\<^sub>w\<^sub>f c1[?x::=?v']\<^sub>c\<^sub>v
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c0[z::=v]\<^sub>v
\<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1
atom z \<sharp> \<Gamma>
 \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
GNil[?x::=?v]\<^sub>\<Gamma>\<^sub>v = GNil
((?y, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?x::=?v]\<^sub>\<Gamma>\<^sub>v = (if ?x = ?y then ?\<Gamma> else (?y, ?b, ?c[?x::=?v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> ?\<Gamma>[?x::=?v]\<^sub>\<Gamma>\<^sub>v)
subst_v = subst_cv_abbrev

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1[z::=v]\<^sub>v
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1[z::=v]\<^sub>v

goal (1 subgoal):
 1. \<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1[z::=v]\<^sub>v

goal (1 subgoal):
 1. \<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
have "\<forall>i. wfI  \<Theta> \<Gamma>   i \<and> is_satis_g i \<Gamma> \<longrightarrow> is_satis i (c1[z::=v]\<^sub>v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
proof(rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
assume  as: "wfI  \<Theta> \<Gamma>   i \<and> is_satis_g i \<Gamma>"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>
[PROOF STEP]
obtain sv where sv: "eval_v i v sv \<and> wfRCV \<Theta> sv b"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>

goal (1 subgoal):
 1. (\<And>sv. i \<lbrakk> v \<rbrakk> ~ sv  \<and>  \<Theta>  \<turnstile> sv : b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_exist assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c0[z::=v]\<^sub>v
\<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1
atom z \<sharp> \<Gamma>
 \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

goal (1 subgoal):
 1. (\<And>sv. i \<lbrakk> v \<rbrakk> ~ sv  \<and>  \<Theta>  \<turnstile> sv : b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ sv  \<and>  \<Theta>  \<turnstile> sv : b

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
hence "is_satis i (c0[z::=v]\<^sub>v)"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ sv  \<and>  \<Theta>  \<turnstile> sv : b

goal (1 subgoal):
 1.  i \<Turnstile> c0[z::=v]\<^sub>v
[PROOF STEP]
using assms valid.simps as
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ sv  \<and>  \<Theta>  \<turnstile> sv : b
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c0[z::=v]\<^sub>v
\<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1
atom z \<sharp> \<Gamma>
 \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>

goal (1 subgoal):
 1.  i \<Turnstile> c0[z::=v]\<^sub>v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c0[z::=v]\<^sub>v

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
hence "is_satis (i(z \<mapsto> sv))  c0"
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c0[z::=v]\<^sub>v

goal (1 subgoal):
 1.  i(z \<mapsto> sv) \<Turnstile> c0
[PROOF STEP]
using subst_c_satis sv as assms valid.simps wfC_wf wfG_elim2 subst_v_c_def
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c0[z::=v]\<^sub>v
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ;  ?\<Theta> ; ?B ; (?x, ?b, ?c') #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i;  ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow>  ?i \<Turnstile> ?c[?x::=?v]\<^sub>c\<^sub>v  =  ?i(?x \<mapsto> ?s) \<Turnstile> ?c
i \<lbrakk> v \<rbrakk> ~ sv  \<and>  \<Theta>  \<turnstile> sv : b
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c0[z::=v]\<^sub>v
\<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1
atom z \<sharp> \<Gamma>
 \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>  \<Longrightarrow>  ?P ; ?\<B> ; (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<and>  ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b
subst_v = subst_cv_abbrev

goal (1 subgoal):
 1.  i(z \<mapsto> sv) \<Turnstile> c0
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(z \<mapsto> sv) \<Turnstile> c0

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i(z \<mapsto> sv) \<Turnstile> c0

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
have "is_satis_g  (i(z \<mapsto> sv)) \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i(z \<mapsto> sv) \<Turnstile> \<Gamma>
[PROOF STEP]
using is_satis_g_i_upd  assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom ?x \<sharp> ?G;  ?i \<Turnstile> ?G \<rbrakk> \<Longrightarrow>  ?i(?x \<mapsto> ?s) \<Turnstile> ?G
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c0[z::=v]\<^sub>v
\<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1
atom z \<sharp> \<Gamma>
 \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

goal (1 subgoal):
 1.  i(z \<mapsto> sv) \<Turnstile> \<Gamma>
[PROOF STEP]
by (simp add: as)
[PROOF STATE]
proof (state)
this:
 i(z \<mapsto> sv) \<Turnstile> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i(z \<mapsto> sv) \<Turnstile> c0
 i(z \<mapsto> sv) \<Turnstile> \<Gamma>
[PROOF STEP]
have "is_satis_g  (i(z \<mapsto> sv)) ((z,b,c0)#\<^sub>\<Gamma>\<Gamma>)"
[PROOF STATE]
proof (prove)
using this:
 i(z \<mapsto> sv) \<Turnstile> c0
 i(z \<mapsto> sv) \<Turnstile> \<Gamma>

goal (1 subgoal):
 1.  i(z \<mapsto> sv) \<Turnstile> (z, b, c0) #\<^sub>\<Gamma> \<Gamma>
[PROOF STEP]
using is_satis_g.simps
[PROOF STATE]
proof (prove)
using this:
 i(z \<mapsto> sv) \<Turnstile> c0
 i(z \<mapsto> sv) \<Turnstile> \<Gamma>
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )

goal (1 subgoal):
 1.  i(z \<mapsto> sv) \<Turnstile> (z, b, c0) #\<^sub>\<Gamma> \<Gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 i(z \<mapsto> sv) \<Turnstile> (z, b, c0) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i(z \<mapsto> sv) \<Turnstile> (z, b, c0) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
have "wfI \<Theta> ((z,b,c0)#\<^sub>\<Gamma>\<Gamma>) (i(z \<mapsto> sv))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(z \<mapsto> sv)
[PROOF STEP]
using as wfI_upd sv assms valid.simps wfC_wf
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>
\<lbrakk> ?\<Theta> ; ?\<Gamma> \<turnstile> ?i;  ?\<Theta>  \<turnstile> ?s : ?b;  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> \<turnstile> ?i(?x \<mapsto> ?s)
i \<lbrakk> v \<rbrakk> ~ sv  \<and>  \<Theta>  \<turnstile> sv : b
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c0[z::=v]\<^sub>v
\<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1
atom z \<sharp> \<Gamma>
 \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>

goal (1 subgoal):
 1.  \<Theta> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(z \<mapsto> sv)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(z \<mapsto> sv)

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i(z \<mapsto> sv) \<Turnstile> (z, b, c0) #\<^sub>\<Gamma> \<Gamma>
 \<Theta> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(z \<mapsto> sv)
[PROOF STEP]
have "is_satis (i(z \<mapsto> sv)) c1"
[PROOF STATE]
proof (prove)
using this:
 i(z \<mapsto> sv) \<Turnstile> (z, b, c0) #\<^sub>\<Gamma> \<Gamma>
 \<Theta> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(z \<mapsto> sv)

goal (1 subgoal):
 1.  i(z \<mapsto> sv) \<Turnstile> c1
[PROOF STEP]
using assms valid.simps
[PROOF STATE]
proof (prove)
using this:
 i(z \<mapsto> sv) \<Turnstile> (z, b, c0) #\<^sub>\<Gamma> \<Gamma>
 \<Theta> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(z \<mapsto> sv)
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c0[z::=v]\<^sub>v
\<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1
atom z \<sharp> \<Gamma>
 \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))

goal (1 subgoal):
 1.  i(z \<mapsto> sv) \<Turnstile> c1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i(z \<mapsto> sv) \<Turnstile> c1

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
thus "is_satis i (c1[z::=v]\<^sub>v)"
[PROOF STATE]
proof (prove)
using this:
 i(z \<mapsto> sv) \<Turnstile> c1

goal (1 subgoal):
 1.  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
using subst_c_satis sv as assms valid.simps wfC_wf wfG_elim2 subst_v_c_def
[PROOF STATE]
proof (prove)
using this:
 i(z \<mapsto> sv) \<Turnstile> c1
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ;  ?\<Theta> ; ?B ; (?x, ?b, ?c') #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i;  ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow>  ?i \<Turnstile> ?c[?x::=?v]\<^sub>c\<^sub>v  =  ?i(?x \<mapsto> ?s) \<Turnstile> ?c
i \<lbrakk> v \<rbrakk> ~ sv  \<and>  \<Theta>  \<turnstile> sv : b
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c0[z::=v]\<^sub>v
\<Theta> ; \<B> ; (z, b, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1
atom z \<sharp> \<Gamma>
 \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>  \<Longrightarrow>  ?P ; ?\<B> ; (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<and>  ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b
subst_v = subst_cv_abbrev

goal (1 subgoal):
 1.  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c1[z::=v]\<^sub>v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v

goal (1 subgoal):
 1. \<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1[z::=v]\<^sub>v
\<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1[z::=v]\<^sub>v
\<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v

goal (1 subgoal):
 1. \<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
using valid.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1[z::=v]\<^sub>v
\<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> c1[z::=v]\<^sub>v
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))

goal (1 subgoal):
 1. \<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c1[z::=v]\<^sub>v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> c1[z::=v]\<^sub>v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_trans_full:
  assumes  "\<Theta> ; \<B> ; ((x, b, c1[z1::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>) \<Turnstile> c2[z2::=V_var x]\<^sub>v" and
    "\<Theta> ; \<B> ; ((x, b, c2[z2::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>) \<Turnstile> c3[z3::=V_var x]\<^sub>v"
  shows  "\<Theta> ; \<B> ; ((x, b, c1[z1::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>) \<Turnstile> c3[z3::=V_var x]\<^sub>v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
unfolding valid.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c3[z3::=[ x ]\<^sup>v]\<^sub>v  \<and> (\<forall>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v )
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  \<Theta> ; \<B> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c3[z3::=[ x ]\<^sup>v]\<^sub>v
 2. \<forall>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
show "\<Theta> ; \<B> ; (x, b, c1[z1::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c3[z3::=V_var x]\<^sub>v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
using wf_trans valid.simps assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b' ; ?\<Gamma> = (?x, ?b, ?c2.0) #\<^sub>\<Gamma> ?G;  ?\<Theta> ; ?\<B> ; (?x, ?b, ?c1.0) #\<^sub>\<Gamma> ?G   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; (?x, ?b, ?c1.0) #\<^sub>\<Gamma> ?G \<turnstile>\<^sub>w\<^sub>f ?v : ?b'
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ; ?\<Gamma> = (?x, ?b, ?c2.0) #\<^sub>\<Gamma> ?G;  ?\<Theta> ; ?\<B> ; (?x, ?b, ?c1.0) #\<^sub>\<Gamma> ?G   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; (?x, ?b, ?c1.0) #\<^sub>\<Gamma> ?G   \<turnstile>\<^sub>w\<^sub>f ?c
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> True
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>  \<Longrightarrow> True
 ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts  \<Longrightarrow> True
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> True
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b  \<Longrightarrow> True
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ce : ?b' ; ?\<Gamma> = (?x, ?b, ?c2.0) #\<^sub>\<Gamma> ?G;  ?\<Theta> ; ?\<B> ; (?x, ?b, ?c1.0) #\<^sub>\<Gamma> ?G   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?\<B> ; (?x, ?b, ?c1.0) #\<^sub>\<Gamma> ?G \<turnstile>\<^sub>w\<^sub>f ?ce : ?b'
 ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?td  \<Longrightarrow> True
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))
\<Theta> ; \<B> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v
\<Theta> ; \<B> ; (x, b, c2[z2::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c3[z3::=[ x ]\<^sup>v]\<^sub>v

goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
show "\<forall>i.  ( wfI  \<Theta> ((x, b, c1[z1::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>) i \<and>  (is_satis_g i ((x, b, c1[z1::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>))  \<longrightarrow>  (is_satis i (c3[z3::=V_var x]\<^sub>v)) ) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
proof(rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
assume as: "\<Theta> ; (x, b, c1[z1::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
have "i \<Turnstile> c2[z2::=V_var x]\<^sub>v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
using is_satis_g.simps as assms
[PROOF STATE]
proof (prove)
using this:
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )
 \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>
\<Theta> ; \<B> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v
\<Theta> ; \<B> ; (x, b, c2[z2::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v

goal (1 subgoal):
 1.  i \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
have  "i \<Turnstile> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> \<Gamma>
[PROOF STEP]
using is_satis_g.simps as
[PROOF STATE]
proof (prove)
using this:
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )
 \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1.  i \<Turnstile> \<Gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v
 i \<Turnstile> \<Gamma>
[PROOF STEP]
show "i \<Turnstile> c3[z3::=V_var x]\<^sub>v "
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v
 i \<Turnstile> \<Gamma>

goal (1 subgoal):
 1.  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
using assms is_satis_g.simps valid.simps
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v
 i \<Turnstile> \<Gamma>
\<Theta> ; \<B> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c2[z2::=[ x ]\<^sup>v]\<^sub>v
\<Theta> ; \<B> ; (x, b, c2[z2::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))

goal (1 subgoal):
 1.  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v
[PROOF STEP]
by (metis append_g.simps(1) as wfI_replace_inside)
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c1[z1::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> c3[z3::=[ x ]\<^sup>v]\<^sub>v

goal:
No subgoals!
[PROOF STEP]
qed