[STATEMENT]
lemma is_satis_bs_boxed:
  fixes c::c
  assumes  "boxed_i \<Theta> \<Gamma> b bv i i'" and "wfC \<Theta> B \<Gamma> c" and "wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "\<Theta> ; \<Gamma> \<turnstile> i'"
    and  "(i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b)"
  shows "(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 "eval_c i (c[bv::=b]\<^sub>c\<^sub>b) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ True
[PROOF STEP]
using is_satis.simps assms
[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 )
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; \<Gamma> \<turnstile> i'
 i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b

goal (1 subgoal):
 1.  i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ True

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ True

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
obtain s where "i' \<lbrakk> c \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s.  i' \<lbrakk> c \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_c_exist assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c \<rbrakk> \<Longrightarrow> \<exists>s.  ?i \<lbrakk> ?c \<rbrakk> ~ s
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; \<Gamma> \<turnstile> i'
 i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b

goal (1 subgoal):
 1. (\<And>s.  i' \<lbrakk> c \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i' \<lbrakk> c \<rbrakk> ~ s

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ True
 i' \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ True
 i' \<lbrakk> c \<rbrakk> ~ s

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
using eval_c_eq_bs_boxed assms is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ True
 i' \<lbrakk> c \<rbrakk> ~ s
\<lbrakk> ?i \<lbrakk> ?c[?bv::=?b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  ?i' \<lbrakk> ?c \<rbrakk> ~ ?s' ;  ?\<Theta> ; ?B ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i';  ?\<Theta> ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;  ?\<Theta>  ; ?\<Gamma> ; ?b , ?bv \<turnstile> ?i \<approx> ?i'\<rbrakk> \<Longrightarrow> ?s = ?s'
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; \<Gamma> \<turnstile> i'
 i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
 ?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' \<Turnstile> c
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i' \<Turnstile> c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_bs_boxed_rev:
  fixes c::c
  assumes  "boxed_i \<Theta> \<Gamma> b bv i i'" and "wfC \<Theta> B \<Gamma> c" and "wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "\<Theta> ; \<Gamma> \<turnstile> i'" and  "wfC \<Theta> {||} \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b (c[bv::=b]\<^sub>c\<^sub>b)"
    and  "(i' \<Turnstile> c)"
  shows "(i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
have "eval_c i' c True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<lbrakk> c \<rbrakk> ~ True
[PROOF STEP]
using is_satis.simps assms
[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 )
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
 i' \<Turnstile> c

goal (1 subgoal):
 1.  i' \<lbrakk> c \<rbrakk> ~ True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i' \<lbrakk> c \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i' \<lbrakk> c \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
obtain s where "i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s.  i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_c_exist assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c \<rbrakk> \<Longrightarrow> \<exists>s.  ?i \<lbrakk> ?c \<rbrakk> ~ s
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
 i' \<Turnstile> c

goal (1 subgoal):
 1. (\<And>s.  i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s

goal (1 subgoal):
 1.  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i' \<lbrakk> c \<rbrakk> ~ True
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c \<rbrakk> ~ True
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s

goal (1 subgoal):
 1.  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
using eval_c_eq_bs_boxed assms is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c \<rbrakk> ~ True
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
\<lbrakk> ?i \<lbrakk> ?c[?bv::=?b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  ?i' \<lbrakk> ?c \<rbrakk> ~ ?s' ;  ?\<Theta> ; ?B ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i';  ?\<Theta> ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;  ?\<Theta>  ; ?\<Gamma> ; ?b , ?bv \<turnstile> ?i \<approx> ?i'\<rbrakk> \<Longrightarrow> ?s = ?s'
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
 i' \<Turnstile> c
 ?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 \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bs_boxed_wfi_aux:
  fixes b::b and bv::bv and \<Theta>::\<Theta> and B::\<B>
  assumes   "boxed_i \<Theta> \<Gamma> b bv i i'" and "wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "\<turnstile>\<^sub>w\<^sub>f \<Theta>" and "wfG \<Theta> B  \<Gamma>"
  shows "\<Theta> ; \<Gamma> \<turnstile> i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
[PROOF STEP]
proof(induct rule: boxed_i.inducts)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Theta> b bv i. \<lbrakk> \<Theta> ; GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f GNil \<rbrakk> \<Longrightarrow>  \<Theta> ; GNil \<turnstile> i
 2. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
case (boxed_i_GNilI T i)
[PROOF STATE]
proof (state)
this:
 T ; GNil[bv_::=i]\<^sub>\<Gamma>\<^sub>b \<turnstile> i_
   \<turnstile>\<^sub>w\<^sub>f T
 T ; B  \<turnstile>\<^sub>w\<^sub>f GNil

goal (2 subgoals):
 1. \<And>\<Theta> b bv i. \<lbrakk> \<Theta> ; GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f GNil \<rbrakk> \<Longrightarrow>  \<Theta> ; GNil \<turnstile> i
 2. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 T ; GNil[bv_::=i]\<^sub>\<Gamma>\<^sub>b \<turnstile> i_
   \<turnstile>\<^sub>w\<^sub>f T
 T ; B  \<turnstile>\<^sub>w\<^sub>f GNil
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 T ; GNil[bv_::=i]\<^sub>\<Gamma>\<^sub>b \<turnstile> i_
   \<turnstile>\<^sub>w\<^sub>f T
 T ; B  \<turnstile>\<^sub>w\<^sub>f GNil

goal (1 subgoal):
 1.  T ; GNil \<turnstile> i_
[PROOF STEP]
using wfI_def
[PROOF STATE]
proof (prove)
using this:
 T ; GNil[bv_::=i]\<^sub>\<Gamma>\<^sub>b \<turnstile> i_
   \<turnstile>\<^sub>w\<^sub>f T
 T ; B  \<turnstile>\<^sub>w\<^sub>f GNil
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)

goal (1 subgoal):
 1.  T ; GNil \<turnstile> i_
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 T ; GNil \<turnstile> i_

goal (1 subgoal):
 1. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
case (boxed_i_GConsI s i x1 T b1 bv b s' G i' c1)
[PROOF STATE]
proof (state)
this:
Some s = i x1
 T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s'
 T  ; G ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i'
 T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
 T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Some s = i x1
 T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s'
 T  ; G ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i'
 T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
 T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
fix x2 b2 c2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
assume as : "(x2,b2,c2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)"
[PROOF STATE]
proof (state)
this:
(x2, b2, c2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)

goal (1 subgoal):
 1. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x2, b2, c2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)
[PROOF STEP]
consider (hd) "(x2,b2,c2) = (x1, b1, c1)" | (tail) "(x2,b2,c2) \<in> toSet G"
[PROOF STATE]
proof (prove)
using this:
(x2, b2, c2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)

goal (1 subgoal):
 1. \<lbrakk>(x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> thesis; (x2, b2, c2) \<in> toSet G \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using toSet.simps
[PROOF STATE]
proof (prove)
using this:
(x2, b2, c2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G

goal (1 subgoal):
 1. \<lbrakk>(x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> thesis; (x2, b2, c2) \<in> toSet G \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>(x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> ?thesis; (x2, b2, c2) \<in> toSet G \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
hence "\<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and> wfRCV T s b2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> ?thesis; (x2, b2, c2) \<in> toSet G \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
 2. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
case hd
[PROOF STATE]
proof (state)
this:
(x2, b2, c2) = (x1, b1, c1)

goal (2 subgoals):
 1. (x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
 2. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
hence "b1=b2"
[PROOF STATE]
proof (prove)
using this:
(x2, b2, c2) = (x1, b1, c1)

goal (1 subgoal):
 1. b1 = b2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b1 = b2

goal (2 subgoals):
 1. (x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
 2. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b1 = b2

goal (2 subgoals):
 1. (x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
 2. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
have "(x2,b2[bv::=b]\<^sub>b\<^sub>b,c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b
[PROOF STEP]
using hd subst_gb.simps
[PROOF STATE]
proof (prove)
using this:
(x2, b2, c2) = (x1, b1, c1)
GNil[?uu::=?uv]\<^sub>\<Gamma>\<^sub>b = GNil
((?y, ?b', ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?bv::=?b]\<^sub>\<Gamma>\<^sub>b = (?y, ?b'[?bv::=?b]\<^sub>b\<^sub>b, ?c[?bv::=?b]\<^sub>c\<^sub>b) #\<^sub>\<Gamma> ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1. (x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (2 subgoals):
 1. (x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
 2. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (2 subgoals):
 1. (x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
 2. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
hence "wfRCV T s b2[bv::=b]\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1.  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
using wfI_def boxed_i_GConsI hd
[PROOF STATE]
proof (prove)
using this:
(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
Some s = i x1
 T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s'
 T  ; G ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i'
 T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
 T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G
(x2, b2, c2) = (x1, b1, c1)

goal (1 subgoal):
 1.  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b); Some s = i x1;  T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s' ;  T  ; G ; b , bv \<turnstile> i \<approx> i'; \<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i';  T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G ; (x2, b2, c2) = (x1, b1, c1)\<rbrakk> \<Longrightarrow>  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
obtain ss :: "b \<Rightarrow> x \<Rightarrow> (x \<Rightarrow> rcl_val option) \<Rightarrow> type_def list \<Rightarrow> rcl_val" where
          "\<forall>x1a x2a x3 x4. (\<exists>v5. Some v5 = x3 x2a \<and> wfRCV x4 v5 x1a) = (Some (ss x1a x2a x3 x4) = x3 x2a \<and> wfRCV x4 (ss x1a x2a x3 x4) x1a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ss. \<forall>x1a x2a x3 x4. (\<exists>v5. Some v5 = x3 x2a \<and>  x4  \<turnstile> v5 : x1a) = (Some (ss x1a x2a x3 x4) = x3 x2a \<and>  x4  \<turnstile> ss x1a x2a x3 x4 : x1a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by moura
[PROOF STATE]
proof (state)
this:
\<forall>x1a x2a x3 x4. (\<exists>v5. Some v5 = x3 x2a \<and>  x4  \<turnstile> v5 : x1a) = (Some (ss x1a x2a x3 x4) = x3 x2a \<and>  x4  \<turnstile> ss x1a x2a x3 x4 : x1a)

goal (1 subgoal):
 1. \<lbrakk>(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b); Some s = i x1;  T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s' ;  T  ; G ; b , bv \<turnstile> i \<approx> i'; \<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i';  T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G ; (x2, b2, c2) = (x1, b1, c1)\<rbrakk> \<Longrightarrow>  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
(* 0.0 ms *)
[PROOF STATE]
proof (state)
this:
\<forall>x1a x2a x3 x4. (\<exists>v5. Some v5 = x3 x2a \<and>  x4  \<turnstile> v5 : x1a) = (Some (ss x1a x2a x3 x4) = x3 x2a \<and>  x4  \<turnstile> ss x1a x2a x3 x4 : x1a)

goal (1 subgoal):
 1. \<lbrakk>(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b); Some s = i x1;  T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s' ;  T  ; G ; b , bv \<turnstile> i \<approx> i'; \<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i';  T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G ; (x2, b2, c2) = (x1, b1, c1)\<rbrakk> \<Longrightarrow>  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x1a x2a x3 x4. (\<exists>v5. Some v5 = x3 x2a \<and>  x4  \<turnstile> v5 : x1a) = (Some (ss x1a x2a x3 x4) = x3 x2a \<and>  x4  \<turnstile> ss x1a x2a x3 x4 : x1a)
[PROOF STEP]
have f1: "Some (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) = i x1 \<and> wfRCV T (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) b2[bv::=b]\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
\<forall>x1a x2a x3 x4. (\<exists>v5. Some v5 = x3 x2a \<and>  x4  \<turnstile> v5 : x1a) = (Some (ss x1a x2a x3 x4) = x3 x2a \<and>  x4  \<turnstile> ss x1a x2a x3 x4 : x1a)

goal (1 subgoal):
 1. Some (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) = i x1 \<and>  T  \<turnstile> ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
using boxed_i_GConsI.prems(1) hd wfI_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x1a x2a x3 x4. (\<exists>v5. Some v5 = x3 x2a \<and>  x4  \<turnstile> v5 : x1a) = (Some (ss x1a x2a x3 x4) = x3 x2a \<and>  x4  \<turnstile> ss x1a x2a x3 x4 : x1a)
 T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
(x2, b2, c2) = (x1, b1, c1)
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)

goal (1 subgoal):
 1. Some (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) = i x1 \<and>  T  \<turnstile> ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) = i x1 \<and>  T  \<turnstile> ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T : b2[bv::=b]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. \<lbrakk>(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b); Some s = i x1;  T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s' ;  T  ; G ; b , bv \<turnstile> i \<approx> i'; \<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i';  T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G ; (x2, b2, c2) = (x1, b1, c1)\<rbrakk> \<Longrightarrow>  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
(* 31 ms *)
[PROOF STATE]
proof (state)
this:
Some (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) = i x1 \<and>  T  \<turnstile> ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T : b2[bv::=b]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. \<lbrakk>(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b); Some s = i x1;  T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s' ;  T  ; G ; b , bv \<turnstile> i \<approx> i'; \<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i';  T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G ; (x2, b2, c2) = (x1, b1, c1)\<rbrakk> \<Longrightarrow>  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) = i x1 \<and>  T  \<turnstile> ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
have "ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T = s"
[PROOF STATE]
proof (prove)
using this:
Some (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) = i x1 \<and>  T  \<turnstile> ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T : b2[bv::=b]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T = s
[PROOF STEP]
by (metis (no_types) boxed_i_GConsI.hyps(1) option.inject)
[PROOF STATE]
proof (state)
this:
ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T = s

goal (1 subgoal):
 1. \<lbrakk>(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b); Some s = i x1;  T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s' ;  T  ; G ; b , bv \<turnstile> i \<approx> i'; \<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i';  T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G ; (x2, b2, c2) = (x1, b1, c1)\<rbrakk> \<Longrightarrow>  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
(* 0.0 ms *)
[PROOF STATE]
proof (state)
this:
ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T = s

goal (1 subgoal):
 1. \<lbrakk>(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b); Some s = i x1;  T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s' ;  T  ; G ; b , bv \<turnstile> i \<approx> i'; \<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i';  T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G ; (x2, b2, c2) = (x1, b1, c1)\<rbrakk> \<Longrightarrow>  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T = s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T = s

goal (1 subgoal):
 1.  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T = s
Some (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) = i x1 \<and>  T  \<turnstile> ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T : b2[bv::=b]\<^sub>b\<^sub>b

goal (1 subgoal):
 1.  T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b

goal:
No subgoals!
[PROOF STEP]
(* 0.0 ms *)
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b

goal (2 subgoals):
 1. (x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
 2. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b1 = b2
(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b
 T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
[PROOF STEP]
have "wfRCV T s' b2"
[PROOF STATE]
proof (prove)
using this:
b1 = b2
(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b
 T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b

goal (1 subgoal):
 1.  T  \<turnstile> s' : b2
[PROOF STEP]
using boxed_i_GConsI boxed_b_wfRCV
[PROOF STATE]
proof (prove)
using this:
b1 = b2
(x2, b2[bv::=b]\<^sub>b\<^sub>b, c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b
 T  \<turnstile> s : b2[bv::=b]\<^sub>b\<^sub>b
Some s = i x1
 T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s'
 T  ; G ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i'
 T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
 T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G
\<lbrakk> ?P  \<turnstile> ?s ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s' ;    \<turnstile>\<^sub>w\<^sub>f ?P \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s : ?b[?bv::=?b']\<^sub>b\<^sub>b \<and>  ?P  \<turnstile> ?s' : ?b

goal (1 subgoal):
 1.  T  \<turnstile> s' : b2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> s' : b2

goal (2 subgoals):
 1. (x2, b2, c2) = (x1, b1, c1) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
 2. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 T  \<turnstile> s' : b2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> s' : b2

goal (1 subgoal):
 1. \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
using hd
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> s' : b2
(x2, b2, c2) = (x1, b1, c1)

goal (1 subgoal):
 1. \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2

goal (1 subgoal):
 1. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
case tail
[PROOF STATE]
proof (state)
this:
(x2, b2, c2) \<in> toSet G

goal (1 subgoal):
 1. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
hence "wfI T G i'"
[PROOF STATE]
proof (prove)
using this:
(x2, b2, c2) \<in> toSet G

goal (1 subgoal):
 1.  T ; G \<turnstile> i'
[PROOF STEP]
using boxed_i_GConsI wfI_suffix wfG_suffix subst_gb.simps
[PROOF STATE]
proof (prove)
using this:
(x2, b2, c2) \<in> toSet G
Some s = i x1
 T  \<turnstile> s ~ b1 [ bv ::= b ] \<setminus> s'
 T  ; G ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> T ; G[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f T ;  T ; B  \<turnstile>\<^sub>w\<^sub>f G \<rbrakk> \<Longrightarrow>  T ; G \<turnstile> i'
 T ; ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
   \<turnstile>\<^sub>w\<^sub>f T
 T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G
\<lbrakk> ?P ; ?G' @ ?G \<turnstile> ?i;  ?P ; ?B  \<turnstile>\<^sub>w\<^sub>f ?G \<rbrakk> \<Longrightarrow>  ?P ; ?G \<turnstile> ?i
 ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' @ ?\<Gamma>  \<Longrightarrow>  ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>
GNil[?uu::=?uv]\<^sub>\<Gamma>\<^sub>b = GNil
((?y, ?b', ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?bv::=?b]\<^sub>\<Gamma>\<^sub>b = (?y, ?b'[?bv::=?b]\<^sub>b\<^sub>b, ?c[?bv::=?b]\<^sub>c\<^sub>b) #\<^sub>\<Gamma> ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1.  T ; G \<turnstile> i'
[PROOF STEP]
by (metis (no_types, lifting) Un_iff toSet.simps(2) wfG_cons2 wfI_def)
[PROOF STATE]
proof (state)
this:
 T ; G \<turnstile> i'

goal (1 subgoal):
 1. (x2, b2, c2) \<in> toSet G \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 T ; G \<turnstile> i'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 T ; G \<turnstile> i'

goal (1 subgoal):
 1. \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
using wfI_def[of T G i'] tail
[PROOF STATE]
proof (prove)
using this:
 T ; G \<turnstile> i'
 T ; G \<turnstile> i' = (\<forall>(x, b, c)\<in>toSet G. \<exists>s. Some s = i' x \<and>  T  \<turnstile> s : b)
(x2, b2, c2) \<in> toSet G

goal (1 subgoal):
 1. \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
using boxed_i_GConsI.prems(3) split_G wfG_cons_fresh2
[PROOF STATE]
proof (prove)
using this:
 T ; G \<turnstile> i'
 T ; G \<turnstile> i' = (\<forall>(x, b, c)\<in>toSet G. \<exists>s. Some s = i' x \<and>  T  \<turnstile> s : b)
(x2, b2, c2) \<in> toSet G
 T ; B  \<turnstile>\<^sub>w\<^sub>f (x1, b1, c1) #\<^sub>\<Gamma> G
?x \<in> toSet ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x #\<^sub>\<Gamma> zs
 ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x', ?b', ?c') #\<^sub>\<Gamma> ?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>  \<Longrightarrow> ?x' \<noteq> ?x

goal (1 subgoal):
 1. \<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and>  T  \<turnstile> s : b2

goal (1 subgoal):
 1. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x2.2, ?b2.2, ?c2.2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) ?x2.2 \<and>  T  \<turnstile> s : ?b2.2

goal (1 subgoal):
 1. \<And>s i x \<Theta> b bv b' s' \<Gamma> i' c. \<lbrakk>Some s = i x;  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk> \<Theta> ; \<Gamma>[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; \<Gamma> \<turnstile> i';  \<Theta> ; ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[bv::=b']\<^sub>\<Gamma>\<^sub>b \<turnstile> i;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<rbrakk> \<Longrightarrow>  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i'(x \<mapsto> s')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(?x2.2, ?b2.2, ?c2.2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) ?x2.2 \<and>  T  \<turnstile> s : ?b2.2

goal (1 subgoal):
 1.  T ; (x1, b1, c1) #\<^sub>\<Gamma> G \<turnstile> i'(x1 \<mapsto> s')
[PROOF STEP]
using wfI_def
[PROOF STATE]
proof (prove)
using this:
(?x2.2, ?b2.2, ?c2.2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G) \<Longrightarrow> \<exists>s. Some s = (i'(x1 \<mapsto> s')) ?x2.2 \<and>  T  \<turnstile> s : ?b2.2
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)

goal (1 subgoal):
 1.  T ; (x1, b1, c1) #\<^sub>\<Gamma> G \<turnstile> i'(x1 \<mapsto> s')
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
 T ; (x1, b1, c1) #\<^sub>\<Gamma> G \<turnstile> i'(x1 \<mapsto> s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_g_bs_boxed_aux:
  fixes G::\<Gamma>
  assumes  "boxed_i \<Theta> G1 b bv i i'" and "wfI \<Theta> G1[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "wfI \<Theta> G1 i'"  and "G1 = (G2@G)" and  "wfG \<Theta> B G1"
    and "(i \<Turnstile> G[bv::=b]\<^sub>\<Gamma>\<^sub>b) "
  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:
 \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; G1 \<turnstile> i'
G1 = G2 @ G
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1
 i \<Turnstile> G[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1.  i' \<Turnstile> G
[PROOF STEP]
proof(induct G arbitrary: G2 rule: \<Gamma>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>G2. \<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = G2 @ GNil;  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> GNil
 2. \<And>x ba c \<Gamma>' G2. \<lbrakk>\<And>G2. \<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = G2 @ \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = G2 @ (x, ba, c) #\<^sub>\<Gamma> \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, ba, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
case GNil
[PROOF STATE]
proof (state)
this:
 \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; G1 \<turnstile> i'
G1 = G2 @ GNil
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1
 i \<Turnstile> GNil[bv::=b]\<^sub>\<Gamma>\<^sub>b

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

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 ba c \<Gamma>' G2. \<lbrakk>\<And>G2. \<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = G2 @ \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = G2 @ (x, ba, c) #\<^sub>\<Gamma> \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, ba, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x ba c \<Gamma>' G2. \<lbrakk>\<And>G2. \<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = G2 @ \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = G2 @ (x, ba, c) #\<^sub>\<Gamma> \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, ba, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
case (GCons x' b' c' \<Gamma>' G2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = ?G2.0 @ \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>'
 \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; G1 \<turnstile> i'
G1 = G2 @ (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1. \<And>x ba c \<Gamma>' G2. \<lbrakk>\<And>G2. \<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = G2 @ \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>' ;  \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = G2 @ (x, ba, c) #\<^sub>\<Gamma> \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> ((x, ba, c) #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> (x, ba, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
proof(subst is_satis_g.simps,rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  i' \<Turnstile> c'
 2.  i' \<Turnstile> \<Gamma>'
[PROOF STEP]
have *:"wfC \<Theta> B G1 c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B ; G1   \<turnstile>\<^sub>w\<^sub>f c'
[PROOF STEP]
using GCons wfG_wfC_inside
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = ?G2.0 @ \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>'
 \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; G1 \<turnstile> i'
G1 = G2 @ (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b
\<lbrakk>(?x, ?b, ?c) \<in> toSet ?G;  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?G \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c

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

goal (2 subgoals):
 1.  i' \<Turnstile> c'
 2.  i' \<Turnstile> \<Gamma>'
[PROOF STEP]
show "i' \<Turnstile> c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<Turnstile> c'
[PROOF STEP]
using is_satis_bs_boxed[OF assms(1) * ] GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i';  i \<Turnstile> c'[bv::=b]\<^sub>c\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> c'
\<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = ?G2.0 @ \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>'
 \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; G1 \<turnstile> i'
G1 = G2 @ (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b

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> \<Gamma>'
[PROOF STEP]
obtain G3 where "G1 = G3 @ \<Gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>G3. G1 = G3 @ \<Gamma>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GCons append_g.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = ?G2.0 @ \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>'
 \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; G1 \<turnstile> i'
G1 = G2 @ (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b
GNil @ ?g = ?g
(?xbc #\<^sub>\<Gamma> ?g1.0) @ ?g2.0 = ?xbc #\<^sub>\<Gamma> ?g1.0 @ ?g2.0

goal (1 subgoal):
 1. (\<And>G3. G1 = G3 @ \<Gamma>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_g_assoc)
[PROOF STATE]
proof (state)
this:
G1 = G3 @ \<Gamma>'

goal (1 subgoal):
 1.  i' \<Turnstile> \<Gamma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G1 = G3 @ \<Gamma>'
[PROOF STEP]
show "i' \<Turnstile> \<Gamma>'"
[PROOF STATE]
proof (prove)
using this:
G1 = G3 @ \<Gamma>'

goal (1 subgoal):
 1.  i' \<Turnstile> \<Gamma>'
[PROOF STEP]
using GCons append_g.simps
[PROOF STATE]
proof (prove)
using this:
G1 = G3 @ \<Gamma>'
\<lbrakk> \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i';  \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i;  \<Theta> ; G1 \<turnstile> i'; G1 = ?G2.0 @ \<Gamma>';  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1 ;  i \<Turnstile> \<Gamma>'[bv::=b]\<^sub>\<Gamma>\<^sub>b \<rbrakk> \<Longrightarrow>  i' \<Turnstile> \<Gamma>'
 \<Theta>  ; G1 ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; G1[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta> ; G1 \<turnstile> i'
G1 = G2 @ (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f G1
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[bv::=b]\<^sub>\<Gamma>\<^sub>b
GNil @ ?g = ?g
(?xbc #\<^sub>\<Gamma> ?g1.0) @ ?g2.0 = ?xbc #\<^sub>\<Gamma> ?g1.0 @ ?g2.0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i' \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_b_valid:
  fixes s::s and b::b
  assumes "\<Theta> ; {||} \<turnstile>\<^sub>w\<^sub>f b"  and "B = {|bv|}" and "\<Theta> ; {|bv|} ;\<Gamma>  \<Turnstile> c"
  shows "\<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
proof(rule validI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
 2. \<forall>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
show **:"\<Theta> ; {||} ;  \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
using assms valid.simps wf_b_subst subst_gb.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f b
B = {|bv|}
\<Theta> ; {|bv|} ; \<Gamma>  \<Turnstile> c
(?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> ?\<Theta> ; ?B' ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b' ; {|?bv|} = ?B';  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?B ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b \<turnstile>\<^sub>w\<^sub>f ?v[?bv::=?b]\<^sub>v\<^sub>b : ?b'[?bv::=?b]\<^sub>b\<^sub>b
\<lbrakk> ?\<Theta> ; ?B' ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ; {|?bv|} = ?B';  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?B ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f ?c[?bv::=?b]\<^sub>c\<^sub>b
\<lbrakk> ?\<Theta> ; ?B'  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; {|?bv|} = ?B';  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b
\<lbrakk> ?\<Theta> ; ?B' ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau> ; {|?bv|} = ?B';  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?B ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f ?\<tau>[?bv::=?b]\<^sub>\<tau>\<^sub>b
 ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts  \<Longrightarrow> True
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> True
\<lbrakk> ?\<Theta> ; ?B'  \<turnstile>\<^sub>w\<^sub>f ?b' ; {|?bv|} = ?B';  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b'[?bv::=?b]\<^sub>b\<^sub>b
\<lbrakk>  ?\<Theta> ; ?B' ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ce : ?b' ; {|?bv|} = ?B';  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?B ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b \<turnstile>\<^sub>w\<^sub>f ?ce[?bv::=?b]\<^sub>c\<^sub>e\<^sub>b : ?b'[?bv::=?b]\<^sub>b\<^sub>b
 ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?td  \<Longrightarrow> True
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?B' ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b' ; {|?bv|} = ?B';  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?B ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b ; ?\<Delta>[?bv::=?b]\<^sub>\<Delta>\<^sub>b \<turnstile>\<^sub>w\<^sub>f ?e[?bv::=?b]\<^sub>e\<^sub>b : ?b'[?bv::=?b]\<^sub>b\<^sub>b
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b  \<Longrightarrow> True
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b  \<Longrightarrow> True
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b  \<Longrightarrow> True
 ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<Longrightarrow> True
\<lbrakk> ?\<Theta> ; ?B' ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ; {|?bv|} = ?B';  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?B ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b \<turnstile>\<^sub>w\<^sub>f ?\<Delta>[?bv::=?b]\<^sub>\<Delta>\<^sub>b
 ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f ?ftq  \<Longrightarrow> True
 ?\<Theta> ; ?\<Phi> ; ?\<B> \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow> True
GNil[?uu::=?uv]\<^sub>\<Gamma>\<^sub>b = GNil
((?y, ?b', ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?bv::=?b]\<^sub>\<Gamma>\<^sub>b = (?y, ?b'[?bv::=?b]\<^sub>b\<^sub>b, ?c[?bv::=?b]\<^sub>c\<^sub>b) #\<^sub>\<Gamma> ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1.  \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b

goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
show "\<forall>i. (wfI \<Theta>  \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i \<and> i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b) \<longrightarrow> i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
proof(rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
assume *:"wfI \<Theta>  \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i \<and> i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
obtain i' where idash: "boxed_i \<Theta> \<Gamma> b bv i i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i'.  \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using boxed_i_ex wfX_wfY assms *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?T ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;    \<turnstile>\<^sub>w\<^sub>f ?T \<rbrakk> \<Longrightarrow> \<exists>i'.  ?T  ; ?\<Gamma> ; ?b , ?bv \<turnstile> ?i \<approx> i'
 ?\<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>
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f b
B = {|bv|}
\<Theta> ; {|bv|} ; \<Gamma>  \<Turnstile> c
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1. (\<And>i'.  \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
have wfc: "\<Theta> ; {|bv|} ; \<Gamma>  \<turnstile>\<^sub>w\<^sub>f c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; {|bv|} ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
[PROOF STEP]
using valid.simps assms
[PROOF STATE]
proof (prove)
using this:
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f b
B = {|bv|}
\<Theta> ; {|bv|} ; \<Gamma>  \<Turnstile> c

goal (1 subgoal):
 1.  \<Theta> ; {|bv|} ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 \<Theta> ; {|bv|} ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
have wfg: "\<Theta> ; {|bv|} \<turnstile>\<^sub>w\<^sub>f \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; {|bv|}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
[PROOF STEP]
using valid.simps wfX_wfY 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 ?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>
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f b
B = {|bv|}
\<Theta> ; {|bv|} ; \<Gamma>  \<Turnstile> c

goal (1 subgoal):
 1.  \<Theta> ; {|bv|}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta> ; {|bv|}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
hence wfi: "wfI \<Theta> \<Gamma> i'"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; {|bv|}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
[PROOF STEP]
using idash * bs_boxed_wfi_aux subst_gb.simps wfX_wfY
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; {|bv|}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b
\<lbrakk> ?\<Theta>  ; ?\<Gamma> ; ?b , ?bv \<turnstile> ?i \<approx> ?i';  ?\<Theta> ; ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b \<turnstile> ?i;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ;  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i'
GNil[?uu::=?uv]\<^sub>\<Gamma>\<^sub>b = GNil
((?y, ?b', ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?bv::=?b]\<^sub>\<Gamma>\<^sub>b = (?y, ?b'[?bv::=?b]\<^sub>b\<^sub>b, ?c[?bv::=?b]\<^sub>c\<^sub>b) #\<^sub>\<Gamma> ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b
 ?\<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>

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

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma> \<turnstile> i'

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
have "i' \<Turnstile>  \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<Turnstile> \<Gamma>
[PROOF STEP]
proof (rule is_satis_g_bs_boxed[OF idash ] wfX_wfY(2)[OF wfc])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 2.  \<Theta> ; \<Gamma> \<turnstile> i'
 3.  \<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 4.  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b
[PROOF STEP]
show "wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
[PROOF STEP]
using subst_gb.simps *
[PROOF STATE]
proof (prove)
using this:
GNil[?uu::=?uv]\<^sub>\<Gamma>\<^sub>b = GNil
((?y, ?b', ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?bv::=?b]\<^sub>\<Gamma>\<^sub>b = (?y, ?b'[?bv::=?b]\<^sub>b\<^sub>b, ?c[?bv::=?b]\<^sub>c\<^sub>b) #\<^sub>\<Gamma> ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i

goal (3 subgoals):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
 2.  \<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 3.  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b
[PROOF STEP]
show "wfI \<Theta> \<Gamma> i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
[PROOF STEP]
using wfi
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i'

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

goal (2 subgoals):
 1.  \<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 2.  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b
[PROOF STEP]
show "\<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
[PROOF STEP]
using wfg assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; {|bv|}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f b
B = {|bv|}
\<Theta> ; {|bv|} ; \<Gamma>  \<Turnstile> c

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.  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b
[PROOF STEP]
show "i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b
[PROOF STEP]
using subst_gb.simps *
[PROOF STATE]
proof (prove)
using this:
GNil[?uu::=?uv]\<^sub>\<Gamma>\<^sub>b = GNil
((?y, ?b', ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?bv::=?b]\<^sub>\<Gamma>\<^sub>b = (?y, ?b'[?bv::=?b]\<^sub>b\<^sub>b, ?c[?bv::=?b]\<^sub>c\<^sub>b) #\<^sub>\<Gamma> ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b

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

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

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<Gamma> \<turnstile> i'
 i' \<Turnstile> \<Gamma>
[PROOF STEP]
have ic:"i' \<Turnstile> c"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i'
 i' \<Turnstile> \<Gamma>

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
using assms valid_def
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i'
 i' \<Turnstile> \<Gamma>
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f b
B = {|bv|}
\<Theta> ; {|bv|} ; \<Gamma>  \<Turnstile> c
valid \<equiv> \<lambda>x0 x1 x2 x3. valid_sumC (x0, x1, x2, x3)

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
using valid.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i'
 i' \<Turnstile> \<Gamma>
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f b
B = {|bv|}
\<Theta> ; {|bv|} ; \<Gamma>  \<Turnstile> c
valid \<equiv> \<lambda>x0 x1 x2 x3. valid_sumC (x0, x1, x2, x3)
(?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 blast
[PROOF STATE]
proof (state)
this:
 i' \<Turnstile> c

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<Longrightarrow>  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
show  "i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
proof(rule is_satis_bs_boxed_rev)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1.  ?\<Theta>  ; ?\<Gamma> ; b , bv \<turnstile> i \<approx> ?i'
 2.  ?\<Theta> ; ?B ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 3.  ?\<Theta> ; ?\<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 4.  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i'
 5.  ?\<Theta> ; {||} ; ?\<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
 6.  ?i' \<Turnstile> c
[PROOF STEP]
show "\<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
using idash
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

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

goal (5 subgoals):
 1.  \<Theta> ; ?B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 2.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 3.  \<Theta> ; \<Gamma> \<turnstile> i'
 4.  \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
 5.  i' \<Turnstile> c
[PROOF STEP]
show "\<Theta> ; B ; \<Gamma>  \<turnstile>\<^sub>w\<^sub>f c "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
[PROOF STEP]
using wfc assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; {|bv|} ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f b
B = {|bv|}
\<Theta> ; {|bv|} ; \<Gamma>  \<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 (4 subgoals):
 1.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 2.  \<Theta> ; \<Gamma> \<turnstile> i'
 3.  \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
 4.  i' \<Turnstile> c
[PROOF STEP]
show "\<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
[PROOF STEP]
using subst_gb.simps *
[PROOF STATE]
proof (prove)
using this:
GNil[?uu::=?uv]\<^sub>\<Gamma>\<^sub>b = GNil
((?y, ?b', ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?bv::=?b]\<^sub>\<Gamma>\<^sub>b = (?y, ?b'[?bv::=?b]\<^sub>b\<^sub>b, ?c[?bv::=?b]\<^sub>c\<^sub>b) #\<^sub>\<Gamma> ?\<Gamma>[?bv::=?b]\<^sub>\<Gamma>\<^sub>b
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i \<and>  i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i

goal (3 subgoals):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
 2.  \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
 3.  i' \<Turnstile> c
[PROOF STEP]
show "\<Theta> ; \<Gamma> \<turnstile> i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i'
[PROOF STEP]
using wfi
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i'

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

goal (2 subgoals):
 1.  \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
 2.  i' \<Turnstile> c
[PROOF STEP]
show "\<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b

goal (1 subgoal):
 1.  \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b   \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\<^sub>c\<^sub>b

goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
show "i' \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i' \<Turnstile> c
[PROOF STEP]
using ic
[PROOF STATE]
proof (prove)
using this:
 i' \<Turnstile> c

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b

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

goal:
No subgoals!
[PROOF STEP]
qed