[STATEMENT]
lemma adj_sub_geq2_fact:"\<And>i j x1 x2. i\<in>SIGT x2 \<Longrightarrow> j \<in> (case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<Longrightarrow> Inl i \<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union>
         {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter>
        {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2. \<lbrakk>i \<in> SIGT x2; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2. \<lbrakk>i \<in> SIGT x2; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x2. \<lbrakk>i \<in> SIGT x2; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT x2_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<in> SIGT x2_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
 2. \<And>a. \<lbrakk>i \<in> SIGT x2_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done