[STATEMENT]
lemma I_implies_IA: 
"I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
assume I: "I \<V> Tr\<^bsub>ES\<^esub>"
[PROOF STATE]
proof (state)
this:
I \<V> Tr\<^bsub>ES\<^esub>

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

goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
fix \<alpha> \<beta> c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
assume "c \<in> C\<^bsub>\<V>\<^esub>"
      and  "\<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>"
      and  "\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []"
      and  "Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c"
[PROOF STATE]
proof (state)
this:
c \<in> C\<^bsub>\<V>\<^esub>
\<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []
Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c

goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
with I
[PROOF STATE]
proof (chain)
picking this:
I \<V> Tr\<^bsub>ES\<^esub>
c \<in> C\<^bsub>\<V>\<^esub>
\<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []
Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c
[PROOF STEP]
have "\<exists> \<alpha>' \<beta>'. \<beta>' @ (c # \<alpha>') \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^esub>  
                            \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []  \<and> \<beta>' \<upharpoonleft>(V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = \<beta> \<upharpoonleft>(V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) "
[PROOF STATE]
proof (prove)
using this:
I \<V> Tr\<^bsub>ES\<^esub>
c \<in> C\<^bsub>\<V>\<^esub>
\<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []
Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c

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

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

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

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

goal (1 subgoal):
 1. IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
unfolding I_def IA_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c2 \<in> C\<^bsub>\<V>\<^esub>; ?\<beta>2 @ ?\<alpha>2 \<in> Tr\<^bsub>ES\<^esub>; ?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []; Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> ?\<beta>2 ?c2\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<beta>' @ ?c2 # \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = ?\<alpha>2 \<upharpoonleft> V\<^bsub>\<V>\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> \<beta>' \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = ?\<beta>2 \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>)

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

goal:
No subgoals!
[PROOF STEP]
qed