[STATEMENT]
lemma eval_v_weakening_x:
  fixes c::v
  assumes  "i' \<lbrakk> c \<rbrakk> ~ s" and "atom x \<sharp> c" and "i = i' (x \<mapsto> s')"
  shows "i \<lbrakk> c \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i' \<lbrakk> c \<rbrakk> ~ s 
atom x \<sharp> c
i = i'(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
proof(induct rule: eval_v.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>ia l. \<lbrakk>atom x \<sharp> [ l ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>  
 2. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv 
 3. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 4. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 5. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_litI i l)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> [ l ]\<^sup>v
i = i(x \<mapsto> s')

goal (5 subgoals):
 1. \<And>ia l. \<lbrakk>atom x \<sharp> [ l ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>  
 2. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv 
 3. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 4. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 5. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> [ l ]\<^sup>v
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> [ l ]\<^sup>v
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>
[PROOF STEP]
using eval_v.intros
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> [ l ]\<^sup>v
i = i(x \<mapsto> s')
?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> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>  

goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv 
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv 
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_varI sv i1 x1)
[PROOF STATE]
proof (state)
this:
Some sv = i1 x1
atom x \<sharp> [ x1 ]\<^sup>v
i = i1(x \<mapsto> s')

goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv 
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
hence "x \<noteq> x1"
[PROOF STATE]
proof (prove)
using this:
Some sv = i1 x1
atom x \<sharp> [ x1 ]\<^sup>v
i = i1(x \<mapsto> s')

goal (1 subgoal):
 1. x \<noteq> x1
[PROOF STEP]
using v.fresh fresh_at_base
[PROOF STATE]
proof (prove)
using this:
Some sv = i1 x1
atom x \<sharp> [ x1 ]\<^sup>v
i = i1(x \<mapsto> s')
?a \<sharp> [ ?l ]\<^sup>v = ?a \<sharp> ?l
?a \<sharp> [ ?x ]\<^sup>v = ?a \<sharp> ?x
?a \<sharp> [ ?v1.0 , ?v2.0 ]\<^sup>v = (?a \<sharp> ?v1.0 \<and> ?a \<sharp> ?v2.0)
?a \<sharp> V_cons ?list1.0 ?list2.0 ?v = (?a \<sharp> ?list1.0 \<and> ?a \<sharp> ?list2.0 \<and> ?a \<sharp> ?v)
?a \<sharp> V_consp ?list1.0 ?list2.0 ?b ?v = (?a \<sharp> ?list1.0 \<and> ?a \<sharp> ?list2.0 \<and> ?a \<sharp> ?b \<and> ?a \<sharp> ?v)
sort_of ?a \<noteq> sort_of (atom ?b) \<Longrightarrow> ?a \<sharp> ?b
?a \<sharp> ?b = (?a \<noteq> atom ?b)

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

goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv 
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
hence "i x1 = Some sv"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1

goal (1 subgoal):
 1. i x1 = Some sv
[PROOF STEP]
using eval_v_varI
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1
Some sv = i1 x1
atom x \<sharp> [ x1 ]\<^sup>v
i = i1(x \<mapsto> s')

goal (1 subgoal):
 1. i x1 = Some sv
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i x1 = Some sv

goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv 
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i x1 = Some sv
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i x1 = Some sv

goal (1 subgoal):
 1. i \<lbrakk> [ x1 ]\<^sup>v \<rbrakk> ~ sv
[PROOF STEP]
using eval_v.intros
[PROOF STATE]
proof (prove)
using this:
i x1 = Some sv
?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> [ x1 ]\<^sup>v \<rbrakk> ~ sv
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x1 ]\<^sup>v \<rbrakk> ~ sv 

goal (3 subgoals):
 1. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 2. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 3. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 2. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 3. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_pairI i v1 s1 v2 s2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ s1 
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 
i \<lbrakk> v2 \<rbrakk> ~ s2 
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i = i(x \<mapsto> s')

goal (3 subgoals):
 1. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 
 2. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 3. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ s1 
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 
i \<lbrakk> v2 \<rbrakk> ~ s2 
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1 
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 
i \<lbrakk> v2 \<rbrakk> ~ s2 
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
using eval_v.intros
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1 
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 
i \<lbrakk> v2 \<rbrakk> ~ s2 
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i = i(x \<mapsto> s')
?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> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2 

goal (2 subgoals):
 1. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 2. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 2. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_consI i v s tyid dc)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s 
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s 
atom x \<sharp> V_cons tyid dc v
i = i(x \<mapsto> s')

goal (2 subgoals):
 1. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 
 2. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s 
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s 
atom x \<sharp> V_cons tyid dc v
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s 
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s 
atom x \<sharp> V_cons tyid dc v
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
[PROOF STEP]
using eval_v.intros
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s 
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s 
atom x \<sharp> V_cons tyid dc v
i = i(x \<mapsto> s')
?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_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s 

goal (1 subgoal):
 1. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_conspI i v s tyid dc b)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s 
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s 
atom x \<sharp> V_consp tyid dc b v
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s 
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s 
atom x \<sharp> V_consp tyid dc b v
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s 
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s 
atom x \<sharp> V_consp tyid dc b v
i = i(x \<mapsto> s')

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> v \<rbrakk> ~ s 
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s 
atom x \<sharp> V_consp tyid dc b v
i = i(x \<mapsto> s')
?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 auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s 

goal:
No subgoals!
[PROOF STEP]
qed