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

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> e \<rbrakk> ~ s
[PROOF STEP]
proof(nominal_induct e arbitrary: b rule:ce.strong_induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x ]\<^sup>c\<^sup>e)
 2. \<And>x1a x2 x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x3);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a x2 x3 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a x2 x3 ]\<^sup>c\<^sup>e)
 3. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x1a); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a @@ x2 ]\<^sup>c\<^sup>e)
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 6. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
case (CE_val v)
[PROOF STATE]
proof (state)
this:
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v ]\<^sup>c\<^sup>e : b

goal (6 subgoals):
 1. \<And>x b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x ]\<^sup>c\<^sup>e)
 2. \<And>x1a x2 x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x3);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a x2 x3 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a x2 x3 ]\<^sup>c\<^sup>e)
 3. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x1a); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a @@ x2 ]\<^sup>c\<^sup>e)
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 6. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v ]\<^sup>c\<^sup>e : b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v ]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
using eval_v_exist wfCE_elims eval_e.intros
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v ]\<^sup>c\<^sup>e : b
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b2.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b , b2 ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b1.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ b1 , ?b ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bitvec;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [| ?v1.0 |]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?opp ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?opp = plus; ?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?opp = leq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<And>b. \<lbrakk>?opp = eq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<And>b. \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
?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))

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

goal (5 subgoals):
 1. \<And>x1a x2 x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x3);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a x2 x3 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a x2 x3 ]\<^sup>c\<^sup>e)
 2. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x1a); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a @@ x2 ]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1a x2 x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x3);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a x2 x3 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a x2 x3 ]\<^sup>c\<^sup>e)
 2. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x1a); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a @@ x2 ]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
case (CE_op op v1 v2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ op v1 v2 ]\<^sup>c\<^sup>e : b

goal (5 subgoals):
 1. \<And>x1a x2 x3 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x3 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x3);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a x2 x3 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a x2 x3 ]\<^sup>c\<^sup>e)
 2. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x1a); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a @@ x2 ]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
proof(rule opp.exhaust)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?y = plus \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 2. ?y = leq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 3. ?y = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
assume \<open>op = Plus\<close>
[PROOF STATE]
proof (state)
this:
op = plus

goal (3 subgoals):
 1. ?y = plus \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 2. ?y = leq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 3. ?y = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
hence "P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int \<and> P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int \<and> b = B_int"
[PROOF STATE]
proof (prove)
using this:
op = plus

goal (1 subgoal):
 1.   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_int
[PROOF STEP]
using wfCE_elims CE_op
[PROOF STATE]
proof (prove)
using this:
op = plus
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b2.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b , b2 ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b1.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ b1 , ?b ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bitvec;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [| ?v1.0 |]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?opp ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?opp = plus; ?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?opp = leq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<And>b. \<lbrakk>?opp = eq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<And>b. \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ op v1 v2 ]\<^sup>c\<^sup>e : b

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

goal (3 subgoals):
 1. ?y = plus \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 2. ?y = leq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 3. ?y = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_int
[PROOF STEP]
obtain n1 and n2 where "eval_e i v1 (SNum n1) \<and> eval_e i v2 (SNum n2)"
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_int

goal (1 subgoal):
 1. (\<And>n1 n2. i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using CE_op eval_v_exist wfV_eval_int
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_int
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ op v1 v2 ]\<^sup>c\<^sup>e : b
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
\<lbrakk> ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : B_int ;  ?P ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>n. ?i \<lbrakk> ?v \<rbrakk> ~ SNum n

goal (1 subgoal):
 1. (\<And>n1 n2. i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis wfI_wfCE_eval_e wfRCV_elims(3))
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2

goal (3 subgoals):
 1. ?y = plus \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 2. ?y = leq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 3. ?y = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
[PROOF STEP]
show \<open>\<exists>a. eval_e i (CE_op op v1 v2) a\<close>
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
using eval_e_plusI[of i v1 _ v2] \<open>op=Plus\<close>
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum ?n1.0 ; i \<lbrakk> v2 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
op = plus

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a

goal (2 subgoals):
 1. op = leq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 2. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op = leq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 2. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
assume \<open>op = LEq\<close>
[PROOF STATE]
proof (state)
this:
op = leq

goal (2 subgoals):
 1. op = leq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 2. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
hence "P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int \<and> P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int \<and> b = B_bool"
[PROOF STATE]
proof (prove)
using this:
op = leq

goal (1 subgoal):
 1.   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_bool
[PROOF STEP]
using wfCE_elims CE_op
[PROOF STATE]
proof (prove)
using this:
op = leq
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b2.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b , b2 ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b1.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ b1 , ?b ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bitvec;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [| ?v1.0 |]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?opp ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?opp = plus; ?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?opp = leq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<And>b. \<lbrakk>?opp = eq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<And>b. \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ op v1 v2 ]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1.   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_bool
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_bool

goal (2 subgoals):
 1. op = leq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 2. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_bool
[PROOF STEP]
obtain n1 and n2 where "eval_e i v1 (SNum n1) \<and> eval_e i v2 (SNum n2)"
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_bool

goal (1 subgoal):
 1. (\<And>n1 n2. i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using CE_op eval_v_exist wfV_eval_int
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int  \<and> b = B_bool
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ op v1 v2 ]\<^sup>c\<^sup>e : b
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
\<lbrakk> ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : B_int ;  ?P ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>n. ?i \<lbrakk> ?v \<rbrakk> ~ SNum n

goal (1 subgoal):
 1. (\<And>n1 n2. i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis wfI_wfCE_eval_e wfRCV_elims(3))
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2

goal (2 subgoals):
 1. op = leq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
 2. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
[PROOF STEP]
show \<open>\<exists>a. eval_e i (CE_op op v1 v2) a\<close>
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
using eval_e_leqI[of i v1 _ v2] eval_v_exist \<open>op=LEq\<close> CE_op
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SNum n1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SNum n2
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SNum ?n1.0 ; i \<lbrakk> v2 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
op = leq
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ op v1 v2 ]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a

goal (1 subgoal):
 1. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
assume \<open>op = Eq\<close>
[PROOF STATE]
proof (state)
this:
op = eq

goal (1 subgoal):
 1. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
op = eq
[PROOF STEP]
obtain b1 where  "P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1 \<and> P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b1 \<and> b = B_bool"
[PROOF STATE]
proof (prove)
using this:
op = eq

goal (1 subgoal):
 1. (\<And>b1.   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b1  \<and> b = B_bool \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfCE_elims CE_op
[PROOF STATE]
proof (prove)
using this:
op = eq
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b2.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b , b2 ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b1.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ b1 , ?b ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bitvec;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [| ?v1.0 |]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?opp ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?opp = plus; ?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?opp = leq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<And>b. \<lbrakk>?opp = eq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<And>b. \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ op v1 v2 ]\<^sup>c\<^sup>e : b

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

goal (1 subgoal):
 1. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b1  \<and> b = B_bool
[PROOF STEP]
obtain s1 and s2 where "eval_e i v1 s1 \<and> eval_e i v2 s2"
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b1  \<and> b = B_bool

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using CE_op eval_v_exist wfV_eval_int
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : b1  \<and>   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : b1  \<and> b = B_bool
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ op v1 v2 ]\<^sup>c\<^sup>e : b
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
\<lbrakk> ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : B_int ;  ?P ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>n. ?i \<lbrakk> ?v \<rbrakk> ~ SNum n

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

goal (1 subgoal):
 1. op = eq \<Longrightarrow> \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2
[PROOF STEP]
show \<open>\<exists>a. eval_e i (CE_op op v1 v2) a\<close>
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
using eval_e_eqI[of i v1 _ v2] eval_v_exist \<open>op=Eq\<close> CE_op
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s1.0 ; i \<lbrakk> v2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
op = eq
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ op v1 v2 ]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. i \<lbrakk> [ op v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a

goal (4 subgoals):
 1. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x1a); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a @@ x2 ]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x1a); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a @@ x2 ]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
case (CE_concat v1 v2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 @@ v2 ]\<^sup>c\<^sup>e : b

goal (4 subgoals):
 1. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x1a); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a @@ x2 ]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 @@ v2 ]\<^sup>c\<^sup>e : b
[PROOF STEP]
obtain bv1 and bv2 where "eval_e i v1 (SBitvec bv1) \<and> eval_e i v2 (SBitvec bv2)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 @@ v2 ]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. (\<And>bv1 bv2. i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfV_eval_bitvec  wfCE_elims(6)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 @@ v2 ]\<^sup>c\<^sup>e : b
\<lbrakk> ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : B_bitvec ;  ?P ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>bv. ?i \<lbrakk> ?v \<rbrakk> ~ SBitvec bv
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bitvec;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>bv1 bv2. i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson eval_e_elims(7) wfI_wfCE_eval_e)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2

goal (4 subgoals):
 1. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x1a : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x1a); \<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x2 : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x2);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [ x1a @@ x2 ]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
using  eval_e.intros
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1  \<and> i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2
?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))

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

goal (3 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
case (CE_fst ce)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1ce]\<^sup>c\<^sup>e : b

goal (3 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1ce]\<^sup>c\<^sup>e : b
[PROOF STEP]
obtain b2 where b:"P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : B_pair b b2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1ce]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. (\<And>b2.   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : [ b , b2 ]\<^sup>b  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfCE_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1ce]\<^sup>c\<^sup>e : b
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b2.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b , b2 ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b1.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ b1 , ?b ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bitvec;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [| ?v1.0 |]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?opp ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?opp = plus; ?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?opp = leq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<And>b. \<lbrakk>?opp = eq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<And>b. \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (3 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : [ b , b2 ]\<^sup>b
[PROOF STEP]
obtain s where s:"i \<lbrakk> ce \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : [ b , b2 ]\<^sup>b

goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> ce \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using CE_fst
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : [ b , b2 ]\<^sup>b
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1ce]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> ce \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> ce \<rbrakk> ~ s

goal (3 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> ce \<rbrakk> ~ s
[PROOF STEP]
obtain s1 and s2 where "s = (SPair s1 s2)"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> ce \<rbrakk> ~ s

goal (1 subgoal):
 1. (\<And>s1 s2. s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_e_elims(4)  CE_fst wfI_wfCE_eval_e[of P B \<Gamma> ce "B_pair b b2" i,OF b] wfRCV_elims(2)[of P s b b2]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> ce \<rbrakk> ~ s
\<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> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1ce]\<^sup>c\<^sup>e : b
 P ; \<Gamma> \<turnstile> i \<Longrightarrow> \<exists>s. i \<lbrakk> ce \<rbrakk> ~ s  \<and>  P  \<turnstile> s : [ b , b2 ]\<^sup>b
\<lbrakk> P  \<turnstile> s : [ b , b2 ]\<^sup>b; \<And>s1 s2. \<lbrakk>s = SPair s1 s2;  P  \<turnstile> s1 : b;  P  \<turnstile> s2 : b2\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. (\<And>s1 s2. s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis eval_e_uniqueness)
[PROOF STATE]
proof (state)
this:
s = SPair s1 s2

goal (3 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#1x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = SPair s1 s2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s = SPair s1 s2

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [#1ce]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
using s eval_e.intros
[PROOF STATE]
proof (prove)
using this:
s = SPair s1 s2
i \<lbrakk> ce \<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))

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

goal (2 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
case (CE_snd ce)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2ce]\<^sup>c\<^sup>e : b

goal (2 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2ce]\<^sup>c\<^sup>e : b
[PROOF STEP]
obtain b1 where b:"P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : B_pair b1 b"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2ce]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. (\<And>b1.   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : [ b1 , b ]\<^sup>b  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfCE_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2ce]\<^sup>c\<^sup>e : b
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b2.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b , b2 ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b1.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ b1 , ?b ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bitvec;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [| ?v1.0 |]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?opp ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?opp = plus; ?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?opp = leq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<And>b. \<lbrakk>?opp = eq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<And>b. \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (2 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : [ b1 , b ]\<^sup>b
[PROOF STEP]
obtain s where s:"i \<lbrakk> ce \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : [ b1 , b ]\<^sup>b

goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> ce \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using CE_snd
[PROOF STATE]
proof (prove)
using this:
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : [ b1 , b ]\<^sup>b
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2ce]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> ce \<rbrakk> ~ s  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> ce \<rbrakk> ~ s

goal (2 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> ce \<rbrakk> ~ s
[PROOF STEP]
obtain s1 and s2 where "s = (SPair s1 s2)"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> ce \<rbrakk> ~ s

goal (1 subgoal):
 1. (\<And>s1 s2. s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_e_elims(5)  CE_snd wfI_wfCE_eval_e[of P B \<Gamma> ce "B_pair b1 b" i,OF b] wfRCV_elims(2)[of P s b b1]
      eval_e_uniqueness
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> ce \<rbrakk> ~ s
\<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> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> ce \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2ce]\<^sup>c\<^sup>e : b
 P ; \<Gamma> \<turnstile> i \<Longrightarrow> \<exists>s. i \<lbrakk> ce \<rbrakk> ~ s  \<and>  P  \<turnstile> s : [ b1 , b ]\<^sup>b
\<lbrakk> P  \<turnstile> s : [ b , b1 ]\<^sup>b; \<And>s1 s2. \<lbrakk>s = SPair s1 s2;  P  \<turnstile> s1 : b;  P  \<turnstile> s2 : b1\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk>?i \<lbrakk> ?e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?e \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'

goal (1 subgoal):
 1. (\<And>s1 s2. s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis wfRCV_elims(2))
[PROOF STATE]
proof (state)
this:
s = SPair s1 s2

goal (2 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [#2x]\<^sup>c\<^sup>e)
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = SPair s1 s2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s = SPair s1 s2

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [#2ce]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
using s eval_e.intros
[PROOF STATE]
proof (prove)
using this:
s = SPair s1 s2
i \<lbrakk> ce \<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))

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

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
case (CE_len v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| v1 |]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| v1 |]\<^sup>c\<^sup>e : b
[PROOF STEP]
obtain bv1  where "eval_e i v1 (SBitvec bv1)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| v1 |]\<^sup>c\<^sup>e : b

goal (1 subgoal):
 1. (\<And>bv1. i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfV_eval_bitvec  CE_len  wfCE_elims eval_e_uniqueness
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| v1 |]\<^sup>c\<^sup>e : b
\<lbrakk> ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : B_bitvec ;  ?P ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>bv. ?i \<lbrakk> ?v \<rbrakk> ~ SBitvec bv
\<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : ?b \<rbrakk> \<Longrightarrow> \<exists>a. i \<lbrakk> v1 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
  P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| v1 |]\<^sup>c\<^sup>e : b
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v ]\<^sup>c\<^sup>e : ?b ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#1?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b2.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ ?b , b2 ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [#2?v1.0]\<^sup>c\<^sup>e : ?b ; \<And>b1.   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : [ b1 , ?b ]\<^sup>b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_bitvec;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [| ?v1.0 |]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_bitvec \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ ?opp ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<lbrakk>?opp = plus; ?b = B_int;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?opp = leq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : B_int ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : B_int \<rbrakk> \<Longrightarrow> ?P; \<And>b. \<lbrakk>?opp = eq; ?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e : ?b ; \<And>b. \<lbrakk>?b = B_bool;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> ?e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?e \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'

goal (1 subgoal):
 1. (\<And>bv1. i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis eval_e_elims(7) wfCE_concatI wfI_wfCE_eval_e)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk> P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f x : b \<rbrakk> \<Longrightarrow> Ex (eval_e i x);  P ; \<Gamma> \<turnstile> i;   P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b \<rbrakk> \<Longrightarrow> Ex (eval_e i [| x |]\<^sup>c\<^sup>e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1

goal (1 subgoal):
 1. \<exists>a. i \<lbrakk> [| v1 |]\<^sup>c\<^sup>e \<rbrakk> ~ a
[PROOF STEP]
using  eval_e.intros
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1
?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))

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

goal:
No subgoals!
[PROOF STEP]
qed