[STATEMENT]
lemma fst_sym_preproc_addnew_less:
  assumes "\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v"
    and "u \<in> set (fst (sym_preproc_addnew gs vs fs v))"
  shows "u \<prec>\<^sub>t v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?u95 \<in> set vs \<Longrightarrow> ?u95 \<prec>\<^sub>t v
u \<in> set (fst (sym_preproc_addnew gs vs fs v))

goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
proof (induct gs arbitrary: fs vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fs vs. \<lbrakk>\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew [] vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
 2. \<And>a gs fs vs. \<lbrakk>\<And>fs vs. \<lbrakk>\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v; \<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew (a # gs) vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
?u95 \<in> set vs \<Longrightarrow> ?u95 \<prec>\<^sub>t v
u \<in> set (fst (sym_preproc_addnew [] vs fs v))

goal (2 subgoals):
 1. \<And>fs vs. \<lbrakk>\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew [] vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
 2. \<And>a gs fs vs. \<lbrakk>\<And>fs vs. \<lbrakk>\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v; \<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew (a # gs) vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
from Nil(2)
[PROOF STATE]
proof (chain)
picking this:
u \<in> set (fst (sym_preproc_addnew [] vs fs v))
[PROOF STEP]
have "u \<in> set vs"
[PROOF STATE]
proof (prove)
using this:
u \<in> set (fst (sym_preproc_addnew [] vs fs v))

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

goal (2 subgoals):
 1. \<And>fs vs. \<lbrakk>\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew [] vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
 2. \<And>a gs fs vs. \<lbrakk>\<And>fs vs. \<lbrakk>\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v; \<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew (a # gs) vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
u \<in> set vs

goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
by (rule Nil(1))
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t v

goal (1 subgoal):
 1. \<And>a gs fs vs. \<lbrakk>\<And>fs vs. \<lbrakk>\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v; \<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew (a # gs) vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a gs fs vs. \<lbrakk>\<And>fs vs. \<lbrakk>\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v; \<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew (a # gs) vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
case (Cons g gs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>u. u \<in> set ?vs95 \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
?u95 \<in> set vs \<Longrightarrow> ?u95 \<prec>\<^sub>t v
u \<in> set (fst (sym_preproc_addnew (g # gs) vs fs v))

goal (1 subgoal):
 1. \<And>a gs fs vs. \<lbrakk>\<And>fs vs. \<lbrakk>\<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v; \<And>u. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v; u \<in> set (fst (sym_preproc_addnew (a # gs) vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
from Cons(3)
[PROOF STATE]
proof (chain)
picking this:
u \<in> set (fst (sym_preproc_addnew (g # gs) vs fs v))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
u \<in> set (fst (sym_preproc_addnew (g # gs) vs fs v))

goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
proof (simp add: Let_def split: if_splits)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
 2. \<lbrakk>\<not> lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
let ?t = "pp_of_term v - lp g"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
 2. \<lbrakk>\<not> lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
assume "lt g adds\<^sub>t v"
[PROOF STATE]
proof (state)
this:
lt g adds\<^sub>t v

goal (2 subgoals):
 1. \<lbrakk>lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
 2. \<lbrakk>\<not> lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
assume "u \<in> set (fst (sym_preproc_addnew gs
                                (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult 1 ?t g))))
                                (insert_list (monom_mult 1 ?t g) fs) v))"
[PROOF STATE]
proof (state)
this:
u \<in> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))

goal (2 subgoals):
 1. \<lbrakk>lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
 2. \<lbrakk>\<not> lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
with _
[PROOF STATE]
proof (chain)
picking this:
PROP ?psi \<Longrightarrow> PROP ?psi
u \<in> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
u \<in> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))

goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
proof (rule Cons(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
assume "u \<in> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult 1 ?t g))))"
[PROOF STATE]
proof (state)
this:
u \<in> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))))

goal (1 subgoal):
 1. \<And>u. u \<in> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
hence "u \<in> set vs \<or> u \<in> keys (tail (monom_mult 1 ?t g))"
[PROOF STATE]
proof (prove)
using this:
u \<in> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))))

goal (1 subgoal):
 1. u \<in> set vs \<or> u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))
[PROOF STEP]
by (simp add: set_merge_wrt keys_to_list_def set_pps_to_list)
[PROOF STATE]
proof (state)
this:
u \<in> set vs \<or> u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. \<And>u. u \<in> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
thus "u \<prec>\<^sub>t v"
[PROOF STATE]
proof (prove)
using this:
u \<in> set vs \<or> u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v
 2. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
assume "u \<in> set vs"
[PROOF STATE]
proof (state)
this:
u \<in> set vs

goal (2 subgoals):
 1. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v
 2. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in> set vs

goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
by (rule Cons(2))
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t v

goal (1 subgoal):
 1. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
assume "u \<in> keys (tail (monom_mult 1 ?t g))"
[PROOF STATE]
proof (state)
this:
u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
hence "u \<prec>\<^sub>t lt (monom_mult 1 ?t g)"
[PROOF STATE]
proof (prove)
using this:
u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. u \<prec>\<^sub>t lt (monom_mult (1::'b) (pp_of_term v - lp g) g)
[PROOF STEP]
by (rule keys_tail_less_lt)
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t lt (monom_mult (1::'b) (pp_of_term v - lp g) g)

goal (1 subgoal):
 1. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t lt (monom_mult (1::'b) (pp_of_term v - lp g) g)

goal (1 subgoal):
 1. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
have "... \<preceq>\<^sub>t ?t \<oplus> lt g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt (monom_mult (1::'b) (pp_of_term v - lp g) g) \<preceq>\<^sub>t (pp_of_term v - lp g) \<oplus> lt g
[PROOF STEP]
by (rule lt_monom_mult_le)
[PROOF STATE]
proof (state)
this:
lt (monom_mult (1::'b) (pp_of_term v - lp g) g) \<preceq>\<^sub>t (pp_of_term v - lp g) \<oplus> lt g

goal (1 subgoal):
 1. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lt (monom_mult (1::'b) (pp_of_term v - lp g) g) \<preceq>\<^sub>t (pp_of_term v - lp g) \<oplus> lt g

goal (1 subgoal):
 1. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
from \<open>lt g adds\<^sub>t v\<close>
[PROOF STATE]
proof (chain)
picking this:
lt g adds\<^sub>t v
[PROOF STEP]
have "... = v"
[PROOF STATE]
proof (prove)
using this:
lt g adds\<^sub>t v

goal (1 subgoal):
 1. (pp_of_term v - lp g) \<oplus> lt g = v
[PROOF STEP]
by (metis add_diff_cancel_right' adds_termE pp_of_term_splus)
[PROOF STATE]
proof (state)
this:
(pp_of_term v - lp g) \<oplus> lt g = v

goal (1 subgoal):
 1. u \<in> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u \<prec>\<^sub>t v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<prec>\<^sub>t v

goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t v

goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
assume "u \<in> set (fst (sym_preproc_addnew gs vs fs v))"
[PROOF STATE]
proof (state)
this:
u \<in> set (fst (sym_preproc_addnew gs vs fs v))

goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; u \<in> set (fst (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
with Cons(2)
[PROOF STATE]
proof (chain)
picking this:
?u95 \<in> set vs \<Longrightarrow> ?u95 \<prec>\<^sub>t v
u \<in> set (fst (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?u95 \<in> set vs \<Longrightarrow> ?u95 \<prec>\<^sub>t v
u \<in> set (fst (sym_preproc_addnew gs vs fs v))

goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
by (rule Cons(1))
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fst_sym_preproc_addnew_dgrad_set_le:
  assumes "dickson_grading d"
  shows "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs)))
[PROOF STEP]
proof (induct gs arbitrary: fs vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fs vs. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew [] vs fs v))) (pp_of_term ` (Keys (set []) \<union> insert v (set vs)))
 2. \<And>a gs fs vs. (\<And>fs vs. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs)))) \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v))) (pp_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>fs vs. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew [] vs fs v))) (pp_of_term ` (Keys (set []) \<union> insert v (set vs)))
 2. \<And>a gs fs vs. (\<And>fs vs. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs)))) \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v))) (pp_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew [] vs fs v))) (pp_of_term ` (Keys (set []) \<union> insert v (set vs)))
[PROOF STEP]
by (auto intro: dgrad_set_le_subset)
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew [] vs fs v))) (pp_of_term ` (Keys (set []) \<union> insert v (set vs)))

goal (1 subgoal):
 1. \<And>a gs fs vs. (\<And>fs vs. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs)))) \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v))) (pp_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a gs fs vs. (\<And>fs vs. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs)))) \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v))) (pp_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs)))
[PROOF STEP]
case (Cons g gs)
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set ?vs95)))

goal (1 subgoal):
 1. \<And>a gs fs vs. (\<And>fs vs. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs)))) \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v))) (pp_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew (g # gs) vs fs v))) (pp_of_term ` (Keys (set (g # gs)) \<union> insert v (set vs)))
[PROOF STEP]
proof (simp add: Let_def, intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
assume "lt g adds\<^sub>t v"
[PROOF STATE]
proof (state)
this:
lt g adds\<^sub>t v

goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
let ?t = "pp_of_term v - lp g"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
let ?vs = "merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult 1 ?t g)))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
let ?fs = "insert_list (monom_mult 1 ?t g) fs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set ?vs95)))
[PROOF STEP]
have "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)))
                                    (pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)))"
[PROOF STATE]
proof (prove)
using this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set ?vs95)))

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)))
[PROOF STEP]
proof (rule dgrad_set_le_trans)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))))))) (pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)))
[PROOF STEP]
show "dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set ?vs)))
                            (pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))))))) (pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)))
[PROOF STEP]
unfolding dgrad_set_le_def set_merge_wrt set_keys_to_list
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>pp_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))). \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
proof (intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
assume "s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult 1 ?t g))))"
[PROOF STATE]
proof (state)
this:
s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))))

goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
hence "s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<union> pp_of_term ` keys (tail (monom_mult 1 ?t g))"
[PROOF STATE]
proof (prove)
using this:
s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))))

goal (1 subgoal):
 1. s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<union> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<union> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. \<And>s. s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
thus "\<exists>t \<in> pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t"
[PROOF STATE]
proof (prove)
using this:
s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<union> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
 2. s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
assume "s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs))"
[PROOF STATE]
proof (state)
this:
s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs))

goal (2 subgoals):
 1. s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
 2. s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> pp_of_term ` (Keys (set gs) \<union> insert v (set vs))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
by (auto simp add: Keys_insert)
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t

goal (1 subgoal):
 1. s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
assume "s \<in> pp_of_term ` keys (tail (monom_mult 1 ?t g))"
[PROOF STATE]
proof (state)
this:
s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
hence "s \<in> pp_of_term ` keys (monom_mult 1 ?t g)"
[PROOF STATE]
proof (prove)
using this:
s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. s \<in> pp_of_term ` keys (monom_mult (1::'b) (pp_of_term v - lp g) g)
[PROOF STEP]
by (auto simp add: keys_tail)
[PROOF STATE]
proof (state)
this:
s \<in> pp_of_term ` keys (monom_mult (1::'b) (pp_of_term v - lp g) g)

goal (1 subgoal):
 1. s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
from this keys_monom_mult_subset
[PROOF STATE]
proof (chain)
picking this:
s \<in> pp_of_term ` keys (monom_mult (1::'b) (pp_of_term v - lp g) g)
keys (monom_mult ?c ?t ?p) \<subseteq> (\<oplus>) ?t ` keys ?p
[PROOF STEP]
have "s \<in> pp_of_term ` (\<oplus>) ?t ` keys g"
[PROOF STATE]
proof (prove)
using this:
s \<in> pp_of_term ` keys (monom_mult (1::'b) (pp_of_term v - lp g) g)
keys (monom_mult ?c ?t ?p) \<subseteq> (\<oplus>) ?t ` keys ?p

goal (1 subgoal):
 1. s \<in> pp_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s \<in> pp_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g

goal (1 subgoal):
 1. s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> pp_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g
[PROOF STEP]
obtain u where "u \<in> keys g" and s: "s = pp_of_term (?t \<oplus> u)"
[PROOF STATE]
proof (prove)
using this:
s \<in> pp_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<in> keys g; s = pp_of_term ((pp_of_term v - lp g) \<oplus> u)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<in> keys g
s = pp_of_term ((pp_of_term v - lp g) \<oplus> u)

goal (1 subgoal):
 1. s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
have "d s = d ?t \<or> d s = d (pp_of_term u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d s = d (pp_of_term v - lp g) \<or> d s = d (pp_of_term u)
[PROOF STEP]
unfolding s pp_of_term_splus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (pp_of_term v - lp g + pp_of_term u) = d (pp_of_term v - lp g) \<or> d (pp_of_term v - lp g + pp_of_term u) = d (pp_of_term u)
[PROOF STEP]
using dickson_gradingD1[OF assms]
[PROOF STATE]
proof (prove)
using this:
d (?s + ?t) = ord_class.max (d ?s) (d ?t)

goal (1 subgoal):
 1. d (pp_of_term v - lp g + pp_of_term u) = d (pp_of_term v - lp g) \<or> d (pp_of_term v - lp g + pp_of_term u) = d (pp_of_term u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d s = d (pp_of_term v - lp g) \<or> d s = d (pp_of_term u)

goal (1 subgoal):
 1. s \<in> pp_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
d s = d (pp_of_term v - lp g) \<or> d s = d (pp_of_term u)

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d s = d (pp_of_term v - lp g) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
 2. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
from \<open>lt g adds\<^sub>t v\<close>
[PROOF STATE]
proof (chain)
picking this:
lt g adds\<^sub>t v
[PROOF STEP]
have "lp g adds pp_of_term v"
[PROOF STATE]
proof (prove)
using this:
lt g adds\<^sub>t v

goal (1 subgoal):
 1. lp g adds pp_of_term v
[PROOF STEP]
by (simp add: adds_term_def)
[PROOF STATE]
proof (state)
this:
lp g adds pp_of_term v

goal (2 subgoals):
 1. d s = d (pp_of_term v - lp g) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
 2. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
assume "d s = d ?t"
[PROOF STATE]
proof (state)
this:
d s = d (pp_of_term v - lp g)

goal (2 subgoals):
 1. d s = d (pp_of_term v - lp g) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
 2. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d s = d (pp_of_term v - lp g)

goal (2 subgoals):
 1. d s = d (pp_of_term v - lp g) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
 2. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
from assms \<open>lp g adds pp_of_term v\<close>
[PROOF STATE]
proof (chain)
picking this:
dickson_grading d
lp g adds pp_of_term v
[PROOF STEP]
have "... \<le> d (pp_of_term v)"
[PROOF STATE]
proof (prove)
using this:
dickson_grading d
lp g adds pp_of_term v

goal (1 subgoal):
 1. d (pp_of_term v - lp g) \<le> d (pp_of_term v)
[PROOF STEP]
by (rule dickson_grading_minus)
[PROOF STATE]
proof (state)
this:
d (pp_of_term v - lp g) \<le> d (pp_of_term v)

goal (2 subgoals):
 1. d s = d (pp_of_term v - lp g) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
 2. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d s \<le> d (pp_of_term v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d s \<le> d (pp_of_term v)

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t

goal (1 subgoal):
 1. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
assume "d s = d (pp_of_term u)"
[PROOF STATE]
proof (state)
this:
d s = d (pp_of_term u)

goal (1 subgoal):
 1. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d s = d (pp_of_term u)

goal (1 subgoal):
 1. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
from \<open>u \<in> keys g\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> keys g
[PROOF STEP]
have "u \<in> Keys (insert g (set gs))"
[PROOF STATE]
proof (prove)
using this:
u \<in> keys g

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

goal (1 subgoal):
 1. d s = d (pp_of_term u) \<Longrightarrow> \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
d s = d (pp_of_term u)
u \<in> Keys (insert g (set gs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d s = d (pp_of_term u)
u \<in> Keys (insert g (set gs))

goal (1 subgoal):
 1. \<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)). d s \<le> d t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))))))) (pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)))

goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
thus "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)))
                        (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))"
[PROOF STATE]
proof (prove)
using this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (pp_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs)))

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))

goal (1 subgoal):
 1. \<not> lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lt g adds\<^sub>t v \<Longrightarrow> dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set ?vs95)))
[PROOF STEP]
show "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v)))
                           (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))"
[PROOF STATE]
proof (prove)
using this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v))) (pp_of_term ` (Keys (set gs) \<union> insert v (set ?vs95)))

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
proof (rule dgrad_set_le_trans)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set vs))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
show "dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set vs)))
                          (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set vs))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))
[PROOF STEP]
by (rule dgrad_set_le_subset, auto simp add: Keys_def)
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set vs))) (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) \<union> set vs)))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew (g # gs) vs fs v))) (pp_of_term ` (Keys (set (g # gs)) \<union> insert v (set vs)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma components_fst_sym_preproc_addnew_subset:
  "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 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]
proof (induct gs arbitrary: fs vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fs vs. component_of_term ` set (fst (sym_preproc_addnew [] vs fs v)) \<subseteq> component_of_term ` (Keys (set []) \<union> insert v (set vs))
 2. \<And>a gs fs vs. (\<And>fs 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))) \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v)) \<subseteq> component_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>fs vs. component_of_term ` set (fst (sym_preproc_addnew [] vs fs v)) \<subseteq> component_of_term ` (Keys (set []) \<union> insert v (set vs))
 2. \<And>a gs fs vs. (\<And>fs 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))) \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v)) \<subseteq> component_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` set (fst (sym_preproc_addnew [] vs fs v)) \<subseteq> component_of_term ` (Keys (set []) \<union> insert v (set vs))
[PROOF STEP]
by (auto intro: dgrad_set_le_subset)
[PROOF STATE]
proof (state)
this:
component_of_term ` set (fst (sym_preproc_addnew [] vs fs v)) \<subseteq> component_of_term ` (Keys (set []) \<union> insert v (set vs))

goal (1 subgoal):
 1. \<And>a gs fs vs. (\<And>fs 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))) \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v)) \<subseteq> component_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a gs fs vs. (\<And>fs 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))) \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v)) \<subseteq> component_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs))
[PROOF STEP]
case (Cons g gs)
[PROOF STATE]
proof (state)
this:
component_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set ?vs95))

goal (1 subgoal):
 1. \<And>a gs fs vs. (\<And>fs 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))) \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew (a # gs) vs fs v)) \<subseteq> component_of_term ` (Keys (set (a # gs)) \<union> insert v (set vs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` set (fst (sym_preproc_addnew (g # gs) vs fs v)) \<subseteq> component_of_term ` (Keys (set (g # gs)) \<union> insert v (set vs))
[PROOF STEP]
proof (simp add: Let_def, intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
assume "lt g adds\<^sub>t v"
[PROOF STATE]
proof (state)
this:
lt g adds\<^sub>t v

goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
let ?t = "pp_of_term v - lp g"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
let ?vs = "merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult 1 ?t g)))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
let ?fs = "insert_list (monom_mult 1 ?t g) fs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
component_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set ?vs95))
[PROOF STEP]
have "component_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)) \<subseteq>
                     component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))"
[PROOF STATE]
proof (prove)
using this:
component_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set ?vs95))

goal (1 subgoal):
 1. component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
proof (rule subset_trans)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. component_of_term ` (Keys (set gs) \<union> insert v (set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))))) \<subseteq> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
show "component_of_term ` (Keys (set gs) \<union> insert v (set ?vs)) \<subseteq>
             component_of_term ` (Keys (insert g (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 (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))))) \<subseteq> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
unfolding set_merge_wrt set_keys_to_list
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<subseteq> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> x \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> x \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
assume "k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult 1 ?t g))))"
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))))

goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> x \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
hence "k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<union> component_of_term ` keys (tail (monom_mult 1 ?t g))"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))))

goal (1 subgoal):
 1. k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<union> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<union> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. \<And>x. x \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs \<union> keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) \<Longrightarrow> x \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
thus "k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<union> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
 2. k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
assume "k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs))"
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs))

goal (2 subgoals):
 1. k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
 2. k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` (Keys (set gs) \<union> insert v (set vs))

goal (1 subgoal):
 1. k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
by (auto simp add: Keys_insert)
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))

goal (1 subgoal):
 1. k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
assume "k \<in> component_of_term ` keys (tail (monom_mult 1 ?t g))"
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
hence "k \<in> component_of_term ` keys (monom_mult 1 ?t g)"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g))

goal (1 subgoal):
 1. k \<in> component_of_term ` keys (monom_mult (1::'b) (pp_of_term v - lp g) g)
[PROOF STEP]
by (auto simp add: keys_tail)
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` keys (monom_mult (1::'b) (pp_of_term v - lp g) g)

goal (1 subgoal):
 1. k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
from this keys_monom_mult_subset
[PROOF STATE]
proof (chain)
picking this:
k \<in> component_of_term ` keys (monom_mult (1::'b) (pp_of_term v - lp g) g)
keys (monom_mult ?c ?t ?p) \<subseteq> (\<oplus>) ?t ` keys ?p
[PROOF STEP]
have "k \<in> component_of_term ` (\<oplus>) ?t ` keys g"
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` keys (monom_mult (1::'b) (pp_of_term v - lp g) g)
keys (monom_mult ?c ?t ?p) \<subseteq> (\<oplus>) ?t ` keys ?p

goal (1 subgoal):
 1. k \<in> component_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g

goal (1 subgoal):
 1. k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g

goal (1 subgoal):
 1. k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
have "... \<subseteq> component_of_term ` keys g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g \<subseteq> component_of_term ` keys g
[PROOF STEP]
using component_of_term_splus
[PROOF STATE]
proof (prove)
using this:
component_of_term (?t \<oplus> ?v) = component_of_term ?v

goal (1 subgoal):
 1. component_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g \<subseteq> component_of_term ` keys g
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
component_of_term ` (\<oplus>) (pp_of_term v - lp g) ` keys g \<subseteq> component_of_term ` keys g

goal (1 subgoal):
 1. k \<in> component_of_term ` keys (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)) \<Longrightarrow> k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
k \<in> component_of_term ` keys g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<in> component_of_term ` keys g

goal (1 subgoal):
 1. k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))
[PROOF STEP]
by (simp add: image_Un Keys_insert)
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<in> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
component_of_term ` (Keys (set gs) \<union> insert v (set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))))) \<subseteq> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))

goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
thus "component_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)) \<subseteq>
           insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))"
[PROOF STATE]
proof (prove)
using this:
component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> component_of_term ` (Keys (insert g (set gs)) \<union> insert v (set vs))

goal (1 subgoal):
 1. component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
component_of_term ` set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))

goal (1 subgoal):
 1. \<not> lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lt g adds\<^sub>t v \<Longrightarrow> component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
component_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set ?vs95))
[PROOF STEP]
show "component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq>
                insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))"
[PROOF STATE]
proof (prove)
using this:
component_of_term ` set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v)) \<subseteq> component_of_term ` (Keys (set gs) \<union> insert v (set ?vs95))

goal (1 subgoal):
 1. component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
proof (rule subset_trans)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
show "component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<subseteq>
             insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))
[PROOF STEP]
by (auto simp add: Keys_def)
[PROOF STATE]
proof (state)
this:
component_of_term ` (Keys (set gs) \<union> insert v (set vs)) \<subseteq> insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) \<union> set vs))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fst_sym_preproc_addnew_superset: "set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
proof (induct gs arbitrary: vs fs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs fs. set vs \<subseteq> set (fst (sym_preproc_addnew [] vs fs v))
 2. \<And>a gs vs fs. (\<And>vs fs. set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>vs fs. set vs \<subseteq> set (fst (sym_preproc_addnew [] vs fs v))
 2. \<And>a gs vs fs. (\<And>vs fs. set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set vs \<subseteq> set (fst (sym_preproc_addnew [] vs fs v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set vs \<subseteq> set (fst (sym_preproc_addnew [] vs fs v))

goal (1 subgoal):
 1. \<And>a gs vs fs. (\<And>vs fs. set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a gs vs fs. (\<And>vs fs. set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
case (Cons g gs)
[PROOF STATE]
proof (state)
this:
set ?vs95 \<subseteq> set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v))

goal (1 subgoal):
 1. \<And>a gs vs fs. (\<And>vs fs. set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set vs \<subseteq> set (fst (sym_preproc_addnew (g # gs) vs fs v))
[PROOF STEP]
proof (simp add: Let_def, intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
let ?t = "pp_of_term v - lp g"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
define f where "f = monom_mult 1 ?t g"
[PROOF STATE]
proof (state)
this:
f = monom_mult (1::'b) (pp_of_term v - lp g) g

goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
have "set vs \<subseteq> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set vs \<subseteq> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f)))
[PROOF STEP]
by (auto simp add: set_merge_wrt)
[PROOF STATE]
proof (state)
this:
set vs \<subseteq> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f)))

goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
thus "set vs \<subseteq> set (fst (sym_preproc_addnew gs
                              (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))) (insert_list f fs) v))"
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f)))

goal (1 subgoal):
 1. set vs \<subseteq> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))) (insert_list f fs) v))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> set (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f)))
set ?vs95 \<subseteq> set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v))

goal (1 subgoal):
 1. set vs \<subseteq> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))) (insert_list f fs) v))
[PROOF STEP]
by (rule subset_trans)
[PROOF STATE]
proof (state)
this:
set vs \<subseteq> set (fst (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))) (insert_list f fs) v))

goal (1 subgoal):
 1. \<not> lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lt g adds\<^sub>t v \<Longrightarrow> set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
show "set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
by (fact Cons)
[PROOF STATE]
proof (state)
this:
set vs \<subseteq> set (fst (sym_preproc_addnew gs vs fs v))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set vs \<subseteq> set (fst (sym_preproc_addnew (g # gs) vs fs v))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma snd_sym_preproc_addnew_superset: "set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
proof (induct gs arbitrary: vs fs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs fs. set fs \<subseteq> set (snd (sym_preproc_addnew [] vs fs v))
 2. \<And>a gs vs fs. (\<And>vs fs. set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>vs fs. set fs \<subseteq> set (snd (sym_preproc_addnew [] vs fs v))
 2. \<And>a gs vs fs. (\<And>vs fs. set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set fs \<subseteq> set (snd (sym_preproc_addnew [] vs fs v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set fs \<subseteq> set (snd (sym_preproc_addnew [] vs fs v))

goal (1 subgoal):
 1. \<And>a gs vs fs. (\<And>vs fs. set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a gs vs fs. (\<And>vs fs. set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
case (Cons g gs)
[PROOF STATE]
proof (state)
this:
set ?fs95 \<subseteq> set (snd (sym_preproc_addnew gs ?vs95 ?fs95 v))

goal (1 subgoal):
 1. \<And>a gs vs fs. (\<And>vs fs. set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))) \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set fs \<subseteq> set (snd (sym_preproc_addnew (g # gs) vs fs v))
[PROOF STEP]
proof (simp add: Let_def, intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
let ?t = "pp_of_term v - lp g"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
define f where "f = monom_mult 1 ?t g"
[PROOF STATE]
proof (state)
this:
f = monom_mult (1::'b) (pp_of_term v - lp g) g

goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
have "set fs \<subseteq> set (insert_list f fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set fs \<subseteq> set (insert_list f fs)
[PROOF STEP]
by (auto simp add: set_insert_list)
[PROOF STATE]
proof (state)
this:
set fs \<subseteq> set (insert_list f fs)

goal (2 subgoals):
 1. lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))
 2. \<not> lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
thus "set fs \<subseteq> set (snd (sym_preproc_addnew gs
                              (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))) (insert_list f fs) v))"
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> set (insert_list f fs)

goal (1 subgoal):
 1. set fs \<subseteq> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))) (insert_list f fs) v))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> set (insert_list f fs)
set ?fs95 \<subseteq> set (snd (sym_preproc_addnew gs ?vs95 ?fs95 v))

goal (1 subgoal):
 1. set fs \<subseteq> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))) (insert_list f fs) v))
[PROOF STEP]
by (rule subset_trans)
[PROOF STATE]
proof (state)
this:
set fs \<subseteq> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))) (insert_list f fs) v))

goal (1 subgoal):
 1. \<not> lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lt g adds\<^sub>t v \<Longrightarrow> set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
show "set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
by (fact Cons)
[PROOF STATE]
proof (state)
this:
set fs \<subseteq> set (snd (sym_preproc_addnew gs vs fs v))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_snd_sym_preproc_addnewE:
  assumes "p \<in> set (snd (sym_preproc_addnew gs vs fs v))"
  assumes 1: "p \<in> set fs \<Longrightarrow> thesis"
  assumes 2: "\<And>g s. g \<in> set gs \<Longrightarrow> p = monom_mult 1 s 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_addnew gs vs fs v))
p \<in> set fs \<Longrightarrow> thesis
\<lbrakk>?g95 \<in> set gs; p = monom_mult (1::'b) ?s95 ?g95\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (induct gs arbitrary: vs fs thesis)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs fs thesis. \<lbrakk>p \<in> set (snd (sym_preproc_addnew [] vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set []; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a gs vs fs thesis. \<lbrakk>\<And>vs fs thesis. \<lbrakk>p \<in> set (snd (sym_preproc_addnew gs vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_addnew (a # gs) vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set (a # gs); p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
p \<in> set (snd (sym_preproc_addnew [] vs fs v))
p \<in> set fs \<Longrightarrow> thesis
\<lbrakk>?g95 \<in> set []; p = monom_mult (1::'b) ?s95 ?g95\<rbrakk> \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<And>vs fs thesis. \<lbrakk>p \<in> set (snd (sym_preproc_addnew [] vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set []; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a gs vs fs thesis. \<lbrakk>\<And>vs fs thesis. \<lbrakk>p \<in> set (snd (sym_preproc_addnew gs vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_addnew (a # gs) vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set (a # gs); p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from Nil(1)
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (snd (sym_preproc_addnew [] vs fs v))
[PROOF STEP]
have "p \<in> set fs"
[PROOF STATE]
proof (prove)
using this:
p \<in> set (snd (sym_preproc_addnew [] vs fs v))

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

goal (2 subgoals):
 1. \<And>vs fs thesis. \<lbrakk>p \<in> set (snd (sym_preproc_addnew [] vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set []; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a gs vs fs thesis. \<lbrakk>\<And>vs fs thesis. \<lbrakk>p \<in> set (snd (sym_preproc_addnew gs vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_addnew (a # gs) vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set (a # gs); p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> set fs

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

goal (1 subgoal):
 1. \<And>a gs vs fs thesis. \<lbrakk>\<And>vs fs thesis. \<lbrakk>p \<in> set (snd (sym_preproc_addnew gs vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_addnew (a # gs) vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set (a # gs); p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a gs vs fs thesis. \<lbrakk>\<And>vs fs thesis. \<lbrakk>p \<in> set (snd (sym_preproc_addnew gs vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_addnew (a # gs) vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set (a # gs); p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Cons g gs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>p \<in> set (snd (sym_preproc_addnew gs ?vs95 ?fs95 v)); p \<in> set ?fs95 \<Longrightarrow> ?thesis95; \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> ?thesis95\<rbrakk> \<Longrightarrow> ?thesis95
p \<in> set (snd (sym_preproc_addnew (g # gs) vs fs v))
p \<in> set fs \<Longrightarrow> thesis
\<lbrakk>?g95 \<in> set (g # gs); p = monom_mult (1::'b) ?s95 ?g95\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>a gs vs fs thesis. \<lbrakk>\<And>vs fs thesis. \<lbrakk>p \<in> set (snd (sym_preproc_addnew gs vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_addnew (a # gs) vs fs v)); p \<in> set fs \<Longrightarrow> thesis; \<And>g s. \<lbrakk>g \<in> set (a # gs); p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from Cons(2)
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (snd (sym_preproc_addnew (g # gs) vs fs v))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> set (snd (sym_preproc_addnew (g # gs) vs fs v))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (simp add: Let_def split: if_splits)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
define f where "f = monom_mult 1 (pp_of_term v - lp g) g"
[PROOF STATE]
proof (state)
this:
f = monom_mult (1::'b) (pp_of_term v - lp g) g

goal (2 subgoals):
 1. \<lbrakk>lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
define ts' where "ts' = merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))"
[PROOF STATE]
proof (state)
this:
ts' = merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail f))

goal (2 subgoals):
 1. \<lbrakk>lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
define fs' where "fs' = insert_list f fs"
[PROOF STATE]
proof (state)
this:
fs' = insert_list f fs

goal (2 subgoals):
 1. \<lbrakk>lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "p \<in> set (snd (sym_preproc_addnew gs ts' fs' v))"
[PROOF STATE]
proof (state)
this:
p \<in> set (snd (sym_preproc_addnew gs ts' fs' v))

goal (2 subgoals):
 1. \<lbrakk>lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs (merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult (1::'b) (pp_of_term v - lp g) g)))) (insert_list (monom_mult (1::'b) (pp_of_term v - lp g) g) fs) v))\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> set (snd (sym_preproc_addnew gs ts' fs' v))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule Cons(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> set fs' \<Longrightarrow> thesis
 2. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "p \<in> set fs'"
[PROOF STATE]
proof (state)
this:
p \<in> set fs'

goal (2 subgoals):
 1. p \<in> set fs' \<Longrightarrow> thesis
 2. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "p = f \<or> p \<in> set fs"
[PROOF STATE]
proof (prove)
using this:
p \<in> set fs'

goal (1 subgoal):
 1. p = f \<or> p \<in> set fs
[PROOF STEP]
by (simp add: fs'_def set_insert_list)
[PROOF STATE]
proof (state)
this:
p = f \<or> p \<in> set fs

goal (2 subgoals):
 1. p \<in> set fs' \<Longrightarrow> thesis
 2. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = f \<or> p \<in> set fs

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = f \<Longrightarrow> thesis
 2. p \<in> set fs \<Longrightarrow> thesis
[PROOF STEP]
assume "p = f"
[PROOF STATE]
proof (state)
this:
p = f

goal (2 subgoals):
 1. p = f \<Longrightarrow> thesis
 2. p \<in> set fs \<Longrightarrow> thesis
[PROOF STEP]
have "g \<in> set (g # gs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> set (g # gs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g \<in> set (g # gs)

goal (2 subgoals):
 1. p = f \<Longrightarrow> thesis
 2. p \<in> set fs \<Longrightarrow> thesis
[PROOF STEP]
from this \<open>p = f\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<in> set (g # gs)
p = f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g \<in> set (g # gs)
p = f

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
g \<in> set (g # gs)
p = monom_mult (1::'b) (pp_of_term v - lp g) g

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

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

goal (1 subgoal):
 1. p \<in> set fs \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> set fs

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

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

goal (1 subgoal):
 1. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix h s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "h \<in> set gs"
[PROOF STATE]
proof (state)
this:
h \<in> set gs

goal (1 subgoal):
 1. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "h \<in> set (g # gs)"
[PROOF STATE]
proof (prove)
using this:
h \<in> set gs

goal (1 subgoal):
 1. h \<in> set (g # gs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h \<in> set (g # gs)

goal (1 subgoal):
 1. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
h \<in> set (g # gs)

goal (1 subgoal):
 1. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "p = monom_mult 1 s h"
[PROOF STATE]
proof (state)
this:
p = monom_mult (1::'b) s h

goal (1 subgoal):
 1. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
h \<in> set (g # gs)
p = monom_mult (1::'b) s h
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
h \<in> set (g # gs)
p = monom_mult (1::'b) s h

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

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

goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "p \<in> set (snd (sym_preproc_addnew gs vs fs v))"
[PROOF STATE]
proof (state)
this:
p \<in> set (snd (sym_preproc_addnew gs vs fs v))

goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<in> set (snd (sym_preproc_addnew gs vs fs v))

goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note Cons(3)
[PROOF STATE]
proof (state)
this:
p \<in> set fs \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<in> set fs \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "h \<in> set gs \<Longrightarrow> p = monom_mult 1 s h \<Longrightarrow> thesis" for h s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<in> set gs; p = monom_mult (1::'b) s h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>h \<in> set gs; p = monom_mult (1::'b) s h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "h \<in> set gs"
[PROOF STATE]
proof (state)
this:
h \<in> set gs

goal (1 subgoal):
 1. \<lbrakk>h \<in> set gs; p = monom_mult (1::'b) s h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "h \<in> set (g # gs)"
[PROOF STATE]
proof (prove)
using this:
h \<in> set gs

goal (1 subgoal):
 1. h \<in> set (g # gs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h \<in> set (g # gs)

goal (1 subgoal):
 1. \<lbrakk>h \<in> set gs; p = monom_mult (1::'b) s h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
h \<in> set (g # gs)

goal (1 subgoal):
 1. \<lbrakk>h \<in> set gs; p = monom_mult (1::'b) s h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "p = monom_mult 1 s h"
[PROOF STATE]
proof (state)
this:
p = monom_mult (1::'b) s h

goal (1 subgoal):
 1. \<lbrakk>h \<in> set gs; p = monom_mult (1::'b) s h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
h \<in> set (g # gs)
p = monom_mult (1::'b) s h
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
h \<in> set (g # gs)
p = monom_mult (1::'b) s h

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?h95 \<in> set gs; p = monom_mult (1::'b) ?s95 ?h95\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<lbrakk>\<not> lt g adds\<^sub>t v; p \<in> set (snd (sym_preproc_addnew gs vs fs v))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (snd (sym_preproc_addnew gs vs fs v))
p \<in> set fs \<Longrightarrow> thesis
\<lbrakk>?h95 \<in> set gs; p = monom_mult (1::'b) ?s95 ?h95\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> set (snd (sym_preproc_addnew gs vs fs v))
p \<in> set fs \<Longrightarrow> thesis
\<lbrakk>?h95 \<in> set gs; p = monom_mult (1::'b) ?s95 ?h95\<rbrakk> \<Longrightarrow> thesis

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

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

goal:
No subgoals!
[PROOF STEP]
qed