[STATEMENT]
lemma components_snd_sym_preproc_aux_subset:
  assumes "set vs \<subseteq> Keys (set (fs::('t \<Rightarrow>\<^sub>0 'b::semiring_1_no_zero_divisors) list))"
  shows "component_of_term ` Keys (set (snd (sym_preproc_aux gs ks (vs, fs)))) \<subseteq>
          component_of_term ` Keys (set gs \<union> set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_aux gs ks (vs, fs)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> Keys (set fs)

goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_aux gs ks (vs, fs)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
proof (induct fs rule: sym_preproc_aux_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ks fs. set [] \<subseteq> Keys (set fs) \<Longrightarrow> component_of_term ` Keys (set (snd (ks, fs))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
 2. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
case (base ks fs)
[PROOF STATE]
proof (state)
this:
set [] \<subseteq> Keys (set fs)

goal (2 subgoals):
 1. \<And>ks fs. set [] \<subseteq> Keys (set fs) \<Longrightarrow> component_of_term ` Keys (set (snd (ks, fs))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
 2. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (ks, fs))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
by (simp add: Keys_Un image_Un)
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (snd (ks, fs))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
case (rec ks vs fs v vs')
[PROOF STATE]
proof (state)
this:
vs \<noteq> []
v = ord_term_lin.Max (set vs)
vs' = removeAll v vs
set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v)))
set vs \<subseteq> Keys (set fs)

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
let ?n = "sym_preproc_addnew gs vs' fs v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
from rec(1)
[PROOF STATE]
proof (chain)
picking this:
vs \<noteq> []
[PROOF STEP]
have "v \<in> set vs"
[PROOF STATE]
proof (prove)
using this:
vs \<noteq> []

goal (1 subgoal):
 1. v \<in> set vs
[PROOF STEP]
by (simp add: rec(2))
[PROOF STATE]
proof (state)
this:
v \<in> set vs

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
hence set_vs: "insert v (set vs') = set vs"
[PROOF STATE]
proof (prove)
using this:
v \<in> set vs

goal (1 subgoal):
 1. insert v (set vs') = set vs
[PROOF STEP]
by (auto simp add: rec(3))
[PROOF STATE]
proof (state)
this:
insert v (set vs') = set vs

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
from rec(5)
[PROOF STATE]
proof (chain)
picking this:
set vs \<subseteq> Keys (set fs)
[PROOF STEP]
have eq: "Keys (set fs) \<union> (Keys (set gs) \<union> set vs) = Keys (set gs) \<union> Keys (set fs)"
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> Keys (set fs)

goal (1 subgoal):
 1. Keys (set fs) \<union> (Keys (set gs) \<union> set vs) = Keys (set gs) \<union> Keys (set fs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Keys (set fs) \<union> (Keys (set gs) \<union> set vs) = Keys (set gs) \<union> Keys (set fs)

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
have "component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) ?n))) \<subseteq>
                        component_of_term ` Keys (set gs \<union> set (snd ?n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
proof (rule rec(4))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
have "set (fst ?n) \<subseteq> Keys (set (snd ?n)) \<union> insert v (set vs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> insert v (set vs')
[PROOF STEP]
by (simp only: Keys_snd_sym_preproc_addnew, blast)
[PROOF STATE]
proof (state)
this:
set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> insert v (set vs')

goal (1 subgoal):
 1. set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> insert v (set vs')

goal (1 subgoal):
 1. set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
have "... = Keys (set (snd ?n)) \<union> (set vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> insert v (set vs') = Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs
[PROOF STEP]
by (simp only: set_vs)
[PROOF STATE]
proof (state)
this:
Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> insert v (set vs') = Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs

goal (1 subgoal):
 1. set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> insert v (set vs') = Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs

goal (1 subgoal):
 1. set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
have "... \<subseteq> Keys (set (snd ?n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
assume "u \<in> set vs"
[PROOF STATE]
proof (state)
this:
u \<in> set vs

goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
with rec(5)
[PROOF STATE]
proof (chain)
picking this:
set vs \<subseteq> Keys (set fs)
u \<in> set vs
[PROOF STEP]
have "u \<in> Keys (set fs)"
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> Keys (set fs)
u \<in> set vs

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

goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> Keys (set fs)
[PROOF STEP]
obtain f where "f \<in> set fs" and "u \<in> keys f"
[PROOF STATE]
proof (prove)
using this:
u \<in> Keys (set fs)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> set fs; u \<in> keys f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule in_KeysE)
[PROOF STATE]
proof (state)
this:
f \<in> set fs
u \<in> keys f

goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
from this(1) snd_sym_preproc_addnew_superset
[PROOF STATE]
proof (chain)
picking this:
f \<in> set fs
set ?fs \<subseteq> set (snd (sym_preproc_addnew ?gs ?vs ?fs ?v))
[PROOF STEP]
have "f \<in> set (snd ?n)"
[PROOF STATE]
proof (prove)
using this:
f \<in> set fs
set ?fs \<subseteq> set (snd (sym_preproc_addnew ?gs ?vs ?fs ?v))

goal (1 subgoal):
 1. f \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
f \<in> set (snd (sym_preproc_addnew gs vs' fs v))

goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
with \<open>u \<in> keys f\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> keys f
f \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
have "u \<in> Keys (set (snd ?n))"
[PROOF STATE]
proof (prove)
using this:
u \<in> keys f
f \<in> set (snd (sym_preproc_addnew gs vs' fs v))

goal (1 subgoal):
 1. u \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
by (rule in_KeysI)
[PROOF STATE]
proof (state)
this:
u \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?u102 \<in> set vs \<Longrightarrow> ?u102 \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?u102 \<in> set vs \<Longrightarrow> ?u102 \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> set vs \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
show "set (fst ?n) \<subseteq> Keys (set (snd ?n))"
[PROOF STATE]
proof (prove)
using this:
set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
have "... \<subseteq> component_of_term ` Keys (set gs \<union> set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
proof (simp only: image_Un Keys_Un Un_subset_iff, rule, fact Un_upper1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set gs) \<union> component_of_term ` Keys (set fs)
[PROOF STEP]
have "component_of_term ` Keys (set (snd ?n)) \<subseteq> component_of_term ` (Keys (set fs) \<union> insert v (set (fst ?n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` (Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v))))
[PROOF STEP]
by (auto simp only: Keys_snd_sym_preproc_addnew[symmetric])
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` (Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v))))

goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set gs) \<union> component_of_term ` Keys (set fs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` (Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v))))

goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set gs) \<union> component_of_term ` Keys (set fs)
[PROOF STEP]
have "... \<subseteq> component_of_term ` Keys (set fs) \<union> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` (Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set fs) \<union> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))
[PROOF STEP]
proof (simp only: Un_subset_iff image_Un, rule, fact Un_upper1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. component_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))
[PROOF STEP]
have "component_of_term ` {v} \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` {v} \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
component_of_term ` {v} \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))

goal (1 subgoal):
 1. component_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
component_of_term ` {v} \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))

goal (1 subgoal):
 1. component_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))
[PROOF STEP]
have "component_of_term ` set (fst ?n) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))
[PROOF STEP]
by (rule components_fst_sym_preproc_addnew_subset)
[PROOF STATE]
proof (state)
this:
component_of_term ` set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))

goal (1 subgoal):
 1. component_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
component_of_term ` {v} \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))
component_of_term ` set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))
[PROOF STEP]
have "component_of_term ` ({v} \<union> set (fst ?n)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))"
[PROOF STATE]
proof (prove)
using this:
component_of_term ` {v} \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))
component_of_term ` set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))

goal (1 subgoal):
 1. component_of_term ` ({v} \<union> set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))
[PROOF STEP]
by (simp only: Un_subset_iff image_Un)
[PROOF STATE]
proof (state)
this:
component_of_term ` ({v} \<union> set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))

goal (1 subgoal):
 1. component_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
component_of_term ` ({v} \<union> set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))

goal (1 subgoal):
 1. component_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))
[PROOF STEP]
have "component_of_term ` (Keys (set gs) \<union> insert v (set vs')) \<subseteq>
                          component_of_term ` (Keys (set fs) \<union> (Keys (set gs) \<union> insert v (set vs')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` (Keys (set gs) \<union> insert v (set vs')) \<subseteq> component_of_term ` (Keys (set fs) \<union> (Keys (set gs) \<union> insert v (set vs')))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
component_of_term ` (Keys (set gs) \<union> insert v (set vs')) \<subseteq> component_of_term ` (Keys (set fs) \<union> (Keys (set gs) \<union> insert v (set vs')))

goal (1 subgoal):
 1. component_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
component_of_term ` ({v} \<union> set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` (Keys (set fs) \<union> (Keys (set gs) \<union> insert v (set vs')))
[PROOF STEP]
show "component_of_term ` insert v (set (fst ?n)) \<subseteq>
                        component_of_term ` Keys (set fs) \<union>
                        (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))"
[PROOF STATE]
proof (prove)
using this:
component_of_term ` ({v} \<union> set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` (Keys (set fs) \<union> (Keys (set gs) \<union> insert v (set vs')))

goal (1 subgoal):
 1. component_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))
[PROOF STEP]
by (simp add: image_Un)
[PROOF STATE]
proof (state)
this:
component_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> (component_of_term ` Keys (set gs) \<union> component_of_term ` insert v (set vs'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
component_of_term ` (Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set fs) \<union> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))

goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set gs) \<union> component_of_term ` Keys (set fs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))
[PROOF STEP]
show "component_of_term ` Keys (set (snd ?n)) \<subseteq>
                    component_of_term ` Keys (set gs) \<union> component_of_term ` Keys (set fs)"
[PROOF STATE]
proof (prove)
using this:
component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set fs) \<union> component_of_term ` (Keys (set gs) \<union> insert v (set vs'))

goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set gs) \<union> component_of_term ` Keys (set fs)
[PROOF STEP]
by (simp only: set_vs eq, metis eq image_Un)
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set gs) \<union> component_of_term ` Keys (set fs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; set (fst (sym_preproc_addnew gs vs' fs v)) \<subseteq> Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set (snd (sym_preproc_addnew gs vs' fs v))); set vs \<subseteq> Keys (set fs)\<rbrakk> \<Longrightarrow> component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)

goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma snd_sym_preproc_aux_complete:
  assumes "\<And>u' g'. u' \<in> Keys (set fs) \<Longrightarrow> u' \<notin> set vs \<Longrightarrow> g' \<in> set gs \<Longrightarrow> lt g' adds\<^sub>t u' \<Longrightarrow>
            monom_mult 1 (pp_of_term u' - lp g') g' \<in> set fs"
  assumes "u \<in> Keys (set (snd (sym_preproc_aux gs ks (vs, fs))))" and "g \<in> set gs" and "lt g adds\<^sub>t u"
  shows "monom_mult (1::'b::semiring_1_no_zero_divisors) (pp_of_term u - lp g) g \<in>
          set (snd (sym_preproc_aux gs ks (vs, fs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs ks (vs, fs)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u'100 \<in> Keys (set fs); ?u'100 \<notin> set vs; ?g'100 \<in> set gs; lt ?g'100 adds\<^sub>t ?u'100\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term ?u'100 - lp ?g'100) ?g'100 \<in> set fs
u \<in> Keys (set (snd (sym_preproc_aux gs ks (vs, fs))))
g \<in> set gs
lt g adds\<^sub>t u

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs ks (vs, fs)))
[PROOF STEP]
proof (induct fs rule: sym_preproc_aux_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ks fs. \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set []; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (ks, fs))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (ks, fs))
 2. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
case (base ks fs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?u'100 \<in> Keys (set fs); ?u'100 \<notin> set []; ?g'100 \<in> set gs; lt ?g'100 adds\<^sub>t ?u'100\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term ?u'100 - lp ?g'100) ?g'100 \<in> set fs
u \<in> Keys (set (snd (ks, fs)))
g \<in> set gs
lt g adds\<^sub>t u

goal (2 subgoals):
 1. \<And>ks fs. \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set []; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (ks, fs))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (ks, fs))
 2. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
from base(2)
[PROOF STATE]
proof (chain)
picking this:
u \<in> Keys (set (snd (ks, fs)))
[PROOF STEP]
have "u \<in> Keys (set fs)"
[PROOF STATE]
proof (prove)
using this:
u \<in> Keys (set (snd (ks, fs)))

goal (1 subgoal):
 1. u \<in> Keys (set fs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<in> Keys (set fs)

goal (2 subgoals):
 1. \<And>ks fs. \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set []; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (ks, fs))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (ks, fs))
 2. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
from this _ base(3, 4)
[PROOF STATE]
proof (chain)
picking this:
u \<in> Keys (set fs)
PROP ?psi \<Longrightarrow> PROP ?psi
g \<in> set gs
lt g adds\<^sub>t u
[PROOF STEP]
have "monom_mult 1 (pp_of_term u - lp g) g \<in> set fs"
[PROOF STATE]
proof (prove)
using this:
u \<in> Keys (set fs)
PROP ?psi \<Longrightarrow> PROP ?psi
g \<in> set gs
lt g adds\<^sub>t u

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set fs
[PROOF STEP]
proof (rule base(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<notin> set []
[PROOF STEP]
show "u \<notin> set []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<notin> set []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<notin> set []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set fs

goal (2 subgoals):
 1. \<And>ks fs. \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set []; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (ks, fs))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (ks, fs))
 2. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set fs

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (ks, fs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (ks, fs))

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
case (rec ks vs fs v vs')
[PROOF STATE]
proof (state)
this:
vs \<noteq> []
v = ord_term_lin.Max (set vs)
vs' = removeAll v vs
\<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
\<lbrakk>?u'100 \<in> Keys (set fs); ?u'100 \<notin> set vs; ?g'100 \<in> set gs; lt ?g'100 adds\<^sub>t ?u'100\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term ?u'100 - lp ?g'100) ?g'100 \<in> set fs
u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))))
g \<in> set gs
lt g adds\<^sub>t u

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
from rec(1)
[PROOF STATE]
proof (chain)
picking this:
vs \<noteq> []
[PROOF STEP]
have "v \<in> set vs"
[PROOF STATE]
proof (prove)
using this:
vs \<noteq> []

goal (1 subgoal):
 1. v \<in> set vs
[PROOF STEP]
by (simp add: rec(2))
[PROOF STATE]
proof (state)
this:
v \<in> set vs

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
hence set_ts: "set vs = insert v (set vs')"
[PROOF STATE]
proof (prove)
using this:
v \<in> set vs

goal (1 subgoal):
 1. set vs = insert v (set vs')
[PROOF STEP]
by (auto simp add: rec(3))
[PROOF STATE]
proof (state)
this:
set vs = insert v (set vs')

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
let ?n = "sym_preproc_addnew gs vs' fs v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>\<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v)); u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set vs; g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs; u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); g \<in> set gs; lt g adds\<^sub>t u\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
from _ rec(6, 7, 8)
[PROOF STATE]
proof (chain)
picking this:
PROP ?psi \<Longrightarrow> PROP ?psi
u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))))
g \<in> set gs
lt g adds\<^sub>t u
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
u \<in> Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))))
g \<in> set gs
lt g adds\<^sub>t u

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
proof (rule rec(4))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
fix v' g'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
assume "v' \<in> Keys (set (snd ?n))" and "v' \<notin> set (fst ?n)" and "g' \<in> set gs" and "lt g' adds\<^sub>t v'"
[PROOF STATE]
proof (state)
this:
v' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
v' \<notin> set (fst (sym_preproc_addnew gs vs' fs v))
g' \<in> set gs
lt g' adds\<^sub>t v'

goal (1 subgoal):
 1. \<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
from this(1) Keys_snd_sym_preproc_addnew
[PROOF STATE]
proof (chain)
picking this:
v' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
Keys (set (snd (sym_preproc_addnew ?gs ?vs ?fs ?v))) \<union> insert ?v (set ?vs) = Keys (set ?fs) \<union> insert ?v (set (fst (sym_preproc_addnew ?gs ?vs ?fs ?v)))
[PROOF STEP]
have "v' \<in> Keys (set fs) \<union> insert v (set (fst ?n))"
[PROOF STATE]
proof (prove)
using this:
v' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v)))
Keys (set (snd (sym_preproc_addnew ?gs ?vs ?fs ?v))) \<union> insert ?v (set ?vs) = Keys (set ?fs) \<union> insert ?v (set (fst (sym_preproc_addnew ?gs ?vs ?fs ?v)))

goal (1 subgoal):
 1. v' \<in> Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v' \<in> Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. \<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
with \<open>v' \<notin> set (fst ?n)\<close>
[PROOF STATE]
proof (chain)
picking this:
v' \<notin> set (fst (sym_preproc_addnew gs vs' fs v))
v' \<in> Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
have disj: "v' \<in> Keys (set fs) \<or> v' = v"
[PROOF STATE]
proof (prove)
using this:
v' \<notin> set (fst (sym_preproc_addnew gs vs' fs v))
v' \<in> Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. v' \<in> Keys (set fs) \<or> v' = v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v' \<in> Keys (set fs) \<or> v' = v

goal (1 subgoal):
 1. \<And>u' g'. \<lbrakk>u' \<in> Keys (set (snd (sym_preproc_addnew gs vs' fs v))); u' \<notin> set (fst (sym_preproc_addnew gs vs' fs v)); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
show "monom_mult 1 (pp_of_term v' - lp g') g' \<in> set (snd ?n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
proof (cases "v' = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v' = v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
 2. v' \<noteq> v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v' = v

goal (2 subgoals):
 1. v' = v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
 2. v' \<noteq> v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
from \<open>g' \<in> set gs\<close> \<open>lt g' adds\<^sub>t v'\<close>
[PROOF STATE]
proof (chain)
picking this:
g' \<in> set gs
lt g' adds\<^sub>t v'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g' \<in> set gs
lt g' adds\<^sub>t v'

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
using this:
g' \<in> set gs
lt g' adds\<^sub>t v

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
by (rule sym_preproc_addnew_complete)
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))

goal (1 subgoal):
 1. v' \<noteq> v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v' \<noteq> v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v' \<noteq> v

goal (1 subgoal):
 1. v' \<noteq> v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
with disj
[PROOF STATE]
proof (chain)
picking this:
v' \<in> Keys (set fs) \<or> v' = v
v' \<noteq> v
[PROOF STEP]
have "v' \<in> Keys (set fs)"
[PROOF STATE]
proof (prove)
using this:
v' \<in> Keys (set fs) \<or> v' = v
v' \<noteq> v

goal (1 subgoal):
 1. v' \<in> Keys (set fs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v' \<in> Keys (set fs)

goal (1 subgoal):
 1. v' \<noteq> v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v' \<in> Keys (set fs)

goal (1 subgoal):
 1. v' \<noteq> v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
have "v' \<notin> set vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<notin> set vs
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v' \<in> set vs \<Longrightarrow> False
[PROOF STEP]
assume "v' \<in> set vs"
[PROOF STATE]
proof (state)
this:
v' \<in> set vs

goal (1 subgoal):
 1. v' \<in> set vs \<Longrightarrow> False
[PROOF STEP]
hence "v' \<in> set vs'"
[PROOF STATE]
proof (prove)
using this:
v' \<in> set vs

goal (1 subgoal):
 1. v' \<in> set vs'
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
v' \<in> set vs
v' \<noteq> v

goal (1 subgoal):
 1. v' \<in> set vs'
[PROOF STEP]
by (simp add: rec(3))
[PROOF STATE]
proof (state)
this:
v' \<in> set vs'

goal (1 subgoal):
 1. v' \<in> set vs \<Longrightarrow> False
[PROOF STEP]
with fst_sym_preproc_addnew_superset
[PROOF STATE]
proof (chain)
picking this:
set ?vs \<subseteq> set (fst (sym_preproc_addnew ?gs ?vs ?fs ?v))
v' \<in> set vs'
[PROOF STEP]
have "v' \<in> set (fst ?n)"
[PROOF STATE]
proof (prove)
using this:
set ?vs \<subseteq> set (fst (sym_preproc_addnew ?gs ?vs ?fs ?v))
v' \<in> set vs'

goal (1 subgoal):
 1. v' \<in> set (fst (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
v' \<in> set (fst (sym_preproc_addnew gs vs' fs v))

goal (1 subgoal):
 1. v' \<in> set vs \<Longrightarrow> False
[PROOF STEP]
with \<open>v' \<notin> set (fst ?n)\<close>
[PROOF STATE]
proof (chain)
picking this:
v' \<notin> set (fst (sym_preproc_addnew gs vs' fs v))
v' \<in> set (fst (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
v' \<notin> set (fst (sym_preproc_addnew gs vs' fs v))
v' \<in> set (fst (sym_preproc_addnew gs vs' fs v))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v' \<notin> set vs

goal (1 subgoal):
 1. v' \<noteq> v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v' \<in> Keys (set fs)
v' \<notin> set vs
[PROOF STEP]
have "monom_mult 1 (pp_of_term v' - lp g') g' \<in> set fs"
[PROOF STATE]
proof (prove)
using this:
v' \<in> Keys (set fs)
v' \<notin> set vs

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set fs
[PROOF STEP]
using \<open>g' \<in> set gs\<close> \<open>lt g' adds\<^sub>t v'\<close>
[PROOF STATE]
proof (prove)
using this:
v' \<in> Keys (set fs)
v' \<notin> set vs
g' \<in> set gs
lt g' adds\<^sub>t v'

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set fs
[PROOF STEP]
by (rule rec(5))
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set fs

goal (1 subgoal):
 1. v' \<noteq> v \<Longrightarrow> monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
with snd_sym_preproc_addnew_superset
[PROOF STATE]
proof (chain)
picking this:
set ?fs \<subseteq> set (snd (sym_preproc_addnew ?gs ?vs ?fs ?v))
monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set fs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set ?fs \<subseteq> set (snd (sym_preproc_addnew ?gs ?vs ?fs ?v))
monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set fs

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (pp_of_term v' - lp g') g' \<in> set (snd (sym_preproc_addnew gs vs' fs v))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (pp_of_term u - lp g) g \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sym_preproc_Nil [simp]: "sym_preproc gs [] = ([], [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym_preproc gs [] = ([], [])
[PROOF STEP]
by (simp add: sym_preproc_def)


[STATEMENT]
lemma fst_sym_preproc:
  "fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs (fs::('t \<Rightarrow>\<^sub>0 'b::semiring_1_no_zero_divisors) list)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
let ?a = "fst (sym_preproc gs fs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
let ?b = "Keys_to_list (snd (sym_preproc gs fs))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
have "antisymp (\<succ>\<^sub>t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antisymp (\<succ>\<^sub>t)
[PROOF STEP]
unfolding antisymp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x \<succ>\<^sub>t y \<longrightarrow> y \<succ>\<^sub>t x \<longrightarrow> x = y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
antisymp (\<succ>\<^sub>t)

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
have "irreflp (\<succ>\<^sub>t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreflp (\<succ>\<^sub>t)
[PROOF STEP]
by (simp add: irreflp_def)
[PROOF STATE]
proof (state)
this:
irreflp (\<succ>\<^sub>t)

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
irreflp (\<succ>\<^sub>t)

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
have "transp (\<succ>\<^sub>t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transp (\<succ>\<^sub>t)
[PROOF STEP]
unfolding transp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y z. x \<succ>\<^sub>t y \<longrightarrow> y \<succ>\<^sub>t z \<longrightarrow> x \<succ>\<^sub>t z
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
transp (\<succ>\<^sub>t)

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
transp (\<succ>\<^sub>t)

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
have s1: "sorted_wrt (\<succ>\<^sub>t) ?a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc gs fs))
[PROOF STEP]
unfolding sym_preproc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs [] (Keys_to_list fs, fs)))
[PROOF STEP]
by (rule fst_sym_preproc_aux_sorted_wrt, simp_all)
[PROOF STATE]
proof (state)
this:
sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc gs fs))

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
irreflp (\<succ>\<^sub>t)
transp (\<succ>\<^sub>t)
sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc gs fs))
[PROOF STEP]
have d1: "distinct ?a"
[PROOF STATE]
proof (prove)
using this:
irreflp (\<succ>\<^sub>t)
transp (\<succ>\<^sub>t)
sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc gs fs))

goal (1 subgoal):
 1. distinct (fst (sym_preproc gs fs))
[PROOF STEP]
by (rule distinct_sorted_wrt_irrefl)
[PROOF STATE]
proof (state)
this:
distinct (fst (sym_preproc gs fs))

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
have s2: "sorted_wrt (\<succ>\<^sub>t) ?b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (\<succ>\<^sub>t) (Keys_to_list (snd (sym_preproc gs fs)))
[PROOF STEP]
by (fact Keys_to_list_sorted_wrt)
[PROOF STATE]
proof (state)
this:
sorted_wrt (\<succ>\<^sub>t) (Keys_to_list (snd (sym_preproc gs fs)))

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
with \<open>irreflp (\<succ>\<^sub>t)\<close> \<open>transp (\<succ>\<^sub>t)\<close>
[PROOF STATE]
proof (chain)
picking this:
irreflp (\<succ>\<^sub>t)
transp (\<succ>\<^sub>t)
sorted_wrt (\<succ>\<^sub>t) (Keys_to_list (snd (sym_preproc gs fs)))
[PROOF STEP]
have d2: "distinct ?b"
[PROOF STATE]
proof (prove)
using this:
irreflp (\<succ>\<^sub>t)
transp (\<succ>\<^sub>t)
sorted_wrt (\<succ>\<^sub>t) (Keys_to_list (snd (sym_preproc gs fs)))

goal (1 subgoal):
 1. distinct (Keys_to_list (snd (sym_preproc gs fs)))
[PROOF STEP]
by (rule distinct_sorted_wrt_irrefl)
[PROOF STATE]
proof (state)
this:
distinct (Keys_to_list (snd (sym_preproc gs fs)))

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
from \<open>antisymp (\<succ>\<^sub>t)\<close> s1 d1 s2 d2
[PROOF STATE]
proof (chain)
picking this:
antisymp (\<succ>\<^sub>t)
sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc gs fs))
distinct (fst (sym_preproc gs fs))
sorted_wrt (\<succ>\<^sub>t) (Keys_to_list (snd (sym_preproc gs fs)))
distinct (Keys_to_list (snd (sym_preproc gs fs)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
antisymp (\<succ>\<^sub>t)
sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc gs fs))
distinct (fst (sym_preproc gs fs))
sorted_wrt (\<succ>\<^sub>t) (Keys_to_list (snd (sym_preproc gs fs)))
distinct (Keys_to_list (snd (sym_preproc gs fs)))

goal (1 subgoal):
 1. fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))
[PROOF STEP]
proof (rule sorted_wrt_distinct_set_unique)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (fst (sym_preproc gs fs)) = set (Keys_to_list (snd (sym_preproc gs fs)))
[PROOF STEP]
show "set ?a = set ?b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (fst (sym_preproc gs fs)) = set (Keys_to_list (snd (sym_preproc gs fs)))
[PROOF STEP]
unfolding set_Keys_to_list sym_preproc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (fst (sym_preproc_aux gs [] (Keys_to_list fs, fs))) = Keys (set (snd (sym_preproc_aux gs [] (Keys_to_list fs, fs))))
[PROOF STEP]
by (rule fst_sym_preproc_aux_complete, simp add: set_Keys_to_list)
[PROOF STATE]
proof (state)
this:
set (fst (sym_preproc gs fs)) = set (Keys_to_list (snd (sym_preproc gs fs)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs fs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma snd_sym_preproc_superset: "set fs \<subseteq> set (snd (sym_preproc gs fs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set fs \<subseteq> set (snd (sym_preproc gs fs))
[PROOF STEP]
by (simp only: sym_preproc_def snd_conv, fact snd_sym_preproc_aux_superset)


[STATEMENT]
lemma in_snd_sym_preprocE:
  assumes "p \<in> set (snd (sym_preproc gs fs))"
  assumes 1: "p \<in> set fs \<Longrightarrow> thesis"
  assumes 2: "\<And>g t. g \<in> set gs \<Longrightarrow> p = monom_mult 1 t g \<Longrightarrow> thesis"
  shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> set (snd (sym_preproc gs fs))
p \<in> set fs \<Longrightarrow> thesis
\<lbrakk>?g101 \<in> set gs; p = monom_mult (1::'b) ?t101 ?g101\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding sym_preproc_def snd_conv
[PROOF STATE]
proof (prove)
using this:
p \<in> set (snd (sym_preproc_aux gs [] (Keys_to_list fs, fs)))
p \<in> set fs \<Longrightarrow> thesis
\<lbrakk>?g101 \<in> set gs; p = monom_mult (1::'b) ?t101 ?g101\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule in_snd_sym_preproc_auxE)


[STATEMENT]
lemma snd_sym_preproc_pmdl: "pmdl (set gs \<union> set (snd (sym_preproc gs fs))) = pmdl (set gs \<union> set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (set gs \<union> set (snd (sym_preproc gs fs))) = pmdl (set gs \<union> set fs)
[PROOF STEP]
unfolding sym_preproc_def snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (set gs \<union> set (snd (sym_preproc_aux gs [] (Keys_to_list fs, fs)))) = pmdl (set gs \<union> set fs)
[PROOF STEP]
by (fact snd_sym_preproc_aux_pmdl)


[STATEMENT]
lemma snd_sym_preproc_dgrad_set_le:
  assumes "dickson_grading d"
  shows "dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc gs fs))))
                        (pp_of_term ` Keys (set gs \<union> set (fs::('t \<Rightarrow>\<^sub>0 'b::semiring_1_no_zero_divisors) list)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc gs fs)))) (pp_of_term ` Keys (set gs \<union> set fs))
[PROOF STEP]
unfolding sym_preproc_def snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_aux gs [] (Keys_to_list fs, fs))))) (pp_of_term ` Keys (set gs \<union> set fs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dickson_grading d

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_aux gs [] (Keys_to_list fs, fs))))) (pp_of_term ` Keys (set gs \<union> set fs))
[PROOF STEP]
proof (rule snd_sym_preproc_aux_dgrad_set_le)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (Keys_to_list fs) \<subseteq> Keys (set fs)
[PROOF STEP]
show "set (Keys_to_list fs) \<subseteq> Keys (set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Keys_to_list fs) \<subseteq> Keys (set fs)
[PROOF STEP]
by (simp add: set_Keys_to_list)
[PROOF STATE]
proof (state)
this:
set (Keys_to_list fs) \<subseteq> Keys (set fs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma components_snd_sym_preproc_subset:
  "component_of_term ` Keys (set (snd (sym_preproc gs fs))) \<subseteq>
          component_of_term ` Keys (set gs \<union> set (fs::('t \<Rightarrow>\<^sub>0 'b::semiring_1_no_zero_divisors) list))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc gs fs))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
unfolding sym_preproc_def snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (snd (sym_preproc_aux gs [] (Keys_to_list fs, fs)))) \<subseteq> component_of_term ` Keys (set gs \<union> set fs)
[PROOF STEP]
by (rule components_snd_sym_preproc_aux_subset, simp add: set_Keys_to_list)


[STATEMENT]
lemma snd_sym_preproc_complete:
  assumes "v \<in> Keys (set (snd (sym_preproc gs fs)))" and "g \<in> set gs" and "lt g adds\<^sub>t v"
  shows "monom_mult (1::'b::semiring_1_no_zero_divisors) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc gs fs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc gs fs))
[PROOF STEP]
using _ assms
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
v \<in> Keys (set (snd (sym_preproc gs fs)))
g \<in> set gs
lt g adds\<^sub>t v

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc gs fs))
[PROOF STEP]
unfolding sym_preproc_def snd_conv
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
v \<in> Keys (set (snd (sym_preproc_aux gs [] (Keys_to_list fs, fs))))
g \<in> set gs
lt g adds\<^sub>t v

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_aux gs [] (Keys_to_list fs, fs)))
[PROOF STEP]
proof (rule snd_sym_preproc_aux_complete)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set (Keys_to_list fs); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs
[PROOF STEP]
fix u' and g'::"'t \<Rightarrow>\<^sub>0 'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set (Keys_to_list fs); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs
[PROOF STEP]
assume "u' \<in> Keys (set fs)" and "u' \<notin> set (Keys_to_list fs)"
[PROOF STATE]
proof (state)
this:
u' \<in> Keys (set fs)
u' \<notin> set (Keys_to_list fs)

goal (1 subgoal):
 1. \<And>u' g'. \<lbrakk>u' \<in> Keys (set fs); u' \<notin> set (Keys_to_list fs); g' \<in> set gs; lt g' adds\<^sub>t u'\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs
[PROOF STEP]
thus "monom_mult 1 (pp_of_term u' - lp g') g' \<in> set fs"
[PROOF STATE]
proof (prove)
using this:
u' \<in> Keys (set fs)
u' \<notin> set (Keys_to_list fs)

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs
[PROOF STEP]
by (simp add: set_Keys_to_list)
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (pp_of_term u' - lp g') g' \<in> set fs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lin_redI:
  assumes "f \<in> F" and "red_single p q f 0"
  shows "lin_red F p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_red F p q
[PROOF STEP]
unfolding lin_red_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f\<in>F. red_single p q f (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> F
red_single p q f (0::'a)

goal (1 subgoal):
 1. \<exists>f\<in>F. red_single p q f (0::'a)
[PROOF STEP]
..


[STATEMENT]
lemma lin_redE:
  assumes "lin_red F p q"
  obtains f::"'t \<Rightarrow>\<^sub>0 'b::field" where "f \<in> F" and "red_single p q f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> F; red_single p q f (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> F; red_single p q f (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
lin_red F p q
[PROOF STEP]
obtain f where "f \<in> F" and t: "red_single p q f 0"
[PROOF STATE]
proof (prove)
using this:
lin_red F p q

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> F; red_single p q f (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding lin_red_def
[PROOF STATE]
proof (prove)
using this:
\<exists>f\<in>F. red_single p q f (0::'a)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> F; red_single p q f (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> F
red_single p q f (0::'a)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> F; red_single p q f (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus "?thesis"
[PROOF STATE]
proof (prove)
using this:
f \<in> F
red_single p q f (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lin_red_imp_red:
  assumes "lin_red F p q"
  shows "red F p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red F p q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red F p q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
lin_red F p q
[PROOF STEP]
obtain f where "f \<in> F" and "red_single p q f 0"
[PROOF STATE]
proof (prove)
using this:
lin_red F p q

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

goal (1 subgoal):
 1. red F p q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<in> F
red_single p q f (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lin_red_Un: "lin_red (F \<union> G) p q = (lin_red F p q \<or> lin_red G p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_red (F \<union> G) p q = (lin_red F p q \<or> lin_red G p q)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lin_red (F \<union> G) p q \<Longrightarrow> lin_red F p q \<or> lin_red G p q
 2. lin_red F p q \<or> lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
assume "lin_red (F \<union> G) p q"
[PROOF STATE]
proof (state)
this:
lin_red (F \<union> G) p q

goal (2 subgoals):
 1. lin_red (F \<union> G) p q \<Longrightarrow> lin_red F p q \<or> lin_red G p q
 2. lin_red F p q \<or> lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lin_red (F \<union> G) p q
[PROOF STEP]
obtain f where "f \<in> F \<union> G" and r: "red_single p q f 0"
[PROOF STATE]
proof (prove)
using this:
lin_red (F \<union> G) p q

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> F \<union> G; red_single p q f (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule lin_redE)
[PROOF STATE]
proof (state)
this:
f \<in> F \<union> G
red_single p q f (0::'a)

goal (2 subgoals):
 1. lin_red (F \<union> G) p q \<Longrightarrow> lin_red F p q \<or> lin_red G p q
 2. lin_red F p q \<or> lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
f \<in> F \<union> G
[PROOF STEP]
show "lin_red F p q \<or> lin_red G p q"
[PROOF STATE]
proof (prove)
using this:
f \<in> F \<union> G

goal (1 subgoal):
 1. lin_red F p q \<or> lin_red G p q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<in> F \<Longrightarrow> lin_red F p q \<or> lin_red G p q
 2. f \<in> G \<Longrightarrow> lin_red F p q \<or> lin_red G p q
[PROOF STEP]
assume "f \<in> F"
[PROOF STATE]
proof (state)
this:
f \<in> F

goal (2 subgoals):
 1. f \<in> F \<Longrightarrow> lin_red F p q \<or> lin_red G p q
 2. f \<in> G \<Longrightarrow> lin_red F p q \<or> lin_red G p q
[PROOF STEP]
from this r
[PROOF STATE]
proof (chain)
picking this:
f \<in> F
red_single p q f (0::'a)
[PROOF STEP]
have "lin_red F p q"
[PROOF STATE]
proof (prove)
using this:
f \<in> F
red_single p q f (0::'a)

goal (1 subgoal):
 1. lin_red F p q
[PROOF STEP]
by (rule lin_redI)
[PROOF STATE]
proof (state)
this:
lin_red F p q

goal (2 subgoals):
 1. f \<in> F \<Longrightarrow> lin_red F p q \<or> lin_red G p q
 2. f \<in> G \<Longrightarrow> lin_red F p q \<or> lin_red G p q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
lin_red F p q

goal (1 subgoal):
 1. lin_red F p q \<or> lin_red G p q
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
lin_red F p q \<or> lin_red G p q

goal (1 subgoal):
 1. f \<in> G \<Longrightarrow> lin_red F p q \<or> lin_red G p q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> G \<Longrightarrow> lin_red F p q \<or> lin_red G p q
[PROOF STEP]
assume "f \<in> G"
[PROOF STATE]
proof (state)
this:
f \<in> G

goal (1 subgoal):
 1. f \<in> G \<Longrightarrow> lin_red F p q \<or> lin_red G p q
[PROOF STEP]
from this r
[PROOF STATE]
proof (chain)
picking this:
f \<in> G
red_single p q f (0::'a)
[PROOF STEP]
have "lin_red G p q"
[PROOF STATE]
proof (prove)
using this:
f \<in> G
red_single p q f (0::'a)

goal (1 subgoal):
 1. lin_red G p q
[PROOF STEP]
by (rule lin_redI)
[PROOF STATE]
proof (state)
this:
lin_red G p q

goal (1 subgoal):
 1. f \<in> G \<Longrightarrow> lin_red F p q \<or> lin_red G p q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
lin_red G p q

goal (1 subgoal):
 1. lin_red F p q \<or> lin_red G p q
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
lin_red F p q \<or> lin_red G p q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lin_red F p q \<or> lin_red G p q

goal (1 subgoal):
 1. lin_red F p q \<or> lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_red F p q \<or> lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
assume "lin_red F p q \<or> lin_red G p q"
[PROOF STATE]
proof (state)
this:
lin_red F p q \<or> lin_red G p q

goal (1 subgoal):
 1. lin_red F p q \<or> lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
thus "lin_red (F \<union> G) p q"
[PROOF STATE]
proof (prove)
using this:
lin_red F p q \<or> lin_red G p q

goal (1 subgoal):
 1. lin_red (F \<union> G) p q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lin_red F p q \<Longrightarrow> lin_red (F \<union> G) p q
 2. lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
assume "lin_red F p q"
[PROOF STATE]
proof (state)
this:
lin_red F p q

goal (2 subgoals):
 1. lin_red F p q \<Longrightarrow> lin_red (F \<union> G) p q
 2. lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lin_red F p q
[PROOF STEP]
obtain f where "f \<in> F" and r: "red_single p q f 0"
[PROOF STATE]
proof (prove)
using this:
lin_red F p q

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

goal (2 subgoals):
 1. lin_red F p q \<Longrightarrow> lin_red (F \<union> G) p q
 2. lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
f \<in> F
[PROOF STEP]
have "f \<in> F \<union> G"
[PROOF STATE]
proof (prove)
using this:
f \<in> F

goal (1 subgoal):
 1. f \<in> F \<union> G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<in> F \<union> G

goal (2 subgoals):
 1. lin_red F p q \<Longrightarrow> lin_red (F \<union> G) p q
 2. lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
from this r
[PROOF STATE]
proof (chain)
picking this:
f \<in> F \<union> G
red_single p q f (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<in> F \<union> G
red_single p q f (0::'a)

goal (1 subgoal):
 1. lin_red (F \<union> G) p q
[PROOF STEP]
by (rule lin_redI)
[PROOF STATE]
proof (state)
this:
lin_red (F \<union> G) p q

goal (1 subgoal):
 1. lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
assume "lin_red G p q"
[PROOF STATE]
proof (state)
this:
lin_red G p q

goal (1 subgoal):
 1. lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lin_red G p q
[PROOF STEP]
obtain g where "g \<in> G" and r: "red_single p q g 0"
[PROOF STATE]
proof (prove)
using this:
lin_red G p q

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

goal (1 subgoal):
 1. lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
g \<in> G
[PROOF STEP]
have "g \<in> F \<union> G"
[PROOF STATE]
proof (prove)
using this:
g \<in> G

goal (1 subgoal):
 1. g \<in> F \<union> G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g \<in> F \<union> G

goal (1 subgoal):
 1. lin_red G p q \<Longrightarrow> lin_red (F \<union> G) p q
[PROOF STEP]
from this r
[PROOF STATE]
proof (chain)
picking this:
g \<in> F \<union> G
red_single p q g (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g \<in> F \<union> G
red_single p q g (0::'a)

goal (1 subgoal):
 1. lin_red (F \<union> G) p q
[PROOF STEP]
by (rule lin_redI)
[PROOF STATE]
proof (state)
this:
lin_red (F \<union> G) p q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lin_red (F \<union> G) p q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lin_red_imp_red_rtrancl:
  assumes "(lin_red F)\<^sup>*\<^sup>* p q"
  shows "(red F)\<^sup>*\<^sup>* p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (red F)\<^sup>*\<^sup>* p q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(lin_red F)\<^sup>*\<^sup>* p q

goal (1 subgoal):
 1. (red F)\<^sup>*\<^sup>* p q
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (red F)\<^sup>*\<^sup>* p p
 2. \<And>y z. \<lbrakk>(lin_red F)\<^sup>*\<^sup>* p y; lin_red F y z; (red F)\<^sup>*\<^sup>* p y\<rbrakk> \<Longrightarrow> (red F)\<^sup>*\<^sup>* p z
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (red F)\<^sup>*\<^sup>* p p
 2. \<And>y z. \<lbrakk>(lin_red F)\<^sup>*\<^sup>* p y; lin_red F y z; (red F)\<^sup>*\<^sup>* p y\<rbrakk> \<Longrightarrow> (red F)\<^sup>*\<^sup>* p z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (red F)\<^sup>*\<^sup>* p p
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(red F)\<^sup>*\<^sup>* p p

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(lin_red F)\<^sup>*\<^sup>* p y; lin_red F y z; (red F)\<^sup>*\<^sup>* p y\<rbrakk> \<Longrightarrow> (red F)\<^sup>*\<^sup>* p z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(lin_red F)\<^sup>*\<^sup>* p y; lin_red F y z; (red F)\<^sup>*\<^sup>* p y\<rbrakk> \<Longrightarrow> (red F)\<^sup>*\<^sup>* p z
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
(lin_red F)\<^sup>*\<^sup>* p y
lin_red F y z
(red F)\<^sup>*\<^sup>* p y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(lin_red F)\<^sup>*\<^sup>* p y; lin_red F y z; (red F)\<^sup>*\<^sup>* p y\<rbrakk> \<Longrightarrow> (red F)\<^sup>*\<^sup>* p z
[PROOF STEP]
from step(2)
[PROOF STATE]
proof (chain)
picking this:
lin_red F y z
[PROOF STEP]
have "red F y z"
[PROOF STATE]
proof (prove)
using this:
lin_red F y z

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

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(lin_red F)\<^sup>*\<^sup>* p y; lin_red F y z; (red F)\<^sup>*\<^sup>* p y\<rbrakk> \<Longrightarrow> (red F)\<^sup>*\<^sup>* p z
[PROOF STEP]
with step(3)
[PROOF STATE]
proof (chain)
picking this:
(red F)\<^sup>*\<^sup>* p y
red F y z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(red F)\<^sup>*\<^sup>* p y
red F y z

goal (1 subgoal):
 1. (red F)\<^sup>*\<^sup>* p z
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(red F)\<^sup>*\<^sup>* p z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phull_closed_lin_red:
  assumes "phull B \<subseteq> phull A" and "p \<in> phull A" and "lin_red B p q"
  shows "q \<in> phull A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> phull A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> phull A
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
lin_red B p q
[PROOF STEP]
obtain f where "f \<in> B" and "red_single p q f 0"
[PROOF STATE]
proof (prove)
using this:
lin_red B p q

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

goal (1 subgoal):
 1. q \<in> phull A
[PROOF STEP]
hence q: "q = p - (lookup p (lt f) / lc f) \<cdot> f"
[PROOF STATE]
proof (prove)
using this:
f \<in> B
red_single p q f (0::'a)

goal (1 subgoal):
 1. q = p - (lookup p (lt f) / lc f) \<cdot> f
[PROOF STEP]
by (simp add: red_single_def term_simps map_scale_eq_monom_mult)
[PROOF STATE]
proof (state)
this:
q = p - (lookup p (lt f) / lc f) \<cdot> f

goal (1 subgoal):
 1. q \<in> phull A
[PROOF STEP]
have "q - p \<in> phull B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q - p \<in> phull B
[PROOF STEP]
by (simp add: q, rule phull.span_neg, rule phull.span_scale, rule phull.span_base, fact \<open>f \<in> B\<close>)
[PROOF STATE]
proof (state)
this:
q - p \<in> phull B

goal (1 subgoal):
 1. q \<in> phull A
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
phull B \<subseteq> phull A
q - p \<in> phull B
[PROOF STEP]
have "q - p \<in> phull A"
[PROOF STATE]
proof (prove)
using this:
phull B \<subseteq> phull A
q - p \<in> phull B

goal (1 subgoal):
 1. q - p \<in> phull A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
q - p \<in> phull A

goal (1 subgoal):
 1. q \<in> phull A
[PROOF STEP]
from this assms(2)
[PROOF STATE]
proof (chain)
picking this:
q - p \<in> phull A
p \<in> phull A
[PROOF STEP]
have "(q - p) + p \<in> phull A"
[PROOF STATE]
proof (prove)
using this:
q - p \<in> phull A
p \<in> phull A

goal (1 subgoal):
 1. q - p + p \<in> phull A
[PROOF STEP]
by (rule phull.span_add)
[PROOF STATE]
proof (state)
this:
q - p + p \<in> phull A

goal (1 subgoal):
 1. q \<in> phull A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
q - p + p \<in> phull A

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Macaulay_red_alt:
  "Macaulay_red (Keys_to_list fs) fs = filter (\<lambda>p. lt p \<notin> lt_set (set fs)) (Macaulay_list fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Macaulay_red (Keys_to_list fs) fs = filter (\<lambda>p. lt p \<notin> lt_set (set fs)) (Macaulay_list fs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Macaulay_red (Keys_to_list fs) fs = filter (\<lambda>p. lt p \<notin> lt_set (set fs)) (Macaulay_list fs)
[PROOF STEP]
have "{x \<in> set fs. x \<noteq> 0} = set fs - {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> set fs. x \<noteq> 0} = set fs - {0}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{x \<in> set fs. x \<noteq> 0} = set fs - {0}

goal (1 subgoal):
 1. Macaulay_red (Keys_to_list fs) fs = filter (\<lambda>p. lt p \<notin> lt_set (set fs)) (Macaulay_list fs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{x \<in> set fs. x \<noteq> 0} = set fs - {0}

goal (1 subgoal):
 1. Macaulay_red (Keys_to_list fs) fs = filter (\<lambda>p. lt p \<notin> lt_set (set fs)) (Macaulay_list fs)
[PROOF STEP]
by (simp add: Macaulay_red_def Macaulay_list_def Macaulay_mat_def lt_set_def Let_def)
[PROOF STATE]
proof (state)
this:
Macaulay_red (Keys_to_list fs) fs = filter (\<lambda>p. lt p \<notin> lt_set (set fs)) (Macaulay_list fs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_Macaulay_red:
  "set (Macaulay_red (Keys_to_list fs) fs) = set (Macaulay_list fs) - {p. lt p \<in> lt_set (set fs)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Macaulay_red (Keys_to_list fs) fs) = set (Macaulay_list fs) - {p. lt p \<in> lt_set (set fs)}
[PROOF STEP]
by (auto simp add: Macaulay_red_alt)


[STATEMENT]
lemma Keys_Macaulay_red: "Keys (set (Macaulay_red (Keys_to_list fs) fs)) \<subseteq> Keys (set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Keys (set (Macaulay_red (Keys_to_list fs) fs)) \<subseteq> Keys (set fs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Keys (set (Macaulay_red (Keys_to_list fs) fs)) \<subseteq> Keys (set fs)
[PROOF STEP]
have "Keys (set (Macaulay_red (Keys_to_list fs) fs)) \<subseteq> Keys (set (Macaulay_list fs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Keys (set (Macaulay_red (Keys_to_list fs) fs)) \<subseteq> Keys (set (Macaulay_list fs))
[PROOF STEP]
unfolding set_Macaulay_red
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Keys (set (Macaulay_list fs) - {p. lt p \<in> lt_set (set fs)}) \<subseteq> Keys (set (Macaulay_list fs))
[PROOF STEP]
by (fact Keys_minus)
[PROOF STATE]
proof (state)
this:
Keys (set (Macaulay_red (Keys_to_list fs) fs)) \<subseteq> Keys (set (Macaulay_list fs))

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed