[STATEMENT]
lemma eval_v_restrict:
  fixes c::v and B::"bv fset"
  assumes "i = i' |` d" and "supp c \<subseteq> atom ` d \<union> supp B "  and "i' \<lbrakk> c \<rbrakk> ~ s"
  shows "i \<lbrakk> c \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i = i' |` d
supp c \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> c \<rbrakk> ~ s

goal (1 subgoal):
 1. i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
proof(nominal_induct c arbitrary:s rule: v.strong_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 3. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 4. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 5. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
case (V_lit x)
[PROOF STATE]
proof (state)
this:
i = i' |` d
supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s

goal (5 subgoals):
 1. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 3. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 4. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 5. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = i' |` d
supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i = i' |` d
supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s

goal (1 subgoal):
 1. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
[PROOF STEP]
using eval_v_elims eval_v_litI
[PROOF STATE]
proof (prove)
using this:
i = i' |` d
supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
\<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
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>

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

goal (4 subgoals):
 1. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 3. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 4. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 3. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 4. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
case (V_var x)
[PROOF STATE]
proof (state)
this:
i = i' |` d
supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s

goal (4 subgoals):
 1. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 3. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 4. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
have "atom x \<in> atom ` d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<in> atom ` d
[PROOF STEP]
using x_not_in_b_set[of x B] assms v.supp(2) supp_at_base
[PROOF STATE]
proof (prove)
using this:
atom x \<notin> supp B
i = i' |` d
supp c \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> c \<rbrakk> ~ s
supp [ ?x ]\<^sup>v = supp ?x
supp ?a = {atom ?a}

goal (1 subgoal):
 1. atom x \<in> atom ` d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>atom x \<notin> supp B; i = i' |` d; supp c \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> c \<rbrakk> ~ s ; \<And>x. supp [ x ]\<^sup>v = supp x; \<And>a. supp a = {atom a}\<rbrakk> \<Longrightarrow> atom x \<in> atom ` d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<in> atom ` d
[PROOF STEP]
by (metis UnE V_var.prems(2) \<open>atom x \<notin> supp B\<close> singletonI subset_iff supp_at_base v.supp(2))
[PROOF STATE]
proof (state)
this:
atom x \<in> atom ` d

goal:
No subgoals!
[PROOF STEP]
(* 46 ms *)
[PROOF STATE]
proof (state)
this:
atom x \<in> atom ` d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atom x \<in> atom ` d

goal (4 subgoals):
 1. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 3. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 4. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom x \<in> atom ` d

goal (4 subgoals):
 1. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 3. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 4. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
have "Some s = i' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some s = i' x
[PROOF STEP]
using assms eval_v_elims(2)
[PROOF STATE]
proof (prove)
using this:
i = i' |` d
supp c \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> c \<rbrakk> ~ s
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. Some s = i' x
[PROOF STEP]
using V_var.prems(3)
[PROOF STATE]
proof (prove)
using this:
i = i' |` d
supp c \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> c \<rbrakk> ~ s
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s

goal (1 subgoal):
 1. Some s = i' x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Some s = i' x

goal (4 subgoals):
 1. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 3. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 4. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
hence "Some s= i x"
[PROOF STATE]
proof (prove)
using this:
Some s = i' x

goal (1 subgoal):
 1. Some s = i x
[PROOF STEP]
using assms insert_subset restrict_in
[PROOF STATE]
proof (prove)
using this:
Some s = i' x
i = i' |` d
supp c \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> c \<rbrakk> ~ s
(insert ?x ?A \<subseteq> ?B) = (?x \<in> ?B \<and> ?A \<subseteq> ?B)
?x \<in> ?A \<Longrightarrow> (?m |` ?A) ?x = ?m ?x

goal (1 subgoal):
 1. Some s = i x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Some s = i' x; i = i' |` d; supp c \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> c \<rbrakk> ~ s ; \<And>x A B. (insert x A \<subseteq> B) = (x \<in> B \<and> A \<subseteq> B); \<And>x A m. x \<in> A \<Longrightarrow> (m |` A) x = m x\<rbrakk> \<Longrightarrow> Some s = i x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some s = i x
[PROOF STEP]
by (metis (no_types) \<open>i = i' |` d\<close> \<open>Some s = i' x\<close> atom_eq_iff calculation imageE restrict_in)
[PROOF STATE]
proof (state)
this:
Some s = i x

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

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

goal (4 subgoals):
 1. \<And>x s. \<lbrakk>i = i' |` d; supp [ x ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 3. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 4. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Some s = i x

goal (1 subgoal):
 1. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
[PROOF STEP]
using eval_v.eval_v_varI
[PROOF STATE]
proof (prove)
using this:
Some s = i x
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv

goal (1 subgoal):
 1. i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s

goal (3 subgoals):
 1. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 3. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 3. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
case (V_pair v1 v2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i = i' |` d; supp v1 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v1 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ ?s
\<lbrakk>i = i' |` d; supp v2 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v2 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ ?s
i = i' |` d
supp [ v1 , v2 ]\<^sup>v \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s

goal (3 subgoals):
 1. \<And>x1a x2a s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x1a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x1a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x1a \<rbrakk> ~ s ; \<And>s. \<lbrakk>i = i' |` d; supp x2a \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x2a \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x2a \<rbrakk> ~ s ; i = i' |` d; supp [ x1a , x2a ]\<^sup>v \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s
 2. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 3. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i = i' |` d; supp v1 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v1 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ ?s
\<lbrakk>i = i' |` d; supp v2 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v2 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ ?s
i = i' |` d
supp [ v1 , v2 ]\<^sup>v \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = i' |` d; supp v1 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v1 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ ?s
\<lbrakk>i = i' |` d; supp v2 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v2 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ ?s
i = i' |` d
supp [ v1 , v2 ]\<^sup>v \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s

goal (1 subgoal):
 1. i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s
[PROOF STEP]
using eval_v_elims(3) eval_v_pairI v.supp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = i' |` d; supp v1 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v1 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ ?s
\<lbrakk>i = i' |` d; supp v2 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v2 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ ?s
i = i' |` d
supp [ v1 , v2 ]\<^sup>v \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s
\<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> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
supp [ ?l ]\<^sup>v = supp ?l
supp [ ?x ]\<^sup>v = supp ?x
supp [ ?v1.0 , ?v2.0 ]\<^sup>v = supp ?v1.0 \<union> supp ?v2.0
supp (V_cons ?list1.0 ?list2.0 ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?v)
supp (V_consp ?list1.0 ?list2.0 ?b ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?v))

goal (1 subgoal):
 1. i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s
[PROOF STEP]
by (metis assms le_sup_iff)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s

goal (2 subgoals):
 1. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 2. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 2. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
case (V_cons dc v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i = i' |` d; supp x3_ \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3_ \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3_ \<rbrakk> ~ ?s
i = i' |` d
supp (V_cons dc v1 x3_) \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> V_cons dc v1 x3_ \<rbrakk> ~ s

goal (2 subgoals):
 1. \<And>x1a x2a x3 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x3 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3 \<rbrakk> ~ s ; i = i' |` d; supp (V_cons x1a x2a x3) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s
 2. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i = i' |` d; supp x3_ \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3_ \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3_ \<rbrakk> ~ ?s
i = i' |` d
supp (V_cons dc v1 x3_) \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> V_cons dc v1 x3_ \<rbrakk> ~ s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = i' |` d; supp x3_ \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3_ \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3_ \<rbrakk> ~ ?s
i = i' |` d
supp (V_cons dc v1 x3_) \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> V_cons dc v1 x3_ \<rbrakk> ~ s

goal (1 subgoal):
 1. i \<lbrakk> V_cons dc v1 x3_ \<rbrakk> ~ s
[PROOF STEP]
using eval_v_elims(4) eval_v_consI v.supp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = i' |` d; supp x3_ \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x3_ \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> x3_ \<rbrakk> ~ ?s
i = i' |` d
supp (V_cons dc v1 x3_) \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> V_cons dc v1 x3_ \<rbrakk> ~ s
\<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
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
supp [ ?l ]\<^sup>v = supp ?l
supp [ ?x ]\<^sup>v = supp ?x
supp [ ?v1.0 , ?v2.0 ]\<^sup>v = supp ?v1.0 \<union> supp ?v2.0
supp (V_cons ?list1.0 ?list2.0 ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?v)
supp (V_consp ?list1.0 ?list2.0 ?b ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?v))

goal (1 subgoal):
 1. i \<lbrakk> V_cons dc v1 x3_ \<rbrakk> ~ s
[PROOF STEP]
by (metis assms le_sup_iff)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> V_cons dc v1 x3_ \<rbrakk> ~ s

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
case (V_consp tyid dc b1 v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i = i' |` d; supp v1 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v1 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ ?s
i = i' |` d
supp (V_consp tyid dc b1 v1) \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i = i' |` d; supp v1 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v1 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ ?s
i = i' |` d
supp (V_consp tyid dc b1 v1) \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s
[PROOF STEP]
obtain sv1 where *:"i' \<lbrakk> v1 \<rbrakk> ~ sv1 \<and> s = SConsp tyid dc b1 sv1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = i' |` d; supp v1 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v1 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ ?s
i = i' |` d
supp (V_consp tyid dc b1 v1) \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s

goal (1 subgoal):
 1. (\<And>sv1. i' \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SConsp tyid dc b1 sv1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = i' |` d; supp v1 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v1 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ ?s
i = i' |` d
supp (V_consp tyid dc b1 v1) \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s
\<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. (\<And>sv1. i' \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SConsp tyid dc b1 sv1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i' \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SConsp tyid dc b1 sv1

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
hence "i \<lbrakk> v1 \<rbrakk> ~ sv1"
[PROOF STATE]
proof (prove)
using this:
i' \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SConsp tyid dc b1 sv1

goal (1 subgoal):
 1. i \<lbrakk> v1 \<rbrakk> ~ sv1
[PROOF STEP]
using V_consp
[PROOF STATE]
proof (prove)
using this:
i' \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SConsp tyid dc b1 sv1
\<lbrakk>i = i' |` d; supp v1 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> v1 \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ ?s
i = i' |` d
supp (V_consp tyid dc b1 v1) \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s

goal (1 subgoal):
 1. i \<lbrakk> v1 \<rbrakk> ~ sv1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ sv1

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s. \<lbrakk>\<And>s. \<lbrakk>i = i' |` d; supp x4 \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> x4 \<rbrakk> ~ s ; i = i' |` d; supp (V_consp x1a x2a x3 x4) \<subseteq> atom ` d \<union> supp B; i' \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ sv1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ sv1

goal (1 subgoal):
 1. i \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s
[PROOF STEP]
using * eval_v_conspI v.supp eval_v.simps  assms le_sup_iff
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ sv1
i' \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SConsp tyid dc b1 sv1
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s
supp [ ?l ]\<^sup>v = supp ?l
supp [ ?x ]\<^sup>v = supp ?x
supp [ ?v1.0 , ?v2.0 ]\<^sup>v = supp ?v1.0 \<union> supp ?v2.0
supp (V_cons ?list1.0 ?list2.0 ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> supp ?v)
supp (V_consp ?list1.0 ?list2.0 ?b ?v) = supp ?list1.0 \<union> (supp ?list2.0 \<union> (supp ?b \<union> supp ?v))
?a1.0 \<lbrakk> ?a2.0 \<rbrakk> ~ ?a3.0  = ((\<exists>i l. ?a1.0 = i \<and> ?a2.0 = [ l ]\<^sup>v \<and> ?a3.0 = \<lbrakk> l \<rbrakk> ) \<or> (\<exists>sv i x. ?a1.0 = i \<and> ?a2.0 = [ x ]\<^sup>v \<and> ?a3.0 = sv \<and> Some sv = i x) \<or> (\<exists>i v1 s1 v2 s2. ?a1.0 = i \<and> ?a2.0 = [ v1 , v2 ]\<^sup>v \<and> ?a3.0 = SPair s1 s2 \<and> i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2 ) \<or> (\<exists>i v s tyid dc. ?a1.0 = i \<and> ?a2.0 = V_cons tyid dc v \<and> ?a3.0 = SCons tyid dc s \<and> i \<lbrakk> v \<rbrakk> ~ s ) \<or> (\<exists>i v s tyid dc b. ?a1.0 = i \<and> ?a2.0 = V_consp tyid dc b v \<and> ?a3.0 = SConsp tyid dc b s \<and> i \<lbrakk> v \<rbrakk> ~ s ))
i = i' |` d
supp c \<subseteq> atom ` d \<union> supp B
i' \<lbrakk> c \<rbrakk> ~ s
(sup ?x ?y \<le> ?z) = (?x \<le> ?z \<and> ?y \<le> ?z)

goal (1 subgoal):
 1. i \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s

goal:
No subgoals!
[PROOF STEP]
qed