[STATEMENT]
lemma is_satis_len_imp:
  assumes "i \<Turnstile> (CE_val (V_var x)  ==  CE_val (V_lit (L_num (int (length v)))) )" (is "is_satis i ?c1")
  shows "i \<Turnstile> (CE_val (V_var x)  ==  CE_len [V_lit (L_bitvec v)]\<^sup>c\<^sup>e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
have *:"eval_c i ?c1 True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using assms is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have  "eval_e i (CE_val (V_lit (L_num (int (length v))))) (SNum (int (length v)))"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1. i \<lbrakk> [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))
[PROOF STEP]
using eval_e_elims(1) eval_v_elims eval_l.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

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

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
hence "eval_e i (CE_val (V_var x)) (SNum (int (length v)))"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))

goal (1 subgoal):
 1. i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))
[PROOF STEP]
using eval_c_elims(7)[OF *]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))
(\<And>sv1 sv2. \<lbrakk>True = (sv1 = sv2); i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1 ; i \<lbrakk> [ [ L_num (int (length v)) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P

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

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
have "eval_e i (CE_len [V_lit (L_bitvec v)]\<^sup>c\<^sup>e) (SNum (int (length v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))
[PROOF STEP]
using eval_e_elims(7) eval_v_elims eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<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> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

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

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))
i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))
i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
using eval_c.intros is_satis.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))
i \<lbrakk> [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length v))
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_plus_imp:
  assumes "i \<Turnstile> (CE_val (V_var x) ==  CE_val (V_lit (L_num (n1+n2))))" (is "is_satis i ?c1")
  shows   "i \<Turnstile> (CE_val (V_var x)  ==  CE_op Plus ([V_lit (L_num n1)]\<^sup>c\<^sup>e) ([V_lit (L_num n2)]\<^sup>c\<^sup>e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have *:"eval_c i ?c1 True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using assms is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have  "eval_e i (CE_val (V_lit (L_num (n1+n2)))) (SNum (n1+n2))"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1. i \<lbrakk> [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
[PROOF STEP]
using eval_e_elims(1) eval_v_elims eval_l.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

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

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
hence "eval_e i (CE_val (V_var x)) (SNum (n1+n2))"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)

goal (1 subgoal):
 1. i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
[PROOF STEP]
using eval_c_elims(7)[OF *]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
(\<And>sv1 sv2. \<lbrakk>True = (sv1 = sv2); i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1 ; i \<lbrakk> [ [ L_num (n1 + n2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P

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

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have "eval_e i (CE_op Plus ([V_lit (L_num n1)]\<^sup>c\<^sup>e) ([V_lit (L_num n2)]\<^sup>c\<^sup>e)) (SNum (n1+n2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
[PROOF STEP]
using eval_e_elims(7) eval_v_elims eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<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> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

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

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
i \<lbrakk> [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
i \<lbrakk> [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
using eval_c.intros is_satis.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
i \<lbrakk> [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (n1 + n2)
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ plus [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_leq_imp:
  assumes "i \<Turnstile> (CE_val (V_var x) ==  CE_val (V_lit (if (n1 \<le> n2) then L_true else L_false)))" (is "is_satis i ?c1")
  shows   "i \<Turnstile> (CE_val (V_var x)  ==  CE_op LEq [(V_lit (L_num n1))]\<^sup>c\<^sup>e [(V_lit (L_num n2))]\<^sup>c\<^sup>e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have *:"eval_c i ?c1 True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using assms is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have  "eval_e i (CE_val (V_lit ((if (n1 \<le> n2) then L_true else L_false)))) (SBool (n1\<le>n2))"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1. i \<lbrakk> [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
[PROOF STEP]
using eval_e_elims(1) eval_v_elims eval_l.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. i \<lbrakk> [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
[PROOF STEP]
by (metis (full_types) eval_e.intros(1) eval_v_litI)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
hence "eval_e i (CE_val (V_var x)) (SBool (n1\<le>n2))"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)

goal (1 subgoal):
 1. i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
[PROOF STEP]
using eval_c_elims(7)[OF *]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
(\<And>sv1 sv2. \<lbrakk>True = (sv1 = sv2); i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1 ; i \<lbrakk> [ [ if n1 \<le> n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P

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

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have "eval_e i (CE_op LEq [(V_lit (L_num n1))]\<^sup>c\<^sup>e [(V_lit (L_num n2) )]\<^sup>c\<^sup>e) (SBool (n1\<le>n2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
[PROOF STEP]
using eval_e_elims(3) eval_v_elims eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<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> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

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

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
i \<lbrakk> [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
i \<lbrakk> [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
using eval_c.intros is_satis.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
i \<lbrakk> [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 \<le> n2)
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ leq [ [ L_num n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_lit_inj:
  fixes n1::l and n2::l
  assumes "\<lbrakk> n1  \<rbrakk> = s" and "\<lbrakk> n2 \<rbrakk> = s"
  shows "n1=n2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> n1 \<rbrakk>  = s
\<lbrakk> n2 \<rbrakk>  = s

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
proof(nominal_induct s rule: rcl_val.strong_induct)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBitvec x; \<lbrakk> n2 \<rbrakk>  = SBitvec x\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SNum x; \<lbrakk> n2 \<rbrakk>  = SNum x\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBool x; \<lbrakk> n2 \<rbrakk>  = SBool x\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 6. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 7. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 8. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
case (SBitvec x)
[PROOF STATE]
proof (state)
this:
\<lbrakk> n1 \<rbrakk>  = SBitvec x
\<lbrakk> n2 \<rbrakk>  = SBitvec x

goal (8 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBitvec x; \<lbrakk> n2 \<rbrakk>  = SBitvec x\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SNum x; \<lbrakk> n2 \<rbrakk>  = SNum x\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBool x; \<lbrakk> n2 \<rbrakk>  = SBool x\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 6. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 7. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 8. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> n1 \<rbrakk>  = SBitvec x
\<lbrakk> n2 \<rbrakk>  = SBitvec x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> n1 \<rbrakk>  = SBitvec x
\<lbrakk> n2 \<rbrakk>  = SBitvec x

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> n1 \<rbrakk>  = SBitvec x
\<lbrakk> n2 \<rbrakk>  = SBitvec x
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
n1 = n2

goal (7 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SNum x; \<lbrakk> n2 \<rbrakk>  = SNum x\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBool x; \<lbrakk> n2 \<rbrakk>  = SBool x\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 6. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 7. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SNum x; \<lbrakk> n2 \<rbrakk>  = SNum x\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBool x; \<lbrakk> n2 \<rbrakk>  = SBool x\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 6. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 7. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
case (SNum x)
[PROOF STATE]
proof (state)
this:
\<lbrakk> n1 \<rbrakk>  = SNum x
\<lbrakk> n2 \<rbrakk>  = SNum x

goal (7 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SNum x; \<lbrakk> n2 \<rbrakk>  = SNum x\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBool x; \<lbrakk> n2 \<rbrakk>  = SBool x\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 6. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 7. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> n1 \<rbrakk>  = SNum x
\<lbrakk> n2 \<rbrakk>  = SNum x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> n1 \<rbrakk>  = SNum x
\<lbrakk> n2 \<rbrakk>  = SNum x

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> n1 \<rbrakk>  = SNum x
\<lbrakk> n2 \<rbrakk>  = SNum x
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
n1 = n2

goal (6 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBool x; \<lbrakk> n2 \<rbrakk>  = SBool x\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 6. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBool x; \<lbrakk> n2 \<rbrakk>  = SBool x\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 6. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
case (SBool x)
[PROOF STATE]
proof (state)
this:
\<lbrakk> n1 \<rbrakk>  = SBool x
\<lbrakk> n2 \<rbrakk>  = SBool x

goal (6 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SBool x; \<lbrakk> n2 \<rbrakk>  = SBool x\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 6. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> n1 \<rbrakk>  = SBool x
\<lbrakk> n2 \<rbrakk>  = SBool x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> n1 \<rbrakk>  = SBool x
\<lbrakk> n2 \<rbrakk>  = SBool x

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> n1 \<rbrakk>  = SBool x
\<lbrakk> n2 \<rbrakk>  = SBool x
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
n1 = n2

goal (5 subgoals):
 1. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
case (SPair x1a x2a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SPair x1a x2a
\<lbrakk> n2 \<rbrakk>  = SPair x1a x2a

goal (5 subgoals):
 1. \<And>x1a x2a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SPair x1a x2a; \<lbrakk> n2 \<rbrakk>  = SPair x1a x2a\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 5. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SPair x1a x2a
\<lbrakk> n2 \<rbrakk>  = SPair x1a x2a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SPair x1a x2a
\<lbrakk> n2 \<rbrakk>  = SPair x1a x2a

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x1a; \<lbrakk> n2 \<rbrakk>  = x1a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x2a; \<lbrakk> n2 \<rbrakk>  = x2a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SPair x1a x2a
\<lbrakk> n2 \<rbrakk>  = SPair x1a x2a
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
n1 = n2

goal (4 subgoals):
 1. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
case (SCons x1a x2a x3a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a
\<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a

goal (4 subgoals):
 1. \<And>x1a x2a x3a. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a; \<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 4. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a
\<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a
\<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x3a; \<lbrakk> n2 \<rbrakk>  = x3a\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SCons x1a x2a x3a
\<lbrakk> n2 \<rbrakk>  = SCons x1a x2a x3a
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
n1 = n2

goal (3 subgoals):
 1. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
case (SConsp x1a x2a x3a x4)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4
\<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4

goal (3 subgoals):
 1. \<And>x1a x2a x3a x4. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4; \<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 3. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4
\<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4
\<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x4; \<lbrakk> n2 \<rbrakk>  = x4\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SConsp x1a x2a x3a x4
\<lbrakk> n2 \<rbrakk>  = SConsp x1a x2a x3a x4
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
n1 = n2

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
case SUnit
[PROOF STATE]
proof (state)
this:
\<lbrakk> n1 \<rbrakk>  = SUnit
\<lbrakk> n2 \<rbrakk>  = SUnit

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk> n1 \<rbrakk>  = SUnit; \<lbrakk> n2 \<rbrakk>  = SUnit\<rbrakk> \<Longrightarrow> n1 = n2
 2. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> n1 \<rbrakk>  = SUnit
\<lbrakk> n2 \<rbrakk>  = SUnit
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> n1 \<rbrakk>  = SUnit
\<lbrakk> n2 \<rbrakk>  = SUnit

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> n1 \<rbrakk>  = SUnit
\<lbrakk> n2 \<rbrakk>  = SUnit
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
n1 = n2

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
case (SUt x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SUt x
\<lbrakk> n2 \<rbrakk>  = SUt x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2; \<lbrakk> n1 \<rbrakk>  = SUt x; \<lbrakk> n2 \<rbrakk>  = SUt x\<rbrakk> \<Longrightarrow> n1 = n2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SUt x
\<lbrakk> n2 \<rbrakk>  = SUt x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SUt x
\<lbrakk> n2 \<rbrakk>  = SUt x

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using eval_l.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk> n1 \<rbrakk>  = x; \<lbrakk> n2 \<rbrakk>  = x\<rbrakk> \<Longrightarrow> n1 = n2
\<lbrakk> n1 \<rbrakk>  = SUt x
\<lbrakk> n2 \<rbrakk>  = SUt x
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
[PROOF STATE]
proof (state)
this:
n1 = n2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_e_lit_inj:
  fixes n1::l and n2::l
  assumes "i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s" and "i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s"
  shows "n1=n2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
using eval_lit_inj assms eval_e_elims eval_v_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk> ?n1.0 \<rbrakk>  = ?s; \<lbrakk> ?n2.0 \<rbrakk>  = ?s\<rbrakk> \<Longrightarrow> ?n1.0 = ?n2.0
i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s
i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^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
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. n1 = n2
[PROOF STEP]
by metis


[STATEMENT]
lemma is_satis_eq_imp:
  assumes "i \<Turnstile> (CE_val (V_var x) ==  CE_val (V_lit (if (n1 =  n2) then L_true else L_false)))" (is "is_satis i ?c1")
  shows   "i \<Turnstile> (CE_val (V_var x)  ==  CE_op Eq [(V_lit (n1))]\<^sup>c\<^sup>e [(V_lit (n2))]\<^sup>c\<^sup>e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have *:"eval_c i ?c1 True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
using assms is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
[PROOF STEP]
have  "eval_e i (CE_val (V_lit ((if (n1=n2) then L_true else L_false)))) (SBool (n1=n2))"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True

goal (1 subgoal):
 1. i \<lbrakk> [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
using eval_e_elims(1) eval_v_elims eval_l.simps
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrakk> ~ True
\<lbrakk>?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

goal (1 subgoal):
 1. i \<lbrakk> [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
by (metis (full_types) eval_e.intros(1) eval_v_litI)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
hence "eval_e i (CE_val (V_var x)) (SBool (n1=n2))"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)

goal (1 subgoal):
 1. i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
using eval_c_elims(7)[OF *]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
(\<And>sv1 sv2. \<lbrakk>True = (sv1 = sv2); i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv1 ; i \<lbrakk> [ [ if n1 = n2 then L_true else L_false ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P) \<Longrightarrow> ?P

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

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
have "eval_e i (CE_op Eq [(V_lit (n1))]\<^sup>c\<^sup>e [(V_lit (n2) )]\<^sup>c\<^sup>e) (SBool (n1=n2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
obtain s1 and s2 where *:"i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_l.simps eval_e.intros eval_v_litI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n
?i \<lbrakk> ?v \<rbrakk> ~ ?sv  \<Longrightarrow> ?i \<lbrakk> [ ?v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ plus ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (?n1.0 + ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SNum ?n1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SNum ?n2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ leq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?n1.0 \<le> ?n2.0)
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ eq ?v1.0 ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (?s1.0 = ?s2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#1?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v1.0
?i \<lbrakk> ?v \<rbrakk> ~ SPair ?v1.0 ?v2.0  \<Longrightarrow> ?i \<lbrakk> [#2?v]\<^sup>c\<^sup>e \<rbrakk> ~ ?v2.0
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ SBitvec ?bv1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ SBitvec ?bv2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 @@ ?v2.0 ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec (?bv1.0 @ ?bv2.0)
?i \<lbrakk> ?v \<rbrakk> ~ SBitvec ?bv  \<Longrightarrow> ?i \<lbrakk> [| ?v |]\<^sup>c\<^sup>e \<rbrakk> ~ SNum (int (length ?bv))
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
have " SBool (n1 = n2)  =  SBool (s1 = s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
proof(cases "n1=n2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n1 = n2 \<Longrightarrow> SBool (n1 = n2) = SBool (s1 = s2)
 2. n1 \<noteq> n2 \<Longrightarrow> SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n1 = n2

goal (2 subgoals):
 1. n1 = n2 \<Longrightarrow> SBool (n1 = n2) = SBool (s1 = s2)
 2. n1 \<noteq> n2 \<Longrightarrow> SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n1 = n2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n1 = n2

goal (1 subgoal):
 1. SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
n1 = n2
i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2

goal (1 subgoal):
 1. SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
by (simp add: calculation eval_e_uniqueness)
[PROOF STATE]
proof (state)
this:
SBool (n1 = n2) = SBool (s1 = s2)

goal (1 subgoal):
 1. n1 \<noteq> n2 \<Longrightarrow> SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n1 \<noteq> n2 \<Longrightarrow> SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n1 \<noteq> n2

goal (1 subgoal):
 1. n1 \<noteq> n2 \<Longrightarrow> SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n1 \<noteq> n2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n1 \<noteq> n2

goal (1 subgoal):
 1. SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
using *  eval_e_lit_inj
[PROOF STATE]
proof (prove)
using this:
n1 \<noteq> n2
i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2
\<lbrakk>?i \<lbrakk> [ [ ?n1.0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s ; ?i \<lbrakk> [ [ ?n2.0 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> ?n1.0 = ?n2.0

goal (1 subgoal):
 1. SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
SBool (n1 = n2) = SBool (s1 = s2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
SBool (n1 = n2) = SBool (s1 = s2)

goal (1 subgoal):
 1. i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2
SBool (n1 = n2) = SBool (s1 = s2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2
SBool (n1 = n2) = SBool (s1 = s2)

goal (1 subgoal):
 1. i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
using eval_e_eqI[of i "[(V_lit (n1))]\<^sup>c\<^sup>e"  s1 "[(V_lit (n2))]\<^sup>c\<^sup>e" s2 ]
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1  \<and> i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2
SBool (n1 = n2) = SBool (s1 = s2)
\<lbrakk>i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1 ; i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (s1 = s2)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
using eval_c.intros is_satis.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
i \<lbrakk> [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e \<rbrakk> ~ SBool (n1 = n2)
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ eq [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ n2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e

goal:
No subgoals!
[PROOF STEP]
qed