[STATEMENT]
lemma is_minimal_basis_trd_distinct:
  assumes min: "is_minimal_basis (set (x # xs))" and dist: "distinct (x # xs)"
  shows "distinct ((trd xs x) # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
let ?y = "trd xs x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
from min
[PROOF STATE]
proof (chain)
picking this:
is_minimal_basis (set (x # xs))
[PROOF STEP]
have lty: "lt ?y = lt x"
[PROOF STATE]
proof (prove)
using this:
is_minimal_basis (set (x # xs))

goal (1 subgoal):
 1. lt (trd xs x) = lt x
[PROOF STEP]
proof (rule minimal_basis_red_rtrancl_lt, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
from dist
[PROOF STATE]
proof (chain)
picking this:
distinct (x # xs)
[PROOF STEP]
have "x \<notin> set xs"
[PROOF STATE]
proof (prove)
using this:
distinct (x # xs)

goal (1 subgoal):
 1. x \<notin> set xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<notin> set xs

goal (1 subgoal):
 1. (red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
hence eq: "set (x # xs) - {x} = set xs"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set xs

goal (1 subgoal):
 1. set (x # xs) - {x} = set xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (x # xs) - {x} = set xs

goal (1 subgoal):
 1. (red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
show "(red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
unfolding eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (red (set xs))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
by (rule trd_red_rtrancl)
[PROOF STATE]
proof (state)
this:
(red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lt (trd xs x) = lt x

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
have "?y \<notin> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trd xs x \<notin> set xs
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trd xs x \<in> set xs \<Longrightarrow> False
[PROOF STEP]
assume "?y \<in> set xs"
[PROOF STATE]
proof (state)
this:
trd xs x \<in> set xs

goal (1 subgoal):
 1. trd xs x \<in> set xs \<Longrightarrow> False
[PROOF STEP]
hence "?y \<in> set (x # xs)"
[PROOF STATE]
proof (prove)
using this:
trd xs x \<in> set xs

goal (1 subgoal):
 1. trd xs x \<in> set (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
trd xs x \<in> set (x # xs)

goal (1 subgoal):
 1. trd xs x \<in> set xs \<Longrightarrow> False
[PROOF STEP]
with min
[PROOF STATE]
proof (chain)
picking this:
is_minimal_basis (set (x # xs))
trd xs x \<in> set (x # xs)
[PROOF STEP]
have "\<not> lt ?y adds\<^sub>t lt x"
[PROOF STATE]
proof (prove)
using this:
is_minimal_basis (set (x # xs))
trd xs x \<in> set (x # xs)

goal (1 subgoal):
 1. \<not> lt (trd xs x) adds\<^sub>t lt x
[PROOF STEP]
proof (rule is_minimal_basisD2, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trd xs x \<noteq> x
[PROOF STEP]
show "?y \<noteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trd xs x \<noteq> x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trd xs x = x \<Longrightarrow> False
[PROOF STEP]
assume "?y = x"
[PROOF STATE]
proof (state)
this:
trd xs x = x

goal (1 subgoal):
 1. trd xs x = x \<Longrightarrow> False
[PROOF STEP]
from dist
[PROOF STATE]
proof (chain)
picking this:
distinct (x # xs)
[PROOF STEP]
have "x \<notin> set xs"
[PROOF STATE]
proof (prove)
using this:
distinct (x # xs)

goal (1 subgoal):
 1. x \<notin> set xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<notin> set xs

goal (1 subgoal):
 1. trd xs x = x \<Longrightarrow> False
[PROOF STEP]
with \<open>?y \<in> set xs\<close>
[PROOF STATE]
proof (chain)
picking this:
trd xs x \<in> set xs
x \<notin> set xs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trd xs x \<in> set xs
x \<notin> set xs

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding \<open>?y = x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs
x \<notin> set xs

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trd xs x \<noteq> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> lt (trd xs x) adds\<^sub>t lt x

goal (1 subgoal):
 1. trd xs x \<in> set xs \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
\<not> lt (trd xs x) adds\<^sub>t lt x

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding lty
[PROOF STATE]
proof (prove)
using this:
\<not> lt x adds\<^sub>t lt x

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: adds_term_refl)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trd xs x \<notin> set xs

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trd xs x \<notin> set xs

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
from dist
[PROOF STATE]
proof (chain)
picking this:
distinct (x # xs)
[PROOF STEP]
have "distinct xs"
[PROOF STATE]
proof (prove)
using this:
distinct (x # xs)

goal (1 subgoal):
 1. distinct xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct xs

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trd xs x \<notin> set xs
distinct xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trd xs x \<notin> set xs
distinct xs

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (trd xs x # xs)

goal:
No subgoals!
[PROOF STEP]
qed