[STATEMENT]
lemma is_satis_imp:
  fixes c1::c and c2::c
  assumes "i \<Turnstile> c1 \<longrightarrow> i \<Turnstile> c2" and "i \<lbrakk> c1 \<rbrakk> ~ b1" and "i \<lbrakk> c2 \<rbrakk> ~ b2"
  shows "i \<Turnstile> (c1 IMP c2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
proof(cases b1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
 2. \<not> b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b1

goal (2 subgoals):
 1. b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
 2. \<not> b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
hence "i \<Turnstile> c2"
[PROOF STATE]
proof (prove)
using this:
b1

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

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

goal (2 subgoals):
 1. b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
 2. \<not> b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
hence "b2 = True"
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c2

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

goal (1 subgoal):
 1. b2 = True
[PROOF STEP]
using eval_c_uniqueness
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c2
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )
 i \<Turnstile> c1  \<longrightarrow>  i \<Turnstile> c2
 i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk> ?i \<lbrakk> ?c \<rbrakk> ~ ?s ;  ?i \<lbrakk> ?c \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'

goal (1 subgoal):
 1. b2 = True
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b2 = True

goal (2 subgoals):
 1. b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
 2. \<not> b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b2 = True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b2 = True

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

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

goal (1 subgoal):
 1. \<not> b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> b1

goal (1 subgoal):
 1. \<not> b1 \<Longrightarrow>  i \<Turnstile> c1  IMP  c2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> b1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> b1

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_iff:
  "i \<Turnstile> G  = (\<forall>x b c. (x,b,c) \<in> toSet G \<longrightarrow> i \<Turnstile> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> G  = (\<forall>x b c. (x, b, c) \<in> toSet G \<longrightarrow>  i \<Turnstile> c )
[PROOF STEP]
by(induct G,auto)


[STATEMENT]
lemma is_satis_g_append:
  "i \<Turnstile> (G1@G2) = (i \<Turnstile>  G1 \<and> i \<Turnstile>  G2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> G1 @ G2  = ( i \<Turnstile> G1  \<and>  i \<Turnstile> G2 )
[PROOF STEP]
using is_satis_g.simps  is_satis_iff
[PROOF STATE]
proof (prove)
using this:
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )
 ?i \<Turnstile> ?G  = (\<forall>x b c. (x, b, c) \<in> toSet ?G \<longrightarrow>  ?i \<Turnstile> c )

goal (1 subgoal):
 1.  i \<Turnstile> G1 @ G2  = ( i \<Turnstile> G1  \<and>  i \<Turnstile> G2 )
[PROOF STEP]
by auto


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

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

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

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
by (metis eval_v_elims(1) eval_v_litI)
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'

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

goal (4 subgoals):
 1. \<And>xa s'. \<lbrakk>atom x \<sharp> [ xa ]\<^sup>v; i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x1a; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>atom x \<sharp> x2a; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; atom x \<sharp> [ x1a , x2a ]\<^sup>v; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 4. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> [ y ]\<^sup>v
i \<lbrakk> [ y ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
obtain s where *: "Some s = i y \<and> s=s'"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> [ y ]\<^sup>v
i \<lbrakk> [ y ]\<^sup>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. (\<And>s. Some s = i y \<and> s = s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> [ y ]\<^sup>v
i \<lbrakk> [ y ]\<^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. (\<And>s. Some s = i y \<and> s = s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Some s = i y \<and> s = s'

goal (4 subgoals):
 1. \<And>xa s'. \<lbrakk>atom x \<sharp> [ xa ]\<^sup>v; i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x1a; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>atom x \<sharp> x2a; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; atom x \<sharp> [ x1a , x2a ]\<^sup>v; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 4. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Some s = i y \<and> s = s'

goal (4 subgoals):
 1. \<And>xa s'. \<lbrakk>atom x \<sharp> [ xa ]\<^sup>v; i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x1a; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>atom x \<sharp> x2a; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; atom x \<sharp> [ x1a , x2a ]\<^sup>v; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 4. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
using \<open>atom x \<sharp> V_var y\<close> v.supp
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> [ y ]\<^sup>v
supp [ ?l ]\<^sup>v = supp ?l
supp [ ?x ]\<^sup>v = supp ?x
supp [ ?v1.0 , ?v2.0 ]\<^sup>v = supp ?v1.0 \<union> supp ?v2.0
supp (V_cons ?list1.0 ?list2.0 ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?v)
supp (V_consp ?list1.0 ?list2.0 ?b ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?v))

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

goal (4 subgoals):
 1. \<And>xa s'. \<lbrakk>atom x \<sharp> [ xa ]\<^sup>v; i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x1a; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>atom x \<sharp> x2a; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; atom x \<sharp> [ x1a , x2a ]\<^sup>v; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 4. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Some s = i y \<and> s = s'
x \<noteq> y
[PROOF STEP]
have "(i ( x \<mapsto>s)) y = Some s"
[PROOF STATE]
proof (prove)
using this:
Some s = i y \<and> s = s'
x \<noteq> y

goal (1 subgoal):
 1. (i(x \<mapsto> s)) y = Some s
[PROOF STEP]
by (simp add: \<open>Some s = i y \<and> s = s'\<close>)
[PROOF STATE]
proof (state)
this:
(i(x \<mapsto> s)) y = Some s

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

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ y ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
using eval_v_varI *  \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (prove)
using this:
(i(x \<mapsto> s)) y = Some s
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
Some s = i y \<and> s = s'
x \<noteq> y

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ y ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
by (simp add: eval_v.eval_v_varI)
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> [ y ]\<^sup>v \<rbrakk> ~ s'

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

goal (3 subgoals):
 1. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x1a; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>atom x \<sharp> x2a; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; atom x \<sharp> [ x1a , x2a ]\<^sup>v; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
hence "atom x \<sharp> v1 \<and> atom x \<sharp> v2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>atom x \<sharp> v2; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. atom x \<sharp> v1 \<and> atom x \<sharp> v2
[PROOF STEP]
using v.supp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>atom x \<sharp> v2; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
supp [ ?l ]\<^sup>v = supp ?l
supp [ ?x ]\<^sup>v = supp ?x
supp [ ?v1.0 , ?v2.0 ]\<^sup>v = supp ?v1.0 \<union> supp ?v2.0
supp (V_cons ?list1.0 ?list2.0 ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?v)
supp (V_consp ?list1.0 ?list2.0 ?b ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?v))

goal (1 subgoal):
 1. atom x \<sharp> v1 \<and> atom x \<sharp> v2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom x \<sharp> v1 \<and> atom x \<sharp> v2

goal (3 subgoals):
 1. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x1a; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>atom x \<sharp> x2a; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; atom x \<sharp> [ x1a , x2a ]\<^sup>v; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom x \<sharp> v1 \<and> atom x \<sharp> v2

goal (3 subgoals):
 1. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x1a; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>atom x \<sharp> x2a; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; atom x \<sharp> [ x1a , x2a ]\<^sup>v; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
obtain s1 and s2 where *: "eval_v i v1 s1 \<and> eval_v i v2 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>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>atom x \<sharp> v2; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
atom x \<sharp> [ v1 , v2 ]\<^sup>v
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'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x1a; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>atom x \<sharp> x2a; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; atom x \<sharp> [ x1a , x2a ]\<^sup>v; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> v1 \<and> atom x \<sharp> v2
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s' = SPair s1 s2
[PROOF STEP]
have "eval_v ((i ( x \<mapsto>s))) v1 s1 \<and> eval_v ((i ( x \<mapsto>s))) v2 s2"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> v1 \<and> atom x \<sharp> v2
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s' = SPair s1 s2

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2
[PROOF STEP]
using V_pair
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> v1 \<and> atom x \<sharp> v2
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s' = SPair s1 s2
\<lbrakk>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>atom x \<sharp> v2; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2

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

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
using eval_v_pairI *
[PROOF STATE]
proof (prove)
using this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2
\<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> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s' = SPair s1 s2

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'

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

goal (2 subgoals):
 1. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
hence "atom x \<sharp> v1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
atom x \<sharp> V_cons tyid dc v1
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'

goal (1 subgoal):
 1. atom x \<sharp> v1
[PROOF STEP]
using v.supp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
atom x \<sharp> V_cons tyid dc v1
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
supp [ ?l ]\<^sup>v = supp ?l
supp [ ?x ]\<^sup>v = supp ?x
supp [ ?v1.0 , ?v2.0 ]\<^sup>v = supp ?v1.0 \<union> supp ?v2.0
supp (V_cons ?list1.0 ?list2.0 ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?v)
supp (V_consp ?list1.0 ?list2.0 ?b ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?v))

goal (1 subgoal):
 1. atom x \<sharp> v1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom x \<sharp> v1

goal (2 subgoals):
 1. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom x \<sharp> v1

goal (2 subgoals):
 1. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
obtain s1 where *: "eval_v i v1 s1 \<and> s' = SCons tyid dc s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> s' = SCons tyid dc s1 \<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>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
atom x \<sharp> V_cons tyid dc v1
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'

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

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

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

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1

goal (2 subgoals):
 1. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x3; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; atom x \<sharp> V_cons x1a x2a x3; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
[PROOF STEP]
using eval_v_consI *
[PROOF STATE]
proof (prove)
using this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> s' = SCons tyid dc s1

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'

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

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
hence "atom x \<sharp> v1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
atom x \<sharp> V_consp tyid dc b1 v1
i \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'

goal (1 subgoal):
 1. atom x \<sharp> v1
[PROOF STEP]
using v.supp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
atom x \<sharp> V_consp tyid dc b1 v1
i \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
supp [ ?l ]\<^sup>v = supp ?l
supp [ ?x ]\<^sup>v = supp ?x
supp [ ?v1.0 , ?v2.0 ]\<^sup>v = supp ?v1.0 \<union> supp ?v2.0
supp (V_cons ?list1.0 ?list2.0 ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?v)
supp (V_consp ?list1.0 ?list2.0 ?b ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?v))

goal (1 subgoal):
 1. atom x \<sharp> v1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom x \<sharp> v1

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom x \<sharp> v1

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
obtain s1 where *: "eval_v i v1 s1 \<and> s' = SConsp tyid dc b1 s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_consp
[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>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
atom x \<sharp> V_consp tyid dc b1 v1
i \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'

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

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> v1
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1
[PROOF STEP]
have "eval_v ((i ( x \<mapsto>s))) v1 s1"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> v1
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1
[PROOF STEP]
using V_consp
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> v1
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1
\<lbrakk>atom x \<sharp> v1; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
atom x \<sharp> V_consp tyid dc b1 v1
i \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>atom x \<sharp> x4; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; atom x \<sharp> V_consp x1a x2a x3 x4; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
[PROOF STEP]
using eval_v_conspI *
[PROOF STATE]
proof (prove)
using this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> e \<rbrakk> ~ s'
[PROOF STEP]
apply(induct rule: eval_e.induct)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>i v sv. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ sv ; atom x \<sharp> [ v ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv
 2. \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; atom x \<sharp> v1 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> v2 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ plus v1 v2 ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
 3. \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; atom x \<sharp> v1 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> v2 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 4. \<And>i v1 s1 v2 s2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ s1 ; atom x \<sharp> v1 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> v2 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 5. \<And>i v v1 v2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> v \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 6. \<And>i v v1 v2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> v \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 7. \<And>i v1 bv1 v2 bv2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; atom x \<sharp> v1 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> v2 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 8. \<And>i v bv. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> v \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
using eval_v_i_upd eval_e_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>atom ?x \<sharp> ?v; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?i(?x \<mapsto> ?s) \<lbrakk> ?v \<rbrakk> ~ ?s'
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SNum (n1 + n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SBool (n1 \<le> n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SBool (s1 = s2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v2. ?i \<lbrakk> ?v \<rbrakk> ~ SPair ?s v2  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v1. ?i \<lbrakk> ?v \<rbrakk> ~ SPair v1 ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv1 bv2. \<lbrakk>?s = SBitvec (bv1 @ bv2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec bv1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv. \<lbrakk>?s = SNum (int (length bv)); ?i \<lbrakk> ?v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (8 subgoals):
 1. \<And>i v sv. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ sv ; atom x \<sharp> [ v ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv
 2. \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; atom x \<sharp> v1 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> v2 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ plus v1 v2 ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
 3. \<And>i v1 n1 v2 n2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; atom x \<sharp> v1 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> v2 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 4. \<And>i v1 s1 v2 s2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ s1 ; atom x \<sharp> v1 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> v2 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 5. \<And>i v v1 v2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> v \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 6. \<And>i v v1 v2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> v \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 7. \<And>i v1 bv1 v2 bv2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; atom x \<sharp> v1 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> v2 \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 8. \<And>i v bv. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> v \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
by (meson ce.fresh eval_e.intros)+


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

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ s'
[PROOF STEP]
proof(induct rule:eval_c.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>i. atom x \<sharp> (TRUE) \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>i. atom x \<sharp> (FALSE) \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; atom x \<sharp> c1 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> c2 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; atom x \<sharp> c1 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> c2 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; atom x \<sharp> c1 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> c2 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>i c b. \<lbrakk> i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> c \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 7. \<And>i e1 sv1 e2 sv2. \<lbrakk>i \<lbrakk> e1 \<rbrakk> ~ sv1 ; i \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_eqI i e1 sv1 e2 sv2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
atom x \<sharp> (e1  ==  e2 )

goal (7 subgoals):
 1. \<And>i. atom x \<sharp> (TRUE) \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>i. atom x \<sharp> (FALSE) \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; atom x \<sharp> c1 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> c2 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; atom x \<sharp> c1 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> c2 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; atom x \<sharp> c1 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> c2 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>i c b. \<lbrakk> i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> c \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 7. \<And>i e1 sv1 e2 sv2. \<lbrakk>i \<lbrakk> e1 \<rbrakk> ~ sv1 ; i \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
atom x \<sharp> (e1  ==  e2 )
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
atom x \<sharp> (e1  ==  e2 )

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
using RCLogic.eval_c_eqI eval_e_i_upd c.fresh
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
atom x \<sharp> (e1  ==  e2 )
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0
\<lbrakk>?i \<lbrakk> ?e \<rbrakk> ~ ?s' ; atom ?x \<sharp> ?e\<rbrakk> \<Longrightarrow> ?i(?x \<mapsto> ?s) \<lbrakk> ?e \<rbrakk> ~ ?s'
?a \<sharp> (TRUE)
?a \<sharp> (FALSE)
?a \<sharp> (?c1.0  AND  ?c2.0 ) = (?a \<sharp> ?c1.0 \<and> ?a \<sharp> ?c2.0)
?a \<sharp> (?c1.0 OR ?c2.0 ) = (?a \<sharp> ?c1.0 \<and> ?a \<sharp> ?c2.0)
?a \<sharp> (\<not> ?c ) = ?a \<sharp> ?c
?a \<sharp> (?c1.0  IMP  ?c2.0 ) = (?a \<sharp> ?c1.0 \<and> ?a \<sharp> ?c2.0)
?a \<sharp> (?ce1.0  ==  ?ce2.0 ) = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2

goal (6 subgoals):
 1. \<And>i. atom x \<sharp> (TRUE) \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>i. atom x \<sharp> (FALSE) \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; atom x \<sharp> c1 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> c2 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; atom x \<sharp> c1 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> c2 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>i c1 b1 c2 b2. \<lbrakk> i \<lbrakk> c1 \<rbrakk> ~ b1 ; atom x \<sharp> c1 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ b1 ;  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> c2 \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>i c b. \<lbrakk> i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> c \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c )\<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
[PROOF STEP]
qed(simp add: eval_c.intros)+