[STATEMENT]
lemma valid_range_length_inv_gnil:
  fixes \<Gamma>::\<Gamma>
  assumes  "\<turnstile>\<^sub>w\<^sub>f \<Theta> "
    and  "\<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_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")
  shows "0 \<le> n \<and> n \<le> int (length v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
have *:"\<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 [ [ 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 assms valid.simps
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
\<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 [ [ 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
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))

goal (1 subgoal):
 1. \<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 [ [ 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 simp
[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 [ [ 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. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
obtain i where i: "i x = Some (SNum n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i x = Some (SNum n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i x = Some (SNum n)

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
have "\<Theta> ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G"
[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> 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
[PROOF STEP]
proof
[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> i
 2.  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
[PROOF STEP]
show  "\<Theta> ; ?G \<turnstile> i"
[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> i
[PROOF STEP]
unfolding wfI_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
using wfRCV_BIntI i *
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SNum ?n : B_int
i x = Some (SNum n)
\<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 [ [ 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>(x, b, c)\<in>toSet ((x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
by auto
[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

goal (1 subgoal):
 1.  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
[PROOF STEP]
have "i \<lbrakk> ([ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e )  \<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 * eval_c.intros(7) eval_e.intros eval_v.intros  eval_l.simps
[PROOF STATE]
proof (prove)
using 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 [ [ 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
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s
\<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> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
by (metis (full_types) i)
[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.  i \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
[PROOF STEP]
thus  "i \<Turnstile> ?G"
[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 \<Turnstile> (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil
[PROOF STEP]
unfolding  is_satis_g.simps is_satis.simps
[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. (\<exists>ia c. i = ia \<and> ([ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) = c \<and>  ia \<lbrakk> c \<rbrakk> ~ True ) \<and> True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 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:
No subgoals!
[PROOF STEP]
qed
[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. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
hence **:"i \<Turnstile> ?c1 AND ?c2"
[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 \<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 *
[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
\<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 [ [ 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.  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 auto
[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 (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
hence  1: "i \<lbrakk> ?c1 \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
using 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 (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_elims(3) is_satis.simps
[PROOF STATE]
proof (prove)
using 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
\<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
 ?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> [ 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 fastforce
[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. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
then
[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  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
obtain sv1 and sv2 where "(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1 \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk>  ~ sv2"
[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  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1. (\<And>sv1 sv2. (sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_c_elims(7)
[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  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
\<lbrakk> ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?s ; \<And>sv1 sv2. \<lbrakk>?s = (sv1 = sv2); ?i \<lbrakk> ?e1.0 \<rbrakk> ~ sv1 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
hence "sv1 = SBool True"
[PROOF STATE]
proof (prove)
using this:
(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2

goal (1 subgoal):
 1. sv1 = SBool True
[PROOF STEP]
using eval_e_elims eval_v_elims eval_l.simps i
[PROOF STATE]
proof (prove)
using this:
(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2
\<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
\<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 x = Some (SNum n)

goal (1 subgoal):
 1. sv1 = SBool True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sv1 = SBool True

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
obtain n1 and n2 where "SBool True = SBool (n1 \<le> n2) \<and> (i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1)  \<and> (i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n1 n2. SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_e_elims(3)[of i " [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e" "[ [ x ]\<^sup>v ]\<^sup>c\<^sup>e "  "SBool True"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>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 ; \<And>n1 n2. \<lbrakk>SBool True = SBool (n1 \<le> n2); i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1 ; i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>n1 n2. SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1 \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2\<close> \<open>sv1 = SBool True\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>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 ; \<And>n1 n2. \<lbrakk>SBool True = SBool (n1 \<le> n2); i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1 ; i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2
sv1 = SBool True

goal (1 subgoal):
 1. (\<And>n1 n2. SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
hence "n1 = 0" and "n2 = n"
[PROOF STATE]
proof (prove)
using this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2

goal (1 subgoal):
 1. n1 = 0 &&& n2 = n
[PROOF STEP]
using eval_e_elims eval_v_elims i
[PROOF STATE]
proof (prove)
using this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2
\<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
i x = Some (SNum n)

goal (1 subgoal):
 1. n1 = 0 &&& n2 = n
[PROOF STEP]
apply (metis eval_l.simps(3) rcl_val.eq_iff(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n2 = n
[PROOF STEP]
using eval_e_elims eval_v_elims i
[PROOF STATE]
proof (prove)
using this:
\<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
i x = Some (SNum n)

goal (1 subgoal):
 1. n2 = n
[PROOF STEP]
by (metis calculation option.inject rcl_val.eq_iff(2))
[PROOF STATE]
proof (state)
this:
n1 = 0
n2 = n

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2
n1 = 0
n2 = n
[PROOF STEP]
have  le1: "0 \<le> n "
[PROOF STATE]
proof (prove)
using this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2
n1 = 0
n2 = n

goal (1 subgoal):
 1. 0 \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> n

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
hence  2: "i \<lbrakk> ?c2 \<rbrakk> ~ True"
[PROOF STATE]
proof (prove)
using this:
0 \<le> 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  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using ** eval_c_elims(3) is_satis.simps
[PROOF STATE]
proof (prove)
using this:
0 \<le> n
 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
\<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
 ?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> [ 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 fastforce
[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. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
then
[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
[PROOF STEP]
obtain sv1 and sv2 where sv: "(sv1 = sv2) = True \<and> 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> ~ sv1 \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk>  ~ sv2"
[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

goal (1 subgoal):
 1. (\<And>sv1 sv2. (sv1 = sv2) = True \<and> 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> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_c_elims(7)
[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
\<lbrakk> ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?s ; \<And>sv1 sv2. \<lbrakk>?s = (sv1 = sv2); ?i \<lbrakk> ?e1.0 \<rbrakk> ~ sv1 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>sv1 sv2. (sv1 = sv2) = True \<and> 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> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(sv1 = sv2) = True \<and> 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> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
hence "sv1 = SBool True"
[PROOF STATE]
proof (prove)
using this:
(sv1 = sv2) = True \<and> 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> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2

goal (1 subgoal):
 1. sv1 = SBool True
[PROOF STEP]
using eval_e_elims eval_v_elims eval_l.simps i
[PROOF STATE]
proof (prove)
using this:
(sv1 = sv2) = True \<and> 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> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2
\<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
\<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 x = Some (SNum n)

goal (1 subgoal):
 1. sv1 = SBool True
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sv1 = SBool True

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
obtain n1 and n2 where ***:"SBool True = SBool (n1 \<le> n2) \<and>  (i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1) \<and> (i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  \<rbrakk> ~ SNum n2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n1 n2. SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_e_elims(3)
[PROOF STATE]
proof (prove)
using this:
\<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

goal (1 subgoal):
 1. (\<And>n1 n2. SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sv \<open>sv1 = SBool True\<close>
[PROOF STATE]
proof (prove)
using this:
\<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
(sv1 = sv2) = True \<and> 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> ~ sv1  \<and> i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2
sv1 = SBool True

goal (1 subgoal):
 1. (\<And>n1 n2. SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
hence "n1 = n"
[PROOF STATE]
proof (prove)
using this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2

goal (1 subgoal):
 1. n1 = n
[PROOF STEP]
using eval_e_elims(1)[of i] eval_v_elims(2)[of i x "SNum n1"] i
[PROOF STATE]
proof (prove)
using this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2
\<lbrakk>i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ SNum n1 ; Some (SNum n1) = i x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
i x = Some (SNum n)

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

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n1 = n

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
have "n2 = int (length v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n2 = int (length v)
[PROOF STEP]
using eval_e_elims(8) eval_v_elims(1) eval_l.simps i
[PROOF STATE]
proof (prove)
using this:
\<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> 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 x = Some (SNum n)

goal (1 subgoal):
 1. n2 = int (length v)
[PROOF STEP]
by (metis "***" eval_e_elims(1) rcl_val.eq_iff(1) rcl_val.eq_iff(2))
[PROOF STATE]
proof (state)
this:
n2 = int (length v)

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2
n1 = n
n2 = int (length v)
[PROOF STEP]
have  le2: "n \<le> int (length v) "
[PROOF STATE]
proof (prove)
using this:
SBool True = SBool (n1 \<le> n2) \<and> i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n2
n1 = n
n2 = int (length v)

goal (1 subgoal):
 1. n \<le> int (length v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<le> int (length v)

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
using le1 le2
[PROOF STATE]
proof (prove)
using this:
0 \<le> n
n \<le> int (length v)

goal (1 subgoal):
 1. 0 \<le> n \<and> n \<le> int (length v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> n \<and> n \<le> int (length v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfI_cons:
  fixes i::valuation and \<Gamma>::\<Gamma>
  assumes "i' \<Turnstile> \<Gamma>" and "\<Theta> ; \<Gamma> \<turnstile> i'" and "i = i' ( x \<mapsto> s)" and "\<Theta>  \<turnstile> s : b" and "atom x \<sharp> \<Gamma>"
  shows "\<Theta> ; (x,b,c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i
[PROOF STEP]
unfolding wfI_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
fix x' b' c'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
assume "(x',b',c') \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)"
[PROOF STATE]
proof (state)
this:
(x', b', c') \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)

goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x', b', c') \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)
[PROOF STEP]
consider "(x',b',c') = (x,b,c)" | "(x',b',c') \<in> toSet \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
(x', b', c') \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)

goal (1 subgoal):
 1. \<lbrakk>(x', b', c') = (x, b, c) \<Longrightarrow> thesis; (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using toSet.simps
[PROOF STATE]
proof (prove)
using this:
(x', b', c') \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G

goal (1 subgoal):
 1. \<lbrakk>(x', b', c') = (x, b, c) \<Longrightarrow> thesis; (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>(x', b', c') = (x, b, c) \<Longrightarrow> ?thesis; (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(x', b', c') = (x, b, c) \<Longrightarrow> ?thesis; (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have "\<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(x', b', c') = (x, b, c) \<Longrightarrow> ?thesis; (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x', b', c') = (x, b, c) \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
 2. (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
(x', b', c') = (x, b, c)

goal (2 subgoals):
 1. (x', b', c') = (x, b, c) \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
 2. (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x', b', c') = (x, b, c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x', b', c') = (x, b, c)

goal (1 subgoal):
 1. \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x', b', c') = (x, b, c)
 i' \<Turnstile> \<Gamma>
 \<Theta> ; \<Gamma> \<turnstile> i'
i = i'(x \<mapsto> s)
 \<Theta>  \<turnstile> s : b
atom x \<sharp> \<Gamma>

goal (1 subgoal):
 1. \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'

goal (1 subgoal):
 1. (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
(x', b', c') \<in> toSet \<Gamma>

goal (1 subgoal):
 1. (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x', b', c') \<in> toSet \<Gamma>
[PROOF STEP]
obtain s where s:"Some s = i' x' \<and> \<Theta>  \<turnstile> s : b'"
[PROOF STATE]
proof (prove)
using this:
(x', b', c') \<in> toSet \<Gamma>

goal (1 subgoal):
 1. (\<And>s. Some s = i' x' \<and>  \<Theta>  \<turnstile> s : b' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms wfI_def
[PROOF STATE]
proof (prove)
using this:
(x', b', c') \<in> toSet \<Gamma>
 i' \<Turnstile> \<Gamma>
 \<Theta> ; \<Gamma> \<turnstile> i'
i = i'(x \<mapsto> s)
 \<Theta>  \<turnstile> s : b
atom x \<sharp> \<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>s. Some s = i' x' \<and>  \<Theta>  \<turnstile> s : b' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some s = i' x' \<and>  \<Theta>  \<turnstile> s : b'

goal (1 subgoal):
 1. (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Some s = i' x' \<and>  \<Theta>  \<turnstile> s : b'

goal (1 subgoal):
 1. (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
have "x' \<noteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<noteq> x
[PROOF STEP]
using assms 2 fresh_dom_free
[PROOF STATE]
proof (prove)
using this:
 i' \<Turnstile> \<Gamma>
 \<Theta> ; \<Gamma> \<turnstile> i'
i = i'(x \<mapsto> s)
 \<Theta>  \<turnstile> s : b
atom x \<sharp> \<Gamma>
(x', b', c') \<in> toSet \<Gamma>
atom ?x \<sharp> ?\<Gamma> \<Longrightarrow> (?x, ?b, ?c) \<notin> toSet ?\<Gamma>

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

goal (1 subgoal):
 1. (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Some s = i' x' \<and>  \<Theta>  \<turnstile> s : b'
x' \<noteq> x
[PROOF STEP]
have "Some s = i x'"
[PROOF STATE]
proof (prove)
using this:
Some s = i' x' \<and>  \<Theta>  \<turnstile> s : b'
x' \<noteq> x

goal (1 subgoal):
 1. Some s = i x'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Some s = i' x' \<and>  \<Theta>  \<turnstile> s : b'
x' \<noteq> x
 i' \<Turnstile> \<Gamma>
 \<Theta> ; \<Gamma> \<turnstile> i'
i = i'(x \<mapsto> s)
 \<Theta>  \<turnstile> s : b
atom x \<sharp> \<Gamma>

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

goal (1 subgoal):
 1. (x', b', c') \<in> toSet \<Gamma> \<Longrightarrow> \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some s = i x'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Some s = i x'

goal (1 subgoal):
 1. \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
using s  wfI_def
[PROOF STATE]
proof (prove)
using this:
Some s = i x'
Some s = i' x' \<and>  \<Theta>  \<turnstile> s : b'
 ?\<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. \<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s. Some s = i x' \<and>  \<Theta>  \<turnstile> s : b'

goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x'2, ?b'2, ?c'2) \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> \<exists>s. Some s = i ?x'2 \<and>  \<Theta>  \<turnstile> s : ?b'2

goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
thus "\<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b"
[PROOF STATE]
proof (prove)
using this:
(?x'2, ?b'2, ?c'2) \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> \<exists>s. Some s = i ?x'2 \<and>  \<Theta>  \<turnstile> s : ?b'2

goal (1 subgoal):
 1. \<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b

goal:
No subgoals!
[PROOF STEP]
qed