[STATEMENT]
lemma wfI_upd:
  assumes  "wfI \<Theta> \<Gamma> i" and "wfRCV \<Theta> s b" and "wfG \<Theta> B ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)"
  shows "wfI \<Theta> ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) (i(x \<mapsto> s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
[PROOF STEP]
proof(subst wfI_def,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
fix xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
assume as:"xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)"
[PROOF STATE]
proof (state)
this:
xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)

goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)
[PROOF STEP]
obtain x1::x and b1::b and c1::c where xa: "xa = (x1,b1,c1)"
[PROOF STATE]
proof (prove)
using this:
xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)

goal (1 subgoal):
 1. (\<And>x1 b1 c1. xa = (x1, b1, c1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using toSet.simps
[PROOF STATE]
proof (prove)
using this:
xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G

goal (1 subgoal):
 1. (\<And>x1 b1 c1. xa = (x1, b1, c1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod_cases3
[PROOF STATE]
proof (prove)
using this:
xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G
(\<And>a b c. ?y = (a, b, c) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x1 b1 c1. xa = (x1, b1, c1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xa = (x1, b1, c1)

goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
have "\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and> wfRCV \<Theta> sa b1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
proof(cases "x=x1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
 2. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = x1

goal (2 subgoals):
 1. x = x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
 2. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
hence "b=b1"
[PROOF STATE]
proof (prove)
using this:
x = x1

goal (1 subgoal):
 1. b = b1
[PROOF STEP]
using as xa wfG_unique assms
[PROOF STATE]
proof (prove)
using this:
x = x1
xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)
xa = (x1, b1, c1)
\<lbrakk> ?B ; ?\<Theta>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> ; (?x1.0, ?b1.0, ?c1.0) \<in> toSet ((?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>); ?x1.0 = ?x\<rbrakk> \<Longrightarrow> ?b1.0 = ?b \<and> ?c1.0 = ?c
 \<Theta> ; \<Gamma> \<turnstile> i
 \<Theta>  \<turnstile> s : b
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>

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

goal (2 subgoals):
 1. x = x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
 2. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
hence "Some s = (i(x \<mapsto> s)) x1 \<and> wfRCV \<Theta> s b1"
[PROOF STATE]
proof (prove)
using this:
b = b1

goal (1 subgoal):
 1. Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1
[PROOF STEP]
using assms True
[PROOF STATE]
proof (prove)
using this:
b = b1
 \<Theta> ; \<Gamma> \<turnstile> i
 \<Theta>  \<turnstile> s : b
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>
x = x1

goal (1 subgoal):
 1. Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1

goal (2 subgoals):
 1. x = x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
 2. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1

goal (1 subgoal):
 1. \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> x1

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
hence "(x1,b1,c1) \<in> toSet \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1

goal (1 subgoal):
 1. (x1, b1, c1) \<in> toSet \<Gamma>
[PROOF STEP]
using xa as
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1
xa = (x1, b1, c1)
xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)

goal (1 subgoal):
 1. (x1, b1, c1) \<in> toSet \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x1, b1, c1) \<in> toSet \<Gamma>

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x1, b1, c1) \<in> toSet \<Gamma>
[PROOF STEP]
obtain sa where "Some sa = i x1 \<and> wfRCV \<Theta> sa b1"
[PROOF STATE]
proof (prove)
using this:
(x1, b1, c1) \<in> toSet \<Gamma>

goal (1 subgoal):
 1. (\<And>sa. Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms wfI_def as xa
[PROOF STATE]
proof (prove)
using this:
(x1, b1, c1) \<in> toSet \<Gamma>
 \<Theta> ; \<Gamma> \<turnstile> i
 \<Theta>  \<turnstile> s : b
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma>
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)
xa = (x1, b1, c1)

goal (1 subgoal):
 1. (\<And>sa. Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
hence "Some sa = (i(x \<mapsto> s)) x1 \<and> wfRCV \<Theta> sa b1"
[PROOF STATE]
proof (prove)
using this:
Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1
x \<noteq> x1

goal (1 subgoal):
 1. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
thus  "case xa of (xa, ba, ca) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and> wfRCV \<Theta> sa ba"
[PROOF STATE]
proof (prove)
using this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. case xa of (xa, ba, ca) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : ba
[PROOF STEP]
using xa
[PROOF STATE]
proof (prove)
using this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
xa = (x1, b1, c1)

goal (1 subgoal):
 1. case xa of (xa, ba, ca) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : ba
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
case xa of (xa, ba, ca) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : ba

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfI_upd_full:
  fixes v::v
  assumes  "wfI \<Theta> G i" and "G =  ((\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v)@\<Gamma>)" and "wfRCV \<Theta> s b" and "wfG \<Theta> B  (\<Gamma>'@((x,b,c)#\<^sub>\<Gamma>\<Gamma>))" and "\<Theta> ; B  ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b"
  shows "wfI \<Theta>  (\<Gamma>'@((x,b,c)#\<^sub>\<Gamma>\<Gamma>)) (i(x \<mapsto> s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
[PROOF STEP]
proof(subst wfI_def,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
fix xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
assume as:"xa \<in> toSet (\<Gamma>'@((x,b,c)#\<^sub>\<Gamma>\<Gamma>))"
[PROOF STATE]
proof (state)
this:
xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>)

goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>)
[PROOF STEP]
obtain x1::x and b1::b and c1::c where xa: "xa = (x1,b1,c1)"
[PROOF STATE]
proof (prove)
using this:
xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>)

goal (1 subgoal):
 1. (\<And>x1 b1 c1. xa = (x1, b1, c1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using toSet.simps
[PROOF STATE]
proof (prove)
using this:
xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>)
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G

goal (1 subgoal):
 1. (\<And>x1 b1 c1. xa = (x1, b1, c1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod_cases3
[PROOF STATE]
proof (prove)
using this:
xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>)
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G
(\<And>a b c. ?y = (a, b, c) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x1 b1 c1. xa = (x1, b1, c1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xa = (x1, b1, c1)

goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
have "\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and> wfRCV \<Theta> sa b1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
proof(cases "x=x1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
 2. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = x1

goal (2 subgoals):
 1. x = x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
 2. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
hence "b=b1"
[PROOF STATE]
proof (prove)
using this:
x = x1

goal (1 subgoal):
 1. b = b1
[PROOF STEP]
using as xa wfG_unique_full assms
[PROOF STATE]
proof (prove)
using this:
x = x1
xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>)
xa = (x1, b1, c1)
\<lbrakk> ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> ; (?x1.0, ?b1.0, ?c1.0) \<in> toSet (?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>); ?x1.0 = ?x\<rbrakk> \<Longrightarrow> ?b1.0 = ?b \<and> ?c1.0 = ?c
 \<Theta> ; G \<turnstile> i
G = \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>
 \<Theta>  \<turnstile> s : b
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

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

goal (2 subgoals):
 1. x = x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
 2. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
hence "Some s = (i(x \<mapsto> s)) x1 \<and> wfRCV \<Theta> s b1"
[PROOF STATE]
proof (prove)
using this:
b = b1

goal (1 subgoal):
 1. Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1
[PROOF STEP]
using assms True
[PROOF STATE]
proof (prove)
using this:
b = b1
 \<Theta> ; G \<turnstile> i
G = \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>
 \<Theta>  \<turnstile> s : b
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
x = x1

goal (1 subgoal):
 1. Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1

goal (2 subgoals):
 1. x = x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
 2. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Some s = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> s : b1

goal (1 subgoal):
 1. \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> x1

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
hence "(x1,b1,c1) \<in> toSet (\<Gamma>'@\<Gamma>)"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1

goal (1 subgoal):
 1. (x1, b1, c1) \<in> toSet (\<Gamma>' @ \<Gamma>)
[PROOF STEP]
using as xa
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1
xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>)
xa = (x1, b1, c1)

goal (1 subgoal):
 1. (x1, b1, c1) \<in> toSet (\<Gamma>' @ \<Gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x1, b1, c1) \<in> toSet (\<Gamma>' @ \<Gamma>)

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x1, b1, c1) \<in> toSet (\<Gamma>' @ \<Gamma>)
[PROOF STEP]
obtain c1' where  "(x1,b1,c1') \<in> toSet (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v@\<Gamma>)"
[PROOF STATE]
proof (prove)
using this:
(x1, b1, c1) \<in> toSet (\<Gamma>' @ \<Gamma>)

goal (1 subgoal):
 1. (\<And>c1'. (x1, b1, c1') \<in> toSet (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xa as wfG_member_subst assms  False
[PROOF STATE]
proof (prove)
using this:
(x1, b1, c1) \<in> toSet (\<Gamma>' @ \<Gamma>)
xa = (x1, b1, c1)
xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>)
\<lbrakk>(?x1.0, ?b1.0, ?c1.0) \<in> toSet (?\<Gamma>' @ ?\<Gamma>);  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> ; ?x \<noteq> ?x1.0\<rbrakk> \<Longrightarrow> \<exists>c1'. (?x1.0, ?b1.0, c1') \<in> toSet (?\<Gamma>'[?x::=?v]\<^sub>\<Gamma>\<^sub>v @ ?\<Gamma>)
 \<Theta> ; G \<turnstile> i
G = \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>
 \<Theta>  \<turnstile> s : b
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
x \<noteq> x1

goal (1 subgoal):
 1. (\<And>c1'. (x1, b1, c1') \<in> toSet (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(x1, b1, c1') \<in> toSet (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>)

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x1, b1, c1') \<in> toSet (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>)
[PROOF STEP]
obtain sa where "Some sa = i x1 \<and> wfRCV \<Theta> sa b1"
[PROOF STATE]
proof (prove)
using this:
(x1, b1, c1') \<in> toSet (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>)

goal (1 subgoal):
 1. (\<And>sa. Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms wfI_def as xa
[PROOF STATE]
proof (prove)
using this:
(x1, b1, c1') \<in> toSet (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>)
 \<Theta> ; G \<turnstile> i
G = \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>
 \<Theta>  \<turnstile> s : b
 \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>)
xa = (x1, b1, c1)

goal (1 subgoal):
 1. (\<And>sa. Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
hence "Some sa = (i(x \<mapsto> s)) x1 \<and> wfRCV \<Theta> sa b1"
[PROOF STATE]
proof (prove)
using this:
Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Some sa = i x1 \<and>  \<Theta>  \<turnstile> sa : b1
x \<noteq> x1

goal (1 subgoal):
 1. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. \<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. \<And>xa. xa \<in> toSet (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<Longrightarrow> case xa of (xa, b, c) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : b
[PROOF STEP]
thus  "case xa of (xa, ba, ca) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and> wfRCV \<Theta> sa ba"
[PROOF STATE]
proof (prove)
using this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1

goal (1 subgoal):
 1. case xa of (xa, ba, ca) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : ba
[PROOF STEP]
using xa
[PROOF STATE]
proof (prove)
using this:
\<exists>sa. Some sa = (i(x \<mapsto> s)) x1 \<and>  \<Theta>  \<turnstile> sa : b1
xa = (x1, b1, c1)

goal (1 subgoal):
 1. case xa of (xa, ba, ca) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : ba
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
case xa of (xa, ba, ca) \<Rightarrow> \<exists>sa. Some sa = (i(x \<mapsto> s)) xa \<and>  \<Theta>  \<turnstile> sa : ba

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_c_satis[simp]:
  fixes v::v
  assumes "i \<lbrakk> v \<rbrakk> ~  s" and "wfC \<Theta> B ((x,b,c')#\<^sub>\<Gamma>\<Gamma>) c" and "wfI \<Theta> \<Gamma> i" and  "\<Theta> ; B  ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b"
  shows "i \<Turnstile> (c[x::=v]\<^sub>c\<^sub>v) \<longleftrightarrow> (i ( x \<mapsto> s)) \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
have "wfI \<Theta> ((x, b, c') #\<^sub>\<Gamma> \<Gamma>) (i(x \<mapsto> s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
[PROOF STEP]
using wfI_upd assms wfC_wf eval_v_base
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta> ; ?\<Gamma> \<turnstile> ?i;  ?\<Theta>  \<turnstile> ?s : ?b;  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> \<turnstile> ?i(?x \<mapsto> ?s)
i \<lbrakk> v \<rbrakk> ~ s
 \<Theta> ; B ; (x, b, c') #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma> \<turnstile> i
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s : ?b

goal (1 subgoal):
 1.  \<Theta> ; (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
 \<Theta> ; (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
[PROOF STEP]
obtain s1 where s1:"eval_c (i(x \<mapsto> s)) c s1"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)

goal (1 subgoal):
 1. (\<And>s1.  i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ s1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  eval_c_exist[of \<Theta> "((x,b,c')#\<^sub>\<Gamma>\<Gamma>)" "(i ( x \<mapsto> s))" B c ] assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
\<lbrakk> \<Theta> ; (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s);  \<Theta> ; B ; (x, b, c') #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c \<rbrakk> \<Longrightarrow> \<exists>sa.  i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ sa
i \<lbrakk> v \<rbrakk> ~ s
 \<Theta> ; B ; (x, b, c') #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma> \<turnstile> i
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

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

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
have "\<Theta> ; B  ; \<Gamma>  \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
using wf_subst1(2)[OF assms(2) _ assms(4) , of GNil x   ] subst_gv.simps
[PROOF STATE]
proof (prove)
using this:
(x, b, c') #\<^sub>\<Gamma> \<Gamma> = GNil @ (x, b, ?c') #\<^sub>\<Gamma> \<Gamma> \<Longrightarrow>  \<Theta> ; B ; ((x, b, c') #\<^sub>\<Gamma> \<Gamma>)[x::=v]\<^sub>\<Gamma>\<^sub>v   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v
GNil[?x::=?v]\<^sub>\<Gamma>\<^sub>v = GNil
((?y, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?x::=?v]\<^sub>\<Gamma>\<^sub>v = (if ?x = ?y then ?\<Gamma> else (?y, ?b, ?c[?x::=?v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> ?\<Gamma>[?x::=?v]\<^sub>\<Gamma>\<^sub>v)

goal (1 subgoal):
 1.  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
obtain s2 where s2:"eval_c i c[x::=v]\<^sub>c\<^sub>v s2"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v

goal (1 subgoal):
 1. (\<And>s2.  i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_c_exist[of \<Theta> "\<Gamma>" "i" B "c[x::=v]\<^sub>c\<^sub>v"  ] assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v
\<lbrakk> \<Theta> ; \<Gamma> \<turnstile> i;  \<Theta> ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v \<rbrakk> \<Longrightarrow> \<exists>s.  i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s
i \<lbrakk> v \<rbrakk> ~ s
 \<Theta> ; B ; (x, b, c') #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma> \<turnstile> i
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

goal (1 subgoal):
 1. (\<And>s2.  i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
using s1 s2 subst_c_eval_v[OF assms(1) s2 s1] is_satis.cases
[PROOF STATE]
proof (prove)
using this:
 i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ s1
 i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2
s2 = s1
\<lbrakk> ?a1.0 \<Turnstile> ?a2.0 ; \<And>i c. \<lbrakk>?a1.0 = i; ?a2.0 = c;  i \<lbrakk> c \<rbrakk> ~ True \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
using eval_c_uniqueness is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ s1
 i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2
s2 = s1
\<lbrakk> ?a1.0 \<Turnstile> ?a2.0 ; \<And>i c. \<lbrakk>?a1.0 = i; ?a2.0 = c;  i \<lbrakk> c \<rbrakk> ~ True \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c \<rbrakk> ~ ?s ;  ?i \<lbrakk> ?c \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 ?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> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_c_satis_full:
  fixes v::v and \<Gamma>'::\<Gamma>
  assumes "i \<lbrakk> v \<rbrakk> ~  s" and "wfC \<Theta> B  (\<Gamma>'@((x,b,c')#\<^sub>\<Gamma>\<Gamma>)) c" and "wfI \<Theta>  ((\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v)@\<Gamma>) i" and  "\<Theta> ; B  ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b"
  shows "i \<Turnstile> (c[x::=v]\<^sub>c\<^sub>v) \<longleftrightarrow> (i ( x \<mapsto> s)) \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
have "wfI \<Theta> (\<Gamma>'@((x, b, c')) #\<^sub>\<Gamma> \<Gamma>) (i(x \<mapsto> s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
[PROOF STEP]
using wfI_upd_full assms wfC_wf eval_v_base wfI_suffix wfI_def wfV_wf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta> ; ?G \<turnstile> ?i; ?G = ?\<Gamma>'[?x::=?v]\<^sub>\<Gamma>\<^sub>v @ ?\<Gamma>;  ?\<Theta>  \<turnstile> ?s : ?b;  ?\<Theta> ; ?B  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> ;  ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> \<turnstile> ?i(?x \<mapsto> ?s)
i \<lbrakk> v \<rbrakk> ~ s
 \<Theta> ; B ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma> \<turnstile> i
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;  ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow>  ?P  \<turnstile> ?s : ?b
\<lbrakk> ?P ; ?G' @ ?G \<turnstile> ?i;  ?P ; ?B  \<turnstile>\<^sub>w\<^sub>f ?G \<rbrakk> \<Longrightarrow>  ?P ; ?G \<turnstile> ?i
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
 ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
[PROOF STEP]
obtain s1 where s1:"eval_c (i(x \<mapsto> s)) c s1"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)

goal (1 subgoal):
 1. (\<And>s1.  i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ s1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  eval_c_exist[of \<Theta> "(\<Gamma>'@(x,b,c')#\<^sub>\<Gamma>\<Gamma>)" "(i ( x \<mapsto> s))" B c ] assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s)
\<lbrakk> \<Theta> ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i(x \<mapsto> s);  \<Theta> ; B ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c \<rbrakk> \<Longrightarrow> \<exists>sa.  i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ sa
i \<lbrakk> v \<rbrakk> ~ s
 \<Theta> ; B ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma> \<turnstile> i
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

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

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
have "\<Theta> ; B ; ((\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v)@\<Gamma>) \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; B ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
using wbc_subst assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>' @ (?x, ?b, ?c') #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>'[?x::=?v]\<^sub>\<Gamma>\<^sub>v @ ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c[?x::=?v]\<^sub>c\<^sub>v
i \<lbrakk> v \<rbrakk> ~ s
 \<Theta> ; B ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma> \<turnstile> i
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

goal (1 subgoal):
 1.  \<Theta> ; B ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; B ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 \<Theta> ; B ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
obtain s2 where s2:"eval_c i c[x::=v]\<^sub>c\<^sub>v s2"
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v

goal (1 subgoal):
 1. (\<And>s2.  i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_c_exist[of \<Theta> "((\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v)@\<Gamma>)" "i" B "c[x::=v]\<^sub>c\<^sub>v" ] assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; B ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v
\<lbrakk> \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma> \<turnstile> i;  \<Theta> ; B ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c[x::=v]\<^sub>c\<^sub>v \<rbrakk> \<Longrightarrow> \<exists>s.  i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s
i \<lbrakk> v \<rbrakk> ~ s
 \<Theta> ; B ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c
 \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ \<Gamma> \<turnstile> i
 \<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b

goal (1 subgoal):
 1. (\<And>s2.  i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
using s1 s2 subst_c_eval_v[OF assms(1) s2 s1] is_satis.cases
[PROOF STATE]
proof (prove)
using this:
 i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ s1
 i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2
s2 = s1
\<lbrakk> ?a1.0 \<Turnstile> ?a2.0 ; \<And>i c. \<lbrakk>?a1.0 = i; ?a2.0 = c;  i \<lbrakk> c \<rbrakk> ~ True \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1.  i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
using eval_c_uniqueness is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ s1
 i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s2
s2 = s1
\<lbrakk> ?a1.0 \<Turnstile> ?a2.0 ; \<And>i c. \<lbrakk>?a1.0 = i; ?a2.0 = c;  i \<lbrakk> c \<rbrakk> ~ True \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?i \<lbrakk> ?c \<rbrakk> ~ ?s ;  ?i \<lbrakk> ?c \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 ?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> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c[x::=v]\<^sub>c\<^sub>v  =  i(x \<mapsto> s) \<Turnstile> c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma validI[intro]:
  fixes c::c
  assumes  "wfC P B G c" and "\<forall>i. P ; G \<turnstile> i \<and> i \<Turnstile> G \<longrightarrow> i \<Turnstile> c"
  shows "P ; B ; G \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ; B ; G  \<Turnstile> c
[PROOF STEP]
using assms valid.simps
[PROOF STATE]
proof (prove)
using this:
 P ; B ; G   \<turnstile>\<^sub>w\<^sub>f c
\<forall>i.  P ; G \<turnstile> i \<and>  i \<Turnstile> G  \<longrightarrow>  i \<Turnstile> c
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))

goal (1 subgoal):
 1. P ; B ; G  \<Turnstile> c
[PROOF STEP]
by presburger


[STATEMENT]
lemma valid_g_wf:
  fixes c::c and G::\<Gamma>
  assumes "P ; B ; G \<Turnstile> c"
  shows "P ; B \<turnstile>\<^sub>w\<^sub>f G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P ; B  \<turnstile>\<^sub>w\<^sub>f G
[PROOF STEP]
using assms wfC_wf valid.simps
[PROOF STATE]
proof (prove)
using this:
P ; B ; G  \<Turnstile> c
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<and>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
(?P ; ?B ; ?G  \<Turnstile> ?c ) = ( ?P ; ?B ; ?G   \<turnstile>\<^sub>w\<^sub>f ?c  \<and> (\<forall>i.  ?P ; ?G \<turnstile> i \<and>  i \<Turnstile> ?G  \<longrightarrow>  i \<Turnstile> ?c ))

goal (1 subgoal):
 1.  P ; B  \<turnstile>\<^sub>w\<^sub>f G
[PROOF STEP]
by blast


[STATEMENT]
lemma valid_reflI [intro]:
  fixes b::b
  assumes  "P ; B ; ((x,b,c1)#\<^sub>\<Gamma>G) \<turnstile>\<^sub>w\<^sub>f c1" and "c1 = c2"
  shows "P ; B ; ((x,b,c1)#\<^sub>\<Gamma>G) \<Turnstile> c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ; B ; (x, b, c1) #\<^sub>\<Gamma> G  \<Turnstile> c2
[PROOF STEP]
using satis_reflI assms
[PROOF STATE]
proof (prove)
using this:
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  \<Longrightarrow>  ?i \<Turnstile> ?c
 P ; B ; (x, b, c1) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c1
c1 = c2

goal (1 subgoal):
 1. P ; B ; (x, b, c1) #\<^sub>\<Gamma> G  \<Turnstile> c2
[PROOF STEP]
by simp


[STATEMENT]
lemma eval_v_weakening:
  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