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

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

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

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_elims eval_l.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s 
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' 
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = s'

goal (4 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (V_var x)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s 
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' 

goal (4 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s 
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s 
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' 

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s 
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' 
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by (metis option.inject)
[PROOF STATE]
proof (state)
this:
s = s'

goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (V_pair v1 v2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> v2 \<rbrakk> ~ ?s ; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s 
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s' 

goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain s1 and s2 where s:"i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2 \<and> s = SPair s1 s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_pair
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> v2 \<rbrakk> ~ ?s ; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s 
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s' 

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

goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain s1' and s2' where s':"i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2' \<and> s' = SPair s1' s2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1' s2'. i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_pair
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> v2 \<rbrakk> ~ ?s ; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s 
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s' 

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

goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using V_pair s s'
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> v2 \<rbrakk> ~ ?s ; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s 
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s' 
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s = SPair s1 s2
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'

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

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (V_cons tyid dc v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s 
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s' 

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain sv1 where 1:"i \<lbrakk> v1 \<rbrakk> ~ sv1 \<and> s = SCons tyid dc sv1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sv1. i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s 
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s' 

goal (1 subgoal):
 1. (\<And>sv1. i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain sv2 where 2:"i \<lbrakk> v1 \<rbrakk> ~ sv2 \<and> s' = SCons tyid dc sv2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sv2. i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s 
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s' 

goal (1 subgoal):
 1. (\<And>sv2. i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2
[PROOF STEP]
have "sv1 = sv2"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2

goal (1 subgoal):
 1. sv1 = sv2
[PROOF STEP]
using V_cons
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s 
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s' 

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

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sv1 = sv2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sv1 = sv2

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
sv1 = sv2
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2

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

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (V_consp tyid dc b v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s 
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s' 

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s 
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s 
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s' 

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s 
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s' 
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = s'

goal:
No subgoals!
[PROOF STEP]
qed