[STATEMENT]
lemma projection_split_arbitrary_element:
  "\<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X \<rbrakk>
      \<Longrightarrow> \<exists> \<alpha>' \<beta>'. (\<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
assume "\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X"
  and  " x \<in> X"
[PROOF STATE]
proof (state)
this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
x \<in> X

goal (1 subgoal):
 1. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
x \<in> X

goal (1 subgoal):
 1. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
have "\<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length(\<alpha>\<upharpoonleft>X) \<rbrakk>
          \<Longrightarrow> \<exists> \<alpha>' \<beta>'. (\<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
proof (induct n arbitrary: \<tau> \<alpha> )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; 0 = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
 2. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
x \<in> X
0 = length (\<alpha> \<upharpoonleft> X)

goal (2 subgoals):
 1. \<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; 0 = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
 2. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
hence "\<alpha>\<upharpoonleft>X = []"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
x \<in> X
0 = length (\<alpha> \<upharpoonleft> X)

goal (1 subgoal):
 1. \<alpha> \<upharpoonleft> X = []
[PROOF STEP]
unfolding projection_def
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>x. x \<in> X) \<tau> = filter (\<lambda>x. x \<in> X) (\<alpha> @ [x] @ \<beta>)
x \<in> X
0 = length (filter (\<lambda>x. x \<in> X) \<alpha>)

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> X) \<alpha> = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<alpha> \<upharpoonleft> X = []

goal (2 subgoals):
 1. \<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; 0 = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
 2. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
with "0.prems"(1) "0.prems"(2)
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
x \<in> X
\<alpha> \<upharpoonleft> X = []
[PROOF STEP]
have "\<tau>\<upharpoonleft>X = x # \<beta>\<upharpoonleft>X"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
x \<in> X
\<alpha> \<upharpoonleft> X = []

goal (1 subgoal):
 1. \<tau> \<upharpoonleft> X = x # \<beta> \<upharpoonleft> X
[PROOF STEP]
unfolding projection_def
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>x. x \<in> X) \<tau> = filter (\<lambda>x. x \<in> X) (\<alpha> @ [x] @ \<beta>)
x \<in> X
filter (\<lambda>x. x \<in> X) \<alpha> = []

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> X) \<tau> = x # filter (\<lambda>x. x \<in> X) \<beta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<tau> \<upharpoonleft> X = x # \<beta> \<upharpoonleft> X

goal (2 subgoals):
 1. \<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; 0 = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
 2. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
with \<open>\<alpha>\<upharpoonleft>X = []\<close>
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<upharpoonleft> X = []
\<tau> \<upharpoonleft> X = x # \<beta> \<upharpoonleft> X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> X = []
\<tau> \<upharpoonleft> X = x # \<beta> \<upharpoonleft> X

goal (1 subgoal):
 1. \<exists>\<alpha>'' \<beta>'. \<tau> = \<alpha>'' @ [x] @ \<beta>' \<and> \<alpha>'' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
using projection_split_first_with_suffix
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> X = []
\<tau> \<upharpoonleft> X = x # \<beta> \<upharpoonleft> X
?\<tau> \<upharpoonleft> ?X = ?x # ?xs \<Longrightarrow> \<exists>\<alpha> \<beta>. ?\<tau> = \<alpha> @ [?x] @ \<beta> \<and> \<alpha> \<upharpoonleft> ?X = [] \<and> \<beta> \<upharpoonleft> ?X = ?xs

goal (1 subgoal):
 1. \<exists>\<alpha>'' \<beta>'. \<tau> = \<alpha>'' @ [x] @ \<beta>' \<and> \<alpha>'' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>'' \<beta>'. \<tau> = \<alpha>'' @ [x] @ \<beta>' \<and> \<alpha>'' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<tau> \<upharpoonleft> X = (?\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (?\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. ?\<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = ?\<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
x \<in> X
Suc n = length (\<alpha> \<upharpoonleft> X)

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
from "Suc.prems"(1)
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
[PROOF STEP]
have "\<tau>\<upharpoonleft>X=\<alpha>\<upharpoonleft>X @ ([x] @ \<beta>) \<upharpoonleft>X"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X

goal (1 subgoal):
 1. \<tau> \<upharpoonleft> X = \<alpha> \<upharpoonleft> X @ ([x] @ \<beta>) \<upharpoonleft> X
[PROOF STEP]
using projection_concatenation_commute
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
(?l1.0 @ ?l2.0) \<upharpoonleft> ?X = ?l1.0 \<upharpoonleft> ?X @ ?l2.0 \<upharpoonleft> ?X

goal (1 subgoal):
 1. \<tau> \<upharpoonleft> X = \<alpha> \<upharpoonleft> X @ ([x] @ \<beta>) \<upharpoonleft> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> \<upharpoonleft> X = \<alpha> \<upharpoonleft> X @ ([x] @ \<beta>) \<upharpoonleft> X

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
from "Suc.prems"(3)
[PROOF STATE]
proof (chain)
picking this:
Suc n = length (\<alpha> \<upharpoonleft> X)
[PROOF STEP]
obtain x' xs' where "\<alpha> \<upharpoonleft>X= x' #xs'"
                                            and "x' \<in> X"
[PROOF STATE]
proof (prove)
using this:
Suc n = length (\<alpha> \<upharpoonleft> X)

goal (1 subgoal):
 1. (\<And>x' xs'. \<lbrakk>\<alpha> \<upharpoonleft> X = x' # xs'; x' \<in> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis filter_eq_ConsD length_Suc_conv projection_def)
[PROOF STATE]
proof (state)
this:
\<alpha> \<upharpoonleft> X = x' # xs'
x' \<in> X

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<upharpoonleft> X = x' # xs'
x' \<in> X
[PROOF STEP]
obtain a\<^sub>1 a\<^sub>2 where "\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2"
                         and "a\<^sub>1\<upharpoonleft>X = []"
                         and "a\<^sub>2\<upharpoonleft>X = xs'"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> X = x' # xs'
x' \<in> X

goal (1 subgoal):
 1. (\<And>a\<^sub>1 a\<^sub>2. \<lbrakk>\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2; a\<^sub>1 \<upharpoonleft> X = []; a\<^sub>2 \<upharpoonleft> X = xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using projection_split_first_with_suffix
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> X = x' # xs'
x' \<in> X
?\<tau> \<upharpoonleft> ?X = ?x # ?xs \<Longrightarrow> \<exists>\<alpha> \<beta>. ?\<tau> = \<alpha> @ [?x] @ \<beta> \<and> \<alpha> \<upharpoonleft> ?X = [] \<and> \<beta> \<upharpoonleft> ?X = ?xs

goal (1 subgoal):
 1. (\<And>a\<^sub>1 a\<^sub>2. \<lbrakk>\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2; a\<^sub>1 \<upharpoonleft> X = []; a\<^sub>2 \<upharpoonleft> X = xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2
a\<^sub>1 \<upharpoonleft> X = []
a\<^sub>2 \<upharpoonleft> X = xs'

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
with \<open>x' \<in> X\<close> "Suc.prems"(1)
[PROOF STATE]
proof (chain)
picking this:
x' \<in> X
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2
a\<^sub>1 \<upharpoonleft> X = []
a\<^sub>2 \<upharpoonleft> X = xs'
[PROOF STEP]
have "\<tau>\<upharpoonleft>X= x' #  (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft>X"
[PROOF STATE]
proof (prove)
using this:
x' \<in> X
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2
a\<^sub>1 \<upharpoonleft> X = []
a\<^sub>2 \<upharpoonleft> X = xs'

goal (1 subgoal):
 1. \<tau> \<upharpoonleft> X = x' # (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X
[PROOF STEP]
unfolding projection_def
[PROOF STATE]
proof (prove)
using this:
x' \<in> X
filter (\<lambda>x. x \<in> X) \<tau> = filter (\<lambda>x. x \<in> X) (\<alpha> @ [x] @ \<beta>)
\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2
filter (\<lambda>x. x \<in> X) a\<^sub>1 = []
filter (\<lambda>x. x \<in> X) a\<^sub>2 = xs'

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> X) \<tau> = x' # filter (\<lambda>x. x \<in> X) (a\<^sub>2 @ [x] @ \<beta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<tau> \<upharpoonleft> X = x' # (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<upharpoonleft> X = x' # (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X
[PROOF STEP]
obtain t\<^sub>1 t\<^sub>2 where "\<tau>= t\<^sub>1 @ [x'] @ t\<^sub>2"
                         and "t\<^sub>1\<upharpoonleft>X = []"
                         and "t\<^sub>2\<upharpoonleft>X = (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft>X"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = x' # (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X

goal (1 subgoal):
 1. (\<And>t\<^sub>1 t\<^sub>2. \<lbrakk>\<tau> = t\<^sub>1 @ [x'] @ t\<^sub>2; t\<^sub>1 \<upharpoonleft> X = []; t\<^sub>2 \<upharpoonleft> X = (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using projection_split_first_with_suffix
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = x' # (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X
?\<tau> \<upharpoonleft> ?X = ?x # ?xs \<Longrightarrow> \<exists>\<alpha> \<beta>. ?\<tau> = \<alpha> @ [?x] @ \<beta> \<and> \<alpha> \<upharpoonleft> ?X = [] \<and> \<beta> \<upharpoonleft> ?X = ?xs

goal (1 subgoal):
 1. (\<And>t\<^sub>1 t\<^sub>2. \<lbrakk>\<tau> = t\<^sub>1 @ [x'] @ t\<^sub>2; t\<^sub>1 \<upharpoonleft> X = []; t\<^sub>2 \<upharpoonleft> X = (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<tau> = t\<^sub>1 @ [x'] @ t\<^sub>2
t\<^sub>1 \<upharpoonleft> X = []
t\<^sub>2 \<upharpoonleft> X = (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
from Suc.prems(3) \<open>\<alpha> \<upharpoonleft>X= x' # xs'\<close> \<open>\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2\<close> \<open>a\<^sub>1\<upharpoonleft>X = []\<close> \<open>a\<^sub>2\<upharpoonleft>X = xs'\<close>
[PROOF STATE]
proof (chain)
picking this:
Suc n = length (\<alpha> \<upharpoonleft> X)
\<alpha> \<upharpoonleft> X = x' # xs'
\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2
a\<^sub>1 \<upharpoonleft> X = []
a\<^sub>2 \<upharpoonleft> X = xs'
[PROOF STEP]
have "n=length(a\<^sub>2\<upharpoonleft>X)"
[PROOF STATE]
proof (prove)
using this:
Suc n = length (\<alpha> \<upharpoonleft> X)
\<alpha> \<upharpoonleft> X = x' # xs'
\<alpha> = a\<^sub>1 @ [x'] @ a\<^sub>2
a\<^sub>1 \<upharpoonleft> X = []
a\<^sub>2 \<upharpoonleft> X = xs'

goal (1 subgoal):
 1. n = length (a\<^sub>2 \<upharpoonleft> X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = length (a\<^sub>2 \<upharpoonleft> X)

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
with "Suc.hyps"(1) "Suc.prems"(2) \<open>t\<^sub>2\<upharpoonleft>X = (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft>X\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<tau> \<upharpoonleft> X = (?\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (?\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. ?\<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = ?\<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
x \<in> X
t\<^sub>2 \<upharpoonleft> X = (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X
n = length (a\<^sub>2 \<upharpoonleft> X)
[PROOF STEP]
obtain t\<^sub>2' t\<^sub>3' where "t\<^sub>2=t\<^sub>2' @ [x] @ t\<^sub>3'"
                         and "t\<^sub>2'\<upharpoonleft>X = a\<^sub>2\<upharpoonleft>X"
                         and "t\<^sub>3'\<upharpoonleft>X = \<beta>\<upharpoonleft>X"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<tau> \<upharpoonleft> X = (?\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (?\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. ?\<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = ?\<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
x \<in> X
t\<^sub>2 \<upharpoonleft> X = (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X
n = length (a\<^sub>2 \<upharpoonleft> X)

goal (1 subgoal):
 1. (\<And>t\<^sub>2' t\<^sub>3'. \<lbrakk>t\<^sub>2 = t\<^sub>2' @ [x] @ t\<^sub>3'; t\<^sub>2' \<upharpoonleft> X = a\<^sub>2 \<upharpoonleft> X; t\<^sub>3' \<upharpoonleft> X = \<beta> \<upharpoonleft> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using projection_concatenation_commute
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<tau> \<upharpoonleft> X = (?\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (?\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. ?\<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = ?\<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
x \<in> X
t\<^sub>2 \<upharpoonleft> X = (a\<^sub>2 @ [x] @ \<beta>) \<upharpoonleft> X
n = length (a\<^sub>2 \<upharpoonleft> X)
(?l1.0 @ ?l2.0) \<upharpoonleft> ?X = ?l1.0 \<upharpoonleft> ?X @ ?l2.0 \<upharpoonleft> ?X

goal (1 subgoal):
 1. (\<And>t\<^sub>2' t\<^sub>3'. \<lbrakk>t\<^sub>2 = t\<^sub>2' @ [x] @ t\<^sub>3'; t\<^sub>2' \<upharpoonleft> X = a\<^sub>2 \<upharpoonleft> X; t\<^sub>3' \<upharpoonleft> X = \<beta> \<upharpoonleft> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t\<^sub>2 = t\<^sub>2' @ [x] @ t\<^sub>3'
t\<^sub>2' \<upharpoonleft> X = a\<^sub>2 \<upharpoonleft> X
t\<^sub>3' \<upharpoonleft> X = \<beta> \<upharpoonleft> X

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
let ?\<alpha>'="t\<^sub>1 @ [x'] @ t\<^sub>2'" and ?\<beta>'="t\<^sub>3'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
from \<open>\<tau>= t\<^sub>1 @ [x'] @ t\<^sub>2\<close> \<open>t\<^sub>2=t\<^sub>2' @ [x] @ t\<^sub>3'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<tau> = t\<^sub>1 @ [x'] @ t\<^sub>2
t\<^sub>2 = t\<^sub>2' @ [x] @ t\<^sub>3'
[PROOF STEP]
have "\<tau>=?\<alpha>'@[x]@?\<beta>'"
[PROOF STATE]
proof (prove)
using this:
\<tau> = t\<^sub>1 @ [x'] @ t\<^sub>2
t\<^sub>2 = t\<^sub>2' @ [x] @ t\<^sub>3'

goal (1 subgoal):
 1. \<tau> = (t\<^sub>1 @ [x'] @ t\<^sub>2') @ [x] @ t\<^sub>3'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> = (t\<^sub>1 @ [x'] @ t\<^sub>2') @ [x] @ t\<^sub>3'

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<tau> = (t\<^sub>1 @ [x'] @ t\<^sub>2') @ [x] @ t\<^sub>3'

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
from  \<open>\<alpha> \<upharpoonleft>X= x' # xs'\<close>  \<open>t\<^sub>1\<upharpoonleft>X = []\<close> \<open>x' \<in> X\<close> \<open>t\<^sub>2'\<upharpoonleft>X = a\<^sub>2\<upharpoonleft>X\<close> \<open>a\<^sub>2\<upharpoonleft>X = xs'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<upharpoonleft> X = x' # xs'
t\<^sub>1 \<upharpoonleft> X = []
x' \<in> X
t\<^sub>2' \<upharpoonleft> X = a\<^sub>2 \<upharpoonleft> X
a\<^sub>2 \<upharpoonleft> X = xs'
[PROOF STEP]
have "?\<alpha>'\<upharpoonleft>X = \<alpha>\<upharpoonleft>X"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> X = x' # xs'
t\<^sub>1 \<upharpoonleft> X = []
x' \<in> X
t\<^sub>2' \<upharpoonleft> X = a\<^sub>2 \<upharpoonleft> X
a\<^sub>2 \<upharpoonleft> X = xs'

goal (1 subgoal):
 1. (t\<^sub>1 @ [x'] @ t\<^sub>2') \<upharpoonleft> X = \<alpha> \<upharpoonleft> X
[PROOF STEP]
using projection_concatenation_commute
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> X = x' # xs'
t\<^sub>1 \<upharpoonleft> X = []
x' \<in> X
t\<^sub>2' \<upharpoonleft> X = a\<^sub>2 \<upharpoonleft> X
a\<^sub>2 \<upharpoonleft> X = xs'
(?l1.0 @ ?l2.0) \<upharpoonleft> ?X = ?l1.0 \<upharpoonleft> ?X @ ?l2.0 \<upharpoonleft> ?X

goal (1 subgoal):
 1. (t\<^sub>1 @ [x'] @ t\<^sub>2') \<upharpoonleft> X = \<alpha> \<upharpoonleft> X
[PROOF STEP]
unfolding projection_def
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>x. x \<in> X) \<alpha> = x' # xs'
filter (\<lambda>x. x \<in> X) t\<^sub>1 = []
x' \<in> X
filter (\<lambda>x. x \<in> X) t\<^sub>2' = filter (\<lambda>x. x \<in> X) a\<^sub>2
filter (\<lambda>x. x \<in> X) a\<^sub>2 = xs'
filter (\<lambda>x. x \<in> ?X) (?l1.0 @ ?l2.0) = filter (\<lambda>x. x \<in> ?X) ?l1.0 @ filter (\<lambda>x. x \<in> ?X) ?l2.0

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> X) (t\<^sub>1 @ [x'] @ t\<^sub>2') = filter (\<lambda>x. x \<in> X) \<alpha>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(t\<^sub>1 @ [x'] @ t\<^sub>2') \<upharpoonleft> X = \<alpha> \<upharpoonleft> X

goal (1 subgoal):
 1. \<And>n \<tau> \<alpha>. \<lbrakk>\<And>\<tau> \<alpha>. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X; \<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; Suc n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<tau> = (t\<^sub>1 @ [x'] @ t\<^sub>2') @ [x] @ t\<^sub>3'
(t\<^sub>1 @ [x'] @ t\<^sub>2') \<upharpoonleft> X = \<alpha> \<upharpoonleft> X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<tau> = (t\<^sub>1 @ [x'] @ t\<^sub>2') @ [x] @ t\<^sub>3'
(t\<^sub>1 @ [x'] @ t\<^sub>2') \<upharpoonleft> X = \<alpha> \<upharpoonleft> X

goal (1 subgoal):
 1. \<exists>\<alpha>'' \<beta>'. \<tau> = \<alpha>'' @ [x] @ \<beta>' \<and> \<alpha>'' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
using \<open>t\<^sub>3'\<upharpoonleft>X = \<beta>\<upharpoonleft>X\<close>
[PROOF STATE]
proof (prove)
using this:
\<tau> = (t\<^sub>1 @ [x'] @ t\<^sub>2') @ [x] @ t\<^sub>3'
(t\<^sub>1 @ [x'] @ t\<^sub>2') \<upharpoonleft> X = \<alpha> \<upharpoonleft> X
t\<^sub>3' \<upharpoonleft> X = \<beta> \<upharpoonleft> X

goal (1 subgoal):
 1. \<exists>\<alpha>'' \<beta>'. \<tau> = \<alpha>'' @ [x] @ \<beta>' \<and> \<alpha>'' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>'' \<beta>'. \<tau> = \<alpha>'' @ [x] @ \<beta>' \<and> \<alpha>'' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; n = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X

goal (1 subgoal):
 1. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; ?n2 = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X

goal (1 subgoal):
 1. \<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
with \<open>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X\<close> \<open> x \<in> X\<close>
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
x \<in> X
\<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; ?n2 = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X
x \<in> X
\<lbrakk>\<tau> \<upharpoonleft> X = (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X; x \<in> X; ?n2 = length (\<alpha> \<upharpoonleft> X)\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X

goal (1 subgoal):
 1. \<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>' \<beta>'. \<tau> = \<alpha>' @ [x] @ \<beta>' \<and> \<alpha>' \<upharpoonleft> X = \<alpha> \<upharpoonleft> X \<and> \<beta>' \<upharpoonleft> X = \<beta> \<upharpoonleft> X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma projection_on_intersection: "l \<upharpoonleft> X = [] \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = []"
(is "?L1 = [] \<Longrightarrow> ?L2 = []")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> X = [] \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<upharpoonleft> X = [] \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = []
[PROOF STEP]
assume "?L1 = []"
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X = []

goal (1 subgoal):
 1. l \<upharpoonleft> X = [] \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = []
[PROOF STEP]
hence "set ?L1 = {}"
[PROOF STATE]
proof (prove)
using this:
l \<upharpoonleft> X = []

goal (1 subgoal):
 1. set (l \<upharpoonleft> X) = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (l \<upharpoonleft> X) = {}

goal (1 subgoal):
 1. l \<upharpoonleft> X = [] \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (l \<upharpoonleft> X) = {}

goal (1 subgoal):
 1. l \<upharpoonleft> X = [] \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = []
[PROOF STEP]
have "set ?L2 \<subseteq> set ?L1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (l \<upharpoonleft> (X \<inter> Y)) \<subseteq> set (l \<upharpoonleft> X)
[PROOF STEP]
by (simp add: projection_def, auto)
[PROOF STATE]
proof (state)
this:
set (l \<upharpoonleft> (X \<inter> Y)) \<subseteq> set (l \<upharpoonleft> X)

goal (1 subgoal):
 1. l \<upharpoonleft> X = [] \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (l \<upharpoonleft> X) = {}
set (l \<upharpoonleft> (X \<inter> Y)) \<subseteq> set (l \<upharpoonleft> X)
[PROOF STEP]
have "set ?L2 = {}"
[PROOF STATE]
proof (prove)
using this:
set (l \<upharpoonleft> X) = {}
set (l \<upharpoonleft> (X \<inter> Y)) \<subseteq> set (l \<upharpoonleft> X)

goal (1 subgoal):
 1. set (l \<upharpoonleft> (X \<inter> Y)) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (l \<upharpoonleft> (X \<inter> Y)) = {}

goal (1 subgoal):
 1. l \<upharpoonleft> X = [] \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = []
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (l \<upharpoonleft> (X \<inter> Y)) = {}

goal (1 subgoal):
 1. l \<upharpoonleft> (X \<inter> Y) = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> (X \<inter> Y) = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma projection_on_subset: "\<lbrakk> Y \<subseteq> X; l \<upharpoonleft> X = [] \<rbrakk> \<Longrightarrow> l \<upharpoonleft> Y = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Y \<subseteq> X; l \<upharpoonleft> X = []\<rbrakk> \<Longrightarrow> l \<upharpoonleft> Y = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Y \<subseteq> X; l \<upharpoonleft> X = []\<rbrakk> \<Longrightarrow> l \<upharpoonleft> Y = []
[PROOF STEP]
assume subset: "Y \<subseteq> X"
[PROOF STATE]
proof (state)
this:
Y \<subseteq> X

goal (1 subgoal):
 1. \<lbrakk>Y \<subseteq> X; l \<upharpoonleft> X = []\<rbrakk> \<Longrightarrow> l \<upharpoonleft> Y = []
[PROOF STEP]
assume proj_empty: "l \<upharpoonleft> X = []"
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X = []

goal (1 subgoal):
 1. \<lbrakk>Y \<subseteq> X; l \<upharpoonleft> X = []\<rbrakk> \<Longrightarrow> l \<upharpoonleft> Y = []
[PROOF STEP]
hence "l \<upharpoonleft> (X \<inter> Y) = []"
[PROOF STATE]
proof (prove)
using this:
l \<upharpoonleft> X = []

goal (1 subgoal):
 1. l \<upharpoonleft> (X \<inter> Y) = []
[PROOF STEP]
by (rule projection_on_intersection)
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> (X \<inter> Y) = []

goal (1 subgoal):
 1. \<lbrakk>Y \<subseteq> X; l \<upharpoonleft> X = []\<rbrakk> \<Longrightarrow> l \<upharpoonleft> Y = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> (X \<inter> Y) = []

goal (1 subgoal):
 1. \<lbrakk>Y \<subseteq> X; l \<upharpoonleft> X = []\<rbrakk> \<Longrightarrow> l \<upharpoonleft> Y = []
[PROOF STEP]
from subset
[PROOF STATE]
proof (chain)
picking this:
Y \<subseteq> X
[PROOF STEP]
have "X \<inter> Y = Y"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> X

goal (1 subgoal):
 1. X \<inter> Y = Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<inter> Y = Y

goal (1 subgoal):
 1. \<lbrakk>Y \<subseteq> X; l \<upharpoonleft> X = []\<rbrakk> \<Longrightarrow> l \<upharpoonleft> Y = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l \<upharpoonleft> (X \<inter> Y) = []
X \<inter> Y = Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l \<upharpoonleft> (X \<inter> Y) = []
X \<inter> Y = Y

goal (1 subgoal):
 1. l \<upharpoonleft> Y = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> Y = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma projection_on_subset2: "\<lbrakk> set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X' \<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
assume setl_subset_L: "set l \<subseteq> L"
[PROOF STATE]
proof (state)
this:
set l \<subseteq> L

goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
assume l_no_X': "l \<upharpoonleft> X' = []"
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X' = []

goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
assume X_inter_L_subset_X': "X \<inter> L \<subseteq> X'"
[PROOF STATE]
proof (state)
this:
X \<inter> L \<subseteq> X'

goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
from X_inter_L_subset_X' l_no_X'
[PROOF STATE]
proof (chain)
picking this:
X \<inter> L \<subseteq> X'
l \<upharpoonleft> X' = []
[PROOF STEP]
have "l \<upharpoonleft> (X \<inter> L) = []"
[PROOF STATE]
proof (prove)
using this:
X \<inter> L \<subseteq> X'
l \<upharpoonleft> X' = []

goal (1 subgoal):
 1. l \<upharpoonleft> (X \<inter> L) = []
[PROOF STEP]
by (rule projection_on_subset)
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> (X \<inter> L) = []

goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> (X \<inter> L) = []

goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
have "l \<upharpoonleft> (X \<inter> L) = (l \<upharpoonleft> L) \<upharpoonleft> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> (X \<inter> L) = l \<upharpoonleft> L \<upharpoonleft> X
[PROOF STEP]
by (simp add: Int_commute projection_def)
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> (X \<inter> L) = l \<upharpoonleft> L \<upharpoonleft> X

goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> (X \<inter> L) = l \<upharpoonleft> L \<upharpoonleft> X

goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
note setl_subset_L
[PROOF STATE]
proof (state)
this:
set l \<subseteq> L

goal (1 subgoal):
 1. \<lbrakk>set l \<subseteq> L; l \<upharpoonleft> X' = []; X \<inter> L \<subseteq> X'\<rbrakk> \<Longrightarrow> l \<upharpoonleft> X = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l \<upharpoonleft> (X \<inter> L) = []
l \<upharpoonleft> (X \<inter> L) = l \<upharpoonleft> L \<upharpoonleft> X
set l \<subseteq> L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l \<upharpoonleft> (X \<inter> L) = []
l \<upharpoonleft> (X \<inter> L) = l \<upharpoonleft> L \<upharpoonleft> X
set l \<subseteq> L

goal (1 subgoal):
 1. l \<upharpoonleft> X = []
[PROOF STEP]
by (simp add: list_subset_iff_projection_neutral)
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma non_empty_projection_on_subset: "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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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
[PROOF STEP]
by (metis projection_subset_eq_from_superset_eq subset_Un_eq)


[STATEMENT]
lemma projection_intersection_neutral: "(set l \<subseteq> X) \<Longrightarrow> (l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y
[PROOF STEP]
assume "set l \<subseteq> X"
[PROOF STATE]
proof (state)
this:
set l \<subseteq> X

goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y
[PROOF STEP]
hence "(l \<upharpoonleft> X) = l"
[PROOF STATE]
proof (prove)
using this:
set l \<subseteq> X

goal (1 subgoal):
 1. l \<upharpoonleft> X = l
[PROOF STEP]
by (simp add: list_subset_iff_projection_neutral)
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X = l

goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y
[PROOF STEP]
hence "(l \<upharpoonleft> X) \<upharpoonleft> Y = l \<upharpoonleft> Y"
[PROOF STATE]
proof (prove)
using this:
l \<upharpoonleft> X = l

goal (1 subgoal):
 1. l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> Y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> Y

goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> Y

goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y
[PROOF STEP]
have "(l \<upharpoonleft> X) \<upharpoonleft> Y = l \<upharpoonleft> (X \<inter> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> (X \<inter> Y)
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> (X \<inter> Y)

goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> Y
l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> (X \<inter> Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> Y
l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> (X \<inter> Y)

goal (1 subgoal):
 1. l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> (X \<inter> Y) = l \<upharpoonleft> Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma projection_commute:
  "(l \<upharpoonleft> X) \<upharpoonleft> Y = (l \<upharpoonleft> Y) \<upharpoonleft> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> Y \<upharpoonleft> X
[PROOF STEP]
by (simp add: projection_def conj_commute)


[STATEMENT]
lemma projection_subset_elim: "Y \<subseteq> X \<Longrightarrow> (l \<upharpoonleft> X) \<upharpoonleft> Y = l \<upharpoonleft> Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<subseteq> X \<Longrightarrow> l \<upharpoonleft> X \<upharpoonleft> Y = l \<upharpoonleft> Y
[PROOF STEP]
by (simp only: projection_def, metis Diff_subset list_subset_iff_projection_neutral
    minus_coset_filter order_trans projection_commute projection_def)


[STATEMENT]
lemma projection_sequence: "(xs \<upharpoonleft> X) \<upharpoonleft> Y = (xs \<upharpoonleft> (X \<inter> Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<upharpoonleft> X \<upharpoonleft> Y = xs \<upharpoonleft> (X \<inter> Y)
[PROOF STEP]
by (metis Int_absorb inf_sup_ord(1) list_subset_iff_projection_neutral
    projection_intersection_neutral projection_subset_elim)