[STATEMENT]
lemma valid_split:
  assumes "split n v (v1,v2)" and "\<turnstile>\<^sub>w\<^sub>f \<Theta>"
  shows "\<Theta> ; {||} ; (z , [B_bitvec , B_bitvec ]\<^sup>b ,  [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec  v1 ]\<^sup>v , [ L_bitvec  v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e) #\<^sub>\<Gamma> GNil
\<Turnstile>  ([ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e)   AND  ([| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e)"
    (is "\<Theta> ;  {||} ;  ?G \<Turnstile> ?c1 AND ?c2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
unfolding valid.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e    \<and> (\<forall>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e   )
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
 2. \<forall>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have wfg: " \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (z, [B_bitvec , B_bitvec ]\<^sup>b ,  [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec  v1 ]\<^sup>v , [ L_bitvec  v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e) #\<^sub>\<Gamma> GNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
[PROOF STEP]
using wf_intros assms base_for_lit.simps  fresh_GNil wfC_v_eq  wfG_intros2
[PROOF STATE]
proof (prove)
using this:
   \<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
split n v (v1, v2)
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
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
?a \<sharp> GNil
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ; atom ?x \<sharp> ?\<Gamma>\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ ?v ]\<^sup>c\<^sup>e
 ?P ; ?\<B> ; (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?P ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>

goal (1 subgoal):
 1.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil

goal (2 subgoals):
 1.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
 2. \<forall>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
show "\<Theta> ; {||} ; ?G  \<turnstile>\<^sub>w\<^sub>f ?c1 AND ?c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
apply(rule wfC_conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
 2.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
apply(rule wfC_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1.   \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e : ?b3
 2.   \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : ?b3
 3.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
apply(rule wfCE_valI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f [ L_bitvec v ]\<^sup>v : ?b3
 2.   \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : ?b3
 3.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
apply(rule wfV_litI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
 2.   \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : base_for_lit (L_bitvec v)
 3.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
using wf_intros wfg lookup.simps base_for_lit.simps wfC_v_eq
[PROOF STATE]
proof (prove)
using this:
   \<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> ; {||}  \<turnstile>\<^sub>w\<^sub>f (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
lookup GNil ?x = None
lookup ((?x, ?b, ?c) #\<^sub>\<Gamma> ?G) ?y = (if ?x = ?y then Some (?b, ?c) else lookup ?G ?y)
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> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ; atom ?x \<sharp> ?\<Gamma>\<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ ?x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ ?v ]\<^sup>c\<^sup>e

goal (3 subgoals):
 1.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
 2.   \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e : base_for_lit (L_bitvec v)
 3.  \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
apply (metis )+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
 \<Theta> ; {||} ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have len:"int (length v1) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (length v1) = n
[PROOF STEP]
using assms split_length
[PROOF STATE]
proof (prove)
using this:
split n v (v1, v2)
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
split ?n ?v (?v1.0, ?v2.0) \<Longrightarrow> ?n = int (length ?v1.0)

goal (1 subgoal):
 1. int (length v1) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (length v1) = n

goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
show "\<forall>i. \<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G \<longrightarrow> i \<Turnstile> (?c1 AND ?c2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
assume a:"\<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
hence "i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil

goal (1 subgoal):
 1.  i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using is_satis_g.simps is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
obtain sv where "i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv \<and> i \<lbrakk>  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1. (\<And>sv. i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_c_elims
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
\<lbrakk> ?i \<lbrakk> TRUE \<rbrakk> ~ True ; ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> FALSE \<rbrakk> ~ False ; ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<and> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<or> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<longrightarrow> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ ?s ; \<And>b. \<lbrakk>?s = (\<not> b);  ?i \<lbrakk> ?c \<rbrakk> ~ b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?s ; \<And>sv1 sv2. \<lbrakk>?s = (sv1 = sv2); ?i \<lbrakk> ?e1.0 \<rbrakk> ~ sv1 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> TRUE \<rbrakk> ~ ?s ; ?s \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> FALSE \<rbrakk> ~ ?s ; \<not> ?s \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>sv. i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
hence "i  \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ (SPair (SBitvec v1) (SBitvec v2))"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv

goal (1 subgoal):
 1. i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SPair (SBitvec v1) (SBitvec v2)
[PROOF STEP]
using eval_c_eqI eval_v.intros eval_l.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv  \<and> i \<lbrakk> [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv
\<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> [ ?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
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SPair (SBitvec v1) (SBitvec v2)
[PROOF STEP]
by (metis eval_e_elims(1) eval_v_uniqueness)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SPair (SBitvec v1) (SBitvec v2)

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
hence b:"i z = Some (SPair (SBitvec v1) (SBitvec v2))"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SPair (SBitvec v1) (SBitvec v2)

goal (1 subgoal):
 1. i z = Some (SPair (SBitvec v1) (SBitvec v2))
[PROOF STEP]
using a eval_e_elims eval_v_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SPair (SBitvec v1) (SBitvec v2)
 \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
\<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
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. i z = Some (SPair (SBitvec v1) (SBitvec v2))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i z = Some (SPair (SBitvec v1) (SBitvec v2))

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have v1: "i \<lbrakk> [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v1 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v1
[PROOF STEP]
using eval_e_fstI eval_e_valI eval_v_varI b
[PROOF STATE]
proof (prove)
using this:
?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> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
i z = Some (SPair (SBitvec v1) (SBitvec v2))

goal (1 subgoal):
 1. i \<lbrakk> [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v1

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have v2: "i \<lbrakk> [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v2
[PROOF STEP]
using eval_e_sndI eval_e_valI eval_v_varI b
[PROOF STATE]
proof (prove)
using this:
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
i z = Some (SPair (SBitvec v1) (SBitvec v2))

goal (1 subgoal):
 1. i \<lbrakk> [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v2

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have "i \<lbrakk> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v
[PROOF STEP]
using eval_e.intros eval_v.intros eval_l.simps
[PROOF STATE]
proof (prove)
using this:
?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
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

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

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have "i \<lbrakk>  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  \<rbrakk> ~ SBitvec v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v
[PROOF STEP]
using assms split_concat v1 v2 eval_e_concatI
[PROOF STATE]
proof (prove)
using this:
split n v (v1, v2)
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
split ?n ?v (?v1.0, ?v2.0) \<Longrightarrow> ?v = ?v1.0 @ ?v2.0
i \<lbrakk> [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v1
i \<lbrakk> [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v2
\<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)

goal (1 subgoal):
 1. i \<lbrakk> [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have "i \<lbrakk>  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v1))
[PROOF STEP]
using v1 eval_e_lenI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v1
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))

goal (1 subgoal):
 1. i \<lbrakk> [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v1))

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v1))

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have "i \<lbrakk>  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ SNum n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n
[PROOF STEP]
using eval_e.intros eval_v.intros eval_l.simps
[PROOF STATE]
proof (prove)
using this:
?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
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. i \<lbrakk> [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v
i \<lbrakk> [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v
i \<lbrakk> [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v1))
i \<lbrakk> [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n
[PROOF STEP]
show  "i \<Turnstile> ?c1 AND ?c2"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v
i \<lbrakk> [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v
i \<lbrakk> [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v1))
i \<lbrakk> [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n

goal (1 subgoal):
 1.  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
using is_satis.intros eval_c_conj2I eval_c_eqI len
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v
i \<lbrakk> [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v
i \<lbrakk> [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v1))
i \<lbrakk> [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n
 ?i \<lbrakk> ?c \<rbrakk> ~ True  \<Longrightarrow>  ?i \<Turnstile> ?c
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ True ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ True \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ True
\<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
int (length v1) = n

goal (1 subgoal):
 1.  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (z, [ B_bitvec , B_bitvec ]\<^sup>b, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_eq:
  assumes "wfI \<Theta> G i" and "wfCE \<Theta> \<B> G e b"
  shows "is_satis i (e == e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> e  ==  e
[PROOF STEP]
proof(rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<lbrakk> e  ==  e  \<rbrakk> ~ True
[PROOF STEP]
obtain s where "eval_e i e s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> e \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_e_exist assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;   ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?e \<rbrakk> ~ s
 \<Theta> ; G \<turnstile> i
  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f e : b

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

goal (1 subgoal):
 1.  i \<lbrakk> e  ==  e  \<rbrakk> ~ True
[PROOF STEP]
thus "eval_c i (e  ==  e ) True"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e \<rbrakk> ~ s

goal (1 subgoal):
 1.  i \<lbrakk> e  ==  e  \<rbrakk> ~ True
[PROOF STEP]
using eval_c_eqI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e \<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> e  ==  e  \<rbrakk> ~ True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> e  ==  e  \<rbrakk> ~ True

goal:
No subgoals!
[PROOF STEP]
qed