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

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

goal (2 subgoals):
 1. \<And>ks fs. Keys (set fs) = set ks \<union> set [] \<Longrightarrow> set (fst (ks, fs)) = Keys (set (snd (ks, fs)))
 2. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; Keys (set (snd (sym_preproc_addnew gs vs' fs v))) = set (ks @ [v]) \<union> set (fst (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> set (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))) = Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); Keys (set fs) = set ks \<union> set vs\<rbrakk> \<Longrightarrow> set (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))) = Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Keys (set fs) = set ks \<union> set []

goal (1 subgoal):
 1. set (fst (ks, fs)) = Keys (set (snd (ks, fs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (fst (ks, fs)) = Keys (set (snd (ks, fs)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; Keys (set (snd (sym_preproc_addnew gs vs' fs v))) = set (ks @ [v]) \<union> set (fst (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> set (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))) = Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))); Keys (set fs) = set ks \<union> set vs\<rbrakk> \<Longrightarrow> set (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))) = Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))))
[PROOF STEP]
have "... = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> insert v (set vs') = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
by (fact Keys_snd_sym_preproc_addnew)
[PROOF STATE]
proof (state)
this:
Keys (set (snd (sym_preproc_addnew gs vs' fs v))) \<union> insert v (set vs') = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. set (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))) = Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))))
[PROOF STEP]
by (rule rec(4))
[PROOF STATE]
proof (state)
this:
set (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))) = Keys (set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))))

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (induct gs ks vs fs arbitrary: thesis rule: sym_preproc_aux_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ks fs thesis. \<lbrakk>p \<in> set (snd (ks, fs)); p \<in> set fs \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<And>ks vs fs v vs' thesis. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<And>thesis. \<lbrakk>p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set (snd (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set fs \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (base ks fs)
[PROOF STATE]
proof (state)
this:
p \<in> set (snd (ks, fs))
p \<in> set fs \<Longrightarrow> thesis
\<lbrakk>?g100 \<in> set gs; p = monom_mult (1::'b) ?t100 ?g100\<rbrakk> \<Longrightarrow> thesis

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

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>ks fs thesis. \<lbrakk>p \<in> set (snd (ks, fs)); p \<in> set fs \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<And>ks vs fs v vs' thesis. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<And>thesis. \<lbrakk>p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set (snd (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set fs \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t 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 base(2))
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>ks vs fs v vs' thesis. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<And>thesis. \<lbrakk>p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set (snd (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set fs \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ks vs fs v vs' thesis. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<And>thesis. \<lbrakk>p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set (snd (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set fs \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (rec ks vs fs v vs')
[PROOF STATE]
proof (state)
this:
vs \<noteq> []
v = ord_term_lin.Max (set vs)
vs' = removeAll v vs
\<lbrakk>p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set (snd (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> ?thesis100; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> ?thesis100\<rbrakk> \<Longrightarrow> ?thesis100
p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
p \<in> set fs \<Longrightarrow> thesis
\<lbrakk>?g100 \<in> set gs; p = monom_mult (1::'b) ?t100 ?g100\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>ks vs fs v vs' thesis. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<And>thesis. \<lbrakk>p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set (snd (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); p \<in> set fs \<Longrightarrow> thesis; \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from rec(5)
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule rec(4))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> set (snd (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> thesis
 2. \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<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 (2 subgoals):
 1. p \<in> set (snd (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow> thesis
 2. \<And>g t. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) t g\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> set (snd (sym_preproc_addnew gs vs' fs v))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule in_snd_sym_preproc_addnewE)
[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]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> set fs

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule rec(6))
[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 g 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 "g \<in> set gs" and "p = monom_mult 1 s g"
[PROOF STATE]
proof (state)
this:
g \<in> set gs
p = monom_mult (1::'b) s g

goal (1 subgoal):
 1. \<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:
g \<in> set gs
p = monom_mult (1::'b) s g

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

goal (1 subgoal):
 1. pmdl (set gs \<union> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) = pmdl (set gs \<union> set fs)
[PROOF STEP]
by (rule trans)
[PROOF STATE]
proof (state)
this:
pmdl (set gs \<union> set (snd (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))) = pmdl (set gs \<union> set fs)

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` Keys (set gs) \<union> pp_of_term ` Keys (set fs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` Keys (set gs) \<union> pp_of_term ` Keys (set fs))
[PROOF STEP]
have "dgrad_set_le d (pp_of_term ` Keys (set (snd ?n))) (pp_of_term ` (Keys (set fs) \<union> insert v (set (fst ?n))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` (Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))))
[PROOF STEP]
by (rule dgrad_set_le_subset, auto simp only: Keys_snd_sym_preproc_addnew[symmetric])
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` (Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v)))))

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

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` Keys (set gs) \<union> pp_of_term ` Keys (set fs))
[PROOF STEP]
have "dgrad_set_le d ... (pp_of_term ` Keys (set fs) \<union> 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 ` (Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew gs vs' fs v))))) (pp_of_term ` Keys (set fs) \<union> pp_of_term ` (Keys (set gs) \<union> insert v (set vs')))
[PROOF STEP]
proof (simp only: dgrad_set_le_Un image_Un, rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dgrad_set_le d (pp_of_term ` Keys (set fs)) (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))
 2. dgrad_set_le d (pp_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))
[PROOF STEP]
show "dgrad_set_le d (pp_of_term ` Keys (set fs))
            (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` Keys (set fs)) (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))
[PROOF STEP]
by (rule dgrad_set_le_subset, blast)
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` Keys (set fs)) (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))
[PROOF STEP]
have "dgrad_set_le d (pp_of_term ` {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 ` {v}) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs')))
[PROOF STEP]
by (rule dgrad_set_le_subset, simp)
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` {v}) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs')))

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

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
dickson_grading d
[PROOF STEP]
have "dgrad_set_le d (pp_of_term ` set (fst ?n)) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs')))"
[PROOF STATE]
proof (prove)
using this:
dickson_grading d

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]
by (rule fst_sym_preproc_addnew_dgrad_set_le)
[PROOF STATE]
proof (state)
this:
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')))

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dgrad_set_le d (pp_of_term ` {v}) (pp_of_term ` (Keys (set gs) \<union> insert v (set 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')))
[PROOF STEP]
have "dgrad_set_le d (pp_of_term ` ({v} \<union> set (fst ?n))) (pp_of_term ` (Keys (set gs) \<union> insert v (set vs')))"
[PROOF STATE]
proof (prove)
using this:
dgrad_set_le d (pp_of_term ` {v}) (pp_of_term ` (Keys (set gs) \<union> insert v (set 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')))

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

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

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` insert v (set (fst (sym_preproc_addnew gs vs' fs v)))) (pp_of_term ` Keys (set fs) \<union> (pp_of_term ` Keys (set gs) \<union> pp_of_term ` insert v (set vs')))
[PROOF STEP]
have "dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set vs')))
                                (pp_of_term ` (Keys (set fs) \<union> (Keys (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 vs'))) (pp_of_term ` (Keys (set fs) \<union> (Keys (set gs) \<union> insert v (set vs'))))
[PROOF STEP]
by (rule dgrad_set_le_subset, blast)
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` (Keys (set gs) \<union> insert v (set vs'))) (pp_of_term ` (Keys (set fs) \<union> (Keys (set gs) \<union> insert v (set vs'))))

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed