[STATEMENT]
lemma eval_v_exist:
  fixes \<Gamma>::\<Gamma> and v::v and b::b
  assumes "P ; \<Gamma>  \<turnstile> i" and "P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b"
  shows "\<exists>s. i \<lbrakk> v \<rbrakk> ~  s \<and> P \<turnstile> s : b "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
proof(nominal_induct v  arbitrary: b rule:v.strong_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 5. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
case (V_lit x)
[PROOF STATE]
proof (state)
this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b

goal (5 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 5. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using eval_l_base eval_v.intros eval_l.simps wfV_elims rcl_val.supp pure_supp
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
 ?\<Theta>  \<turnstile> \<lbrakk> ?l \<rbrakk>  : base_for_lit ?l
?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
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?x ]\<^sup>v : ?b ; \<And>c. \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; Some (?b, c) = lookup ?\<Gamma> ?x\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : ?b ; \<lbrakk>?b = base_for_lit ?l;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 , ?v2.0 ]\<^sup>v : ?b ; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b1 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?tyid ?dc ?v : ?b ; \<And>dclist x b' c. \<lbrakk>?b = B_id ?tyid; AF_typedef ?tyid dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b' \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp ?tyid ?dc ?b ?v : ?b' ; \<And>bv dclist x b' c. \<lbrakk>?b' = B_app ?tyid ?b; AF_typedef_poly ?tyid bv dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; atom bv \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>, ?b, ?v);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b'[bv::=?b]\<^sub>b\<^sub>b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
supp (SBitvec ?list) = supp ?list
supp (SNum ?int) = supp ?int
supp (SBool ?bool) = supp ?bool
supp (SPair ?rcl_val1.0 ?rcl_val2.0) = supp ?rcl_val1.0 \<union> supp ?rcl_val2.0
supp (SCons ?list1.0 ?list2.0 ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?rcl_val)
supp (SConsp ?list1.0 ?list2.0 ?b ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?rcl_val))
supp SUnit = {}
supp (SUt ?rcl_val) = supp ?rcl_val
supp ?x = {}

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal (4 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
case (V_var x)
[PROOF STATE]
proof (state)
this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b

goal (4 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
[PROOF STEP]
obtain c where  *:"Some (b,c) = lookup \<Gamma> x"
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b

goal (1 subgoal):
 1. (\<And>c. Some (b, c) = lookup \<Gamma> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfV_elims
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?x ]\<^sup>v : ?b ; \<And>c. \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; Some (?b, c) = lookup ?\<Gamma> ?x\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : ?b ; \<lbrakk>?b = base_for_lit ?l;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 , ?v2.0 ]\<^sup>v : ?b ; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b1 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?tyid ?dc ?v : ?b ; \<And>dclist x b' c. \<lbrakk>?b = B_id ?tyid; AF_typedef ?tyid dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b' \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp ?tyid ?dc ?b ?v : ?b' ; \<And>bv dclist x b' c. \<lbrakk>?b' = B_app ?tyid ?b; AF_typedef_poly ?tyid bv dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; atom bv \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>, ?b, ?v);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b'[bv::=?b]\<^sub>b\<^sub>b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>c. Some (b, c) = lookup \<Gamma> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Some (b, c) = lookup \<Gamma> x

goal (4 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
hence "x \<in> fst ` toSet \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
Some (b, c) = lookup \<Gamma> x

goal (1 subgoal):
 1. x \<in> fst ` toSet \<Gamma>
[PROOF STEP]
using lookup_x
[PROOF STATE]
proof (prove)
using this:
Some (b, c) = lookup \<Gamma> x
Some (?b, ?c) = lookup ?G ?x \<Longrightarrow> ?x \<in> fst ` toSet ?G

goal (1 subgoal):
 1. x \<in> fst ` toSet \<Gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> fst ` toSet \<Gamma>

goal (4 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
hence "x \<in> dom i"
[PROOF STATE]
proof (prove)
using this:
x \<in> fst ` toSet \<Gamma>

goal (1 subgoal):
 1. x \<in> dom i
[PROOF STEP]
using wfI_domi
[PROOF STATE]
proof (prove)
using this:
x \<in> fst ` toSet \<Gamma>
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i \<Longrightarrow> fst ` toSet ?\<Gamma> \<subseteq> dom ?i

goal (1 subgoal):
 1. x \<in> dom i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> fst ` toSet \<Gamma>
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i \<Longrightarrow> fst ` toSet ?\<Gamma> \<subseteq> dom ?i
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

goal (1 subgoal):
 1. x \<in> dom i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> dom i

goal (4 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> dom i
[PROOF STEP]
obtain s where "i x = Some s"
[PROOF STATE]
proof (prove)
using this:
x \<in> dom i

goal (1 subgoal):
 1. (\<And>s. i x = Some s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i x = Some s

goal (4 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i x = Some s

goal (4 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
hence "P \<turnstile> s : b"
[PROOF STATE]
proof (prove)
using this:
i x = Some s

goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
using wfRCV.intros wfI_lookup * V_var
[PROOF STATE]
proof (prove)
using this:
i x = Some s
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
\<lbrakk>Some (?b, ?c) = lookup ?G ?x;  ?P ; ?G \<turnstile> ?i; Some ?s = ?i ?x;  ?P ; ?B  \<turnstile>\<^sub>w\<^sub>f ?G \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s : ?b
Some (b, c) = lookup \<Gamma> x
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b

goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
by (metis wfV_wf)
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s : b

goal (4 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i x = Some s
 P  \<turnstile> s : b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i x = Some s
 P  \<turnstile> s : b

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using eval_v.intros rcl_val.supp b.supp
[PROOF STATE]
proof (prove)
using this:
i x = Some s
 P  \<turnstile> s : b
?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
supp (SBitvec ?list) = supp ?list
supp (SNum ?int) = supp ?int
supp (SBool ?bool) = supp ?bool
supp (SPair ?rcl_val1.0 ?rcl_val2.0) = supp ?rcl_val1.0 \<union> supp ?rcl_val2.0
supp (SCons ?list1.0 ?list2.0 ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?rcl_val)
supp (SConsp ?list1.0 ?list2.0 ?b ?rcl_val) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?rcl_val))
supp SUnit = {}
supp (SUt ?rcl_val) = supp ?rcl_val
supp B_int = {}
supp B_bool = {}
supp (B_id ?list) = supp ?list
supp [ ?b1.0 , ?b2.0 ]\<^sup>b = supp ?b1.0 \<union> supp ?b2.0
supp B_unit = {}
supp B_bitvec = {}
supp (B_var ?bv) = supp ?bv
supp (B_app ?list ?b) = supp ?list \<union> supp ?b

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal (3 subgoals):
 1. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
case (V_pair v1 v2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b

goal (3 subgoals):
 1. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
[PROOF STEP]
obtain b1 and b2 where *:"P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1 \<and>  P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b2 \<and> b = B_pair b1 b2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b

goal (1 subgoal):
 1. (\<And>b1 b2.  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b2  \<and> b = [ b1 , b2 ]\<^sup>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfV_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?x ]\<^sup>v : ?b ; \<And>c. \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; Some (?b, c) = lookup ?\<Gamma> ?x\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?l ]\<^sup>v : ?b ; \<lbrakk>?b = base_for_lit ?l;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 , ?v2.0 ]\<^sup>v : ?b ; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b1 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?tyid ?dc ?v : ?b ; \<And>dclist x b' c. \<lbrakk>?b = B_id ?tyid; AF_typedef ?tyid dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b' \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp ?tyid ?dc ?b ?v : ?b' ; \<And>bv dclist x b' c. \<lbrakk>?b' = B_app ?tyid ?b; AF_typedef_poly ?tyid bv dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; atom bv \<sharp> (?\<Theta>, ?\<B>, ?\<Gamma>, ?b, ?v);  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b'[bv::=?b]\<^sub>b\<^sub>b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>b1 b2.  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b2  \<and> b = [ b1 , b2 ]\<^sup>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b2  \<and> b = [ b1 , b2 ]\<^sup>b

goal (3 subgoals):
 1. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b2  \<and> b = [ b1 , b2 ]\<^sup>b
[PROOF STEP]
obtain s1 and s2 where "eval_v i v1 s1 \<and> wfRCV P s1 b1 \<and> eval_v i v2 s2 \<and> wfRCV P s2 b2"
[PROOF STATE]
proof (prove)
using this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b2  \<and> b = [ b1 , b2 ]\<^sup>b

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : b1 \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : b2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using V_pair
[PROOF STATE]
proof (prove)
using this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b2  \<and> b = [ b1 , b2 ]\<^sup>b
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 , v2 ]\<^sup>v : b

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : b1 \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : b2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : b1 \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : b2

goal (3 subgoals):
 1. \<And>x1a x2a b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2a : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a , x2a ]\<^sup>v : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
thus   ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : b1 \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : b2

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using eval_v.intros wfRCV.intros *
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : b1 \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : b2
?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
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b2  \<and> b = [ b1 , b2 ]\<^sup>b

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal (2 subgoals):
 1. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
case (V_cons tyid dc v)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v : b

goal (2 subgoals):
 1. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v : b
[PROOF STEP]
obtain  s and  b'::b and dclist and x::x and c::c where "(wfV P  B  \<Gamma> v  b') \<and> i \<lbrakk> v \<rbrakk> ~  s \<and> P \<turnstile> s : b' \<and> b = B_id tyid \<and>
                 AF_typedef tyid dclist \<in> set P \<and> (dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v : b

goal (1 subgoal):
 1. (\<And>b' s dclist x c.  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'  \<and> i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b' \<and> b = B_id tyid \<and> AF_typedef tyid dclist \<in> set P \<and> (dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  wfV_elims(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v : b
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons ?tyid ?dc ?v : ?b ; \<And>dclist x b' c. \<lbrakk>?b = B_id ?tyid; AF_typedef ?tyid dclist \<in> set ?\<Theta>; (?dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : b' \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>b' s dclist x c.  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'  \<and> i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b' \<and> b = B_id tyid \<and> AF_typedef tyid dclist \<in> set P \<and> (dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'  \<and> i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b' \<and> b = B_id tyid \<and> AF_typedef tyid dclist \<in> set P \<and> (dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist

goal (2 subgoals):
 1. \<And>x1a x2a x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons x1a x2a x3 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'  \<and> i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b' \<and> b = B_id tyid \<and> AF_typedef tyid dclist \<in> set P \<and> (dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'  \<and> i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b' \<and> b = B_id tyid \<and> AF_typedef tyid dclist \<in> set P \<and> (dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using eval_v.intros(4) wfRCV.intros(5) V_cons
[PROOF STATE]
proof (prove)
using this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'  \<and> i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b' \<and> b = B_id tyid \<and> AF_typedef tyid dclist \<in> set P \<and> (dc, \<lbrace> x : b'  | c \<rbrace>) \<in> set dclist
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_cons tyid dc v : b

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
case (V_consp tyid dc b' v)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp tyid dc b' v : b

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
obtain  b'a::b and bv and dclist and x::x and c::c where *:"(wfV P  B  \<Gamma> v  b'a[bv::=b']\<^sub>b\<^sub>b) \<and> b = B_app tyid b' \<and>
                 AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and>
           atom bv \<sharp> (P, B_app tyid b',B) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b'a bv dclist x c.  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  wf_strong_elim(1)[OF V_consp(3)]
[PROOF STATE]
proof (prove)
using this:
\<exists>bv dclist x b'a c. b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and>  P ; B  \<turnstile>\<^sub>w\<^sub>f b'  \<and> atom bv \<sharp> (P, B, \<Gamma>, b', v) \<and>  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> atom bv \<sharp> ?tm

goal (1 subgoal):
 1. (\<And>b'a bv dclist x c.  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B)

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B)
[PROOF STEP]
obtain s where **:"i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b'a[bv::=b']\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B)

goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b'a[bv::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using V_consp
[PROOF STATE]
proof (prove)
using this:
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B)
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp tyid dc b' v : b

goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b'a[bv::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b'a[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
have " \<turnstile>\<^sub>w\<^sub>f P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.    \<turnstile>\<^sub>w\<^sub>f P
[PROOF STEP]
using wfX_wfY V_consp
[PROOF STATE]
proof (prove)
using this:
 ?\<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>
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp tyid dc b' v : b

goal (1 subgoal):
 1.    \<turnstile>\<^sub>w\<^sub>f P
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
   \<turnstile>\<^sub>w\<^sub>f P
[PROOF STEP]
obtain bv1::bv and dclist1 x1 b1 c1 where 3:"AF_typedef_poly tyid bv dclist =  AF_typedef_poly tyid bv1 dclist1
      \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp>  (P, SConsp tyid dc b' s, B_app tyid b')
          \<and> b'a[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b') \<and> b'a[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  *  obtain_fresh_bv_dclist_b_iff
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f P
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B)
\<lbrakk>(?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; AF_typedef_poly ?tyid ?bv ?dclist \<in> set ?P;    \<turnstile>\<^sub>w\<^sub>f ?P ; \<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly ?tyid ?bv ?dclist = AF_typedef_poly ?tyid bv1 dclist1 \<and> (?dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> ?tm \<and> ?b[?bv::=?b']\<^sub>b\<^sub>b = b1[bv1::=?b']\<^sub>b\<^sub>b \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b') \<and> b'a[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b') \<and> b'a[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
have " i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ SConsp tyid dc b' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ SConsp tyid dc b' s
[PROOF STEP]
using  eval_v.intros
[PROOF STATE]
proof (prove)
using this:
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s

goal (1 subgoal):
 1. i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ SConsp tyid dc b' s
[PROOF STEP]
by (simp add: "**")
[PROOF STATE]
proof (state)
this:
i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ SConsp tyid dc b' s

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ SConsp tyid dc b' s

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
have " P  \<turnstile>  SConsp tyid dc b' s : B_app tyid b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> SConsp tyid dc b' s : B_app tyid b'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. AF_typedef_poly tyid ?bv ?dclist \<in> set P
 2. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist
 3. atom ?bv \<sharp> (P, SConsp tyid dc b' s, B_app tyid b')
 4.  P  \<turnstile> s : ?b[?bv::=b']\<^sub>b\<^sub>b
[PROOF STEP]
show \<open>AF_typedef_poly tyid bv1 dclist1 \<in> set P\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AF_typedef_poly tyid bv1 dclist1 \<in> set P
[PROOF STEP]
using 3 *
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b') \<and> b'a[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B)

goal (1 subgoal):
 1. AF_typedef_poly tyid bv1 dclist1 \<in> set P
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bv1 dclist1 \<in> set P

goal (3 subgoals):
 1. (dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set dclist1
 2. atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b')
 3.  P  \<turnstile> s : ?b[bv1::=b']\<^sub>b\<^sub>b
[PROOF STEP]
show \<open>(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b') \<and> b'a[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1

goal (2 subgoals):
 1. atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b')
 2.  P  \<turnstile> s : b1[bv1::=b']\<^sub>b\<^sub>b
[PROOF STEP]
thus \<open>atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b')\<close>
[PROOF STATE]
proof (prove)
using this:
(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1

goal (1 subgoal):
 1. atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b')
[PROOF STEP]
using * 3 fresh_prodN
[PROOF STATE]
proof (prove)
using this:
(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B)
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b') \<and> b'a[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b
?a \<sharp> (?x, ?y) = (?a \<sharp> ?x \<and> ?a \<sharp> ?y)
?x \<sharp> (?a, ?b, ?c) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c)
?x \<sharp> (?a, ?b, ?c, ?d) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d)
?x \<sharp> (?a, ?b, ?c, ?d, ?e) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h, ?i) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h \<and> ?x \<sharp> ?i)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h, ?i, ?j) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h \<and> ?x \<sharp> ?i \<and> ?x \<sharp> ?j)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h, ?i, ?j, ?k, ?l) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h \<and> ?x \<sharp> ?i \<and> ?x \<sharp> ?j \<and> ?x \<sharp> ?k \<and> ?x \<sharp> ?l)

goal (1 subgoal):
 1. atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b')

goal (1 subgoal):
 1.  P  \<turnstile> s : b1[bv1::=b']\<^sub>b\<^sub>b
[PROOF STEP]
show \<open> P  \<turnstile> s : b1[bv1::=b']\<^sub>b\<^sub>b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> s : b1[bv1::=b']\<^sub>b\<^sub>b
[PROOF STEP]
using  3 **
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> (P, SConsp tyid dc b' s, B_app tyid b') \<and> b'a[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b'a[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1.  P  \<turnstile> s : b1[bv1::=b']\<^sub>b\<^sub>b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s : b1[bv1::=b']\<^sub>b\<^sub>b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> SConsp tyid dc b' s : B_app tyid b'

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp x1a x2a x3 x4 : b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ SConsp tyid dc b' s
 P  \<turnstile> SConsp tyid dc b' s : B_app tyid b'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ SConsp tyid dc b' s
 P  \<turnstile> SConsp tyid dc b' s : B_app tyid b'

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using eval_v.intros wfRCV.intros V_consp *
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ SConsp tyid dc b' s
 P  \<turnstile> SConsp tyid dc b' s : B_app tyid b'
?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
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f V_consp tyid dc b' v : b
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b'a[bv::=b']\<^sub>b\<^sub>b  \<and> b = B_app tyid b' \<and> AF_typedef_poly tyid bv dclist \<in> set P \<and> (dc, \<lbrace> x : b'a  | c \<rbrace>) \<in> set dclist \<and> atom bv \<sharp> (P, B_app tyid b', B)

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> V_consp tyid dc b' v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_v_base:
  fixes \<Gamma>::\<Gamma> and v::v and b::b
  assumes "P ; \<Gamma>  \<turnstile> i" and "P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b" and "i \<lbrakk> v \<rbrakk> ~  s"
  shows "P \<turnstile> s : b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
using eval_v_exist eval_v_uniqueness assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
i \<lbrakk> v \<rbrakk> ~ s

goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
by metis