[STATEMENT]
lemma eval_c_eq_bs_boxed:
  fixes c::c
  assumes "i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s" and "i' \<lbrakk> c \<rbrakk> ~ s'" and "wfC \<Theta> B \<Gamma> c" and "wfI \<Theta> \<Gamma> i'" and "\<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<turnstile> i "
    and "boxed_i \<Theta> \<Gamma> b bv i i'"
  shows "s = s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 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'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
proof(nominal_induct c arbitrary: s s'  rule:c.strong_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> (TRUE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> TRUE \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  \<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'
 2. \<And>s s'. \<lbrakk> i \<lbrakk> (FALSE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> FALSE \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 6. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 7. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
case C_true
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> (TRUE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> TRUE \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (7 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> (TRUE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> TRUE \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  \<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'
 2. \<And>s s'. \<lbrakk> i \<lbrakk> (FALSE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> FALSE \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 6. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 7. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> (TRUE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> TRUE \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> (TRUE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> TRUE \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_c_elims subst_cb.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> (TRUE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> TRUE \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> TRUE \<rbrakk> ~ True ; ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> FALSE \<rbrakk> ~ False ; ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<and> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<or> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<longrightarrow> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ ?s ; \<And>b. \<lbrakk>?s = (\<not> b);  ?i \<lbrakk> ?c \<rbrakk> ~ b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?s ; \<And>sv1 sv2. \<lbrakk>?s = (sv1 = sv2); ?i \<lbrakk> ?e1.0 \<rbrakk> ~ sv1 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> TRUE \<rbrakk> ~ ?s ; ?s \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> FALSE \<rbrakk> ~ ?s ; \<not> ?s \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(TRUE)[?x::=?v]\<^sub>c\<^sub>b = (TRUE)
(FALSE)[?x::=?v]\<^sub>c\<^sub>b = (FALSE)
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>b )
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b OR ?c2.0[?x::=?v]\<^sub>c\<^sub>b )
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>b )
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>b  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>b )
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>b = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>b )

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = s'

goal (6 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> (FALSE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> FALSE \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 5. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 6. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> (FALSE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> FALSE \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 5. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 6. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
case C_false
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> (FALSE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> FALSE \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (6 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> (FALSE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> FALSE \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 5. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 6. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> (FALSE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> FALSE \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> (FALSE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> FALSE \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_c_elims  subst_cb.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> (FALSE)[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> FALSE \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> TRUE \<rbrakk> ~ True ; ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> FALSE \<rbrakk> ~ False ; ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<and> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<or> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<longrightarrow> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ ?s ; \<And>b. \<lbrakk>?s = (\<not> b);  ?i \<lbrakk> ?c \<rbrakk> ~ b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?s ; \<And>sv1 sv2. \<lbrakk>?s = (sv1 = sv2); ?i \<lbrakk> ?e1.0 \<rbrakk> ~ sv1 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> TRUE \<rbrakk> ~ ?s ; ?s \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> FALSE \<rbrakk> ~ ?s ; \<not> ?s \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(TRUE)[?x::=?v]\<^sub>c\<^sub>b = (TRUE)
(FALSE)[?x::=?v]\<^sub>c\<^sub>b = (FALSE)
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>b )
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b OR ?c2.0[?x::=?v]\<^sub>c\<^sub>b )
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>b )
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>b  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>b )
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>b = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>b )

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = s'

goal (5 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 5. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 5. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
case (C_conj c1 c2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1  AND  c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1  AND  c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  AND  c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (5 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 5. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1 and s2 where 1: "eval_c i (c1[bv::=b]\<^sub>c\<^sub>b) s1 \<and> eval_c i (c2[bv::=b]\<^sub>c\<^sub>b) s2 \<and> s = (s1\<and>s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2.  i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1  \<and>  i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s2  \<and> s = (s1 \<and> s2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_conj eval_c_elims(3) subst_cb.simps(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1  AND  c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1  AND  c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  AND  c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<and> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>b )

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

goal (5 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 5. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1' and s2' where 2:"eval_c i' c1 s1' \<and> eval_c i' c2 s2' \<and> s' = (s1'\<and>s2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1' s2'.  i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<and> s2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_conj eval_c_elims(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1  AND  c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1  AND  c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  AND  c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<and> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (5 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  AND  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 5. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<and> s2')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<and> s2')

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using 1 2 wfC_elims C_conj
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<and> s2')
 i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1  \<and>  i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s2  \<and> s = (s1 \<and> s2)
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<and> s2')
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1  AND  c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1  AND  c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  AND  c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = s'

goal (4 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
case (C_disj c1 c2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1 OR c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1 OR c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 OR c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (4 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1 and s2 where 1: "eval_c i (c1[bv::=b]\<^sub>c\<^sub>b) s1 \<and> eval_c i (c2[bv::=b]\<^sub>c\<^sub>b) s2 \<and> s = (s1\<or>s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2.  i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1  \<and>  i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s2  \<and> s = (s1 \<or> s2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_disj eval_c_elims(4) subst_cb.simps(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1 OR c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1 OR c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 OR c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<or> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b OR ?c2.0[?x::=?v]\<^sub>c\<^sub>b )

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

goal (4 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1' and s2' where 2:"eval_c i' c1 s1' \<and> eval_c i' c2 s2' \<and> s' = (s1'\<or>s2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1' s2'.  i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<or> s2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_disj eval_c_elims(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1 OR c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1 OR c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 OR c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<or> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>s1' s2'.  i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<or> s2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<or> s2')

goal (4 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1 OR x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 OR x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  \<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'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 4. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<or> s2')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<or> s2')

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using 1 2 wfC_elims C_disj
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<or> s2')
 i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1  \<and>  i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s2  \<and> s = (s1 \<or> s2)
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<or> s2')
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1 OR c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1 OR c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 OR c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = s'

goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
case (C_not c)
[PROOF STATE]
proof (state)
this:
\<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'
 i \<lbrakk> (\<not> c )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> \<not> c  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> c
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1::bool  where 1: "(i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1) \<and> (s = (\<not> s1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1.  i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1  \<and> s = (\<not> s1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  C_not eval_c_elims(6) subst_cb.simps(7)
[PROOF STATE]
proof (prove)
using this:
\<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'
 i \<lbrakk> (\<not> c )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> \<not> c  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> c
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ ?s ; \<And>b. \<lbrakk>?s = (\<not> b);  ?i \<lbrakk> ?c \<rbrakk> ~ b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>b = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>b )

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

goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1'::bool where 2: "(i' \<lbrakk> c \<rbrakk> ~ s1') \<and> (s' = (\<not> s1'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1'.  i' \<lbrakk> c \<rbrakk> ~ s1'  \<and> s' = (\<not> s1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_not eval_c_elims(6)
[PROOF STATE]
proof (prove)
using this:
\<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'
 i \<lbrakk> (\<not> c )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> \<not> c  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> c
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ ?s ; \<And>b. \<lbrakk>?s = (\<not> b);  ?i \<lbrakk> ?c \<rbrakk> ~ b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x ;  \<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';  i \<lbrakk> (\<not> x )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> \<not> x  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 3. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i' \<lbrakk> c \<rbrakk> ~ s1'  \<and> s' = (\<not> s1')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c \<rbrakk> ~ s1'  \<and> s' = (\<not> s1')

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using 1 2 wfC_elims C_not
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c \<rbrakk> ~ s1'  \<and> s' = (\<not> s1')
 i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1  \<and> s = (\<not> s1)
 i' \<lbrakk> c \<rbrakk> ~ s1'  \<and> s' = (\<not> s1')
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<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'
 i \<lbrakk> (\<not> c )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> \<not> c  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> c
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = s'

goal (2 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
case (C_imp c1 c2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1  IMP  c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1  IMP  c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  IMP  c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (2 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1 and s2 where 1: "eval_c i (c1[bv::=b]\<^sub>c\<^sub>b) s1 \<and> eval_c i (c2[bv::=b]\<^sub>c\<^sub>b) s2 \<and> s = (s1 \<longrightarrow> s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2.  i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1  \<and>  i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s2  \<and> s = (s1 \<longrightarrow> s2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_imp eval_c_elims(5) subst_cb.simps(5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1  IMP  c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1  IMP  c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  IMP  c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<longrightarrow> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>b )

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

goal (2 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1' and s2' where 2:"eval_c i' c1 s1' \<and> eval_c i' c2 s2' \<and> s' = (s1' \<longrightarrow> s2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1' s2'.  i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<longrightarrow> s2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_imp eval_c_elims(5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1  IMP  c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1  IMP  c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  IMP  c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<longrightarrow> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>s1' s2'.  i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<longrightarrow> s2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<longrightarrow> s2')

goal (2 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 ;  \<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'; \<And>s s'. \<lbrakk> i \<lbrakk> x2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x2 \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 ;  \<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';  i \<lbrakk> (x1  IMP  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  \<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'
 2. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<longrightarrow> s2')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<longrightarrow> s2')

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using 1 2 wfC_elims C_imp
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<longrightarrow> s2')
 i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1  \<and>  i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s2  \<and> s = (s1 \<longrightarrow> s2)
 i' \<lbrakk> c1 \<rbrakk> ~ s1'  \<and>  i' \<lbrakk> c2 \<rbrakk> ~ s2'  \<and> s' = (s1' \<longrightarrow> s2')
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> i \<lbrakk> c1[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c1 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 ;  \<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'
\<lbrakk> i \<lbrakk> c2[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ ?s ;  i' \<lbrakk> c2 \<rbrakk> ~ ?s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 ;  \<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'
 i \<lbrakk> (c1  IMP  c2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> c1  IMP  c2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  IMP  c2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = s'

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
case (C_eq e1 e2)
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> (e1  ==  e2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f e1  ==  e2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain be where be: "wfCE \<Theta> B \<Gamma> e1 be \<and> wfCE \<Theta> B \<Gamma> e2 be"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>be.   \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f e1 : be  \<and>   \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f e2 : be  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_eq wfC_elims
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> (e1  ==  e2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f e1  ==  e2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>be.   \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f e1 : be  \<and>   \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f e2 : be  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f e1 : be  \<and>   \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f e2 : be

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1 and s2 where 1: "eval_e i (e1[bv::=b]\<^sub>c\<^sub>e\<^sub>b) s1 \<and> eval_e i (e2[bv::=b]\<^sub>c\<^sub>e\<^sub>b) s2 \<and> s = (s1 = s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> e1[bv::=b]\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ s1  \<and> i \<lbrakk> e2[bv::=b]\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ s2  \<and> s = (s1 = s2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_eq eval_c_elims(7) subst_cb.simps(6)
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> (e1  ==  e2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f e1  ==  e2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?s ; \<And>sv1 sv2. \<lbrakk>?s = (sv1 = sv2); ?i \<lbrakk> ?e1.0 \<rbrakk> ~ sv1 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>b  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>b )

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

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
obtain s1' and s2' where 2:"eval_e i' e1 s1' \<and> eval_e i' e2 s2' \<and> s' = (s1' = s2' )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1' s2'. i' \<lbrakk> e1 \<rbrakk> ~ s1'  \<and> i' \<lbrakk> e2 \<rbrakk> ~ s2'  \<and> s' = (s1' = s2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_eq eval_c_elims(7)
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> (e1  ==  e2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f e1  ==  e2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?s ; \<And>sv1 sv2. \<lbrakk>?s = (sv1 = sv2); ?i \<lbrakk> ?e1.0 \<rbrakk> ~ sv1 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
have "\<turnstile>\<^sub>w\<^sub>f \<Theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
[PROOF STEP]
using C_eq wfX_wfY
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> (e1  ==  e2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f e1  ==  e2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<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>

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

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
have "\<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 C_eq
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> (e1  ==  e2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f e1  ==  e2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'

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

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> (x1  ==  x2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s ;  i' \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' ;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  \<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'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using boxed_b_eq[of \<Theta> s1 be bv b s1' s2 s2'] 1 2 boxed_i_eval_ce_boxed_b  C_eq wfC_elims subst_cb.simps 1 2 be
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
\<lbrakk> \<Theta>  \<turnstile> s1 ~ be [ bv ::= b ] \<setminus> s1' ;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;    \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta>  \<turnstile> s2 ~ be [ bv ::= b ] \<setminus> s2' \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2')
i \<lbrakk> e1[bv::=b]\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ s1  \<and> i \<lbrakk> e2[bv::=b]\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ s2  \<and> s = (s1 = s2)
i' \<lbrakk> e1 \<rbrakk> ~ s1'  \<and> i' \<lbrakk> e2 \<rbrakk> ~ s2'  \<and> s' = (s1' = s2')
\<lbrakk>?i' \<lbrakk> ?e \<rbrakk> ~ ?s' ; ?i \<lbrakk> ?e[?bv::=?b']\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ ?s ;   ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e : ?b ;  ?\<Theta>  ; ?\<Gamma> ; ?b' , ?bv \<turnstile> ?i \<approx> ?i';  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i'\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> ?s ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s'
 i \<lbrakk> (e1  ==  e2 )[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s
 i' \<lbrakk> e1  ==  e2  \<rbrakk> ~ s'
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f e1  ==  e2
 \<Theta> ; \<Gamma> \<turnstile> i'
 \<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i
 \<Theta>  ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(TRUE)[?x::=?v]\<^sub>c\<^sub>b = (TRUE)
(FALSE)[?x::=?v]\<^sub>c\<^sub>b = (FALSE)
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>b )
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b OR ?c2.0[?x::=?v]\<^sub>c\<^sub>b )
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?c1.0[?x::=?v]\<^sub>c\<^sub>b  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>b )
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>b = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>b  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>b )
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>b = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>b )
i \<lbrakk> e1[bv::=b]\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ s1  \<and> i \<lbrakk> e2[bv::=b]\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ s2  \<and> s = (s1 = s2)
i' \<lbrakk> e1 \<rbrakk> ~ s1'  \<and> i' \<lbrakk> e2 \<rbrakk> ~ s2'  \<and> s' = (s1' = s2')
  \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f e1 : be  \<and>   \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f e2 : be

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

goal:
No subgoals!
[PROOF STEP]
qed