[STATEMENT]
lemma list_split_two_elems:
  assumes "distinct xs"
    and "x \<in> set xs" and "y \<in> set xs"
    and "x \<noteq> y"
  shows "\<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
obtain as bs where as_bs: "xs = as @ [x] @ bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as bs. xs = as @ [x] @ bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2) split_list_first
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>as bs. xs = as @ [x] @ bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xs = as @ [x] @ bs

goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
proof(cases "y \<in> set as")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
 2. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in> set as

goal (2 subgoals):
 1. y \<in> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
 2. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set as
[PROOF STEP]
obtain cs ds where "as = cs @ [y] @ ds"
[PROOF STATE]
proof (prove)
using this:
y \<in> set as

goal (1 subgoal):
 1. (\<And>cs ds. as = cs @ [y] @ ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(3) split_list_first
[PROOF STATE]
proof (prove)
using this:
y \<in> set as
y \<in> set xs
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>cs ds. as = cs @ [y] @ ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
as = cs @ [y] @ ds

goal (2 subgoals):
 1. y \<in> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
 2. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as = cs @ [y] @ ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = cs @ [y] @ ds

goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
by (auto simp add: as_bs)
[PROOF STATE]
proof (state)
this:
\<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf

goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<notin> set as

goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<notin> set as
[PROOF STEP]
have "y \<in> set bs"
[PROOF STATE]
proof (prove)
using this:
y \<notin> set as

goal (1 subgoal):
 1. y \<in> set bs
[PROOF STEP]
using as_bs assms(3) assms(4)
[PROOF STATE]
proof (prove)
using this:
y \<notin> set as
xs = as @ [x] @ bs
y \<in> set xs
x \<noteq> y

goal (1 subgoal):
 1. y \<in> set bs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> set bs

goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set bs
[PROOF STEP]
obtain cs ds where "bs = cs @ [y] @ ds"
[PROOF STATE]
proof (prove)
using this:
y \<in> set bs

goal (1 subgoal):
 1. (\<And>cs ds. bs = cs @ [y] @ ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(3) split_list_first
[PROOF STATE]
proof (prove)
using this:
y \<in> set bs
y \<in> set xs
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>cs ds. bs = cs @ [y] @ ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bs = cs @ [y] @ ds

goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bs = cs @ [y] @ ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bs = cs @ [y] @ ds

goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
by (auto simp add: as_bs)
[PROOF STATE]
proof (state)
this:
\<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf

goal:
No subgoals!
[PROOF STEP]
qed