[STATEMENT]
lemma valid_eq_imp:
  fixes c1::c and c2::c
  assumes " \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<turnstile>\<^sub>w\<^sub>f c1 IMP c2"
  shows  " \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile>  c1   IMP  c2 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1  IMP  c2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1  IMP  c2
[PROOF STEP]
have "\<forall>i.  (\<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>)  \<longrightarrow>  i \<Turnstile> ( c1  IMP  c2 )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
proof(rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
assume as:"\<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
have "\<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<turnstile>\<^sub>w\<^sub>f c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1
[PROOF STEP]
using wfC_elims assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
 \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  IMP  c2

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1
[PROOF STEP]
obtain sc where "i \<lbrakk> c1 \<rbrakk> ~ sc"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1

goal (1 subgoal):
 1. (\<And>sc.  i \<lbrakk> c1 \<rbrakk> ~ sc  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_c_exist assms as
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c \<rbrakk> \<Longrightarrow> \<exists>s.  ?i \<lbrakk> ?c \<rbrakk> ~ s
 \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  IMP  c2
 \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>

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

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1 \<rbrakk> ~ sc

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
have  "i \<lbrakk> c2 \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> c2 \<rbrakk> ~ True
[PROOF STEP]
using as is_satis_g.simps is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>
 ?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> c2 \<rbrakk> ~ True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c2 \<rbrakk> ~ True

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c1 \<rbrakk> ~ sc
 i \<lbrakk> c2 \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk> c1  IMP  c2 \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1 \<rbrakk> ~ sc
 i \<lbrakk> c2 \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ True
[PROOF STEP]
using eval_c_impI
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1 \<rbrakk> ~ sc
 i \<lbrakk> c2 \<rbrakk> ~ True
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0

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

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
thus  "i \<Turnstile> c1  IMP  c2"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
using is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ True
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> c1  IMP  c2

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1  IMP  c2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> c1  IMP  c2

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1  IMP  c2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i.  \<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> c1  IMP  c2
 \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  IMP  c2

goal (1 subgoal):
 1. \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1  IMP  c2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> c1  IMP  c2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_range:
  assumes "0 \<le> n \<and> n \<le> m" and "\<turnstile>\<^sub>w\<^sub>f \<Theta>"
  shows "\<Theta> ; {||} ; (x, B_int  , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #\<^sub>\<Gamma>  GNil \<Turnstile>
                              (C_eq (CE_op LEq (CE_val (V_var x)) (CE_val (V_lit (L_num m))))  [[ L_true ]\<^sup>v ]\<^sup>c\<^sup>e) AND
                             (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x)))  [[ L_true ]\<^sup>v ]\<^sup>c\<^sup>e)"
    (is "\<Theta> ; {||} ; ?G \<Turnstile> ?c1 AND ?c2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule validI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
 2. \<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have wfg: " \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
[PROOF STEP]
using assms base_for_lit.simps wfG_nilI wfV_litI fresh_GNil wfB_intI wfC_v_eq wfG_cons1I wfG_cons2I
[PROOF STATE]
proof (prove)
using this:
0 \<le> n \<and> n \<le> m
   \<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
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
?a \<sharp> GNil
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f B_int
\<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
\<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>

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

goal (2 subgoals):
 1.  \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
 2. \<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^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> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
using wfC_conjI wfC_eqI wfCE_leqI wfCE_valI wfV_varI wfg lookup.simps base_for_lit.simps wfV_litI wfB_intI wfB_boolI
[PROOF STATE]
proof (prove)
using this:
\<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 ?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
\<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
 ?\<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>  \<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> ; {||}  \<turnstile>\<^sub>w\<^sub>f (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^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
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
   \<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

goal (1 subgoal):
 1.  \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^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> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
assume a:"\<Theta> ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
hence *:"i \<lbrakk> V_var x \<rbrakk> ~ SNum n"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil

goal (1 subgoal):
 1. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
obtain sv where sv: "i x = Some sv \<and> \<Theta> \<turnstile> sv : B_int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sv. i x = Some sv \<and>  \<Theta>  \<turnstile> sv : B_int \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a wfI_def
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)

goal (1 subgoal):
 1. (\<And>sv. i x = Some sv \<and>  \<Theta>  \<turnstile> sv : B_int \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
i x = Some sv \<and>  \<Theta>  \<turnstile> sv : B_int

goal (1 subgoal):
 1.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
have "i \<lbrakk>  (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n)))) \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using a is_satis_g.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^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 )

goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using is_satis.cases
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^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 )
\<lbrakk> ?a1.0 \<Turnstile> ?a2.0 ; \<And>i c. \<lbrakk>?a1.0 = i; ?a2.0 = c;  i \<lbrakk> c \<rbrakk> ~ True \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
hence "i x = Some(SNum n)"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1. i x = Some (SNum n)
[PROOF STEP]
using sv
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
i x = Some sv \<and>  \<Theta>  \<turnstile> sv : B_int

goal (1 subgoal):
 1. i x = Some (SNum n)
[PROOF STEP]
by (metis eval_c_elims(7) eval_e_elims(1) eval_l.simps(3) eval_v_elims(1) eval_v_elims(2))
[PROOF STATE]
proof (state)
this:
i x = Some (SNum n)

goal (1 subgoal):
 1.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i x = Some (SNum n)

goal (1 subgoal):
 1. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
using eval_v_varI
[PROOF STATE]
proof (prove)
using this:
i x = Some (SNum n)
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<Longrightarrow>  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
show "i \<Turnstile> ?c1 AND ?c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have "i \<lbrakk> ?c1 \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e\<rbrakk> ~ SBool True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
using eval_e_leqI assms eval_v_litI eval_l.simps *
[PROOF STATE]
proof (prove)
using this:
\<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)
0 \<le> n \<and> n \<le> m
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
\<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
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n

goal (1 subgoal):
 1. i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
by (metis (full_types) eval_e_valI)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk>  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ SBool True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
using eval_v_litI eval_e_valI eval_l.simps
[PROOF STATE]
proof (prove)
using this:
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<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_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using  eval_c_eqI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool 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

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

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

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have "i \<lbrakk> ?c2 \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
using eval_e_leqI assms eval_v_litI eval_l.simps *
[PROOF STATE]
proof (prove)
using this:
\<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)
0 \<le> n \<and> n \<le> m
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
\<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
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n

goal (1 subgoal):
 1. i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
by (metis (full_types) eval_e_valI)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk>  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ SBool True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
using eval_v_litI eval_e_valI eval_l.simps
[PROOF STATE]
proof (prove)
using this:
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<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_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using  eval_c_eqI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool 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

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

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

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
 i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
 i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
using eval_c_conjI is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
 i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil  \<longrightarrow>  i \<Turnstile> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_range_length:
  fixes \<Gamma>::\<Gamma>
  assumes "0 \<le> n \<and> n \<le> int (length v)" and " \<Theta> ; {||} \<turnstile>\<^sub>w\<^sub>f \<Gamma>" and "atom x \<sharp> \<Gamma>"
  shows "\<Theta> ; {||} ; (x, B_int  , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #\<^sub>\<Gamma>  \<Gamma> \<Turnstile>
                     (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x)))  [[ L_true ]\<^sup>v ]\<^sup>c\<^sup>e) AND
                     (C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ))  [[ L_true ]\<^sup>v ]\<^sup>c\<^sup>e)
                            "
    (is "\<Theta> ; {||} ; ?G \<Turnstile> ?c1 AND ?c2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule validI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
 2. \<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have wfg: " \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>
[PROOF STEP]
apply(rule  wfG_cons1I)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. ([ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) \<notin> {TRUE, FALSE}
 2.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 3. atom x \<sharp> \<Gamma>
 4.  \<Theta> ; {||} ; (x, B_int, TRUE) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
 5.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f B_int
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 2. atom x \<sharp> \<Gamma>
 3.  \<Theta> ; {||} ; (x, B_int, TRUE) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
 4.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f B_int
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> n \<and> n \<le> int (length v)
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>

goal (4 subgoals):
 1.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
 2. atom x \<sharp> \<Gamma>
 3.  \<Theta> ; {||} ; (x, B_int, TRUE) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
 4.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f B_int
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1.  \<Theta> ; {||} ; (x, B_int, TRUE) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
 2.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f B_int
[PROOF STEP]
using assms base_for_lit.simps wfG_nilI wfV_litI  wfB_intI wfC_v_eq  wfB_intI wfX_wfY assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> n \<and> n \<le> int (length v)
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>
base_for_lit L_true = B_bool
base_for_lit L_false = B_bool
base_for_lit (L_num ?n) = B_int
base_for_lit L_unit = B_unit
base_for_lit (L_bitvec ?v) = B_bitvec
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f B_int
\<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
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f B_int
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f b_of ?\<tau>
 ?\<Theta> ; ?\<B>  ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ts  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> True
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?ce : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> \<turnstile>\<^sub>w\<^sub>f ?td  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?e : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> \<turnstile>\<^sub>w\<^sub>f ?s : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dc ; ?t \<turnstile>\<^sub>w\<^sub>f ?cs : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta> ; ?\<Phi> ; ?\<B> ; ?\<Gamma> ; ?\<Delta> ; ?tid ; ?dclist \<turnstile>\<^sub>w\<^sub>f ?css : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<and>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>
 ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?\<Delta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta>  ; ?\<Phi> \<turnstile>\<^sub>w\<^sub>f ?ftq  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
 ?\<Theta> ; ?\<Phi> ; ?\<B> \<turnstile>\<^sub>w\<^sub>f ?ft  \<Longrightarrow>  ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f ?\<Phi>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
0 \<le> n \<and> n \<le> int (length v)
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>

goal (2 subgoals):
 1.  \<Theta> ; {||} ; (x, B_int, TRUE) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e
 2.  \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f B_int
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>

goal (2 subgoals):
 1.  \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
 2. \<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^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> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
using wfC_conjI wfC_eqI wfCE_leqI wfCE_valI wfV_varI wfg lookup.simps base_for_lit.simps wfV_litI wfB_intI wfB_boolI
[PROOF STATE]
proof (prove)
using this:
\<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 ?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
\<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
 ?\<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>  \<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> ; {||}  \<turnstile>\<^sub>w\<^sub>f (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>
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
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : base_for_lit ?l
   \<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

goal (1 subgoal):
 1.  \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
by (metis (full_types) wfCE_lenI)
[PROOF STATE]
proof (state)
this:
 \<Theta> ; {||} ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e

goal (1 subgoal):
 1. \<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^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> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
proof(rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
assume a:"\<Theta> ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G"
[PROOF STATE]
proof (state)
this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
hence *:"i \<lbrakk> V_var x \<rbrakk> ~ SNum n"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>

goal (1 subgoal):
 1. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
obtain sv where sv: "i x = Some sv \<and> \<Theta> \<turnstile> sv : B_int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sv. i x = Some sv \<and>  \<Theta>  \<turnstile> sv : B_int \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a wfI_def
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)

goal (1 subgoal):
 1. (\<And>sv. i x = Some sv \<and>  \<Theta>  \<turnstile> sv : B_int \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
i x = Some sv \<and>  \<Theta>  \<turnstile> sv : B_int

goal (1 subgoal):
 1.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
have "i \<lbrakk>  (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n)))) \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using a is_satis_g.simps
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )

goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using is_satis.cases
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )
\<lbrakk> ?a1.0 \<Turnstile> ?a2.0 ; \<And>i c. \<lbrakk>?a1.0 = i; ?a2.0 = c;  i \<lbrakk> c \<rbrakk> ~ True \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
hence "i x = Some(SNum n)"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1. i x = Some (SNum n)
[PROOF STEP]
using sv
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
i x = Some sv \<and>  \<Theta>  \<turnstile> sv : B_int

goal (1 subgoal):
 1. i x = Some (SNum n)
[PROOF STEP]
by (metis eval_c_elims(7) eval_e_elims(1) eval_l.simps(3) eval_v_elims(1) eval_v_elims(2))
[PROOF STATE]
proof (state)
this:
i x = Some (SNum n)

goal (1 subgoal):
 1.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i x = Some (SNum n)

goal (1 subgoal):
 1. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n
[PROOF STEP]
using eval_v_varI
[PROOF STATE]
proof (prove)
using this:
i x = Some (SNum n)
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n

goal (1 subgoal):
 1. \<And>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<Longrightarrow>  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
show "i \<Turnstile> ?c1 AND ?c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have "i \<lbrakk> ?c2 \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e\<rbrakk> ~ SBool True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
using eval_e_leqI assms eval_v_litI eval_l.simps *
[PROOF STATE]
proof (prove)
using this:
\<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)
0 \<le> n \<and> n \<le> int (length v)
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
\<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
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n

goal (1 subgoal):
 1. i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
by (metis (full_types) eval_e_lenI eval_e_valI)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk>  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ SBool True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
using eval_v_litI eval_e_valI eval_l.simps
[PROOF STATE]
proof (prove)
using this:
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<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_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using  eval_c_eqI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool 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

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

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

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
have "i \<lbrakk> ?c1 \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
using eval_e_leqI assms eval_v_litI eval_l.simps *
[PROOF STATE]
proof (prove)
using this:
\<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)
0 \<le> n \<and> n \<le> int (length v)
 \<Theta> ; {||}  \<turnstile>\<^sub>w\<^sub>f \<Gamma>
atom x \<sharp> \<Gamma>
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
\<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
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n

goal (1 subgoal):
 1. i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
by (metis (full_types) eval_e_valI)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have "i \<lbrakk>  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ SBool True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
using eval_v_litI eval_e_valI eval_l.simps
[PROOF STATE]
proof (prove)
using this:
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<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_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using  eval_c_eqI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool True
i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool 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

goal (1 subgoal):
 1.  i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

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

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
 i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
 i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
using eval_c_conjI is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
 i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i.  \<Theta> ; (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and>  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>  \<longrightarrow>  i \<Turnstile> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed