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

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

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

goal (1 subgoal):
 1. i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv
[PROOF STEP]
using  eval_v_weakening_x eval_e.intros  ce.fresh
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ sv
atom x \<sharp> [ v ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
\<lbrakk>?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?c \<rbrakk> ~ ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?a \<sharp> [ ?v ]\<^sup>c\<^sup>e = ?a \<sharp> ?v
?a \<sharp> [ ?opp ?ce1.0 ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?opp \<and> ?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [ ?ce1.0 @@ ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [#1?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [#2?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [| ?ce |]\<^sup>c\<^sup>e = ?a \<sharp> ?ce

goal (1 subgoal):
 1. i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv

goal (7 subgoals):
 1. \<And>ia v1 n1 v2 n2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; ia \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ plus v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
 2. \<And>ia v1 n1 v2 n2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; ia \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 3. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 4. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 5. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 6. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 7. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>ia v1 n1 v2 n2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; ia \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ plus v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
 2. \<And>ia v1 n1 v2 n2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; ia \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 3. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 4. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 5. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 6. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 7. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
case (eval_e_plusI i v1 n1 v2 n2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1
i \<lbrakk> v2 \<rbrakk> ~ SNum n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
atom x \<sharp> [ plus v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

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

goal (1 subgoal):
 1. i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
[PROOF STEP]
using  eval_v_weakening_x eval_e.intros  ce.fresh
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1
i \<lbrakk> v2 \<rbrakk> ~ SNum n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
atom x \<sharp> [ plus v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
\<lbrakk>?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?c \<rbrakk> ~ ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?a \<sharp> [ ?v ]\<^sup>c\<^sup>e = ?a \<sharp> ?v
?a \<sharp> [ ?opp ?ce1.0 ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?opp \<and> ?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [ ?ce1.0 @@ ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [#1?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [#2?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [| ?ce |]\<^sup>c\<^sup>e = ?a \<sharp> ?ce

goal (1 subgoal):
 1. i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)

goal (6 subgoals):
 1. \<And>ia v1 n1 v2 n2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; ia \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 3. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 4. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 5. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 6. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>ia v1 n1 v2 n2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; ia \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 3. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 4. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 5. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 6. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
case (eval_e_leqI i v1 n1 v2 n2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1
i \<lbrakk> v2 \<rbrakk> ~ SNum n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (6 subgoals):
 1. \<And>ia v1 n1 v2 n2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; ia \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2 ; atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 3. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 4. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 5. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 6. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1
i \<lbrakk> v2 \<rbrakk> ~ SNum n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1
i \<lbrakk> v2 \<rbrakk> ~ SNum n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
[PROOF STEP]
using  eval_v_weakening_x eval_e.intros  ce.fresh
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SNum n1
i \<lbrakk> v2 \<rbrakk> ~ SNum n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
atom x \<sharp> [ leq v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
\<lbrakk>?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?c \<rbrakk> ~ ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?a \<sharp> [ ?v ]\<^sup>c\<^sup>e = ?a \<sharp> ?v
?a \<sharp> [ ?opp ?ce1.0 ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?opp \<and> ?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [ ?ce1.0 @@ ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [#1?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [#2?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [| ?ce |]\<^sup>c\<^sup>e = ?a \<sharp> ?ce

goal (1 subgoal):
 1. i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)

goal (5 subgoals):
 1. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 2. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 3. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 4. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 5. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 2. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 3. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 4. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 5. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
case (eval_e_eqI i v1 n1 v2 n2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ n1
i \<lbrakk> v2 \<rbrakk> ~ n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ n2
atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (5 subgoals):
 1. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 2. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 3. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 4. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 5. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ n1
i \<lbrakk> v2 \<rbrakk> ~ n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ n2
atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ n1
i \<lbrakk> v2 \<rbrakk> ~ n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ n2
atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
using  eval_v_weakening_x eval_e.intros  ce.fresh
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ n1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ n1
i \<lbrakk> v2 \<rbrakk> ~ n2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ n2
atom x \<sharp> [ eq v1 v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
\<lbrakk>?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?c \<rbrakk> ~ ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?a \<sharp> [ ?v ]\<^sup>c\<^sup>e = ?a \<sharp> ?v
?a \<sharp> [ ?opp ?ce1.0 ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?opp \<and> ?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [ ?ce1.0 @@ ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [#1?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [#2?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [| ?ce |]\<^sup>c\<^sup>e = ?a \<sharp> ?ce

goal (1 subgoal):
 1. i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)

goal (4 subgoals):
 1. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 2. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 3. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 4. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 2. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 3. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 4. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
case (eval_e_fstI i v v1 v2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
atom x \<sharp> [#1v]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (4 subgoals):
 1. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#1v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
 2. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 3. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 4. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
atom x \<sharp> [#1v]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
atom x \<sharp> [#1v]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
[PROOF STEP]
using  eval_v_weakening_x eval_e.intros  ce.fresh
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
atom x \<sharp> [#1v]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
\<lbrakk>?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?c \<rbrakk> ~ ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?a \<sharp> [ ?v ]\<^sup>c\<^sup>e = ?a \<sharp> ?v
?a \<sharp> [ ?opp ?ce1.0 ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?opp \<and> ?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [ ?ce1.0 @@ ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [#1?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [#2?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [| ?ce |]\<^sup>c\<^sup>e = ?a \<sharp> ?ce

goal (1 subgoal):
 1. i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ v1

goal (3 subgoals):
 1. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 2. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 3. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 2. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 3. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
case (eval_e_sndI i v v1 v2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
atom x \<sharp> [#2v]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (3 subgoals):
 1. \<And>ia v v1 v2. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2 ; atom x \<sharp> [#2v]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
 2. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 3. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
atom x \<sharp> [#2v]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
atom x \<sharp> [#2v]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
[PROOF STEP]
using  eval_v_weakening_x eval_e.intros  ce.fresh
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SPair v1 v2
atom x \<sharp> [#2v]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
\<lbrakk>?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?c \<rbrakk> ~ ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?a \<sharp> [ ?v ]\<^sup>c\<^sup>e = ?a \<sharp> ?v
?a \<sharp> [ ?opp ?ce1.0 ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?opp \<and> ?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [ ?ce1.0 @@ ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [#1?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [#2?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [| ?ce |]\<^sup>c\<^sup>e = ?a \<sharp> ?ce

goal (1 subgoal):
 1. i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ v2

goal (2 subgoals):
 1. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 2. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 2. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
case (eval_e_concatI i v1 bv1 v2 bv2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (2 subgoals):
 1. \<And>ia v1 bv1 v2 bv2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; ia \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 ; atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
 2. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
[PROOF STEP]
using  eval_v_weakening_x eval_e.intros  ce.fresh
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
atom x \<sharp> [ v1 @@ v2 ]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
\<lbrakk>?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?c \<rbrakk> ~ ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?a \<sharp> [ ?v ]\<^sup>c\<^sup>e = ?a \<sharp> ?v
?a \<sharp> [ ?opp ?ce1.0 ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?opp \<and> ?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [ ?ce1.0 @@ ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [#1?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [#2?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [| ?ce |]\<^sup>c\<^sup>e = ?a \<sharp> ?ce

goal (1 subgoal):
 1. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2)

goal (1 subgoal):
 1. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
case (eval_e_lenI i v bv)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ SBitvec bv
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv
atom x \<sharp> [| v |]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. \<And>ia v bv. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ SBitvec bv ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv ; atom x \<sharp> [| v |]\<^sup>c\<^sup>e; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ SBitvec bv
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv
atom x \<sharp> [| v |]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ SBitvec bv
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv
atom x \<sharp> [| v |]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
using  eval_v_weakening_x eval_e.intros  ce.fresh
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ SBitvec bv
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ SBitvec bv
atom x \<sharp> [| v |]\<^sup>c\<^sup>e
i = i(x \<mapsto> s')
\<lbrakk>?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?c \<rbrakk> ~ ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?a \<sharp> [ ?v ]\<^sup>c\<^sup>e = ?a \<sharp> ?v
?a \<sharp> [ ?opp ?ce1.0 ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?opp \<and> ?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [ ?ce1.0 @@ ?ce2.0 ]\<^sup>c\<^sup>e = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
?a \<sharp> [#1?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [#2?ce]\<^sup>c\<^sup>e = ?a \<sharp> ?ce
?a \<sharp> [| ?ce |]\<^sup>c\<^sup>e = ?a \<sharp> ?ce

goal (1 subgoal):
 1. i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length bv))

goal:
No subgoals!
[PROOF STEP]
qed