[STATEMENT]
lemma BSD_implies_BSD_for_modified_view:
"BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub>\<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub> \<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub> \<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
assume BSD_\<V>\<^sub>1: "BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub>"
[PROOF STATE]
proof (state)
this:
BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub> \<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub> \<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
fix \<alpha> \<beta> c n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub> \<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
assume  c_in_C\<^sub>2: "c \<in> C\<^bsub>\<V>\<^sub>2\<^esub>"
[PROOF STATE]
proof (state)
this:
c \<in> C\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub> \<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
from C2_subset_C1  c_in_C\<^sub>2
[PROOF STATE]
proof (chain)
picking this:
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>
c \<in> C\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
have c_in_C\<^sub>1: "c \<in> C\<^bsub>\<V>\<^sub>1\<^esub>"
[PROOF STATE]
proof (prove)
using this:
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>
c \<in> C\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. c \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> C\<^bsub>\<V>\<^sub>1\<^esub>

goal (1 subgoal):
 1. BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub> \<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
have "\<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub>=[]; n= length(\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk>
            \<Longrightarrow> \<exists> \<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'\<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft>V\<^bsub>\<V>\<^sub>2\<^esub>  \<and> \<alpha>' \<upharpoonleft>C\<^bsub>\<V>\<^sub>2\<^esub> = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
proof(induct n arbitrary: \<alpha>  )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; 0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
 2. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)

goal (2 subgoals):
 1. \<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; 0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
 2. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from "0.prems"(3)
[PROOF STATE]
proof (chain)
picking this:
0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)
[PROOF STEP]
have "\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []"
[PROOF STATE]
proof (prove)
using this:
0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)

goal (1 subgoal):
 1. \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []

goal (2 subgoals):
 1. \<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; 0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
 2. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
with c_in_C\<^sub>1 "0.prems"(1)
[PROOF STATE]
proof (chain)
picking this:
c \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
[PROOF STEP]
have "\<exists> \<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha>' \<upharpoonleft>C\<^bsub>\<V>\<^sub>1\<^esub> =[]"
[PROOF STATE]
proof (prove)
using this:
c \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []

goal (1 subgoal):
 1. \<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
[PROOF STEP]
using BSD_\<V>\<^sub>1
[PROOF STATE]
proof (prove)
using this:
c \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. \<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
[PROOF STEP]
unfolding BSD_def
[PROOF STATE]
proof (prove)
using this:
c \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
\<forall>\<alpha> \<beta>. \<forall>c\<in>C\<^bsub>\<V>\<^sub>1\<^esub>. \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = [] \<longrightarrow> (\<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = [])

goal (1 subgoal):
 1. \<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []

goal (2 subgoals):
 1. \<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; 0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
 2. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
[PROOF STEP]
obtain \<alpha>' where "\<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub>"
                    and "\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>"
                    and "\<alpha>' \<upharpoonleft>C\<^bsub>\<V>\<^sub>1\<^esub> =[]"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []

goal (1 subgoal):
 1. (\<And>\<alpha>''. \<lbrakk>\<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub>; \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>; \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub>
\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>
\<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []

goal (2 subgoals):
 1. \<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; 0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
 2. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from V2_subset_V1  \<open>\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
V\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> V\<^bsub>\<V>\<^sub>1\<^esub>
\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>
[PROOF STEP]
have  "\<alpha>'\<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft>V\<^bsub>\<V>\<^sub>2\<^esub>"
[PROOF STATE]
proof (prove)
using this:
V\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> V\<^bsub>\<V>\<^sub>1\<^esub>
\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>

goal (1 subgoal):
 1. \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
using non_empty_projection_on_subset
[PROOF STATE]
proof (prove)
using this:
V\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> V\<^bsub>\<V>\<^sub>1\<^esub>
\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>
?X \<subseteq> ?Y \<and> ?l\<^sub>1 \<upharpoonleft> ?Y = ?l\<^sub>2 \<upharpoonleft> ?Y \<Longrightarrow> ?l\<^sub>1 \<upharpoonleft> ?X = ?l\<^sub>2 \<upharpoonleft> ?X

goal (1 subgoal):
 1. \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (2 subgoals):
 1. \<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; 0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
 2. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (2 subgoals):
 1. \<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; 0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
 2. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from \<open>\<alpha>' \<upharpoonleft>C\<^bsub>\<V>\<^sub>1\<^esub> =[]\<close>  C2_subset_C1
[PROOF STATE]
proof (chain)
picking this:
\<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>
[PROOF STEP]
have "\<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []"
[PROOF STATE]
proof (prove)
using this:
\<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>

goal (1 subgoal):
 1. \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
using projection_on_subset
[PROOF STATE]
proof (prove)
using this:
\<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>
\<lbrakk>?Y \<subseteq> ?X; ?l \<upharpoonleft> ?X = []\<rbrakk> \<Longrightarrow> ?l \<upharpoonleft> ?Y = []

goal (1 subgoal):
 1. \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (2 subgoals):
 1. \<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; 0 = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
 2. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
\<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
\<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. \<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
using \<open>\<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
\<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
\<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
\<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. \<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<beta> @ [c] @ ?\<alpha> \<in> Tr\<^bsub>ES\<^esub>; ?\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (?\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = ?\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from "Suc.prems"(3) projection_split_last[OF "Suc.prems"(3)]
[PROOF STATE]
proof (chain)
picking this:
Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)
\<exists>\<beta> x \<alpha>. x \<in> C\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)
[PROOF STEP]
obtain \<gamma>\<^sub>1 \<gamma>\<^sub>2 c\<^sub>1 where c\<^sub>1_in_C\<^sub>1: "c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>"
                         and "\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2"
                         and "\<gamma>\<^sub>2 \<upharpoonleft>C\<^bsub>\<V>\<^sub>1\<^esub> = []"
                         and "n = length((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2)\<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)
\<exists>\<beta> x \<alpha>. x \<in> C\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)

goal (1 subgoal):
 1. (\<And>c\<^sub>1 \<gamma>\<^sub>1 \<gamma>\<^sub>2. \<lbrakk>c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>; \<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2; \<gamma>\<^sub>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []; n = length ((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2) \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2
\<gamma>\<^sub>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
n = length ((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2) \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from  "Suc.prems"(2) \<open>\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2\<close>
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2
[PROOF STEP]
have "\<gamma>\<^sub>1 \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2

goal (1 subgoal):
 1. \<gamma>\<^sub>1 \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
by (simp add: projection_concatenation_commute)
[PROOF STATE]
proof (state)
this:
\<gamma>\<^sub>1 \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from  "Suc.prems"(1) \<open>\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2\<close>
[PROOF STATE]
proof (chain)
picking this:
\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2
[PROOF STEP]
obtain \<beta>' where "\<beta>'=\<beta> @ [c] @ \<gamma>\<^sub>1"
                    and "\<beta>' @ [c\<^sub>1] @ \<gamma>\<^sub>2 \<in> Tr\<^bsub>ES\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2

goal (1 subgoal):
 1. (\<And>\<beta>'. \<lbrakk>\<beta>' = \<beta> @ [c] @ \<gamma>\<^sub>1; \<beta>' @ [c\<^sub>1] @ \<gamma>\<^sub>2 \<in> Tr\<^bsub>ES\<^esub>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<beta>' = \<beta> @ [c] @ \<gamma>\<^sub>1
\<beta>' @ [c\<^sub>1] @ \<gamma>\<^sub>2 \<in> Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from \<open>\<beta>' @ [c\<^sub>1] @ \<gamma>\<^sub>2 \<in> Tr\<^bsub>ES\<^esub>\<close>  \<open>\<gamma>\<^sub>2 \<upharpoonleft>C\<^bsub>\<V>\<^sub>1\<^esub> = []\<close> \<open>c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<beta>' @ [c\<^sub>1] @ \<gamma>\<^sub>2 \<in> Tr\<^bsub>ES\<^esub>
\<gamma>\<^sub>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
[PROOF STEP]
obtain \<gamma>\<^sub>2' where " \<beta>' @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>"
                    and "\<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>"
                    and "\<gamma>\<^sub>2' \<upharpoonleft>C\<^bsub>\<V>\<^sub>1\<^esub> =[]"
[PROOF STATE]
proof (prove)
using this:
\<beta>' @ [c\<^sub>1] @ \<gamma>\<^sub>2 \<in> Tr\<^bsub>ES\<^esub>
\<gamma>\<^sub>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>

goal (1 subgoal):
 1. (\<And>\<gamma>\<^sub>2'. \<lbrakk>\<beta>' @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>; \<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>; \<gamma>\<^sub>2' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using BSD_\<V>\<^sub>1
[PROOF STATE]
proof (prove)
using this:
\<beta>' @ [c\<^sub>1] @ \<gamma>\<^sub>2 \<in> Tr\<^bsub>ES\<^esub>
\<gamma>\<^sub>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. (\<And>\<gamma>\<^sub>2'. \<lbrakk>\<beta>' @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>; \<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>; \<gamma>\<^sub>2' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding BSD_def
[PROOF STATE]
proof (prove)
using this:
\<beta>' @ [c\<^sub>1] @ \<gamma>\<^sub>2 \<in> Tr\<^bsub>ES\<^esub>
\<gamma>\<^sub>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
\<forall>\<alpha> \<beta>. \<forall>c\<in>C\<^bsub>\<V>\<^sub>1\<^esub>. \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = [] \<longrightarrow> (\<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = [])

goal (1 subgoal):
 1. (\<And>\<gamma>\<^sub>2'. \<lbrakk>\<beta>' @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>; \<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>; \<gamma>\<^sub>2' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<beta>' @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>
\<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>
\<gamma>\<^sub>2' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from \<open>\<beta>'=\<beta> @ [c] @ \<gamma>\<^sub>1\<close> \<open>\<beta>' @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<beta>' = \<beta> @ [c] @ \<gamma>\<^sub>1
\<beta>' @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
have "\<beta> @ [c] @ \<gamma>\<^sub>1 @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<beta>' = \<beta> @ [c] @ \<gamma>\<^sub>1
\<beta>' @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. \<beta> @ [c] @ \<gamma>\<^sub>1 @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<beta> @ [c] @ \<gamma>\<^sub>1 @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<beta> @ [c] @ \<gamma>\<^sub>1 @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from  \<open>\<gamma>\<^sub>1 \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub>=[]\<close>  \<open>\<gamma>\<^sub>2' \<upharpoonleft>C\<^bsub>\<V>\<^sub>1\<^esub> =[]\<close> C2_subset_C1
[PROOF STATE]
proof (chain)
picking this:
\<gamma>\<^sub>1 \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
\<gamma>\<^sub>2' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>
[PROOF STEP]
have "(\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> =[]"
[PROOF STATE]
proof (prove)
using this:
\<gamma>\<^sub>1 \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
\<gamma>\<^sub>2' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>

goal (1 subgoal):
 1. (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
by (metis append_Nil projection_concatenation_commute projection_on_subset)
[PROOF STATE]
proof (state)
this:
(\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from \<open>n = length((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2)\<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<close> \<open>\<gamma>\<^sub>2 \<upharpoonleft>C\<^bsub>\<V>\<^sub>1\<^esub> = []\<close> \<open>\<gamma>\<^sub>2' \<upharpoonleft>C\<^bsub>\<V>\<^sub>1\<^esub> =[]\<close>
[PROOF STATE]
proof (chain)
picking this:
n = length ((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2) \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)
\<gamma>\<^sub>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
\<gamma>\<^sub>2' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
[PROOF STEP]
have "n = length((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2')\<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
n = length ((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2) \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)
\<gamma>\<^sub>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []
\<gamma>\<^sub>2' \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub> = []

goal (1 subgoal):
 1. n = length ((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)
[PROOF STEP]
by (simp add: projection_concatenation_commute)
[PROOF STATE]
proof (state)
this:
n = length ((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<beta> @ [c] @ \<gamma>\<^sub>1 @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>
(\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
n = length ((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)
[PROOF STEP]
have witness: "\<exists> \<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'\<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft>V\<^bsub>\<V>\<^sub>2\<^esub>  \<and> \<alpha>' \<upharpoonleft>C\<^bsub>\<V>\<^sub>2\<^esub> = []"
[PROOF STATE]
proof (prove)
using this:
\<beta> @ [c] @ \<gamma>\<^sub>1 @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>
(\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
n = length ((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)

goal (1 subgoal):
 1. \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
using  Suc.hyps
[PROOF STATE]
proof (prove)
using this:
\<beta> @ [c] @ \<gamma>\<^sub>1 @ \<gamma>\<^sub>2' \<in> Tr\<^bsub>ES\<^esub>
(\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
n = length ((\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)
\<lbrakk>\<beta> @ [c] @ ?\<alpha> \<in> Tr\<^bsub>ES\<^esub>; ?\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (?\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = ?\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from  \<V>\<^sub>1IsViewOnE \<V>\<^sub>2IsViewOnE V2_subset_V1 C2_subset_C1  c\<^sub>1_in_C\<^sub>1
[PROOF STATE]
proof (chain)
picking this:
isViewOn \<V>\<^sub>1 E\<^bsub>ES\<^esub>
isViewOn \<V>\<^sub>2 E\<^bsub>ES\<^esub>
V\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> V\<^bsub>\<V>\<^sub>1\<^esub>
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>
c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>
[PROOF STEP]
have "c\<^sub>1 \<notin> V\<^bsub>\<V>\<^sub>2\<^esub>"
[PROOF STATE]
proof (prove)
using this:
isViewOn \<V>\<^sub>1 E\<^bsub>ES\<^esub>
isViewOn \<V>\<^sub>2 E\<^bsub>ES\<^esub>
V\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> V\<^bsub>\<V>\<^sub>1\<^esub>
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>
c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>

goal (1 subgoal):
 1. c\<^sub>1 \<notin> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
unfolding isViewOn_def V_valid_def  VC_disjoint_def
[PROOF STATE]
proof (prove)
using this:
(VN_disjoint \<V>\<^sub>1 \<and> V\<^bsub>\<V>\<^sub>1\<^esub> \<inter> C\<^bsub>\<V>\<^sub>1\<^esub> = {} \<and> NC_disjoint \<V>\<^sub>1) \<and> V\<^bsub>\<V>\<^sub>1\<^esub> \<union> N\<^bsub>\<V>\<^sub>1\<^esub> \<union> C\<^bsub>\<V>\<^sub>1\<^esub> = E\<^bsub>ES\<^esub>
(VN_disjoint \<V>\<^sub>2 \<and> V\<^bsub>\<V>\<^sub>2\<^esub> \<inter> C\<^bsub>\<V>\<^sub>2\<^esub> = {} \<and> NC_disjoint \<V>\<^sub>2) \<and> V\<^bsub>\<V>\<^sub>2\<^esub> \<union> N\<^bsub>\<V>\<^sub>2\<^esub> \<union> C\<^bsub>\<V>\<^sub>2\<^esub> = E\<^bsub>ES\<^esub>
V\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> V\<^bsub>\<V>\<^sub>1\<^esub>
C\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> C\<^bsub>\<V>\<^sub>1\<^esub>
c\<^sub>1 \<in> C\<^bsub>\<V>\<^sub>1\<^esub>

goal (1 subgoal):
 1. c\<^sub>1 \<notin> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<notin> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
with \<open>\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2\<close>
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2
c\<^sub>1 \<notin> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
have "\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2) \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2
c\<^sub>1 \<notin> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2) \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
unfolding projection_def
[PROOF STATE]
proof (prove)
using this:
\<alpha> = \<gamma>\<^sub>1 @ [c\<^sub>1] @ \<gamma>\<^sub>2
c\<^sub>1 \<notin> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> V\<^bsub>\<V>\<^sub>2\<^esub>) \<alpha> = filter (\<lambda>x. x \<in> V\<^bsub>\<V>\<^sub>2\<^esub>) (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2) \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
hence "\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> "
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2) \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
using projection_concatenation_commute
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2) \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
(?l1.0 @ ?l2.0) \<upharpoonleft> ?X = ?l1.0 \<upharpoonleft> ?X @ ?l2.0 \<upharpoonleft> ?X

goal (1 subgoal):
 1. \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
with V2_subset_V1 \<open>\<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
V\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> V\<^bsub>\<V>\<^sub>1\<^esub>
\<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
have "\<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1\<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>"
[PROOF STATE]
proof (prove)
using this:
V\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> V\<^bsub>\<V>\<^sub>1\<^esub>
\<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
using non_empty_projection_on_subset
[PROOF STATE]
proof (prove)
using this:
V\<^bsub>\<V>\<^sub>2\<^esub> \<subseteq> V\<^bsub>\<V>\<^sub>1\<^esub>
\<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub> = \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>1\<^esub>
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
?X \<subseteq> ?Y \<and> ?l\<^sub>1 \<upharpoonleft> ?Y = ?l\<^sub>2 \<upharpoonleft> ?Y \<Longrightarrow> ?l\<^sub>1 \<upharpoonleft> ?X = ?l\<^sub>2 \<upharpoonleft> ?X

goal (1 subgoal):
 1. \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
with \<open>\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
\<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
have "\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
\<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<gamma>\<^sub>1 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> @ \<gamma>\<^sub>2' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
by (simp add: projection_concatenation_commute)
[PROOF STATE]
proof (state)
this:
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<And>n \<alpha>. \<lbrakk>\<And>\<alpha>. \<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; Suc n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
from witness  \<open>\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
\<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = (\<gamma>\<^sub>1 @ \<gamma>\<^sub>2') \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub>

goal (1 subgoal):
 1. \<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>''. \<beta> @ \<alpha>'' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>'' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>'' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>; \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; n = length (\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub> \<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c2 \<in> C\<^bsub>\<V>\<^sub>2\<^esub>; ?\<beta>2 @ [?c2] @ ?\<alpha>2 \<in> Tr\<^bsub>ES\<^esub>; ?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; ?n2 = length (?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. ?\<beta>2 @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = ?\<alpha>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. BSD \<V>\<^sub>1 Tr\<^bsub>ES\<^esub> \<Longrightarrow> BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c2 \<in> C\<^bsub>\<V>\<^sub>2\<^esub>; ?\<beta>2 @ [?c2] @ ?\<alpha>2 \<in> Tr\<^bsub>ES\<^esub>; ?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; ?n2 = length (?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. ?\<beta>2 @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = ?\<alpha>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>
[PROOF STEP]
unfolding BSD_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c2 \<in> C\<^bsub>\<V>\<^sub>2\<^esub>; ?\<beta>2 @ [?c2] @ ?\<alpha>2 \<in> Tr\<^bsub>ES\<^esub>; ?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []; ?n2 = length (?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^sub>1\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>'. ?\<beta>2 @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = ?\<alpha>2 \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = []

goal (1 subgoal):
 1. \<forall>\<alpha> \<beta>. \<forall>c\<in>C\<^bsub>\<V>\<^sub>2\<^esub>. \<beta> @ [c] @ \<alpha> \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = [] \<longrightarrow> (\<exists>\<alpha>'. \<beta> @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^sub>2\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^sub>2\<^esub> = [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
BSD \<V>\<^sub>2 Tr\<^bsub>ES\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakRes:
  fixes P  :: ccs
  and   \<alpha>  :: act
  and   P' :: ccs
  and   x  :: name

  assumes "P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"
  and     "x \<sharp> \<alpha>"

  shows "\<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<alpha> \<prec> \<lparr>\<nu>x\<rparr>P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<alpha> \<prec> \<lparr>\<nu>x\<rparr>P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'
x \<sharp> \<alpha>

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<alpha> \<prec> \<lparr>\<nu>x\<rparr>P'
[PROOF STEP]
by(auto simp add: weakTrans_def intro: weakCongRes)


[STATEMENT]
lemma dotprod_eq_nonzero_iff:
  assumes "a \<bullet> x = b \<bullet> y" and "length x = length a" and "length y = length b"
    and "0 \<notin> set a" and "0 \<notin> set b"
  shows "nonzero x \<longleftrightarrow> nonzero y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonzero x = nonzero y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<bullet> x = b \<bullet> y
length x = length a
length y = length b
0 \<notin> set a
0 \<notin> set b

goal (1 subgoal):
 1. nonzero x = nonzero y
[PROOF STEP]
by (auto simp: nonzero_iff) (metis dotprod_commute dotprod_eq_0_iff neq0_conv)+


[STATEMENT]
lemma symmetric_mk_symmetric:
  "symmetric (mk_symmetric G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric (with_proj (mk_symmetric G))
[PROOF STEP]
by (auto simp: symmetric_def parcs_mk_symmetric intro: symI)


[STATEMENT]
lemma essential_BI: "\<And>B. x \<in> B \<Longrightarrow> essential G B S x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>B. x \<in> B \<Longrightarrow> essential G B S x
[PROOF STEP]
by(auto simp add: essential_def intro: rtrancl_path.base)


[STATEMENT]
lemma verts_nempty: "verts G \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verts G \<noteq> {}
[PROOF STEP]
using connected connected_iff_reachable
[PROOF STATE]
proof (prove)
using this:
Digraph_Component.connected G
Digraph_Component.connected G = ((\<forall>x\<in>verts G. \<forall>y\<in>verts G. x \<rightarrow>\<^sup>*\<^bsub>G\<^esub> y) \<and> verts G \<noteq> {})

goal (1 subgoal):
 1. verts G \<noteq> {}
[PROOF STEP]
by auto