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

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
proof(nominal_induct e arbitrary: s s' rule:ce.strong_induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2 x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 6. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (CE_val x)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (6 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2 x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 6. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_uniqueness eval_e_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SNum (n1 + n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SBool (n1 \<le> n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SBool (s1 = s2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v2. ?i \<lbrakk> ?v \<rbrakk> ~ SPair ?s v2  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v1. ?i \<lbrakk> ?v \<rbrakk> ~ SPair v1 ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv1 bv2. \<lbrakk>?s = SBitvec (bv1 @ bv2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec bv1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv. \<lbrakk>?s = SNum (int (length bv)); ?i \<lbrakk> ?v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (5 subgoals):
 1. \<And>x1a x2 x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1a x2 x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (CE_op opp x1 x2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (5 subgoals):
 1. \<And>x1a x2 x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[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 metis
[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 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a x2 x3 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[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. s = s'
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. opp = plus \<Longrightarrow> s = s'
 2. opp = leq \<Longrightarrow> s = s'
 3. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
opp = plus

goal (3 subgoals):
 1. opp = plus \<Longrightarrow> s = s'
 2. opp = leq \<Longrightarrow> s = s'
 3. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
hence a1:"eval_e i (CE_op Plus x1 x2) s" and a2:"eval_e i (CE_op Plus x1 x2) s'"
[PROOF STATE]
proof (prove)
using this:
opp = plus

goal (1 subgoal):
 1. i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  &&& i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
using CE_op
[PROOF STATE]
proof (prove)
using this:
opp = plus
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  &&& i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (3 subgoals):
 1. opp = plus \<Longrightarrow> s = s'
 2. opp = leq \<Longrightarrow> s = s'
 3. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using   eval_e_elims(2)[OF a1] eval_e_elims(2)[OF a2]
        CE_op eval_e_plusI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ plus x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
(\<And>n1 n2. \<lbrakk>s = SNum (n1 + n2); i \<lbrakk> x1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> x2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
(\<And>n1 n2. \<lbrakk>s' = SNum (n1 + n2); i \<lbrakk> x1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> x2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<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)

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

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> s = s'
 2. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. opp = leq \<Longrightarrow> s = s'
 2. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
opp = leq

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> s = s'
 2. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
hence a1:"eval_e i (CE_op LEq x1 x2) s" and a2:"eval_e i (CE_op LEq x1 x2) s'"
[PROOF STATE]
proof (prove)
using this:
opp = leq

goal (1 subgoal):
 1. i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  &&& i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
using CE_op
[PROOF STATE]
proof (prove)
using this:
opp = leq
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  &&& i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (2 subgoals):
 1. opp = leq \<Longrightarrow> s = s'
 2. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_uniqueness  eval_e_elims(3)[OF a1] eval_e_elims(3)[OF a2]
        CE_op eval_e_plusI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ leq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
(\<And>n1 n2. \<lbrakk>s = SBool (n1 \<le> n2); i \<lbrakk> x1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> x2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
(\<And>n1 n2. \<lbrakk>s' = SBool (n1 \<le> n2); i \<lbrakk> x1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> x2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<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)

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

goal (1 subgoal):
 1. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
opp = eq

goal (1 subgoal):
 1. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
hence a1:"eval_e i (CE_op Eq x1 x2) s" and a2:"eval_e i (CE_op Eq x1 x2) s'"
[PROOF STATE]
proof (prove)
using this:
opp = eq

goal (1 subgoal):
 1. i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  &&& i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
using CE_op
[PROOF STATE]
proof (prove)
using this:
opp = eq
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  &&& i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. opp = eq \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_uniqueness  eval_e_elims(4)[OF a1] eval_e_elims(4)[OF a2]
        CE_op eval_e_plusI
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ eq x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
(\<And>s1 s2. \<lbrakk>s = SBool (s1 = s2); i \<lbrakk> x1 \<rbrakk> ~ s1 ; i \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
(\<And>s1 s2. \<lbrakk>s' = SBool (s1 = s2); i \<lbrakk> x1 \<rbrakk> ~ s1 ; i \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ opp x1 x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<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)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s = s'

goal (4 subgoals):
 1. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (CE_concat x1 x2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (4 subgoals):
 1. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
hence a1:"eval_e i (CE_concat x1 x2) s" and a2:"eval_e i (CE_concat x1 x2) s'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  &&& i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
using CE_concat
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s  &&& i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (4 subgoals):
 1. \<And>x1a x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1a @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using  eval_e_elims(7)[OF a1] eval_e_elims(7)[OF a2] CE_concat eval_e_concatI rcl_val.eq_iff
[PROOF STATE]
proof (prove)
using this:
(\<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
(\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ ?s ; i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ ?s ; i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<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)
(SBitvec ?list = SBitvec ?lista) = (?list = ?lista)
(SNum ?int = SNum ?inta) = (?int = ?inta)
(SBool ?bool = SBool ?boola) = (?bool = ?boola)
(SPair ?rcl_val1.0 ?rcl_val2.0 = SPair ?rcl_val1a ?rcl_val2a) = (?rcl_val1.0 = ?rcl_val1a \<and> ?rcl_val2.0 = ?rcl_val2a)
(SCons ?list1.0 ?list2.0 ?rcl_val = SCons ?list1a ?list2a ?rcl_vala) = (?list1.0 = ?list1a \<and> ?list2.0 = ?list2a \<and> ?rcl_val = ?rcl_vala)
(SConsp ?list1.0 ?list2.0 ?b ?rcl_val = SConsp ?list1a ?list2a ?ba ?rcl_vala) = (?list1.0 = ?list1a \<and> ?list2.0 = ?list2a \<and> ?b = ?ba \<and> ?rcl_val = ?rcl_vala)
(SUnit = SUnit) = True
(SUt ?rcl_val = SUt ?rcl_vala) = (?rcl_val = ?rcl_vala)

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. (\<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>P. (\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>s s'. \<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ s ; i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<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>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
assume "\<And>P. (\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P"
[PROOF STATE]
proof (state)
this:
(\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<lbrakk>\<And>P. (\<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>P. (\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>s s'. \<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ s ; i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<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>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain bbs :: "bit list" and bbsa :: "bit list" where
      "i \<lbrakk> x2 \<rbrakk> ~ SBitvec bbs \<and> i \<lbrakk> x1 \<rbrakk> ~ SBitvec bbsa \<and> SBitvec (bbsa @ bbs) = s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bbs bbsa. i \<lbrakk> x2 \<rbrakk> ~ SBitvec bbs  \<and> i \<lbrakk> x1 \<rbrakk> ~ SBitvec bbsa  \<and> SBitvec (bbsa @ bbs) = s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<open>\<And>P. (\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P\<close>)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> x2 \<rbrakk> ~ SBitvec bbs  \<and> i \<lbrakk> x1 \<rbrakk> ~ SBitvec bbsa  \<and> SBitvec (bbsa @ bbs) = s'

goal (1 subgoal):
 1. \<lbrakk>\<And>P. (\<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>P. (\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>s s'. \<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ s ; i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<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>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
(* 93 ms *)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> x2 \<rbrakk> ~ SBitvec bbs  \<and> i \<lbrakk> x1 \<rbrakk> ~ SBitvec bbsa  \<and> SBitvec (bbsa @ bbs) = s'

goal (1 subgoal):
 1. \<lbrakk>\<And>P. (\<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>P. (\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>s s'. \<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ s ; i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<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>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> x2 \<rbrakk> ~ SBitvec bbs  \<and> i \<lbrakk> x1 \<rbrakk> ~ SBitvec bbsa  \<and> SBitvec (bbsa @ bbs) = s'
[PROOF STEP]
have "s' = s"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> x2 \<rbrakk> ~ SBitvec bbs  \<and> i \<lbrakk> x1 \<rbrakk> ~ SBitvec bbsa  \<and> SBitvec (bbsa @ bbs) = s'

goal (1 subgoal):
 1. s' = s
[PROOF STEP]
by (metis (no_types) \<open>\<And>P. (\<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P\<close> \<open>\<And>s' s. \<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ s ; i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'\<close> \<open>\<And>s' s. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'\<close> rcl_val.eq_iff(1))
[PROOF STATE]
proof (state)
this:
s' = s

goal (1 subgoal):
 1. \<lbrakk>\<And>P. (\<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>P. (\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>s s'. \<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ s ; i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<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>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
(* 125 ms *)
[PROOF STATE]
proof (state)
this:
s' = s

goal (1 subgoal):
 1. \<lbrakk>\<And>P. (\<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>P. (\<And>bv1 bv2. \<lbrakk>s' = SBitvec (bv1 @ bv2); i \<lbrakk> x1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> x2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P; \<And>s s'. \<lbrakk>i \<lbrakk> x1 \<rbrakk> ~ s ; i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2 \<rbrakk> ~ s ; i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [ x1 @@ x2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<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>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s' = s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s' = s

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

goal:
No subgoals!
[PROOF STEP]
(* 0.0 ms *)
[PROOF STATE]
proof (state)
this:
s = s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s = s'

goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (CE_fst x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_uniqueness
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [#1x]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by (meson eval_e_elims rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
s = s'

goal (2 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (CE_snd x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (2 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_uniqueness
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [#2x]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by (meson eval_e_elims rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
s = s'

goal (1 subgoal):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (CE_len x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s'

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

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using  eval_e_elims rcl_val.eq_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> x \<rbrakk> ~ ?s ; i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SNum (n1 + n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>n1 n2. \<lbrakk>?s = SBool (n1 \<le> n2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum n1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SBool (s1 = s2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v2. ?i \<lbrakk> ?v \<rbrakk> ~ SPair ?s v2  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>v1. ?i \<lbrakk> ?v \<rbrakk> ~ SPair v1 ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv1 bv2. \<lbrakk>?s = SBitvec (bv1 @ bv2); ?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec bv1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; \<And>bv. \<lbrakk>?s = SNum (int (length bv)); ?i \<lbrakk> ?v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(SBitvec ?list = SBitvec ?lista) = (?list = ?lista)
(SNum ?int = SNum ?inta) = (?int = ?inta)
(SBool ?bool = SBool ?boola) = (?bool = ?boola)
(SPair ?rcl_val1.0 ?rcl_val2.0 = SPair ?rcl_val1a ?rcl_val2a) = (?rcl_val1.0 = ?rcl_val1a \<and> ?rcl_val2.0 = ?rcl_val2a)
(SCons ?list1.0 ?list2.0 ?rcl_val = SCons ?list1a ?list2a ?rcl_vala) = (?list1.0 = ?list1a \<and> ?list2.0 = ?list2a \<and> ?rcl_val = ?rcl_vala)
(SConsp ?list1.0 ?list2.0 ?b ?rcl_val = SConsp ?list1a ?list2a ?ba ?rcl_vala) = (?list1.0 = ?list1a \<and> ?list2.0 = ?list2a \<and> ?b = ?ba \<and> ?rcl_val = ?rcl_vala)
(SUnit = SUnit) = True
(SUt ?rcl_val = SUt ?rcl_vala) = (?rcl_val = ?rcl_vala)

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<And>i v s P. \<lbrakk>i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SNum (n1 + n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SBool (n1 \<le> n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>s1 s2. \<lbrakk>s = SBool (s1 = s2); i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v2. i \<lbrakk> v \<rbrakk> ~ SPair s v2  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v1. i \<lbrakk> v \<rbrakk> ~ SPair v1 s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv. \<lbrakk>s = SNum (int (length bv)); i \<lbrakk> v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain bbs :: "rcl_val \<Rightarrow> ce \<Rightarrow> (x \<Rightarrow> rcl_val option) \<Rightarrow> bit list" where
      "\<forall>x0 x1 x2. (\<exists>v3. x0 = SNum (int (length v3)) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec v3 ) = (x0 = SNum (int (length (bbs x0 x1 x2))) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec (bbs x0 x1 x2) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bbs. \<forall>x0 x1 x2. (\<exists>v3. x0 = SNum (int (length v3)) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec v3 ) = (x0 = SNum (int (length (bbs x0 x1 x2))) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec (bbs x0 x1 x2) ) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by moura
[PROOF STATE]
proof (state)
this:
\<forall>x0 x1 x2. (\<exists>v3. x0 = SNum (int (length v3)) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec v3 ) = (x0 = SNum (int (length (bbs x0 x1 x2))) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec (bbs x0 x1 x2) )

goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<And>i v s P. \<lbrakk>i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SNum (n1 + n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SBool (n1 \<le> n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>s1 s2. \<lbrakk>s = SBool (s1 = s2); i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v2. i \<lbrakk> v \<rbrakk> ~ SPair s v2  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v1. i \<lbrakk> v \<rbrakk> ~ SPair v1 s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv. \<lbrakk>s = SNum (int (length bv)); i \<lbrakk> v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
(* 0.0 ms *)
[PROOF STATE]
proof (state)
this:
\<forall>x0 x1 x2. (\<exists>v3. x0 = SNum (int (length v3)) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec v3 ) = (x0 = SNum (int (length (bbs x0 x1 x2))) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec (bbs x0 x1 x2) )

goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<And>i v s P. \<lbrakk>i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SNum (n1 + n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SBool (n1 \<le> n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>s1 s2. \<lbrakk>s = SBool (s1 = s2); i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v2. i \<lbrakk> v \<rbrakk> ~ SPair s v2  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v1. i \<lbrakk> v \<rbrakk> ~ SPair v1 s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv. \<lbrakk>s = SNum (int (length bv)); i \<lbrakk> v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x0 x1 x2. (\<exists>v3. x0 = SNum (int (length v3)) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec v3 ) = (x0 = SNum (int (length (bbs x0 x1 x2))) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec (bbs x0 x1 x2) )
[PROOF STEP]
have "\<forall>f c r. \<not> f \<lbrakk> [| c |]\<^sup>c\<^sup>e \<rbrakk> ~ r \<or> r = SNum (int (length (bbs r c f))) \<and> f \<lbrakk> c \<rbrakk> ~ SBitvec (bbs r c f)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x0 x1 x2. (\<exists>v3. x0 = SNum (int (length v3)) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec v3 ) = (x0 = SNum (int (length (bbs x0 x1 x2))) \<and> x2 \<lbrakk> x1 \<rbrakk> ~ SBitvec (bbs x0 x1 x2) )

goal (1 subgoal):
 1. \<forall>f c r. \<not> f \<lbrakk> [| c |]\<^sup>c\<^sup>e \<rbrakk> ~ r  \<or> r = SNum (int (length (bbs r c f))) \<and> f \<lbrakk> c \<rbrakk> ~ SBitvec (bbs r c f)
[PROOF STEP]
by (meson eval_e_elims(8))
[PROOF STATE]
proof (state)
this:
\<forall>f c r. \<not> f \<lbrakk> [| c |]\<^sup>c\<^sup>e \<rbrakk> ~ r  \<or> r = SNum (int (length (bbs r c f))) \<and> f \<lbrakk> c \<rbrakk> ~ SBitvec (bbs r c f)

goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<And>i v s P. \<lbrakk>i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SNum (n1 + n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SBool (n1 \<le> n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>s1 s2. \<lbrakk>s = SBool (s1 = s2); i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v2. i \<lbrakk> v \<rbrakk> ~ SPair s v2  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v1. i \<lbrakk> v \<rbrakk> ~ SPair v1 s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv. \<lbrakk>s = SNum (int (length bv)); i \<lbrakk> v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
(* 46 ms *)
[PROOF STATE]
proof (state)
this:
\<forall>f c r. \<not> f \<lbrakk> [| c |]\<^sup>c\<^sup>e \<rbrakk> ~ r  \<or> r = SNum (int (length (bbs r c f))) \<and> f \<lbrakk> c \<rbrakk> ~ SBitvec (bbs r c f)

goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x \<rbrakk> ~ s ; i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> [| x |]\<^sup>c\<^sup>e \<rbrakk> ~ s' ; \<And>i v s P. \<lbrakk>i \<lbrakk> [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; i \<lbrakk> v \<rbrakk> ~ s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ plus v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SNum (n1 + n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ leq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>n1 n2. \<lbrakk>s = SBool (n1 \<le> n2); i \<lbrakk> v1 \<rbrakk> ~ SNum n1 ; i \<lbrakk> v2 \<rbrakk> ~ SNum n2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ eq v1 v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>s1 s2. \<lbrakk>s = SBool (s1 = s2); i \<lbrakk> v1 \<rbrakk> ~ s1 ; i \<lbrakk> v2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#1v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v2. i \<lbrakk> v \<rbrakk> ~ SPair s v2  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [#2v]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>v1. i \<lbrakk> v \<rbrakk> ~ SPair v1 s  \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v1 v2 s P. \<lbrakk>i \<lbrakk> [ v1 @@ v2 ]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv1 bv2. \<lbrakk>s = SBitvec (bv1 @ bv2); i \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1 ; i \<lbrakk> v2 \<rbrakk> ~ SBitvec bv2 \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>i v s P. \<lbrakk>i \<lbrakk> [| v |]\<^sup>c\<^sup>e \<rbrakk> ~ s ; \<And>bv. \<lbrakk>s = SNum (int (length bv)); i \<lbrakk> v \<rbrakk> ~ SBitvec bv \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; \<And>list lista. (SBitvec list = SBitvec lista) = (list = lista); \<And>int inta. (SNum int = SNum inta) = (int = inta); \<And>bool boola. (SBool bool = SBool boola) = (bool = boola); \<And>rcl_val1 rcl_val2 rcl_val1a rcl_val2a. (SPair rcl_val1 rcl_val2 = SPair rcl_val1a rcl_val2a) = (rcl_val1 = rcl_val1a \<and> rcl_val2 = rcl_val2a); \<And>list1 list2 rcl_val list1a list2a rcl_vala. (SCons list1 list2 rcl_val = SCons list1a list2a rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> rcl_val = rcl_vala); \<And>list1 list2 b rcl_val list1a list2a ba rcl_vala. (SConsp list1 list2 b rcl_val = SConsp list1a list2a ba rcl_vala) = (list1 = list1a \<and> list2 = list2a \<and> b = ba \<and> rcl_val = rcl_vala); (SUnit = SUnit) = True; \<And>rcl_val rcl_vala. (SUt rcl_val = SUt rcl_vala) = (rcl_val = rcl_vala)\<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>f c r. \<not> f \<lbrakk> [| c |]\<^sup>c\<^sup>e \<rbrakk> ~ r  \<or> r = SNum (int (length (bbs r c f))) \<and> f \<lbrakk> c \<rbrakk> ~ SBitvec (bbs r c f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>f c r. \<not> f \<lbrakk> [| c |]\<^sup>c\<^sup>e \<rbrakk> ~ r  \<or> r = SNum (int (length (bbs r c f))) \<and> f \<lbrakk> c \<rbrakk> ~ SBitvec (bbs r c f)

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by (metis (no_types) CE_len.hyps CE_len.prems(1) CE_len.prems(2) rcl_val.eq_iff(1))
[PROOF STATE]
proof (state)
this:
s = s'

goal:
No subgoals!
[PROOF STEP]
(* 31 ms *)
[PROOF STATE]
proof (state)
this:
s = s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s = s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfV_eval_bitvec:
  fixes v::v
  assumes  "P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : B_bitvec" and "P ; \<Gamma>  \<turnstile> i"
  shows "\<exists>bv. eval_v i v (SBitvec bv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv
[PROOF STEP]
obtain s where "i \<lbrakk> v \<rbrakk> ~  s \<and> wfRCV P s B_bitvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_bitvec \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_exist assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : B_bitvec
 P ; \<Gamma> \<turnstile> i

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

goal (1 subgoal):
 1. \<exists>bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_bitvec

goal (1 subgoal):
 1. \<exists>bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_bitvec
[PROOF STEP]
obtain bv where "s = SBitvec bv"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_bitvec

goal (1 subgoal):
 1. (\<And>bv. s = SBitvec bv \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_elims(1)[of P s]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_bitvec
\<lbrakk> P  \<turnstile> s : B_bitvec; \<And>bv. s = SBitvec bv \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

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

goal (1 subgoal):
 1. \<exists>bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_bitvec
s = SBitvec bv
[PROOF STEP]
show  ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_bitvec
s = SBitvec bv

goal (1 subgoal):
 1. \<exists>bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>bv. i \<lbrakk> v \<rbrakk> ~ SBitvec bv

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfV_eval_pair:
  fixes v::v
  assumes  "P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : B_pair b1 b2" and "P ; \<Gamma>  \<turnstile> i"
  shows "\<exists>s1 s2. eval_v i v (SPair s1 s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s1 s2. i \<lbrakk> v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s1 s2. i \<lbrakk> v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
obtain s  where "i \<lbrakk> v \<rbrakk> ~  s \<and> wfRCV P s (B_pair b1 b2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : [ b1 , b2 ]\<^sup>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_exist assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : [ b1 , b2 ]\<^sup>b
 P ; \<Gamma> \<turnstile> i

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

goal (1 subgoal):
 1. \<exists>s1 s2. i \<lbrakk> v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : [ b1 , b2 ]\<^sup>b

goal (1 subgoal):
 1. \<exists>s1 s2. i \<lbrakk> v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : [ b1 , b2 ]\<^sup>b
[PROOF STEP]
obtain s1 and s2 where "s = SPair s1 s2"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : [ b1 , b2 ]\<^sup>b

goal (1 subgoal):
 1. (\<And>s1 s2. s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_elims(2)[of P s]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : [ b1 , b2 ]\<^sup>b
\<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

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

goal (1 subgoal):
 1. \<exists>s1 s2. i \<lbrakk> v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : [ b1 , b2 ]\<^sup>b
s = SPair s1 s2
[PROOF STEP]
show  ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : [ b1 , b2 ]\<^sup>b
s = SPair s1 s2

goal (1 subgoal):
 1. \<exists>s1 s2. i \<lbrakk> v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>s1 s2. i \<lbrakk> v \<rbrakk> ~ SPair s1 s2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfV_eval_int:
  fixes v::v
  assumes  "P ;  B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : B_int" and "P ; \<Gamma>  \<turnstile> i"
  shows "\<exists>n. eval_v i v (SNum n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. i \<lbrakk> v \<rbrakk> ~ SNum n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. i \<lbrakk> v \<rbrakk> ~ SNum n
[PROOF STEP]
obtain s  where "i \<lbrakk> v \<rbrakk> ~  s \<and> wfRCV P s (B_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_int \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_exist assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?v \<rbrakk> ~ s  \<and>  ?P  \<turnstile> s : ?b
 P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : B_int
 P ; \<Gamma> \<turnstile> i

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

goal (1 subgoal):
 1. \<exists>n. i \<lbrakk> v \<rbrakk> ~ SNum n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_int

goal (1 subgoal):
 1. \<exists>n. i \<lbrakk> v \<rbrakk> ~ SNum n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_int
[PROOF STEP]
obtain n where "s = SNum n"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_int

goal (1 subgoal):
 1. (\<And>n. s = SNum n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfRCV_elims(3)[of P s]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_int
\<lbrakk> P  \<turnstile> s : B_int; \<And>n. s = SNum n \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

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

goal (1 subgoal):
 1. \<exists>n. i \<lbrakk> v \<rbrakk> ~ SNum n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_int
s = SNum n
[PROOF STEP]
show  ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s  \<and>  P  \<turnstile> s : B_int
s = SNum n

goal (1 subgoal):
 1. \<exists>n. i \<lbrakk> v \<rbrakk> ~ SNum n
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>n. i \<lbrakk> v \<rbrakk> ~ SNum n

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<exists>s. i \<lbrakk> v \<rbrakk> ~ s  \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
by auto