[STATEMENT]
lemma valid_arith_bop:
  assumes "wfG \<Theta> \<B>  \<Gamma>" and "opp = Plus \<and> ll = (L_num (n1+n2)) \<or> (opp = LEq \<and> ll = ( if n1\<le>n2 then L_true else L_false))"
    and "(opp = Plus \<longrightarrow> b = B_int) \<and> (opp = LEq \<longrightarrow> b = B_bool)" and
    "atom x \<sharp> \<Gamma>"
  shows   "\<Theta>; \<B> ; (x, b, (CE_val (V_var x)  ==  CE_val (V_lit (ll)) )) #\<^sub>\<Gamma> \<Gamma>
                          \<Turnstile> (CE_val (V_var x)  ==  CE_op opp ([V_lit (L_num n1)]\<^sup>c\<^sup>e) ([V_lit (L_num n2)]\<^sup>c\<^sup>e ))" (is "\<Theta> ; \<B> ; ?G \<Turnstile> ?c")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have "wfC \<Theta> \<B> ?G ?c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule wfC_e_eq2)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e : b
 2.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : b
 3.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
 4. atom x \<sharp> \<Gamma>
[PROOF STEP]
show "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f CE_val (V_lit ll) : b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e : b
[PROOF STEP]
using wfCE_valI wfV_litI assms base_for_lit.simps
[PROOF STATE]
proof (prove)
using this:
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
opp = plus \<and> ll = L_num (n1 + n2) \<or> opp = leq \<and> ll = (if n1 \<le> n2 then L_true else L_false)
(opp = plus \<longrightarrow> b = B_int) \<and> (opp = leq \<longrightarrow> b = B_bool)
atom x \<sharp> \<Gamma>
base_for_lit L_true = B_bool
base_for_lit L_false = B_bool
base_for_lit (L_num ?n) = B_int
base_for_lit L_unit = B_unit
base_for_lit (L_bitvec ?v) = B_bitvec

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e : b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e : b

goal (3 subgoals):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : b
 2.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
 3. atom x \<sharp> \<Gamma>
[PROOF STEP]
show "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f CE_op opp ([V_lit (L_num n1)]\<^sup>c\<^sup>e) ([V_lit (L_num n2)]\<^sup>c\<^sup>e) : b "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : b
[PROOF STEP]
using wfCE_plusI wfCE_leqI   wfCE_eqI wfV_litI wfCE_valI base_for_lit.simps assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : B_int
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : B_bool
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : ?b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : ?b \<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : B_bool
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b
base_for_lit L_true = B_bool
base_for_lit L_false = B_bool
base_for_lit (L_num ?n) = B_int
base_for_lit L_unit = B_unit
base_for_lit (L_bitvec ?v) = B_bitvec
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
opp = plus \<and> ll = L_num (n1 + n2) \<or> opp = leq \<and> ll = (if n1 \<le> n2 then L_true else L_false)
(opp = plus \<longrightarrow> b = B_int) \<and> (opp = leq \<longrightarrow> b = B_bool)
atom x \<sharp> \<Gamma>

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : b

goal (2 subgoals):
 1.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
 2. atom x \<sharp> \<Gamma>
[PROOF STEP]
show "\<turnstile>\<^sub>w\<^sub>f \<Theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
[PROOF STEP]
using assms wfX_wfY
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
opp = plus \<and> ll = L_num (n1 + n2) \<or> opp = leq \<and> ll = (if n1 \<le> n2 then L_true else L_false)
(opp = plus \<longrightarrow> b = B_int) \<and> (opp = leq \<longrightarrow> b = B_bool)
atom x \<sharp> \<Gamma>
 ?\<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 auto
[PROOF STATE]
proof (state)
this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>

goal (1 subgoal):
 1. atom x \<sharp> \<Gamma>
[PROOF STEP]
show "atom x \<sharp> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
opp = plus \<and> ll = L_num (n1 + n2) \<or> opp = leq \<and> ll = (if n1 \<le> n2 then L_true else L_false)
(opp = plus \<longrightarrow> b = B_int) \<and> (opp = leq \<longrightarrow> b = B_bool)
atom x \<sharp> \<Gamma>

goal (1 subgoal):
 1. atom x \<sharp> \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have "\<forall>i. wfI \<Theta> ?G i \<and> is_satis_g i ?G \<longrightarrow> is_satis i ?c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule allI , rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
assume "wfI \<Theta> ?G i \<and> is_satis_g i ?G"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
hence "is_satis i  ((CE_val (V_var x)  ==  CE_val (V_lit (ll)) ))"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
thus  "is_satis i ((CE_val (V_var x)  ==  CE_op opp ([V_lit (L_num n1)]\<^sup>c\<^sup>e) ([V_lit (L_num n2)]\<^sup>c\<^sup>e)))"
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
using is_satis_plus_imp assms opp.exhaust is_satis_leq_imp
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e
 ?i \<Turnstile> [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (?n1.0 + ?n2.0) ]\<^sup>v ]\<^sup>c\<^sup>e   \<Longrightarrow>  ?i \<Turnstile> [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num ?n1.0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num ?n2.0 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
opp = plus \<and> ll = L_num (n1 + n2) \<or> opp = leq \<and> ll = (if n1 \<le> n2 then L_true else L_false)
(opp = plus \<longrightarrow> b = B_int) \<and> (opp = leq \<longrightarrow> b = B_bool)
atom x \<sharp> \<Gamma>
\<lbrakk>?y = plus \<Longrightarrow> ?P; ?y = leq \<Longrightarrow> ?P; ?y = eq \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
 ?i \<Turnstile> [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if ?n1.0 \<le> ?n2.0 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e   \<Longrightarrow>  ?i \<Turnstile> [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num ?n1.0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num ?n2.0 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
\<forall>i.  \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
\<forall>i.  \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
using valid.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
\<forall>i.  \<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<Theta> ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ ll ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ opp [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_eq_bop:
  assumes "wfG \<Theta> \<B>  \<Gamma>" and  "atom x \<sharp> \<Gamma>"  and  "base_for_lit l1 = base_for_lit l2"
  shows   "\<Theta>; \<B> ; (x, B_bool, (CE_val (V_var x)  ==  CE_val (V_lit (if l1 = l2 then L_true else L_false)) )) #\<^sub>\<Gamma> \<Gamma>
                          \<Turnstile> (CE_val (V_var x)  ==  CE_op Eq ([V_lit (l1)]\<^sup>c\<^sup>e) ([V_lit (l2)]\<^sup>c\<^sup>e ))" (is "\<Theta> ; \<B> ; ?G \<Turnstile> ?c")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
let ?ll = "(if l1 = l2 then L_true else L_false)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have "wfC \<Theta> \<B> ?G ?c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule wfC_e_eq2)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e : B_bool
 2.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bool
 3.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
 4. atom x \<sharp> \<Gamma>
[PROOF STEP]
show "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f CE_val (V_lit ?ll) : B_bool"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e : B_bool
[PROOF STEP]
using wfCE_valI wfV_litI assms base_for_lit.simps
[PROOF STATE]
proof (prove)
using this:
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>
base_for_lit l1 = base_for_lit l2
base_for_lit L_true = B_bool
base_for_lit L_false = B_bool
base_for_lit (L_num ?n) = B_int
base_for_lit L_unit = B_unit
base_for_lit (L_bitvec ?v) = B_bitvec

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e : B_bool
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e : B_bool

goal (3 subgoals):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bool
 2.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
 3. atom x \<sharp> \<Gamma>
[PROOF STEP]
show "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f CE_op Eq ([V_lit (l1)]\<^sup>c\<^sup>e) ([V_lit (l2)]\<^sup>c\<^sup>e) : B_bool "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bool
[PROOF STEP]
using wfCE_eqI wfCE_leqI   wfCE_eqI wfV_litI wfCE_valI base_for_lit.simps assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : ?b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : ?b \<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : B_bool
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : B_bool
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : ?b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : ?b \<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : B_bool
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b
base_for_lit L_true = B_bool
base_for_lit L_false = B_bool
base_for_lit (L_num ?n) = B_int
base_for_lit L_unit = B_unit
base_for_lit (L_bitvec ?v) = B_bitvec
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>
base_for_lit l1 = base_for_lit l2

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bool
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bool

goal (2 subgoals):
 1.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
 2. atom x \<sharp> \<Gamma>
[PROOF STEP]
show "\<turnstile>\<^sub>w\<^sub>f \<Theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.    \<turnstile>\<^sub>w\<^sub>f \<Theta>
[PROOF STEP]
using assms wfX_wfY
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>
base_for_lit l1 = base_for_lit l2
 ?\<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 auto
[PROOF STATE]
proof (state)
this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>

goal (1 subgoal):
 1. atom x \<sharp> \<Gamma>
[PROOF STEP]
show "atom x \<sharp> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>
base_for_lit l1 = base_for_lit l2

goal (1 subgoal):
 1. atom x \<sharp> \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have "\<forall>i. wfI \<Theta> ?G i \<and> is_satis_g i ?G \<longrightarrow> is_satis i ?c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule allI , rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
assume "wfI \<Theta> ?G i \<and> is_satis_g i ?G"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
hence "is_satis i  ((CE_val (V_var x)  ==  CE_val (V_lit (?ll)) ))"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
thus  "is_satis i ((CE_val (V_var x)  ==  CE_op Eq ([V_lit (l1)]\<^sup>c\<^sup>e) ([V_lit (l2)]\<^sup>c\<^sup>e)))"
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
using is_satis_eq_imp assms
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e
 ?i \<Turnstile> [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if ?n1.0 = ?n2.0 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e   \<Longrightarrow>  ?i \<Turnstile> [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ ?n1.0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ ?n2.0 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>
base_for_lit l1 = base_for_lit l2

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
\<forall>i.  \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
\<forall>i.  \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
using valid.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
\<forall>i.  \<Theta> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<Theta> ; \<B> ; (x, B_bool, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if l1 = l2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ l1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ l2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_fst:
  fixes x::x and v\<^sub>1::v and v\<^sub>2::v
  assumes   "wfTh \<Theta>" and "wfV \<Theta> \<B> GNil (V_pair v\<^sub>1 v\<^sub>2) (B_pair b\<^sub>1 b\<^sub>2)"
  shows "\<Theta> ; \<B> ; (x, b\<^sub>1, [[x]\<^sup>v]\<^sup>c\<^sup>e  ==  [v\<^sub>1]\<^sup>c\<^sup>e) #\<^sub>\<Gamma> GNil  \<Turnstile> [[x]\<^sup>v]\<^sup>c\<^sup>e  ==  [#1[[v\<^sub>1,v\<^sub>2]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b\<^sub>1, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v\<^sub>1 ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule valid_eq_e)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<forall>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
 2.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 ]\<^sup>c\<^sup>e : b\<^sub>1
 3.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>1
[PROOF STEP]
show \<open>\<forall>i s1 s2.  (\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil)  \<and>  (\<Theta> ; GNil \<turnstile> i) \<and> (i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1)  \<and> (i \<lbrakk> [#1[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2)  \<longrightarrow> s1 = s2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
[PROOF STEP]
proof(rule+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
fix i s1 s2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
assume as:"\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> (i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1)  \<and> (i \<lbrakk> [#1[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2)"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2
[PROOF STEP]
obtain s2' where *:"i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2 s2'"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. (\<And>s2'. i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2 s2'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_e_elims(5)[of i "[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e" s2] eval_e_elims
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2
\<lbrakk>i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2 ; \<And>v2. i \<lbrakk> [ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SPair s2 v2  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SNum (n1 + n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SBool (n1 \<le> n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SBool (s1 = s2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v2. ?i \<lbrakk> ?v \<rbrakk> ~ SPair ?s v2  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v1. ?i \<lbrakk> ?v \<rbrakk> ~ SPair v1 ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv1 bv2. \<lbrakk>?s = SBitvec (bv1 @ bv2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec bv1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv. \<lbrakk>?s = SNum (int (length bv)); ?i \<lbrakk> ?v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>s2'. i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2 s2'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2 s2'

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2 s2'
[PROOF STEP]
have " i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s2"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2 s2'

goal (1 subgoal):
 1. i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s2
[PROOF STEP]
using eval_v_elims(3)[OF *]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2 s2'
(\<And>s1 s2a. \<lbrakk>SPair s2 s2' = SPair s1 s2a; i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s1 ; i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2a \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s2
[PROOF STEP]
show "s1 = s2"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using eval_v_uniqueness as
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s2
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using eval_e_uniqueness eval_e_valI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s2
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2
\<lbrakk>?i \<lbrakk> ?e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?e \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s1 = s2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>1 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<longrightarrow> s1 = s2

goal (2 subgoals):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 ]\<^sup>c\<^sup>e : b\<^sub>1
 2.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>1
[PROOF STEP]
show \<open>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 ]\<^sup>c\<^sup>e : b\<^sub>1 \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 ]\<^sup>c\<^sup>e : b\<^sub>1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v : [ b\<^sub>1 , b\<^sub>2 ]\<^sup>b

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 ]\<^sup>c\<^sup>e : b\<^sub>1
[PROOF STEP]
by (metis b.eq_iff(4) wfV_elims(3) wfV_wfCE)
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 ]\<^sup>c\<^sup>e : b\<^sub>1

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>1
[PROOF STEP]
show \<open>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>1 \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v : [ b\<^sub>1 , b\<^sub>2 ]\<^sup>b

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>1
[PROOF STEP]
using wfCE_fstI
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v : [ b\<^sub>1 , b\<^sub>2 ]\<^sup>b
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0]\<^sup>c\<^sup>e : ?b1.0

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>1
[PROOF STEP]
using wfCE_valI
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v : [ b\<^sub>1 , b\<^sub>2 ]\<^sup>b
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0]\<^sup>c\<^sup>e : ?b1.0
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_snd:
  fixes x::x and v\<^sub>1::v and v\<^sub>2::v
  assumes   "wfTh \<Theta>" and "wfV \<Theta> \<B> GNil (V_pair v\<^sub>1 v\<^sub>2) (B_pair b\<^sub>1 b\<^sub>2)"
  shows "\<Theta> ; \<B> ; (x, b\<^sub>2, [[x]\<^sup>v]\<^sup>c\<^sup>e  ==  [v\<^sub>2]\<^sup>c\<^sup>e) #\<^sub>\<Gamma> GNil  \<Turnstile> [[x]\<^sup>v]\<^sup>c\<^sup>e  ==  [#2[[v\<^sub>1,v\<^sub>2]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b\<^sub>2, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v\<^sub>2 ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule valid_eq_e)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<forall>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
 2.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>2 ]\<^sup>c\<^sup>e : b\<^sub>2
 3.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>2
[PROOF STEP]
show \<open>\<forall>i s1 s2.  (\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil)  \<and>  (\<Theta> ; GNil \<turnstile> i) \<and> (i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1)  \<and>
(i \<lbrakk> [#2[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2)  \<longrightarrow> s1 = s2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
[PROOF STEP]
proof(rule+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
fix i s1 s2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
assume as:"\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> (i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1)  \<and> (i \<lbrakk> [#2[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2)"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2
[PROOF STEP]
obtain s2' where *:"i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2' s2"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. (\<And>s2'. i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2' s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_e_elims(5)[of i "[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e" s2] eval_e_elims
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2
\<lbrakk>i \<lbrakk> [#1[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2 ; \<And>v2. i \<lbrakk> [ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SPair s2 v2  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SNum (n1 + n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SBool (n1 \<le> n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SBool (s1 = s2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v2. ?i \<lbrakk> ?v \<rbrakk> ~ SPair ?s v2  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v1. ?i \<lbrakk> ?v \<rbrakk> ~ SPair v1 ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv1 bv2. \<lbrakk>?s = SBitvec (bv1 @ bv2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec bv1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv. \<lbrakk>?s = SNum (int (length bv)); ?i \<lbrakk> ?v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>s2'. i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2' s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2' s2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2' s2
[PROOF STEP]
have " i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2' s2

goal (1 subgoal):
 1. i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2
[PROOF STEP]
using eval_v_elims(3)[OF *]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2' s2
(\<And>s1 s2a. \<lbrakk>SPair s2' s2 = SPair s1 s2a; i \<lbrakk> v\<^sub>1 \<rbrakk> ~ s1 ; i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2a \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2
[PROOF STEP]
show "s1 = s2"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using eval_v_uniqueness as
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using eval_e_uniqueness eval_e_valI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v\<^sub>2 \<rbrakk> ~ s2
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2
\<lbrakk>?i \<lbrakk> ?e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?e \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s1 = s2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i s1 s2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Theta> ; GNil \<turnstile> i \<and> i \<lbrakk> [ v\<^sub>2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<longrightarrow> s1 = s2

goal (2 subgoals):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>2 ]\<^sup>c\<^sup>e : b\<^sub>2
 2.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>2
[PROOF STEP]
show \<open>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>2 ]\<^sup>c\<^sup>e : b\<^sub>2 \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>2 ]\<^sup>c\<^sup>e : b\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v : [ b\<^sub>1 , b\<^sub>2 ]\<^sup>b

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>2 ]\<^sup>c\<^sup>e : b\<^sub>2
[PROOF STEP]
by (metis b.eq_iff wfV_elims wfV_wfCE)
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>2 ]\<^sup>c\<^sup>e : b\<^sub>2

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>2
[PROOF STEP]
show \<open>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#2[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>2 \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v : [ b\<^sub>1 , b\<^sub>2 ]\<^sup>b

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>2
[PROOF STEP]
using wfCE_sndI wfCE_valI
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
 \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v : [ b\<^sub>1 , b\<^sub>2 ]\<^sup>b
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2?v1.0]\<^sup>c\<^sup>e : ?b2.0
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#2[ [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e : b\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_concat:
  fixes v1::"bit list" and v2::"bit list"
  assumes " \<turnstile>\<^sub>w\<^sub>f \<Pi>"
  shows "\<Pi> ; \<B> ; (x, B_bitvec, (CE_val (V_var x)  ==  CE_val (V_lit (L_bitvec (v1@ v2))))) #\<^sub>\<Gamma> GNil \<Turnstile>
            (CE_val (V_var x)  ==  CE_concat ([V_lit (L_bitvec v1)]\<^sup>c\<^sup>e ) ([V_lit (L_bitvec v2)]\<^sup>c\<^sup>e) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Pi> ; \<B> ; (x, B_bitvec, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule valid_eq_e)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<forall>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
 2.   \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e : B_bitvec
 3.   \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bitvec
[PROOF STEP]
show \<open>\<forall>i s1 s2.  ((\<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil)  \<and>  (\<Pi> ; GNil \<turnstile> i) \<and>
            (i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1)  \<and> (i \<lbrakk> [[[ L_bitvec v1 ]\<^sup>v]\<^sup>c\<^sup>e  @@ [[ L_bitvec v2 ]\<^sup>v]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  \<rbrakk> ~ s2)  \<longrightarrow>
           s1 = s2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
[PROOF STEP]
proof(rule+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
fix i s1 s2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
assume as: "(\<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil)  \<and>  (\<Pi> ; GNil \<turnstile> i) \<and> (i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1)  \<and>
            (i \<lbrakk> [[[ L_bitvec v1 ]\<^sup>v]\<^sup>c\<^sup>e @@ [[ L_bitvec v2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e  \<rbrakk> ~ s2) "
[PROOF STATE]
proof (state)
this:
 \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
hence *: "i \<lbrakk> [[[ L_bitvec v1 ]\<^sup>v]\<^sup>c\<^sup>e @@ [[ L_bitvec v2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e  \<rbrakk> ~ s2"
[PROOF STATE]
proof (prove)
using this:
 \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
obtain bv1 bv2 where s2:"s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SBitvec bv1  \<and> (i \<lbrakk> [ L_bitvec v2 ]\<^sup>v \<rbrakk> ~ SBitvec bv2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bv1 bv2. s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> [ L_bitvec v2 ]\<^sup>v \<rbrakk> ~ SBitvec bv2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_e_elims(7)[OF *] eval_e_elims(1)
[PROOF STATE]
proof (prove)
using this:
(\<And>bv1 bv2. \<lbrakk>s2 = SBitvec (bv1 @ bv2); i \<lbrakk> [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>bv1 bv2. s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> [ L_bitvec v2 ]\<^sup>v \<rbrakk> ~ SBitvec bv2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> [ L_bitvec v2 ]\<^sup>v \<rbrakk> ~ SBitvec bv2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
hence "v1 = bv1 \<and> v2 = bv2"
[PROOF STATE]
proof (prove)
using this:
s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> [ L_bitvec v2 ]\<^sup>v \<rbrakk> ~ SBitvec bv2

goal (1 subgoal):
 1. v1 = bv1 \<and> v2 = bv2
[PROOF STEP]
using eval_v_elims(1) eval_l.simps(5)
[PROOF STATE]
proof (prove)
using this:
s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> [ L_bitvec v2 ]\<^sup>v \<rbrakk> ~ SBitvec bv2
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. v1 = bv1 \<and> v2 = bv2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
v1 = bv1 \<and> v2 = bv2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v1 = bv1 \<and> v2 = bv2

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 = bv1 \<and> v2 = bv2
[PROOF STEP]
have "s1 = SBitvec  (bv1 @ bv2)"
[PROOF STATE]
proof (prove)
using this:
v1 = bv1 \<and> v2 = bv2

goal (1 subgoal):
 1. s1 = SBitvec (bv1 @ bv2)
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
v1 = bv1 \<and> v2 = bv2
s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> [ L_bitvec v2 ]\<^sup>v \<rbrakk> ~ SBitvec bv2

goal (1 subgoal):
 1. s1 = SBitvec (bv1 @ bv2)
[PROOF STEP]
using eval_v_elims(1) eval_l.simps(5)
[PROOF STATE]
proof (prove)
using this:
v1 = bv1 \<and> v2 = bv2
s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> [ L_bitvec v2 ]\<^sup>v \<rbrakk> ~ SBitvec bv2
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. s1 = SBitvec (bv1 @ bv2)
[PROOF STEP]
by (metis as eval_e_elims(1))
[PROOF STATE]
proof (state)
this:
s1 = SBitvec (bv1 @ bv2)

goal (1 subgoal):
 1. \<And>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 = SBitvec (bv1 @ bv2)
[PROOF STEP]
show "s1 = s2"
[PROOF STATE]
proof (prove)
using this:
s1 = SBitvec (bv1 @ bv2)

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
s1 = SBitvec (bv1 @ bv2)
s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> [ L_bitvec v2 ]\<^sup>v \<rbrakk> ~ SBitvec bv2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i s1 s2.  \<Pi> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  \<Pi> ; GNil \<turnstile> i \<and> i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<longrightarrow> s1 = s2

goal (2 subgoals):
 1.   \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e : B_bitvec
 2.   \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bitvec
[PROOF STEP]
show \<open>  \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e : B_bitvec \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e : B_bitvec
[PROOF STEP]
by (metis assms base_for_lit.simps(5) wfG_nilI wfV_litI wfV_wfCE)
[PROOF STATE]
proof (state)
this:
  \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e : B_bitvec

goal (1 subgoal):
 1.   \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bitvec
[PROOF STEP]
show \<open>  \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [[[ L_bitvec v1 ]\<^sup>v]\<^sup>c\<^sup>e @@ [[ L_bitvec v2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e  : B_bitvec \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bitvec
[PROOF STEP]
by (metis assms base_for_lit.simps(5) wfCE_concatI wfG_nilI wfV_litI wfCE_valI)
[PROOF STATE]
proof (state)
this:
  \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ [ L_bitvec v1 ]\<^sup>v ]\<^sup>c\<^sup>e @@ [ [ L_bitvec v2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : B_bitvec

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_ce_eq:
  fixes ce::ce
  assumes  "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : b"
  shows \<open>\<Theta> ; \<B> ; \<Gamma>  \<Turnstile> ce  ==  ce \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; \<Gamma>  \<Turnstile> ce  ==  ce
[PROOF STEP]
unfolding valid.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f ce  ==  ce   \<and> (\<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> ce  ==  ce  )
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f ce  ==  ce
 2. \<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> ce  ==  ce
[PROOF STEP]
show \<open> \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f ce  ==  ce  \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f ce  ==  ce
[PROOF STEP]
using assms wfC_eqI
[PROOF STATE]
proof (prove)
using this:
  \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : 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>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0

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

goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> ce  ==  ce
[PROOF STEP]
show \<open>\<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> ce  ==  ce  \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<longrightarrow>  i \<Turnstile> ce  ==  ce
[PROOF STEP]
proof(rule+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<lbrakk> ce  ==  ce  \<rbrakk> ~ True
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<lbrakk> ce  ==  ce  \<rbrakk> ~ True
[PROOF STEP]
assume "\<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<lbrakk> ce  ==  ce  \<rbrakk> ~ True
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>
[PROOF STEP]
obtain s where "i\<lbrakk> ce \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>

goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> ce \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms eval_e_exist
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>
  \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : b
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;   ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?e \<rbrakk> ~ s

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

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; \<Gamma> \<turnstile> i \<and>  i \<Turnstile> \<Gamma>  \<Longrightarrow>  i \<lbrakk> ce  ==  ce  \<rbrakk> ~ True
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> ce \<rbrakk> ~ s
[PROOF STEP]
show "i \<lbrakk> ce  ==  ce  \<rbrakk> ~ True "
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> ce \<rbrakk> ~ s

goal (1 subgoal):
 1.  i \<lbrakk> ce  ==  ce  \<rbrakk> ~ True
[PROOF STEP]
using eval_c_eqI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> ce \<rbrakk> ~ s
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0

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

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

goal:
No subgoals!
[PROOF STEP]
qed