[STATEMENT]
lemma Macaulay_red_reducible:
  assumes "f \<in> phull (set fs)" and "F \<subseteq> set fs" and "lt_set F = lt_set (set fs)"
  shows "(lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
define A where "A = F \<union> set (Macaulay_red (Keys_to_list fs) fs)"
[PROOF STATE]
proof (state)
this:
A = F \<union> set (Macaulay_red (Keys_to_list fs) fs)

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
have phull_A: "phull A \<subseteq> phull (set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phull A \<subseteq> phull (set fs)
[PROOF STEP]
proof (rule phull.span_subset_spanI, simp add: A_def, rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. F \<subseteq> phull (set fs)
 2. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
have "F \<subseteq> phull F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<subseteq> phull F
[PROOF STEP]
by (rule phull.span_superset)
[PROOF STATE]
proof (state)
this:
F \<subseteq> phull F

goal (2 subgoals):
 1. F \<subseteq> phull (set fs)
 2. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
F \<subseteq> phull F

goal (2 subgoals):
 1. F \<subseteq> phull (set fs)
 2. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
F \<subseteq> set fs
[PROOF STEP]
have "... \<subseteq> phull (set fs)"
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> set fs

goal (1 subgoal):
 1. phull F \<subseteq> phull (set fs)
[PROOF STEP]
by (rule phull.span_mono)
[PROOF STATE]
proof (state)
this:
phull F \<subseteq> phull (set fs)

goal (2 subgoals):
 1. F \<subseteq> phull (set fs)
 2. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
F \<subseteq> phull (set fs)
[PROOF STEP]
show "F \<subseteq> phull (set fs)"
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> phull (set fs)

goal (1 subgoal):
 1. F \<subseteq> phull (set fs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
F \<subseteq> phull (set fs)

goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
have "set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> set (Macaulay_list fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> set (Macaulay_list fs)
[PROOF STEP]
by (auto simp add: set_Macaulay_red)
[PROOF STATE]
proof (state)
this:
set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> set (Macaulay_list fs)

goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> set (Macaulay_list fs)

goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
have "... \<subseteq> phull (set (Macaulay_list fs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Macaulay_list fs) \<subseteq> phull (set (Macaulay_list fs))
[PROOF STEP]
by (rule phull.span_superset)
[PROOF STATE]
proof (state)
this:
set (Macaulay_list fs) \<subseteq> phull (set (Macaulay_list fs))

goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (Macaulay_list fs) \<subseteq> phull (set (Macaulay_list fs))

goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
have "... = phull (set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phull (set (Macaulay_list fs)) = phull (set fs)
[PROOF STEP]
by (rule phull_Macaulay_list)
[PROOF STATE]
proof (state)
this:
phull (set (Macaulay_list fs)) = phull (set fs)

goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
show "set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)"
[PROOF STATE]
proof (prove)
using this:
set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)

goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (Macaulay_red (Keys_to_list fs) fs) \<subseteq> phull (set fs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
phull A \<subseteq> phull (set fs)

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
have lt_A: "p \<in> phull (set fs) \<Longrightarrow> p \<noteq> 0 \<Longrightarrow> (\<And>g. g \<in> A \<Longrightarrow> g \<noteq> 0 \<Longrightarrow> lt g = lt p \<Longrightarrow> thesis) \<Longrightarrow> thesis"
    for p thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> phull (set fs); p \<noteq> 0; \<And>g. \<lbrakk>g \<in> A; g \<noteq> 0; lt g = lt p\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>p \<in> phull (set fs); p \<noteq> 0; \<And>g. \<lbrakk>g \<in> A; g \<noteq> 0; lt g = lt p\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "p \<in> phull (set fs)" and "p \<noteq> 0"
[PROOF STATE]
proof (state)
this:
p \<in> phull (set fs)
p \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>p \<in> phull (set fs); p \<noteq> 0; \<And>g. \<lbrakk>g \<in> A; g \<noteq> 0; lt g = lt p\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> phull (set fs)
p \<noteq> 0
[PROOF STEP]
obtain g where g_in: "g \<in> set (Macaulay_list fs)" and "g \<noteq> 0" and "lt p = lt g"
[PROOF STATE]
proof (prove)
using this:
p \<in> phull (set fs)
p \<noteq> 0

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> set (Macaulay_list fs); g \<noteq> 0; lt p = lt g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Macaulay_list_lt)
[PROOF STATE]
proof (state)
this:
g \<in> set (Macaulay_list fs)
g \<noteq> 0
lt p = lt g

goal (1 subgoal):
 1. \<lbrakk>p \<in> phull (set fs); p \<noteq> 0; \<And>g. \<lbrakk>g \<in> A; g \<noteq> 0; lt g = lt p\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume *: "\<And>g. g \<in> A \<Longrightarrow> g \<noteq> 0 \<Longrightarrow> lt g = lt p \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<lbrakk>?g101 \<in> A; ?g101 \<noteq> 0; lt ?g101 = lt p\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<lbrakk>p \<in> phull (set fs); p \<noteq> 0; \<And>g. \<lbrakk>g \<in> A; g \<noteq> 0; lt g = lt p\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases "g \<in> set (Macaulay_red (Keys_to_list fs) fs)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g \<in> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
 2. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
g \<in> set (Macaulay_red (Keys_to_list fs) fs)

goal (2 subgoals):
 1. g \<in> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
 2. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
hence "g \<in> A"
[PROOF STATE]
proof (prove)
using this:
g \<in> set (Macaulay_red (Keys_to_list fs) fs)

goal (1 subgoal):
 1. g \<in> A
[PROOF STEP]
by (simp add: A_def)
[PROOF STATE]
proof (state)
this:
g \<in> A

goal (2 subgoals):
 1. g \<in> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
 2. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
from this \<open>g \<noteq> 0\<close> \<open>lt p = lt g\<close>[symmetric]
[PROOF STATE]
proof (chain)
picking this:
g \<in> A
g \<noteq> 0
lt g = lt p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g \<in> A
g \<noteq> 0
lt g = lt p

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule *)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
g \<notin> set (Macaulay_red (Keys_to_list fs) fs)

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
with g_in
[PROOF STATE]
proof (chain)
picking this:
g \<in> set (Macaulay_list fs)
g \<notin> set (Macaulay_red (Keys_to_list fs) fs)
[PROOF STEP]
have "lt g \<in> lt_set (set fs)"
[PROOF STATE]
proof (prove)
using this:
g \<in> set (Macaulay_list fs)
g \<notin> set (Macaulay_red (Keys_to_list fs) fs)

goal (1 subgoal):
 1. lt g \<in> lt_set (set fs)
[PROOF STEP]
by (simp add: set_Macaulay_red)
[PROOF STATE]
proof (state)
this:
lt g \<in> lt_set (set fs)

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lt g \<in> lt_set (set fs)

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
have "... = lt_set F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt_set (set fs) = lt_set F
[PROOF STEP]
by (simp only: assms(3))
[PROOF STATE]
proof (state)
this:
lt_set (set fs) = lt_set F

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lt g \<in> lt_set F
[PROOF STEP]
obtain g' where "g' \<in> F" and "g' \<noteq> 0" and "lt g' = lt g"
[PROOF STATE]
proof (prove)
using this:
lt g \<in> lt_set F

goal (1 subgoal):
 1. (\<And>g'. \<lbrakk>g' \<in> F; g' \<noteq> 0; lt g' = lt g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule lt_setE)
[PROOF STATE]
proof (state)
this:
g' \<in> F
g' \<noteq> 0
lt g' = lt g

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
g' \<in> F
[PROOF STEP]
have "g' \<in> A"
[PROOF STATE]
proof (prove)
using this:
g' \<in> F

goal (1 subgoal):
 1. g' \<in> A
[PROOF STEP]
by (simp add: A_def)
[PROOF STATE]
proof (state)
this:
g' \<in> A

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g' \<in> A

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
note \<open>g' \<noteq> 0\<close>
[PROOF STATE]
proof (state)
this:
g' \<noteq> 0

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g' \<noteq> 0

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
have "lt g' = lt p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt g' = lt p
[PROOF STEP]
by (simp only: \<open>lt p = lt g\<close> \<open>lt g' = lt g\<close>)
[PROOF STATE]
proof (state)
this:
lt g' = lt p

goal (1 subgoal):
 1. g \<notin> set (Macaulay_red (Keys_to_list fs) fs) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g' \<in> A
g' \<noteq> 0
lt g' = lt p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g' \<in> A
g' \<noteq> 0
lt g' = lt p

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule *)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p101 \<in> phull (set fs); ?p101 \<noteq> 0; \<And>g. \<lbrakk>g \<in> A; g \<noteq> 0; lt g = lt ?p101\<rbrakk> \<Longrightarrow> ?thesis101\<rbrakk> \<Longrightarrow> ?thesis101

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
from assms(2) finite_set
[PROOF STATE]
proof (chain)
picking this:
F \<subseteq> set fs
finite (set ?xs)
[PROOF STEP]
have "finite F"
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> set fs
finite (set ?xs)

goal (1 subgoal):
 1. finite F
[PROOF STEP]
by (rule finite_subset)
[PROOF STATE]
proof (state)
this:
finite F

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
from this finite_set
[PROOF STATE]
proof (chain)
picking this:
finite F
finite (set ?xs)
[PROOF STEP]
have fin_A: "finite A"
[PROOF STATE]
proof (prove)
using this:
finite F
finite (set ?xs)

goal (1 subgoal):
 1. finite A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
finite F
finite (set ?xs)

goal (1 subgoal):
 1. finite (F \<union> set (Macaulay_red (Keys_to_list fs) fs))
[PROOF STEP]
by (rule finite_UnI)
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
from ex_dgrad
[PROOF STATE]
proof (chain)
picking this:
\<exists>d. dickson_grading d
[PROOF STEP]
obtain d::"'a \<Rightarrow> nat" where dg: "dickson_grading d"
[PROOF STATE]
proof (prove)
using this:
\<exists>d. dickson_grading d

goal (1 subgoal):
 1. (\<And>d. dickson_grading d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
dickson_grading d

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
from fin_A
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "finite (insert f A)"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. finite (insert f A)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
finite (insert f A)

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (insert f A)
[PROOF STEP]
obtain m where "insert f A \<subseteq> dgrad_p_set d m"
[PROOF STATE]
proof (prove)
using this:
finite (insert f A)

goal (1 subgoal):
 1. (\<And>m. insert f A \<subseteq> dgrad_p_set d m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule dgrad_p_set_exhaust)
[PROOF STATE]
proof (state)
this:
insert f A \<subseteq> dgrad_p_set d m

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
hence A_sub: "A \<subseteq> dgrad_p_set d m" and "f \<in> dgrad_p_set d m"
[PROOF STATE]
proof (prove)
using this:
insert f A \<subseteq> dgrad_p_set d m

goal (1 subgoal):
 1. A \<subseteq> dgrad_p_set d m &&& f \<in> dgrad_p_set d m
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
A \<subseteq> dgrad_p_set d m
f \<in> dgrad_p_set d m

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
from dg
[PROOF STATE]
proof (chain)
picking this:
dickson_grading d
[PROOF STEP]
have "wfP (dickson_less_p d m)"
[PROOF STATE]
proof (prove)
using this:
dickson_grading d

goal (1 subgoal):
 1. wfP (dickson_less_p d m)
[PROOF STEP]
by (rule wf_dickson_less_p)
[PROOF STATE]
proof (state)
this:
wfP (dickson_less_p d m)

goal (1 subgoal):
 1. (lin_red (F \<union> set (Macaulay_red (Keys_to_list fs) fs)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
from this assms(1) \<open>f \<in> dgrad_p_set d m\<close>
[PROOF STATE]
proof (chain)
picking this:
wfP (dickson_less_p d m)
f \<in> phull (set fs)
f \<in> dgrad_p_set d m
[PROOF STEP]
show "(lin_red A)\<^sup>*\<^sup>* f 0"
[PROOF STATE]
proof (prove)
using this:
wfP (dickson_less_p d m)
f \<in> phull (set fs)
f \<in> dgrad_p_set d m

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* f 0
[PROOF STEP]
proof (induct f)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>dickson_less_p d m y x; y \<in> phull (set fs); y \<in> dgrad_p_set d m\<rbrakk> \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* y 0; x \<in> phull (set fs); x \<in> dgrad_p_set d m\<rbrakk> \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* x 0
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>dickson_less_p d m y x; y \<in> phull (set fs); y \<in> dgrad_p_set d m\<rbrakk> \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* y 0; x \<in> phull (set fs); x \<in> dgrad_p_set d m\<rbrakk> \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* x 0
[PROOF STEP]
assume IH: "\<And>q. dickson_less_p d m q p \<Longrightarrow> q \<in> phull (set fs) \<Longrightarrow> q \<in> dgrad_p_set d m \<Longrightarrow>
                    (lin_red A)\<^sup>*\<^sup>* q 0"
      and "p \<in> phull (set fs)" and "p \<in> dgrad_p_set d m"
[PROOF STATE]
proof (state)
this:
\<lbrakk>dickson_less_p d m ?q102 p; ?q102 \<in> phull (set fs); ?q102 \<in> dgrad_p_set d m\<rbrakk> \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* ?q102 0
p \<in> phull (set fs)
p \<in> dgrad_p_set d m

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>dickson_less_p d m y x; y \<in> phull (set fs); y \<in> dgrad_p_set d m\<rbrakk> \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* y 0; x \<in> phull (set fs); x \<in> dgrad_p_set d m\<rbrakk> \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* x 0
[PROOF STEP]
show "(lin_red A)\<^sup>*\<^sup>* p 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
proof (cases "p = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
 2. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p = 0

goal (2 subgoals):
 1. p = 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
 2. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = 0

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(lin_red A)\<^sup>*\<^sup>* p 0

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
with \<open>p \<in> phull (set fs)\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<in> phull (set fs)
p \<noteq> 0
[PROOF STEP]
obtain g where "g \<in> A" and "g \<noteq> 0" and "lt g = lt p"
[PROOF STATE]
proof (prove)
using this:
p \<in> phull (set fs)
p \<noteq> 0

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> A; g \<noteq> 0; lt g = lt p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule lt_A)
[PROOF STATE]
proof (state)
this:
g \<in> A
g \<noteq> 0
lt g = lt p

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
define q where "q = p - monom_mult (lc p / lc g) 0 g"
[PROOF STATE]
proof (state)
this:
q = p - monom_mult (lc p / lc g) (0::'a) g

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
from \<open>g \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<in> A
[PROOF STEP]
have lr: "lin_red A p q"
[PROOF STATE]
proof (prove)
using this:
g \<in> A

goal (1 subgoal):
 1. lin_red A p q
[PROOF STEP]
proof (rule lin_redI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red_single p q g (0::'a)
[PROOF STEP]
show "red_single p q g 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red_single p q g (0::'a)
[PROOF STEP]
by (simp add: red_single_def \<open>lt g = lt p\<close> lc_def[symmetric] q_def \<open>g \<noteq> 0\<close> lc_not_0[OF False] term_simps)
[PROOF STATE]
proof (state)
this:
red_single p q g (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lin_red A p q

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lin_red A p q

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
have "(lin_red A)\<^sup>*\<^sup>* q 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
from lr
[PROOF STATE]
proof (chain)
picking this:
lin_red A p q
[PROOF STEP]
have red: "red A p q"
[PROOF STATE]
proof (prove)
using this:
lin_red A p q

goal (1 subgoal):
 1. red A p q
[PROOF STEP]
by (rule lin_red_imp_red)
[PROOF STATE]
proof (state)
this:
red A p q

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
with dg A_sub \<open>p \<in> dgrad_p_set d m\<close>
[PROOF STATE]
proof (chain)
picking this:
dickson_grading d
A \<subseteq> dgrad_p_set d m
p \<in> dgrad_p_set d m
red A p q
[PROOF STEP]
have "q \<in> dgrad_p_set d m"
[PROOF STATE]
proof (prove)
using this:
dickson_grading d
A \<subseteq> dgrad_p_set d m
p \<in> dgrad_p_set d m
red A p q

goal (1 subgoal):
 1. q \<in> dgrad_p_set d m
[PROOF STEP]
by (rule dgrad_p_set_closed_red)
[PROOF STATE]
proof (state)
this:
q \<in> dgrad_p_set d m

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
q \<in> dgrad_p_set d m

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
from red
[PROOF STATE]
proof (chain)
picking this:
red A p q
[PROOF STEP]
have "q \<prec>\<^sub>p p"
[PROOF STATE]
proof (prove)
using this:
red A p q

goal (1 subgoal):
 1. q \<prec>\<^sub>p p
[PROOF STEP]
by (rule red_ord)
[PROOF STATE]
proof (state)
this:
q \<prec>\<^sub>p p

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
q \<in> dgrad_p_set d m
q \<prec>\<^sub>p p
[PROOF STEP]
have "dickson_less_p d m q p"
[PROOF STATE]
proof (prove)
using this:
q \<in> dgrad_p_set d m
q \<prec>\<^sub>p p

goal (1 subgoal):
 1. dickson_less_p d m q p
[PROOF STEP]
using \<open>p \<in> dgrad_p_set d m\<close>
[PROOF STATE]
proof (prove)
using this:
q \<in> dgrad_p_set d m
q \<prec>\<^sub>p p
p \<in> dgrad_p_set d m

goal (1 subgoal):
 1. dickson_less_p d m q p
[PROOF STEP]
by (simp add: dickson_less_p_def)
[PROOF STATE]
proof (state)
this:
dickson_less_p d m q p

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dickson_less_p d m q p

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
from phull_A \<open>p \<in> phull (set fs)\<close> lr
[PROOF STATE]
proof (chain)
picking this:
phull A \<subseteq> phull (set fs)
p \<in> phull (set fs)
lin_red A p q
[PROOF STEP]
have "q \<in> phull (set fs)"
[PROOF STATE]
proof (prove)
using this:
phull A \<subseteq> phull (set fs)
p \<in> phull (set fs)
lin_red A p q

goal (1 subgoal):
 1. q \<in> phull (set fs)
[PROOF STEP]
by (rule phull_closed_lin_red)
[PROOF STATE]
proof (state)
this:
q \<in> phull (set fs)

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dickson_less_p d m q p
q \<in> phull (set fs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dickson_less_p d m q p
q \<in> phull (set fs)

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
using \<open>q \<in> dgrad_p_set d m\<close>
[PROOF STATE]
proof (prove)
using this:
dickson_less_p d m q p
q \<in> phull (set fs)
q \<in> dgrad_p_set d m

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
by (rule IH)
[PROOF STATE]
proof (state)
this:
(lin_red A)\<^sup>*\<^sup>* q 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(lin_red A)\<^sup>*\<^sup>* q 0

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lin_red A p q
(lin_red A)\<^sup>*\<^sup>* q 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lin_red A p q
(lin_red A)\<^sup>*\<^sup>* q 0

goal (1 subgoal):
 1. (lin_red A)\<^sup>*\<^sup>* p 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(lin_red A)\<^sup>*\<^sup>* p 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(lin_red A)\<^sup>*\<^sup>* p 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(lin_red A)\<^sup>*\<^sup>* f 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_pdata_pairs_to_listI1:
  assumes "(f, g) \<in> set ps"
  shows "monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f)))
              (fst f) \<in> set (pdata_pairs_to_list ps)" (is "?m \<in> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
proof (induct ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (f, g) \<in> set [] \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list [])
 2. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set []

goal (2 subgoals):
 1. (f, g) \<in> set [] \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list [])
 2. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set []

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list [])

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps)
(f, g) \<in> set (p # ps)

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
from Cons(2)
[PROOF STATE]
proof (chain)
picking this:
(f, g) \<in> set (p # ps)
[PROOF STEP]
have "p = (f, g) \<or> (f, g) \<in> set ps"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set (p # ps)

goal (1 subgoal):
 1. p = (f, g) \<or> (f, g) \<in> set ps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = (f, g) \<or> (f, g) \<in> set ps

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p = (f, g) \<or> (f, g) \<in> set ps

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = (f, g) \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
 2. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
assume "p = (f, g)"
[PROOF STATE]
proof (state)
this:
p = (f, g)

goal (2 subgoals):
 1. p = (f, g) \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
 2. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
by (simp add: \<open>p = (f, g)\<close> Let_def)
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))

goal (1 subgoal):
 1. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
assume "(f, g) \<in> set ps"
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps

goal (1 subgoal):
 1. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
hence "?m \<in> set (pdata_pairs_to_list ps)"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
by (rule Cons(1))
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps)

goal (1 subgoal):
 1. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list ps)

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f) \<in> set (pdata_pairs_to_list (p # ps))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_pdata_pairs_to_listI2:
  assumes "(f, g) \<in> set ps"
  shows "monom_mult (1 / lc (fst g)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst g)))
              (fst g) \<in> set (pdata_pairs_to_list ps)" (is "?m \<in> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
proof (induct ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (f, g) \<in> set [] \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list [])
 2. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set []

goal (2 subgoals):
 1. (f, g) \<in> set [] \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list [])
 2. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set []

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list [])

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps)
(f, g) \<in> set (p # ps)

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
from Cons(2)
[PROOF STATE]
proof (chain)
picking this:
(f, g) \<in> set (p # ps)
[PROOF STEP]
have "p = (f, g) \<or> (f, g) \<in> set ps"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set (p # ps)

goal (1 subgoal):
 1. p = (f, g) \<or> (f, g) \<in> set ps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = (f, g) \<or> (f, g) \<in> set ps

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>(f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps); (f, g) \<in> set (a # ps)\<rbrakk> \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (a # ps))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p = (f, g) \<or> (f, g) \<in> set ps

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = (f, g) \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
 2. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
assume "p = (f, g)"
[PROOF STATE]
proof (state)
this:
p = (f, g)

goal (2 subgoals):
 1. p = (f, g) \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
 2. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
by (simp add: \<open>p = (f, g)\<close> Let_def)
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))

goal (1 subgoal):
 1. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
assume "(f, g) \<in> set ps"
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps

goal (1 subgoal):
 1. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
hence "?m \<in> set (pdata_pairs_to_list ps)"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
by (rule Cons(1))
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps)

goal (1 subgoal):
 1. (f, g) \<in> set ps \<Longrightarrow> monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list ps)

goal (1 subgoal):
 1. monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
monom_mult ((1::'b) / lc (fst g)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst g)) (fst g) \<in> set (pdata_pairs_to_list (p # ps))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_pdata_pairs_to_listE:
  assumes "h \<in> set (pdata_pairs_to_list ps)"
  obtains f g where "(f, g) \<in> set ps \<or> (g, f) \<in> set ps"
    and "h = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<in> set (pdata_pairs_to_list ps)

goal (1 subgoal):
 1. (\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induct ps arbitrary: thesis)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set [] \<or> (g, f) \<in> set []; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list [])\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?f102, ?g102) \<in> set [] \<or> (?g102, ?f102) \<in> set []; h = monom_mult ((1::'b) / lc (fst ?f102)) (lcs (lp (fst ?f102)) (lp (fst ?g102)) - lp (fst ?f102)) (fst ?f102)\<rbrakk> \<Longrightarrow> thesis
h \<in> set (pdata_pairs_to_list [])

goal (2 subgoals):
 1. \<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set [] \<or> (g, f) \<in> set []; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list [])\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from Nil(2)
[PROOF STATE]
proof (chain)
picking this:
h \<in> set (pdata_pairs_to_list [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
h \<in> set (pdata_pairs_to_list [])

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

goal (1 subgoal):
 1. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> ?thesis102; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> ?thesis102
\<lbrakk>(?f102, ?g102) \<in> set (p # ps) \<or> (?g102, ?f102) \<in> set (p # ps); h = monom_mult ((1::'b) / lc (fst ?f102)) (lcs (lp (fst ?f102)) (lp (fst ?g102)) - lp (fst ?f102)) (fst ?f102)\<rbrakk> \<Longrightarrow> thesis
h \<in> set (pdata_pairs_to_list (p # ps))

goal (1 subgoal):
 1. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let ?f = "fst (fst p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let ?g = "fst (snd p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let ?lf = "lp ?f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let ?lg = "lp ?g"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let ?l = "lcs ?lf ?lg"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from Cons(3)
[PROOF STATE]
proof (chain)
picking this:
h \<in> set (pdata_pairs_to_list (p # ps))
[PROOF STEP]
have "h = monom_mult (1 / lc ?f) (?l - ?lf) ?f \<or> h = monom_mult (1 / lc ?g) (?l - ?lg) ?g \<or>
                     h \<in> set (pdata_pairs_to_list ps)"
[PROOF STATE]
proof (prove)
using this:
h \<in> set (pdata_pairs_to_list (p # ps))

goal (1 subgoal):
 1. h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p)) \<or> h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<or> h \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p)) \<or> h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<or> h \<in> set (pdata_pairs_to_list ps)

goal (1 subgoal):
 1. \<And>a ps thesis. \<lbrakk>\<And>thesis. \<lbrakk>\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis; \<And>f g. \<lbrakk>(f, g) \<in> set (a # ps) \<or> (g, f) \<in> set (a # ps); h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis; h \<in> set (pdata_pairs_to_list (a # ps))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p)) \<or> h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<or> h \<in> set (pdata_pairs_to_list ps)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p)) \<Longrightarrow> thesis
 2. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 3. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
assume h: "h = monom_mult (1 / lc ?f) (?l - ?lf) ?f"
[PROOF STATE]
proof (state)
this:
h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p))

goal (3 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p)) \<Longrightarrow> thesis
 2. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 3. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
have "(fst p, snd p) \<in> set (p # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst p, snd p) \<in> set (p # ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(fst p, snd p) \<in> set (p # ps)

goal (3 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p)) \<Longrightarrow> thesis
 2. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 3. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
hence "(fst p, snd p) \<in> set (p # ps) \<or> (snd p, fst p) \<in> set (p # ps)"
[PROOF STATE]
proof (prove)
using this:
(fst p, snd p) \<in> set (p # ps)

goal (1 subgoal):
 1. (fst p, snd p) \<in> set (p # ps) \<or> (snd p, fst p) \<in> set (p # ps)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(fst p, snd p) \<in> set (p # ps) \<or> (snd p, fst p) \<in> set (p # ps)

goal (3 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p)) \<Longrightarrow> thesis
 2. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 3. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
from this h
[PROOF STATE]
proof (chain)
picking this:
(fst p, snd p) \<in> set (p # ps) \<or> (snd p, fst p) \<in> set (p # ps)
h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(fst p, snd p) \<in> set (p # ps) \<or> (snd p, fst p) \<in> set (p # ps)
h = monom_mult ((1::'b) / lc (fst (fst p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (fst p))) (fst (fst p))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule Cons(2))
[PROOF STATE]
proof (state)
this:
thesis

goal (2 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 2. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 2. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
assume h: "h = monom_mult (1 / lc ?g) (?l - ?lg) ?g"
[PROOF STATE]
proof (state)
this:
h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p))

goal (2 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 2. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
have "(fst p, snd p) \<in> set (p # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst p, snd p) \<in> set (p # ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(fst p, snd p) \<in> set (p # ps)

goal (2 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 2. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
hence "(snd p, fst p) \<in> set (p # ps) \<or> (fst p, snd p) \<in> set (p # ps)"
[PROOF STATE]
proof (prove)
using this:
(fst p, snd p) \<in> set (p # ps)

goal (1 subgoal):
 1. (snd p, fst p) \<in> set (p # ps) \<or> (fst p, snd p) \<in> set (p # ps)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(snd p, fst p) \<in> set (p # ps) \<or> (fst p, snd p) \<in> set (p # ps)

goal (2 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 2. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(snd p, fst p) \<in> set (p # ps) \<or> (fst p, snd p) \<in> set (p # ps)

goal (2 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 2. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
from h
[PROOF STATE]
proof (chain)
picking this:
h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p))
[PROOF STEP]
have "h = monom_mult (1 / lc ?g) ((lcs ?lg ?lf) - ?lg) ?g"
[PROOF STATE]
proof (prove)
using this:
h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p))

goal (1 subgoal):
 1. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (snd p))) (lp (fst (fst p))) - lp (fst (snd p))) (fst (snd p))
[PROOF STEP]
by (simp only: lcs_comm)
[PROOF STATE]
proof (state)
this:
h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (snd p))) (lp (fst (fst p))) - lp (fst (snd p))) (fst (snd p))

goal (2 subgoals):
 1. h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (fst p))) (lp (fst (snd p))) - lp (fst (snd p))) (fst (snd p)) \<Longrightarrow> thesis
 2. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(snd p, fst p) \<in> set (p # ps) \<or> (fst p, snd p) \<in> set (p # ps)
h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (snd p))) (lp (fst (fst p))) - lp (fst (snd p))) (fst (snd p))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(snd p, fst p) \<in> set (p # ps) \<or> (fst p, snd p) \<in> set (p # ps)
h = monom_mult ((1::'b) / lc (fst (snd p))) (lcs (lp (fst (snd p))) (lp (fst (fst p))) - lp (fst (snd p))) (fst (snd p))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule Cons(2))
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
assume h_in: "h \<in> set (pdata_pairs_to_list ps)"
[PROOF STATE]
proof (state)
this:
h \<in> set (pdata_pairs_to_list ps)

goal (1 subgoal):
 1. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
obtain f g where "(f, g) \<in> set ps \<or> (g, f) \<in> set ps"
      and h: "h = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f g. \<lbrakk>(f, g) \<in> set ps \<or> (g, f) \<in> set ps; h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Cons(1), assumption, intro h_in)
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps
h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)

goal (1 subgoal):
 1. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps
[PROOF STEP]
have "(f, g) \<in> set (p # ps) \<or> (g, f) \<in> set (p # ps)"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps

goal (1 subgoal):
 1. (f, g) \<in> set (p # ps) \<or> (g, f) \<in> set (p # ps)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set (p # ps) \<or> (g, f) \<in> set (p # ps)

goal (1 subgoal):
 1. h \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> thesis
[PROOF STEP]
from this h
[PROOF STATE]
proof (chain)
picking this:
(f, g) \<in> set (p # ps) \<or> (g, f) \<in> set (p # ps)
h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set (p # ps) \<or> (g, f) \<in> set (p # ps)
h = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule Cons(2))
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f4_red_aux_not_zero: "0 \<notin> set (f4_red_aux bs ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> set (f4_red_aux bs ps)
[PROOF STEP]
by (simp add: f4_red_aux_def Let_def fst_sym_preproc set_Macaulay_red set_Macaulay_list)


[STATEMENT]
lemma f4_red_aux_irredudible:
  assumes "h \<in> set (f4_red_aux bs ps)" and "b \<in> set bs" and "fst b \<noteq> 0"
  shows "\<not> lt (fst b) adds\<^sub>t lt h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> lt (fst b) adds\<^sub>t lt h
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
from assms(1) f4_red_aux_not_zero
[PROOF STATE]
proof (chain)
picking this:
h \<in> set (f4_red_aux bs ps)
0 \<notin> set (f4_red_aux ?bs ?ps)
[PROOF STEP]
have "h \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
h \<in> set (f4_red_aux bs ps)
0 \<notin> set (f4_red_aux ?bs ?ps)

goal (1 subgoal):
 1. h \<noteq> 0
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
h \<noteq> 0

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
hence "lt h \<in> keys h"
[PROOF STATE]
proof (prove)
using this:
h \<noteq> 0

goal (1 subgoal):
 1. lt h \<in> keys h
[PROOF STEP]
by (rule lt_in_keys)
[PROOF STATE]
proof (state)
this:
lt h \<in> keys h

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lt h \<in> keys h

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
h \<in> set (f4_red_aux bs ps)
[PROOF STEP]
have "... \<subseteq> Keys (set (f4_red_aux bs ps))"
[PROOF STATE]
proof (prove)
using this:
h \<in> set (f4_red_aux bs ps)

goal (1 subgoal):
 1. keys h \<subseteq> Keys (set (f4_red_aux bs ps))
[PROOF STEP]
by (rule keys_subset_Keys)
[PROOF STATE]
proof (state)
this:
keys h \<subseteq> Keys (set (f4_red_aux bs ps))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
keys h \<subseteq> Keys (set (f4_red_aux bs ps))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
have "... \<subseteq> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
    (is "_ \<subseteq> Keys (set ?s)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Keys (set (f4_red_aux bs ps)) \<subseteq> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
by (simp only: f4_red_aux_def Let_def fst_sym_preproc Keys_Macaulay_red)
[PROOF STATE]
proof (state)
this:
Keys (set (f4_red_aux bs ps)) \<subseteq> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lt h \<in> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
have "lt h \<in> Keys (set ?s)"
[PROOF STATE]
proof (prove)
using this:
lt h \<in> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. lt h \<in> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lt h \<in> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lt h \<in> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
b \<in> set bs
[PROOF STEP]
have "fst b \<in> set (map fst bs)"
[PROOF STATE]
proof (prove)
using this:
b \<in> set bs

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

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst b \<in> set (map fst bs)

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
assume a: "lt (fst b) adds\<^sub>t lt h"
[PROOF STATE]
proof (state)
this:
lt (fst b) adds\<^sub>t lt h

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lt h \<in> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
fst b \<in> set (map fst bs)
lt (fst b) adds\<^sub>t lt h
[PROOF STEP]
have "monom_mult 1 (lp h - lp (fst b)) (fst b) \<in> set ?s" (is "?m \<in> _")
[PROOF STATE]
proof (prove)
using this:
lt h \<in> Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
fst b \<in> set (map fst bs)
lt (fst b) adds\<^sub>t lt h

goal (1 subgoal):
 1. monom_mult (1::'b) (lp h - lp (fst b)) (fst b) \<in> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))
[PROOF STEP]
by (rule snd_sym_preproc_complete)
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (lp h - lp (fst b)) (fst b) \<in> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
fst b \<noteq> 0
[PROOF STEP]
have "?m \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
fst b \<noteq> 0

goal (1 subgoal):
 1. monom_mult (1::'b) (lp h - lp (fst b)) (fst b) \<noteq> 0
[PROOF STEP]
by (simp add: monom_mult_eq_zero_iff)
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (lp h - lp (fst b)) (fst b) \<noteq> 0

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
with \<open>?m \<in> set ?s\<close>
[PROOF STATE]
proof (chain)
picking this:
monom_mult (1::'b) (lp h - lp (fst b)) (fst b) \<in> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))
monom_mult (1::'b) (lp h - lp (fst b)) (fst b) \<noteq> 0
[PROOF STEP]
have "lt ?m \<in> lt_set (set ?s)"
[PROOF STATE]
proof (prove)
using this:
monom_mult (1::'b) (lp h - lp (fst b)) (fst b) \<in> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))
monom_mult (1::'b) (lp h - lp (fst b)) (fst b) \<noteq> 0

goal (1 subgoal):
 1. lt (monom_mult (1::'b) (lp h - lp (fst b)) (fst b)) \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
by (rule lt_setI)
[PROOF STATE]
proof (state)
this:
lt (monom_mult (1::'b) (lp h - lp (fst b)) (fst b)) \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lt (monom_mult (1::'b) (lp h - lp (fst b)) (fst b)) \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
from assms(3) a
[PROOF STATE]
proof (chain)
picking this:
fst b \<noteq> 0
lt (fst b) adds\<^sub>t lt h
[PROOF STEP]
have "lt ?m = lt h"
[PROOF STATE]
proof (prove)
using this:
fst b \<noteq> 0
lt (fst b) adds\<^sub>t lt h

goal (1 subgoal):
 1. lt (monom_mult (1::'b) (lp h - lp (fst b)) (fst b)) = lt h
[PROOF STEP]
by (simp add: lt_monom_mult, metis add_diff_cancel_right' adds_termE pp_of_term_splus)
[PROOF STATE]
proof (state)
this:
lt (monom_mult (1::'b) (lp h - lp (fst b)) (fst b)) = lt h

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lt (monom_mult (1::'b) (lp h - lp (fst b)) (fst b)) \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
lt (monom_mult (1::'b) (lp h - lp (fst b)) (fst b)) = lt h
[PROOF STEP]
have "lt h \<in> lt_set (set ?s)"
[PROOF STATE]
proof (prove)
using this:
lt (monom_mult (1::'b) (lp h - lp (fst b)) (fst b)) \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
lt (monom_mult (1::'b) (lp h - lp (fst b)) (fst b)) = lt h

goal (1 subgoal):
 1. lt h \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lt h \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lt h \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
h \<in> set (f4_red_aux bs ps)
[PROOF STEP]
have "lt h \<notin> lt_set (set ?s)"
[PROOF STATE]
proof (prove)
using this:
h \<in> set (f4_red_aux bs ps)

goal (1 subgoal):
 1. lt h \<notin> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
by (simp add: f4_red_aux_def Let_def fst_sym_preproc set_Macaulay_red)
[PROOF STATE]
proof (state)
this:
lt h \<notin> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. lt (fst b) adds\<^sub>t lt h \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lt h \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
lt h \<notin> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
lt h \<in> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
lt h \<notin> lt_set (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

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

goal:
No subgoals!
[PROOF STEP]
qed