[STATEMENT]
lemma f4_red_aux_dgrad_p_set_le:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d (set (f4_red_aux bs ps)) (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_p_set_le d (set (f4_red_aux bs ps)) (args_to_set ([], bs, ps))
[PROOF STEP]
unfolding dgrad_p_set_le_def dgrad_set_le_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>pp_of_term ` Keys (set (f4_red_aux bs ps)). \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
assume "s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps))"
[PROOF STATE]
proof (state)
this:
s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps))

goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps))

goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
have "... \<subseteq> pp_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
    (is "_ \<subseteq> pp_of_term ` Keys (set ?s)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pp_of_term ` Keys (set (f4_red_aux bs ps)) \<subseteq> pp_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
by (rule image_mono, simp only: f4_red_aux_def Let_def fst_sym_preproc Keys_Macaulay_red)
[PROOF STATE]
proof (state)
this:
pp_of_term ` Keys (set (f4_red_aux bs ps)) \<subseteq> pp_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
s \<in> pp_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
have "s \<in> pp_of_term ` Keys (set ?s)"
[PROOF STATE]
proof (prove)
using this:
s \<in> pp_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

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

goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
with snd_sym_preproc_dgrad_set_le[OF assms]
[PROOF STATE]
proof (chain)
picking this:
dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc ?gs ?fs)))) (pp_of_term ` Keys (set ?gs \<union> set ?fs))
s \<in> pp_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
obtain t
    where "t \<in> pp_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps))" and "d s \<le> d t"
[PROOF STATE]
proof (prove)
using this:
dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc ?gs ?fs)))) (pp_of_term ` Keys (set ?gs \<union> set ?fs))
s \<in> pp_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> pp_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps)); d s \<le> d t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule dgrad_set_leE)
[PROOF STATE]
proof (state)
this:
t \<in> pp_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps))
d s \<le> d t

goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
t \<in> pp_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps))
[PROOF STEP]
have "t \<in> pp_of_term ` Keys (fst ` set bs) \<or> t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps))"
[PROOF STATE]
proof (prove)
using this:
t \<in> pp_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (fst ` set bs) \<or> t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps))
[PROOF STEP]
by (simp add: Keys_Un image_Un)
[PROOF STATE]
proof (state)
this:
t \<in> pp_of_term ` Keys (fst ` set bs) \<or> t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
thus "\<exists>t \<in> pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t"
[PROOF STATE]
proof (prove)
using this:
t \<in> pp_of_term ` Keys (fst ` set bs) \<or> t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<in> pp_of_term ` Keys (fst ` set bs) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
assume "t \<in> pp_of_term ` Keys (fst `  set bs)"
[PROOF STATE]
proof (state)
this:
t \<in> pp_of_term ` Keys (fst ` set bs)

goal (2 subgoals):
 1. t \<in> pp_of_term ` Keys (fst ` set bs) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t \<in> pp_of_term ` Keys (fst ` set bs)

goal (2 subgoals):
 1. t \<in> pp_of_term ` Keys (fst ` set bs) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
have "... \<subseteq> pp_of_term ` Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pp_of_term ` Keys (fst ` set bs) \<subseteq> pp_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
by (rule image_mono, rule Keys_mono, auto simp add: args_to_set_alt)
[PROOF STATE]
proof (state)
this:
pp_of_term ` Keys (fst ` set bs) \<subseteq> pp_of_term ` Keys (args_to_set ([], bs, ps))

goal (2 subgoals):
 1. t \<in> pp_of_term ` Keys (fst ` set bs) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
t \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
have "t \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
t \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
t \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))

goal (2 subgoals):
 1. t \<in> pp_of_term ` Keys (fst ` set bs) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
with \<open>d s \<le> d t\<close>
[PROOF STATE]
proof (chain)
picking this:
d s \<le> d t
t \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d s \<le> d t
t \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
assume "t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps))"
[PROOF STATE]
proof (state)
this:
t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps))
[PROOF STEP]
obtain p where "p \<in> set (pdata_pairs_to_list ps)" and "t \<in> pp_of_term ` keys p"
[PROOF STATE]
proof (prove)
using this:
t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> set (pdata_pairs_to_list ps); t \<in> pp_of_term ` keys p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: in_KeysE)
[PROOF STATE]
proof (state)
this:
p \<in> set (pdata_pairs_to_list ps)
t \<in> pp_of_term ` keys p

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
obtain f g where disj: "(f, g) \<in> set ps \<or> (g, f) \<in> set ps"
      and p: "p = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
[PROOF STATE]
proof (prove)
using this:
p \<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; p = 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 in_pdata_pairs_to_listE)
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps
p = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
from disj
[PROOF STATE]
proof (chain)
picking this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps
[PROOF STEP]
have "fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps

goal (1 subgoal):
 1. fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (f, g) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
 2. (g, f) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
assume "(f, g) \<in> set ps"
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps

goal (2 subgoals):
 1. (f, g) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
 2. (g, f) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
hence "f \<in> fst ` set ps" and "g \<in> snd ` set ps"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps

goal (1 subgoal):
 1. f \<in> fst ` set ps &&& g \<in> snd ` set ps
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
f \<in> fst ` set ps
g \<in> snd ` set ps

goal (2 subgoals):
 1. (f, g) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
 2. (g, f) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
hence "fst f \<in> fst ` fst ` set ps" and "fst g \<in> fst ` snd ` set ps"
[PROOF STATE]
proof (prove)
using this:
f \<in> fst ` set ps
g \<in> snd ` set ps

goal (1 subgoal):
 1. fst f \<in> fst ` fst ` set ps &&& fst g \<in> fst ` snd ` set ps
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
fst f \<in> fst ` fst ` set ps
fst g \<in> fst ` snd ` set ps

goal (2 subgoals):
 1. (f, g) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
 2. (g, f) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fst f \<in> fst ` fst ` set ps
fst g \<in> fst ` snd ` set ps

goal (1 subgoal):
 1. fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
by (simp add: args_to_set_def image_Un)
[PROOF STATE]
proof (state)
this:
fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. (g, f) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (g, f) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
assume "(g, f) \<in> set ps"
[PROOF STATE]
proof (state)
this:
(g, f) \<in> set ps

goal (1 subgoal):
 1. (g, f) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
hence "f \<in> snd ` set ps" and "g \<in> fst ` set ps"
[PROOF STATE]
proof (prove)
using this:
(g, f) \<in> set ps

goal (1 subgoal):
 1. f \<in> snd ` set ps &&& g \<in> fst ` set ps
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
f \<in> snd ` set ps
g \<in> fst ` set ps

goal (1 subgoal):
 1. (g, f) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
hence "fst f \<in> fst ` snd ` set ps" and "fst g \<in> fst ` fst ` set ps"
[PROOF STATE]
proof (prove)
using this:
f \<in> snd ` set ps
g \<in> fst ` set ps

goal (1 subgoal):
 1. fst f \<in> fst ` snd ` set ps &&& fst g \<in> fst ` fst ` set ps
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
fst f \<in> fst ` snd ` set ps
fst g \<in> fst ` fst ` set ps

goal (1 subgoal):
 1. (g, f) \<in> set ps \<Longrightarrow> fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fst f \<in> fst ` snd ` set ps
fst g \<in> fst ` fst ` set ps

goal (1 subgoal):
 1. fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
by (simp add: args_to_set_def image_Un)
[PROOF STATE]
proof (state)
this:
fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
hence "fst f \<in> args_to_set ([], bs, ps)" and "fst g \<in> args_to_set ([], bs, ps)"
[PROOF STATE]
proof (prove)
using this:
fst f \<in> args_to_set ([], bs, ps) \<and> fst g \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. fst f \<in> args_to_set ([], bs, ps) &&& fst g \<in> args_to_set ([], bs, ps)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
fst f \<in> args_to_set ([], bs, ps)
fst g \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
hence keys_f: "keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))"
      and keys_g: "keys (fst g) \<subseteq> Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
fst f \<in> args_to_set ([], bs, ps)
fst g \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps)) &&& keys (fst g) \<subseteq> Keys (args_to_set ([], bs, ps))
[PROOF STEP]
by (auto intro!: keys_subset_Keys)
[PROOF STATE]
proof (state)
this:
keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))
keys (fst g) \<subseteq> Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
let ?lf = "lp (fst f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
let ?lg = "lp (fst g)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
define l where "l = lcs ?lf ?lg"
[PROOF STATE]
proof (state)
this:
l = lcs (lp (fst f)) (lp (fst g))

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
have "pp_of_term ` keys p \<subseteq> pp_of_term ` ((\<oplus>) (lcs ?lf ?lg - ?lf) ` keys (fst f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pp_of_term ` keys p \<subseteq> pp_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pp_of_term ` keys (monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)) \<subseteq> pp_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
using keys_monom_mult_subset
[PROOF STATE]
proof (prove)
using this:
keys (monom_mult ?c ?t ?p) \<subseteq> (\<oplus>) ?t ` keys ?p

goal (1 subgoal):
 1. pp_of_term ` keys (monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)) \<subseteq> pp_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
by (rule image_mono)
[PROOF STATE]
proof (state)
this:
pp_of_term ` keys p \<subseteq> pp_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
with \<open>t \<in> pp_of_term ` keys p\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> pp_of_term ` keys p
pp_of_term ` keys p \<subseteq> pp_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
have "t \<in> pp_of_term ` ((\<oplus>) (l - ?lf) ` keys (fst f))"
[PROOF STATE]
proof (prove)
using this:
t \<in> pp_of_term ` keys p
pp_of_term ` keys p \<subseteq> pp_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. t \<in> pp_of_term ` (\<oplus>) (l - lp (fst f)) ` keys (fst f)
[PROOF STEP]
unfolding l_def
[PROOF STATE]
proof (prove)
using this:
t \<in> pp_of_term ` keys p
pp_of_term ` keys p \<subseteq> pp_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. t \<in> pp_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
t \<in> pp_of_term ` (\<oplus>) (l - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> pp_of_term ` (\<oplus>) (l - lp (fst f)) ` keys (fst f)
[PROOF STEP]
obtain t' where "t' \<in> pp_of_term ` keys (fst f)" and t: "t = (l - ?lf) + t'"
[PROOF STATE]
proof (prove)
using this:
t \<in> pp_of_term ` (\<oplus>) (l - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<in> pp_of_term ` keys (fst f); t = l - lp (fst f) + t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pp_of_term_splus
[PROOF STATE]
proof (prove)
using this:
t \<in> pp_of_term ` (\<oplus>) (l - lp (fst f)) ` keys (fst f)
pp_of_term (?t \<oplus> ?v) = ?t + pp_of_term ?v

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<in> pp_of_term ` keys (fst f); t = l - lp (fst f) + t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
t' \<in> pp_of_term ` keys (fst f)
t = l - lp (fst f) + t'

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
t' \<in> pp_of_term ` keys (fst f)
[PROOF STEP]
have "fst f \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
t' \<in> pp_of_term ` keys (fst f)

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

goal (1 subgoal):
 1. t \<in> pp_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
proof (cases "fst g = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst g = 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
fst g = 0

goal (2 subgoals):
 1. fst g = 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
hence "?lg = 0"
[PROOF STATE]
proof (prove)
using this:
fst g = 0

goal (1 subgoal):
 1. lp (fst g) = (0::'a)
[PROOF STEP]
by (simp add: lt_def min_term_def term_simps)
[PROOF STATE]
proof (state)
this:
lp (fst g) = (0::'a)

goal (2 subgoals):
 1. fst g = 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
hence "l = ?lf"
[PROOF STATE]
proof (prove)
using this:
lp (fst g) = (0::'a)

goal (1 subgoal):
 1. l = lp (fst f)
[PROOF STEP]
by (simp add: l_def lcs_zero lcs_comm)
[PROOF STATE]
proof (state)
this:
l = lp (fst f)

goal (2 subgoals):
 1. fst g = 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
hence "t = t'"
[PROOF STATE]
proof (prove)
using this:
l = lp (fst f)

goal (1 subgoal):
 1. t = t'
[PROOF STEP]
by (simp add: t)
[PROOF STATE]
proof (state)
this:
t = t'

goal (2 subgoals):
 1. fst g = 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
with \<open>d s \<le> d t\<close>
[PROOF STATE]
proof (chain)
picking this:
d s \<le> d t
t = t'
[PROOF STEP]
have "d s \<le> d t'"
[PROOF STATE]
proof (prove)
using this:
d s \<le> d t
t = t'

goal (1 subgoal):
 1. d s \<le> d t'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d s \<le> d t'

goal (2 subgoals):
 1. fst g = 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d s \<le> d t'

goal (2 subgoals):
 1. fst g = 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
from \<open>t' \<in> pp_of_term ` keys (fst f)\<close> keys_f
[PROOF STATE]
proof (chain)
picking this:
t' \<in> pp_of_term ` keys (fst f)
keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))
[PROOF STEP]
have "t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
t' \<in> pp_of_term ` keys (fst f)
keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))

goal (2 subgoals):
 1. fst g = 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
d s \<le> d t'
t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d s \<le> d t'
t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t

goal (1 subgoal):
 1. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
fst g \<noteq> 0

goal (1 subgoal):
 1. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
have "d t = d (l - ?lf) \<or> d t = d t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d t = d (l - lp (fst f)) \<or> d t = d t'
[PROOF STEP]
by (auto simp add: t dickson_gradingD1[OF assms])
[PROOF STATE]
proof (state)
this:
d t = d (l - lp (fst f)) \<or> d t = d t'

goal (1 subgoal):
 1. fst g \<noteq> 0 \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d t = d (l - lp (fst f)) \<or> d t = d t'

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d t = d (l - lp (fst f)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
assume "d t = d (l - ?lf)"
[PROOF STATE]
proof (state)
this:
d t = d (l - lp (fst f))

goal (2 subgoals):
 1. d t = d (l - lp (fst f)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d t = d (l - lp (fst f))

goal (2 subgoals):
 1. d t = d (l - lp (fst f)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
dickson_grading d
[PROOF STEP]
have "... \<le> ord_class.max (d ?lf) (d ?lg)"
[PROOF STATE]
proof (prove)
using this:
dickson_grading d

goal (1 subgoal):
 1. d (l - lp (fst f)) \<le> ord_class.max (d (lp (fst f))) (d (lp (fst g)))
[PROOF STEP]
unfolding l_def
[PROOF STATE]
proof (prove)
using this:
dickson_grading d

goal (1 subgoal):
 1. d (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) \<le> ord_class.max (d (lp (fst f))) (d (lp (fst g)))
[PROOF STEP]
by (rule dickson_grading_lcs_minus)
[PROOF STATE]
proof (state)
this:
d (l - lp (fst f)) \<le> ord_class.max (d (lp (fst f))) (d (lp (fst g)))

goal (2 subgoals):
 1. d t = d (l - lp (fst f)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d t \<le> ord_class.max (d (lp (fst f))) (d (lp (fst g)))
[PROOF STEP]
have "d s \<le> d ?lf \<or> d s \<le> d ?lg"
[PROOF STATE]
proof (prove)
using this:
d t \<le> ord_class.max (d (lp (fst f))) (d (lp (fst g)))

goal (1 subgoal):
 1. d s \<le> d (lp (fst f)) \<or> d s \<le> d (lp (fst g))
[PROOF STEP]
using \<open>d s \<le> d t\<close>
[PROOF STATE]
proof (prove)
using this:
d t \<le> ord_class.max (d (lp (fst f))) (d (lp (fst g)))
d s \<le> d t

goal (1 subgoal):
 1. d s \<le> d (lp (fst f)) \<or> d s \<le> d (lp (fst g))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d s \<le> d (lp (fst f)) \<or> d s \<le> d (lp (fst g))

goal (2 subgoals):
 1. d t = d (l - lp (fst f)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d s \<le> d (lp (fst f)) \<or> d s \<le> d (lp (fst g))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d s \<le> d (lp (fst f)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. d s \<le> d (lp (fst g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
assume "d s \<le> d ?lf"
[PROOF STATE]
proof (state)
this:
d s \<le> d (lp (fst f))

goal (2 subgoals):
 1. d s \<le> d (lp (fst f)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. d s \<le> d (lp (fst g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d s \<le> d (lp (fst f))

goal (2 subgoals):
 1. d s \<le> d (lp (fst f)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. d s \<le> d (lp (fst g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
have "lt (fst f) \<in> Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt (fst f) \<in> Keys (args_to_set ([], bs, ps))
[PROOF STEP]
by (rule, rule lt_in_keys, fact+)
[PROOF STATE]
proof (state)
this:
lt (fst f) \<in> Keys (args_to_set ([], bs, ps))

goal (2 subgoals):
 1. d s \<le> d (lp (fst f)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
 2. d s \<le> d (lp (fst g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
d s \<le> d (lp (fst f))
lt (fst f) \<in> Keys (args_to_set ([], bs, ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d s \<le> d (lp (fst f))
lt (fst f) \<in> Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t

goal (1 subgoal):
 1. d s \<le> d (lp (fst g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d s \<le> d (lp (fst g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
assume "d s \<le> d ?lg"
[PROOF STATE]
proof (state)
this:
d s \<le> d (lp (fst g))

goal (1 subgoal):
 1. d s \<le> d (lp (fst g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d s \<le> d (lp (fst g))

goal (1 subgoal):
 1. d s \<le> d (lp (fst g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
have "lt (fst g) \<in> Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt (fst g) \<in> Keys (args_to_set ([], bs, ps))
[PROOF STEP]
by (rule, rule lt_in_keys, fact+)
[PROOF STATE]
proof (state)
this:
lt (fst g) \<in> Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. d s \<le> d (lp (fst g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
d s \<le> d (lp (fst g))
lt (fst g) \<in> Keys (args_to_set ([], bs, ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d s \<le> d (lp (fst g))
lt (fst g) \<in> Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t

goal (1 subgoal):
 1. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
assume "d t = d t'"
[PROOF STATE]
proof (state)
this:
d t = d t'

goal (1 subgoal):
 1. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
with \<open>d s \<le> d t\<close>
[PROOF STATE]
proof (chain)
picking this:
d s \<le> d t
d t = d t'
[PROOF STEP]
have "d s \<le> d t'"
[PROOF STATE]
proof (prove)
using this:
d s \<le> d t
d t = d t'

goal (1 subgoal):
 1. d s \<le> d t'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d s \<le> d t'

goal (1 subgoal):
 1. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d s \<le> d t'

goal (1 subgoal):
 1. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
from \<open>t' \<in> pp_of_term ` keys (fst f)\<close> keys_f
[PROOF STATE]
proof (chain)
picking this:
t' \<in> pp_of_term ` keys (fst f)
keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))
[PROOF STEP]
have "t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
t' \<in> pp_of_term ` keys (fst f)
keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. d t = d t' \<Longrightarrow> \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
d s \<le> d t'
t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d s \<le> d t'
t' \<in> pp_of_term ` Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` Keys (args_to_set ([], bs, ps)). d s \<le> d t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma components_f4_red_aux_subset:
  "component_of_term ` Keys (set (f4_red_aux bs ps)) \<subseteq> component_of_term ` Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (f4_red_aux bs ps)) \<subseteq> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> x \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> x \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
assume "k \<in> component_of_term ` Keys (set (f4_red_aux bs ps))"
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` Keys (set (f4_red_aux bs ps))

goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> x \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` Keys (set (f4_red_aux bs ps))

goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> x \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
have "... \<subseteq> component_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (f4_red_aux bs ps)) \<subseteq> component_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
by (rule image_mono, simp only: f4_red_aux_def Let_def fst_sym_preproc Keys_Macaulay_red)
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (f4_red_aux bs ps)) \<subseteq> component_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> x \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (f4_red_aux bs ps)) \<subseteq> component_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> x \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
have "... \<subseteq> component_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) \<subseteq> component_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps))
[PROOF STEP]
by (fact components_snd_sym_preproc_subset)
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) \<subseteq> component_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> x \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
k \<in> component_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps))
[PROOF STEP]
have "k \<in> component_of_term ` Keys (fst ` set bs) \<union> component_of_term ` Keys (set (pdata_pairs_to_list ps))"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` Keys (set (map fst bs) \<union> set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (fst ` set bs) \<union> component_of_term ` Keys (set (pdata_pairs_to_list ps))
[PROOF STEP]
by (simp add: image_Un Keys_Un)
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` Keys (fst ` set bs) \<union> component_of_term ` Keys (set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` Keys (set (f4_red_aux bs ps)) \<Longrightarrow> x \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
thus "k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` Keys (fst ` set bs) \<union> component_of_term ` Keys (set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<in> component_of_term ` Keys (fst ` set bs) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
 2. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
assume "k \<in> component_of_term ` Keys (fst `  set bs)"
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` Keys (fst ` set bs)

goal (2 subgoals):
 1. k \<in> component_of_term ` Keys (fst ` set bs) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
 2. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` Keys (fst ` set bs)

goal (2 subgoals):
 1. k \<in> component_of_term ` Keys (fst ` set bs) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
 2. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
have "... \<subseteq> component_of_term ` Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (fst ` set bs) \<subseteq> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
by (rule image_mono, rule Keys_mono, auto simp add: args_to_set_alt)
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (fst ` set bs) \<subseteq> component_of_term ` Keys (args_to_set ([], bs, ps))

goal (2 subgoals):
 1. k \<in> component_of_term ` Keys (fst ` set bs) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
 2. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
show "k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
assume "k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps))"
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps))
[PROOF STEP]
obtain p where "p \<in> set (pdata_pairs_to_list ps)" and "k \<in> component_of_term ` keys p"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> set (pdata_pairs_to_list ps); k \<in> component_of_term ` keys p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: in_KeysE)
[PROOF STATE]
proof (state)
this:
p \<in> set (pdata_pairs_to_list ps)
k \<in> component_of_term ` keys p

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
obtain f g where disj: "(f, g) \<in> set ps \<or> (g, f) \<in> set ps"
      and p: "p = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
[PROOF STATE]
proof (prove)
using this:
p \<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; p = 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 in_pdata_pairs_to_listE)
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps
p = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
from disj
[PROOF STATE]
proof (chain)
picking this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps
[PROOF STEP]
have "fst f \<in> args_to_set ([], bs, ps)"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps

goal (1 subgoal):
 1. fst f \<in> args_to_set ([], bs, ps)
[PROOF STEP]
by (simp add: args_to_set_alt, metis fst_conv image_eqI snd_conv)
[PROOF STATE]
proof (state)
this:
fst f \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
hence "fst f \<in> args_to_set ([], bs, ps)"
[PROOF STATE]
proof (prove)
using this:
fst f \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. fst f \<in> args_to_set ([], bs, ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst f \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
hence keys_f: "keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
fst f \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))
[PROOF STEP]
by (auto intro!: keys_subset_Keys)
[PROOF STATE]
proof (state)
this:
keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
let ?lf = "lp (fst f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
let ?lg = "lp (fst g)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
define l where "l = lcs ?lf ?lg"
[PROOF STATE]
proof (state)
this:
l = lcs (lp (fst f)) (lp (fst g))

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
have "component_of_term ` keys p \<subseteq> component_of_term ` ((\<oplus>) (lcs ?lf ?lg - ?lf) ` keys (fst f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` keys p \<subseteq> component_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` keys (monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)) \<subseteq> component_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
using keys_monom_mult_subset
[PROOF STATE]
proof (prove)
using this:
keys (monom_mult ?c ?t ?p) \<subseteq> (\<oplus>) ?t ` keys ?p

goal (1 subgoal):
 1. component_of_term ` keys (monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)) \<subseteq> component_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
by (rule image_mono)
[PROOF STATE]
proof (state)
this:
component_of_term ` keys p \<subseteq> component_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
with \<open>k \<in> component_of_term ` keys p\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<in> component_of_term ` keys p
component_of_term ` keys p \<subseteq> component_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
have "k \<in> component_of_term ` ((\<oplus>) (l - ?lf) ` keys (fst f))"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` keys p
component_of_term ` keys p \<subseteq> component_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. k \<in> component_of_term ` (\<oplus>) (l - lp (fst f)) ` keys (fst f)
[PROOF STEP]
unfolding l_def
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` keys p
component_of_term ` keys p \<subseteq> component_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. k \<in> component_of_term ` (\<oplus>) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) ` keys (fst f)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` (\<oplus>) (l - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
hence "k \<in> component_of_term ` keys (fst f)"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` (\<oplus>) (l - lp (fst f)) ` keys (fst f)

goal (1 subgoal):
 1. k \<in> component_of_term ` keys (fst f)
[PROOF STEP]
using component_of_term_splus
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` (\<oplus>) (l - lp (fst f)) ` keys (fst f)
component_of_term (?t \<oplus> ?v) = component_of_term ?v

goal (1 subgoal):
 1. k \<in> component_of_term ` keys (fst f)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` keys (fst f)

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (set (pdata_pairs_to_list ps)) \<Longrightarrow> k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
with keys_f
[PROOF STATE]
proof (chain)
picking this:
keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))
k \<in> component_of_term ` keys (fst f)
[PROOF STEP]
show "k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
keys (fst f) \<subseteq> Keys (args_to_set ([], bs, ps))
k \<in> component_of_term ` keys (fst f)

goal (1 subgoal):
 1. k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` Keys (args_to_set ([], bs, ps))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmdl_f4_red_aux: "set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
have "set (f4_red_aux bs ps) \<subseteq>
          set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
by (auto simp add: f4_red_aux_def Let_def fst_sym_preproc set_Macaulay_red)
[PROOF STATE]
proof (state)
this:
set (f4_red_aux bs ps) \<subseteq> set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (f4_red_aux bs ps) \<subseteq> set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
have "... \<subseteq> pmdl (set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) \<subseteq> pmdl (set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))))
[PROOF STEP]
by (fact pmdl.span_superset)
[PROOF STATE]
proof (state)
this:
set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) \<subseteq> pmdl (set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) \<subseteq> pmdl (set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
have "... = pmdl (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))) = pmdl (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
by (fact pmdl_Macaulay_list)
[PROOF STATE]
proof (state)
this:
pmdl (set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))) = pmdl (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmdl (set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))) = pmdl (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
have "... \<subseteq> pmdl (set (map fst bs) \<union>
                        set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) \<subseteq> pmdl (set (map fst bs) \<union> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))
[PROOF STEP]
by (rule pmdl.span_mono, blast)
[PROOF STATE]
proof (state)
this:
pmdl (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) \<subseteq> pmdl (set (map fst bs) \<union> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmdl (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) \<subseteq> pmdl (set (map fst bs) \<union> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
have "... = pmdl (set (map fst bs) \<union> set (pdata_pairs_to_list ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (set (map fst bs) \<union> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) = pmdl (set (map fst bs) \<union> set (pdata_pairs_to_list ps))
[PROOF STEP]
by (fact snd_sym_preproc_pmdl)
[PROOF STATE]
proof (state)
this:
pmdl (set (map fst bs) \<union> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) = pmdl (set (map fst bs) \<union> set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmdl (set (map fst bs) \<union> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))) = pmdl (set (map fst bs) \<union> set (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
have "... \<subseteq> pmdl (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (set (map fst bs) \<union> set (pdata_pairs_to_list ps)) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
proof (rule pmdl.span_subset_spanI, simp only: Un_subset_iff, rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (map fst bs) \<subseteq> pmdl (args_to_set ([], bs, ps))
 2. set (pdata_pairs_to_list ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
have "set (map fst bs) \<subseteq> args_to_set ([], bs, ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map fst bs) \<subseteq> args_to_set ([], bs, ps)
[PROOF STEP]
by (auto simp add: args_to_set_def)
[PROOF STATE]
proof (state)
this:
set (map fst bs) \<subseteq> args_to_set ([], bs, ps)

goal (2 subgoals):
 1. set (map fst bs) \<subseteq> pmdl (args_to_set ([], bs, ps))
 2. set (pdata_pairs_to_list ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (map fst bs) \<subseteq> args_to_set ([], bs, ps)

goal (2 subgoals):
 1. set (map fst bs) \<subseteq> pmdl (args_to_set ([], bs, ps))
 2. set (pdata_pairs_to_list ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
have "... \<subseteq> pmdl (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. args_to_set ([], bs, ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
by (rule pmdl.span_superset)
[PROOF STATE]
proof (state)
this:
args_to_set ([], bs, ps) \<subseteq> pmdl (args_to_set ([], bs, ps))

goal (2 subgoals):
 1. set (map fst bs) \<subseteq> pmdl (args_to_set ([], bs, ps))
 2. set (pdata_pairs_to_list ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (map fst bs) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
show "set (map fst bs) \<subseteq> pmdl (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
set (map fst bs) \<subseteq> pmdl (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. set (map fst bs) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (map fst bs) \<subseteq> pmdl (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. set (pdata_pairs_to_list ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (pdata_pairs_to_list ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
show "set (pdata_pairs_to_list ps) \<subseteq> pmdl (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (pdata_pairs_to_list ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> x \<in> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> x \<in> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
assume "p \<in> set (pdata_pairs_to_list ps)"
[PROOF STATE]
proof (state)
this:
p \<in> set (pdata_pairs_to_list ps)

goal (1 subgoal):
 1. \<And>x. x \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> x \<in> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
obtain f g where "(f, g) \<in> set ps \<or> (g, f) \<in> set ps"
        and p: "p = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
[PROOF STATE]
proof (prove)
using this:
p \<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; p = 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 in_pdata_pairs_to_listE)
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps
p = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)

goal (1 subgoal):
 1. \<And>x. x \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> x \<in> pmdl (args_to_set ([], bs, ps))
[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 \<in> fst ` set ps \<union> snd ` set ps"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps

goal (1 subgoal):
 1. f \<in> fst ` set ps \<union> snd ` set ps
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f \<in> fst ` set ps \<union> snd ` set ps

goal (1 subgoal):
 1. \<And>x. x \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> x \<in> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
hence "fst f \<in> args_to_set ([], bs, ps)"
[PROOF STATE]
proof (prove)
using this:
f \<in> fst ` set ps \<union> snd ` set ps

goal (1 subgoal):
 1. fst f \<in> args_to_set ([], bs, ps)
[PROOF STEP]
by (auto simp add: args_to_set_alt)
[PROOF STATE]
proof (state)
this:
fst f \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. \<And>x. x \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> x \<in> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
hence "fst f \<in> pmdl (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
fst f \<in> args_to_set ([], bs, ps)

goal (1 subgoal):
 1. fst f \<in> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
by (rule pmdl.span_base)
[PROOF STATE]
proof (state)
this:
fst f \<in> pmdl (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. \<And>x. x \<in> set (pdata_pairs_to_list ps) \<Longrightarrow> x \<in> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
thus "p \<in> pmdl (args_to_set ([], bs, ps))"
[PROOF STATE]
proof (prove)
using this:
fst f \<in> pmdl (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. p \<in> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
using this:
fst f \<in> pmdl (args_to_set ([], bs, 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> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
by (rule pmdl_closed_monom_mult)
[PROOF STATE]
proof (state)
this:
p \<in> pmdl (args_to_set ([], bs, ps))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (pdata_pairs_to_list ps) \<subseteq> pmdl (args_to_set ([], bs, ps))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pmdl (set (map fst bs) \<union> set (pdata_pairs_to_list ps)) \<subseteq> pmdl (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))

goal (1 subgoal):
 1. set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (f4_red_aux bs ps) \<subseteq> pmdl (args_to_set ([], bs, ps))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f4_red_aux_phull_reducible:
  assumes "set ps \<subseteq> set bs \<times> set bs"
    and "f \<in> phull (set (pdata_pairs_to_list ps))"
  shows "(red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
define fs where "fs = snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))"
[PROOF STATE]
proof (state)
this:
fs = snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))

goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
have "set (pdata_pairs_to_list ps) \<subseteq> set fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (pdata_pairs_to_list ps) \<subseteq> set fs
[PROOF STEP]
unfolding fs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (pdata_pairs_to_list ps) \<subseteq> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))
[PROOF STEP]
by (fact snd_sym_preproc_superset)
[PROOF STATE]
proof (state)
this:
set (pdata_pairs_to_list ps) \<subseteq> set fs

goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
hence "phull (set (pdata_pairs_to_list ps)) \<subseteq> phull (set fs)"
[PROOF STATE]
proof (prove)
using this:
set (pdata_pairs_to_list ps) \<subseteq> set fs

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

goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
f \<in> phull (set (pdata_pairs_to_list ps))
phull (set (pdata_pairs_to_list ps)) \<subseteq> phull (set fs)
[PROOF STEP]
have f_in: "f \<in> phull (set fs)"
[PROOF STATE]
proof (prove)
using this:
f \<in> phull (set (pdata_pairs_to_list ps))
phull (set (pdata_pairs_to_list ps)) \<subseteq> phull (set fs)

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

goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
have eq: "(set fs) \<union> set (f4_red_aux bs ps) = (set fs) \<union> set (Macaulay_red (Keys_to_list fs) fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set fs \<union> set (f4_red_aux bs ps) = set fs \<union> set (Macaulay_red (Keys_to_list fs) fs)
[PROOF STEP]
by (simp add: f4_red_aux_def fs_def Let_def fst_sym_preproc)
[PROOF STATE]
proof (state)
this:
set fs \<union> set (f4_red_aux bs ps) = set fs \<union> set (Macaulay_red (Keys_to_list fs) fs)

goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
have "(lin_red ((set fs) \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
by (simp only: eq, rule Macaulay_red_reducible, fact f_in, fact subset_refl, fact refl)
[PROOF STATE]
proof (state)
this:
(lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0

goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0

goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f f
 2. \<And>y z. \<lbrakk>(lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y; lin_red (set fs \<union> set (f4_red_aux bs ps)) y z; (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y\<rbrakk> \<Longrightarrow> (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f z
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f f
 2. \<And>y z. \<lbrakk>(lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y; lin_red (set fs \<union> set (f4_red_aux bs ps)) y z; (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y\<rbrakk> \<Longrightarrow> (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f f
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f f

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y; lin_red (set fs \<union> set (f4_red_aux bs ps)) y z; (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y\<rbrakk> \<Longrightarrow> (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y; lin_red (set fs \<union> set (f4_red_aux bs ps)) y z; (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y\<rbrakk> \<Longrightarrow> (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f z
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
(lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y
lin_red (set fs \<union> set (f4_red_aux bs ps)) y z
(red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y; lin_red (set fs \<union> set (f4_red_aux bs ps)) y z; (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y\<rbrakk> \<Longrightarrow> (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f z
[PROOF STEP]
from step(2)
[PROOF STATE]
proof (chain)
picking this:
lin_red (set fs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
have "red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z"
[PROOF STATE]
proof (prove)
using this:
lin_red (set fs \<union> set (f4_red_aux bs ps)) y z

goal (1 subgoal):
 1. red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
unfolding lin_red_Un
[PROOF STATE]
proof (prove)
using this:
lin_red (set fs) y z \<or> lin_red (set (f4_red_aux bs ps)) y z

goal (1 subgoal):
 1. red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lin_red (set fs) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
 2. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
assume "lin_red (set fs) y z"
[PROOF STATE]
proof (state)
this:
lin_red (set fs) y z

goal (2 subgoals):
 1. lin_red (set fs) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
 2. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lin_red (set fs) y z
[PROOF STEP]
obtain a where "a \<in> set fs" and r: "red_single y z a 0"
[PROOF STATE]
proof (prove)
using this:
lin_red (set fs) y z

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> set fs; red_single y z a (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule lin_redE)
[PROOF STATE]
proof (state)
this:
a \<in> set fs
red_single y z a (0::'a)

goal (2 subgoals):
 1. lin_red (set fs) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
 2. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
a \<in> set fs
[PROOF STEP]
obtain b c t where "b \<in> fst ` set bs" and a: "a = monom_mult c t b"
[PROOF STATE]
proof (prove)
using this:
a \<in> set fs

goal (1 subgoal):
 1. (\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding fs_def
[PROOF STATE]
proof (prove)
using this:
a \<in> set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))

goal (1 subgoal):
 1. (\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule in_snd_sym_preprocE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; a \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume *: "\<And>b c t. b \<in> fst ` set bs \<Longrightarrow> a = monom_mult c t b \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<lbrakk>?b103 \<in> fst ` set bs; a = monom_mult ?c103 ?t103 ?b103\<rbrakk> \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; a \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "a \<in> set (pdata_pairs_to_list ps)"
[PROOF STATE]
proof (state)
this:
a \<in> set (pdata_pairs_to_list ps)

goal (2 subgoals):
 1. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; a \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set (pdata_pairs_to_list ps)
[PROOF STEP]
obtain f g where "(f, g) \<in> set ps \<or> (g, f) \<in> set ps"
          and a: "a = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
[PROOF STATE]
proof (prove)
using this:
a \<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; a = 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 in_pdata_pairs_to_listE)
[PROOF STATE]
proof (state)
this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps
a = monom_mult ((1::'b) / lc (fst f)) (lcs (lp (fst f)) (lp (fst g)) - lp (fst f)) (fst f)

goal (2 subgoals):
 1. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; a \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<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 \<in> fst ` set ps \<union> snd ` set ps"
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> set ps \<or> (g, f) \<in> set ps

goal (1 subgoal):
 1. f \<in> fst ` set ps \<union> snd ` set ps
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f \<in> fst ` set ps \<union> snd ` set ps

goal (2 subgoals):
 1. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; a \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
set ps \<subseteq> set bs \<times> set bs
f \<in> fst ` set ps \<union> snd ` set ps
[PROOF STEP]
have "f \<in> set bs"
[PROOF STATE]
proof (prove)
using this:
set ps \<subseteq> set bs \<times> set bs
f \<in> fst ` set ps \<union> snd ` set ps

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

goal (2 subgoals):
 1. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; a \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "fst f \<in> fst ` set bs"
[PROOF STATE]
proof (prove)
using this:
f \<in> set bs

goal (1 subgoal):
 1. fst f \<in> fst ` set bs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst f \<in> fst ` set bs

goal (2 subgoals):
 1. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; a \<in> set (pdata_pairs_to_list ps)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from this a
[PROOF STATE]
proof (chain)
picking this:
fst f \<in> fst ` set bs
a = 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:
fst f \<in> fst ` set bs
a = 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 *)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix g s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume *: "\<And>b c t. b \<in> fst ` set bs \<Longrightarrow> a = monom_mult c t b \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<lbrakk>?b103 \<in> fst ` set bs; a = monom_mult ?c103 ?t103 ?b103\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "g \<in> set (map fst bs)"
[PROOF STATE]
proof (state)
this:
g \<in> set (map fst bs)

goal (1 subgoal):
 1. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "g \<in> fst ` set bs"
[PROOF STATE]
proof (prove)
using this:
g \<in> set (map fst bs)

goal (1 subgoal):
 1. g \<in> fst ` set bs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g \<in> fst ` set bs

goal (1 subgoal):
 1. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g \<in> fst ` set bs

goal (1 subgoal):
 1. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "a = monom_mult 1 s g"
[PROOF STATE]
proof (state)
this:
a = monom_mult (1::'b) s g

goal (1 subgoal):
 1. \<And>g t. \<lbrakk>\<And>b c t. \<lbrakk>b \<in> fst ` set bs; a = monom_mult c t b\<rbrakk> \<Longrightarrow> thesis; g \<in> set (map fst bs); a = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g \<in> fst ` set bs
a = monom_mult (1::'b) s g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g \<in> fst ` set bs
a = monom_mult (1::'b) s g

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:
b \<in> fst ` set bs
a = monom_mult c t b

goal (2 subgoals):
 1. lin_red (set fs) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
 2. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
from r
[PROOF STATE]
proof (chain)
picking this:
red_single y z a (0::'a)
[PROOF STEP]
have "c \<noteq> 0" and "b \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
red_single y z a (0::'a)

goal (1 subgoal):
 1. c \<noteq> (0::'b) &&& b \<noteq> 0
[PROOF STEP]
by (simp_all add: a red_single_def monom_mult_eq_zero_iff)
[PROOF STATE]
proof (state)
this:
c \<noteq> (0::'b)
b \<noteq> 0

goal (2 subgoals):
 1. lin_red (set fs) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
 2. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
from r
[PROOF STATE]
proof (chain)
picking this:
red_single y z a (0::'a)
[PROOF STEP]
have "red_single y z b t"
[PROOF STATE]
proof (prove)
using this:
red_single y z a (0::'a)

goal (1 subgoal):
 1. red_single y z b t
[PROOF STEP]
by (simp add: a red_single_def monom_mult_eq_zero_iff lt_monom_mult[OF \<open>c \<noteq> 0\<close> \<open>b \<noteq> 0\<close>]
                      monom_mult_assoc term_simps)
[PROOF STATE]
proof (state)
this:
red_single y z b t

goal (2 subgoals):
 1. lin_red (set fs) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
 2. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
with \<open>b \<in> fst ` set bs\<close>
[PROOF STATE]
proof (chain)
picking this:
b \<in> fst ` set bs
red_single y z b t
[PROOF STEP]
have "red (fst ` set bs) y z"
[PROOF STATE]
proof (prove)
using this:
b \<in> fst ` set bs
red_single y z b t

goal (1 subgoal):
 1. red (fst ` set bs) y z
[PROOF STEP]
by (rule red_setI)
[PROOF STATE]
proof (state)
this:
red (fst ` set bs) y z

goal (2 subgoals):
 1. lin_red (set fs) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
 2. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
red (fst ` set bs) y z

goal (1 subgoal):
 1. red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
by (rule red_unionI1)
[PROOF STATE]
proof (state)
this:
red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z

goal (1 subgoal):
 1. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
assume "lin_red (set (f4_red_aux bs ps)) y z"
[PROOF STATE]
proof (state)
this:
lin_red (set (f4_red_aux bs ps)) y z

goal (1 subgoal):
 1. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
hence "red (set (f4_red_aux bs ps)) y z"
[PROOF STATE]
proof (prove)
using this:
lin_red (set (f4_red_aux bs ps)) y z

goal (1 subgoal):
 1. red (set (f4_red_aux bs ps)) y z
[PROOF STEP]
by (rule lin_red_imp_red)
[PROOF STATE]
proof (state)
this:
red (set (f4_red_aux bs ps)) y z

goal (1 subgoal):
 1. lin_red (set (f4_red_aux bs ps)) y z \<Longrightarrow> red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
red (set (f4_red_aux bs ps)) y z

goal (1 subgoal):
 1. red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
by (rule red_unionI2)
[PROOF STATE]
proof (state)
this:
red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(lin_red (set fs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y; lin_red (set fs \<union> set (f4_red_aux bs ps)) y z; (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y\<rbrakk> \<Longrightarrow> (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f z
[PROOF STEP]
with step(3)
[PROOF STATE]
proof (chain)
picking this:
(red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y
red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f y
red (fst ` set bs \<union> set (f4_red_aux bs ps)) y z

goal (1 subgoal):
 1. (red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f z
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(red (fst ` set bs \<union> set (f4_red_aux bs ps)))\<^sup>*\<^sup>* f 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fst_set_fst_f4_red: "fst ` set (fst (f4_red gs bs ps sps data)) = set (f4_red_aux (gs @ bs) sps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` set (fst (f4_red gs bs ps sps data)) = set (f4_red_aux (gs @ bs) sps)
[PROOF STEP]
by (simp add: f4_red_def, force)