[STATEMENT]
lemma remove_cycles_self:
  "x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
assume x:"x \<in> set xs"
[PROOF STATE]
proof (state)
this:
x \<in> set xs

goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set xs
[PROOF STEP]
obtain ws where ws: "remove_cycles xs x ys = x # ws" "x \<notin> set ws"
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs

goal (1 subgoal):
 1. (\<And>ws. \<lbrakk>remove_cycles xs x ys = x # ws; x \<notin> set ws\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using remove_cycles_begins_with[OF x, of ys]
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs
\<exists>zs. remove_cycles xs x ys = x # zs \<and> x \<notin> set zs

goal (1 subgoal):
 1. (\<And>ws. \<lbrakk>remove_cycles xs x ys = x # ws; x \<notin> set ws\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
remove_cycles xs x ys = x # ws
x \<notin> set ws

goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
from remove_cycles_id[OF this(2)]
[PROOF STATE]
proof (chain)
picking this:
remove_cycles ws x ?ys = rev ?ys @ ws
[PROOF STEP]
have "remove_cycles ws x [x] = x # ws"
[PROOF STATE]
proof (prove)
using this:
remove_cycles ws x ?ys = rev ?ys @ ws

goal (1 subgoal):
 1. remove_cycles ws x [x] = x # ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
remove_cycles ws x [x] = x # ws

goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
with ws(1)
[PROOF STATE]
proof (chain)
picking this:
remove_cycles xs x ys = x # ws
remove_cycles ws x [x] = x # ws
[PROOF STEP]
show "remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys"
[PROOF STATE]
proof (prove)
using this:
remove_cycles xs x ys = x # ws
remove_cycles ws x [x] = x # ws

goal (1 subgoal):
 1. remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys

goal:
No subgoals!
[PROOF STEP]
qed