[STATEMENT]
lemma valid_eq_e:
  assumes "\<forall>i s1 s2. wfG P \<B> GNil \<and> wfI P GNil i \<and> eval_e i e1 s1 \<and> eval_e i e2 s2 \<longrightarrow> s1 = s2"
    and "wfCE P  \<B> GNil e1 b" and "wfCE P \<B> GNil e2 b"
  shows "P ; \<B> ; (x, b , CE_val (V_var x)  ==  e1 )#\<^sub>\<Gamma> GNil \<Turnstile>  CE_val (V_var x)  ==  e2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2
[PROOF STEP]
unfolding valid.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2   \<and> (\<forall>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  )
[PROOF STEP]
proof(intro conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  P ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2
 2. \<forall>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2
[PROOF STEP]
show \<open> P ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2
[PROOF STEP]
using assms wf_intros wfX_wfY  b.eq_iff fresh_GNil wfC_e_eq2 wfV_elims
[PROOF STATE]
proof (prove)
using this:
\<forall>i s1 s2.  P ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  P ; GNil \<turnstile> i \<and> i \<lbrakk> e1 \<rbrakk> ~ s1  \<and> i \<lbrakk> e2 \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
  P ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f e1 : b
  P ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f e2 : b
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f B_int
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f B_bool
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f B_unit
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f B_bitvec
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b1.0 ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b2.0 \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ; AF_typedef ?s ?dclist \<in> set ?\<Theta>\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f B_id ?s
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f B_app ?s ?b
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; Some (?b, ?c) = lookup ?\<Gamma> ?x\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?x ]\<^sup>v : ?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
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : ?b1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : ?b2.0 \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 , ?v2.0 ]\<^sup>v : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b'  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b' \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?s ?dc ?v : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b'  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; atom ?bv \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>, ?b, ?v);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b'[?bv::=?b]\<^sub>b\<^sub>b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp ?s ?dc ?b ?v : B_app ?s ?b
 ?\<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
\<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> ; ?\<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 ?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
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e : B_bitvec
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec  \<Longrightarrow>   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [| ?v1.0 |]\<^sup>c\<^sup>e : B_int
\<lbrakk>atom ?z \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>);  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ;  ?\<Theta> ; ?\<B> ; (?z, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<lbrace> ?z : ?b  | ?c \<rbrace>
\<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
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil
\<lbrakk>?c \<notin> {TRUE, FALSE};  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B> ; (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>
\<lbrakk>?c \<in> {TRUE, FALSE};  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>
   \<turnstile>\<^sub>w\<^sub>f []
\<lbrakk>name_of_type ?tdef \<notin> name_of_type ` set ?\<Theta>;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ;  ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?tdef \<rbrakk> \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?tdef # ?\<Theta>
 ?\<Theta> ; {||}  ; GNil \<turnstile>\<^sub>w\<^sub>f ?lst  \<Longrightarrow>  ?\<Theta> \<turnstile>\<^sub>w\<^sub>f AF_typedef ?s ?lst
 ?\<Theta> ; {|?bv|}  ; GNil \<turnstile>\<^sub>w\<^sub>f ?lst  \<Longrightarrow>  ?\<Theta> \<turnstile>\<^sub>w\<^sub>f AF_typedef_poly ?s ?bv ?lst
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f []
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau> ; ?dc \<notin> fst ` set ?ts;  ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f (?dc, ?\<tau>) # ?ts
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>e : ?b
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<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> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ plus ?v1.0 ?v2.0 ]\<^sup>e : B_int
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<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> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>e : B_bool
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : ?b ; ?b \<in> {B_bool, B_int, B_unit}\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>e : B_bool
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0 ]\<^sup>e : ?b1.0
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [#2?v1.0 ]\<^sup>e : ?b2.0
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>e : B_bitvec
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0  ?v2.0 ]\<^sup>e : [ B_bitvec , B_bitvec ]\<^sup>b
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [| ?v1.0 |]\<^sup>e : B_int
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ; Some (AF_fundef ?f (AF_fun_typ_none (AF_fun_typ ?x ?b ?c ?\<tau> ?s))) = lookup_fun ?\<Phi> ?f;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ ?f  ?v  ]\<^sup>e : b_of ?\<tau>
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b' ; atom ?bv \<sharp> (?\<Phi>, ?\<Theta>, ?\<B>, ?\<Gamma>, ?\<Delta>, ?b', ?v, (b_of ?\<tau>)[?bv::=?b']\<^sub>b); Some (AF_fundef ?f (AF_fun_typ_some ?bv (AF_fun_typ ?x ?b ?c ?\<tau> ?s))) = lookup_fun ?\<Phi> ?f;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b[?bv::=?b']\<^sub>b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [?f [ ?b' ]  ?v ]\<^sup>e : (b_of ?\<tau>)[?bv::=?b']\<^sub>b
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ; (?u, ?\<tau>) \<in> setD ?\<Delta>\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ ?u ]\<^sup>e : b_of ?\<tau>
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [?v]\<^sup>s : ?b
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b' ;  ?\<Theta> ; ?\<Phi> ; ?\<B> ; (?x, ?b', TRUE) #\<^sub>\<Gamma> ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ; atom ?x \<sharp> (?\<Phi>, ?\<Theta>, ?\<B>, ?\<Gamma>, ?\<Delta>, ?e, ?b)\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f LET ?x = ?e IN ?s : ?b
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; (?x, B_bool, ?c) #\<^sub>\<Gamma> ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ; atom ?x \<sharp> (?\<Phi>, ?\<Theta>, ?\<B>, ?\<Gamma>, ?\<Delta>, ?c, ?b, ?s)\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ASSERT ?c IN ?s  : ?b
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s1.0 : b_of ?\<tau> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau> ;  ?\<Theta> ; ?\<Phi> ; ?\<B> ; (?x, b_of ?\<tau>, TRUE) #\<^sub>\<Gamma> ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s2.0 : ?b ; atom ?x \<sharp> (?\<Phi>, ?\<Theta>, ?\<B>, ?\<Gamma>, ?\<Delta>, ?s1.0, ?b, ?\<tau>)\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f LET ?x : ?\<tau> = ?s1.0 IN ?s2.0 : ?b
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : B_bool ;  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s1.0 : ?b ;  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s2.0 : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f IF ?v THEN ?s1.0 ELSE ?s2.0 : ?b
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b_of ?\<tau> ; atom ?u \<sharp> (?\<Phi>, ?\<Theta>, ?\<B>, ?\<Gamma>, ?\<Delta>, ?\<tau>, ?v, ?b);  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; (?u, ?\<tau>) #\<^sub>\<Delta> ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f VAR ?u : ?\<tau> = ?v IN ?s : ?b
\<lbrakk>(?u, ?\<tau>) \<in> setD ?\<Delta>;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b_of ?\<tau> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?u ::= ?v : B_unit
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s1.0 : B_bool ;  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s2.0 : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f WHILE ?s1.0 DO { ?s2.0 }  : ?b
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s1.0 : B_unit ;  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s2.0 : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f  ?s1.0 ;; ?s2.0  : ?b
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : B_id ?tid ; AF_typedef ?tid ?dclist \<in> set ?\<Theta>;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?cs : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f MATCH ?v WITH { ?cs } : ?b
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; (?x, b_of ?\<tau>, TRUE) #\<^sub>\<Gamma> ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b ; atom ?x \<sharp> (?\<Phi>, ?\<Theta>, ?\<B>, ?\<Gamma>, ?\<Delta>, ?\<Gamma>, ?\<tau>);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?\<tau> \<turnstile>\<^sub>w\<^sub>f  ?dc ?x \<Rightarrow> ?s  : ?b
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; [(?dc, ?t)] \<turnstile>\<^sub>w\<^sub>f { ?cs } : ?b
\<lbrakk> ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b ;  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; (?dc, ?t) # ?dclist \<turnstile>\<^sub>w\<^sub>f  ?cs | ?css   : ?b
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau> ; ?u \<notin> fst ` setD ?\<Delta>\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f (?u, ?\<tau>) #\<^sub>\<Delta> ?\<Delta>
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f []
\<lbrakk>?f \<notin> name_of_fun ` set ?\<Phi>;  ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f ?ft ;  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> \<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f AF_fundef ?f ?ft # ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; {||} \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow>  ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f AF_fun_typ_none ?ft
 ?\<Theta> ; ?\<Phi> ; {|?bv|} \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow>  ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f AF_fun_typ_some ?bv ?ft
\<lbrakk> ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?b ; supp ?s \<subseteq> {atom ?x} \<union> supp ?B; supp ?c \<subseteq> {atom ?x};  ?\<Theta> ; ?B ; (?x, ?b, ?c) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f ?\<tau> ;  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?B \<turnstile>\<^sub>w\<^sub>f AF_fun_typ ?x ?b ?c ?\<tau> ?s
 ?\<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>
(B_int = B_int) = True
(B_bool = B_bool) = True
(B_id ?list = B_id ?lista) = (?list = ?lista)
([ ?b1.0 , ?b2.0 ]\<^sup>b = [ ?b1a , ?b2a ]\<^sup>b) = (?b1.0 = ?b1a \<and> ?b2.0 = ?b2a)
(B_unit = B_unit) = True
(B_bitvec = B_bitvec) = True
(B_var ?bv = B_var ?bva) = (?bv = ?bva)
(B_app ?list ?b = B_app ?lista ?ba) = (?list = ?lista \<and> ?b = ?ba)
?a \<sharp> GNil
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : ?b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : ?b ;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ; atom ?x \<sharp> ?\<Gamma>\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; (?x, ?b, [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  ?e1.0 ) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  ?e2.0
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?x ]\<^sup>v : ?b ; \<And>c. \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; Some (?b, c) = lookup ?\<Gamma> ?x\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : ?b ; \<lbrakk>?b = base_for_lit ?l;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 , ?v2.0 ]\<^sup>v : ?b ; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b1 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?tyid ?dc ?v : ?b ; \<And>dclist x b' c. \<lbrakk>?b = B_id ?tyid; AF_typedef ?tyid dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b' \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp ?tyid ?dc ?b ?v : ?b' ; \<And>bv dclist x b' c. \<lbrakk>?b' = B_app ?tyid ?b; AF_typedef_poly ?tyid bv dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; atom bv \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>, ?b, ?v);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b'[bv::=?b]\<^sub>b\<^sub>b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1.  P ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
 P ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2

goal (1 subgoal):
 1. \<forall>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2
[PROOF STEP]
show \<open>\<forall>i.  ((P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i) \<and>  (i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil)  \<longrightarrow>
             (i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2)) \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2
[PROOF STEP]
proof(rule+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
assume as:"P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil"
[PROOF STATE]
proof (state)
this:
 P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil

goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
have *: "P ; GNil \<turnstile> i "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P ; GNil \<turnstile> i
[PROOF STEP]
using wfI_def
[PROOF STATE]
proof (prove)
using this:
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)

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

goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; GNil \<turnstile> i
[PROOF STEP]
obtain s1 where s1:"eval_e i e1 s1"
[PROOF STATE]
proof (prove)
using this:
 P ; GNil \<turnstile> i

goal (1 subgoal):
 1. (\<And>s1. i \<lbrakk> e1 \<rbrakk> ~ s1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms eval_e_exist
[PROOF STATE]
proof (prove)
using this:
 P ; GNil \<turnstile> i
\<forall>i s1 s2.  P ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  P ; GNil \<turnstile> i \<and> i \<lbrakk> e1 \<rbrakk> ~ s1  \<and> i \<lbrakk> e2 \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
  P ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f e1 : b
  P ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f e2 : 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>s1. i \<lbrakk> e1 \<rbrakk> ~ s1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> e1 \<rbrakk> ~ s1

goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
obtain s2 where s2:"eval_e i e2 s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2. i \<lbrakk> e2 \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms eval_e_exist  *
[PROOF STATE]
proof (prove)
using this:
\<forall>i s1 s2.  P ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  P ; GNil \<turnstile> i \<and> i \<lbrakk> e1 \<rbrakk> ~ s1  \<and> i \<lbrakk> e2 \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
  P ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f e1 : b
  P ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f e2 : 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
 P ; GNil \<turnstile> i

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

goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> e2 \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
have "i x = Some s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i x = Some s1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i x = Some s1
[PROOF STEP]
have "i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1
[PROOF STEP]
using as is_satis_g.simps
[PROOF STATE]
proof (prove)
using this:
 P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )

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

goal (1 subgoal):
 1. i x = Some s1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1

goal (1 subgoal):
 1. i x = Some s1
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1
i \<lbrakk> e1 \<rbrakk> ~ s1

goal (1 subgoal):
 1. i x = Some s1
[PROOF STEP]
by (metis eval_c_elims(7) eval_e_elims(1) eval_e_uniqueness eval_v_elims(2) is_satis.cases)
[PROOF STATE]
proof (state)
this:
i x = Some s1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i x = Some s1

goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i x = Some s1

goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
have "s1 = s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using s1 s2 * assms wfG_nilI wfX_wfY
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e1 \<rbrakk> ~ s1
i \<lbrakk> e2 \<rbrakk> ~ s2
 P ; GNil \<turnstile> i
\<forall>i s1 s2.  P ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil  \<and>  P ; GNil \<turnstile> i \<and> i \<lbrakk> e1 \<rbrakk> ~ s1  \<and> i \<lbrakk> e2 \<rbrakk> ~ s2  \<longrightarrow> s1 = s2
  P ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f e1 : b
  P ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f e2 : b
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil
 ?\<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. s1 = s2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s1 = s2

goal (1 subgoal):
 1. \<And>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> e2 \<rbrakk> ~ s2
i x = Some s1
s1 = s2
[PROOF STEP]
show "i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e2 \<rbrakk> ~ s2
i x = Some s1
s1 = s2

goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
using eval_c.intros eval_e.intros eval_v.intros
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e2 \<rbrakk> ~ s2
i x = Some s1
s1 = s2
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s

goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i \<lbrakk> e2 \<rbrakk> ~ s2 ; i x = Some s1; s1 = s2; \<And>i.  i \<lbrakk> TRUE \<rbrakk> ~ True ; \<And>i.  i \<lbrakk> FALSE \<rbrakk> ~ False ; \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2 ; \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2 ; \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2 ; \<And>i c b.  i \<lbrakk> c \<rbrakk> ~ b  \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b ; \<And>i e1 sv1 e2 sv2. \<lbrakk>i \<lbrakk> e1 \<rbrakk> ~ sv1 ; i \<lbrakk> e2 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2 ; \<And>i v sv. i \<lbrakk> v \<rbrakk> ~ sv  \<Longrightarrow> i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv ; \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2) ; \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2) ; \<And>i v1 s1 v2 s2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2) ; \<And>i v v1 v2. i \<lbrakk> v \<rbrakk> ~ SPair v1 v2  \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1 ; \<And>i v v1 v2. i \<lbrakk> v \<rbrakk> ~ SPair v1 v2  \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2 ; \<And>i v1 bv1 v2 bv2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2) ; \<And>i v bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv  \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv)) ; \<And>i l. i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>  ; \<And>sv i x. Some sv = i x \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ sv ; \<And>i v1 s1 v2 s2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 ; \<And>i v s tyid dc. i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s ; \<And>i v s tyid dc b. i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s \<rbrakk> \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk> e2 \<rbrakk> ~ s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> e2 \<rbrakk> ~ s1
[PROOF STEP]
by (metis \<open>s1 = s2\<close> s2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> e2 \<rbrakk> ~ s1

goal (1 subgoal):
 1. \<lbrakk>i \<lbrakk> e2 \<rbrakk> ~ s2 ; i x = Some s1; s1 = s2; \<And>i.  i \<lbrakk> TRUE \<rbrakk> ~ True ; \<And>i.  i \<lbrakk> FALSE \<rbrakk> ~ False ; \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2 ; \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2 ; \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2 ; \<And>i c b.  i \<lbrakk> c \<rbrakk> ~ b  \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b ; \<And>i e1 sv1 e2 sv2. \<lbrakk>i \<lbrakk> e1 \<rbrakk> ~ sv1 ; i \<lbrakk> e2 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2 ; \<And>i v sv. i \<lbrakk> v \<rbrakk> ~ sv  \<Longrightarrow> i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv ; \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2) ; \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2) ; \<And>i v1 s1 v2 s2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2) ; \<And>i v v1 v2. i \<lbrakk> v \<rbrakk> ~ SPair v1 v2  \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1 ; \<And>i v v1 v2. i \<lbrakk> v \<rbrakk> ~ SPair v1 v2  \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2 ; \<And>i v1 bv1 v2 bv2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2) ; \<And>i v bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv  \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv)) ; \<And>i l. i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>  ; \<And>sv i x. Some sv = i x \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ sv ; \<And>i v1 s1 v2 s2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 ; \<And>i v s tyid dc. i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s ; \<And>i v s tyid dc b. i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s \<rbrakk> \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
(* 0.0 ms *)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> e2 \<rbrakk> ~ s1

goal (1 subgoal):
 1. \<lbrakk>i \<lbrakk> e2 \<rbrakk> ~ s2 ; i x = Some s1; s1 = s2; \<And>i.  i \<lbrakk> TRUE \<rbrakk> ~ True ; \<And>i.  i \<lbrakk> FALSE \<rbrakk> ~ False ; \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2 ; \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2 ; \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2 ; \<And>i c b.  i \<lbrakk> c \<rbrakk> ~ b  \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b ; \<And>i e1 sv1 e2 sv2. \<lbrakk>i \<lbrakk> e1 \<rbrakk> ~ sv1 ; i \<lbrakk> e2 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2 ; \<And>i v sv. i \<lbrakk> v \<rbrakk> ~ sv  \<Longrightarrow> i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv ; \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2) ; \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2) ; \<And>i v1 s1 v2 s2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2) ; \<And>i v v1 v2. i \<lbrakk> v \<rbrakk> ~ SPair v1 v2  \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1 ; \<And>i v v1 v2. i \<lbrakk> v \<rbrakk> ~ SPair v1 v2  \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2 ; \<And>i v1 bv1 v2 bv2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2) ; \<And>i v bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv  \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv)) ; \<And>i l. i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>  ; \<And>sv i x. Some sv = i x \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ sv ; \<And>i v1 s1 v2 s2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 ; \<And>i v s tyid dc. i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s ; \<And>i v s tyid dc b. i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s \<rbrakk> \<Longrightarrow>  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> e2 \<rbrakk> ~ s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e2 \<rbrakk> ~ s1

goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True
[PROOF STEP]
by (metis (full_types) \<open>i x = Some s1\<close> eval_c_eqI eval_e_valI eval_v_varI)
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True

goal:
No subgoals!
[PROOF STEP]
(* 31 ms *)
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2  \<rbrakk> ~ True

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e1 ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  e2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_len:
  assumes " \<turnstile>\<^sub>w\<^sub>f \<Theta>"
  shows  "\<Theta> ; \<B> ; (x, B_int, [[x]\<^sup>v]\<^sup>c\<^sup>e  ==  [[ L_num (int (length v)) ]\<^sup>v]\<^sup>c\<^sup>e) #\<^sub>\<Gamma> GNil  \<Turnstile> [[x]\<^sup>v]\<^sup>c\<^sup>e  ==  CE_len [[ L_bitvec v ]\<^sup>v]\<^sup>c\<^sup>e"  (is "\<Theta> ; \<B> ; ?G \<Turnstile> ?c" )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^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_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
have *:"\<Theta>  \<turnstile>\<^sub>w\<^sub>f ([]::\<Phi>)  \<and>  \<Theta> ; \<B> ; GNil  \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile>\<^sub>w\<^sub>f []  \<and>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>
[PROOF STEP]
using assms wfG_nilI wfD_emptyI wfPhi_emptyI
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f []

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

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 \<Theta>  \<turnstile>\<^sub>w\<^sub>f []  \<and>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
hence "\<Theta>  ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f CE_val (V_lit (L_num (int (length v)))) : B_int"
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile>\<^sub>w\<^sub>f []  \<and>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>

goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e : B_int
[PROOF STEP]
using wfCE_valI * wfV_litI base_for_lit.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile>\<^sub>w\<^sub>f []  \<and>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>
 ?\<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>  \<turnstile>\<^sub>w\<^sub>f []  \<and>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
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> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e : B_int
[PROOF STEP]
by (metis wfE_valI wfX_wfY)
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e : B_int

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e : B_int

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
have "\<Theta>  ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f CE_len [(V_lit (L_bitvec v))]\<^sup>c\<^sup>e : B_int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.   \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e : B_int
[PROOF STEP]
using wfE_valI * wfV_litI base_for_lit.simps  wfE_valI wfX_wfY wfCE_valI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>e : ?b
 \<Theta>  \<turnstile>\<^sub>w\<^sub>f []  \<and>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
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
\<lbrakk> ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta> ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>e : ?b
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f b_of ?\<tau>
 ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> True
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ce : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?td  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f ?ftq  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<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 [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e : B_int
[PROOF STEP]
by (metis wfCE_lenI)
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e : B_int

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e : B_int

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
have "atom x \<sharp> GNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> GNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> GNil

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 \<Theta>  \<turnstile>\<^sub>w\<^sub>f []  \<and>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e : B_int
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e : B_int
atom x \<sharp> GNil
[PROOF STEP]
have "\<Theta> ; \<B> ; ?G \<turnstile>\<^sub>w\<^sub>f ?c"
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile>\<^sub>w\<^sub>f []  \<and>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e : B_int
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e : B_int
atom x \<sharp> GNil

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
using wfC_e_eq2 assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile>\<^sub>w\<^sub>f []  \<and>  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f []\<^sub>\<Delta>
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e : B_int
  \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e : B_int
atom x \<sharp> GNil
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : ?b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : ?b ;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ; atom ?x \<sharp> ?\<Gamma>\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; (?x, ?b, [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  ?e1.0 ) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  ?e2.0
   \<turnstile>\<^sub>w\<^sub>f \<Theta>

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^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_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
using is_satis_len_imp
[PROOF STATE]
proof (prove)
using this:
 ?i \<Turnstile> [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length ?v)) ]\<^sup>v ]\<^sup>c\<^sup>e   \<Longrightarrow>  ?i \<Turnstile> [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec ?v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e

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

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^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_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
\<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^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_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Theta> ; \<B> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed