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

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[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 ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2 x3 b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x2 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x3 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x1a x2 x3 ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x1a : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x2 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 6. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
case (CE_val v)
[PROOF STATE]
proof (state)
this:
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ v ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

goal (6 subgoals):
 1. \<And>x b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2 x3 b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x2 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x3 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x1a x2 x3 ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x1a : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x2 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 6. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
obtain s where "i \<lbrakk> v \<rbrakk> ~ s \<and> P \<turnstile> s : b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfI_wfV_eval_v[of P B G v b i]  assms wfCE_elims(1)  [of P B G v b] CE_val
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; B ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f e : b
 P ; G \<turnstile> i
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ v ]\<^sup>c\<^sup>e : b ;  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v : b  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ v ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

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

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

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using CE_val   eval_e.intros(1)[of i v s ]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ v ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i
i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ s

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

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

goal (5 subgoals):
 1. \<And>x1a x2 x3 b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x2 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x3 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x1a x2 x3 ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x1a : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x2 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
consider "opp =Plus" | "opp=LEq" | "opp=Eq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>opp = plus \<Longrightarrow> thesis; opp = leq \<Longrightarrow> thesis; opp = eq \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using opp.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = plus \<Longrightarrow> ?P; ?y = leq \<Longrightarrow> ?P; ?y = eq \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<lbrakk>opp = plus \<Longrightarrow> thesis; opp = leq \<Longrightarrow> thesis; opp = eq \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>opp = plus \<Longrightarrow> ?thesis; opp = leq \<Longrightarrow> ?thesis; opp = eq \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (5 subgoals):
 1. \<And>x1a x2 x3 b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x2 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x3 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x3 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x1a x2 x3 ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x1a : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x2 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 5. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>opp = plus \<Longrightarrow> ?thesis; opp = leq \<Longrightarrow> ?thesis; opp = eq \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. opp = plus \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
opp = plus

goal (3 subgoals):
 1. opp = plus \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
hence  "wfCE P  B G v1 B_int \<and> wfCE P  B G v2 B_int"
[PROOF STATE]
proof (prove)
using this:
opp = plus

goal (1 subgoal):
 1.   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : B_int
[PROOF STEP]
using wfCE_elims(2) CE_op
[PROOF STATE]
proof (prove)
using this:
opp = plus
\<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>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ opp v1 v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

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

goal (3 subgoals):
 1. opp = plus \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : B_int
[PROOF STEP]
obtain s1 and s2 where *: "eval_e i v1 s1 \<and> wfRCV P s1 B_int \<and> eval_e i v2 s2 \<and> wfRCV P s2 B_int"
[PROOF STATE]
proof (prove)
using this:
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : B_int

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfI_wfV_eval_v  CE_op
[PROOF STATE]
proof (prove)
using this:
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : B_int
\<lbrakk> ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?\<Theta>  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ opp v1 v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

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

goal (3 subgoals):
 1. opp = plus \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int
[PROOF STEP]
obtain n1 and n2 where **:"s2=SNum n2 \<and> s1 = SNum n1"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int

goal (1 subgoal):
 1. (\<And>n2 n1. s2 = SNum n2 \<and> s1 = SNum n1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int
\<lbrakk> ?P  \<turnstile> ?s : B_bitvec; \<And>bv. ?s = SBitvec bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : [ ?b1.0 , ?b2.0 ]\<^sup>b; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2;  ?P  \<turnstile> s1 : ?b1.0;  ?P  \<turnstile> s2 : ?b2.0\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_int; \<And>n. ?s = SNum n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_bool; \<And>b. ?s = SBool b \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_id ?ss; \<And>dclist dc x b c s1. \<lbrakk>?s = SCons ?ss dc s1; AF_typedef ?ss dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_var ?bv; \<And>n. ?s = SUt n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_unit; ?s = SUnit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_app ?tyid ?b; \<And>bv dclist dc x b c s1. \<lbrakk>?s = SConsp ?tyid dc ?b s1; AF_typedef_poly ?tyid bv dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?tyid dc ?b s1, B_app ?tyid ?b);  ?P  \<turnstile> s1 : b[bv::=?b]\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBitvec ?bv : ?b; ?b = B_bitvec \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SNum ?n : ?b; ?b = B_int \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBool ?n : ?b; ?b = B_bool \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SPair ?s1.0 ?s2.0 : ?b; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?P  \<turnstile> ?s1.0 : b1;  ?P  \<turnstile> ?s2.0 : b2\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SCons ?s ?dc ?s1.0 : ?b; \<And>dclist x b c. \<lbrakk>?b = B_id ?s; AF_typedef ?s dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> ?s1.0 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : ?b; \<And>bv dclist x b c. \<lbrakk>?b = B_app ?s ?b'; AF_typedef_poly ?s bv dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?P  \<turnstile> ?s1.0 : b[bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUnit : ?b; ?b = B_unit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUt ?s1.0 : ?b; \<And>bv. ?b = B_var bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. (\<And>n2 n1. s2 = SNum n2 \<and> s1 = SNum n1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
s2 = SNum n2 \<and> s1 = SNum n1

goal (3 subgoals):
 1. opp = plus \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
hence "eval_e i (CE_op Plus v1 v2) (SNum (n1+n2))"
[PROOF STATE]
proof (prove)
using this:
s2 = SNum n2 \<and> s1 = SNum n1

goal (1 subgoal):
 1. i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
[PROOF STEP]
using eval_e_plusI * **
[PROOF STATE]
proof (prove)
using this:
s2 = SNum n2 \<and> s1 = SNum n1
\<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)
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int
s2 = SNum n2 \<and> s1 = SNum n1

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

goal (3 subgoals):
 1. opp = plus \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)

goal (3 subgoals):
 1. opp = plus \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
have "wfRCV P (SNum (n1+n2)) B_int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> SNum (n1 + n2) : B_int
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1.  P  \<turnstile> SNum (n1 + n2) : B_int
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> SNum (n1 + n2) : B_int

goal (3 subgoals):
 1. opp = plus \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
 P  \<turnstile> SNum (n1 + n2) : B_int
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
 P  \<turnstile> SNum (n1 + n2) : B_int

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
 P  \<turnstile> SNum (n1 + n2) : B_int
opp = plus

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using CE_op.prems(1) wfCE_elims(2)
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
 P  \<turnstile> SNum (n1 + n2) : B_int
opp = plus
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ opp v1 v2 ]\<^sup>c\<^sup>e : b
\<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

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
opp = leq

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
hence  "wfCE P  B G v1 B_int \<and> wfCE P  B G v2 B_int"
[PROOF STATE]
proof (prove)
using this:
opp = leq

goal (1 subgoal):
 1.   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : B_int
[PROOF STEP]
using wfCE_elims(3) CE_op
[PROOF STATE]
proof (prove)
using this:
opp = leq
\<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>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ opp v1 v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

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

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : B_int
[PROOF STEP]
obtain s1 and s2 where *: "eval_e i v1 s1 \<and> wfRCV P s1 B_int \<and> eval_e i v2 s2 \<and> wfRCV P s2 B_int"
[PROOF STATE]
proof (prove)
using this:
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : B_int

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfI_wfV_eval_v  CE_op
[PROOF STATE]
proof (prove)
using this:
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : B_int  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : B_int
\<lbrakk> ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?\<Theta>  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ opp v1 v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

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

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int
[PROOF STEP]
obtain n1 and n2 where **:"s2=SNum n2 \<and> s1 = SNum n1"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int

goal (1 subgoal):
 1. (\<And>n2 n1. s2 = SNum n2 \<and> s1 = SNum n1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int
\<lbrakk> ?P  \<turnstile> ?s : B_bitvec; \<And>bv. ?s = SBitvec bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : [ ?b1.0 , ?b2.0 ]\<^sup>b; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2;  ?P  \<turnstile> s1 : ?b1.0;  ?P  \<turnstile> s2 : ?b2.0\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_int; \<And>n. ?s = SNum n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_bool; \<And>b. ?s = SBool b \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_id ?ss; \<And>dclist dc x b c s1. \<lbrakk>?s = SCons ?ss dc s1; AF_typedef ?ss dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_var ?bv; \<And>n. ?s = SUt n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_unit; ?s = SUnit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_app ?tyid ?b; \<And>bv dclist dc x b c s1. \<lbrakk>?s = SConsp ?tyid dc ?b s1; AF_typedef_poly ?tyid bv dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?tyid dc ?b s1, B_app ?tyid ?b);  ?P  \<turnstile> s1 : b[bv::=?b]\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBitvec ?bv : ?b; ?b = B_bitvec \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SNum ?n : ?b; ?b = B_int \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBool ?n : ?b; ?b = B_bool \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SPair ?s1.0 ?s2.0 : ?b; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?P  \<turnstile> ?s1.0 : b1;  ?P  \<turnstile> ?s2.0 : b2\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SCons ?s ?dc ?s1.0 : ?b; \<And>dclist x b c. \<lbrakk>?b = B_id ?s; AF_typedef ?s dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> ?s1.0 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : ?b; \<And>bv dclist x b c. \<lbrakk>?b = B_app ?s ?b'; AF_typedef_poly ?s bv dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?P  \<turnstile> ?s1.0 : b[bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUnit : ?b; ?b = B_unit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUt ?s1.0 : ?b; \<And>bv. ?b = B_var bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. (\<And>n2 n1. s2 = SNum n2 \<and> s1 = SNum n1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
s2 = SNum n2 \<and> s1 = SNum n1

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
hence "eval_e i (CE_op LEq v1 v2) (SBool (n1 \<le> n2))"
[PROOF STATE]
proof (prove)
using this:
s2 = SNum n2 \<and> s1 = SNum n1

goal (1 subgoal):
 1. i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
[PROOF STEP]
using eval_e_leqI * **
[PROOF STATE]
proof (prove)
using this:
s2 = SNum n2 \<and> s1 = SNum n1
\<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)
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : B_int \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : B_int
s2 = SNum n2 \<and> s1 = SNum n1

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

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
have "wfRCV P (SBool (n1\<le>n2)) B_bool"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> SBool (n1 \<le> n2) : B_bool
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1.  P  \<turnstile> SBool (n1 \<le> n2) : B_bool
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> SBool (n1 \<le> n2) : B_bool

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 P  \<turnstile> SBool (n1 \<le> n2) : B_bool
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 P  \<turnstile> SBool (n1 \<le> n2) : B_bool

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 P  \<turnstile> SBool (n1 \<le> n2) : B_bool
opp = leq

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using CE_op.prems wfCE_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 P  \<turnstile> SBool (n1 \<le> n2) : B_bool
opp = leq
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ opp v1 v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i
\<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. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal (1 subgoal):
 1. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
opp = eq

goal (1 subgoal):
 1. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
opp = eq
[PROOF STEP]
obtain b2 where "wfCE P  B G v1 b2 \<and> wfCE P  B G v2 b2"
[PROOF STATE]
proof (prove)
using this:
opp = eq

goal (1 subgoal):
 1. (\<And>b2.   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : b2  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : b2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfCE_elims(9) CE_op
[PROOF STATE]
proof (prove)
using this:
opp = eq
\<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 ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ opp v1 v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

goal (1 subgoal):
 1. (\<And>b2.   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : b2  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : b2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : b2  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : b2

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

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : b2 \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : b2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfI_wfV_eval_v  CE_op
[PROOF STATE]
proof (prove)
using this:
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : b2  \<and>   P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : b2
\<lbrakk> ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?\<Theta>  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ opp v1 v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

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

goal (1 subgoal):
 1. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
hence "eval_e i (CE_op Eq v1 v2) (SBool (s1 = s2))"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : b2 \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : b2

goal (1 subgoal):
 1. i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
[PROOF STEP]
using eval_e_leqI *
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : b2 \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : b2
\<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)
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and>  P  \<turnstile> s1 : b2 \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s2 : b2

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

goal (1 subgoal):
 1. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)

goal (1 subgoal):
 1. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
have "wfRCV P (SBool (s1 = s2)) B_bool"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> SBool (s1 = s2) : B_bool
[PROOF STEP]
using wfRCV.intros
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv

goal (1 subgoal):
 1.  P  \<turnstile> SBool (s1 = s2) : B_bool
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> SBool (s1 = s2) : B_bool

goal (1 subgoal):
 1. opp = eq \<Longrightarrow> \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 P  \<turnstile> SBool (s1 = s2) : B_bool
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 P  \<turnstile> SBool (s1 = s2) : B_bool

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 P  \<turnstile> SBool (s1 = s2) : B_bool
opp = eq

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using CE_op.prems wfCE_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)
 P  \<turnstile> SBool (s1 = s2) : B_bool
opp = eq
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ opp v1 v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i
\<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. \<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ opp v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

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

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

goal (1 subgoal):
 1. (\<And>s1 s2. b = B_bitvec \<and> i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s1 : B_bitvec \<and>  P  \<turnstile> s2 : B_bitvec \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
    CE_concat
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ v1 @@ v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v2 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ v1 @@ v2 ]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

goal (1 subgoal):
 1. (\<And>s1 s2. b = B_bitvec \<and> i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s1 : B_bitvec \<and>  P  \<turnstile> s2 : B_bitvec \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson wfCE_elims(6))
[PROOF STATE]
proof (state)
this:
b = B_bitvec \<and> i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s1 : B_bitvec \<and>  P  \<turnstile> s2 : B_bitvec

goal (4 subgoals):
 1. \<And>x1a x2 b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x1a : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x1a \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b; \<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x2 : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x2 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [ x1a @@ x2 ]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 4. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
b = B_bitvec \<and> i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s1 : B_bitvec \<and>  P  \<turnstile> s2 : B_bitvec

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using  eval_e_concatI wfRCV.intros(1) wfRCV_elims
[PROOF STATE]
proof (prove)
using this:
b = B_bitvec \<and> i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s1 : B_bitvec \<and>  P  \<turnstile> s2 : B_bitvec
\<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)
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
\<lbrakk> ?P  \<turnstile> ?s : B_bitvec; \<And>bv. ?s = SBitvec bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : [ ?b1.0 , ?b2.0 ]\<^sup>b; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2;  ?P  \<turnstile> s1 : ?b1.0;  ?P  \<turnstile> s2 : ?b2.0\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_int; \<And>n. ?s = SNum n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_bool; \<And>b. ?s = SBool b \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_id ?ss; \<And>dclist dc x b c s1. \<lbrakk>?s = SCons ?ss dc s1; AF_typedef ?ss dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_var ?bv; \<And>n. ?s = SUt n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_unit; ?s = SUnit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s : B_app ?tyid ?b; \<And>bv dclist dc x b c s1. \<lbrakk>?s = SConsp ?tyid dc ?b s1; AF_typedef_poly ?tyid bv dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?tyid dc ?b s1, B_app ?tyid ?b);  ?P  \<turnstile> s1 : b[bv::=?b]\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBitvec ?bv : ?b; ?b = B_bitvec \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SNum ?n : ?b; ?b = B_int \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SBool ?n : ?b; ?b = B_bool \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SPair ?s1.0 ?s2.0 : ?b; \<And>b1 b2. \<lbrakk>?b = [ b1 , b2 ]\<^sup>b;  ?P  \<turnstile> ?s1.0 : b1;  ?P  \<turnstile> ?s2.0 : b2\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SCons ?s ?dc ?s1.0 : ?b; \<And>dclist x b c. \<lbrakk>?b = B_id ?s; AF_typedef ?s dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> ?s1.0 : b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : ?b; \<And>bv dclist x b c. \<lbrakk>?b = B_app ?s ?b'; AF_typedef_poly ?s bv dclist \<in> set ?P; (?dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (?P, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?P  \<turnstile> ?s1.0 : b[bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUnit : ?b; ?b = B_unit \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> SUt ?s1.0 : ?b; \<And>bv. ?b = B_var bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>b = B_bitvec \<and> i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s1 : B_bitvec \<and>  P  \<turnstile> s2 : B_bitvec; \<And>i v1 bv1 v2 bv2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2) ; \<And>P bv.  P  \<turnstile> SBitvec bv : B_bitvec; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_bitvec; \<And>bv. s = SBitvec bv \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s b1 b2 Pa. \<lbrakk> P  \<turnstile> s : [ b1 , b2 ]\<^sup>b; \<And>s1 s2. \<lbrakk>s = SPair s1 s2;  P  \<turnstile> s1 : b1;  P  \<turnstile> s2 : b2\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_int; \<And>n. s = SNum n \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_bool; \<And>b. s = SBool b \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s ss Pa. \<lbrakk> P  \<turnstile> s : B_id ss; \<And>dclist dc x b c s1. \<lbrakk>s = SCons ss dc s1; AF_typedef ss dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 : b\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s bv Pa. \<lbrakk> P  \<turnstile> s : B_var bv; \<And>n. s = SUt n \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_unit; s = SUnit \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s tyid b Pa. \<lbrakk> P  \<turnstile> s : B_app tyid b; \<And>bv dclist dc x ba c s1. \<lbrakk>s = SConsp tyid dc b s1; AF_typedef_poly tyid bv dclist \<in> set P; (dc, \<lbrace> x : ba  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (P, SConsp tyid dc b s1, B_app tyid b);  P  \<turnstile> s1 : ba[bv::=b]\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P bv b Pa. \<lbrakk> P  \<turnstile> SBitvec bv : b; b = B_bitvec \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P n b Pa. \<lbrakk> P  \<turnstile> SNum n : b; b = B_int \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P n b Pa. \<lbrakk> P  \<turnstile> SBool n : b; b = B_bool \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s1 s2 b Pa. \<lbrakk> P  \<turnstile> SPair s1 s2 : b; \<And>b1 b2. \<lbrakk>b = [ b1 , b2 ]\<^sup>b;  P  \<turnstile> s1 : b1;  P  \<turnstile> s2 : b2\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s dc s1 b Pa. \<lbrakk> P  \<turnstile> SCons s dc s1 : b; \<And>dclist x ba c. \<lbrakk>b = B_id s; AF_typedef s dclist \<in> set P; (dc, \<lbrace> x : ba  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 : ba\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s dc b' s1 b Pa. \<lbrakk> P  \<turnstile> SConsp s dc b' s1 : b; \<And>bv dclist x ba c. \<lbrakk>b = B_app s b'; AF_typedef_poly s bv dclist \<in> set P; (dc, \<lbrace> x : ba  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (P, SConsp s dc b' s1, B_app s b');  P  \<turnstile> s1 : ba[bv::=b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P b Pa. \<lbrakk> P  \<turnstile> SUnit : b; b = B_unit \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s1 b Pa. \<lbrakk> P  \<turnstile> SUt s1 : b; \<And>bv. b = B_var bv \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
obtain bbs :: "type_def list \<Rightarrow> rcl_val \<Rightarrow> bit list" where
      "\<forall>ts s. \<not> ts \<turnstile> s : B_bitvec \<or> s = SBitvec (bbs ts s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bbs. \<forall>ts s. \<not>  ts  \<turnstile> s : B_bitvec \<or> s = SBitvec (bbs ts s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_elims(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?P  \<turnstile> ?s : B_bitvec; \<And>bv. ?s = SBitvec bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. (\<And>bbs. \<forall>ts s. \<not>  ts  \<turnstile> s : B_bitvec \<or> s = SBitvec (bbs ts s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by moura
[PROOF STATE]
proof (state)
this:
\<forall>ts s. \<not>  ts  \<turnstile> s : B_bitvec \<or> s = SBitvec (bbs ts s)

goal (1 subgoal):
 1. \<lbrakk>b = B_bitvec \<and> i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s1 : B_bitvec \<and>  P  \<turnstile> s2 : B_bitvec; \<And>i v1 bv1 v2 bv2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2) ; \<And>P bv.  P  \<turnstile> SBitvec bv : B_bitvec; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_bitvec; \<And>bv. s = SBitvec bv \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s b1 b2 Pa. \<lbrakk> P  \<turnstile> s : [ b1 , b2 ]\<^sup>b; \<And>s1 s2. \<lbrakk>s = SPair s1 s2;  P  \<turnstile> s1 : b1;  P  \<turnstile> s2 : b2\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_int; \<And>n. s = SNum n \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_bool; \<And>b. s = SBool b \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s ss Pa. \<lbrakk> P  \<turnstile> s : B_id ss; \<And>dclist dc x b c s1. \<lbrakk>s = SCons ss dc s1; AF_typedef ss dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 : b\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s bv Pa. \<lbrakk> P  \<turnstile> s : B_var bv; \<And>n. s = SUt n \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_unit; s = SUnit \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s tyid b Pa. \<lbrakk> P  \<turnstile> s : B_app tyid b; \<And>bv dclist dc x ba c s1. \<lbrakk>s = SConsp tyid dc b s1; AF_typedef_poly tyid bv dclist \<in> set P; (dc, \<lbrace> x : ba  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (P, SConsp tyid dc b s1, B_app tyid b);  P  \<turnstile> s1 : ba[bv::=b]\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P bv b Pa. \<lbrakk> P  \<turnstile> SBitvec bv : b; b = B_bitvec \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P n b Pa. \<lbrakk> P  \<turnstile> SNum n : b; b = B_int \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P n b Pa. \<lbrakk> P  \<turnstile> SBool n : b; b = B_bool \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s1 s2 b Pa. \<lbrakk> P  \<turnstile> SPair s1 s2 : b; \<And>b1 b2. \<lbrakk>b = [ b1 , b2 ]\<^sup>b;  P  \<turnstile> s1 : b1;  P  \<turnstile> s2 : b2\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s dc s1 b Pa. \<lbrakk> P  \<turnstile> SCons s dc s1 : b; \<And>dclist x ba c. \<lbrakk>b = B_id s; AF_typedef s dclist \<in> set P; (dc, \<lbrace> x : ba  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 : ba\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s dc b' s1 b Pa. \<lbrakk> P  \<turnstile> SConsp s dc b' s1 : b; \<And>bv dclist x ba c. \<lbrakk>b = B_app s b'; AF_typedef_poly s bv dclist \<in> set P; (dc, \<lbrace> x : ba  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (P, SConsp s dc b' s1, B_app s b');  P  \<turnstile> s1 : ba[bv::=b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P b Pa. \<lbrakk> P  \<turnstile> SUnit : b; b = B_unit \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s1 b Pa. \<lbrakk> P  \<turnstile> SUt s1 : b; \<And>bv. b = B_var bv \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
(* 156 ms *)
[PROOF STATE]
proof (state)
this:
\<forall>ts s. \<not>  ts  \<turnstile> s : B_bitvec \<or> s = SBitvec (bbs ts s)

goal (1 subgoal):
 1. \<lbrakk>b = B_bitvec \<and> i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and>  P  \<turnstile> s1 : B_bitvec \<and>  P  \<turnstile> s2 : B_bitvec; \<And>i v1 bv1 v2 bv2. \<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (bv1 @ bv2) ; \<And>P bv.  P  \<turnstile> SBitvec bv : B_bitvec; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_bitvec; \<And>bv. s = SBitvec bv \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s b1 b2 Pa. \<lbrakk> P  \<turnstile> s : [ b1 , b2 ]\<^sup>b; \<And>s1 s2. \<lbrakk>s = SPair s1 s2;  P  \<turnstile> s1 : b1;  P  \<turnstile> s2 : b2\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_int; \<And>n. s = SNum n \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_bool; \<And>b. s = SBool b \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s ss Pa. \<lbrakk> P  \<turnstile> s : B_id ss; \<And>dclist dc x b c s1. \<lbrakk>s = SCons ss dc s1; AF_typedef ss dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 : b\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s bv Pa. \<lbrakk> P  \<turnstile> s : B_var bv; \<And>n. s = SUt n \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s Pa. \<lbrakk> P  \<turnstile> s : B_unit; s = SUnit \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s tyid b Pa. \<lbrakk> P  \<turnstile> s : B_app tyid b; \<And>bv dclist dc x ba c s1. \<lbrakk>s = SConsp tyid dc b s1; AF_typedef_poly tyid bv dclist \<in> set P; (dc, \<lbrace> x : ba  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (P, SConsp tyid dc b s1, B_app tyid b);  P  \<turnstile> s1 : ba[bv::=b]\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P bv b Pa. \<lbrakk> P  \<turnstile> SBitvec bv : b; b = B_bitvec \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P n b Pa. \<lbrakk> P  \<turnstile> SNum n : b; b = B_int \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P n b Pa. \<lbrakk> P  \<turnstile> SBool n : b; b = B_bool \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s1 s2 b Pa. \<lbrakk> P  \<turnstile> SPair s1 s2 : b; \<And>b1 b2. \<lbrakk>b = [ b1 , b2 ]\<^sup>b;  P  \<turnstile> s1 : b1;  P  \<turnstile> s2 : b2\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s dc s1 b Pa. \<lbrakk> P  \<turnstile> SCons s dc s1 : b; \<And>dclist x ba c. \<lbrakk>b = B_id s; AF_typedef s dclist \<in> set P; (dc, \<lbrace> x : ba  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 : ba\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s dc b' s1 b Pa. \<lbrakk> P  \<turnstile> SConsp s dc b' s1 : b; \<And>bv dclist x ba c. \<lbrakk>b = B_app s b'; AF_typedef_poly s bv dclist \<in> set P; (dc, \<lbrace> x : ba  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> (P, SConsp s dc b' s1, B_app s b');  P  \<turnstile> s1 : ba[bv::=b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P b Pa. \<lbrakk> P  \<turnstile> SUnit : b; b = B_unit \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa; \<And>P s1 b Pa. \<lbrakk> P  \<turnstile> SUt s1 : b; \<And>bv. b = B_var bv \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> Pa\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>ts s. \<not>  ts  \<turnstile> s : B_bitvec \<or> s = SBitvec (bbs ts s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>ts s. \<not>  ts  \<turnstile> s : B_bitvec \<or> s = SBitvec (bbs ts s)

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by (metis (no_types) "local.*" wfRCV_BBitvecI eval_e_concatI)
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal:
No subgoals!
[PROOF STEP]
(* 78 ms *)
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

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

goal (3 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#1x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 3. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#1v1]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [#1v1]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using  eval_e_fstI  wfRCV.intros wfCE_elims wfI_wfV_eval_v
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#1v1]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
\<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> ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?\<Theta>  \<turnstile> s : ?b

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [#1v1]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by (metis wfRCV_elims(2) rcl_val.eq_iff(4))
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [#1v1]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

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

goal (2 subgoals):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#2x]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
 2. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#2v1]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [#2v1]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using  eval_e_sndI  wfRCV.intros wfCE_elims wfI_wfV_eval_v
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f v1 : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> v1 \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [#2v1]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
\<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> ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?\<Theta>  \<turnstile> s : ?b

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [#2v1]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by (metis wfRCV_elims(2) rcl_val.eq_iff(4))
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [#2v1]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

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

goal (1 subgoal):
 1. \<And>x b. \<lbrakk>\<And>b. \<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b;   P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
using  eval_e_lenI  wfRCV.intros wfCE_elims wfI_wfV_eval_v wfV_eval_bitvec
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>  P ; B ; G \<turnstile>\<^sub>w\<^sub>f x : ?b ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> \<exists>s. i \<lbrakk> x \<rbrakk> ~ s  \<and>  P  \<turnstile> s : ?b
  P ; B ; G \<turnstile>\<^sub>w\<^sub>f [| x |]\<^sup>c\<^sup>e : b
 P ; G \<turnstile> i
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
\<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> ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ;  ?\<Theta> ; ?\<Gamma> \<turnstile> ?i\<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?\<Theta>  \<turnstile> s : ?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

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b
[PROOF STEP]
by (metis wfRCV_elims(1))
[PROOF STATE]
proof (state)
this:
\<exists>s. i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s  \<and>  P  \<turnstile> s : b

goal:
No subgoals!
[PROOF STEP]
qed