[STATEMENT]
lemma eval_c_i_weakening:
  fixes c::c and B::"bv fset"
  assumes  "i \<lbrakk> c \<rbrakk> ~ s" and "i = i' |` d" and "supp c \<subseteq> atom ` d \<union> supp B"
  shows "i' \<lbrakk> c \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c \<rbrakk> ~ s
i = i' |` d
supp c \<subseteq> atom ` d \<union> supp B

goal (1 subgoal):
 1.  i' \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
proof(induct rule:eval_c.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>i. \<lbrakk>i = i' |` d; supp (TRUE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>i. \<lbrakk>i = i' |` d; supp (FALSE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = i' |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = i' |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c2 \<rbrakk> ~ b2 ; i = i' |` d; supp (c1  AND  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = i' |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = i' |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c2 \<rbrakk> ~ b2 ; i = i' |` d; supp (c1 OR c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = i' |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = i' |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c2 \<rbrakk> ~ b2 ; i = i' |` d; supp (c1  IMP  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>i c b. \<lbrakk> i \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>i = i' |` d; supp c \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c \<rbrakk> ~ b ; i = i' |` d; supp (\<not> c ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 7. \<And>i e1 sv1 e2 sv2. \<lbrakk>i \<lbrakk> e1 \<rbrakk> ~ sv1 ; i \<lbrakk> e2 \<rbrakk> ~ sv2 ; i = i' |` d; supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_eqI i e1 sv1 e2 sv2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
i = i' |` d
supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B

goal (7 subgoals):
 1. \<And>i. \<lbrakk>i = i' |` d; supp (TRUE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>i. \<lbrakk>i = i' |` d; supp (FALSE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = i' |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = i' |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c2 \<rbrakk> ~ b2 ; i = i' |` d; supp (c1  AND  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = i' |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = i' |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c2 \<rbrakk> ~ b2 ; i = i' |` d; supp (c1 OR c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = i' |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = i' |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c2 \<rbrakk> ~ b2 ; i = i' |` d; supp (c1  IMP  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>i c b. \<lbrakk> i \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>i = i' |` d; supp c \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c \<rbrakk> ~ b ; i = i' |` d; supp (\<not> c ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 7. \<And>i e1 sv1 e2 sv2. \<lbrakk>i \<lbrakk> e1 \<rbrakk> ~ sv1 ; i \<lbrakk> e2 \<rbrakk> ~ sv2 ; i = i' |` d; supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
i = i' |` d
supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
i = i' |` d
supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B

goal (1 subgoal):
 1.  i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
using eval_c.intros eval_e_weakening
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
i = i' |` d
supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0
\<lbrakk>?i \<lbrakk> ?e \<rbrakk> ~ ?s ; ?i = ?i' |` ?d; supp ?e \<subseteq> atom ` ?d \<union> supp ?B\<rbrakk> \<Longrightarrow> ?i' \<lbrakk> ?e \<rbrakk> ~ ?s

goal (1 subgoal):
 1.  i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2

goal (6 subgoals):
 1. \<And>i. \<lbrakk>i = i' |` d; supp (TRUE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>i. \<lbrakk>i = i' |` d; supp (FALSE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = i' |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = i' |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c2 \<rbrakk> ~ b2 ; i = i' |` d; supp (c1  AND  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = i' |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = i' |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c2 \<rbrakk> ~ b2 ; i = i' |` d; supp (c1 OR c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = i' |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = i' |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c2 \<rbrakk> ~ b2 ; i = i' |` d; supp (c1  IMP  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>i c b. \<lbrakk> i \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>i = i' |` d; supp c \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> c \<rbrakk> ~ b ; i = i' |` d; supp (\<not> c ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i' \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
[PROOF STEP]
qed(auto simp add: eval_c.intros)+


[STATEMENT]
lemma eval_c_i_restrict:
  fixes c::c and B::"bv fset"
  assumes  "i' \<lbrakk> c \<rbrakk> ~ s" and "i = i' |` d" and "supp c \<subseteq> atom ` d \<union> supp B"
  shows "i \<lbrakk> c \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c \<rbrakk> ~ s
i = i' |` d
supp c \<subseteq> atom ` d \<union> supp B

goal (1 subgoal):
 1.  i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
proof(induct rule:eval_c.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>ia. \<lbrakk>i = ia |` d; supp (TRUE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>ia. \<lbrakk>i = ia |` d; supp (FALSE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = ia |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = ia |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; i = ia |` d; supp (c1  AND  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = ia |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = ia |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; i = ia |` d; supp (c1 OR c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = ia |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = ia |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; i = ia |` d; supp (c1  IMP  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>i = ia |` d; supp c \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; i = ia |` d; supp (\<not> c ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 7. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; i = ia |` d; supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_eqI i e1 sv1 e2 sv2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
i = i |` d
supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B

goal (7 subgoals):
 1. \<And>ia. \<lbrakk>i = ia |` d; supp (TRUE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>ia. \<lbrakk>i = ia |` d; supp (FALSE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = ia |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = ia |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; i = ia |` d; supp (c1  AND  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = ia |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = ia |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; i = ia |` d; supp (c1 OR c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = ia |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = ia |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; i = ia |` d; supp (c1  IMP  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>i = ia |` d; supp c \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; i = ia |` d; supp (\<not> c ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 7. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; i = ia |` d; supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
i = i |` d
supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
i = i |` d
supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B

goal (1 subgoal):
 1.  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
using eval_c.intros eval_e_restrict
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
i = i |` d
supp (e1  ==  e2 ) \<subseteq> atom ` d \<union> supp B
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0
\<lbrakk>?i' \<lbrakk> ?e \<rbrakk> ~ ?s ; ?i = ?i' |` ?d; supp ?e \<subseteq> atom ` ?d \<union> supp ?B\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?e \<rbrakk> ~ ?s

goal (1 subgoal):
 1.  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2

goal (6 subgoals):
 1. \<And>ia. \<lbrakk>i = ia |` d; supp (TRUE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>ia. \<lbrakk>i = ia |` d; supp (FALSE) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = ia |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = ia |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; i = ia |` d; supp (c1  AND  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = ia |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = ia |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; i = ia |` d; supp (c1 OR c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>i = ia |` d; supp c1 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>i = ia |` d; supp c2 \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; i = ia |` d; supp (c1  IMP  c2 ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>i = ia |` d; supp c \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; i = ia |` d; supp (\<not> c ) \<subseteq> atom ` d \<union> supp B\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
[PROOF STEP]
qed(auto simp add: eval_c.intros)+


[STATEMENT]
lemma is_satis_i_weakening:
  fixes c::c and B::"bv fset"
  assumes "i = i' |` d" and "supp c \<subseteq> atom ` d  \<union> supp B " and  "i \<Turnstile> c"
  shows "i' \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
using is_satis.simps eval_c_i_weakening[OF _ assms(1) assms(2) ]
[PROOF STATE]
proof (prove)
using this:
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )
 i \<lbrakk> c \<rbrakk> ~ ?s  \<Longrightarrow>  i' \<lbrakk> c \<rbrakk> ~ ?s

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )
 i \<lbrakk> c \<rbrakk> ~ ?s  \<Longrightarrow>  i' \<lbrakk> c \<rbrakk> ~ ?s
 i \<Turnstile> c

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
by auto


[STATEMENT]
lemma is_satis_i_restrict:
  fixes c::c and B::"bv fset"
  assumes "i = i' |` d" and "supp c \<subseteq> atom ` d  \<union> supp B" and  "i' \<Turnstile> c"
  shows "i \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
using is_satis.simps eval_c_i_restrict[OF _ assms(1) assms(2) ]
[PROOF STATE]
proof (prove)
using this:
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )
 i' \<lbrakk> c \<rbrakk> ~ ?s  \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ ?s

goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )
 i' \<lbrakk> c \<rbrakk> ~ ?s  \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ ?s
 i' \<Turnstile> c

goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
by auto


[STATEMENT]
lemma is_satis_g_restrict1:
  fixes \<Gamma>'::\<Gamma> and  \<Gamma>::\<Gamma>
  assumes "toSet \<Gamma> \<subseteq> toSet \<Gamma>'" and "i \<Turnstile> \<Gamma>'"
  shows "i \<Turnstile> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 i \<Turnstile> \<Gamma>'

goal (1 subgoal):
 1.  i \<Turnstile> \<Gamma>
[PROOF STEP]
proof(induct \<Gamma> rule: \<Gamma>.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>toSet GNil \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> GNil
 2. \<And>x1 x2. \<lbrakk>\<lbrakk>toSet x2 \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x2 ; toSet (x1 #\<^sub>\<Gamma> x2) \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x1 #\<^sub>\<Gamma> x2
[PROOF STEP]
case GNil
[PROOF STATE]
proof (state)
this:
toSet GNil \<subseteq> toSet \<Gamma>'
 i \<Turnstile> \<Gamma>'

goal (2 subgoals):
 1. \<lbrakk>toSet GNil \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> GNil
 2. \<And>x1 x2. \<lbrakk>\<lbrakk>toSet x2 \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x2 ; toSet (x1 #\<^sub>\<Gamma> x2) \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x1 #\<^sub>\<Gamma> x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
toSet GNil \<subseteq> toSet \<Gamma>'
 i \<Turnstile> \<Gamma>'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
toSet GNil \<subseteq> toSet \<Gamma>'
 i \<Turnstile> \<Gamma>'

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

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk>toSet x2 \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x2 ; toSet (x1 #\<^sub>\<Gamma> x2) \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x1 #\<^sub>\<Gamma> x2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk>toSet x2 \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x2 ; toSet (x1 #\<^sub>\<Gamma> x2) \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x1 #\<^sub>\<Gamma> x2
[PROOF STEP]
case (GCons xbc G)
[PROOF STATE]
proof (state)
this:
\<lbrakk>toSet G \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
toSet (xbc #\<^sub>\<Gamma> G) \<subseteq> toSet \<Gamma>'
 i \<Turnstile> \<Gamma>'

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk>toSet x2 \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x2 ; toSet (x1 #\<^sub>\<Gamma> x2) \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x1 #\<^sub>\<Gamma> x2
[PROOF STEP]
obtain x and b and c::c where xbc: "xbc=(x,b,c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x b c. xbc = (x, b, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod_cases3
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c. ?y = (a, b, c) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x b c. xbc = (x, b, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xbc = (x, b, c)

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk>toSet x2 \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x2 ; toSet (x1 #\<^sub>\<Gamma> x2) \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x1 #\<^sub>\<Gamma> x2
[PROOF STEP]
hence "i \<Turnstile> G"
[PROOF STATE]
proof (prove)
using this:
xbc = (x, b, c)

goal (1 subgoal):
 1.  i \<Turnstile> G
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
xbc = (x, b, c)
\<lbrakk>toSet G \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
toSet (xbc #\<^sub>\<Gamma> G) \<subseteq> toSet \<Gamma>'
 i \<Turnstile> \<Gamma>'

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

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk>toSet x2 \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x2 ; toSet (x1 #\<^sub>\<Gamma> x2) \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x1 #\<^sub>\<Gamma> x2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> G

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk>toSet x2 \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x2 ; toSet (x1 #\<^sub>\<Gamma> x2) \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x1 #\<^sub>\<Gamma> x2
[PROOF STEP]
have "i \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
using GCons
      is_satis_iff toSet.simps  subset_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>toSet G \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
toSet (xbc #\<^sub>\<Gamma> G) \<subseteq> toSet \<Gamma>'
 i \<Turnstile> \<Gamma>'
 ?i \<Turnstile> ?G  = (\<forall>x b c. (x, b, c) \<in> toSet ?G \<longrightarrow>  ?i \<Turnstile> c )
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)

goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
using xbc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>toSet G \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
toSet (xbc #\<^sub>\<Gamma> G) \<subseteq> toSet \<Gamma>'
 i \<Turnstile> \<Gamma>'
 ?i \<Turnstile> ?G  = (\<forall>x b c. (x, b, c) \<in> toSet ?G \<longrightarrow>  ?i \<Turnstile> c )
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)
xbc = (x, b, c)

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

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk>toSet x2 \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x2 ; toSet (x1 #\<^sub>\<Gamma> x2) \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> x1 #\<^sub>\<Gamma> x2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i \<Turnstile> G
 i \<Turnstile> c
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> G
 i \<Turnstile> c

goal (1 subgoal):
 1.  i \<Turnstile> xbc #\<^sub>\<Gamma> G
[PROOF STEP]
using is_satis_g.simps GCons
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> G
 i \<Turnstile> c
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )
\<lbrakk>toSet G \<subseteq> toSet \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
toSet (xbc #\<^sub>\<Gamma> G) \<subseteq> toSet \<Gamma>'
 i \<Turnstile> \<Gamma>'

goal (1 subgoal):
 1.  i \<Turnstile> xbc #\<^sub>\<Gamma> G
[PROOF STEP]
by (simp add: xbc)
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> xbc #\<^sub>\<Gamma> G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_g_restrict2:
  fixes \<Gamma>'::\<Gamma> and  \<Gamma>::\<Gamma>
  assumes "i \<Turnstile> \<Gamma>" and  "i' = i |` d" and "atom_dom \<Gamma> \<subseteq> atom ` d" and "\<Theta> ; B \<turnstile>\<^sub>w\<^sub>f \<Gamma>"
  shows "i' \<Turnstile> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<Turnstile> \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> \<Gamma>
i' = i |` d
atom_dom \<Gamma> \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>

goal (1 subgoal):
 1.  i' \<Turnstile> \<Gamma>
[PROOF STEP]
proof(induct \<Gamma> rule: \<Gamma>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk> i \<Turnstile> GNil ; i' = i |` d; atom_dom GNil \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f GNil \<rbrakk> \<Longrightarrow>  i' \<Turnstile> GNil
 2. \<And>x b c \<Gamma>'. \<lbrakk>\<lbrakk> i \<Turnstile> \<Gamma>' ; i' = i |` d; atom_dom \<Gamma>' \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>' ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
case GNil
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> GNil
i' = i |` d
atom_dom GNil \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f GNil

goal (2 subgoals):
 1. \<lbrakk> i \<Turnstile> GNil ; i' = i |` d; atom_dom GNil \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f GNil \<rbrakk> \<Longrightarrow>  i' \<Turnstile> GNil
 2. \<And>x b c \<Gamma>'. \<lbrakk>\<lbrakk> i \<Turnstile> \<Gamma>' ; i' = i |` d; atom_dom \<Gamma>' \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>' ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<Turnstile> GNil
i' = i |` d
atom_dom GNil \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f GNil
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> GNil
i' = i |` d
atom_dom GNil \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f GNil

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

goal (1 subgoal):
 1. \<And>x b c \<Gamma>'. \<lbrakk>\<lbrakk> i \<Turnstile> \<Gamma>' ; i' = i |` d; atom_dom \<Gamma>' \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>' ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x b c \<Gamma>'. \<lbrakk>\<lbrakk> i \<Turnstile> \<Gamma>' ; i' = i |` d; atom_dom \<Gamma>' \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>' ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
case (GCons x b c G)
[PROOF STATE]
proof (state)
this:
\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
i' = i |` d
atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1. \<And>x b c \<Gamma>'. \<lbrakk>\<lbrakk> i \<Turnstile> \<Gamma>' ; i' = i |` d; atom_dom \<Gamma>' \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>' ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
hence "i' \<Turnstile> G"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
i' = i |` d
atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1.  i' \<Turnstile> G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
[PROOF STEP]
have "i \<Turnstile> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> G
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
i' = i |` d
atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G

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

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> G

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
[PROOF STEP]
have "atom_dom G \<subseteq> atom ` d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom_dom G \<subseteq> atom ` d
[PROOF STEP]
using  GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
i' = i |` d
atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1. atom_dom G \<subseteq> atom ` d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom_dom G \<subseteq> atom ` d

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i \<Turnstile> G
atom_dom G \<subseteq> atom ` d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> G
atom_dom G \<subseteq> atom ` d

goal (1 subgoal):
 1.  i' \<Turnstile> G
[PROOF STEP]
using GCons wfG_cons2
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> G
atom_dom G \<subseteq> atom ` d
\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
i' = i |` d
atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G
 ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?zbc #\<^sub>\<Gamma> ?\<Gamma>  \<Longrightarrow>  ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i' \<Turnstile> G

goal (1 subgoal):
 1. \<And>x b c \<Gamma>'. \<lbrakk>\<lbrakk> i \<Turnstile> \<Gamma>' ; i' = i |` d; atom_dom \<Gamma>' \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>' ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i' \<Turnstile> G

goal (1 subgoal):
 1. \<And>x b c \<Gamma>'. \<lbrakk>\<lbrakk> i \<Turnstile> \<Gamma>' ; i' = i |` d; atom_dom \<Gamma>' \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>' ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
have "i' \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
have "i \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
i' = i |` d
atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G

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

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
have "\<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c
[PROOF STEP]
using wfG_wfC GCons
[PROOF STATE]
proof (prove)
using this:
 ?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
\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
i' = i |` d
atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1.  \<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 \<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 \<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
hence "supp c \<subseteq> atom ` d \<union> supp B"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c

goal (1 subgoal):
 1. supp c \<subseteq> atom ` d \<union> supp B
[PROOF STEP]
using wfC_supp GCons atom_dom_eq
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow> supp ?c \<subseteq> atom_dom ?\<Gamma> \<union> supp ?\<B>
\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
i' = i |` d
atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G
atom_dom ((?x, ?b, ?c) #\<^sub>\<Gamma> ?G) = atom_dom ((?x, ?b, ?c') #\<^sub>\<Gamma> ?G)

goal (1 subgoal):
 1. supp c \<subseteq> atom ` d \<union> supp B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
supp c \<subseteq> atom ` d \<union> supp B

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i \<Turnstile> c
 \<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c
supp c \<subseteq> atom ` d \<union> supp B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c
 \<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c
supp c \<subseteq> atom ` d \<union> supp B

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
using is_satis_i_restrict[of i' i d c] GCons
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c
 \<Theta> ; B ; (x, b, TRUE) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c
supp c \<subseteq> atom ` d \<union> supp B
\<lbrakk>i' = i |` d; supp c \<subseteq> atom ` d \<union> supp ?B;  i \<Turnstile> c \<rbrakk> \<Longrightarrow>  i' \<Turnstile> c
\<lbrakk> i \<Turnstile> G ; i' = i |` d; atom_dom G \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  i' \<Turnstile> G
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
i' = i |` d
atom_dom ((x, b, c) #\<^sub>\<Gamma> G) \<subseteq> atom ` d
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> G

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i' \<Turnstile> c

goal (1 subgoal):
 1. \<And>x b c \<Gamma>'. \<lbrakk>\<lbrakk> i \<Turnstile> \<Gamma>' ; i' = i |` d; atom_dom \<Gamma>' \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>' ; i' = i |` d; atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> atom ` d;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i' \<Turnstile> G
 i' \<Turnstile> c
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i' \<Turnstile> G
 i' \<Turnstile> c

goal (1 subgoal):
 1.  i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i' \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_g_restrict:
  fixes \<Gamma>'::\<Gamma> and \<Gamma>::\<Gamma>
  assumes "toSet \<Gamma> \<subseteq> toSet \<Gamma>'" and "i' \<Turnstile> \<Gamma>'" and  "i =   i' |` (fst ` toSet \<Gamma>)"  and "\<Theta> ; B \<turnstile>\<^sub>w\<^sub>f \<Gamma>"
  shows "i \<Turnstile> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> \<Gamma>
[PROOF STEP]
using assms is_satis_g_restrict1[OF assms(1) assms(2)] is_satis_g_restrict2[OF _ assms(3)]
[PROOF STATE]
proof (prove)
using this:
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 i' \<Turnstile> \<Gamma>'
i = i' |` (fst ` toSet \<Gamma>)
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 i' \<Turnstile> \<Gamma>
\<lbrakk> i' \<Turnstile> ?\<Gamma> ; atom_dom ?\<Gamma> \<subseteq> atom ` fst ` toSet \<Gamma>;  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow>  i \<Turnstile> ?\<Gamma>

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


[STATEMENT]
lemma is_satis_c_i_upd:
  fixes c::c
  assumes "atom x \<sharp> c" and "i \<Turnstile> c"
  shows "((i ( x \<mapsto>s))) \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
using assms eval_c_i_upd is_satis.simps
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> c
 i \<Turnstile> c
\<lbrakk> ?i \<lbrakk> ?c \<rbrakk> ~ ?s' ; atom ?x \<sharp> ?c\<rbrakk> \<Longrightarrow>  ?i(?x \<mapsto> ?s) \<lbrakk> ?c \<rbrakk> ~ ?s'
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
by simp


[STATEMENT]
lemma is_satis_g_i_upd:
  fixes G::\<Gamma>
  assumes "atom x \<sharp> G"  and "i \<Turnstile> G"
  shows "((i ( x \<mapsto>s))) \<Turnstile> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> G
 i \<Turnstile> G

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> G
[PROOF STEP]
proof(induct G rule: \<Gamma>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>atom x \<sharp> GNil;  i \<Turnstile> GNil \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> GNil
 2. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
case GNil
[PROOF STATE]
proof (state)
this:
atom x \<sharp> GNil
 i \<Turnstile> GNil

goal (2 subgoals):
 1. \<lbrakk>atom x \<sharp> GNil;  i \<Turnstile> GNil \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> GNil
 2. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> GNil
 i \<Turnstile> GNil
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> GNil
 i \<Turnstile> GNil

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> GNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> GNil

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
case (GCons x' b' c' G')
[PROOF STATE]
proof (state)
this:
\<lbrakk>atom x \<sharp> G';  i \<Turnstile> G' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> G'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> G'
 i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
hence *:"atom x \<sharp> G' \<and> atom x \<sharp> c'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom x \<sharp> G';  i \<Turnstile> G' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> G'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> G'
 i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'

goal (1 subgoal):
 1. atom x \<sharp> G' \<and> atom x \<sharp> c'
[PROOF STEP]
using fresh_def fresh_GCons GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom x \<sharp> G';  i \<Turnstile> G' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> G'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> G'
 i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'
?a \<sharp> ?x \<equiv> ?a \<notin> supp ?x
?a \<sharp> ?x #\<^sub>\<Gamma> ?xs = (?a \<sharp> ?x \<and> ?a \<sharp> ?xs)
\<lbrakk>atom x \<sharp> G';  i \<Turnstile> G' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> G'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> G'
 i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'

goal (1 subgoal):
 1. atom x \<sharp> G' \<and> atom x \<sharp> c'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
atom x \<sharp> G' \<and> atom x \<sharp> c'

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom x \<sharp> G' \<and> atom x \<sharp> c'

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
hence "is_satis ((i ( x \<mapsto>s))) c'"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> G' \<and> atom x \<sharp> c'

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> c'
[PROOF STEP]
using is_satis_c_i_upd GCons is_satis_g.simps
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> G' \<and> atom x \<sharp> c'
\<lbrakk>atom ?x \<sharp> ?c;  ?i \<Turnstile> ?c \<rbrakk> \<Longrightarrow>  ?i(?x \<mapsto> ?s) \<Turnstile> ?c
\<lbrakk>atom x \<sharp> G';  i \<Turnstile> G' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> G'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> G'
 i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> c'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> c'

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> c'

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
have " is_satis_g (i(x \<mapsto> s)) G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> G'
[PROOF STEP]
using GCons *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom x \<sharp> G';  i \<Turnstile> G' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> G'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> G'
 i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'
atom x \<sharp> G' \<and> atom x \<sharp> c'

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> G'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> G'

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk>atom x \<sharp> \<Gamma>';  i \<Turnstile> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>';  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> G' \<and> atom x \<sharp> c'
 i(x \<mapsto> s) \<Turnstile> c'
 i(x \<mapsto> s) \<Turnstile> G'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> G' \<and> atom x \<sharp> c'
 i(x \<mapsto> s) \<Turnstile> c'
 i(x \<mapsto> s) \<Turnstile> G'

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'
[PROOF STEP]
using GCons is_satis_g.simps(2)
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> G' \<and> atom x \<sharp> c'
 i(x \<mapsto> s) \<Turnstile> c'
 i(x \<mapsto> s) \<Turnstile> G'
\<lbrakk>atom x \<sharp> G';  i \<Turnstile> G' \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> G'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> G'
 i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> (x', b', c') #\<^sub>\<Gamma> G'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_weakening:
  assumes "\<Theta> ; B ; \<Gamma> \<Turnstile> c" and "toSet \<Gamma> \<subseteq> toSet \<Gamma>'" and "wfG \<Theta> B  \<Gamma>'"
  shows  "\<Theta> ; B ; \<Gamma>' \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; B ; \<Gamma>'  \<Turnstile> c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Theta> ; B ; \<Gamma>'  \<Turnstile> c
[PROOF STEP]
have "wfC \<Theta> B  \<Gamma> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
[PROOF STEP]
using assms valid.simps
[PROOF STATE]
proof (prove)
using this:
\<Theta> ; B ; \<Gamma>  \<Turnstile> c
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'
(?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>\<^sub>w\<^sub>f c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c

goal (1 subgoal):
 1. \<Theta> ; B ; \<Gamma>'  \<Turnstile> c
[PROOF STEP]
hence sp: "supp c \<subseteq> atom `(fst `toSet \<Gamma>) \<union> supp B"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c

goal (1 subgoal):
 1. supp c \<subseteq> atom ` fst ` toSet \<Gamma> \<union> supp B
[PROOF STEP]
using wfX_wfY wfG_elims
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<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>
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f b_of ?\<tau>
 ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> True
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ce : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?td  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f ?ftq  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil ;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> ; \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B> ; (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; ?c \<noteq> (TRUE); ?c \<noteq> (FALSE)\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?c = (TRUE) \<or> ?c = (FALSE);  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma> ; \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, FALSE) #\<^sub>\<Gamma> ?\<Gamma> ; \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. supp c \<subseteq> atom ` fst ` toSet \<Gamma> \<union> supp B
[PROOF STEP]
using atom_dom.simps dom.simps wf_supp(2)
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<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>
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f b_of ?\<tau>
 ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> True
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ce : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?td  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f ?ftq  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil ;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> ; \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B> ; (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; ?c \<noteq> (TRUE); ?c \<noteq> (FALSE)\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?c = (TRUE) \<or> ?c = (FALSE);  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma> ; \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, FALSE) #\<^sub>\<Gamma> ?\<Gamma> ; \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
atom_dom ?\<Gamma> = atom ` ??.Syntax.dom ?\<Gamma>
??.Syntax.dom ?\<Gamma> = fst ` toSet ?\<Gamma>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow> supp ?c \<subseteq> atom_dom ?\<Gamma> \<union> supp ?\<B>

goal (1 subgoal):
 1. supp c \<subseteq> atom ` fst ` toSet \<Gamma> \<union> supp B
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
supp c \<subseteq> atom ` fst ` toSet \<Gamma> \<union> supp B

goal (1 subgoal):
 1. \<Theta> ; B ; \<Gamma>'  \<Turnstile> c
[PROOF STEP]
have wfg: "wfG \<Theta> B  \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
[PROOF STEP]
using assms valid.simps wfC_wf
[PROOF STATE]
proof (prove)
using this:
\<Theta> ; B ; \<Gamma>  \<Turnstile> c
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'
(?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> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>

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

goal (1 subgoal):
 1. \<Theta> ; B ; \<Gamma>'  \<Turnstile> c
[PROOF STEP]
have a1: "(\<forall>i. wfI \<Theta> \<Gamma>' i \<and> i \<Turnstile> \<Gamma>' \<longrightarrow> i \<Turnstile> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'  \<longrightarrow>  i \<Turnstile> c
[PROOF STEP]
proof(rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'  \<Longrightarrow>  i \<Turnstile> c
[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> c
[PROOF STEP]
assume as: "wfI \<Theta> \<Gamma>' i \<and> i \<Turnstile> \<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> c
[PROOF STEP]
hence as1: "fst ` toSet \<Gamma> \<subseteq> dom i"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'

goal (1 subgoal):
 1. fst ` toSet \<Gamma> \<subseteq> dom i
[PROOF STEP]
using assms wfI_domi
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'
\<Theta> ; B ; \<Gamma>  \<Turnstile> c
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i \<Longrightarrow> fst ` toSet ?\<Gamma> \<subseteq> dom ?i

goal (1 subgoal):
 1. fst ` toSet \<Gamma> \<subseteq> dom i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst ` toSet \<Gamma> \<subseteq> dom i

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'  \<Longrightarrow>  i \<Turnstile> c
[PROOF STEP]
obtain i' where idash: "i' =  restrict_map i (fst `toSet \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i'. i' = i |` (fst ` toSet \<Gamma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i' = i |` (fst ` toSet \<Gamma>)

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'  \<Longrightarrow>  i \<Turnstile> c
[PROOF STEP]
hence as2: "dom i' = (fst `toSet \<Gamma>)"
[PROOF STATE]
proof (prove)
using this:
i' = i |` (fst ` toSet \<Gamma>)

goal (1 subgoal):
 1. dom i' = fst ` toSet \<Gamma>
[PROOF STEP]
using dom_restrict as1
[PROOF STATE]
proof (prove)
using this:
i' = i |` (fst ` toSet \<Gamma>)
dom (?m |` ?A) = dom ?m \<inter> ?A
fst ` toSet \<Gamma> \<subseteq> dom i

goal (1 subgoal):
 1. dom i' = fst ` toSet \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom i' = fst ` toSet \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'  \<Longrightarrow>  i \<Turnstile> c
[PROOF STEP]
have id2: "\<Theta> ; \<Gamma> \<turnstile> i' \<and> i' \<Turnstile> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>
[PROOF STEP]
have "wfI \<Theta>  \<Gamma> i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
[PROOF STEP]
using as2 wfI_restrict_weakening[of \<Theta> \<Gamma>' i i' \<Gamma>] as  assms
[PROOF STATE]
proof (prove)
using this:
dom i' = fst ` toSet \<Gamma>
\<lbrakk> \<Theta> ; \<Gamma>' \<turnstile> i; i' = i |` (fst ` toSet \<Gamma>); toSet \<Gamma> \<subseteq> toSet \<Gamma>'\<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'
\<Theta> ; B ; \<Gamma>  \<Turnstile> c
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
[PROOF STEP]
using idash
[PROOF STATE]
proof (prove)
using this:
dom i' = fst ` toSet \<Gamma>
\<lbrakk> \<Theta> ; \<Gamma>' \<turnstile> i; i' = i |` (fst ` toSet \<Gamma>); toSet \<Gamma> \<subseteq> toSet \<Gamma>'\<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'
\<Theta> ; B ; \<Gamma>  \<Turnstile> c
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'
i' = i |` (fst ` toSet \<Gamma>)

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>
[PROOF STEP]
have "i' \<Turnstile> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<Turnstile> \<Gamma>
[PROOF STEP]
using is_satis_g_restrict[OF assms(2)] wfg as idash
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?i' \<Turnstile> \<Gamma>' ; ?i = ?i' |` (fst ` toSet \<Gamma>);  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  ?i \<Turnstile> \<Gamma>
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'
i' = i |` (fst ` toSet \<Gamma>)

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

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<Gamma> \<turnstile> i'
 i' \<Turnstile> \<Gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i'
 i' \<Turnstile> \<Gamma>

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>
[PROOF STEP]
using idash
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i'
 i' \<Turnstile> \<Gamma>
i' = i |` (fst ` toSet \<Gamma>)

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[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> c
[PROOF STEP]
hence "i' \<Turnstile> c"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
using assms valid.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i' \<and>  i' \<Turnstile> \<Gamma>
\<Theta> ; B ; \<Gamma>  \<Turnstile> c
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'
(?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> c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i' \<Turnstile> c

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'  \<Longrightarrow>  i \<Turnstile> c
[PROOF STEP]
thus  "i \<Turnstile> c"
[PROOF STATE]
proof (prove)
using this:
 i' \<Turnstile> c

goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
using assms valid.simps is_satis_i_weakening  idash sp
[PROOF STATE]
proof (prove)
using this:
 i' \<Turnstile> c
\<Theta> ; B ; \<Gamma>  \<Turnstile> c
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'
(?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 ))
\<lbrakk>?i = ?i' |` ?d; supp ?c \<subseteq> atom ` ?d \<union> supp ?B;  ?i \<Turnstile> ?c \<rbrakk> \<Longrightarrow>  ?i' \<Turnstile> ?c
i' = i |` (fst ` toSet \<Gamma>)
supp c \<subseteq> atom ` fst ` toSet \<Gamma> \<union> supp B

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'  \<longrightarrow>  i \<Turnstile> c

goal (1 subgoal):
 1. \<Theta> ; B ; \<Gamma>'  \<Turnstile> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'  \<longrightarrow>  i \<Turnstile> c

goal (1 subgoal):
 1. \<Theta> ; B ; \<Gamma>'  \<Turnstile> c
[PROOF STEP]
have "wfC \<Theta> B \<Gamma>' c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B ; \<Gamma>'   \<turnstile>\<^sub>w\<^sub>f c
[PROOF STEP]
using wf_weakening assms valid.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' ; toSet ?\<Gamma> \<subseteq> toSet ?\<Gamma>'\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>' \<turnstile>\<^sub>w\<^sub>f ?v : ?b
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' ; toSet ?\<Gamma> \<subseteq> toSet ?\<Gamma>'\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>'   \<turnstile>\<^sub>w\<^sub>f ?c
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> True
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau> ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' ; toSet ?\<Gamma> \<subseteq> toSet ?\<Gamma>'\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>'   \<turnstile>\<^sub>w\<^sub>f ?\<tau>
 ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts  \<Longrightarrow> True
   \<turnstile>\<^sub>w\<^sub>f ?P  \<Longrightarrow> True
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; ?\<B> |\<subseteq>| ?\<B>'\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ce : ?b ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' ; toSet ?\<Gamma> \<subseteq> toSet ?\<Gamma>'\<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma>' \<turnstile>\<^sub>w\<^sub>f ?ce : ?b
 ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?td  \<Longrightarrow> True
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' ; toSet ?\<Gamma> \<subseteq> toSet ?\<Gamma>'\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma>' ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' ; toSet ?\<Gamma> \<subseteq> toSet ?\<Gamma>'\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma>' ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' ; toSet ?\<Gamma> \<subseteq> toSet ?\<Gamma>'\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma>' ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' ; toSet ?\<Gamma> \<subseteq> toSet ?\<Gamma>'\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma>' ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b
 ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<Longrightarrow> True
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' ; toSet ?\<Gamma> \<subseteq> toSet ?\<Gamma>'\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>' \<turnstile>\<^sub>w\<^sub>f ?\<Delta>
 ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f ?ftq  \<Longrightarrow> True
 ?\<Theta> ; ?\<Phi> ; ?\<B> \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow> True
\<Theta> ; B ; \<Gamma>  \<Turnstile> c
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'
(?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>\<^sub>w\<^sub>f c
[PROOF STEP]
by (meson  wfg)
[PROOF STATE]
proof (state)
this:
 \<Theta> ; B ; \<Gamma>'   \<turnstile>\<^sub>w\<^sub>f c

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

goal (1 subgoal):
 1. \<Theta> ; B ; \<Gamma>'  \<Turnstile> c
[PROOF STEP]
using assms valid.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
\<forall>i.  \<Theta> ; \<Gamma>' \<turnstile> i \<and>  i \<Turnstile> \<Gamma>'  \<longrightarrow>  i \<Turnstile> c
 \<Theta> ; B ; \<Gamma>'   \<turnstile>\<^sub>w\<^sub>f c
\<Theta> ; B ; \<Gamma>  \<Turnstile> c
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'
(?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> c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Theta> ; B ; \<Gamma>'  \<Turnstile> c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_g_suffix:
  fixes G::\<Gamma>
  assumes "i \<Turnstile> (G'@G)"
  shows "i \<Turnstile> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> G' @ G

goal (1 subgoal):
 1.  i \<Turnstile> G
[PROOF STEP]
proof(induct G' rule:\<Gamma>.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  i \<Turnstile> GNil @ G  \<Longrightarrow>  i \<Turnstile> G
 2. \<And>x1 x2. \<lbrakk> i \<Turnstile> x2 @ G  \<Longrightarrow>  i \<Turnstile> G ;  i \<Turnstile> (x1 #\<^sub>\<Gamma> x2) @ G \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
[PROOF STEP]
case GNil
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> GNil @ G

goal (2 subgoals):
 1.  i \<Turnstile> GNil @ G  \<Longrightarrow>  i \<Turnstile> G
 2. \<And>x1 x2. \<lbrakk> i \<Turnstile> x2 @ G  \<Longrightarrow>  i \<Turnstile> G ;  i \<Turnstile> (x1 #\<^sub>\<Gamma> x2) @ G \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<Turnstile> GNil @ G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> GNil @ G

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

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk> i \<Turnstile> x2 @ G  \<Longrightarrow>  i \<Turnstile> G ;  i \<Turnstile> (x1 #\<^sub>\<Gamma> x2) @ G \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk> i \<Turnstile> x2 @ G  \<Longrightarrow>  i \<Turnstile> G ;  i \<Turnstile> (x1 #\<^sub>\<Gamma> x2) @ G \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
[PROOF STEP]
case (GCons xbc x2)
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> x2 @ G  \<Longrightarrow>  i \<Turnstile> G
 i \<Turnstile> (xbc #\<^sub>\<Gamma> x2) @ G

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk> i \<Turnstile> x2 @ G  \<Longrightarrow>  i \<Turnstile> G ;  i \<Turnstile> (x1 #\<^sub>\<Gamma> x2) @ G \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
[PROOF STEP]
obtain x and b and c::c where xbc: "xbc=(x,b,c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x b c. xbc = (x, b, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod_cases3
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c. ?y = (a, b, c) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x b c. xbc = (x, b, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xbc = (x, b, c)

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk> i \<Turnstile> x2 @ G  \<Longrightarrow>  i \<Turnstile> G ;  i \<Turnstile> (x1 #\<^sub>\<Gamma> x2) @ G \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
[PROOF STEP]
hence " i \<Turnstile> (xbc #\<^sub>\<Gamma> (x2 @ G))"
[PROOF STATE]
proof (prove)
using this:
xbc = (x, b, c)

goal (1 subgoal):
 1.  i \<Turnstile> xbc #\<^sub>\<Gamma> x2 @ G
[PROOF STEP]
using append_g.simps GCons
[PROOF STATE]
proof (prove)
using this:
xbc = (x, b, c)
GNil @ ?g = ?g
(?xbc #\<^sub>\<Gamma> ?g1.0) @ ?g2.0 = ?xbc #\<^sub>\<Gamma> ?g1.0 @ ?g2.0
 i \<Turnstile> x2 @ G  \<Longrightarrow>  i \<Turnstile> G
 i \<Turnstile> (xbc #\<^sub>\<Gamma> x2) @ G

goal (1 subgoal):
 1.  i \<Turnstile> xbc #\<^sub>\<Gamma> x2 @ G
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> xbc #\<^sub>\<Gamma> x2 @ G

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk> i \<Turnstile> x2 @ G  \<Longrightarrow>  i \<Turnstile> G ;  i \<Turnstile> (x1 #\<^sub>\<Gamma> x2) @ G \<rbrakk> \<Longrightarrow>  i \<Turnstile> G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<Turnstile> xbc #\<^sub>\<Gamma> x2 @ G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> xbc #\<^sub>\<Gamma> x2 @ G

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfG_inside_valid2:
  fixes x::x and \<Gamma>::\<Gamma> and c0::c and c0'::c
  assumes "wfG \<Theta> B  (\<Gamma>'@((x,b0,c0')#\<^sub>\<Gamma>\<Gamma>))" and
    "\<Theta> ; B ; \<Gamma>'@(x,b0,c0)#\<^sub>\<Gamma>\<Gamma> \<Turnstile> c0'"
  shows "wfG \<Theta> B  (\<Gamma>'@((x,b0,c0)#\<^sub>\<Gamma>\<Gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b0, c0) #\<^sub>\<Gamma> \<Gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b0, c0) #\<^sub>\<Gamma> \<Gamma>
[PROOF STEP]
have "wfG \<Theta>  B  (\<Gamma>'@(x,b0,c0)#\<^sub>\<Gamma>\<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b0, c0) #\<^sub>\<Gamma> \<Gamma>
[PROOF STEP]
using valid.simps wfC_wf 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>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b0, c0') #\<^sub>\<Gamma> \<Gamma>
\<Theta> ; B ; \<Gamma>' @ (x, b0, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c0'

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

goal (1 subgoal):
 1.  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b0, c0) #\<^sub>\<Gamma> \<Gamma>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b0, c0) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1.  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b0, c0) #\<^sub>\<Gamma> \<Gamma>
[PROOF STEP]
using wfG_replace_inside_full assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b0, c0) #\<^sub>\<Gamma> \<Gamma>
\<lbrakk> ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' @ (?x, ?b, ?c') #\<^sub>\<Gamma> ?\<Gamma> ;  ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> \<rbrakk> \<Longrightarrow>  ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b0, c0') #\<^sub>\<Gamma> \<Gamma>
\<Theta> ; B ; \<Gamma>' @ (x, b0, c0) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c0'

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

goal:
No subgoals!
[PROOF STEP]
qed